mutable_typed_shared_data: Generalise address of the WSealRange

logsem · Jun 28, 2023 · 15ebe14 · 15ebe14
1 parent 1a0c84a
commit 15ebe14
Show file tree

Hide file tree

Showing 3 changed files with 81 additions and 128 deletions.
diff --git a/theories/examples/mutable_typed_shared_data/invariants.v b/theories/examples/mutable_typed_shared_data/invariants.v
@@ -13,7 +13,7 @@ Section invariants.
 
   (* Note: `arch_sealing.seal_state` is the combination of `seal_pred` and a invariant. *)
   (* > This invariant pins `WSealRange` in memory to retrieve an access to it. *)
-  (* For simplicity, we will explicitly split `seal_pred` and the invariant on `WSealRange`. *)
+  (* For simplicity, `WSealRange` will be easily accessible (hidden in front of our instructions). *)
 
   (* Fact that the value `w`, if `interp w`, has been validly sealed satisfying a `Φ` predicate. *)
   Definition valid_sealed w τ Φ := arch_sealing.valid_sealed w τ Φ.

diff --git a/theories/examples/mutable_typed_shared_data/load.v b/theories/examples/mutable_typed_shared_data/load.v
@@ -14,13 +14,13 @@ Section load_int.
       Load r_t2 r_t2
     ].
 
