repr_same wip

rems-project · Nov 8, 2023 · 794018e · 794018e
1 parent a69e9fa
commit 794018e
Showing 1 changed file with 20 additions and 5 deletions.
diff --git a/coq/Proofs/Revocation.v b/coq/Proofs/Revocation.v
@@ -876,13 +876,14 @@ Module RevocationProofs.
     intros fuel funptrmap1 funptrmap2 capmeta1 capmeta2 addr1 addr2 mval1 mval2
       [Ffun [Ecap [Eaddr Emval]]].
     destruct fuel;[reflexivity|].
-    cbn.
     subst.
-    unfold CheriMemoryWithPNVI.DEFAULT_FUEL, CheriMemoryWithoutPNVI.DEFAULT_FUEL.
-    repeat rewrite sizeof_same.
-    induction mval2.
+    induction mval2 eqn:IMV;
+      cbn;
+      unfold CheriMemoryWithPNVI.DEFAULT_FUEL, CheriMemoryWithoutPNVI.DEFAULT_FUEL;
+      repeat rewrite sizeof_same.
     -
-      break_match.
+      (* mval2 = MVunspecified c *)
+      break_match_goal.
       reflexivity.
       repeat split; auto.
       apply ghost_tags_same.
@@ -892,6 +893,20 @@ Module RevocationProofs.
       unfold CheriMemoryWithoutPNVI.default_prov.
       rewrite is_PNVI_WithPNVI, is_PNVI_WithoutPNVI.
 
+      apply list_init_proper;[reflexivity|].
+      intros x y E.
+      constructor.
+      split; auto.
+    - (* mval2 = MVinteger i i0 *)
+      destruct i0 eqn:II0.
+      +
+        (* i0 = IV z *)
+        break_match ; [reflexivity|].
+        break_match ; [reflexivity|].
+        admit.
+      +
+        (* i0 = IC b t *)
+
   Admitted.
 
   (* --- Stateful proofs below --- *)