WIP test replace E-perm by sealed entry

_CoqProject

@@ -52,18 +52,18 @@ theories/rules/rules_UnSeal.v
 theories/rules.v
 
 # Program logic: Binary WP rules
-theories/rules_binary/rules_binary_base.v
-theories/rules_binary/rules_binary_Get.v
-theories/rules_binary/rules_binary_Load.v
-theories/rules_binary/rules_binary_Store.v
-theories/rules_binary/rules_binary_AddSubLt.v
-theories/rules_binary/rules_binary_Lea.v
-theories/rules_binary/rules_binary_Mov.v
-theories/rules_binary/rules_binary_Restrict.v
-theories/rules_binary/rules_binary_Jmp.v
-theories/rules_binary/rules_binary_Jnz.v
-theories/rules_binary/rules_binary_Subseg.v
-theories/rules_binary.v
+# theories/rules_binary/rules_binary_base.v
+# theories/rules_binary/rules_binary_Get.v
+# theories/rules_binary/rules_binary_Load.v
+# theories/rules_binary/rules_binary_Store.v
+# theories/rules_binary/rules_binary_AddSubLt.v
+# theories/rules_binary/rules_binary_Lea.v
+# theories/rules_binary/rules_binary_Mov.v
+# theories/rules_binary/rules_binary_Restrict.v
+# theories/rules_binary/rules_binary_Jmp.v
+# theories/rules_binary/rules_binary_Jnz.v
+# theories/rules_binary/rules_binary_Subseg.v
+# theories/rules_binary.v
 
 # Cerise Proofmode
 theories/proofmode/region.v
@@ -95,22 +95,22 @@ theories/ftlr/UnSeal.v
 theories/fundamental.v
 
 # Binary Logical Relation
-theories/logrel_binary.v
-theories/ftlr_binary/ftlr_base_binary.v
-theories/ftlr_binary/interp_weakening.v
-theories/ftlr_binary/Load_binary.v
-theories/ftlr_binary/Mov_binary.v
-theories/ftlr_binary/AddSubLt_binary.v
-theories/ftlr_binary/Get_binary.v
-theories/ftlr_binary/Jmp_binary.v
-theories/ftlr_binary/Jnz_binary.v
-theories/ftlr_binary/Lea_binary.v
-theories/ftlr_binary/Subseg_binary.v
-theories/ftlr_binary/Restrict_binary.v
-theories/ftlr_binary/Store_binary.v
-theories/ftlr_binary/Seal_binary.v
-theories/ftlr_binary/UnSeal_binary.v
-theories/fundamental_binary.v
+# theories/logrel_binary.v
+# theories/ftlr_binary/ftlr_base_binary.v
+# theories/ftlr_binary/interp_weakening.v
+# theories/ftlr_binary/Load_binary.v
+# theories/ftlr_binary/Mov_binary.v
+# theories/ftlr_binary/AddSubLt_binary.v
+# theories/ftlr_binary/Get_binary.v
+# theories/ftlr_binary/Jmp_binary.v
+# theories/ftlr_binary/Jnz_binary.v
+# theories/ftlr_binary/Lea_binary.v
+# theories/ftlr_binary/Subseg_binary.v
+# theories/ftlr_binary/Restrict_binary.v
+# theories/ftlr_binary/Store_binary.v
+# theories/ftlr_binary/Seal_binary.v
+# theories/ftlr_binary/UnSeal_binary.v
+# theories/fundamental_binary.v
 
 # Misc for examples
 theories/monotone.v
@@ -130,10 +130,10 @@ theories/examples/template_adequacy.v
 theories/examples/template_adequacy_ocpl.v
 
 # Tutorial and Exercises for learning Cerise in Coq
-theories/exercises/cerise_tutorial.v
-theories/exercises/cerise_tutorial_solutions.v
-theories/exercises/cerise_modularity.v
-theories/exercises/cerise_modularity_solutions.v
+# theories/exercises/cerise_tutorial.v
+# theories/exercises/cerise_tutorial_solutions.v
+# theories/exercises/cerise_modularity.v
+# theories/exercises/cerise_modularity_solutions.v
 
 theories/exercises/subseg_buffer.v
 theories/exercises/restrict_buffer.v
