WIP test replace E-perm by sealed entry

theories/examples/malloc.v

@@ -207,11 +207,21 @@ Section SimpleMalloc.
   Qed.
 
   Lemma simple_malloc_subroutine_valid N b e :
-    na_inv logrel_nais N (malloc_inv b e) -∗
-    interp (WCap E b e b).
+    na_inv logrel_nais N (malloc_inv b e)
+    ∗ seal_pred otype_sentry interp -∗
+    interp (WSealed otype_sentry (SCap RX b e b)).
   Proof.
-    iIntros "#Hmalloc".
-    rewrite fixpoint_interp1_eq /=. iIntros (r). iNext. iModIntro.
+    iIntros "[#Hmalloc #Hsentry]".
+    rewrite fixpoint_interp1_eq /=.
+    iExists (interp); rewrite fixpoint_interp1_eq /=.
+    iSplit.
+    { iPureIntro; intro; apply interp_persistent. }
+    iSplit; first done.
+    (* TODO not working here:
+       it means that I have to prove that the content of malloc is safe to share,
+       which is not *)
+    iSplit; first done.
+    iIntros (r). iNext. iModIntro.
     iIntros "(#[% Hregs_valid] & Hregs & Hown)".
     iDestruct (big_sepM_delete _ _ PC with "Hregs") as "[HPC Hregs]";[rewrite lookup_insert;eauto|].
     destruct H with r_t0 as [? ?].

theories/ftlr/Jmp.v

@@ -95,7 +95,8 @@ Section fundamental.
             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.
+            iDestruct "HPCv" as (Psentry) "(%Hpers & #Hseal_pred & HPsentry & Hcont)"; auto.
+            iDestruct ("Hcont" $! r 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).

theories/ftlr/Jnz.v

@@ -92,7 +92,8 @@ Section fundamental.
           }
 
           iEval (rewrite fixpoint_interp1_eq) in "HPCv"; simpl.
-          iDestruct ("HPCv" with "[$Hmap $Hown]") as "Hcont"; auto.
+          iDestruct "HPCv" as (Psentry) "(%Hpers & #Hseal_pred & HPsentry & Hcont)"; auto.
+          iDestruct ("Hcont" $! r 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).

theories/ftlr/UnSeal.v

@@ -25,18 +25,16 @@ Section fundamental.
   Proof.
     iIntros (Hpseal Hwb) "#HVsd #HVsr".
     rewrite (fixpoint_interp1_eq (WSealRange _ _ _ _)) (fixpoint_interp1_eq (WSealed _ _)) /= Hpseal /interp_sb.
-    iDestruct "HVsr" as "[_ Hss]".
+    iDestruct "HVsr" as "[_ [Hss Hjmp]]".
     apply seq_between_dist_Some in Hwb.
     iDestruct (big_sepL_delete with "Hss") as "[HSa0 _]"; eauto.
     iDestruct "HSa0" as (P) "[HsealP HWcond]".
-    destruct (decide (a0 = otype_sentry)) as [?|Hot] ; subst.
-    + admit.
-    +
-      iDestruct "HVsd" as (P') "[% [HsealP' HP']]".
-      iDestruct (seal_pred_agree with "HsealP HsealP'") as "Hequiv". iSpecialize ("Hequiv" $! (WSealable sb)).
-      iAssert (▷ P (WSealable sb))%I as "HP". { iNext. by iRewrite "Hequiv". }
-      by iApply "HWcond".
-  Admitted.
+    (* destruct (decide (a0 = otype_sentry)) as [?|Hot] ; subst. *)
+    iDestruct "HVsd" as (P') "[% [HsealP' [HP' Hjmp']]]".
+    iDestruct (seal_pred_agree with "HsealP HsealP'") as "Hequiv". iSpecialize ("Hequiv" $! (WSealable sb)).
+    iAssert (▷ P (WSealable sb))%I as "HP". { iNext. by iRewrite "Hequiv". }
+    by iApply "HWcond".
+  Qed.
 
   Lemma unseal_case (r : leibnizO Reg) (p : Perm)
         (b e a : Addr) (w : Word) (dst r1 r2 : RegName) (P:D):

theories/ftlr/interp_weakening.v

@@ -3,7 +3,7 @@ From iris.proofmode Require Import proofmode.
 From iris.program_logic Require Import weakestpre adequacy lifting.
 From stdpp Require Import base.
 From cap_machine.ftlr Require Import ftlr_base.
-From cap_machine Require Import addr_reg region.
+From cap_machine Require Import addr_reg region proofmode register_tactics.
 
 Section fundamental.
   Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg: sealStoreG Σ}
