unsued lemma

rems-project · Aug 13, 2024 · 7a4768c · 7a4768c
1 parent a0b38eb
commit 7a4768c
Showing 1 changed file with 0 additions and 10 deletions.
diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
@@ -5475,16 +5475,6 @@ Module CheriMemoryImplWithProofs
     apply H0.
   Qed.
 
-  (* TODO: We can get away with just proving [0<l] but this is more precise formulation *)
-  Fact Capability_GS_encode_length
-    (isexact : bool)
-    (c : Capability_GS.t)
-    (l: list ascii)
-    (t: bool):
-    Capability_GS.encode isexact c = Some (l, t) -> Datatypes.length l =  sizeof_pointer MorelloImpl.get.
-  Proof.
-  Admitted.
-
   (** Storing some bytes into memory and ghosting the tags for corresponding region preserves invariant *)
   Fact mem_state_with_bytes_preserves:
     forall s : mem_state_r,