@@ -176,16 +176,16 @@ theories/examples/interval_arch/interval_client_closure_arch.v
 theories/examples/interval_arch/interval_client_adequacy_arch.v
 
 # Common macros (binary)
-theories/examples/malloc_binary.v
-theories/examples/macros_binary.v
+# theories/examples/malloc_binary.v
+# theories/examples/macros_binary.v
 
 # Counter example (binary)
-theories/examples/counter_binary/counter_binary.v
-theories/examples/counter_binary/counter_binary_preamble_def.v
-theories/examples/counter_binary/counter_binary_preamble.v
-theories/examples/counter_binary/counter_binary_preamble_left.v
-theories/examples/counter_binary/counter_binary_adequacy.v
-theories/examples/counter_binary/counter_binary_adequacy_theorem.v
+# theories/examples/counter_binary/counter_binary.v
+# theories/examples/counter_binary/counter_binary_preamble_def.v
+# theories/examples/counter_binary/counter_binary_preamble.v
+# theories/examples/counter_binary/counter_binary_preamble_left.v
+# theories/examples/counter_binary/counter_binary_adequacy.v
+# theories/examples/counter_binary/counter_binary_adequacy_theorem.v
 
 # Other examples
 theories/examples/adder.v

theories/cap_lang.v

@@ -246,13 +246,10 @@ Section opsem.
       wdst ← (reg φ) !! dst;
       match wdst with
       | WCap p b e a =>
-        match p with
-        | E => None
-        | _ => match (a + n)%a with
-               | Some a' => updatePC (update_reg φ dst (WCap p b e a'))
-               | None => None
-               end
-        end
+          match (a + n)%a with
+          | Some a' => updatePC (update_reg φ dst (WCap p b e a'))
+          | None => None
+          end
       | WSealRange p b e a =>
          match (a + n)%ot with
           | Some a' => updatePC (update_reg φ dst (WSealRange p b e a'))
@@ -264,13 +261,10 @@ Section opsem.
       n ← z_of_argument (reg φ) ρ ;
       wdst ← (reg φ) !! dst;
       match wdst with
-      | WCap permPair b e a =>
-        match permPair with
-        | E => None
-        | _ => if PermFlowsTo (decodePerm n) permPair then
-                updatePC (update_reg φ dst (WCap (decodePerm n) b e a))
-              else None
-        end
+      | WCap p b e a =>
+          if PermFlowsTo (decodePerm n) p then
+            updatePC (update_reg φ dst (WCap (decodePerm n) b e a))
+          else None
       | WSealRange p b e a =>
         if SealPermFlowsTo (decodeSealPerms n) p then
               updatePC (update_reg φ dst (WSealRange (decodeSealPerms n) b e a))
@@ -295,13 +289,9 @@ Section opsem.
     | WCap p b e a =>
       a1 ← addr_of_argument (reg φ) ρ1;
       a2 ← addr_of_argument (reg φ) ρ2;
-      match p with
-      | E => None
-      | _ =>
-        if isWithin a1 a2 b e then
-          updatePC (update_reg φ dst (WCap p a1 a2 a))
-        else None
-      end
+      if isWithin a1 a2 b e then
+        updatePC (update_reg φ dst (WCap p a1 a2 a))
+      else None
     | WSealRange p b e a =>
       o1 ← otype_of_argument (reg φ) ρ1;
       o2 ← otype_of_argument (reg φ) ρ2;
@@ -368,6 +358,15 @@ Section opsem.
         else None
     | _,_ => None
     end
+  (* | SealEntry dst r => *)
+  (*   wr ← (reg φ) !! r; *)
+  (*   match wr with *)
+  (*   | WCap p b e a => *)
+  (*       if executeAllowed p *)
+  (*       then updatePC (update_reg φ dst (WSealed otype_sentry (SCap p b e a))) *)
+  (*       else None *)
+  (*   |  _ => None *)
+  (*   end *)
   end.
 
   Definition exec (i: instr) (φ: ExecConf) : Conf :=

