From a09536a1160f7d2ee3ba549824e15a46e0e7d583 Mon Sep 17 00:00:00 2001
From: Vadim Zaliva <vz231@cl.cam.ac.uk>
Date: Tue, 17 Sep 2024 10:44:06 -0700
Subject: [PATCH] CHERI: fixing last Admit with new lemmas from
 `coq-cheri-capabilies` (#580)

* adjustements to new coq-cheri-capabilities API.

* adjusted encode_decode lemma

* CHERI: fixing last Admit with new lemmas from `coq-cheri-capabilies`
---
 coq/Morello/CapabilitiesGS.v | 13 +++++++--
 coq/Morello/MorelloCapsGS.v  | 28 +++++++++++++------
 coq/Proofs/Revocation.v      | 53 ++++++++++++++++++++----------------
 3 files changed, 59 insertions(+), 35 deletions(-)

diff --git a/coq/Morello/CapabilitiesGS.v b/coq/Morello/CapabilitiesGS.v
index 8590e1936..bba1394fc 100644
--- a/coq/Morello/CapabilitiesGS.v
+++ b/coq/Morello/CapabilitiesGS.v
@@ -259,7 +259,14 @@ Module Type CAPABILITY_GS
   Parameter cap_encode_length:
     forall c l t, encode c = Some (l, t) -> List.length l = sizeof_cap.
 
-  Parameter cap_exact_encode_decode:
-    forall c c' t l, encode c = Some (l, t) -> decode l t = Some c' -> eqb c
-c' = true.
+  Parameter cap_encode_valid:
+    forall cap cb b,
+      cap_is_valid cap = true -> encode cap = Some (cb, b) -> b = true.
+
+  Parameter cap_encode_decode_bounds:
+    forall cap bytes t,
+      encode cap = Some (bytes, t) ->
+      exists cap', decode bytes t = Some cap'
+              /\ cap_get_bounds cap = cap_get_bounds cap'.
+
 End CAPABILITY_GS.
diff --git a/coq/Morello/MorelloCapsGS.v b/coq/Morello/MorelloCapsGS.v
index ba910758d..a502815ec 100644
--- a/coq/Morello/MorelloCapsGS.v
+++ b/coq/Morello/MorelloCapsGS.v
@@ -238,15 +238,27 @@ Module Capability_GS <: CAPABILITY_GS (MorelloCaps.AddressValue) (MorelloCaps.Fl
     apply H.
   Qed.
 
-  Lemma cap_exact_encode_decode:
-    forall c c' t l, encode c = Some (l, t) -> decode l t = Some c' -> eqb c c' = true.
+  Lemma cap_encode_valid:
+    forall cap cb b,
+      cap_is_valid cap = true -> encode cap = Some (cb, b) -> b = true.
   Proof.
-    intros.
-    apply Capability.cap_exact_encode_decode with (t:=t0) (l:=l).
-    auto.
-    unfold decode in H0.
-    destruct (Capability.decode l t0); inversion H0.
-    reflexivity.
+    intros c cb b V E.
+    eapply Capability.cap_encode_valid; eauto.
+  Qed.
+
+  Lemma cap_encode_decode_bounds:
+    forall cap bytes t,
+      encode cap = Some (bytes, t) ->
+      exists cap', decode bytes t = Some cap'
+              /\ cap_get_bounds cap = cap_get_bounds cap'.
+  Proof.
+    intros cap0 bytes t E.
+    apply Capability.cap_encode_decode_bounds in E.
+    destruct E as [cap' [D E]].
+    unfold decode.
+    exists (add_gs cap').
+    rewrite D.
+    split;auto.
   Qed.
 
 End Capability_GS.  
diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
index f51b5250f..3d72cb3c3 100644
--- a/coq/Proofs/Revocation.v
+++ b/coq/Proofs/Revocation.v
@@ -5577,25 +5577,27 @@ Module CheriMemoryImplWithProofs
     apply MorelloImpl.pointer_size_cap_size.
   Qed.
 
-  Fact cap_encode_decode
+  Fact cap_encode_decode_bounds
     (cap : Capability_GS.t)
-    (cb : list ascii)
-    (b : bool) :
-    Capability_GS.encode cap = Some (cb, b) ->
-    decode_cap (map Some cb) true cap.
-  Proof.
-    intros ENC.
+    (cb : list ascii):
+    Capability_GS.cap_is_valid cap = true ->
+    Capability_GS.encode cap = Some (cb, true) ->
+    exists cap' : Capability_GS.t,
+      decode_cap (map Some cb) true cap' /\
+        Capability_GS.cap_get_bounds cap =
+        Capability_GS.cap_get_bounds cap'.
+  Proof.
+    intros V H.
+    apply Capability_GS.cap_encode_decode_bounds in H.
+    destruct H as [cap' [D E]].
+    exists cap'.
+    split;[|assumption].
     unfold decode_cap.
     exists cb.
-    split.
-    -
-      clear.
-      induction cb; cbn; constructor; tauto.
-    -
-      pose proof Capability_GS.cap_exact_encode_decode as H.
-      specialize (H cap cap b cb ENC).
-
-  Admitted.
+    split;[|assumption].
+    clear.
+    induction cb; cbn; constructor;auto.
+  Qed.
 
   (** Storing a capability bytes into memory and and addit it to capmeta preserves invariant *)
   Fact mem_state_with_cap_preserves:
@@ -5651,20 +5653,23 @@ Module CheriMemoryImplWithProofs
       destruct (MorelloCaps.AddressValue.morello_address_eq_dec start addr)
         as [EQ | NEQ].
       +
-        subst start.
-        exists cap.
+        apply AMap.P.F.add_mapsto_iff in M as [[_ M] | M]; [| tauto].
+        tuple_inversion.
+        pose proof (Capability_GS.cap_encode_valid cap cb b H0 E) as B.
+        subst b.
+        apply cap_encode_decode_bounds in E.
+        destruct E as [cap' [DX EX]].
+        exists cap'.
         split.
         --
-          subst bs'.
           rewrite fetch_bytes_add_eq_o by lia.
-          subst.
-          clear - E.
-          eapply cap_encode_decode.
           eassumption.
         --
-          apply AMap.P.F.add_mapsto_iff in M as [[_ M] | M]; [| tauto].
-          invc M.
+          unfold cap_bounds_within_alloc in *.
+          rewrite <- EX.
           now apply CAPA.
+        --
+          assumption.
       +
         eapply MIcap.
         *