use new lemma cap_invalidate_invalidates

rems-project · Jan 24, 2024 · f1c5a6e · f1c5a6e
1 parent c868f2b
commit f1c5a6e
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 13 deletions.
diff --git a/coq/Morello/CapabilitiesGS.v b/coq/Morello/CapabilitiesGS.v
@@ -252,4 +252,6 @@ Module Type CAPABILITY_GS
   (* Make sure `eqb` and `value_compare` are consistent *)
   Parameter eqb_value_compare: forall a b, eqb a b = true -> value_compare a b = Eq.
 
+  Parameter cap_invalidate_invalidates: forall c, cap_is_valid (cap_invalidate c) = false.
+
 End CAPABILITY_GS.
diff --git a/coq/Morello/MorelloCapsGS.v b/coq/Morello/MorelloCapsGS.v
@@ -216,7 +216,13 @@ Module Capability_GS <: CAPABILITY_GS (MorelloCaps.AddressValue) (MorelloCaps.Fl
 
   Lemma eqb_exact_compare: forall (a b : t), eqb a b = true <-> exact_compare a b = Eq.
   Proof. intros. unfold eqb. unfold exact_compare. apply Capability.eqb_exact_compare. Qed. 
-
+
+  Lemma cap_invalidate_invalidates: forall c, cap_is_valid (cap_invalidate c) = false.
+  Proof.
+    intros c.
+    apply MorelloCaps.Capability.cap_invalidate_invalidates.
+  Qed.
+
 End Capability_GS.  
 
 
@@ -236,4 +242,4 @@ Module TestCaps.
   Definition c3_bytes := ["208"%char;"230"%char;"255"%char;"255"%char;"000"%char;"000"%char;"000"%char;
     "042"%char;"208"%char;"230"%char;"212"%char;"102"%char;"000"%char;"000"%char;"000"%char;"220"%char].
 
-End TestCaps.
+End TestCaps.
diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
@@ -923,16 +923,6 @@ Module RevocationProofs.
     reflexivity.
   Qed.
 
-  (* TODO: this should be part of capabilities library *)
-  Lemma invalidate_invalidates:
-    forall c : Capability_GS.t, Capability_GS.cap_is_valid (Capability_GS.cap_invalidate c) = false.
-  Proof.
-    intros c.
-    unfold Capability_GS.cap_is_valid, Capability_GS.cap_invalidate.
-    unfold Capability.cap_is_valid, Capability_GS.cap, Capability_GS.set_cap, Capability.cap_invalidate.
-    unfold CapFns.CapIsTagClear.
-  Admitted.
-
   Lemma single_alloc_id_cap_cmp_value_eq:
     forall m1 alloc_id c1 c2 ,
       single_alloc_id_cap_cmp (CheriMemoryWithPNVI.allocations m1) alloc_id c1 c2
@@ -1732,7 +1722,7 @@ Module RevocationProofs.
           * (* cap which is being added *)
             subst k.
             left.
-            repeat rewrite invalidate_invalidates.
+            repeat rewrite Capability_GS.cap_invalidate_invalidates.
             repeat rewrite <- cap_invalidate_preserves_ghost_state.
             exists (Capability_GS.cap_is_valid c1, Capability_GS.get_ghost_state c1).
             exists (false, Capability_GS.get_ghost_state c1).