-  (* Instructions to load in `r_t1` the integer store in the seal `r_t1`, sealed by the hidden `WSealRange`. *)
+  (* Instructions to load in `r_t1` the integer store in the seal `r_t1`, sealed by the hidden `WSealRange` placed at `off_seal`. *)
   (* This will return a new sealed value in `r_t1` and override the registers r_t2`. *)
-  Definition load_global_macro_int_closure_instrs (τ : OType) :=
-    [ WSealRange (true, true) τ (τ ^+ 1)%ot τ ] ++ encodeInstrsW [
+  Definition load_global_macro_int_closure_instrs (off_seal : Z) (τ : OType) :=
+    encodeInstrsW [
       Mov r_t2 r_t1;
       Mov r_t1 PC;
-      Lea r_t1 (-2)%Z;
+      Lea r_t1 (off_seal - 1)%Z;
       Load r_t1 r_t1
     ] ++ load_global_macro_int_instrs ++ encodeInstrsW [
       Mov r_t1 r_t2;
@@ -98,28 +98,31 @@ Section load_int.
     iSplitL "Hr_t2"; eauto.
   Qed.
 
-  Lemma load_global_macro_int_closure_spec
-    p_pc b_pc   (* PC *)
-    a_cap       (* Address *)
-    p_seal τ Φ  (* Seal capability *)
-    adv w2      (* Values in registers *)
+  Lemma load_global_macro_int_closure_spec (off_seal : Z)
+    p_pc b_pc e_pc a_pc  (* PC *)
+    a_seal a_cap         (* Address *)
+    p_seal τ Φ           (* Seal capability *)
+    adv w2               (* Values in registers *)
     φ:
 
-    let instrs := load_global_macro_int_closure_instrs τ in
+    let instrs := load_global_macro_int_closure_instrs off_seal τ 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 instrs) →
-    SubBounds b_pc e_pc (b_pc ^+ 1)%a (b_pc ^+ (length instrs))%a →
+    ContiguousRegion a_pc (length instrs) →
+    SubBounds b_pc e_pc a_pc (a_pc ^+ (length instrs))%a →
 
     permit_unseal p_seal = true →
     withinBounds a_cap (a_cap ^+ 1)%a a_cap = true →
     withinBounds τ (τ ^+ 1)%ot τ = true →
 
-    PC ↦ᵣ WCap p_pc b_pc e_pc (b_pc ^+ 1)%a
-      ∗ region_mapsto b_pc e_pc instrs
+    (a_pc + off_seal)%a = Some a_seal →
+    withinBounds b_pc e_pc a_seal = true →
 
+    PC ↦ᵣ WCap p_pc b_pc e_pc a_pc
+      ∗ region_mapsto a_pc (a_pc ^+ length instrs)%a instrs
+
+      ∗ a_seal ↦ₐ WSealRange p_seal τ (τ ^+ 1)%ot τ
       ∗ r_t0 ↦ᵣ adv
       ∗ r_t1 ↦ᵣ WSealed τ scap
       ∗ r_t2 ↦ᵣ w2
@@ -129,7 +132,7 @@ Section load_int.
       ∗ na_own logrel_nais ⊤
 
       ∗ ▷ (PC ↦ᵣ updatePcPerm adv
-             ∗ region_mapsto b_pc e_pc instrs
+             ∗ region_mapsto a_pc (a_pc ^+ length instrs)%a instrs
 
              ∗ r_t0 ↦ᵣ adv
              ∗ (∃ w, r_t1 ↦ᵣ w ∗ ⌜is_z w⌝)
@@ -141,30 +144,16 @@ Section load_int.
              -∗ WP Seq (Instr Executable) {{ λ v, φ v }})
     -∗ WP Seq (Instr Executable) {{ λ v, φ v }}.
   Proof.
-    iIntros (? ? ? ? Hbounds ? ? ? ?)
-      "(HPC & Hprog & Hr_t0 & Hr_t1 & Hr_t2 & Hseal_valid & Hseal_pred & Hna & Hφ)".
-
-    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 |].
+    iIntros (? ? ? Hbounds ? ? ? ? ? ?)
+      "(HPC & Hprog & Hseal & Hr_t0 & Hr_t1 & Hr_t2 & Hseal_valid & Hseal_pred & Hna & Hφ)".
 
-    iDestruct (region_mapsto_single with "Hseal") as (seal) "(Hseal & %w)"
-      ; [ solve_addr +Hbounds | case: w => <- ].
-
-    match goal with
-      |- context [ ([[ (b_pc ^+ 1)%a, _ ]] ↦ₐ [[ ?instrs ]])%I ] => set instrs' := instrs
-    end.
-
-    iAssert (codefrag (b_pc ^+ 1)%a instrs') with "[Hprog]" as "Hprog".
-    { replace e_pc with ((b_pc ^+ 1) ^+ (length instrs'))%a
-        ; [ iFrame | subst e_pc; solve_addr ]. }
-
-    clear Hbounds.
+    iAssert (codefrag a_pc instrs) with "[Hprog]" as "Hprog"; [ iFrame |].
 
     codefrag_facts "Hprog".
     focus_block_0 "Hprog" as "Hblock" "Hcont".
 
     iGo "Hblock".
-    { transitivity (Some b_pc); [ solve_addr +H6 | eauto ]. }
+    { transitivity (a_pc + off_seal)%a; [ solve_addr +H6 | eauto ]. }
 
     iInstr "Hblock".
 
@@ -188,49 +177,36 @@ Section load_int.
     unfocus_block "Hblock" "Hcont" as "Hprog".
 
     iApply "Hφ"; iFrame.
-
-    iAssert (codefrag b_pc _)%I with "[Hseal]" as "Hseal".
-    { iDestruct (region_mapsto_cons with "[Hseal]") as "Hseal"; [| | iFrame | done ].
-      { transitivity (Some (b_pc ^+ 1))%a; [ solve_addr +H4 | reflexivity ]. }
-      { solve_addr +. }
-
-      rewrite /region_mapsto finz_seq_between_empty; [ done | solve_addr + ]. }
-
-    unfold codefrag; simpl.
-
-    iDestruct (region_mapsto_split with "[$Hseal $Hprog]") as "Hprog";
-      [ solve_addr + | rewrite /finz.dist; solve_finz |].
-
-    replace ((b_pc ^+ 1) ^+ 9%nat)%a with (b_pc ^+ 10)%a by solve_addr.
-    iFrame.
-
     by iExists _; iFrame.
   Qed.
 
-  Lemma load_global_macro_int_closure_spec_full
-    p_pc b_pc  (* PC *)
-    a_cap      (* Address *)
-    p_seal τ   (* Seal capability *)
-    adv w2     (* Values in registers *)
+  Lemma load_global_macro_int_closure_spec_full (off_seal : Z)
+    p_pc b_pc e_pc a_pc  (* PC *)
+    a_seal a_cap         (* Address *)
+    p_seal τ             (* Seal capability *)
+    adv w2               (* Values in registers *)
     rmap:
 
-    let instrs := load_global_macro_int_closure_instrs τ in
+    let instrs := load_global_macro_int_closure_instrs off_seal τ 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 instrs) →
-    SubBounds b_pc e_pc b_pc (b_pc ^+ (length instrs))%a →
+    ContiguousRegion a_pc (length instrs) →
+    SubBounds b_pc e_pc a_pc (a_pc ^+ (length instrs))%a →
 
     permit_unseal p_seal = true →
     withinBounds a_cap (a_cap ^+ 1)%a a_cap = true →
     withinBounds τ (τ ^+ 1)%ot τ = true →
 
+    (a_pc + off_seal)%a = Some a_seal →
+    withinBounds b_pc e_pc a_seal = true →
+
     dom rmap = all_registers_s ∖ {[ PC; r_t0; r_t1; r_t2 ]} →
 
-    ⊢ (PC ↦ᵣ WCap p_pc b_pc e_pc (b_pc ^+ 1)%a
-      ∗ region_mapsto b_pc e_pc instrs
+    ⊢ (PC ↦ᵣ WCap p_pc b_pc e_pc a_pc
+      ∗ region_mapsto a_pc (a_pc ^+ length instrs)%a instrs
 
+      ∗ a_seal ↦ₐ WSealRange p_seal τ (τ ^+ 1)%ot τ
       ∗ r_t0 ↦ᵣ adv ∗ interp adv
       ∗ r_t1 ↦ᵣ WSealed τ scap ∗ interp (WSealed τ scap)
       ∗ r_t2 ↦ᵣ w2
@@ -243,16 +219,16 @@ Section load_int.
       -∗ WP Seq (Instr Executable)
             {{ v, ⌜v = HaltedV⌝ → ∃ r: Reg, full_map r ∧ registers_mapsto r ∗ na_own logrel_nais ⊤ }})%I.
   Proof.
-    iIntros (? ? ? ? Hbounds ? ? ? ? Hdom)
-      "(HPC & Hprog & Hr_t0 & #Hadv_interp & Hr_t1 & #Hseal_interp & Hr_t2 & Hseal_pred & Hna & Hrmap)".
+    iIntros (? ? ? Hbounds ? ? ? ? ? ? Hdom)
+      "(HPC & Hprog & Hseal & Hr_t0 & #Hadv_interp & Hr_t1 & #Hseal_interp & Hr_t2 & Hseal_pred & Hna & Hrmap)".
 
     iDestruct (jmp_to_unknown with "Hadv_interp") as "Cont".
 
     iAssert (∃ Φ, ▷ valid_sealed (WSealed τ scap) τ Φ)%I as (Φ) "-#Hseal_valid".
     { iDestruct (interp_valid_sealed with "Hseal_interp") as (Φ) "Hseal_valid".
       by iExists Φ. }
 
-    iApply load_global_macro_int_closure_spec; last iFrame; eauto; [ solve_addr + |].
+    iApply load_global_macro_int_closure_spec; last iFrame; eauto.
 
     iIntros "!> (HPC & Hprog & Hr_t0 & Hr_t1 & Hr_t2 & Hseal_int & Hna)".
     iDestruct "Hr_t1" as (v) "Hr_t1".

diff --git a/theories/examples/mutable_typed_shared_data/store.v b/theories/examples/mutable_typed_shared_data/store.v
@@ -19,19 +19,19 @@ Section store_int.
       Store r_t4 r_t3
     ].
 
-  (* Instructions to store a word `r_t2` in the seal `r_t1`, sealed by the hidden `WSealRange`. *)
+  (* Instructions to store a word `r_t2` in the seal `r_t1`, sealed by the hidden `WSealRange` placed at `off_seal`. *)
 
   (* This function will succeed only if the word in `r_t2` is an integer. *)
   (* > Otherwise, the machine will enter in a `Failed` state. *)
 
   (* This will return a new sealed value in `r_t1` and override the registers r_t2`, `r_t3`, `r_t4` and `r_t5`. *)
   (* > Note: The new sealed value is the same as the old one, both keeping the new value. *)
