compilation fixes after coq-cheri-capabilities library changes

rems-project · Oct 22, 2024 · e73d6a1 · e73d6a1
1 parent ccc8fb4
commit e73d6a1
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 15 deletions.
diff --git a/coq/Common/AMap.v b/coq/Common/AMap.v
@@ -3,6 +3,7 @@
 Require Import Coq.ZArith.BinInt.
 From Coq.Structures Require Import OrderedType OrderedTypeEx.
 From CheriCaps.Morello Require Import Capabilities.
+Require Import CheriCaps.Common.Utils.
 
 Require Import FMapExt.
 

diff --git a/coq/Proofs/ProofsAux.v b/coq/Proofs/ProofsAux.v
@@ -1665,38 +1665,38 @@ Section AddressValue_Lemmas.
 
   Lemma AdddressValue_eqb_eq:
     forall (a b: AddressValue.t),
-      eqb a b = true <-> a = b.
+      AddressValue.eqb a b = true <-> a = b.
   Proof.
     intros a b.
     split.
     -
       intros H.
-      unfold eqb in H.
+      unfold AddressValue.eqb, Utils.eqb in H.
       bool_to_prop_hyp.
       apply bitvector.bv_eq.
       assumption.
     -
       intros H.
-      unfold eqb.
+      unfold AddressValue.eqb, Utils.eqb.
       subst.
       lia.
   Qed.
 
   Lemma AdddressValue_eqb_neq:
     forall (a b: AddressValue.t),
-      eqb a b = false <-> a <> b.
+      AddressValue.eqb a b = false <-> a <> b.
   Proof.
     intros a b.
     split.
     -
       intros H.
-      unfold eqb in H.
+      unfold AddressValue.eqb, Utils.eqb in H.
       bool_to_prop_hyp.
       apply bitvector.bv_neq.
       assumption.
     -
       intros H.
-      unfold eqb.
+      unfold AddressValue.eqb, Utils.eqb.
       apply bitvector.bv_neq in H.
       lia.
   Qed.
@@ -1714,16 +1714,16 @@ Section AddressValue_Lemmas.
   Proof.
     (* This should not be so tedious! *)
     intros a b.
-    unfold AddressValue.leb, leb, Z.leb.
+    unfold AddressValue.leb, leb, Utils.leb, Z.leb.
     rewrite orb_lazy_alt.
     repeat break_match_goal;auto.
     -
       rewrite AddressValue_ltb_Z_ltb in Heqb0.
       rewrite Z.ltb_compare in Heqb0.
       break_match_hyp; discriminate.
     -
-      unfold eqb.
-      unfold AddressValue.to_Z, bv_to_Z_unsigned in *.
+      unfold eqb, Utils.eqb.
+      unfold AddressValue.to_Z, Utils.bv_to_Z_unsigned in *.
       pose proof (Z.eqb_compare (bitvector.bv_unsigned a) (bitvector.bv_unsigned b)) as ZC.
       break_match_hyp ; try discriminate.
       auto.
@@ -1733,7 +1733,7 @@ Section AddressValue_Lemmas.
       break_match_hyp; discriminate.
     -
       unfold eqb.
-      unfold AddressValue.to_Z, bv_to_Z_unsigned in *.
+      unfold AddressValue.to_Z, Utils.bv_to_Z_unsigned in *.
       pose proof (Z.eqb_compare (bitvector.bv_unsigned a) (bitvector.bv_unsigned b)) as ZC.
       break_match_hyp ; try discriminate.
       auto.
@@ -1745,7 +1745,7 @@ Section AddressValue_Lemmas.
   Proof.
     split ; intros H.
     -
-      unfold AddressValue.to_Z, bv_to_Z_unsigned in H.
+      unfold AddressValue.to_Z, Utils.bv_to_Z_unsigned in H.
       apply bitvector.bv_unsigned_inj.
       assumption.
     -
@@ -1766,7 +1766,7 @@ Section AddressValue_Lemmas.
   Proof.
     intros a.
     unfold AddressValue.of_Z, AddressValue.to_Z.
-    unfold bv_to_Z_unsigned.
+    unfold Utils.bv_to_Z_unsigned.
     apply bitvector.Z_to_bv_bv_unsigned.
   Qed.
 

diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
@@ -69,8 +69,8 @@ Fact ADDR_LIMIT_to_Z:
   AddressValue.to_Z (AddressValue.of_Z AddressValue.ADDR_LIMIT) = 0.
 Proof.
   unfold AddressValue.ADDR_LIMIT, AddressValue.of_Z, AddressValue.to_Z.
-  Transparent bv_to_Z_unsigned.
-  unfold bv_to_Z_unsigned.
+  Transparent Utils.bv_to_Z_unsigned.
+  unfold Utils.bv_to_Z_unsigned.
   rewrite bitvector.Z_to_bv_unsigned.
   replace (bitvector.bv_modulus AddressValue.len) with (0 + (bitvector.bv_modulus AddressValue.len)) by lia.
   apply bitvector.bv_wrap_add_modulus_1.
@@ -5428,7 +5428,7 @@ Module CheriMemoryImplWithProofs
     (f : A -> option B)
     (l : list A)
     (l' : list B):
-    Capability.try_map f l = Some l' ->
+    Utils.try_map f l = Some l' ->
     length l' = length l.
   Proof.
     generalize dependent l'.