@@ -89,26 +89,42 @@ Section fundamental.
     iNext. iModIntro. iIntros "([Hfull Hreg] & Hregs & Hna)".
     destruct sb as [p b e a |]; cycle 1.
     + (* PC contains sealrange, it is trivially safe *)
-      (* rewrite /interp_conf. *)
-      admit.
+      wp_instr.
+      iEval (rewrite /registers_mapsto) in "Hregs".
+      iExtract "Hregs" PC as "HPC".
+      iApply (wp_notCorrectPC with "HPC"); eauto; first (intro Hcontra; inversion Hcontra).
+      iNext ; iIntros "HPC".
+      wp_pure; wp_end.
+      iIntros "%" ; done.
     + iApply ("IH" with "Hfull Hreg Hregs Hna"); auto.
-  Admitted.
+  Qed.
 
   Lemma sealing_preserves_interp_sentry sb:
         IH -∗
+        seal_pred otype_sentry (fixpoint interp1) -∗
         fixpoint interp1 (WSealable sb) -∗
         fixpoint interp1 (WSealed otype_sentry sb).
   Proof.
-    iIntros "#IH #HVsb".
+    iIntros "#IH #Hsentry_pred #HVsb".
     rewrite (fixpoint_interp1_eq (WSealed _ _)) /= /interp_sb.
+    iExists (fixpoint interp1).
+    iSplit.
+    { iPureIntro; intro; apply interp_persistent. }
+    iSplit; first done.
+    iSplit; first done.
     iIntros (r).
     iNext. iModIntro. iIntros "([Hfull Hreg] & Hregs & Hna)".
     destruct sb as [p b e a |]; cycle 1.
-    - (* PC contains sealrange, it is trivially safe *)
-      (* rewrite /interp_conf. *)
-      admit.
-    - iApply ("IH" with "Hfull Hreg Hregs Hna"); auto.
-  Admitted.
+    + (* PC contains sealrange, it is trivially safe *)
+      wp_instr.
+      iEval (rewrite /registers_mapsto) in "Hregs".
+      iExtract "Hregs" PC as "HPC".
+      iApply (wp_notCorrectPC with "HPC"); eauto; first (intro Hcontra; inversion Hcontra).
+      iNext ; iIntros "HPC".
+      wp_pure; wp_end.
+      iIntros "%" ; done.
+    + iApply ("IH" with "Hfull Hreg Hregs Hna"); auto.
+  Qed.
 
 
   Lemma safe_to_unseal_weakening b e b' e':