-  Definition store_global_macro_int_closure_instrs (τ : OType) :=
-    [ WSealRange (true, true) τ (τ ^+ 1)%ot τ ] ++ encodeInstrsW [
+  Definition store_global_macro_int_closure_instrs (off_seal : Z) (τ : OType) :=
+    encodeInstrsW [
       Mov r_t3 r_t2;
       Mov r_t2 r_t1;
       Mov r_t1 PC;
-      Lea r_t1 (-3)%Z;
+      Lea r_t1 (off_seal - 2)%Z;
       Load r_t1 r_t1
     ] ++ store_global_macro_int_instrs ++ encodeInstrsW [
       Mov r_t1 r_t2;
@@ -131,28 +131,31 @@ Section store_int.
     iSplitL "Hr_t4"; eauto.
   Qed.
 
-  Lemma store_global_macro_int_closure_spec
-    p_pc b_pc       (* PC *)
-    a_cap           (* Address *)
-    p_seal τ Φ      (* Seal capability *)
-    adv v w3 w4 w5  (* Values in registers *)
+  Lemma store_global_macro_int_closure_spec (off_seal : Z)
+    p_pc b_pc e_pc a_pc  (* PC *)
+    a_seal a_cap         (* Address *)
+    p_seal τ Φ           (* Seal capability *)
+    adv v w3 w4 w5       (* Values in registers *)
     φ:
 
-    let instrs := store_global_macro_int_closure_instrs τ in
+    let instrs := store_global_macro_int_closure_instrs off_seal τ 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 instrs) →
-    SubBounds b_pc e_pc (b_pc ^+ 1)%a (b_pc ^+ (length instrs))%a →
+    ContiguousRegion a_pc (length instrs) →
+    SubBounds b_pc e_pc a_pc (a_pc ^+ (length instrs))%a →
 
     permit_unseal p_seal = true →
     withinBounds a_cap (a_cap ^+ 1)%a a_cap = true →
     withinBounds τ (τ ^+ 1)%ot τ = true →
 
-    PC ↦ᵣ WCap p_pc b_pc e_pc (b_pc ^+ 1)%a
-      ∗ region_mapsto b_pc e_pc instrs
+    (a_pc + off_seal)%a = Some a_seal →
+    withinBounds b_pc e_pc a_seal = true →
+
+    PC ↦ᵣ WCap p_pc b_pc e_pc a_pc
+      ∗ region_mapsto a_pc (a_pc ^+ length instrs)%a instrs
 
+      ∗ a_seal ↦ₐ WSealRange p_seal τ (τ ^+ 1)%ot τ
       ∗ r_t0 ↦ᵣ adv
       ∗ r_t1 ↦ᵣ WSealed τ scap
       ∗ r_t2 ↦ᵣ v
@@ -165,7 +168,7 @@ Section store_int.
       ∗ na_own logrel_nais ⊤
 
       ∗ ▷ (PC ↦ᵣ updatePcPerm adv
-             ∗ region_mapsto b_pc e_pc instrs
+             ∗ region_mapsto a_pc (a_pc ^+ length instrs)%a instrs
 
              ∗ r_t0 ↦ᵣ adv
              ∗ r_t1 ↦ᵣ WSealed τ scap
@@ -180,30 +183,16 @@ Section store_int.
              -∗ 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 & Hr_t2 & Hr_t3 & Hr_t4 & Hr_t5 & Hseal_valid & Hseal_pred & Hna & Hφ)".
-
-    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 |].
+    iIntros (? ? ? Hbounds ? ? ? ? ? ?)
+      "(HPC & Hprog & Hseal & Hr_t0 & Hr_t1 & Hr_t2 & Hr_t3 & Hr_t4 & Hr_t5 & Hseal_valid & Hseal_pred & Hna & Hφ)".
 
