Merge branch 'main' into proof_of_equivalence_monadic_nonmonadic_CapFns

.github/workflows/ci.yml

@@ -12,7 +12,7 @@ jobs:
  - run: eval $(opam env --switch=default)
  - run: opam repo add --yes --this-switch coq-released https://coq.inria.fr/opam/released
  - run: opam repo add --yes --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git
- - run: opam pin --yes -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git
+ - run: opam pin --yes -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git#f319aad
  - run: opam install --yes ./coq-cheri-capabilities.opam
  - run: eval $(opam env)
 

README.md

@@ -16,7 +16,7 @@ Make sure to run `eval $(opam env --switch=coq-cheri-capabilities)` (or whicheve
 ```
 opam repo add --this-switch coq-released https://coq.inria.fr/opam/released
 opam repo add --this-switch iris-dev https://gitlab.mpi-sws.org/iris/opam.git
-opam pin -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git
+opam pin -n coq-sail-stdpp https://github.com/rems-project/coq-sail.git#f319aad
 ```
 
 4. You may now install the opam package `coq-cheri-capabilities` and its dependencies with

coq-cheri-capabilities.opam

@@ -6,14 +6,13 @@ maintainer: ["ricardo.almeida@ed.ac.uk"]
 authors: ["Ricardo Almeida" "Vadim Zaliva"]
 license: "BSD-3-clause"
 homepage: "https://github.com/rems-project/coq-cheri-capabilities"
-version: "20240521"
+version: "20240611"
 bug-reports: "https://github.com/rems-project/coq-cheri-capabilities/issues"
 depends: [
  "dune" {>= "3.7"}
  "coq"
  "coq-stdpp" { (= "dev") | (>= "dev.2022-12-05.0.0231fed2" & <= "dev.2024-03-11.0.a8c0c0f8") }
  "coq-sail-stdpp"
- "coq-ext-lib"
  "coq-stdpp-unstable"
  "odoc" {with-doc}
 ]

theories/Common/dune

@@ -1,5 +1,5 @@
 (coq.theory
  (name CheriCaps.Common)
  (package coq-cheri-capabilities)
- (theories stdpp SailStdpp ExtLib)
+ (theories stdpp SailStdpp)
 )

theories/Morello/Bv_extensions.v

@@ -0,0 +1,73 @@
+From stdpp.unstable Require Import bitvector bitvector_tactics.
+
+
+Lemma bv_wrap_of_smaller_wrap n m b:
+ (m <= n)%N ->
+ bv_wrap n (bv_wrap m b) = bv_wrap m b.
+Proof.
+ intros ?. rewrite bv_wrap_small; [ reflexivity |].
+ assert (0 ≤ bv_wrap m b < bv_modulus m)%Z by apply bv_wrap_in_range.
+ assert (P: (m <= n)%N) by lia. 
+ apply bv_modulus_le_mono in P. 
+ lia. 
+ Qed.
+
+Lemma bv_wrap_of_larger_wrap_sum n m (b : bv 129) :
+ (m < n)%N -> 
+ bv_wrap m (bv_wrap n (bv_unsigned b) + 16) = bv_wrap m (bv_unsigned b + 16).
+Proof.
+ intros ?.
+ replace (bv_wrap m (bv_wrap n (bv_unsigned b) + 16)) with (bv_wrap m (bv_wrap n ((bv_wrap n (bv_unsigned b) + 16))));
+ [ rewrite bv_wrap_add_idemp_l; rewrite bv_wrap_bv_wrap; [ reflexivity | lia ] 
+ | rewrite bv_wrap_bv_wrap; [ reflexivity | lia ]; reflexivity ].
+ Qed.
+
+Lemma bv_extract_idemp n m (b : bv n) : 
+ bv_extract 0 m (bv_extract 0 m b) = bv_extract 0 m b.
+Proof. 
+ apply bv_eq_wrap. rewrite bv_extract_0_unsigned. 
+ apply bv_wrap_bv_wrap. lia.
+ Qed.
+
+Lemma bv_extract_full n (b : bv n) :
+ bv_extract 0 n b = b.
+Proof. 
+ apply bv_eq_wrap. rewrite bv_extract_0_unsigned. 
+ apply bv_wrap_bv_wrap. lia.
+ Qed.
+
+Global Hint Rewrite bv_wrap_of_smaller_wrap using lia : bv_simplify.
+Global Hint Rewrite bv_wrap_of_larger_wrap_sum using lia : bv_simplify.
+Global Hint Rewrite bv_extract_idemp : bv_simplify.
+Global Hint Rewrite bv_extract_full : bv_simplify.
+Global Hint Rewrite @bv_extract_0_unsigned : bv_simplify.
+Global Hint Rewrite @bv_and_unsigned : bv_simplify.
+
+
+(** * Light versions of the [bv_simplify], [bv_simplify_arith] and [bv_solve] tactics from stdpp's bitvector *)
+
+Tactic Notation "bv_simplify_light" :=
+ autorewrite with bv_simplify;
+ lazymatch goal with
+ | |- _ =@{bv _} _ => apply bv_eq_wrap
+ | |- not (_ =@{bv _} _) => apply bv_neq_wrap
+ | _ => idtac
+ end;
+ bv_unfold;
+ autorewrite with bv_unfolded_simplify.
+
+Tactic Notation "bv_simplify_arith_light" :=
+ bv_simplify_light;
+ autorewrite with bv_unfolded_to_arith.
+
+Ltac bv_solve_light :=
+ bv_simplify_arith_light;
+ unfold bv_signed, bv_swrap, bv_wrap, bv_half_modulus, bv_modulus, bv_unsigned;
+ simpl;
+ lia.
+
+Ltac bv_simp_r := repeat bv_simplify.
+Tactic Notation "bv_simp_r" := bv_simp_r.
+Tactic Notation "bv_simp_r" ident(H) :=
+ repeat (bv_simplify H).
+