mutable_typed_shared_data: Use of seal_state/valid_sealed

theories/examples/mutable_typed_shared_data/invariants.v

@@ -6,18 +6,59 @@ Section invariants.
           {nainv: logrel_na_invs Σ} `{MP: MachineParameters}.
 
   Notation "a ↪ₐ w" := (mapsto (L := Addr) (V := Word) a DfracDiscarded w) (at level 20) : bi_scope.
+  Definition sealN : namespace := nroot .@ "seal".
 
   Definition isIntSealed_int w': Word → iProp Σ :=
     (λ w, (∃ a_cap, ⌜w = WCap RW a_cap (a_cap ^+ 1)%a a_cap⌝ ∗ a_cap ↪ₐ w' ∗ ⌜is_z w'⌝)%I).
 
   Definition isIntSealed: Word → iProp Σ := (λ w, (∃ w', isIntSealed_int w' w))%I.
 
+  Instance isIntSealed_timeless w : Timeless (isIntSealed w).
+  Proof. apply _. Qed.
+
+  Instance isIntSealed_persistent w : Persistent (isIntSealed w).
+  Proof. apply _. Qed.
+
   Definition seal_state ι addr τ {Hpers : ∀ w, Persistent (isIntSealed w)} : iProp Σ
     := na_inv logrel_nais ι
-         (∃ τ_e, addr ↦ₐ WSealRange (true, true) τ τ_e τ ∗ ⌜(τ < τ_e)%ot⌝)%I
+         (∃ v, addr ↦ₐ v ∗ ⌜is_z v⌝)%I
        ∗ seal_pred τ isIntSealed.
 
-  Definition sealN : namespace := nroot .@ "seal".
+  Definition valid_sealed w τ Φ :=
+    (∃ sb, ⌜w = WSealed τ sb⌝ ∗ ⌜∀ w : leibnizO Word, Persistent (Φ w)⌝ ∗ seal_pred τ Φ ∗ Φ (WSealable sb))%I.
+
+  Global Instance valid_sealed_persistent w o Φ: Persistent (valid_sealed w o Φ).
+  Proof.
+    Import uPred. (* exist_persistent *)
+
+    apply exist_persistent; intros sb.
+    unfold Persistent.
+    iIntros "(%Hw & %Hpers & #Hs & HP)".
+
+    (* use knowledge about persistence *)
+    iAssert (<pers> Φ (WSealable sb))%I with "[HP]" as "HP".
+    { by iApply Hpers. }
+
+    repeat (iApply persistently_sep_2; iSplitR); auto.
+  Qed.
+
+  Lemma interp_valid_sealed sb o:
+    interp (WSealed o sb) -∗ ▷ ∃ Φ, valid_sealed (WSealed o sb) o Φ.
+  Proof.
+    iIntros "Hsl".
+    rewrite fixpoint_interp1_eq /=.
+    iDestruct "Hsl" as (Φ) "(%Hpers & Hpred & Hφ)".
+    iExists Φ, sb.
+    by repeat iSplit.
+  Qed.
+
+  Lemma seal_state_valid_sealed_pred_eq ι ll o w Φ: seal_state ι ll o -∗ valid_sealed w o Φ -∗  (∀ w, ▷ (isIntSealed w ≡ Φ w)).
+  Proof.
+    iIntros "HsealLL Hvs".
+    iDestruct "HsealLL" as "[_ Hsp]".
+    iDestruct "Hvs" as (sb) "(_ & _ & Hsp' & _)".
+    iApply (seal_pred_agree with "Hsp Hsp'").
+  Qed.
 
   Lemma isIntSealed_alloc a_cap w:
     a_cap ↦ₐ w ∗ ⌜is_z w⌝ ==∗ isIntSealed_int w (WCap RW a_cap (a_cap ^+ 1)%a a_cap).
@@ -27,10 +68,4 @@ Section invariants.
     iModIntro. iExists _; eauto.
   Qed.
 
-  Instance isIntSealed_timeless w : Timeless (isIntSealed w).
-  Proof. apply _. Qed.
-
-  Instance isIntSealed_persistent w : Persistent (isIntSealed w).
-  Proof. apply _. Qed.
-
 End invariants.

theories/examples/mutable_typed_shared_data/store.v

@@ -32,19 +32,18 @@ Section store_int.
       Jmp r_t0
     ].
 
-
   Lemma store_global_macro_int_spec
-    p_pc b_pc e_pc a_pc     (* PC *)
-    a_cap                   (* Value capability *)
-    p_seal b_seal e_seal τ  (* Seal capability *)
-    v w4 w5                 (* Values in registers *)
+    p_pc b_pc e_pc a_pc       (* PC *)
+    a_cap                     (* Value capability *)
+    p_seal b_seal e_seal τ Φ  (* Seal capability *)
+    v w4 w5                   (* Values in registers *)
     φ:
 
     let instrs := store_global_macro_int_instrs in
-    let length := (length instrs) in
+    let scap := SCap RW a_cap (a_cap ^+ 1)%a a_cap in
 
     ExecPCPerm p_pc →
-    SubBounds b_pc e_pc a_pc (a_pc ^+ length)%a →
+    SubBounds b_pc e_pc a_pc (a_pc ^+ (length instrs))%a →
 
     permit_unseal p_seal = true →
     withinBounds b_seal e_seal τ = true →
@@ -54,32 +53,33 @@ Section store_int.
       ∗ codefrag a_pc instrs
 
       ∗ r_t1 ↦ᵣ WSealRange p_seal b_seal e_seal τ
-      ∗ r_t2 ↦ᵣ WSealed τ (SCap RW a_cap (a_cap ^+ 1)%a a_cap)
-      ∗ (∃ w, a_cap ↦ₐ w ∗ ⌜is_z w⌝)
-
+      ∗ r_t2 ↦ᵣ WSealed τ scap
       ∗ r_t3 ↦ᵣ v
       ∗ r_t4 ↦ᵣ w4
       ∗ r_t5 ↦ᵣ w5
 
-      ∗ ▷ (PC ↦ᵣ WCap p_pc b_pc e_pc (a_pc ^+ length)%a
+      ∗ ▷ (valid_sealed (WSealed τ scap) τ Φ)
+      ∗ seal_state sealN a_cap τ
+      ∗ na_own logrel_nais ⊤
+
+      ∗ ▷ (PC ↦ᵣ WCap p_pc b_pc e_pc (a_pc ^+ (length instrs))%a
              ∗ codefrag a_pc instrs
 
              ∗ r_t1 ↦ᵣ WSealRange p_seal b_seal e_seal τ
-             ∗ r_t2 ↦ᵣ WSealed τ (SCap RW a_cap (a_cap ^+ 1)%a a_cap)
+             ∗ r_t2 ↦ᵣ WSealed τ scap
              ∗ r_t3 ↦ᵣ v
              ∗ (∃ w, r_t4 ↦ᵣ w)
              ∗ (∃ w, r_t5 ↦ᵣ w)
 
-             ∗ a_cap ↦ₐ v
-             ∗ ⌜is_z v⌝
+             ∗ isIntSealed (WCap RW a_cap (a_cap ^+ 1)%a a_cap)
+             ∗ na_own logrel_nais ⊤
 
              -∗ WP Seq (Instr Executable) {{ λ v, φ v ∨ ⌜v = FailedV⌝ }})
     -∗ WP Seq (Instr Executable) {{ λ v, φ v ∨ ⌜v = FailedV⌝ }}.
   Proof.
     iIntros (? ? Hexec ? ? ? ?)
-      "(HPC & Hprog & Hr_t1 & Hr_t2 & Haddr & Hr_t3 & Hr_t4 & Hr_t5 & Hφ)".
-    subst instrs length; simpl in *.
-    iDestruct "Haddr" as (w) "[Ha_cap %]".
+      "(HPC & Hprog & Hr_t1 & Hr_t2 & Hr_t3 & Hr_t4 & Hr_t5 & #Hseal_valid & [#Hseal_inv #Hseal_pred] & Hna & Hφ)".
+    subst instrs; simpl in *.
 
     focus_block_0 "Hprog" as "Hblock" "Hcont".
 
@@ -91,23 +91,42 @@ Section store_int.
     unfocus_block "Hblock" "Hcont" as "Hprog".
 
     focus_block 1%nat "Hprog" as a_block Ha_block "Hblock" "Hcont".
+
+    iMod (na_inv_acc with "Hseal_inv Hna") as "(>Haddr & Hna & Hclose)"; [ solve_ndisj .. |].
+    iDestruct "Haddr" as (v') "(Haddr & _)".
+
+    iDestruct (seal_state_valid_sealed_pred_eq with "[$Hseal_inv $Hseal_pred] Hseal_valid") as "Heqv".
+
     iGo "Hblock".
+
+    iMod ("Hclose" with "[Haddr $Hna]") as "Hna".
+    { by iExists _; iFrame. }
+
     unfocus_block "Hblock" "Hcont" as "Hprog".
 
     iApply "Hφ".
     replace (a_block ^+ 2)%a with (a_pc ^+ 8)%a by solve_addr.
     iFrame.
-    iSplitL "Hr_t4"; eauto.
+    iSplitL "Hr_t4"; [ eauto |].
+    iSplitL "Hr_t5"; [ eauto |].
+
+    rewrite -/scap.
+    iDestruct "Hseal_valid" as (x) "(%Heq & _ & _ & HΦ)".
+    inversion Heq; subst.
+    iSpecialize ("Heqv" $! (WSealable scap)).
+    iRewrite "Heqv".
+    iFrame "HΦ".
   Qed.
 
   Lemma store_global_macro_int_closure_spec
     p_pc b_pc       (* PC *)
     a_cap           (* Value capability *)
-    p_seal τ        (* Seal capability *)
+    p_seal τ Φ      (* Seal capability *)
     adv v w3 w4 w5  (* Values in registers *)
     φ:
 
     let instrs := store_global_macro_int_closure_instrs τ in
+    let scap := SCap RW a_cap (a_cap ^+ 1)%a a_cap in
     let e_pc := (b_pc ^+ length instrs)%a in
 
     ExecPCPerm p_pc →
@@ -122,31 +141,35 @@ Section store_int.
       ∗ region_mapsto b_pc e_pc instrs
 
       ∗ r_t0 ↦ᵣ adv
-      ∗ r_t1 ↦ᵣ WSealed τ (SCap RW a_cap (a_cap ^+ 1)%a a_cap)
-      ∗ (∃ w, a_cap ↦ₐ w ∗ ⌜is_z w⌝)
-
+      ∗ r_t1 ↦ᵣ WSealed τ scap
       ∗ r_t2 ↦ᵣ v
       ∗ r_t3 ↦ᵣ w3
       ∗ r_t4 ↦ᵣ w4
       ∗ r_t5 ↦ᵣ w5
 
+      ∗ ▷ (valid_sealed (WSealed τ scap) τ Φ)
+      ∗ seal_state sealN a_cap τ
+      ∗ na_own logrel_nais ⊤
+
       ∗ ▷ (PC ↦ᵣ updatePcPerm adv
              ∗ region_mapsto b_pc e_pc instrs
 
              ∗ r_t0 ↦ᵣ adv
-             ∗ r_t1 ↦ᵣ WSealed τ (SCap RW a_cap (a_cap ^+ 1)%a a_cap)
-             ∗ (∃ w, a_cap ↦ₐ w ∗ ⌜is_z w⌝)
-
+             ∗ r_t1 ↦ᵣ WSealed τ scap
              ∗ r_t2 ↦ᵣ WInt 0
              ∗ r_t3 ↦ᵣ WInt 0
              ∗ r_t4 ↦ᵣ WInt 0
              ∗ r_t5 ↦ᵣ WInt 0
 
+             ∗ isIntSealed (WCap RW a_cap (a_cap ^+ 1)%a a_cap)
+             ∗ na_own logrel_nais ⊤
+
              -∗ WP Seq (Instr Executable) {{ λ v, φ v ∨ ⌜v = FailedV⌝ }})
     -∗ WP Seq (Instr Executable) {{ λ v, φ v ∨ ⌜v = FailedV⌝ }}.
   Proof.
-    iIntros (? ? ? Hbounds ? ? ? ?)
-      "(HPC & Hprog & Hr_t0 & Hr_t1 & Haddr & Hr_t2 & Hr_t3 & Hr_t4 & Hr_t5 & Hφ)".
+    iIntros (? ? ? ? Hbounds ? ? ? ?)
+      "(HPC & Hprog & Hr_t0 & Hr_t1 & Hr_t2 & Hr_t3 & Hr_t4 & Hr_t5 & Hseal_valid & Hseal_inv & Hna & Hφ)".
+    subst scap.
 
     iDestruct (region_mapsto_split b_pc e_pc (b_pc ^+ 1)%a _ _ with "Hprog") as "(Hseal & Hprog)"
       ; [ subst e_pc; solve_addr + | rewrite /finz.dist; solve_finz +Hbounds |].
@@ -176,7 +199,7 @@ Section store_int.
 
     focus_block 1%nat "Hprog" as addr_block1 Haddr_block1 "Hblock" "Hcont".
 
-    iApply (store_global_macro_int_spec with "[-]"); last iFrame; eauto.
+    iApply store_global_macro_int_spec; last iFrame; eauto.
 
     iIntros "!> (HPC & Hblock & Hr_t1 & Hr_t2 & Hr_t3 & Hr_t4 & Hr_t5 & Haddr)".
     iDestruct "Hr_t4" as (w4') "Hr_t4".
@@ -206,7 +229,6 @@ Section store_int.
 
     replace ((b_pc ^+ 1) ^+ 19%nat)%a with (b_pc ^+ 20)%a by solve_addr.
     iFrame.
-    iExists v; iFrame.
   Qed.
 
   Lemma store_global_macro_int_closure_spec_full
@@ -217,12 +239,12 @@ Section store_int.
     rmap:
 
     let instrs := store_global_macro_int_closure_instrs τ in
-    let length := length instrs in
-    let e_pc := (b_pc ^+ length)%a in
+    let scap := SCap RW a_cap (a_cap ^+ 1)%a a_cap in
+    let e_pc := (b_pc ^+ length instrs)%a in
 
     ExecPCPerm p_pc →
-    ContiguousRegion b_pc length →
-    SubBounds b_pc e_pc b_pc (b_pc ^+ length)%a →
+    ContiguousRegion b_pc (length instrs) →
+    SubBounds b_pc e_pc b_pc (b_pc ^+ (length instrs))%a →
 
     permit_unseal p_seal = true →
     withinBounds a_cap (a_cap ^+ 1)%a a_cap = true →
@@ -233,40 +255,38 @@ Section store_int.
     ⊢ (PC ↦ᵣ WCap p_pc b_pc e_pc (b_pc ^+ 1)%a
       ∗ region_mapsto b_pc e_pc instrs
 
-      ∗ r_t0 ↦ᵣ adv
-      ∗ r_t1 ↦ᵣ WSealed τ (SCap RW a_cap (a_cap ^+ 1)%a a_cap)
-      ∗ (∃ w, a_cap ↦ₐ w ∗ ⌜is_z w⌝)
-
+      ∗ r_t0 ↦ᵣ adv ∗ interp adv
+      ∗ r_t1 ↦ᵣ WSealed τ scap ∗ interp (WSealed τ scap)
       ∗ r_t2 ↦ᵣ v
       ∗ r_t3 ↦ᵣ w3
 
       ∗ seal_state sealN a_cap τ
       ∗ na_own logrel_nais ⊤
 
       ∗ ([∗ map] r_i↦w_i ∈ rmap, r_i ↦ᵣ w_i ∗ ⌜is_z w_i = true⌝)
-      ∗ interp adv
+      (* ∗ ([∗ map] r_i↦w_i ∈ rmap, r_i ↦ᵣ w_i ∗ interp w_i) *)
 
       -∗ WP Seq (Instr Executable)
             {{ v,
                 (⌜v = HaltedV⌝ → (∃ r: Reg, full_map r ∧ registers_mapsto r ∗ na_own logrel_nais ⊤))
                   ∨ ⌜ v = FailedV ⌝ }})%I.
   Proof.
     iIntros (? ? ? ? Hbounds ? ? ? ? Hdom)
-      "(HPC & Hprog & Hr_t0 & Hr_t1 & Haddr & Hr_t2 & Hr_t3 & Hseal & Hna & Hrmap & #Hadv_interp)".
+      "(HPC & Hprog & Hr_t0 & #Hadv_interp & Hr_t1 & #Hseal_interp & Hr_t2 & Hr_t3 & Hseal_inv & Hna & Hrmap)".
 
     iDestruct (jmp_to_unknown with "Hadv_interp") as "Cont".
 
     iExtractList "Hrmap" [r_t4; r_t5] as ["[Hr_t4 _]"; "[Hr_t5 _]"].
 
-    iApply (store_global_macro_int_closure_spec with "[-]")
-      ; last iFrame; eauto; [ solve_addr + |].
+    iAssert (∃ Φ, ▷ valid_sealed (WSealed τ scap) τ Φ)%I as (Φ) "-#Hseal_valid".
+    { iDestruct (interp_valid_sealed with "Hseal_interp") as (Φ) "Hseal_valid".
+      by iExists Φ. }
 
-    iIntros "!> (HPC & Hprog & Hr_t0 & Hr_t1 & Haddr & Hr_t2 & Hr_t3 & Hr_t4 & Hr_t5)".
+    iApply (store_global_macro_int_closure_spec); last iFrame; eauto; [ solve_addr + |].
 
-    iApply (wp_wand with "[-]"); [| iIntros (?) "?"; by iLeft ].
+    iIntros "!> (HPC & Hprog & Hr_t0 & Hr_t1 & Hr_t2 & Hr_t3 & Hr_t4 & Hr_t5 & Hseal & Hna)".
 
-    iDestruct "Haddr" as (w') "Haddr".
-    iMod (isIntSealed_alloc a_cap w' with "Haddr") as "Haddr".
+    iApply (wp_wand with "[-]"); [| iIntros (?) "?"; by iLeft ].
 
     iApply "Cont"; eauto; iFrame; revgoals.
     { iAssert (⌜is_z (WInt 0) = true⌝)%I as "H"; [ done |].
@@ -282,16 +302,6 @@ Section store_int.
         destruct w; [| discriminate.. ].
         by rewrite fixpoint_interp1_eq. }
 
-      iAssert (interp (WSealed τ (SCap RW a_cap (a_cap ^+ 1)%a a_cap)))%I as "#Hseal_interp".
-      { iApply fixpoint_interp1_eq.
-        iExists isIntSealed.
-        repeat iSplit.
-        - iPureIntro.
-          apply isIntSealed_persistent.
-        - iDestruct "Hseal" as "(_ & Hpred)".
-          iFrame.
-        - by iExists w'. }
-
       iCombine "Hr_t1 Hseal_interp" as "Hr_t1".
       iCombine "Hr_t0 Hadv_interp" as "Hr_t0".
       iInsertList "Hrmap" [r_t1; r_t0].