-    iDestruct (region_mapsto_single with "Hseal") as (seal) "(Hseal & %w)"
-      ; [ solve_addr +Hbounds | case: w => <- ].
-
-    match goal with
-      |- context [ ([[ (b_pc ^+ 1)%a, _ ]] ↦ₐ [[ ?instrs ]])%I ] => set instrs' := instrs
-    end.
-
-    iAssert (codefrag (b_pc ^+ 1)%a instrs') with "[Hprog]" as "Hprog".
-    { replace e_pc with ((b_pc ^+ 1) ^+ (length instrs'))%a
-        ; [ iFrame | subst e_pc; solve_addr ]. }
-
-    clear Hbounds.
+    iAssert (codefrag a_pc instrs) with "[Hprog]" as "Hprog"; [ iFrame |].
 
     codefrag_facts "Hprog".
     focus_block_0 "Hprog" as "Hblock" "Hcont".
 
     iGo "Hblock".
-    { transitivity (Some b_pc); [ solve_addr +H6 | eauto ]. }
+    { transitivity (a_pc + off_seal)%a; [ solve_addr +H6 | eauto ]. }
 
     iInstr "Hblock".
 
@@ -226,47 +215,35 @@ Section store_int.
     unfocus_block "Hblock" "Hcont" as "Hprog".
 
     iApply "Hφ"; iFrame.
-
-    iAssert (codefrag b_pc _)%I with "[Hseal]" as "Hseal".
-    { iDestruct (region_mapsto_cons with "[Hseal]") as "Hseal"; [| | iFrame | done ].
-      { transitivity (Some (b_pc ^+ 1))%a; [ solve_addr +H4 | reflexivity ]. }
-      { solve_addr +. }
-
-      rewrite /region_mapsto finz_seq_between_empty; [ done | solve_addr + ]. }
-
-    unfold codefrag; simpl.
-
-    iDestruct (region_mapsto_split with "[$Hseal $Hprog]") as "Hprog";
-      [ solve_addr + | rewrite /finz.dist; solve_finz |].
-
-    replace ((b_pc ^+ 1) ^+ 19%nat)%a with (b_pc ^+ 20)%a by solve_addr.
-    iFrame.
   Qed.
 
-  Lemma store_global_macro_int_closure_spec_full
-    p_pc b_pc  (* PC *)
-    a_cap      (* Address *)
-    p_seal τ   (* Seal capability *)
-    adv v w3   (* Values in registers *)
+  Lemma store_global_macro_int_closure_spec_full (off_seal : Z)
+    p_pc b_pc e_pc a_pc  (* PC *)
+    a_seal a_cap         (* Address *)
+    p_seal τ             (* Seal capability *)
+    adv v w3             (* Values in registers *)
     rmap:
 
-    let instrs := store_global_macro_int_closure_instrs τ in
+    let instrs := store_global_macro_int_closure_instrs off_seal τ 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 instrs) →
-    SubBounds b_pc e_pc b_pc (b_pc ^+ (length instrs))%a →
+    ContiguousRegion a_pc (length instrs) →
+    SubBounds b_pc e_pc a_pc (a_pc ^+ (length instrs))%a →
 
     permit_unseal p_seal = true →
     withinBounds a_cap (a_cap ^+ 1)%a a_cap = true →
     withinBounds τ (τ ^+ 1)%ot τ = true →
 
+    (a_pc + off_seal)%a = Some a_seal →
+    withinBounds b_pc e_pc a_seal = true →
+
     dom rmap = all_registers_s ∖ {[ PC; r_t0; r_t1; r_t2; r_t3 ]} →
 
-    ⊢ (PC ↦ᵣ WCap p_pc b_pc e_pc (b_pc ^+ 1)%a
-      ∗ region_mapsto b_pc e_pc instrs
+    ⊢ (PC ↦ᵣ WCap p_pc b_pc e_pc a_pc
+      ∗ region_mapsto a_pc (a_pc ^+ length instrs)%a instrs
 
+      ∗ a_seal ↦ₐ WSealRange p_seal τ (τ ^+ 1)%ot τ
       ∗ r_t0 ↦ᵣ adv ∗ interp adv
       ∗ r_t1 ↦ᵣ WSealed τ scap ∗ interp (WSealed τ scap)
       ∗ r_t2 ↦ᵣ v
@@ -282,8 +259,8 @@ Section store_int.
                 (⌜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 & #Hadv_interp & Hr_t1 & #Hseal_interp & Hr_t2 & Hr_t3 & Hseal_state & Hna & Hrmap)".
+    iIntros (? ? ? Hbounds ? ? ? ? ? ? Hdom)
+      "(HPC & Hprog & Hseal & Hr_t0 & #Hadv_interp & Hr_t1 & #Hseal_interp & Hr_t2 & Hr_t3 & Hseal_state & Hna & Hrmap)".
 
     iDestruct (jmp_to_unknown with "Hadv_interp") as "Cont".
 
@@ -293,7 +270,7 @@ Section store_int.
     { iDestruct (interp_valid_sealed with "Hseal_interp") as (Φ) "Hseal_valid".
       by iExists Φ. }
 
-    iApply store_global_macro_int_closure_spec; last iFrame; eauto; [ solve_addr + |].
+    iApply store_global_macro_int_closure_spec; last iFrame; eauto.
 
     iIntros "!> (HPC & Hprog & Hr_t0 & Hr_t1 & Hr_t2 & Hr_t3 & Hr_t4 & Hr_t5 & Hseal_int & Hna)".