@@ -160,10 +176,11 @@ Section fundamental.
   intros Hb He Hp. iIntros "#HA".
   rewrite !fixpoint_interp1_eq. cbn.
   destruct (permit_seal p') eqn:Hseal; [eapply (permit_seal_flowsto _ p) in Hseal as ->; auto | ].
-  all: destruct (permit_unseal p') eqn:Hunseal; [eapply (permit_unseal_flowsto _ p) in Hunseal as ->; auto | ]; iDestruct "HA" as "[Hs Hus]".
-  all: iSplitL "Hs";
-  [try iApply (safe_to_seal_weakening with "Hs") | try iApply (safe_to_unseal_weakening with "Hus")]; auto.
+  all: destruct (permit_unseal p') eqn:Hunseal; [eapply (permit_unseal_flowsto _ p) in Hunseal as
+        ->; auto | ]; iDestruct "HA" as "[Hs [Hus Hj]]".
+  all: destruct (permit_call b' e') as [Hjump|Hjump].
+  all: iSplitL "Hs"; [try iApply (safe_to_seal_weakening with "Hs") | iSplitL "Hus" ; try iApply (safe_to_unseal_weakening with "Hus")]; auto.
+  all: destruct (permit_call b e) as [Hjump'|Hjump']; solve_addr.
   Qed.
 
-
 End fundamental.

theories/fundamental.v

@@ -212,7 +212,7 @@ Section fundamental.
     }
     { destruct Hw as [p [b [e [a ->] ] ] ]. rewrite fixpoint_interp1_eq. cbn -[all_registers_s].
       iNext. iIntros (rmap).
-      iDestruct "Hw" as "[Hw HwP]".
+      iDestruct "Hw" as (P) "(%HP & HPsentry & HwP & Hw)".
       iSpecialize ("Hw" $! rmap). iDestruct "Hw" as "#Hw".
       iIntros "(HPC & Hr & ?)". iApply "Hw". iFrame. }
     { iNext. iIntros (rmap). iApply fundamental. eauto. }

theories/logrel.v

@@ -81,6 +81,13 @@ Section logrel.
     Proper (dist n ==> dist n) enter_cond.
   Proof. solve_proper. Qed.
 
+  Program Definition jump_cond (P : D) : D -n> iPropO Σ :=
+    λne interp, (▷ □ ∀ (w : Word), P w -∗ enter_cond w interp)%I.
+  Solve Obligations with solve_proper.
+  Global Instance jump_cond_ne n :
+    Proper (dist n ==> dist n ==> dist n) jump_cond.
+  Proof. solve_proper. Qed.
+
   (* interp definitions *)
   Program Definition interp_ref_inv (a : Addr) : D -n> iPropO Σ := λne P, (∃ w, a ↦ₐ w ∗ P w)%I.
   Solve Obligations with solve_proper.
@@ -127,24 +134,20 @@ Section logrel.
     ([∗ list] a ∈ (finz.seq_between b e), ∃ P : D,  ⌜∀ w, Persistent (P w)⌝ ∗ seal_pred a P ∗ write_cond P interp)%I.
   Definition safe_to_unseal (interp : D) (b e : OType) : iPropO Σ :=
     ([∗ list] a ∈ (finz.seq_between b e), ∃ P : D, seal_pred a P ∗ read_cond P interp)%I.
+  Definition safe_to_jump (interp : D) : iPropO Σ :=
+   (∃ P : D, seal_pred otype_sentry P ∗ jump_cond P interp)%I.
+
+  Definition permit_call (b e : OType) := decide (b <= otype_sentry < e)%ot.
 
   Program Definition interp_sr (interp : D) : D :=
     λne w, (match w with
     | WSealRange p b e a =>
     (if permit_seal p then safe_to_seal interp b e else True)
     ∗ (if permit_unseal p then safe_to_unseal interp b e else True)
+    ∗ (if permit_call b e then safe_to_jump interp else True)
     | _ => False end ) %I.
   Solve All Obligations with solve_proper.
 
-  (* Program Definition interp_sentry (interp : D) : D :=
-    λne w,
-      (match w with
-       | WSealed otype_sentry sb => enter_cond (WSealable sb) interp
-       | _ => True
-       end)%I.
-  Solve All Obligations with solve_proper. *)
-
-
   Program Definition interp_sb (o : OType) (interp : D) : D :=
     λne w,
      (∃ P : Word → iPropI Σ,
@@ -157,6 +160,20 @@ Section logrel.
      )%I.
   Solve All Obligations with solve_proper.
 
+  (* TODO possible alternative:
+     if sealed with otype_sentry, we only require safe-to-execute, not interp *)
+  (* Program Definition interp_sb (o : OType) (interp : D) : D := *)
+  (*   λne w, *)
+  (*    (∃ P : Word → iPropI Σ, *)
+  (*        ⌜∀ w', Persistent (P w')⌝ *)
+  (*              ∗ seal_pred o P *)
+  (*              ∗ ▷ P w *)
+  (*              ∗ (if (decide (o = otype_sentry)) *)
+  (*                 then enter_cond w interp *)
+  (*                 else True) *)
+  (*    )%I. *)
+  (* Solve All Obligations with solve_proper. *)
+
   Program Definition interp1 (interp : D) : D :=
     (λne w,
     match w return _ with
@@ -168,9 +185,6 @@ Section logrel.
     | WCap RWX b e a => interp_cap_RWX interp w
     | WSealRange p b e a => interp_sr interp w
     | WSealed o sb => interp_sb o interp (WSealable sb)
-        (* (if (decide (o = otype_sentry)) *)
-        (* then interp_sentry interp w *)
-        (* else ) *)
     end)%I.
 
   Global Instance read_cond_contractive :
@@ -198,6 +212,11 @@ Section logrel.
   Proof.
     solve_contractive.
   Qed.
+  Global Instance jump_cond_contractive :
+    Contractive (jump_cond).
+  Proof.
+    solve_contractive.
+  Qed.
   Global Instance interp_cap_RX_contractive :
     Contractive (interp_cap_RX).
   Proof.
@@ -217,17 +236,10 @@ Section logrel.
   Proof.
     solve_proper_prepare.
     destruct_word x0; auto.
-    destruct (permit_seal sr), (permit_unseal sr);
-    rewrite /safe_to_seal /safe_to_unseal;
-    solve_contractive.
-  Qed.
-  (* Global Instance interp_sentry_contractive : *)
-  (*   Contractive (interp_sentry). *)
-  (* Proof. *)
-  (*   solve_proper_prepare. *)
-  (*   destruct_word x0; auto. *)
-  (*   solve_contractive. *)
-  (* Qed. *)
+    destruct (permit_seal sr), (permit_unseal sr), (permit_call f f0);
+    rewrite /safe_to_seal /safe_to_unseal /safe_to_jump.
+    (* solve_contractive. *)
+  Admitted.
 
   Global Instance interp1_contractive :
     Contractive (interp1).