theories/examples/addr_reg_sample.v

@@ -53,7 +53,7 @@ Section instr_encodings.
   Definition fail_end := encodeInstrW Fail.
 
   (* encodings of return pointer permission pair *)
-  Definition e := encodePerm E.
+  (* Definition e := encodePerm E. *)
 End instr_encodings.
 
 (* Some additional helper lemmas about region_addrs *)

theories/ftlr/Jmp.v

@@ -38,7 +38,7 @@ Section fundamental.
       iIntros "_".
       iApply ("IH" $! _ _ b e a with "[] [] [Hmap] [$Hown]"); eauto.
       { iPureIntro. apply Hsome. }
-      destruct Hp as [-> | ->]; iFrame.
+      (* destruct Hp as [-> | ->]; iFrame. *)
     * specialize Hsome with r0 as Hr0.
       destruct Hr0 as [wsrc Hsomesrc].
       iDestruct ((big_sepM_delete _ _ r0) with "Hmap") as "[Hsrc Hmap]"; eauto.
@@ -54,23 +54,22 @@ Section fundamental.
       iMod ("Hcls" with "[HP Ha]");[iExists w;iFrame|iModIntro].
 
      (* Needed because IH disallows non-capability values *)
-      destruct wsrc as [ | [p' b' e' a' | ] | ]; cycle 1.
+      destruct wsrc as [ | [p' b' e' a' | ] | ot sb ]
+      ; [
+          (* Integer *) shelve
+        | (* Unsealed cap *) idtac
+        | (* Sealing cap *) shelve
+        | (* Sealed cap *) idtac
+        ].
+
+      (* Unsealed capability *)
       {
+        iNext; iIntros "_".
         rewrite /updatePcPerm.
-        (* Special case for E-values*)
-        destruct (decide (p' = E)) as [-> | HneE].
-        -
-          unshelve iDestruct ("Hreg" $! r0 _ _ Hsomesrc) as "HPCv"; auto.
-          iClear "Hinv".
-          rewrite fixpoint_interp1_eq; simpl.
-
-          iDestruct (big_sepM_insert _ _ PC with "[$Hmap $HPC]") as "Hmap"; [apply lookup_delete|]. rewrite insert_delete_insert; auto.
-          iDestruct ("HPCv" with "[$Hmap $Hown]") as "Hcont"; auto.
         - iAssert (PC ↦ᵣ WCap p' b' e' a')%I  with "[HPC]" as "HPC".
-          { destruct p'; auto. congruence. }
+          { destruct p'; auto. (* congruence. *) }
 
           iDestruct (big_sepM_insert _ _ PC with "[$Hmap $HPC]") as "Hmap"; [apply lookup_delete|]. rewrite insert_delete_insert; auto.
-          iNext; iIntros "_".
           iApply ("IH" $! (<[PC:=WCap p' b' e' a']> r) with "[%] [] [Hmap] [$Hown]").
           { cbn. intros. by repeat (rewrite lookup_insert_is_Some'; right). }
           { iIntros (ri v Hri Hvs).
@@ -86,10 +85,27 @@ Section fundamental.
           unshelve iSpecialize ("Hreg" $! r0 _ _ Hsomesrc); eauto.
       }
 
-     (* Non-capability cases *)
+      (* Sealed capability *)
+      {
+        rewrite /updatePcPerm.
+        destruct (decide (ot = otype_sentry)) as [Hot|Hot]; subst.
+        + destruct sb as [p' b' e' a' | ]; [|shelve].
+          (* Sentry *)
+            unshelve iDestruct ("Hreg" $! r0 _ _ Hsomesrc) as "HPCv"; auto.
+            iClear "Hinv".
+            rewrite fixpoint_interp1_eq; simpl.
+            iDestruct (big_sepM_insert _ _ PC with "[$Hmap $HPC]") as "Hmap"; [apply lookup_delete|]. rewrite insert_delete_insert; auto.
+            iDestruct ("HPCv" with "[$Hmap $Hown]") as "Hcont"; auto.
+        + (* Not a sentry *)
+          rewrite (_: match sb with | SCap _ _ _ _ | _ => WSealed ot sb end = WSealed ot sb)
+          ; last (by destruct sb).
+          shelve.
+      }
+
+      Unshelve.
       all: iNext; iIntros "_".
-      all: rewrite /updatePcPerm; iApply (wp_bind (fill [SeqCtx]));
-        iApply (wp_notCorrectPC with "HPC"); [intros HFalse; inversion HFalse| ].
+      all: iApply (wp_bind (fill [SeqCtx]));
+            iApply (wp_notCorrectPC with "HPC"); [intros HFalse; inversion HFalse| ].
       all: repeat iNext; iIntros "HPC /=".
       all: iApply wp_pure_step_later; auto.
       all: iNext; iIntros "_".

theories/ftlr/Jnz.v

@@ -46,48 +46,72 @@ Section fundamental.
     { simplify_map_eq. iApply wp_pure_step_later; auto.
       rewrite !insert_insert.
 
+
       iMod ("Hcls" with "[HP Ha]");[iExists w;iFrame|iModIntro].
 
-      (* Needed because IH disallows non-capability values *)
-      destruct w' as [ | [p' b' e' a' | ] | ]; cycle 1.
+     (* Needed because IH disallows non-capability values *)
+      destruct w' as [ | [p' b' e' a' | ] | ot sb ]
+      ; [
+          (* Integer *) shelve
+        | (* Unsealed cap *) idtac
+        | (* Sealing cap *) shelve
+        | (* Sealed cap *) idtac
+        ].
+
+      (* Unsealed capability *)
       {
+        iNext; iIntros "_".
         rewrite /updatePcPerm.
-        iAssert (fixpoint interp1 (WCap p' b' e' a')) as "HECap".
+        iAssert (fixpoint interp1 (WCap p' b' e' a')) as "HCap".
         { destruct (decide (r1 = PC)) as [-> | Hne]. by simplify_map_eq.
           rewrite lookup_insert_ne // in H1.
           unshelve iDestruct ("Hreg" $! r1 _ _ H1) as "HPCv"; auto.
         }
+        iAssert ([∗ map] k↦y ∈ <[PC:= WCap p' b' e' a']> r, k ↦ᵣ y)%I  with "[Hmap]" as "Hmap".
+        { destruct p'; auto. }
 
-        (* Special case for E-values*)
-        destruct (decide (p' = E)) as [-> | HneE].
-        - iClear "Hinv".
-          rewrite fixpoint_interp1_eq; simpl.
-          iDestruct ("HECap" with "[$Hmap $Hown]") as "Hcont"; auto.
-        - iAssert ([∗ map] k↦y ∈ <[PC:= WCap p' b' e' a']> r, k ↦ᵣ y)%I  with "[Hmap]" as "Hmap".
-          { destruct p'; auto. congruence. }
-          iNext; iIntros "_".
+        iApply ("IH" $! (<[PC:=WCap p' b' e' a']> r) with "[%] [] [Hmap] [$Hown]").
+        { cbn. intros. by repeat (rewrite lookup_insert_is_Some'; right). }
+        { iIntros (ri v Hri Hvs).
+          rewrite lookup_insert_ne in Hvs; auto.
+          unshelve iSpecialize ("Hreg" $! ri _ _ Hvs); eauto. }
+        { rewrite insert_insert. iApply "Hmap". }
+        auto.
+      }
 
-          iApply ("IH" $! (<[PC:=WCap p' b' e' a']> r) with "[%] [] [Hmap] [$Hown]").
-          { cbn. intros. by repeat (rewrite lookup_insert_is_Some'; right). }
-          { iIntros (ri v Hri Hvs).
-            rewrite lookup_insert_ne in Hvs; auto.
-              unshelve iSpecialize ("Hreg" $! ri _ _ Hvs); eauto. }
-          { rewrite insert_insert. iApply "Hmap". }
-          auto.
+      (* Sealed capability *)
+      {
+        rewrite /updatePcPerm.
+        destruct (decide (ot = otype_sentry)) as [Hot|Hot]; subst.
+        + destruct sb as [p' b' e' a' | ]; [|shelve].
+          (* Sentry *)
+          iAssert (fixpoint interp1 (WSealed otype_sentry (SCap p' b' e' a'))) as "HPCv".
+          { destruct (decide (r1 = PC)) as [-> | Hne]. by simplify_map_eq.
+            rewrite lookup_insert_ne // in H1.
+            unshelve iDestruct ("Hreg" $! r1 _ _ H1) as "HPCv"; auto.
+          }
+
+          iEval (rewrite fixpoint_interp1_eq) in "HPCv"; simpl.
+          iDestruct ("HPCv" with "[$Hmap $Hown]") as "Hcont"; auto.
+        + (* Not a sentry *)
+          rewrite (_: match sb with | SCap _ _ _ _ | _ => WSealed ot sb end = WSealed ot sb)
+          ; last (by destruct sb).
+          shelve.
       }
-     (* Non-capability cases *)
 
+      (* Non-capability cases *)
+      Unshelve.
       all: iNext; iIntros "_".
-     all: iDestruct ((big_sepM_delete _ _ PC) with "Hmap") as "[HPC Hmap] /=";
-      [apply lookup_insert|]; simpl.
-     all: rewrite /updatePcPerm; iApply (wp_bind (fill [SeqCtx]));
+      all: iDestruct ((big_sepM_delete _ _ PC) with "Hmap") as "[HPC Hmap] /=";
+        [apply lookup_insert|]; simpl.
+      all: rewrite /updatePcPerm; iApply (wp_bind (fill [SeqCtx]));
         iApply (wp_notCorrectPC with "HPC"); [intros HFalse; inversion HFalse| ].
-     all: repeat iNext; iIntros "HPC /=".
-     all: iApply wp_pure_step_later; auto.
-     all: iNext; iIntros "_".
-     all: iApply wp_value.
-     all: iIntros.
-     all: discriminate.
+      all: repeat iNext; iIntros "HPC /=".
+      all: iApply wp_pure_step_later; auto.
+      all: iNext; iIntros "_".
+      all: iApply wp_value.
+      all: iIntros.
+      all: discriminate.
      }
 Qed.
 

theories/ftlr/Lea.v

@@ -29,7 +29,7 @@ Section fundamental.
       apply elem_of_dom. apply lookup_insert_is_Some'; eauto. }
 
     iIntros "!>" (regs' retv). iDestruct 1 as (HSpec) "[Ha Hmap]".
-    destruct HSpec as [ * Hdst ? Hz Hoffset HincrPC | * Hdst Hz Hoffset HincrPC | ].
+    destruct HSpec as [ * Hdst Hz Hoffset HincrPC | * Hdst Hz Hoffset HincrPC | ].
     { apply incrementPC_Some_inv in HincrPC as (p''&b''&e''&a''& ? & HPC & Z & Hregs').
 
       assert (p'' = p ∧ b'' = b ∧ e'' = e) as (-> & -> & ->).
@@ -56,7 +56,6 @@ Section fundamental.
       { subst regs'. rewrite insert_insert. iApply "Hmap". }
       iModIntro.
       iApply (interp_weakening with "IH Hinv"); auto; try solve_addr.
-      { destruct Hp; by subst p. }
       { by rewrite PermFlowsToReflexive. } }
     { apply incrementPC_Some_inv in HincrPC as (p''&b''&e''&a''& ? & HPC & Z & Hregs').
 
@@ -84,7 +83,6 @@ Section fundamental.
       { subst regs'. rewrite insert_insert. iApply "Hmap". }
       iModIntro.
       iApply (interp_weakening with "IH Hinv"); auto; try solve_addr.
-      { destruct Hp; by subst p. }
       { by rewrite PermFlowsToReflexive. } }
     { iApply wp_pure_step_later; auto.
       iMod ("Hcls" with "[HP Ha]");[iExists w;iFrame|iModIntro].