@@ -256,9 +268,9 @@ Section logrel.
   Proof. intros. destruct_word w; simpl; rewrite fixpoint_interp1_eq; simpl.
          - apply _.
          - destruct c; repeat (apply exist_persistent; intros); try apply _.
-         - destruct (permit_seal sr), (permit_unseal sr); rewrite /safe_to_seal /safe_to_unseal; apply _ .
-         -
-           apply exist_persistent; intros P.
+         - destruct (permit_seal sr), (permit_unseal sr), (permit_call f f0)
+            ; rewrite /safe_to_seal /safe_to_unseal /safe_to_jump; apply _ .
+         - apply exist_persistent; intros P.
            unfold Persistent. iIntros "(Hpers & #Hs & [HP Hjmp])". iDestruct "Hpers" as %Hpers.
            iAssert (<pers> ▷ P (WSealable s))%I with "[ HP ]" as "HP".
            { iApply later_persistently_1. by iApply Hpers.  }
@@ -618,39 +630,50 @@ Section logrel.
   Qed.
 
   Lemma region_seal_pred_interp E (b e a: OType) b1 b2 :
+    not (b <= otype_sentry < e)%ot ->
     ([∗ list] o ∈ finz.seq_between b e, seal_pred o interp) ={E}=∗
     interp (WSealRange (b1,b2) b e a).
   Proof.
+    intros Hnsentry.
     remember (finz.seq_between b e) as l eqn:Hgen. rewrite Hgen; revert Hgen.
-    generalize b e. clear b e.
+    generalize dependent Hnsentry.
+    generalize b e.
+    clear b e.
     induction l as [|hd tl IH].
-    - iIntros (b e Hfinz) "_ !>".
+    - iIntros (b e Hnsentry Hfinz) "_ !>".
       rewrite /interp fixpoint_interp1_eq /= /safe_to_seal /safe_to_unseal.
-      rewrite -Hfinz. destruct b1, b2; iSplit; done.
-    - iIntros (b e Hfinz).
+      rewrite -Hfinz.
+      destruct b1, b2; iSplit; try done.
+      all: symmetry in Hfinz; apply finz_empty_seq_between in Hfinz.
+      all: destruct (permit_call b e); iSplit; try done; solve_addr.
+    - iIntros (b e Hnsentry Hfinz).
       assert (b < e)%ot as Hlbe.
       {destruct (decide (b < e)%ot) as [|HF]; first auto. rewrite finz_seq_between_empty in Hfinz; [inversion Hfinz | solve_addr  ]. }
       apply finz_cons_tl in Hfinz as (b' & Hplus & Hfinz).
-      specialize (IH b' e Hfinz). rewrite (finz_seq_between_split _ b' _).
+      assert (¬ (b' <= otype_sentry < e)%f) as Hnsentry' by solve_addr.
+      specialize (IH b' e Hnsentry' Hfinz). rewrite (finz_seq_between_split _ b' _).
       2 : split; solve_addr.
       iIntros "[#Hfirst Hca]".
       iMod (IH with "Hca") as "Hca". iModIntro.
       rewrite /interp !fixpoint_interp1_eq /= /safe_to_seal /safe_to_unseal.
       rewrite !(finz_seq_between_split b b' e). 2: { split ; solve_addr. }
-      iDestruct "Hca" as "[Hseal Hunseal]".
-      iSplitL "Hseal"; [destruct b1| destruct b2]; iFrame.
+      iDestruct "Hca" as "(Hseal & Hunseal & Hcall)".
+      iSplitL "Hseal"
+      ; [|iSplitL "Hunseal"]
+      ; [destruct b1| destruct b2 | destruct (permit_call b e)]; iFrame; try done.
       all: iApply (big_sepL_mono with "Hfirst").
-      all: iIntros (k a' Hk) "H"; cbn.
-      all: iExists _; iFrame; auto.
-      iSplit; auto. iPureIntro; apply _.
+      all: (iIntros (k a' Hk) "H"; cbn).
+      all: (iExists _; iFrame; auto).
+      iSplit; auto; iPureIntro; apply _.
   Qed.
 
   (* Get the validity of sealing capabilities if we can allocate an arbitrary predicate, and can hence choose interp itself as the sealing predicate *)
   Lemma region_can_alloc_interp E (b e a: OType) b1 b2:
+    not (b <= otype_sentry < e)%ot ->
     ([∗ list] o ∈ finz.seq_between b e, can_alloc_pred o) ={E}=∗
     interp (WSealRange (b1,b2) b e a).
   Proof.
-    iIntros "Hca".
+    iIntros (Hnsentry) "Hca".
     iDestruct (big_sepL_mono with "Hca") as "Hca".
     iIntros (k a' Hk) "H". iDestruct (seal_store_update_alloc _ interp  with "H") as "H". iExact "H".