diff --git a/_CoqProject b/_CoqProject index 3aded5149de892a5ae20a9b31984e980518395c3..acb5d6cacc460f338b1921f0b093bcac9d91c159 100644 --- a/_CoqProject +++ b/_CoqProject @@ -77,7 +77,8 @@ theories/stacked_borrows/steps_inv.v theories/stacked_borrows/tactics.v theories/stacked_borrows/class_instances.v theories/stacked_borrows/tkmap_view.v -theories/stacked_borrows/heap.v +theories/stacked_borrows/logical_state.v +theories/stacked_borrows/inv_accessors.v theories/stacked_borrows/steps_refl.v theories/stacked_borrows/steps_opt.v theories/stacked_borrows/primitive_laws.v diff --git a/theories/stacked_borrows/examples/opt1.v b/theories/stacked_borrows/examples/opt1.v index 8a270ff406c6bd8872313eb32d92ae726e37debf..3779c669eb73a1ca5530fddc2a525b68061a0672 100644 --- a/theories/stacked_borrows/examples/opt1.v +++ b/theories/stacked_borrows/examples/opt1.v @@ -1,5 +1,5 @@ From simuliris.simulation Require Import lifting. -From simuliris.stacked_borrows Require Import proofmode defs lang heap. +From simuliris.stacked_borrows Require Import primitive_laws proofmode. Set Default Proof Using "Type". (** Moving read of mutable reference up across code not using that ref. *) @@ -47,7 +47,7 @@ Definition ex1_opt : ectx := Free "x" ;; "v". -Lemma sim_new_place_local `{sborG Σ} T v_t v_s Ï€ Φ : +Lemma sim_new_place_local `{sborGS Σ} T v_t v_s Ï€ Φ : ⌜length v_t = length v_s⌠-∗ (∀ t l, ⌜length v_s = tsize T⌠-∗ @@ -88,7 +88,7 @@ Qed. then we could use the above generic lemma for [new_place]. currently we don't use it since, in order to apply it, we'd need to use UB that happens during its execution... *) -Lemma sim_opt1 `{sborG Σ} Ï€ : +Lemma sim_opt1 `{sborGS Σ} Ï€ : ⊢ sim_ectx rrel Ï€ ex1_opt ex1_unopt rrel. Proof. iIntros (r_t r_s) "Hrel". @@ -162,7 +162,7 @@ Definition ex1_opt' : ectx := Free "x" ;; "v". -Lemma sim_opt1' `{sborG Σ} Ï€ : +Lemma sim_opt1' `{sborGS Σ} Ï€ : ⊢ sim_ectx rrel Ï€ ex1_opt' ex1_unopt rrel. Proof. iIntros (r_t r_s) "Hrel". diff --git a/theories/stacked_borrows/examples/opt1_down.v b/theories/stacked_borrows/examples/opt1_down.v index 2e622c47c0958e998c9325a6b4aa5e7a772887bf..8e85003b377e28f5f0ed09cceb84bc31ddd3cac7 100644 --- a/theories/stacked_borrows/examples/opt1_down.v +++ b/theories/stacked_borrows/examples/opt1_down.v @@ -1,5 +1,5 @@ From simuliris.simulation Require Import lifting. -From simuliris.stacked_borrows Require Import proofmode defs lang heap. +From simuliris.stacked_borrows Require Import primitive_laws proofmode. Set Default Proof Using "Type". (** Moving a read of a mutable reference down across code that *may* use that ref. *) @@ -46,7 +46,7 @@ Definition ex1_down_opt : ectx := (*Lemma value_rel_poison *) -Lemma sim_opt1_down `{sborG Σ} Ï€ : +Lemma sim_opt1_down `{sborGS Σ} Ï€ : ⊢ sim_ectx rrel Ï€ ex1_down_opt ex1_down_unopt rrel. Proof. iIntros (r_t r_s) "Hrel". diff --git a/theories/stacked_borrows/examples/opt2.v b/theories/stacked_borrows/examples/opt2.v index 6f3f1f51505c556a37d192ef9fa9420dd61eb189..bbe8f0a0f9478328d284cd4802ee429b810f191d 100644 --- a/theories/stacked_borrows/examples/opt2.v +++ b/theories/stacked_borrows/examples/opt2.v @@ -50,7 +50,7 @@ Definition ex2_opt : ectx := "v" . -Lemma sim_opt2 `{sborG Σ} Ï€ : +Lemma sim_opt2 `{sborGS Σ} Ï€ : ⊢ sim_ectx rrel Ï€ ex2_opt ex2_unopt rrel. Proof. iIntros (r_t r_s) "Hrel". @@ -161,7 +161,7 @@ Definition ex2_opt' : ectx := . -Lemma sim_opt2' `{sborG Σ} Ï€ : +Lemma sim_opt2' `{sborGS Σ} Ï€ : ⊢ sim_ectx rrel Ï€ ex2_opt' ex2_unopt' rrel. Proof. iIntros (r_t r_s) "Hrel". diff --git a/theories/stacked_borrows/examples/pure.v b/theories/stacked_borrows/examples/pure.v index 39d538902b6ebf08396fc74e8a8e41ac307604d8..453d757c02507ca426bd0441d0d1e35bb00e2591 100644 --- a/theories/stacked_borrows/examples/pure.v +++ b/theories/stacked_borrows/examples/pure.v @@ -2,7 +2,7 @@ From simuliris.stacked_borrows Require Import proofmode. (** * Some trivial tests to check that the proofmode works *) Section boring_lang. -Context `{sborG Σ}. +Context `{sborGS Σ}. Definition val_rel (r1 r2 : result) : iProp Σ := ⌜r1 = r2âŒ. (*Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{val_rel} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.*) diff --git a/theories/stacked_borrows/heap.v b/theories/stacked_borrows/heap.v deleted file mode 100644 index 133b1476e67dbfe3298b3f64fefe215c2c1fd334..0000000000000000000000000000000000000000 --- a/theories/stacked_borrows/heap.v +++ /dev/null @@ -1,1860 +0,0 @@ -(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *) -From iris.proofmode Require Export tactics. -From iris.bi.lib Require Import fractional. -From iris.base_logic.lib Require Import ghost_map. -From simuliris.base_logic Require Export gen_sim_prog. -From simuliris.simulation Require Export slsls. -From simuliris.simulation Require Import lifting. -From iris.prelude Require Import options. -From simuliris.stacked_borrows Require Import tkmap_view. -From simuliris.stacked_borrows Require Export defs. -From simuliris.stacked_borrows Require Import steps_progress steps_retag. - -Fixpoint heap_array (l : loc) (scs : list scalar) : gmap loc scalar := - match scs with - | [] => ∅ - | sc :: scs' => {[l := sc]} ∪ heap_array (l +â‚— 1) scs' - end. - -Lemma heap_array_singleton l sc : heap_array l [sc] = {[l := sc]}. -Proof. by rewrite /heap_array right_id. Qed. - -Lemma heap_array_lookup l scs sc k : - heap_array l scs !! k = Some sc ↔ - ∃ j, (0 ≤ j)%Z ∧ k = l +â‚— j ∧ scs !! (Z.to_nat j) = Some sc. -Proof. - revert k l; induction scs as [|sc' scs IH]=> l' l /=. - { rewrite lookup_empty. naive_solver lia. } - rewrite -insert_union_singleton_l lookup_insert_Some IH. split. - - intros [[-> ->] | (Hl & j & ? & -> & ?)]. - { eexists 0. rewrite shift_loc_0. naive_solver lia. } - eexists (1 + j)%Z. rewrite shift_loc_assoc !Z.add_1_l Z2Nat.inj_succ; auto with lia. - - intros (j & ? & -> & Hil). destruct (decide (j = 0)); simplify_eq/=. - { rewrite shift_loc_0; eauto. } - right. split. - { rewrite -{1}(shift_loc_0 l). intros ?%(inj (shift_loc _)); lia. } - assert (Z.to_nat j = S (Z.to_nat (j - 1))) as Hj. - { rewrite -Z2Nat.inj_succ; last lia. f_equal; lia. } - rewrite Hj /= in Hil. - eexists (j - 1)%Z. rewrite shift_loc_assoc Z.add_sub_assoc Z.add_simpl_l. - auto with lia. -Qed. - -Lemma heap_array_map_disjoint (h : gmap loc scalar) (l : loc) (scs : list scalar) : - (∀ i, (0 ≤ i)%Z → (i < length scs)%Z → h !! (l +â‚— i) = None) → - (heap_array l scs) ##ₘ h. -Proof. - intros Hdisj. apply map_disjoint_spec=> l' v1 v2. - intros (j&?&->&Hj%lookup_lt_Some%inj_lt)%heap_array_lookup. - move: Hj. rewrite Z2Nat.id // => ?. by rewrite Hdisj. -Qed. - -Lemma lookup_free_mem_1 l l' n σ : - l.1 ≠l'.1 → (free_mem l n σ) !! l' = σ !! l'. -Proof. - induction n as [ | n IH] in l |-*; cbn; first done. - intros Hneq. rewrite lookup_delete_ne; last by congruence. - by apply IH. -Qed. -Lemma lookup_free_mem_2 l l' (n : nat) σ : - l.1 = l'.1 → (l.2 ≤ l'.2 < l.2 + n)%Z → (free_mem l n σ) !! l' = None. -Proof. - induction n as [ | n IH] in l |-*; cbn; first lia. - intros Hchunk Hi. - destruct (decide (l.2 = l'.2)) as [Heq | Hneq]. - - rewrite lookup_delete_None; left. destruct l, l'; simpl in *; congruence. - - rewrite lookup_delete_ne; last congruence. apply IH; first done. destruct l, l'; simpl in *; lia. -Qed. -Lemma lookup_free_mem_3 l l' (n : nat) σ : - l.1 = l'.1 → (l'.2 < l.2)%Z → (free_mem l n σ) !! l' = σ !! l'. -Proof. - induction n as [ | n IH] in l |-*; cbn; first done. - intros Hchunk Hi. rewrite lookup_delete_ne. - - apply IH; first done. destruct l, l'; cbn in *; lia. - - destruct l, l'; cbn in *; intros [=]. lia. -Qed. -Lemma lookup_free_mem_4 l l' (n : nat) σ : - l.1 = l'.1 → (l'.2 >= l.2 + n)%Z → (free_mem l n σ) !! l' = σ !! l'. -Proof. - induction n as [ | n IH] in l |-*; cbn; first done. - intros Hchunk Hi. rewrite lookup_delete_ne. - - apply IH; first done. destruct l, l'; cbn in *; lia. - - destruct l, l'; cbn in *; intros [=]. lia. -Qed. - -Lemma delete_free_mem σ l n o: - (o > 0)%Z → - delete l (free_mem (l +â‚— o) n σ) = free_mem (l +â‚— o) n (delete l σ). -Proof. - intros HO. - induction n as [|n IH] in o, HO|-* => //=. rewrite delete_commute. f_equal. - rewrite shift_loc_assoc IH; [done | lia]. -Qed. - -(* maintain for each tag: the permissions (public or unique) and, optionally, the - regions of memory maintained by it: base locations for target and source, and the length of the maintained allocation. -*) -Class bor_stateG Σ := { - (* Maintaining the stack & scalar for each location *) - (*heap_inG :> ghost_mapG Σ loc (scalar * stack);*) - (*heap_source_name : gname;*) - (*heap_target_name : gname;*) - - (* Maintaining the locations protected by each call id *) - call_inG :> ghost_mapG Σ call_id (gmap ptr_id (gset loc)); - call_name : gname; - - (* tag ownership *) - tag_inG :> tkmapG Σ ptr_id unit; - tag_name : gname; - - (* A view of parts of the heap, conditional on the ptr_id *) - heap_view_inG :> ghost_mapG Σ (ptr_id * loc) scalar; - heap_view_source_name : gname; - heap_view_target_name : gname; - - (* Blocked tags: a set of tag * source location *) - tainted_tag_collection :> ghost_mapG Σ (ptr_id * loc) unit; - tainted_tags_name : gname; -}. - -Section mem_bijection. - Context {Σ} `{bor_stateG Σ}. - - (* The bijection serves the following purpose: - * the blocks are of the same size - * the stacks for the locations are pointwise the same - * every location is either a private location or a public location, which is tied to the tag ghost state - *) - Context (sc_rel : scalar → scalar → iProp Σ). - - Section defs. - (* We need all the maps from the tag interpretation here.... - TODO: can we make that more beautiful? all the different invariants are interleaved in subtle ways, which makes modular reasoning really hard... *) - Context (M_tag : gmap ptr_id (tag_kind * unit)) (M_t M_s : gmap (ptr_id * loc) scalar) (Mcall_t : gmap call_id (gmap ptr_id (gset loc))). - - - Definition call_set_in (M : gmap ptr_id (gset loc)) t l := - ∃ L, M !! t = Some L ∧ l ∈ L. - Definition call_set_in' (M : gmap call_id (gmap ptr_id (gset loc))) c t l := - ∃ M', M !! c = Some M' ∧ call_set_in M' t l. - Definition pub_loc σ_t σ_s (l : loc) : iProp Σ := - ∀ sc_t, ⌜σ_t.(shp) !! l = Some sc_t⌠→ ∃ sc_s, ⌜σ_s.(shp) !! l = Some sc_s⌠∗ sc_rel sc_t sc_s. - Definition priv_loc t (l : loc) : Prop := - ∃ tk, M_tag !! t = Some (tk, tt) ∧ is_Some (M_t !! (t, l)) ∧ - (* local *) - (tk = tk_local ∨ - (* unique with protector *) - (tk = tk_unq ∧ ∃ c, call_set_in' Mcall_t c t l)). - - (* This definition enforces quite strict requirements on the state: - - the domains of the heaps shp are the same - - the stacks are the same - - the call counter is the same - - the tag counter is the same - - the set of ongoing calls is the same - - there's a relation on the scalars stored at locations ([pub_loc]), except when the location is currently controlled by a tag ([priv_loc]). - - Note that, while the definition may appear asymmetric in source and target, due to the well-formedness on states [state_wf] and the relation of the tag maps enforced below, it really is symmetric in practice. - *) - Definition state_rel σ_t σ_s : iProp Σ := - ⌜dom (gset loc) σ_s.(shp) = dom (gset loc) σ_t.(shp)⌠∗ - ⌜σ_s.(sst) = σ_t.(sst)⌠∗ - ⌜σ_s.(snp) = σ_t.(snp)⌠∗ - ⌜σ_s.(snc) = σ_t.(snc)⌠∗ - ⌜σ_s.(scs) = σ_t.(scs)⌠∗ - (* private / public locations of the target *) - ∀ l, ⌜is_Some (σ_t.(shp) !! l)⌠→ pub_loc σ_t σ_s l ∨ ⌜∃ t, priv_loc t lâŒ. - - Global Instance state_rel_persistent σ_t σ_s `{∀ sc_t sc_s, Persistent (sc_rel sc_t sc_s)} : - Persistent (state_rel σ_t σ_s). - Proof. intros. apply _. Qed. - - End defs. -End mem_bijection. - -Section bijection_lemmas. - Context {Σ} `{bor_stateG Σ}. - Context (sc_rel : scalar → scalar → iProp Σ). - Local Notation state_rel := (state_rel sc_rel). - - Lemma state_rel_get_pure Mtag Mt Mcall σ_t σ_s : - state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜σ_s.(sst) = σ_t.(sst) ∧ σ_s.(snp) = σ_t.(snp) ∧ σ_s.(snc) = σ_t.(snc) ∧ σ_s.(scs) = σ_t.(scs)âŒ. - Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. - Lemma state_rel_stacks_eq Mtag Mt Mcall σ_t σ_s : - state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜σ_s.(sst) = σ_t.(sst)âŒ. - Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. - Lemma state_rel_snp_eq Mtag Mt Mcall σ_t σ_s : - state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜σ_s.(snp) = σ_t.(snp)âŒ. - Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. - Lemma state_rel_snc_eq Mtag Mt Mcall σ_t σ_s : - state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜σ_s.(snc) = σ_t.(snc)âŒ. - Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. - Lemma state_rel_calls_eq Mtag Mt Mcall σ_t σ_s : - state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜σ_s.(scs) = σ_t.(scs)âŒ. - Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. - Lemma state_rel_dom_eq Mtag Mt Mcall σ_t σ_s : - state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜dom (gset loc) σ_t.(shp) = dom (gset loc) σ_s.(shp)âŒ. - Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. - - (*Lemma heap_bij_interp_alloc L t : *) - (*(∀ b_s, (b_t, b_s) ∉ L) →*) - (*heap_bij_interp sc_rel M_tag M_t Mcall_t L σ_t σ_s -∗*) - (*heap_bij_interp sc_rel M_tag (Minit_mem ) Mcall_t L (state_upd_mem (init_mem (b_t, 0) n) σ_t)*) - - Lemma state_rel_upd_pub_both M_tag M_t Mcall_t σ_t σ_s l sc_t sc_s : - sc_rel sc_t sc_s -∗ - state_rel M_tag M_t Mcall_t σ_t σ_s -∗ - state_rel M_tag M_t Mcall_t (state_upd_mem (<[l := sc_t]>) σ_t) (state_upd_mem (<[l := sc_s]>) σ_s). - Proof. - iIntros "Hs (%Hshp & % & % & % & % & Hrel)". rewrite /state_rel /=. - iSplitR. { iPureIntro. by rewrite !dom_insert_L Hshp. } - do 4 (iSplitR; first done). - iIntros (l') "%Hsome". destruct (decide (l = l')) as [<- | Hneq]. - - iLeft. iIntros (sc_t') "%Hsc_t'". iExists sc_s. - iSplitR. { iPureIntro. by rewrite lookup_insert. } - move :Hsc_t'; rewrite lookup_insert => [= <-] //. - - rewrite lookup_insert_ne in Hsome; last done. - iDestruct ("Hrel" $! l' with "[//]") as "[Hpub | Hpriv]". - + iLeft. iIntros (sc_t'). rewrite !lookup_insert_ne; [ | done | done]. iApply "Hpub". - + iRight. done. - Qed. - - Lemma priv_loc_upd_insert Mtag Mt Mcall t l t' l' sc : - priv_loc Mtag Mt Mcall t l → - priv_loc Mtag (<[(t',l') := sc]> Mt) Mcall t l. - Proof. - rewrite /priv_loc. intros (tk & Ht & Hs & Hinv). exists tk. - split_and!; [ done | | done]. - apply lookup_insert_is_Some. destruct (decide ((t', l') = (t, l))); eauto. - Qed. - - Lemma state_rel_upd_priv_target M_tag M_t Mcall σ_t σ_s l t sc : - is_Some (σ_t.(shp) !! l) → - priv_loc M_tag M_t Mcall t l → - state_rel M_tag M_t Mcall σ_t σ_s -∗ - state_rel M_tag (<[(t, l) := sc]> M_t) Mcall (state_upd_mem (<[l := sc]>) σ_t) σ_s. - Proof. - iIntros (Hs Hpriv) "(%Hshp & % & % & % & % & Hrel)". rewrite /state_rel /=. - iSplitR. { iPureIntro. rewrite dom_insert_lookup_L; done. } - do 4 (iSplitR; first done). - iIntros (l') "%Hsome". destruct (decide (l = l')) as [<- | Hneq]. - - iRight. iExists t. iPureIntro. apply priv_loc_upd_insert. done. - - rewrite lookup_insert_ne in Hsome; last done. - iDestruct ("Hrel" $! l' with "[//]") as "[Hpub | %Hpriv']". - + iLeft. iIntros (sc_t'). rewrite !lookup_insert_ne; [ | done ]. iApply "Hpub". - + iRight. iPureIntro. destruct Hpriv' as (t' & Hpriv'). exists t'. - by eapply priv_loc_upd_insert. - Qed. - - Lemma state_rel_upd_priv_source M_tag M_t Mcall σ_t σ_s l t sc : - ⌜is_Some (σ_t.(shp) !! l)⌠-∗ - ⌜priv_loc M_tag M_t Mcall t l⌠-∗ - state_rel M_tag M_t Mcall σ_t σ_s -∗ - state_rel M_tag M_t Mcall σ_t (state_upd_mem (<[l := sc]>) σ_s). - Proof. - iIntros (Hs Hpriv) "(%Hshp & % & % & % & % & Hrel)". rewrite /state_rel /=. - iSplitR. { iPureIntro. rewrite dom_insert_lookup_L; [ by rewrite Hshp| ]. - rewrite lookup_lookup_total_dom; first by eauto. - rewrite Hshp. by apply elem_of_dom. - } - do 4 (iSplitR; first done). - iIntros (l') "%Hsome". destruct (decide (l = l')) as [<- | Hneq]. - - iRight. iExists t. done. - - iDestruct ("Hrel" $! l' with "[//]") as "[Hpub | %Hpriv']". - + iLeft. iIntros (sc_t'). rewrite !lookup_insert_ne; [ | done ]. iApply "Hpub". - + iRight. iPureIntro. destruct Hpriv' as (t' & Hpriv'). exists t'. done. - Qed. - - Lemma state_rel_pub_if_not_priv M_tag M_t Mcall σ_t σ_s l : - ⌜is_Some (σ_t.(shp) !! l)⌠-∗ - state_rel M_tag M_t Mcall σ_t σ_s -∗ - ⌜∀ t, ¬ priv_loc M_tag M_t Mcall t l⌠-∗ - pub_loc sc_rel σ_t σ_s l. - Proof. - iIntros (Hs) "(%& % & % & % & % & Hrel) %Hnpriv". - iPoseProof ("Hrel" $! l with "[//]") as "[Hpub | %Hpriv]"; first done. - destruct Hpriv as (t & Hpriv). exfalso; by eapply Hnpriv. - Qed. - - Lemma state_rel_heap_lookup_Some M_tag M_t Mcall σ_t σ_s : - state_rel M_tag M_t Mcall σ_t σ_s -∗ - ∀ l, ⌜is_Some (σ_t.(shp) !! l)⌠↔ ⌜is_Some (σ_s.(shp) !! l)âŒ. - Proof. - iIntros "(%Hshp & _)". iPureIntro. move => l. cbn. by rewrite -!elem_of_dom Hshp. - Qed. - - Lemma state_rel_pub_or_priv M_tag M_t Mcall σ_t σ_s l : - ⌜is_Some (σ_t.(shp) !! l)⌠-∗ - state_rel M_tag M_t Mcall σ_t σ_s -∗ - pub_loc sc_rel σ_t σ_s l ∨ ⌜∃ t, priv_loc M_tag M_t Mcall t lâŒ. - Proof. - iIntros "Hsome Hstate". iDestruct "Hstate" as "(_ & _ & _ & _ & _ & Hl)". - by iApply "Hl". - Qed. - - Lemma pub_loc_lookup σ_t σ_s l : - ⌜is_Some (σ_t.(shp) !! l)⌠-∗ - pub_loc sc_rel σ_t σ_s l -∗ - ∃ sc_t sc_s, ⌜σ_t.(shp) !! l = Some sc_t ∧ σ_s.(shp) !! l = Some sc_s⌠∗ sc_rel sc_t sc_s. - Proof. - iIntros (Hs) "Hpub". destruct Hs as (sc_t & Ht). - iDestruct ("Hpub" $! sc_t with "[//]") as (sc_s) "[%Hs Hsc]". - iExists sc_t, sc_s. eauto. - Qed. - -End bijection_lemmas. - -(* Interpretation for call ids *) -Section call_defs. - Context {Σ} (call_gname : gname) {call_inG : ghost_mapG Σ (call_id) (gmap ptr_id (gset loc))}. - - Implicit Types (c : call_id) (pid : ptr_id) (pm : permission). - - Definition call_set_is (c : call_id) (M : gmap ptr_id (gset loc)) := - ghost_map_elem call_gname c (DfracOwn 1) M. - - (* This does not assert ownership of the authoritative part. Instead, this is owned by bor_interp below. *) - Definition call_set_interp (M : gmap call_id (gmap ptr_id (gset loc))) (σ : state) : Prop := - ∀ c (M' : gmap ptr_id (gset loc)), M !! c = Some M' → - c ∈ σ.(scs) ∧ - (* for every ptr_id *) - ∀ pid (S : gset loc), M' !! pid = Some S → - (pid < σ.(snp))%nat ∧ - (* for every protected location [l], there needs to be a protector in the stack *) - ∀ (l : loc), l ∈ S → ∃ s pm, σ.(sst) !! l = Some s ∧ - mkItem pm (Tagged pid) (Some c) ∈ s ∧ pm ≠Disabled. - - Definition loc_protected_by σ t l c := - c ∈ σ.(scs) ∧ (t < σ.(snp))%nat ∧ ∃ stk pm, σ.(sst) !! l = Some stk ∧ - mkItem pm (Tagged t) (Some c) ∈ stk ∧ pm ≠Disabled. - Lemma call_set_interp_access M σ c t l : - call_set_interp M σ → - call_set_in' M c t l → - loc_protected_by σ t l c. - Proof. - intros Hinterp (M' & HM_some & L & HM'_some & Hin). - specialize (Hinterp _ _ HM_some) as (? & Hinterp). - specialize (Hinterp _ _ HM'_some) as (? & Hinterp). - specialize (Hinterp _ Hin). done. - Qed. - - Lemma call_set_interp_remove c M σ : - call_set_interp M σ → - call_set_interp (delete c M) (state_upd_calls (.∖ {[c]}) σ). - Proof. - intros Hinterp c' M' Hsome. destruct (decide (c' = c)) as [-> | Hneq]. - { rewrite lookup_delete in Hsome. done. } - rewrite lookup_delete_ne in Hsome; last done. - apply Hinterp in Hsome as (Hin & Hpid). - split. - { destruct σ; cbn in *. apply elem_of_difference; split; first done. by apply not_elem_of_singleton. } - intros t S HS. - apply Hpid in HS as (Ht & Hlookup). split; first by destruct σ. - intros l Hl. apply Hlookup in Hl as (s & pm & Hsst & Hs & Hpm). - exists s, pm. split_and!; [ | done..]. by destruct σ. - Qed. - -End call_defs. - -Notation "c '@@' M" := (call_set_is call_name c M) (at level 50). - - -(* Interpretation for heap assertions under control of tags - The interpretation of the tag map and the "heap view" fragments are interlinked. - *) -Section heap_defs. - (** The assumption on the location still being valid for tag [t], i.e., [t] not being disabled. *) - (* Note: That the stack is still there needs to be part of the precondition [bor_state_pre]. - Otherwise, we will not be able to prove reflexivity for deallocation: - that needs to be able to remove stacks from the state without updating all the ghost state that may still make assumptions about it. - *) - - Definition bor_state_pre (l : loc) (t : ptr_id) (tk : tag_kind) (σ : state) := - match tk with - | tk_local => True - | _ => ∃ st pm pro, σ.(sst) !! l = Some st ∧ - mkItem pm (Tagged t) pro ∈ st ∧ pm ≠Disabled - end. - - Lemma loc_protected_bor_state_pre l t c σ tk : - loc_protected_by σ t l c → bor_state_pre l t tk σ. - Proof. - intros (_ & _ & (stk & pm & ?)). destruct tk; [| | done]; rewrite /bor_state_pre; eauto. - Qed. - - Definition bor_state_own (l : loc) (t : ptr_id) (tk : tag_kind) (σ : state) := - match tk with - | tk_local => σ.(sst) !! l = Some ([mkItem Unique (Tagged t) None]) - | tk_unq => ∃ st, σ.(sst) !! l = Some st ∧ ∃ opro st', - st = mkItem Unique (Tagged t) opro :: st' - | tk_pub => ∃ st, σ.(sst) !! l = Some st ∧ t ∈ active_SRO st - end. - - Lemma bor_state_own_some_stack l t tk σ : - bor_state_own l t tk σ → ∃ stk, σ.(sst) !! l = Some stk. - Proof. rewrite /bor_state_own. destruct tk; naive_solver. Qed. - - Definition loc_controlled (l : loc) (t : ptr_id) (tk : tag_kind) (sc : scalar) (σ : state) := - (bor_state_pre l t tk σ → bor_state_own l t tk σ ∧ σ.(shp) !! l = Some sc). - - Lemma loc_controlled_local l t sc σ : - loc_controlled l t tk_local sc σ → - σ.(sst) !! l = Some [mkItem Unique (Tagged t) None] ∧ - σ.(shp) !! l = Some sc. - Proof. intros Him. specialize (Him I) as (Hbor & Hmem). split;done. Qed. - - Lemma loc_controlled_unq l t sc s σ : - loc_controlled l t tk_unq sc σ → - σ.(sst) !! l = Some s → - (∃ pm opro, mkItem pm (Tagged t) opro ∈ s ∧ pm ≠Disabled) → - (∃ s' op, s = (mkItem Unique (Tagged t) op) :: s') ∧ - σ.(shp) !! l = Some sc. - Proof. - intros Him Hstk (pm & opro & Hpm). - edestruct Him as (Hown & ?). { rewrite /bor_state_pre. eauto. } - split; last done. - destruct Hown as (st' & opro' & st'' & Hst' & ->). simplify_eq. eauto. - Qed. - - Lemma loc_controlled_pub l t sc σ s : - loc_controlled l t tk_pub sc σ → - σ.(sst) !! l = Some s → - (∃ pm opro, mkItem pm (Tagged t) opro ∈ s ∧ pm ≠Disabled) → - t ∈ active_SRO s ∧ - σ.(shp) !! l = Some sc. - Proof. - intros Him Hst (pm & opro & Hin & Hpm). - edestruct Him as (Hown & ?). { rewrite /bor_state_pre; eauto 8. } - split; last done. destruct Hown as (st' & Hst' & Hsro). - simplify_eq. eauto. - Qed. - - Lemma loc_controlled_mem_insert_ne l l' t tk sc sc' σ : - l ≠l' → - loc_controlled l t tk sc σ → - loc_controlled l t tk sc (state_upd_mem <[l' := sc']> σ). - Proof. - intros Hneq Him Hpre. - apply Him in Hpre as [Hown Hmem]. split; first done. - rewrite lookup_insert_ne; done. - Qed. - Lemma loc_controlled_mem_insert l t tk sc sc' σ : - loc_controlled l t tk sc σ → - loc_controlled l t tk sc' (state_upd_mem <[l := sc']> σ). - Proof. - intros Him Hpre. apply Him in Hpre as [Hown Hmem]. split; first done. - rewrite lookup_insert; done. - Qed. - - Section local. - (** Facts about local tags *) - Lemma loc_controlled_local_unique l t t' sc sc' σ : - loc_controlled l t tk_local sc σ → - loc_controlled l t' tk_local sc' σ → - t' = t ∧ sc' = sc. - Proof. - intros Hcontrol Hcontrol'. specialize (Hcontrol I) as [Hown Hmem]. - specialize (Hcontrol' I) as [Hown' Hmem']. - split; last by simplify_eq. - move : Hown Hown'. rewrite /bor_state_own // => -> [=] //. - Qed. - - Lemma loc_controlled_local_pre l t t' tk' sc σ : - loc_controlled l t tk_local sc σ → - bor_state_pre l t' tk' σ → - tk' = tk_local ∨ t' = t. - Proof. - intros [Heq _]%loc_controlled_local. - destruct tk'; last by eauto. - - intros (st' & pm & opro & Hst & Hin & Hpm). - move : Hst Hin. rewrite Heq. - move => [= <-] /elem_of_list_singleton [=]; eauto. - - intros (st' & pm & opro & Hst & Hin & Hpm). - move : Hst Hin. rewrite Heq. - move => [= <-] /elem_of_list_singleton [=]; eauto. - Qed. - Lemma loc_controlled_local_own l t t' tk' sc σ : - loc_controlled l t tk_local sc σ → - bor_state_own l t' tk' σ → - (tk' = tk_unq ∨ tk' = tk_local) ∧ t = t'. - Proof. - intros [Heq _]%loc_controlled_local. destruct tk'. - - move => [st' []]. rewrite Heq => [= <-] //. - - move => [st' [Heq' [opro [st'' ]]]]. move : Heq'. rewrite Heq => [= <-] [= ->] //; eauto. - - rewrite /bor_state_own Heq => [=]; eauto. - Qed. - - (* having local ownership of a location is authoritative, in the sense that we can update memory without hurting other tags that control this location. *) - Lemma loc_controlled_local_authoritative l t t' tk' sc sc' σ f : - loc_controlled l t tk_local sc (state_upd_mem f σ) → - loc_controlled l t' tk' sc' σ → - t ≠t' → - loc_controlled l t' tk' sc' (state_upd_mem f σ). - Proof. - intros Hcontrol Hcontrol' Hneq [Hown Hmem]%Hcontrol'. split; first done. - by edestruct (loc_controlled_local_own l t t' tk' sc (state_upd_mem f σ)) as [_ <-]. - Qed. - End local. - - Definition dom_agree_on_tag (M_t M_s : gmap (ptr_id * loc) scalar) (t : ptr_id) := - (∀ l, is_Some (M_t !! (t, l)) → is_Some (M_s !! (t, l))) ∧ - (∀ l, is_Some (M_s !! (t, l)) → is_Some (M_t !! (t, l))). - - Lemma dom_agree_on_tag_upd_ne_target M_t M_s t t' l sc : - t ≠t' → - dom_agree_on_tag M_t M_s t' → - dom_agree_on_tag (<[(t, l) := sc]> M_t) M_s t'. - Proof. - intros Hneq [Htgt Hsrc]. split => l'' Hsome. - - apply Htgt. move : Hsome. rewrite lookup_insert_is_Some. by intros [[= -> <-] | [_ ?]]. - - apply lookup_insert_is_Some. right. split; first congruence. by apply Hsrc. - Qed. - Lemma dom_agree_on_tag_upd_ne_source M_t M_s t t' l sc : - t ≠t' → - dom_agree_on_tag M_t M_s t' → - dom_agree_on_tag M_t (<[(t, l) := sc]> M_s) t'. - Proof. - intros Hneq [Htgt Hsrc]. split => l'' Hsome. - - apply lookup_insert_is_Some. right. split; first congruence. by apply Htgt. - - apply Hsrc. move : Hsome. rewrite lookup_insert_is_Some. by intros [[= -> <-] | [_ ?]]. - Qed. - Lemma dom_agree_on_tag_upd_target M_t M_s t l sc : - is_Some (M_t !! (t, l)) → - dom_agree_on_tag M_t M_s t → - dom_agree_on_tag (<[(t, l) := sc]> M_t) M_s t. - Proof. - intros Hs [Htgt Hsrc]. split => l''. - - rewrite lookup_insert_is_Some. intros [[= <-] | [_ ?]]; by apply Htgt. - - intros Hsome. rewrite lookup_insert_is_Some'. right; by apply Hsrc. - Qed. - Lemma dom_agree_on_tag_upd_source M_t M_s t l sc : - is_Some (M_s !! (t, l)) → - dom_agree_on_tag M_t M_s t → - dom_agree_on_tag M_t (<[(t, l) := sc]> M_s) t. - Proof. - intros Hs [Htgt Hsrc]. split => l''. - - intros Hsome. rewrite lookup_insert_is_Some'. right; by apply Htgt. - - rewrite lookup_insert_is_Some. intros [[= <-] | [_ ?]]; by apply Hsrc. - Qed. - Lemma dom_agree_on_tag_lookup_target M_t M_s t l : - dom_agree_on_tag M_t M_s t → is_Some (M_t !! (t, l)) → is_Some (M_s !! (t, l)). - Proof. intros Hag Hsome. apply Hag, Hsome. Qed. - Lemma dom_agree_on_tag_lookup_source M_t M_s t l : - dom_agree_on_tag M_t M_s t → is_Some (M_s !! (t, l)) → is_Some (M_t !! (t, l)). - Proof. intros Hag Hsome. apply Hag, Hsome. Qed. - - Definition tag_interp (M : gmap ptr_id (tag_kind * unit)) (M_t M_s : gmap (ptr_id * loc) scalar) σ_t σ_s : Prop := - (∀ (t : ptr_id) tk, M !! t = Some (tk, ()) → - (* tags are valid *) - (t < σ_t.(snp))%nat ∧ (t < σ_s.(snp))%nat ∧ - (* at all locations, the values agree, and match the physical state assuming the tag currently has control over the location *) - (∀ l sc_t, M_t !! (t, l) = Some sc_t → loc_controlled l t tk sc_t σ_t) ∧ - (∀ l sc_s, M_s !! (t, l) = Some sc_s → loc_controlled l t tk sc_s σ_s) ∧ - dom_agree_on_tag M_t M_s t) ∧ - (∀ (t : ptr_id) (l : loc), is_Some (M_t !! (t, l)) → is_Some (M !! t)) ∧ - (∀ (t : ptr_id) (l : loc), is_Some (M_s !! (t, l)) → is_Some (M !! t)). -End heap_defs. - - -Notation "p '$$' tk" := (tkmap_elem tag_name p tk ()) (at level 50). - -Definition tk_to_frac (tk : tag_kind) := - match tk with - | tk_pub => DfracDiscarded - | _ => DfracOwn 1 - end. -Notation "l '↦t[' tk ']{' t } sc" := (ghost_map_elem heap_view_target_name (t, l) (tk_to_frac tk) sc) - (at level 20, format "l ↦t[ tk ]{ t } sc") : bi_scope. -Notation "l '↦s[' tk ']{' t } sc" := (ghost_map_elem heap_view_source_name (t, l) (tk_to_frac tk) sc) - (at level 20, format "l ↦s[ tk ]{ t } sc") : bi_scope. - - -Section tainted_tags. - Context {Σ} `{bor_stateG Σ}. - - Definition tag_tainted_for (t : ptr_id) (l : loc) := - ghost_map_elem tainted_tags_name (t, l) DfracDiscarded tt. - (* tag t is not in l's stack, and can never be in that stack again *) - Definition tag_tainted_interp (σ_s : state) : iProp Σ := - ∃ (M : gmap (ptr_id * loc) unit), ghost_map_auth tainted_tags_name 1 M ∗ - ∀ (t : ptr_id) (l : loc), ⌜is_Some (M !! (t, l))⌠-∗ - ⌜(t < σ_s.(snp))%nat⌠∗ - (* we have a persistent element here to remove sideconditions from the insert lemma *) - tag_tainted_for t l ∗ - ⌜∀ (stk : stack) (it : item), σ_s.(sst) !! l = Some stk → it ∈ stk → - tg it ≠Tagged t ∨ perm it = DisabledâŒ. - - (* the result of a read in the target: either the tag was invalid, and it now must be invalid for the source, too, - or the result agrees with what we expected to get. *) - Definition deferred_read (v_t v_t' : value) l t : iProp Σ := - (∃ i : nat, ⌜(i < length v_t)%nat ∧ length v_t = length v_t'⌠∗ tag_tainted_for t (l +â‚— i)) ∨ ⌜v_t' = v_tâŒ. - - Lemma tag_tainted_interp_insert σ_s t l : - (t < σ_s.(snp))%nat → - (∀ (stk : stack) (it : item), σ_s.(sst) !! l = Some stk → it ∈ stk → tg it ≠Tagged t ∨ perm it = Disabled) → - tag_tainted_interp σ_s ==∗ - tag_tainted_interp σ_s ∗ tag_tainted_for t l. - Proof. - iIntros (Ht Hnot_in) "(%M & Hauth & #Hinterp)". - destruct (M !! (t, l)) as [[] | ] eqn:Hlookup. - - iModIntro. iPoseProof ("Hinterp" $! t l with "[]") as "(_ & $ & _)"; first by eauto. - iExists M. iFrame "Hauth Hinterp". - - iMod (ghost_map_insert (t, l) () Hlookup with "Hauth") as "[Hauth He]". - iMod (ghost_map_elem_persist with "He") as "#He". iFrame "He". - iModIntro. iExists (<[(t, l) := ()]> M). iFrame "Hauth". - iIntros (t' l' [[= <- <-] | [Hneq Hsome]]%lookup_insert_is_Some). - { iFrame "He". eauto. } - iApply "Hinterp". done. - Qed. - - Lemma tag_tainted_interp_lookup σ_s t l : - tag_tainted_for t l -∗ - tag_tainted_interp σ_s -∗ - ⌜(t < σ_s.(snp))%nat⌠∗ - ⌜∀ (stk : stack) (it : item), σ_s.(sst) !! l = Some stk → it ∈ stk → tg it ≠Tagged t ∨ perm it = DisabledâŒ. - Proof. - iIntros "Helem (%M & Hauth & Hinterp)". - iPoseProof (ghost_map_lookup with "Hauth Helem") as "%Hlookup". - iPoseProof ("Hinterp" $! t l with "[]") as "(% & _ & %)"; by eauto. - Qed. - - Definition is_fresh_tag σ tg := - match tg with - | Untagged => True - | Tagged t => σ.(snp) ≤ t - end. - Lemma tag_tainted_interp_preserve σ_s σ_s' : - σ_s'.(snp) ≥ σ_s.(snp) → - (∀ l stk', σ_s'.(sst) !! l = Some stk' → ∀ it, it ∈ stk' → - is_fresh_tag σ_s it.(tg) ∨ it.(perm) = Disabled ∨ - ∃ stk, σ_s.(sst) !! l = Some stk ∧ it ∈ stk) → - tag_tainted_interp σ_s -∗ tag_tainted_interp σ_s'. - Proof. - iIntros (Hge Hupd) "(%M & Hauth & Hinterp)". - iExists M. iFrame "Hauth". iIntros (t l Hsome). - iDestruct ("Hinterp" $! t l with "[//]") as "(%Hlt & $ & %Hsst)". - iSplit; iPureIntro; first lia. - intros stk' it Hstk' Hit. - specialize (Hupd _ _ Hstk' _ Hit) as [Hfresh | [Hdisabled | (stk & Hstk & Hit')]]. - - left. destruct (tg it) as [t' | ]; last done. intros [= ->]. - simpl in Hfresh. lia. - - right; done. - - eapply Hsst; done. - Qed. - - Lemma tag_tainted_interp_tagged_sublist σ_s σ_s' : - σ_s'.(snp) ≥ σ_s.(snp) → - (∀ l stk', σ_s'.(sst) !! l = Some stk' → - ∃ stk, σ_s.(sst) !! l = Some stk ∧ - tagged_sublist stk' stk) → - tag_tainted_interp σ_s -∗ tag_tainted_interp σ_s'. - Proof. - iIntros (Hge Hupd). iApply tag_tainted_interp_preserve; first done. - intros l stk' Hstk' it Hit. - destruct (Hupd _ _ Hstk') as (stk & Hstk & Hsubl). - destruct (Hsubl _ Hit) as (it' & Hit' & Htg & Hprot & Hperm). - destruct (decide (perm it = Disabled)) as [ | Hperm'%Hperm]; first by eauto. - right; right. exists stk. split; first done. - destruct it, it'; simpl in *; simplify_eq. done. - Qed. - - Lemma tag_tainted_interp_retag σ_s c l old rk pk T new α' nxtp' : - retag σ_s.(sst) σ_s.(snp) σ_s.(scs) c l old rk pk T = Some (new, α', nxtp') → - tag_tainted_interp σ_s -∗ tag_tainted_interp (mkState σ_s.(shp) α' σ_s.(scs) nxtp' σ_s.(snc)). - Proof. - iIntros (Hretag). - iApply (tag_tainted_interp_preserve); simpl. - { specialize (retag_change_nxtp _ _ _ _ _ _ _ _ _ _ _ _ Hretag). lia. } - intros l' stk' Hstk' it Hit. - specialize (retag_item_in _ _ _ _ _ _ _ _ _ _ _ _ Hretag l' stk') as Ht. - destruct (decide (perm it = Disabled)) as [Hdisabled | Hndisabled]; first by eauto. - destruct (tg it) as [t | ] eqn:Htg; last by (left; done). - destruct (decide (t < σ_s.(snp))%nat) as [Hlt | Hnlt]. - - right; right. eapply (Ht t it); done. - - left. simpl. lia. - Qed. - - Lemma tag_tainted_interp_alloc σ l n : - let nt := Tagged σ.(snp) in - tag_tainted_interp σ -∗ tag_tainted_interp (mkState (init_mem l n σ.(shp)) (init_stacks σ.(sst) l n nt) σ.(scs) (S σ.(snp)) σ.(snc)). - Proof. - intros nt. iIntros "Htainted". - iApply (tag_tainted_interp_preserve σ with "Htainted"). { simpl. lia. } - intros l' stk' Hstk' it Hit. - specialize (init_stacks_lookup_case _ _ _ _ _ _ Hstk') as [(Hstk'' & Hi) | (i & Hi & ->)]. - + right. right. eauto. - + left. simpl. move : Hstk'. rewrite (proj1 (init_stacks_lookup _ _ _ _)); last done. - intros [= <-]. move : Hit. rewrite elem_of_list_singleton => -> /=. lia. - Qed. -End tainted_tags. - - -Section state_interp. - Context `{bor_stateG Σ} (sc_rel : scalar → scalar → iProp Σ). - - (* We generally do not enforce that stacks for all locations are equal: that would make non-determinism in choosing locations slightly clunky. - Rather, we should again force equality in bijections. - *) - Definition bor_auth (M_call : gmap call_id (gmap ptr_id (gset loc))) (M_tag : gmap ptr_id (tag_kind * unit)) (M_t M_s : gmap (ptr_id * loc) scalar) : iProp Σ := - ghost_map_auth call_name 1 M_call ∗ - tkmap_auth tag_name 1 M_tag ∗ - ghost_map_auth heap_view_target_name 1 M_t ∗ - ghost_map_auth heap_view_source_name 1 M_s. - Definition bor_interp (σ_t : state) (σ_s : state) : iProp Σ := - (* since multiple parts of the interpretation need access to these maps, we own the authoritative parts here and not in the interpretations below *) - ∃ (M_call : gmap call_id (gmap ptr_id (gset loc))) - (M_tag : gmap ptr_id (tag_kind * unit)) - (M_t M_s : gmap (ptr_id * loc) scalar), - bor_auth M_call M_tag M_t M_s ∗ - - tag_tainted_interp σ_s ∗ - - state_rel sc_rel M_tag M_t M_call σ_t σ_s ∗ - (* due to the [state_rel], enforcing this on [σ_t] also does the same for [σ_s] *) - ⌜call_set_interp M_call σ_t⌠∗ - ⌜tag_interp M_tag M_t M_s σ_t σ_s⌠∗ - - ⌜state_wf σ_s⌠∗ - ⌜state_wf σ_tâŒ. - - Lemma bor_interp_get_pure σ_t σ_s : - bor_interp σ_t σ_s -∗ ⌜σ_s.(sst) = σ_t.(sst) ∧ σ_s.(snp) = σ_t.(snp) ∧ σ_s.(snc) = σ_t.(snc) ∧ σ_s.(scs) = σ_t.(scs) ∧ state_wf σ_s ∧ state_wf σ_t ∧ dom (gset loc) σ_s.(shp) = dom (gset loc) σ_t.(shp)âŒ. - Proof. - iIntros "(% & % & % & % & ? & _ & Hstate & _ & _ & % & %)". - iPoseProof (state_rel_get_pure with "Hstate") as "%". - iPoseProof (state_rel_dom_eq with "Hstate") as "<-". - iPureIntro. tauto. - Qed. - - Lemma bor_interp_get_state_wf σ_t σ_s : - bor_interp σ_t σ_s -∗ - ⌜state_wf σ_t⌠∗ ⌜state_wf σ_sâŒ. - Proof. iIntros "(% & % & % & % & ? & ? & Hstate & _ & _ & % & %)". eauto. Qed. - -End state_interp. - - -(** Array generalizes pointsto connectives to lists of scalars *) -Definition array_tag `{!bor_stateG Σ} γh (t : ptr_id) (l : loc) (dq : dfrac) (scs : list scalar) : iProp Σ := - ([∗ list] i ↦ sc ∈ scs, ghost_map_elem γh (t, l +â‚— i) dq sc)%I. -Notation "l '↦t∗[' tk ']{' t } scs" := (array_tag heap_view_target_name t l (tk_to_frac tk) scs) - (at level 20, format "l ↦t∗[ tk ]{ t } scs") : bi_scope. -Notation "l '↦s∗[' tk ']{' t } scs" := (array_tag heap_view_source_name t l (tk_to_frac tk) scs) - (at level 20, format "l ↦s∗[ tk ]{ t } scs") : bi_scope. - - -Fixpoint array_tag_map (l : loc) (t : ptr_id) (v : list scalar) : gmap (ptr_id * loc) scalar := - match v with - | [] => ∅ - | sc :: v' => <[(t, l) := sc]> (array_tag_map (l +â‚— 1) t v') - end. -Lemma array_tag_map_lookup1 l t v t' l' : - is_Some (array_tag_map l t v !! (t', l')) → - t' = t ∧ l.1 = l'.1 ∧ l.2 ≤ l'.2 < l.2 + length v. -Proof. - induction v as [ | sc v IH] in l |-*. - - simpl. rewrite lookup_empty. intros [? [=]]. - - simpl. move => [sc0 ]. rewrite lookup_insert_Some. move => [[[= <- <-] Heq] | [Hneq Ht]]; first lia. - move : (IH (l +â‚— 1) ltac:(eauto)). destruct l. simpl. lia. -Qed. -Lemma array_tag_map_lookup2 l t v t' l' : - is_Some (array_tag_map l t v !! (t', l')) → - t' = t ∧ ∃ i, (i < length v)%nat ∧ l' = l +â‚— i. -Proof. - intros (-> & H1 & H2)%array_tag_map_lookup1. - split; first done. exists (Z.to_nat (l'.2 - l.2)). - destruct l, l'; rewrite /shift_loc; simpl in *. split. - - lia. - - apply pair_equal_spec. split; lia. -Qed. - -Lemma array_tag_map_lookup_Some l t v (i : nat) : - (i < length v)%nat → - array_tag_map l t v !! (t, l +â‚— i) = v !! i. -Proof. - induction v as [ | sc v IH] in l, i |-*. - - simpl. lia. - - simpl. intros Hi. destruct i as [ | i]. - + rewrite shift_loc_0_nat. rewrite lookup_insert. done. - + rewrite lookup_insert_ne; first last. { destruct l; simpl; intros [= ?]; lia. } - move : (IH (l +â‚— 1) i ltac:(lia)). rewrite shift_loc_assoc. - by replace (Z.of_nat (S i)) with (1 + i) by lia. -Qed. - -Lemma array_tag_map_lookup_None t t' l v : - t ≠t' → ∀ l', array_tag_map l t v !! (t', l') = None. -Proof. - intros Hneq l'. destruct (array_tag_map l t v !! (t', l')) eqn:Harr; last done. - specialize (array_tag_map_lookup1 l t v t' l' ltac:(eauto)) as [Heq _]; congruence. -Qed. - -Lemma array_tag_map_lookup_None' l t v l' : - (∀ i:nat, (i < length v)%nat → l +â‚— i ≠l') → - array_tag_map l t v !! (t, l') = None. -Proof. - intros Hneq. destruct (array_tag_map _ _ _ !! _) eqn:Heq; last done. exfalso. - specialize (array_tag_map_lookup2 l t v t l' ltac:(eauto)) as [_ (i & Hi & ->)]. - eapply Hneq; last reflexivity. done. -Qed. - -Lemma array_tag_map_lookup_None2 l t t' v l' : - array_tag_map l t v !! (t', l') = None → - t ≠t' ∨ (∀ i: nat, (i < length v)%nat → l +â‚— i ≠l'). -Proof. -Admitted. - -Lemma ghost_map_array_tag_lookup `{!bor_stateG Σ} (γh : gname) (q : Qp) (M : gmap (ptr_id * loc) scalar) (scs : list scalar) (t : ptr_id) (l : loc) dq : - ghost_map_auth γh q M -∗ - ([∗ list] i ↦ sc ∈ scs, ghost_map_elem γh (t, l +â‚— i) dq sc) -∗ - ⌜∀ i : nat, (i < length scs)%nat → M !! (t, l +â‚— i) = scs !! iâŒ. -Proof. - iIntros "Hauth Helem". iInduction scs as [ |sc scs ] "IH" forall (l) "Hauth Helem". - - iPureIntro; cbn. lia. - - rewrite big_sepL_cons. iDestruct "Helem" as "[Hsc Hscs]". - iPoseProof (ghost_map_lookup with "Hauth Hsc") as "%Hl". - iDestruct ("IH" $! (l +â‚— 1) with "Hauth [Hscs]") as "%IH". - { iApply (big_sepL_mono with "Hscs"). intros i sc' Hs. cbn. rewrite shift_loc_assoc. - replace (Z.of_nat $ S i) with (1 + i)%Z by lia. done. } - iPureIntro. intros i Hle. destruct i; first done. - replace (Z.of_nat $ S i) with (1 + i)%Z by lia. cbn in *. rewrite -(IH i); last lia. - by rewrite shift_loc_assoc. -Qed. - -Lemma ghost_map_array_tag_update `{!bor_stateG Σ} (γh : gname) (M : gmap (ptr_id * loc) scalar) (v v' : list scalar) (t : ptr_id) (l : loc) : - ghost_map_auth γh 1 M -∗ - ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +â‚— i) (DfracOwn 1) sc) ==∗ - ([∗ list] i ↦ sc' ∈ v', ghost_map_elem γh (t, l +â‚— i) (DfracOwn 1) sc') ∗ - ghost_map_auth γh 1 (array_tag_map l t v' ∪ M). -Proof. - -Admitted. - -Lemma ghost_map_array_tag_insert `{!bor_stateG Σ} (γh : gname) (M : gmap (ptr_id * loc) scalar) (v : list scalar) (t : ptr_id) (l : loc) : - (∀ i : nat, (i < length v)%nat → M !! (t, l +â‚— i) = None) → - ghost_map_auth γh 1 M ==∗ - ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +â‚— i) (DfracOwn 1) sc) ∗ - ghost_map_auth γh 1 (array_tag_map l t v ∪ M). -Proof. -Admitted. - -Lemma ghost_map_array_tag_delete `{!bor_stateG Σ} (γh : gname) (M : gmap (ptr_id * loc) scalar) (v : list scalar) (t : ptr_id) (l : loc) : - ghost_map_auth γh 1 M -∗ - ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +â‚— i) (DfracOwn 1) sc) ==∗ - ghost_map_auth γh 1 (M ∖ array_tag_map l t v). -Proof. - iIntros "Hauth Helems". - iApply (ghost_map_delete_big (array_tag_map l t v) with "Hauth [Helems]"). - iInduction v as [ | sc v] "IH" forall (l); first done. - simpl. iApply big_sepM_insert. - { destruct (_ !! _) eqn:Heq; last done. - specialize (array_tag_map_lookup2 (l +â‚— 1) t v t l ltac:(eauto)) as [_ (i & _ & Hl)]. - destruct l. injection Hl. lia. - } - rewrite shift_loc_0_nat. iDestruct "Helems" as "[$ Helems]". - iApply "IH". iApply (big_sepL_mono with "Helems"). - iIntros (i sc' Hi). simpl. - rewrite shift_loc_assoc. replace (Z.of_nat (S i)) with (1 + i) by lia; done. -Qed. - - -Lemma ghost_map_array_tag_tk `{!bor_stateG Σ} (γh : gname) (v : list scalar) (t : ptr_id) (l : loc) tk : - ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +â‚— i) (DfracOwn 1) sc) ==∗ - ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +â‚— i) (tk_to_frac tk) sc). -Proof. - destruct tk; cbn; [ | by eauto | by eauto]. - iInduction v as [| sc v] "IH" forall (l); first by eauto. - rewrite !big_sepL_cons. iIntros "[Hh Hr]". - iMod (ghost_map_elem_persist with "Hh") as "$". - iMod ("IH" $! (l +â‚— 1) with "[Hr]") as "Hr". - - iApply (big_sepL_mono with "Hr"). intros i sc' Hs. simpl. rewrite shift_loc_assoc. - by replace (Z.of_nat (S i)) with (1 + i) by lia. - - iModIntro. - iApply (big_sepL_mono with "Hr"). intros i sc' Hs. simpl. rewrite shift_loc_assoc. - by replace (Z.of_nat (S i)) with (1 + i) by lia. -Qed. - - -Lemma lookup_union_Some_l' `{EqDecision K} `{Countable K} V (M1 M2 : gmap K V) (k : K) (v : V) : - (M1 ∪ M2) !! k = Some v → M2 !! k = None → M1 !! k = Some v. -Proof. - destruct (M1 !! k) as [ v' | ] eqn:Hv'. - - specialize (lookup_union_Some_l M1 M2 _ _ Hv') as ->. move => [= ->]. done. - - rewrite lookup_union_r; last done. congruence. -Qed. -Lemma lookup_union_is_Some `{EqDecision K} `{Countable K} V (M1 M2 : gmap K V) (k : K) : - is_Some ((M1 ∪ M2) !! k) ↔ is_Some (M1 !! k) ∨ is_Some (M2 !! k). -Proof. - split. - - intros (v & Hv). destruct (M1 !! k) eqn:HM1; first by eauto. - right. erewrite <-lookup_union_r; eauto. - - intros [(v & HM1) | (v & HM2)]. - + rewrite (lookup_union_Some_l _ _ _ _ HM1); eauto. - + destruct (M1 !! k) eqn:HM1. { rewrite (lookup_union_Some_l _ _ _ _ HM1); eauto. } - rewrite lookup_union_r; eauto. -Qed. - -Lemma dom_agree_on_tag_union M1_t M1_s M2_t M2_s t : - dom_agree_on_tag M1_t M1_s t → dom_agree_on_tag M2_t M2_s t → - dom_agree_on_tag (M1_t ∪ M2_t) (M1_s ∪ M2_s) t. -Proof. - intros [H1a H1b] [H2a H2b]. split; intros l; rewrite !lookup_union_is_Some; naive_solver. -Qed. - -Lemma dom_agree_on_tag_array_tag_map l t v_t v_s : - length v_t = length v_s → - dom_agree_on_tag (array_tag_map l t v_t) (array_tag_map l t v_s) t. -Proof. - intros Hlen. split; intros l'. - - intros (_ & (i & Hi & ->))%array_tag_map_lookup2. rewrite array_tag_map_lookup_Some; last lia. - apply lookup_lt_is_Some_2. lia. - - intros (_ & (i & Hi & ->))%array_tag_map_lookup2. rewrite array_tag_map_lookup_Some; last lia. - apply lookup_lt_is_Some_2. lia. -Qed. - - -Lemma dom_agree_on_tag_not_elem M_t M_s t : - (∀ l, M_t !! (t, l) = None) → (∀ l, M_s !! (t, l) = None) → - dom_agree_on_tag M_t M_s t. -Proof. intros Ht Hs. split; intros l; rewrite Ht Hs; congruence. Qed. - -(* TODO: move somewhere? *) -Lemma lookup_difference_is_Some `{Countable K} (V : Type) (M1 M2 : gmap K V) (k : K) : - is_Some ((M1 ∖ M2) !! k) ↔ is_Some (M1 !! k) ∧ M2 !! k = None. -Proof. rewrite /is_Some. setoid_rewrite lookup_difference_Some. naive_solver. Qed. - -Lemma dom_agree_on_tag_difference M1_t M1_s M2_t M2_s t : - dom_agree_on_tag M1_t M1_s t → dom_agree_on_tag M2_t M2_s t → - dom_agree_on_tag (M1_t ∖ M2_t) (M1_s ∖ M2_s) t. -Proof. - intros [H1a H1b] [H2a H2b]. split; intros l. - all: rewrite !lookup_difference_is_Some !eq_None_not_Some; naive_solver. -Qed. - - -Section val_rel. - Context {Σ} `{bor_stateG Σ}. - Definition sc_rel (sc1 sc2 : scalar) : iProp Σ := - match sc1, sc2 with - | ScInt z1, ScInt z2 => ⌜z1 = z2⌠- | ScFnPtr f1, ScFnPtr f2 => ⌜f1 = f2⌠- | ScPtr l1 p1, ScPtr l2 p2 => - (* through srel: the stacks are the same, the allocation size is the same, and the locations are related (i.e.: if tagged, then it is public) *) - ⌜l1 = l2⌠∗ - (⌜p1 = Untagged⌠∗ ⌜p2 = Untagged⌠∨ - (∃ t1 t2, ⌜p1 = Tagged t1⌠∗ ⌜p2 = Tagged t2⌠∗ - (* may want to generalize that properly when we have a proper bijection on tags*) - ⌜t1 = t2⌠∗ - t1 $$ tk_pub)) - (* note: we do not have any assertion about the value as viewed by the tag here -- we don't really care about it, we need to do a retag anyways. what the tk_pub gives us is that the locations store related values *) - | ScCallId c, ScCallId c' => ⌜c = c'⌠- | ScPtr l t, ScPoison => True - | ScInt z, ScPoison => True - | ScPoison, ScPoison => True - | ScFnPtr fn, ScPoison => True - | ScCallId c, ScPoison => True - | _, _ => False - end. - - Definition value_rel (v1 v2 : value) : iProp Σ := [∗ list] sc_t; sc_s ∈ v1; v2, sc_rel sc_t sc_s. - - Definition rrel (r1 r2 : result) : iProp Σ := - match r1, r2 with - | ValR v1, ValR v2 => value_rel v1 v2 - | PlaceR l1 bor1 T1, PlaceR l2 bor2 T2 => - (* places must be related in a similar way as pointers: either untagged or public. Types should be equal. *) - sc_rel (ScPtr l1 bor1) (ScPtr l2 bor2) ∧ ⌜T1 = T2⌠- | _, _ => False - end. - - Global Instance sc_rel_persistent sc_t sc_s : Persistent (sc_rel sc_t sc_s). - Proof. destruct sc_t, sc_s; apply _. Qed. - Global Instance value_rel_persistent v_t v_s : Persistent (value_rel v_t v_s). - Proof. apply _. Qed. - Global Instance rrel_persistent r_t r_s : Persistent (rrel r_t r_s). - Proof. destruct r_t, r_s; apply _. Qed. - - (* Inversion lemmas *) - Lemma sc_rel_ptr_source sc_t l_s t_s : - sc_rel sc_t (ScPtr l_s t_s) -∗ ⌜sc_t = ScPtr l_s t_s⌠∗ (if t_s is Tagged t then t $$ tk_pub else True). - Proof. - iIntros "Hrel". destruct sc_t; [done | done | | done | done ]. - iDestruct "Hrel" as "(-> & [[-> ->] | (% & %t & -> & -> & -> & ?)])"; iFrame; done. - Qed. - Lemma sc_rel_fnptr_source sc_t fn : - sc_rel sc_t (ScFnPtr fn) -∗ ⌜sc_t = ScFnPtr fnâŒ. - Proof. - iIntros "Hrel". destruct sc_t; [done | done | done | | done]. - by iDestruct "Hrel" as "->". - Qed. - Lemma sc_rel_int_source sc_t z : - sc_rel sc_t (ScInt z) -∗ ⌜sc_t = ScInt zâŒ. - Proof. - iIntros "Hrel". destruct sc_t; [ done | | done..]. - by iDestruct "Hrel" as "->". - Qed. - Lemma sc_rel_cid_source sc_t c : - sc_rel sc_t (ScCallId c) -∗ ⌜sc_t = ScCallId câŒ. - Proof. iIntros "Hrel"; destruct sc_t; [done.. | ]. by iDestruct "Hrel" as "->". Qed. - - Lemma sc_rel_poison_target sc_s : - sc_rel (ScPoison) sc_s -∗ ⌜sc_s = ScPoisonâŒ. - Proof. iIntros "Hrel". destruct sc_s; done. Qed. - - Lemma rrel_place_source r_t l_s t_s T : - rrel r_t (PlaceR l_s t_s T) -∗ - ∃ l_t, ⌜r_t = PlaceR l_t t_s T⌠∗ (if t_s is Tagged t then t $$ tk_pub else True). - Proof. - iIntros "Hrel". - destruct r_t as [ | l_t t' T']; first done. iDestruct "Hrel" as "(#H & ->)". - iDestruct (sc_rel_ptr_source with "H") as "[%Heq Htag]". - injection Heq as [= -> ->]. iExists l_s. eauto. - Qed. - Lemma rrel_value_source r_t v_s : - rrel r_t (ValR v_s) -∗ - ∃ v_t, ⌜r_t = ValR v_t⌠∗ value_rel v_t v_s. - Proof. - iIntros "Hrel". destruct r_t as [ v_t | ]; last done. - iExists v_t. iFrame "Hrel". done. - Qed. - - Lemma value_rel_length v_t v_s : - value_rel v_t v_s -∗ ⌜length v_t = length v_sâŒ. - Proof. iApply big_sepL2_length. Qed. - Lemma value_rel_empty : - ⊢ value_rel [] []. - Proof. by iApply big_sepL2_nil. Qed. - - Lemma value_rel_singleton_source v_t sc_s : - value_rel v_t [sc_s] -∗ ∃ sc_t, ⌜v_t = [sc_t]⌠∗ sc_rel sc_t sc_s. - Proof. - iIntros "Hv". iPoseProof (value_rel_length with "Hv") as "%Hlen". - destruct v_t as [ | sc_t []]; [done | | done ]. - iExists sc_t. iSplitR "Hv"; first done. iRevert "Hv". rewrite /value_rel big_sepL2_singleton. eauto. - Qed. - - - Lemma value_rel_lookup v_t v_s (i : nat) : - i < length v_t → - value_rel v_t v_s -∗ - ∃ sc_t sc_s, ⌜v_t !! i = Some sc_t⌠∗ ⌜v_s !! i = Some sc_s⌠∗ sc_rel sc_t sc_s. - Proof. - iIntros (Hi) "Hvrel". rewrite /value_rel big_sepL2_forall. - iDestruct "Hvrel" as "[%Hlen Hvrel]". - iSpecialize ("Hvrel" $! i (v_t !!! i) (v_s !!! i)). iExists (v_t !!! i), (v_s !!! i). - assert (v_t !! i = Some (v_t !!! i)) as Heq. - { apply list_lookup_lookup_total. apply lookup_lt_is_Some_2. lia. } - assert (v_s !! i = Some (v_s !!! i)) as Heq'. - { apply list_lookup_lookup_total. apply lookup_lt_is_Some_2. lia. } - iSplit; first done. iSplit; first done. iApply "Hvrel"; done. - Qed. - - Lemma value_rel_lookup_total (v_t v_s : list scalar) (i : nat) : - i < length v_t → value_rel v_t v_s -∗ sc_rel (v_t !!! i) (v_s !!! i). - Proof. - iIntros (Hi) "Hvrel". rewrite /value_rel big_sepL2_forall. - iDestruct "Hvrel" as "[%Hlen Hvrel]". - iApply ("Hvrel" $! i (v_t !!! i) (v_s !!! i)). - all: iPureIntro; apply list_lookup_lookup_total; apply lookup_lt_is_Some_2; lia. - Qed. - - Lemma tag_values_included_iff v t : - tag_values_included v t ↔ (∀ i, (i < length v)%nat → wf_scalar t (v !!! i)). - Proof. - rewrite /tag_values_included /wf_scalar. split. - - intros Hin i Hi t' l Hvi. eapply (Hin l). rewrite -Hvi. by apply elem_of_list_lookup_total_2. - - intros Hs l tg (i & Hi & Hl)%elem_of_list_lookup_total_1. by eapply Hs. - Qed. - - Lemma tag_values_included_cons sc v t : - tag_values_included (sc :: v) t ↔ wf_scalar t sc ∧ tag_values_included v t. - Proof. - rewrite !tag_values_included_iff. split. - - intros Ha. split. - + apply (Ha O). cbn. lia. - + intros i Hi. apply (Ha (S i)). cbn. lia. - - intros [Hwf Ha]. intros [ | i] Hi; first done. apply Ha. cbn in Hi. lia. - Qed. - -End val_rel. - -Class sborG (Σ: gFunctors) := SBorG { - sborG_gen_progG :> gen_sim_progGS string ectx ectx Σ; - sborG_stateG :> bor_stateG Σ; -}. - -Global Program Instance sborG_simulirisG `{!sborG Σ} : simulirisG (iPropI Σ) bor_lang := { - state_interp P_t σ_t P_s σ_s T_s := - (gen_prog_interp (hG := gen_prog_inG_target) P_t ∗ - gen_prog_interp (hG := gen_prog_inG_source) P_s ∗ - bor_interp sc_rel σ_t σ_s - )%I; -}. -Next Obligation. -Admitted. - - - - - -(** Lemmas / Accessors *) -Add Printing Constructor state item. -Section lemmas. - Context `{bor_stateG Σ}. - Local Notation bor_interp := (bor_interp sc_rel). - - Implicit Types - (l : loc) (sc : scalar). - - Lemma init_mem_dom_L l n h : - dom (gset loc) (init_mem l n h) = dom (gset loc) h ∪ dom (gset loc) (init_mem l n ∅). - Proof. apply set_eq. intros l'. rewrite init_mem_dom. done. Qed. - - Lemma fresh_block_not_elem_dom h i : - (fresh_block h, i) ∉ dom (gset loc) h. - Proof. - rewrite /fresh_block. - rewrite -elem_of_elements. - Admitted. - - Lemma fresh_block_det σ_s σ_t : - dom (gset loc) σ_s.(shp) = dom (gset loc) σ_t.(shp) → - fresh_block σ_s.(shp) = fresh_block σ_t.(shp). - Proof. rewrite /fresh_block. intros ->. done. Qed. - - Lemma free_mem_dom σ_t σ_s l n : - dom (gset loc) σ_t.(shp) = dom (gset loc) σ_s.(shp) → - dom (gset loc) (free_mem l n σ_t.(shp)) = dom (gset loc) (free_mem l n σ_s.(shp)). - Proof. - intros Hdom. induction n as [ | n IH] in l |-*; first done. - simpl. rewrite !dom_delete_L IH. done. - Qed. - - - - Lemma init_stack_preserve σ n : - let l := (fresh_block σ.(shp), 0) in - let nt := σ.(snp) in - let α' := init_stacks σ.(sst) l n (Tagged nt) in - state_wf σ → - ∀ l' stk, σ.(sst) !! l' = Some stk → α' !! l' = Some stk. - Proof. - intros l nt α' Hwf l' stk Hl'. - rewrite (proj2 (init_stacks_lookup _ _ _ _) l'); first done. - intros i Hi ->. - specialize (elem_of_dom σ.(sst) ((fresh_block (shp σ), 0) +â‚— i)). - rewrite Hl'. intros (_ &Ha). specialize (Ha ltac:(eauto)). - move : Ha. rewrite -state_wf_dom; last done. - apply fresh_block_not_elem_dom. - Qed. - - Lemma init_mem_preserve σ n : - let l := (fresh_block σ.(shp), 0) in - let nt := σ.(snp) in - let h' := init_mem l n σ.(shp) in - ∀ l' sc, σ.(shp) !! l' = Some sc → h' !! l' = Some sc. - Proof. - intros l nt h' l' sc Hsc. - rewrite (proj2 (init_mem_lookup _ _ _) l'); first done. - intros i Hi ->. - specialize (elem_of_dom σ.(shp) ((fresh_block (shp σ), 0) +â‚— i)). - rewrite Hsc. intros (_ &Ha). specialize (Ha ltac:(eauto)). - move : Ha. apply fresh_block_not_elem_dom. - Qed. - - Lemma loc_controlled_alloc_update σ l' n (t : ptr_id) (tk : tag_kind) sc : - let l := (fresh_block σ.(shp), 0) in - let nt := σ.(snp) in - let α' := init_stacks σ.(sst) l n (Tagged nt) in - state_wf σ → - nt ≠t → - loc_controlled l' t tk sc σ → - loc_controlled l' t tk sc (mkState (init_mem l n σ.(shp)) α' σ.(scs) (S σ.(snp)) σ.(snc)). - Proof. - intros l nt α' Hwf Hne Hcontrolled Hpre. - assert (∀ l' stk, α' !! l' = Some stk → stk = init_stack (Tagged nt) ∨ σ.(sst) !! l' = Some stk) as Hα'. - { intros l'' stk Hl'. - specialize (init_stacks_lookup_case _ _ _ _ _ _ Hl') as [(Hstk & _) | (i & Hi & ->)]; first by eauto. - left. rewrite (proj1 (init_stacks_lookup _ _ _ _) i Hi) in Hl'. - injection Hl' as [= <-]. done. - } - assert (bor_state_pre l' t tk σ) as [Hown Hmem]%Hcontrolled. - { destruct tk; last done. - all: destruct Hpre as (stk & pm & opro & [-> | Hstk]%Hα' & Hit & ?); simpl in *; last by eauto 8. - all: exfalso; move : Hit; rewrite elem_of_list_singleton; injection 1; congruence. - } - simpl. split. - - destruct tk. - + destruct Hown as (stk & Hstk & ?). exists stk. split; last done. apply init_stack_preserve; done. - + destruct Hown as (stk & Hstk & ?). exists stk. split; last done. apply init_stack_preserve; done. - + apply init_stack_preserve; done. - - apply init_mem_preserve. done. - Qed. - - Lemma sim_alloc_state_rel_update σ_t σ_s M_tag M_t M_t' M_call l n tk : - let nt := σ_t.(snp) in - (∀ t, is_Some (M_tag !! t) → t ≠nt) → - state_rel sc_rel M_tag M_t M_call σ_t σ_s -∗ - state_rel sc_rel (<[nt := (tk, ())]> M_tag) (M_t' ∪ M_t) M_call - (mkState (init_mem l n (shp σ_t)) (init_stacks (sst σ_t) l n (Tagged nt)) (scs σ_t) (S σ_t.(snp)) (snc σ_t)) - (mkState (init_mem l n (shp σ_s)) (init_stacks (sst σ_s) l n (Tagged nt)) (scs σ_s) (S (snp σ_s)) (snc σ_s)). - Proof. - intros nt Hneq. iIntros "(%Hdom_eq & %Hsst_eq & %Hsnp_eq & %Hsnc_eq & %Hscs_eq & Hstate)". - iSplitR. { simpl. rewrite !(init_mem_dom_L _ _ (shp _)) Hdom_eq. iPureIntro. set_solver. } - simpl. rewrite Hsst_eq. iSplitR; first done. - iSplitR; first by rewrite Hsnp_eq. do 2 (iSplitR; first done). - iIntros (l' (s & [(Heq & Hi) | (i & Hi & ->)]%init_mem_lookup_case)). - + (* old location *) - iDestruct ("Hstate" $! l' with "[]") as "[Hpub | (%t & %Hpriv)]". - { eauto. } - * iLeft. simpl. iIntros (sc_t Hsc_t). simpl in Hsc_t. - rewrite (proj2 (init_mem_lookup _ n _) l' Hi) in Hsc_t. simplify_eq. - iDestruct ("Hpub" $! s with "[//]") as (sc_s Hsc_s) "Hscrel". - iExists sc_s. iSplit; last done. iPureIntro. - by rewrite (proj2 (init_mem_lookup _ n _) l' Hi). - * iRight. iPureIntro. exists t. - destruct Hpriv as (tk' & Htk & Hs & ?). exists tk'. split_and!; [ | | done]. - { rewrite lookup_insert_ne; first done. specialize (Hneq t ltac:(eauto)). done. } - rewrite lookup_union_is_Some. eauto. - + (* new location *) - iLeft. rewrite /pub_loc /=. rewrite !(proj1 (init_mem_lookup _ _ _)); [ | done | done]. - iIntros (? [= <-]). iExists ☠%S. iSplit; done. - Qed. - - Lemma sim_alloc_call_set_interp_update σ n M_call : - state_wf σ → - let nt := σ.(snp) in - let l := (fresh_block σ.(shp), 0) in - call_set_interp M_call σ → - call_set_interp M_call (mkState (init_mem l n (shp σ)) (init_stacks (sst σ) l n (Tagged nt)) (scs σ) (S σ.(snp)) (snc σ)). - Proof. - intros Hwf nt l Hcall_interp c M' [? HM']%Hcall_interp. simpl. split; first done. - intros t L HL. specialize (HM' _ _ HL) as (?& HL'). split; first lia. intros l' Hl'. - specialize (HL' l' Hl') as (stk & pm & Hstk & Hit & ?). - exists stk, pm. split_and!; [ | done..]. - apply init_stack_preserve; done. - Qed. - - Lemma local_alloc_loc_controlled σ l nt n l' sc : - array_tag_map l nt (replicate n ScPoison) !! (nt, l') = Some sc → - loc_controlled l' nt tk_local sc (mkState (init_mem l n σ.(shp)) (init_stacks σ.(sst) l n (Tagged nt)) σ.(scs) (S σ.(snp)) σ.(snc)). - Proof. - intros Hsc. - specialize (array_tag_map_lookup2 l nt _ nt l' ltac:(eauto)) as [_ (i & Hi & ->)]. - intros _. - rewrite array_tag_map_lookup_Some in Hsc; last done. - apply lookup_replicate in Hsc as [-> Hi']. split. - * simpl. rewrite (proj1 (init_stacks_lookup _ _ _ _)); done. - * simpl. rewrite (proj1 (init_mem_lookup _ _ _ )); done. - Qed. - - Lemma heap_local_alloc σ_t σ_s T : - let l_t := (fresh_block σ_t.(shp), 0) in - let l_s := (fresh_block σ_s.(shp), 0) in - let nt := σ_t.(snp) in - state_wf (mkState (init_mem l_t (tsize T) σ_t.(shp)) (init_stacks σ_t.(sst) l_t (tsize T) (Tagged nt)) σ_t.(scs) (S σ_t.(snp)) σ_t.(snc)) → - state_wf (mkState (init_mem l_s (tsize T) σ_s.(shp)) (init_stacks σ_s.(sst) l_s (tsize T) (Tagged nt)) σ_s.(scs) (S σ_s.(snp)) σ_s.(snc)) → - bor_interp σ_t σ_s ==∗ - bor_interp - (mkState (init_mem l_t (tsize T) σ_t.(shp)) (init_stacks σ_t.(sst) l_t (tsize T) (Tagged nt)) σ_t.(scs) (S σ_t.(snp)) σ_t.(snc)) - (mkState (init_mem l_s (tsize T) σ_s.(shp)) (init_stacks σ_s.(sst) l_s (tsize T) (Tagged nt)) σ_s.(scs) (S σ_s.(snp)) σ_s.(snc)) ∗ - nt $$ tk_local ∗ - l_t ↦t∗[tk_local]{nt} replicate (tsize T) ScPoison ∗ - l_s ↦s∗[tk_local]{nt} replicate (tsize T) ScPoison. - Proof. - intros l_t l_s nt Hwf_t' Hwf_s'. - iIntros "(% & % & % & % & (Hcall_auth & Htag_auth & Ht_auth & Hs_auth) & Htainted & #Hstate & %Hcall_interp & %Htag_interp & %Hwf_s & %Hwf_t)". - destruct Htag_interp as (Htag_interp & Ht_dom& Hs_dom). - assert (M_tag !! nt = None) as M_tag_none. - { destruct (M_tag !! nt) as [[? []] | ]eqn:Hs; last done. - apply Htag_interp in Hs as (? & ? & _). lia. - } - assert (∀ l, M_t !! (nt, l) = None). - { intros l. destruct (M_t !! (nt, l)) eqn:Hl; last done. - specialize (Ht_dom nt l ltac:(eauto)) as (? & ?); congruence. - } - assert (∀ l, M_s !! (nt, l) = None). - { intros l. destruct (M_s !! (nt, l)) eqn:Hl; last done. - specialize (Hs_dom nt l ltac:(eauto)) as (? & ?); congruence. - } - (* update ghost state *) - iMod (ghost_map_array_tag_insert _ _ (replicate (tsize T) ScPoison ) nt l_t with "Ht_auth") as "[Ht_mem Ht_auth]"; first done. - iMod (ghost_map_array_tag_insert _ _ (replicate (tsize T) ScPoison ) nt l_s with "Hs_auth") as "[Hs_mem Hs_auth]"; first done. - iMod (tkmap_insert tk_local nt () with "Htag_auth") as "[Htag_auth Hnt]"; first done. - iModIntro. - - iFrame "Hnt Hs_mem Ht_mem". - iExists _, _, _, _. iFrame "Htag_auth Ht_auth Hs_auth Hcall_auth". simpl. - iPoseProof (state_rel_get_pure with "Hstate") as "%Hp". - iPoseProof (state_rel_dom_eq with "Hstate") as "%Hdom_eq". - destruct Hp as (Hsst_eq & Hsnp_eq & Hsnc_eq & Hscs_eq). - assert (l_s = l_t) as Hl_eq. - { subst l_s l_t. rewrite (fresh_block_det _ _ Hdom_eq). done. } - iSplitL "Htainted". { subst nt. rewrite -Hsnp_eq. by iApply tag_tainted_interp_alloc. } - iSplitL. - { (* state rel *) - rewrite Hl_eq. iApply sim_alloc_state_rel_update; last done. - intros t ([?[]] & Hs). specialize (Htag_interp _ _ Hs) as (? & ? & _). lia. - } - iSplitL. - { iPureIntro. apply sim_alloc_call_set_interp_update; done. } - iSplitL. - { (* tag interp *) - iPureIntro. split_and!. - { simpl. intros t tk. rewrite lookup_insert_Some. intros [[<- [= <-]] | [Hneq Hsome]]. - - (* new tag: under local control *) - split_and!; [ lia | lia | | |]. - + intros l' sc_t Hsc_t%lookup_union_Some_l'; last done. by apply local_alloc_loc_controlled. - + intros l' sc_t Hsc_s%lookup_union_Some_l'; last done. by apply local_alloc_loc_controlled. - + apply dom_agree_on_tag_union; first last. - { apply dom_agree_on_tag_not_elem; done. } - rewrite Hl_eq. apply dom_agree_on_tag_array_tag_map. - by rewrite replicate_length. - - (* old tag *) - specialize (Htag_interp _ _ Hsome) as (? & ? & Hcontrol_t & Hcontrol_s & Hag). - split_and!; [lia | lia | .. ]. - + intros l' sc_t Hsc_t. apply loc_controlled_alloc_update; [done | done| ]. - rewrite lookup_union_r in Hsc_t; first by apply Hcontrol_t. - apply array_tag_map_lookup_None. lia. - + intros l' sc_s Hsc_s. subst nt. rewrite -Hsnp_eq. apply loc_controlled_alloc_update; [done | lia | ]. - rewrite lookup_union_r in Hsc_s; first by apply Hcontrol_s. - apply array_tag_map_lookup_None. lia. - + apply dom_agree_on_tag_union; last done. - rewrite Hl_eq. apply dom_agree_on_tag_not_elem. - all: intros l; rewrite array_tag_map_lookup_None; done. - } - all: intros t l'; rewrite lookup_insert_is_Some' lookup_union_is_Some; - intros [[-> _]%array_tag_map_lookup2 | ?]; eauto. - } - eauto. - Qed. - - Lemma state_wf_upd_mem σ l sc : - is_Some (σ.(shp) !! l) → - state_wf σ → - state_wf (state_upd_mem (<[l := sc]>) σ). - Proof. - intros Hs []. constructor; try done. - rewrite dom_insert //. - have ->: {[l]} ∪ dom (gset loc) (shp σ) ≡ dom (gset loc) (shp σ); last done. - split; rewrite elem_of_union; last by eauto. - intros [ ->%elem_of_singleton_1 | ]; last done. - by apply elem_of_dom. - Qed. - - Lemma heap_local_write_target σ_t σ_s (t : ptr_id) l sc sc' : - bor_interp σ_t σ_s -∗ - l ↦t[tk_local]{t} sc -∗ - t $$ tk_local ==∗ - bor_interp (state_upd_mem (<[l := sc']>) σ_t) σ_s ∗ - l ↦t[tk_local]{t} sc' ∗ - t $$ tk_local. - Proof. - iIntros "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & Hsrel & ? & %Htag_interp & %Hwf_s & %Hwf_t)". - iIntros "Hp Htag". - iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Htag_lookup". - destruct Htag_interp as (Htag_interp & Ht_dom & Hs_dom). - destruct (Htag_interp _ _ Htag_lookup) as (_ & _ & Ht & Hs & Hagree). - iPoseProof (ghost_map_lookup with "Htag_t_auth Hp") as "%Ht_lookup". - specialize (Ht _ _ Ht_lookup) as Hcontrol. - specialize (loc_controlled_local _ _ _ _ Hcontrol) as (Hstack & Hmem). - - iMod (ghost_map_update sc' with "Htag_t_auth Hp") as "[Htag_t_auth $]". - iModIntro. iFrame "Htag". rewrite /bor_interp. - iExists M_call, M_tag, (<[(t, l):=sc']> M_t), M_s. - iFrame. cbn. iSplitL "Hsrel". - { iApply (state_rel_upd_priv_target with "Hsrel"). - - eauto. - - exists tk_local. split_and!; [done | by eauto | by left ]. - } - iSplitL; first last. - { repeat iSplitL; [ done.. | ]. - iPureIntro. apply state_wf_upd_mem; [by eauto | done]. - } - - iPureIntro. - split_and!. - - intros t' tk' (? & ? & H')%Htag_interp. do 2 (split; first done). - destruct H' as (Ha_t & Ha_s & Hagree'). - split_and!; [ | done | ]. - + intros l' sc_t. - destruct (decide (t = t')) as [<- | Hneq]; first last. - { rewrite lookup_insert_ne; last congruence. intros Hsc_t. - destruct (decide (l' = l)) as [-> | Hneq_loc]. - { (* this is fine as tag t has local ownership: t' doesn't have any control *) - eapply loc_controlled_local_authoritative; [ | by apply Ha_t | done]. - eapply loc_controlled_mem_insert. done. - } - apply loc_controlled_mem_insert_ne; [done | by apply Ha_t]. - } - revert Ha_t. - destruct (decide (l' = l)) as [-> | Hneq_loc] => Ha_t. - * rewrite lookup_insert => [= ->]. by eapply loc_controlled_mem_insert, Ha_t. - * rewrite lookup_insert_ne; last congruence. intros ?. - eapply loc_controlled_mem_insert_ne; [done | by apply Ha_t]. - + destruct (decide (t = t')) as [<- | Hneq]. - * eapply dom_agree_on_tag_upd_target; eauto. - * eapply dom_agree_on_tag_upd_ne_target; eauto. - - intros t' l'. rewrite lookup_insert_is_Some. intros [[= <- <-] | [_ ?%Ht_dom]]; last done. eauto. - - done. - Qed. - - Lemma heap_local_readN_target σ_t σ_s (t : ptr_id) l scs : - bor_interp σ_t σ_s -∗ - l ↦t∗[tk_local]{t} scs -∗ - t $$ tk_local -∗ - ⌜∀ i : nat, (i < length scs)%nat → σ_t.(shp) !! (l +â‚— i) = scs !! i⌠∗ - ⌜∀ i:nat, (i < length scs)%nat → bor_state_own (l +â‚— i) t tk_local σ_tâŒ. - Proof. - iIntros "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & ? & Hsrel & ? & %Htag_interp & %Hwf_s & %Hwf_t)". - iIntros "Hp Htag". - iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Htag_lookup". - destruct Htag_interp as (Htag_interp & _ & _). - destruct (Htag_interp _ _ Htag_lookup) as (_ & _ & Ht & Hs & Hagree). - iPoseProof (ghost_map_array_tag_lookup with "Htag_t_auth Hp") as "%Ht_lookup". - iPureIntro. - enough (∀ i: nat, (i < length scs)%nat → σ_t.(shp) !! (l +â‚— i) = scs !! i ∧ σ_t.(sst) !! (l +â‚— i) = Some [mkItem Unique (Tagged t) None]) as Hsingle. - { split_and!; [ apply Hsingle..]. } - intros i Hi. - specialize (Ht_lookup i Hi). rewrite list_lookup_lookup_total in Ht_lookup; first last. - { by apply lookup_lt_is_Some_2. } - specialize (Ht _ _ Ht_lookup) as Hcontrol. - specialize (loc_controlled_local _ _ _ _ Hcontrol) as (Hstack & Hmem). - split_and!. - - rewrite Hmem. rewrite list_lookup_lookup_total; [done | by apply lookup_lt_is_Some_2]. - - done. - Qed. - - Lemma heap_protected_readN_target σ_t σ_s (t : ptr_id) tk l v_t c M : - (∀ i: nat, (i < length v_t)%nat → call_set_in M t (l +â‚— i)) → - bor_interp σ_t σ_s -∗ - l ↦t∗[tk]{t} v_t -∗ - t $$ tk -∗ - c @@ M -∗ - ⌜∀ i : nat, (i < length v_t)%nat → σ_t.(shp) !! (l +â‚— i) = v_t !! i⌠∗ - ⌜∀ i:nat, (i < length v_t)%nat → bor_state_own (l +â‚— i) t tk σ_tâŒ. - Proof. - iIntros (Hprot) "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & Hsrel & %Hcall & %Htag_interp & %Hwf_s & %Hwf_t)". - iIntros "Hp Htag Hcall". - iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Htag_lookup". - destruct Htag_interp as (Htag_interp & _ & _). - destruct (Htag_interp _ _ Htag_lookup) as (_ & _ & Ht & Hs & Hagree). - iPoseProof (ghost_map_array_tag_lookup with "Htag_t_auth Hp") as "%Ht_lookup". - iPoseProof (ghost_map_lookup with "Hc Hcall") as "%Hc_lookup". - iPureIntro. - enough (∀ i: nat, (i < length v_t)%nat → σ_t.(shp) !! (l +â‚— i) = v_t !! i ∧ bor_state_own (l +â‚— i) t tk σ_t) as Hsingle. - { split_and!; [ apply Hsingle..]. } - intros i Hi. - specialize (Ht_lookup i Hi). rewrite list_lookup_lookup_total in Ht_lookup; first last. - { by apply lookup_lt_is_Some_2. } - specialize (Ht _ _ Ht_lookup) as Hcontrol. - assert (bor_state_pre (l +â‚— i) t tk σ_t) as Hpre. - { specialize (Hprot i Hi). - specialize (call_set_interp_access _ _ _ _ _ Hcall ltac:(exists M; done)). apply loc_protected_bor_state_pre. - } - specialize (Hcontrol Hpre) as [Hown Hmem]. - split_and!; [| done ]. - - rewrite Hmem. rewrite list_lookup_lookup_total; [done | ]. by apply lookup_lt_is_Some_2. - Qed. - - Lemma heap_readN_target σ_t σ_s (t : ptr_id) tk l v_t : - bor_interp σ_t σ_s -∗ - l ↦t∗[tk]{t} v_t -∗ - t $$ tk -∗ - ⌜∀ i:nat, (i < length v_t)%nat → loc_controlled (l +â‚— i) t tk (v_t !!! i) σ_tâŒ. - Proof. - iIntros "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & Hsrel & %Hcall & %Htag_interp & %Hwf_s & %Hwf_t)". - iIntros "Hp Htag". - iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Htag_lookup". - destruct Htag_interp as (Htag_interp & _ & _). - destruct (Htag_interp _ _ Htag_lookup) as (_ & _ & Ht & _ & _). - iPoseProof (ghost_map_array_tag_lookup with "Htag_t_auth Hp") as "%Ht_lookup". - iPureIntro. - intros i Hi. - specialize (Ht_lookup i Hi). rewrite list_lookup_lookup_total in Ht_lookup; first last. - { by apply lookup_lt_is_Some_2. } - apply Ht. done. - Qed. - - Lemma heap_readN_source σ_t σ_s (t : ptr_id) tk l v_s : - bor_interp σ_t σ_s -∗ - l ↦s∗[tk]{t} v_s -∗ - t $$ tk -∗ - ⌜∀ i:nat, (i < length v_s)%nat → loc_controlled (l +â‚— i) t tk (v_s !!! i) σ_sâŒ. - Proof. - iIntros "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & Hsrel & %Hcall & %Htag_interp & %Hwf_s & %Hwf_t)". - iIntros "Hp Htag". - iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Htag_lookup". - destruct Htag_interp as (Htag_interp & _ & _). - destruct (Htag_interp _ _ Htag_lookup) as (_ & _ & _ & Hs & _). - iPoseProof (ghost_map_array_tag_lookup with "Htag_s_auth Hp") as "%Hs_lookup". - iPureIntro. intros i Hi. - specialize (Hs_lookup i Hi). rewrite list_lookup_lookup_total in Hs_lookup; first last. - { by apply lookup_lt_is_Some_2. } - apply Hs. done. - Qed. - - Lemma heap_protected_readN_source σ_t σ_s (t : ptr_id) tk l v_t c M : - (∀ i: nat, (i < length v_t)%nat → call_set_in M t (l +â‚— i)) → - bor_interp σ_t σ_s -∗ - l ↦s∗[tk]{t} v_t -∗ - t $$ tk -∗ - c @@ M -∗ - ⌜∀ i : nat, (i < length v_t)%nat → σ_s.(shp) !! (l +â‚— i) = v_t !! i⌠∗ - ⌜∀ i:nat, (i < length v_t)%nat → bor_state_own (l +â‚— i) t tk σ_sâŒ. - Proof. - Admitted. - - Lemma state_upd_mem_compose f g σ : - state_upd_mem f (state_upd_mem g σ) = state_upd_mem (f ∘ g) σ. - Proof. destruct σ. done. Qed. - - Lemma write_mem_insert_commute_1 l l' v sc M : - l.2 < l'.2 → - <[ l := sc ]> (write_mem l' v M) = write_mem l' v (<[ l := sc ]> M). - Proof. - induction v in l, l', sc, M |-*; cbn; first done. - intros Hl. rewrite (IHv l (l' +â‚— 1)); first last. - { destruct l', l; cbn in *; lia. } - rewrite insert_commute; first done. intros ->; lia. - Qed. - Lemma write_mem_head l sc v M : - <[ l := sc ]> (write_mem (l +â‚— 1) v M) = write_mem l (sc :: v) M. - Proof. rewrite write_mem_insert_commute_1; last by destruct l; cbn; lia. done. Qed. - - Global Instance state_upd_mem_proper : Proper ((eq ==> eq) ==> eq ==> eq) state_upd_mem. - Proof. - intros f g Heq ? σ ->. destruct σ as [ mem ]. by rewrite /state_upd_mem (Heq mem mem eq_refl). - Qed. - Lemma state_upd_write_mem_head sc v l σ : - state_upd_mem (<[ l := sc ]> ∘ write_mem (l +â‚— 1) v) σ = state_upd_mem (write_mem l (sc :: v)) σ. - Proof. destruct σ. rewrite /state_upd_mem. cbn. by rewrite write_mem_head. Qed. - - Lemma heap_local_writeN_target σ_t σ_s (t : ptr_id) l scs scs' : - bor_interp σ_t σ_s -∗ - l ↦t∗[tk_local]{t} scs -∗ - t $$ tk_local -∗ - ⌜length scs' = length scs⌠==∗ - bor_interp (state_upd_mem (write_mem l scs') σ_t) σ_s ∗ - l ↦t∗[tk_local]{t} scs' ∗ - t $$ tk_local. - Proof. - iInduction scs' as [ | sc' scs'] "IH" forall (l scs). - - iIntros "Hbor Hp Ht %Hlen". destruct scs; last done. iFrame "Ht Hp". iModIntro. destruct σ_t; eauto. - - iIntros "Hbor Hp Ht %Hlen". destruct scs as [ | sc scs]; first done. - iPoseProof (big_sepL_cons with "Hp") as "[Hh Hp]". - iMod ("IH" $! (l +â‚— 1) scs with "Hbor [Hp] Ht []") as "(Hbor & Hp & Ht)". - { iApply (big_sepL_mono with "Hp"). intros i sc0 Hsc0. cbn. - rewrite shift_loc_assoc. replace (1 + i)%Z with (Z.of_nat $ S i) by lia. done. } - { cbn in Hlen. iPureIntro. lia. } - iMod (heap_local_write_target _ _ _ _ _ sc' with "Hbor Hh Ht") as "(Hbor & Hh & Ht)". - iModIntro. iFrame "Ht". iSplitL "Hbor". - { rewrite state_upd_mem_compose. rewrite shift_loc_0_nat. by rewrite state_upd_write_mem_head. } - iApply big_sepL_cons. iFrame "Hh". iApply (big_sepL_mono with "Hp"). - intros i sc0 Hsc0. cbn. - rewrite shift_loc_assoc. replace (1 + i)%Z with (Z.of_nat $ S i) by lia. done. - Qed. - - Lemma heap_local_readN_source σ_t σ_s (t : ptr_id) l scs : - bor_interp σ_t σ_s -∗ - l ↦s∗[tk_local]{t} scs -∗ - t $$ tk_local -∗ - ⌜∀ i : nat, (i < length scs)%nat → σ_s.(shp) !! (l +â‚— i) = scs !! i⌠∗ - ⌜∀ i:nat, (i < length scs)%nat → bor_state_own (l +â‚— i) t tk_local σ_sâŒ. - Proof. - Admitted. - - Lemma heap_local_writeN_source σ_t σ_s (t : ptr_id) l scs scs' : - bor_interp σ_t σ_s -∗ - l ↦s∗[tk_local]{t} scs -∗ - t $$ tk_local -∗ - ⌜length scs' = length scs⌠==∗ - bor_interp σ_t (state_upd_mem (write_mem l scs') σ_s) ∗ - l ↦s∗[tk_local]{t} scs' ∗ - t $$ tk_local. - Proof. - Admitted. - - Lemma loc_controlled_dealloc_update σ l l' (bor : tag) n (α' : stacks) (t : ptr_id) (tk : tag_kind) sc : - memory_deallocated σ.(sst) σ.(scs) l bor n = Some α' → - state_wf σ → - (bor = Tagged t ∧ (∃ i:nat, l' = l +â‚— i ∧ (i < n)%nat) → tk = tk_pub) → - loc_controlled l' t tk sc σ → - loc_controlled l' t tk sc (mkState (free_mem l n σ.(shp)) α' σ.(scs) σ.(snp) σ.(snc)). - Proof. - intros Hdealloc Hwf Hpub Hcontrol Hpre. - destruct tk. - - (* public *) - destruct Hpre as (stk & pm & opro & Hstk & Hit & Hpm). simpl in *. - destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Hdealloc _ _ Hstk) as [Hneq Hstk']. - destruct Hcontrol as [Hown Hshp]. { exists stk, pm, opro. done. } - destruct Hown as (stk' & Hstk'' & Hsro). - split. - + simplify_eq. exists stk. done. - + destruct (free_mem_lookup_case l' l n σ.(shp)) as [(_ & ->) | (i & Hi & -> & _)]; first done. - specialize (Hneq i Hi). congruence. - - (* unique *) - destruct Hpre as (stk & pm & opro & Hstk & Hit & Hpm). simpl in *. - destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Hdealloc _ _ Hstk) as [Hneq Hstk']. - destruct Hcontrol as [Hown Hshp]. { exists stk, pm, opro. done. } - destruct Hown as (stk' & Hstk'' & (opro' & ? & ->)). - split. - + simplify_eq. exists stk. split; first done. rewrite Hstk' in Hstk''. - injection Hstk'' as ->. eauto. - + destruct (free_mem_lookup_case l' l n σ.(shp)) as [(_ & ->) | (i & Hi & -> & _)]; first done. - specialize (Hneq i Hi). congruence. - - (* local *) clear Hpre. destruct Hcontrol as [Hown Hshp]; first done. simpl. - destruct (free_mem_lookup_case l' l n σ.(shp)) as [(Hi & ->) | (i & Hi & -> & Hfree)]. - + split; last done. destruct (for_each_dealloc_lookup _ _ _ _ _ Hdealloc) as (_ & Heq). - rewrite Heq; done. - + exfalso. destruct (for_each_true_lookup_case_2 _ _ _ _ _ Hdealloc) as [Heq _]. - specialize (Heq _ Hi) as (stk & stk' & Hstk & Hstk' & Hd1). - rewrite Hown in Hstk. injection Hstk as <-. - destruct (dealloc1 _ _ _) eqn:Heq; [ | done]. - destruct (dealloc1_singleton_Some _ _ _ ltac:(eauto)) as (<- & _). - enough (tk_local = tk_pub) by congruence. apply Hpub. eauto. - Qed. -End lemmas. - -(* accessing a local location is only possible with the same tag, retaining the same stack for the access *) -Lemma local_access_eq l t t' stk n stk' kind σ_s σ_t M_tag M_t M_s : - σ_t.(sst) !! l = Some stk → - access1 stk kind t' σ_t.(scs) = Some (n, stk') → - M_tag !! t = Some (tk_local, ()) → - is_Some (M_t !! (t, l)) → - tag_interp M_tag M_t M_s σ_t σ_s → - t' = Tagged t ∧ stk' = stk. -Proof. - intros Hst Haccess Htag Ht Htag_interp. - specialize (access1_in_stack _ _ _ _ _ _ Haccess) as (it & Hin_stack & <- & Henabled). - destruct Htag_interp as (Htag_interp & _ & _). - specialize (Htag_interp _ _ Htag) as (_ & _ & Htl & Hsl & Hdom). - destruct Ht as (sc_t & Ht). - specialize (Htl _ _ Ht) as Hcontrol. - apply loc_controlled_local in Hcontrol as (Hcontrol & _). - destruct (tag_unique_head_access σ_t.(scs) _ (Tagged t) None kind ltac:(by exists [])) as (n' & Hn). - move : Hst Hin_stack Haccess . - rewrite Hcontrol => [= <-]. rewrite elem_of_list_singleton => ->. - rewrite Hn => [= _ <-]. done. -Qed. - -Lemma protector_access_eq l t t' stk n stk' kind σ_s σ_t M_tag Mcall M_t M_s : - σ_t.(sst) !! l = Some stk → - access1 stk kind t' σ_t.(scs) = Some (n, stk') → - M_tag !! t = Some (tk_unq, ()) → - is_Some (M_t !! (t, l)) → - (∃ (c: call_id), call_set_in' Mcall c t l) → - tag_interp M_tag M_t M_s σ_t σ_s → - call_set_interp Mcall σ_t → - state_wf σ_t → - t' = Tagged t. -Proof. - intros Hst Haccess Htag Ht (c & Hcall) Htag_interp Hcall_interp Hwf. - specialize (call_set_interp_access _ _ _ _ _ Hcall_interp Hcall) as (Hc_in & _ & (stk'' & pm & Hstk'' & Hin & Hpm)). - destruct Htag_interp as (Htag_interp & _ & _). - specialize (Htag_interp _ _ Htag) as (_ & _ & Htl & Hsl & Hdom). - destruct Ht as (sc_t & Ht). - specialize (Htl _ _ Ht) as Hcontrol. - specialize (loc_controlled_unq _ _ _ _ _ Hcontrol Hstk'' ltac:(eauto)) as ((stk''' & opro & ->) & Hmem). - move : Hstk'' Hin Haccess. rewrite Hst => [= Heq]. move : Hst. rewrite Heq => Hst Hi. - have ->: opro = Some c. - { destruct (state_wf_stack_item _ Hwf _ _ Hst) as [_ ND]. - have [=] := stack_item_tagged_NoDup_eq _ _ _ t ND Hi ltac:(by left) eq_refl eq_refl. - done. - } - eapply access1_incompatible_head_protector; [by (eexists; eauto) | done]. -Qed. - -(* successfully accesses with a private location are only possible when the tag is equal *) -Lemma priv_loc_UB_access_eq l kind σ_s σ_t t t' stk M_tag M_t M_s Mcall : - σ_t.(sst) !! l = Some stk → - is_Some (access1 stk kind t' σ_t.(scs)) → - priv_loc M_tag M_t Mcall t l → - tag_interp M_tag M_t M_s σ_t σ_s → - call_set_interp Mcall σ_t → - state_wf σ_t → - t' = Tagged t. -Proof. - intros Hs ([? ?] & Haccess) Hpriv Htag_interp Hcall_interp Hwf. - destruct Hpriv as (tk & Htag & Ht & [-> | [-> Hc]]). - - by eapply local_access_eq. - - eapply protector_access_eq; done. -Qed. - -Definition untagged_or_public (M_tag : gmap ptr_id (tag_kind * unit)) t := - match t with - | Tagged t2 => M_tag !! t2 = Some (tk_pub, ()) - | Untagged => True - end. -Lemma priv_pub_access_UB l kind σ_s σ_t t t' stk M_tag Mcall M_t M_s : - σ_t.(sst) !! l = Some stk → - is_Some (access1 stk kind t' σ_t.(scs)) → - priv_loc M_tag M_t Mcall t l → - tag_interp M_tag M_t M_s σ_t σ_s → - call_set_interp Mcall σ_t → - state_wf σ_t → - untagged_or_public M_tag t' → - False. -Proof. - intros Hs Haccess Hpriv Htag_interp Hcall_interp Hwf. - rewrite (priv_loc_UB_access_eq _ _ _ _ _ _ _ _ _ _ _ Hs Haccess Hpriv Htag_interp Hcall_interp Hwf). - destruct Hpriv as (tk & Hl & _ & [-> | [-> _]]); cbn; intros; simplify_eq. -Qed. - -Lemma priv_loc_UB_retag_access_eq σ_s σ_t c l old new mut T kind α' nxtp' M_tag M_t M_s Mcall - (FRZ: if mut is Immutable then is_freeze T else True) - (N2P: kind ≠TwoPhase) : - retag σ_t.(sst) σ_t.(snp) σ_t.(scs) c l old kind (RefPtr mut) T = Some (new, α', nxtp') → - ∀ i t, (i < tsize T)%nat → - priv_loc M_tag M_t Mcall t (l +â‚— i) → - tag_interp M_tag M_t M_s σ_t σ_s → - call_set_interp Mcall σ_t → - state_wf σ_t → - untagged_or_public M_tag old → - False. -Proof. - intros Hrt i t Hi. - have NZST: (0 < tsize T)%nat by lia. - destruct (retag_change_ref_NZST _ _ _ _ _ _ _ _ _ _ _ _ NZST Hrt); - subst new nxtp'. - destruct (retag_Some_Ref _ _ _ _ _ _ _ _ _ _ _ _ NZST FRZ N2P Hrt _ Hi) - as (stk & stk' & Eqstk & Eqstk' & GR). - apply grant_access1 in GR; [|by destruct mut]. - revert Eqstk GR. by apply priv_pub_access_UB. -Qed. - - - -Fixpoint seq_loc_set (l : loc) (n : nat) : gset loc := - match n with - | O => ∅ - | S n => {[ l +â‚— n ]} ∪ seq_loc_set l n - end. -Lemma seq_loc_set_elem l n l' : - l' ∈ seq_loc_set l n ↔ (∃ (i : nat), (i < n)%nat ∧ l' = l +â‚— i). -Proof. - induction n as [ | n IH]; simpl. - - rewrite elem_of_empty. split; first done. intros (i & Hi & _). lia. - - rewrite elem_of_union elem_of_singleton. split. - + intros [-> | (i & Hi & ->)%IH]; [ exists n; naive_solver | exists i; naive_solver]. - + intros (i & Hi & ->). destruct (decide (i = n)) as [-> | Hneq]; first by left. - right. apply IH. exists i. split; [lia | done]. -Qed. - -(** TODO: these lemmas need a new home *) -Section lemmas. -Context `{!sborG Σ}. -Implicit Types P Q : iProp Σ. -Implicit Types Φ : expr → expr → iProp Σ. -Implicit Types σ σ_s σ_t : state. -Implicit Types r r_s r_t : result. -Implicit Types l : loc. -Implicit Types f : fname. - -Context (Ω : result → result → iProp Σ). - -Lemma bor_state_own_access1_read l t tk stk σ : - bor_state_own l t tk σ → - σ.(sst) !! l = Some stk → - ∃ n, access1 stk AccessRead (Tagged t) σ.(scs) = Some (n, stk). -Proof. - intros Hown. destruct tk; cbn in *. - - destruct Hown as (st & -> & Hsro). move => [= <-]. by apply tag_SRO_top_access. - - destruct Hown as (st & Hsst & (opro & st' & H)). simplify_eq. rewrite Hsst => [= <-]. - eapply tag_unique_head_access. eexists; eauto. - - rewrite Hown => [= <-]. - eapply tag_unique_head_access. eexists; eauto. -Qed. - -Lemma memory_read_access1 (stks : stacks) l n t calls : - (∀ i: nat, (i < n)%nat → ∃ stk, stks !! (l +â‚— i) = Some stk ∧ ∃ m, access1 stk AccessRead (Tagged t) calls = Some (m, stk)) → - memory_read stks calls l (Tagged t) n = Some stks. -Proof. - induction n as [ | n IH]; cbn; first done. - intros Hacc1. destruct (Hacc1 n ltac:(lia)) as (stkn & Hl & (m & Hacc1_n)). rewrite Hl. - cbn. rewrite Hacc1_n. cbn. - rewrite insert_id; last done. apply IH. intros i Hi. apply Hacc1. lia. -Qed. - -Lemma retag_mut_loc_controlled σ c l ot T mut α' rk i sc : - let nt := σ.(snp) in - let pk := RefPtr mut in - let tk := match mut with Mutable => tk_unq | Immutable => tk_pub end in - (if mut is Immutable then is_freeze T else True) → - retag σ.(sst) σ.(snp) σ.(scs) c l ot rk pk T = Some (Tagged nt, α', S σ.(snp)) → - (is_two_phase rk = false) → - (i < tsize T)%nat → - σ.(shp) !! (l +â‚— i) = Some sc → - loc_controlled (l +â‚— i) nt tk sc (mkState σ.(shp) α' σ.(scs) (S σ.(snp)) σ.(snc)). -Proof. - intros nt pk tk Hfreeze Hretag Hrk Hi Hsc Hpre. split; last done. - destruct mut. - * (* unique *) - destruct Hpre as (st & pm' & opro & Hst & Hit & Hpm'). exists st. split; first done. - rewrite /retag Hrk in Hretag. - have EqRT': - retag_ref σ.(sst) σ.(scs) σ.(snp) l ot T (UniqueRef false) (adding_protector rk c) = - Some (Tagged nt, α', S nt) by done. - destruct (tag_on_top_retag_ref_uniq _ _ _ _ _ _ _ _ _ _ EqRT' i ltac:(lia)) - as [pro1 Eqstk1]. rewrite Hst /= in Eqstk1. - clear -Eqstk1. destruct st as [|? stk1]; [done|]. - simpl in Eqstk1. simplify_eq. by exists pro1, stk1. - * (* shared *) - destruct Hpre as (stk' & pm' & pro & Eqstk' & In' & NDIS). simpl in Eqstk'. - exists stk'. split; [done|]. - have EqRT': - retag_ref σ.(sst) σ.(scs) σ.(snp) l ot T SharedRef (adding_protector rk c) = Some (Tagged nt, α', S nt) by done. - have HTOP := (tag_on_top_retag_ref_shr _ _ _ _ _ _ _ _ _ _ Hfreeze EqRT' i ltac:(lia)). - clear -HTOP Eqstk'. - apply tag_on_top_shr_active_SRO in HTOP as (?&?&?). by simplify_eq. -Qed. - -Lemma retag_loc_controlled_preserved σ c l l' t tk' ot T pk rk α' nt nxtp' sc : - state_wf σ → - retag σ.(sst) σ.(snp) σ.(scs) c l ot rk pk T = Some (nt, α', nxtp') → - (Tagged t = ot → tk' = tk_pub) → - (t < σ.(snp))%nat → - loc_controlled l' t tk' sc σ → - loc_controlled l' t tk' sc (mkState σ.(shp) α' σ.(scs) nxtp' σ.(snc)). -Proof. - intros Hwf Hretag Hneq Hlt Hcontrolled. - intros Hpre. destruct tk'. - * destruct Hpre as (stk' & pm' & pro & Eqstk' & In' & ND). - destruct (retag_item_in _ _ _ _ _ _ _ _ _ _ _ _ Hretag _ _ t _ Eqstk' In') - as (stk & Eqstk & In); [done..|]. - - destruct Hcontrolled as (Hown & Hl'). { simpl; naive_solver. } - cbn. split; last done. - exists stk'. split; [done|]. - destruct Hown as (stk1 & Eqstk1 & HTOP). - rewrite Eqstk1 in Eqstk. simplify_eq. - move : HTOP. - have ND2 := proj2 (state_wf_stack_item _ Hwf _ _ Eqstk1). - by apply (retag_item_active_SRO_preserving _ _ _ _ _ _ _ _ _ _ _ _ Hretag _ _ _ _ _ ND2 Eqstk1 Eqstk' In In'). - * destruct Hpre as (stk' & pm' & pro & Eqstk' & In' & ND). - destruct (retag_item_in _ _ _ _ _ _ _ _ _ _ _ _ Hretag _ _ t _ Eqstk' In') - as (stk & Eqstk & In); [done..|]. - destruct Hcontrolled as (Hown & Hl'); [simpl; naive_solver|]. - split; last done. cbn. - exists stk'. split; [done|]. - destruct Hown as (stk1 & Eqstk1 & opro1 & HTOP). - rewrite Eqstk1 in Eqstk. simplify_eq. - have ND2 := proj2 (state_wf_stack_item _ Hwf _ _ Eqstk1). - assert (opro1 = pro ∧ pm' = Unique) as []. - { have In1 : mkItem Unique (Tagged t) opro1 ∈ stk. - { destruct HTOP as [? HTOP]. rewrite HTOP. by left. } - have EQ := stack_item_tagged_NoDup_eq _ _ _ t ND2 In1 In eq_refl eq_refl. - by simplify_eq. } subst opro1 pm'. exists pro. - have NEq: Tagged t ≠ot. - { intros <-. specialize (Hneq eq_refl). congruence. } - move : HTOP. - by apply (retag_item_head_preserving _ _ _ _ _ _ _ _ _ _ _ _ Hretag - _ _ _ _ _ ND2 Eqstk1 Eqstk' NEq In'). - * clear Hpre. specialize (Hcontrolled I) as (Hown & Hl'). split; last done. - move : Hown. cbn. - have NEq: ot ≠Tagged t. - { intros ->. specialize (Hneq eq_refl). congruence. } - move : NEq. by eapply retag_Some_local. -Qed. -End lemmas. - diff --git a/theories/stacked_borrows/inv_accessors.v b/theories/stacked_borrows/inv_accessors.v new file mode 100644 index 0000000000000000000000000000000000000000..a771becf785d5d801f08a587b3c747d5cd0240e3 --- /dev/null +++ b/theories/stacked_borrows/inv_accessors.v @@ -0,0 +1,765 @@ +From iris.proofmode Require Export tactics. +From iris.base_logic.lib Require Import ghost_map. +From simuliris.base_logic Require Export gen_sim_prog. +From simuliris.simulation Require Export slsls. +From simuliris.simulation Require Import lifting. +From simuliris.stacked_borrows Require Import tkmap_view. +From simuliris.stacked_borrows Require Export defs. +From simuliris.stacked_borrows Require Import steps_progress steps_retag steps_inv logical_state. +From iris.prelude Require Import options. + + + +(** Lemmas / Accessors *) +Add Printing Constructor state item. +Section lemmas. + Context `{bor_stateGS Σ}. + Local Notation bor_interp := (bor_interp sc_rel). + + Implicit Types + (l : loc) (sc : scalar). + + Lemma init_mem_dom_L l n h : + dom (gset loc) (init_mem l n h) = dom (gset loc) h ∪ dom (gset loc) (init_mem l n ∅). + Proof. apply set_eq. intros l'. rewrite init_mem_dom. done. Qed. + + Lemma fresh_block_not_elem_dom h i : + (fresh_block h, i) ∉ dom (gset loc) h. + Proof. + rewrite /fresh_block. + rewrite -elem_of_elements. + Admitted. + + Lemma fresh_block_det σ_s σ_t : + dom (gset loc) σ_s.(shp) = dom (gset loc) σ_t.(shp) → + fresh_block σ_s.(shp) = fresh_block σ_t.(shp). + Proof. rewrite /fresh_block. intros ->. done. Qed. + + Lemma free_mem_dom σ_t σ_s l n : + dom (gset loc) σ_t.(shp) = dom (gset loc) σ_s.(shp) → + dom (gset loc) (free_mem l n σ_t.(shp)) = dom (gset loc) (free_mem l n σ_s.(shp)). + Proof. + intros Hdom. induction n as [ | n IH] in l |-*; first done. + simpl. rewrite !dom_delete_L IH. done. + Qed. + + Lemma init_stack_preserve σ n : + let l := (fresh_block σ.(shp), 0) in + let nt := σ.(snp) in + let α' := init_stacks σ.(sst) l n (Tagged nt) in + state_wf σ → + ∀ l' stk, σ.(sst) !! l' = Some stk → α' !! l' = Some stk. + Proof. + intros l nt α' Hwf l' stk Hl'. + rewrite (proj2 (init_stacks_lookup _ _ _ _) l'); first done. + intros i Hi ->. + specialize (elem_of_dom σ.(sst) ((fresh_block (shp σ), 0) +â‚— i)). + rewrite Hl'. intros (_ &Ha). specialize (Ha ltac:(eauto)). + move : Ha. rewrite -state_wf_dom; last done. + apply fresh_block_not_elem_dom. + Qed. + + Lemma init_mem_preserve σ n : + let l := (fresh_block σ.(shp), 0) in + let nt := σ.(snp) in + let h' := init_mem l n σ.(shp) in + ∀ l' sc, σ.(shp) !! l' = Some sc → h' !! l' = Some sc. + Proof. + intros l nt h' l' sc Hsc. + rewrite (proj2 (init_mem_lookup _ _ _) l'); first done. + intros i Hi ->. + specialize (elem_of_dom σ.(shp) ((fresh_block (shp σ), 0) +â‚— i)). + rewrite Hsc. intros (_ &Ha). specialize (Ha ltac:(eauto)). + move : Ha. apply fresh_block_not_elem_dom. + Qed. + + Lemma loc_controlled_alloc_update σ l' n (t : ptr_id) (tk : tag_kind) sc : + let l := (fresh_block σ.(shp), 0) in + let nt := σ.(snp) in + let α' := init_stacks σ.(sst) l n (Tagged nt) in + state_wf σ → + nt ≠t → + loc_controlled l' t tk sc σ → + loc_controlled l' t tk sc (mkState (init_mem l n σ.(shp)) α' σ.(scs) (S σ.(snp)) σ.(snc)). + Proof. + intros l nt α' Hwf Hne Hcontrolled Hpre. + assert (∀ l' stk, α' !! l' = Some stk → stk = init_stack (Tagged nt) ∨ σ.(sst) !! l' = Some stk) as Hα'. + { intros l'' stk Hl'. + specialize (init_stacks_lookup_case _ _ _ _ _ _ Hl') as [(Hstk & _) | (i & Hi & ->)]; first by eauto. + left. rewrite (proj1 (init_stacks_lookup _ _ _ _) i Hi) in Hl'. + injection Hl' as [= <-]. done. + } + assert (bor_state_pre l' t tk σ) as [Hown Hmem]%Hcontrolled. + { destruct tk; last done. + all: destruct Hpre as (stk & pm & opro & [-> | Hstk]%Hα' & Hit & ?); simpl in *; last by eauto 8. + all: exfalso; move : Hit; rewrite elem_of_list_singleton; injection 1; congruence. + } + simpl. split. + - destruct tk. + + destruct Hown as (stk & Hstk & ?). exists stk. split; last done. apply init_stack_preserve; done. + + destruct Hown as (stk & Hstk & ?). exists stk. split; last done. apply init_stack_preserve; done. + + apply init_stack_preserve; done. + - apply init_mem_preserve. done. + Qed. + + Lemma state_rel_alloc_update σ_t σ_s M_tag M_t M_t' M_call l n tk : + let nt := σ_t.(snp) in + (∀ t, is_Some (M_tag !! t) → t ≠nt) → + state_rel sc_rel M_tag M_t M_call σ_t σ_s -∗ + state_rel sc_rel (<[nt := (tk, ())]> M_tag) (M_t' ∪ M_t) M_call + (mkState (init_mem l n (shp σ_t)) (init_stacks (sst σ_t) l n (Tagged nt)) (scs σ_t) (S σ_t.(snp)) (snc σ_t)) + (mkState (init_mem l n (shp σ_s)) (init_stacks (sst σ_s) l n (Tagged nt)) (scs σ_s) (S (snp σ_s)) (snc σ_s)). + Proof. + intros nt Hneq. iIntros "(%Hdom_eq & %Hsst_eq & %Hsnp_eq & %Hsnc_eq & %Hscs_eq & Hstate)". + iSplitR. { simpl. rewrite !(init_mem_dom_L _ _ (shp _)) Hdom_eq. iPureIntro. set_solver. } + simpl. rewrite Hsst_eq. iSplitR; first done. + iSplitR; first by rewrite Hsnp_eq. do 2 (iSplitR; first done). + iIntros (l' (s & [(Heq & Hi) | (i & Hi & ->)]%init_mem_lookup_case)). + + (* old location *) + iDestruct ("Hstate" $! l' with "[]") as "[Hpub | (%t & %Hpriv)]". + { eauto. } + * iLeft. simpl. iIntros (sc_t Hsc_t). simpl in Hsc_t. + rewrite (proj2 (init_mem_lookup _ n _) l' Hi) in Hsc_t. simplify_eq. + iDestruct ("Hpub" $! s with "[//]") as (sc_s Hsc_s) "Hscrel". + iExists sc_s. iSplit; last done. iPureIntro. + by rewrite (proj2 (init_mem_lookup _ n _) l' Hi). + * iRight. iPureIntro. exists t. + destruct Hpriv as (tk' & Htk & Hs & ?). exists tk'. split_and!; [ | | done]. + { rewrite lookup_insert_ne; first done. specialize (Hneq t ltac:(eauto)). done. } + rewrite lookup_union_is_Some. eauto. + + (* new location *) + iLeft. rewrite /pub_loc /=. rewrite !(proj1 (init_mem_lookup _ _ _)); [ | done | done]. + iIntros (? [= <-]). iExists ☠%S. iSplit; done. + Qed. + + Lemma call_set_interp_alloc_update σ n M_call : + state_wf σ → + let nt := σ.(snp) in + let l := (fresh_block σ.(shp), 0) in + call_set_interp M_call σ → + call_set_interp M_call (mkState (init_mem l n (shp σ)) (init_stacks (sst σ) l n (Tagged nt)) (scs σ) (S σ.(snp)) (snc σ)). + Proof. + intros Hwf nt l Hcall_interp c M' [? HM']%Hcall_interp. simpl. split; first done. + intros t L HL. specialize (HM' _ _ HL) as (?& HL'). split; first lia. intros l' Hl'. + specialize (HL' l' Hl') as (stk & pm & Hstk & Hit & ?). + exists stk, pm. split_and!; [ | done..]. + apply init_stack_preserve; done. + Qed. + + Lemma loc_controlled_alloc_local σ l nt n l' sc : + array_tag_map l nt (replicate n ScPoison) !! (nt, l') = Some sc → + loc_controlled l' nt tk_local sc (mkState (init_mem l n σ.(shp)) (init_stacks σ.(sst) l n (Tagged nt)) σ.(scs) (S σ.(snp)) σ.(snc)). + Proof. + intros Hsc. + specialize (array_tag_map_lookup2 l nt _ nt l' ltac:(eauto)) as [_ (i & Hi & ->)]. + intros _. + rewrite array_tag_map_lookup_Some in Hsc; last done. + apply lookup_replicate in Hsc as [-> Hi']. split. + * simpl. rewrite (proj1 (init_stacks_lookup _ _ _ _)); done. + * simpl. rewrite (proj1 (init_mem_lookup _ _ _ )); done. + Qed. + + Lemma bor_interp_alloc_local σ_t σ_s T : + let l_t := (fresh_block σ_t.(shp), 0) in + let l_s := (fresh_block σ_s.(shp), 0) in + let nt := σ_t.(snp) in + state_wf (mkState (init_mem l_t (tsize T) σ_t.(shp)) (init_stacks σ_t.(sst) l_t (tsize T) (Tagged nt)) σ_t.(scs) (S σ_t.(snp)) σ_t.(snc)) → + state_wf (mkState (init_mem l_s (tsize T) σ_s.(shp)) (init_stacks σ_s.(sst) l_s (tsize T) (Tagged nt)) σ_s.(scs) (S σ_s.(snp)) σ_s.(snc)) → + bor_interp σ_t σ_s ==∗ + bor_interp + (mkState (init_mem l_t (tsize T) σ_t.(shp)) (init_stacks σ_t.(sst) l_t (tsize T) (Tagged nt)) σ_t.(scs) (S σ_t.(snp)) σ_t.(snc)) + (mkState (init_mem l_s (tsize T) σ_s.(shp)) (init_stacks σ_s.(sst) l_s (tsize T) (Tagged nt)) σ_s.(scs) (S σ_s.(snp)) σ_s.(snc)) ∗ + nt $$ tk_local ∗ + l_t ↦t∗[tk_local]{nt} replicate (tsize T) ScPoison ∗ + l_s ↦s∗[tk_local]{nt} replicate (tsize T) ScPoison. + Proof. + intros l_t l_s nt Hwf_t' Hwf_s'. + iIntros "(% & % & % & % & (Hcall_auth & Htag_auth & Ht_auth & Hs_auth) & Htainted & #Hstate & %Hcall_interp & %Htag_interp & %Hwf_s & %Hwf_t)". + destruct Htag_interp as (Htag_interp & Ht_dom& Hs_dom). + assert (M_tag !! nt = None) as M_tag_none. + { destruct (M_tag !! nt) as [[? []] | ]eqn:Hs; last done. + apply Htag_interp in Hs as (? & ? & _). lia. + } + assert (∀ l, M_t !! (nt, l) = None). + { intros l. destruct (M_t !! (nt, l)) eqn:Hl; last done. + specialize (Ht_dom nt l ltac:(eauto)) as (? & ?); congruence. + } + assert (∀ l, M_s !! (nt, l) = None). + { intros l. destruct (M_s !! (nt, l)) eqn:Hl; last done. + specialize (Hs_dom nt l ltac:(eauto)) as (? & ?); congruence. + } + (* update ghost state *) + iMod (ghost_map_array_tag_insert _ _ (replicate (tsize T) ScPoison ) nt l_t with "Ht_auth") as "[Ht_mem Ht_auth]"; first done. + iMod (ghost_map_array_tag_insert _ _ (replicate (tsize T) ScPoison ) nt l_s with "Hs_auth") as "[Hs_mem Hs_auth]"; first done. + iMod (tkmap_insert tk_local nt () with "Htag_auth") as "[Htag_auth Hnt]"; first done. + iModIntro. + + iFrame "Hnt Hs_mem Ht_mem". + iExists _, _, _, _. iFrame "Htag_auth Ht_auth Hs_auth Hcall_auth". simpl. + iPoseProof (state_rel_get_pure with "Hstate") as "%Hp". + iPoseProof (state_rel_dom_eq with "Hstate") as "%Hdom_eq". + destruct Hp as (Hsst_eq & Hsnp_eq & Hsnc_eq & Hscs_eq). + assert (l_s = l_t) as Hl_eq. + { subst l_s l_t. rewrite (fresh_block_det _ _ Hdom_eq). done. } + iSplitL "Htainted". { subst nt. rewrite -Hsnp_eq. by iApply tag_tainted_interp_alloc. } + iSplitL. + { (* state rel *) + rewrite Hl_eq. iApply state_rel_alloc_update; last done. + intros t ([?[]] & Hs). specialize (Htag_interp _ _ Hs) as (? & ? & _). lia. + } + iSplitL. + { iPureIntro. apply call_set_interp_alloc_update; done. } + iSplitL. + { (* tag interp *) + iPureIntro. split_and!. + { simpl. intros t tk. rewrite lookup_insert_Some. intros [[<- [= <-]] | [Hneq Hsome]]. + - (* new tag: under local control *) + split_and!; [ lia | lia | | |]. + + intros l' sc_t Hsc_t%lookup_union_Some_l'; last done. by apply loc_controlled_alloc_local. + + intros l' sc_t Hsc_s%lookup_union_Some_l'; last done. by apply loc_controlled_alloc_local. + + apply dom_agree_on_tag_union; first last. + { apply dom_agree_on_tag_not_elem; done. } + rewrite Hl_eq. apply dom_agree_on_tag_array_tag_map. + by rewrite replicate_length. + - (* old tag *) + specialize (Htag_interp _ _ Hsome) as (? & ? & Hcontrol_t & Hcontrol_s & Hag). + split_and!; [lia | lia | .. ]. + + intros l' sc_t Hsc_t. apply loc_controlled_alloc_update; [done | done| ]. + rewrite lookup_union_r in Hsc_t; first by apply Hcontrol_t. + apply array_tag_map_lookup_None. lia. + + intros l' sc_s Hsc_s. subst nt. rewrite -Hsnp_eq. apply loc_controlled_alloc_update; [done | lia | ]. + rewrite lookup_union_r in Hsc_s; first by apply Hcontrol_s. + apply array_tag_map_lookup_None. lia. + + apply dom_agree_on_tag_union; last done. + rewrite Hl_eq. apply dom_agree_on_tag_not_elem. + all: intros l; rewrite array_tag_map_lookup_None; done. + } + all: intros t l'; rewrite lookup_insert_is_Some' lookup_union_is_Some; + intros [[-> _]%array_tag_map_lookup2 | ?]; eauto. + } + eauto. + Qed. + + (** Read lemmas *) + Lemma bor_interp_readN_target_local σ_t σ_s (t : ptr_id) l scs : + bor_interp σ_t σ_s -∗ + l ↦t∗[tk_local]{t} scs -∗ + t $$ tk_local -∗ + ⌜∀ i : nat, (i < length scs)%nat → σ_t.(shp) !! (l +â‚— i) = scs !! i⌠∗ + ⌜∀ i:nat, (i < length scs)%nat → bor_state_own (l +â‚— i) t tk_local σ_tâŒ. + Proof. + iIntros "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & ? & Hsrel & ? & %Htag_interp & %Hwf_s & %Hwf_t)". + iIntros "Hp Htag". + iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Htag_lookup". + destruct Htag_interp as (Htag_interp & _ & _). + destruct (Htag_interp _ _ Htag_lookup) as (_ & _ & Ht & Hs & Hagree). + iPoseProof (ghost_map_array_tag_lookup with "Htag_t_auth Hp") as "%Ht_lookup". + iPureIntro. + enough (∀ i: nat, (i < length scs)%nat → σ_t.(shp) !! (l +â‚— i) = scs !! i ∧ σ_t.(sst) !! (l +â‚— i) = Some [mkItem Unique (Tagged t) None]) as Hsingle. + { split_and!; [ apply Hsingle..]. } + intros i Hi. + specialize (Ht_lookup i Hi). rewrite list_lookup_lookup_total in Ht_lookup; first last. + { by apply lookup_lt_is_Some_2. } + specialize (Ht _ _ Ht_lookup) as Hcontrol. + specialize (loc_controlled_local _ _ _ _ Hcontrol) as (Hstack & Hmem). + split_and!. + - rewrite Hmem. rewrite list_lookup_lookup_total; [done | by apply lookup_lt_is_Some_2]. + - done. + Qed. + + Lemma bor_interp_readN_target_protected σ_t σ_s (t : ptr_id) tk l v_t c M : + (∀ i: nat, (i < length v_t)%nat → call_set_in M t (l +â‚— i)) → + bor_interp σ_t σ_s -∗ + l ↦t∗[tk]{t} v_t -∗ + t $$ tk -∗ + c @@ M -∗ + ⌜∀ i : nat, (i < length v_t)%nat → σ_t.(shp) !! (l +â‚— i) = v_t !! i⌠∗ + ⌜∀ i:nat, (i < length v_t)%nat → bor_state_own (l +â‚— i) t tk σ_tâŒ. + Proof. + iIntros (Hprot) "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & Hsrel & %Hcall & %Htag_interp & %Hwf_s & %Hwf_t)". + iIntros "Hp Htag Hcall". + iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Htag_lookup". + destruct Htag_interp as (Htag_interp & _ & _). + destruct (Htag_interp _ _ Htag_lookup) as (_ & _ & Ht & Hs & Hagree). + iPoseProof (ghost_map_array_tag_lookup with "Htag_t_auth Hp") as "%Ht_lookup". + iPoseProof (ghost_map_lookup with "Hc Hcall") as "%Hc_lookup". + iPureIntro. + enough (∀ i: nat, (i < length v_t)%nat → σ_t.(shp) !! (l +â‚— i) = v_t !! i ∧ bor_state_own (l +â‚— i) t tk σ_t) as Hsingle. + { split_and!; [ apply Hsingle..]. } + intros i Hi. + specialize (Ht_lookup i Hi). rewrite list_lookup_lookup_total in Ht_lookup; first last. + { by apply lookup_lt_is_Some_2. } + specialize (Ht _ _ Ht_lookup) as Hcontrol. + assert (bor_state_pre (l +â‚— i) t tk σ_t) as Hpre. + { specialize (Hprot i Hi). + specialize (call_set_interp_access _ _ _ _ _ Hcall ltac:(exists M; done)). apply loc_protected_bor_state_pre. + } + specialize (Hcontrol Hpre) as [Hown Hmem]. + split_and!; [| done ]. + - rewrite Hmem. rewrite list_lookup_lookup_total; [done | ]. by apply lookup_lt_is_Some_2. + Qed. + + Lemma bor_interp_readN_target σ_t σ_s (t : ptr_id) tk l v_t : + bor_interp σ_t σ_s -∗ + l ↦t∗[tk]{t} v_t -∗ + t $$ tk -∗ + ⌜∀ i:nat, (i < length v_t)%nat → loc_controlled (l +â‚— i) t tk (v_t !!! i) σ_tâŒ. + Proof. + iIntros "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & Hsrel & %Hcall & %Htag_interp & %Hwf_s & %Hwf_t)". + iIntros "Hp Htag". + iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Htag_lookup". + destruct Htag_interp as (Htag_interp & _ & _). + destruct (Htag_interp _ _ Htag_lookup) as (_ & _ & Ht & _ & _). + iPoseProof (ghost_map_array_tag_lookup with "Htag_t_auth Hp") as "%Ht_lookup". + iPureIntro. + intros i Hi. + specialize (Ht_lookup i Hi). rewrite list_lookup_lookup_total in Ht_lookup; first last. + { by apply lookup_lt_is_Some_2. } + apply Ht. done. + Qed. + + Lemma bor_interp_readN_source σ_t σ_s (t : ptr_id) tk l v_s : + bor_interp σ_t σ_s -∗ + l ↦s∗[tk]{t} v_s -∗ + t $$ tk -∗ + ⌜∀ i:nat, (i < length v_s)%nat → loc_controlled (l +â‚— i) t tk (v_s !!! i) σ_sâŒ. + Proof. + iIntros "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & Hsrel & %Hcall & %Htag_interp & %Hwf_s & %Hwf_t)". + iIntros "Hp Htag". + iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Htag_lookup". + destruct Htag_interp as (Htag_interp & _ & _). + destruct (Htag_interp _ _ Htag_lookup) as (_ & _ & _ & Hs & _). + iPoseProof (ghost_map_array_tag_lookup with "Htag_s_auth Hp") as "%Hs_lookup". + iPureIntro. intros i Hi. + specialize (Hs_lookup i Hi). rewrite list_lookup_lookup_total in Hs_lookup; first last. + { by apply lookup_lt_is_Some_2. } + apply Hs. done. + Qed. + + Lemma bor_interp_readN_source_protected σ_t σ_s (t : ptr_id) tk l v_t c M : + (∀ i: nat, (i < length v_t)%nat → call_set_in M t (l +â‚— i)) → + bor_interp σ_t σ_s -∗ + l ↦s∗[tk]{t} v_t -∗ + t $$ tk -∗ + c @@ M -∗ + ⌜∀ i : nat, (i < length v_t)%nat → σ_s.(shp) !! (l +â‚— i) = v_t !! i⌠∗ + ⌜∀ i:nat, (i < length v_t)%nat → bor_state_own (l +â‚— i) t tk σ_sâŒ. + Proof. + Admitted. + + Lemma bor_interp_readN_source_local σ_t σ_s (t : ptr_id) l scs : + bor_interp σ_t σ_s -∗ + l ↦s∗[tk_local]{t} scs -∗ + t $$ tk_local -∗ + ⌜∀ i : nat, (i < length scs)%nat → σ_s.(shp) !! (l +â‚— i) = scs !! i⌠∗ + ⌜∀ i:nat, (i < length scs)%nat → bor_state_own (l +â‚— i) t tk_local σ_sâŒ. + Proof. + Admitted. + + (** * Write lemmas *) + Lemma state_upd_mem_compose f g σ : + state_upd_mem f (state_upd_mem g σ) = state_upd_mem (f ∘ g) σ. + Proof. destruct σ. done. Qed. + + Lemma write_mem_insert_commute_1 l l' v sc M : + l.2 < l'.2 → + <[ l := sc ]> (write_mem l' v M) = write_mem l' v (<[ l := sc ]> M). + Proof. + induction v in l, l', sc, M |-*; cbn; first done. + intros Hl. rewrite (IHv l (l' +â‚— 1)); first last. + { destruct l', l; cbn in *; lia. } + rewrite insert_commute; first done. intros ->; lia. + Qed. + Lemma write_mem_head l sc v M : + <[ l := sc ]> (write_mem (l +â‚— 1) v M) = write_mem l (sc :: v) M. + Proof. rewrite write_mem_insert_commute_1; last by destruct l; cbn; lia. done. Qed. + + Global Instance state_upd_mem_proper : Proper ((eq ==> eq) ==> eq ==> eq) state_upd_mem. + Proof. + intros f g Heq ? σ ->. destruct σ as [ mem ]. by rewrite /state_upd_mem (Heq mem mem eq_refl). + Qed. + Lemma state_upd_write_mem_head sc v l σ : + state_upd_mem (<[ l := sc ]> ∘ write_mem (l +â‚— 1) v) σ = state_upd_mem (write_mem l (sc :: v)) σ. + Proof. destruct σ. rewrite /state_upd_mem. cbn. by rewrite write_mem_head. Qed. + + Lemma state_wf_upd_mem σ l sc : + is_Some (σ.(shp) !! l) → + state_wf σ → + state_wf (state_upd_mem (<[l := sc]>) σ). + Proof. + intros Hs []. constructor; try done. + rewrite dom_insert //. + have ->: {[l]} ∪ dom (gset loc) (shp σ) ≡ dom (gset loc) (shp σ); last done. + split; rewrite elem_of_union; last by eauto. + intros [ ->%elem_of_singleton_1 | ]; last done. + by apply elem_of_dom. + Qed. + + Lemma bor_interp_write_target_local σ_t σ_s (t : ptr_id) l sc sc' : + bor_interp σ_t σ_s -∗ + l ↦t[tk_local]{t} sc -∗ + t $$ tk_local ==∗ + bor_interp (state_upd_mem (<[l := sc']>) σ_t) σ_s ∗ + l ↦t[tk_local]{t} sc' ∗ + t $$ tk_local. + Proof. + iIntros "(% & % & % & % & (Hc & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & Hsrel & ? & %Htag_interp & %Hwf_s & %Hwf_t)". + iIntros "Hp Htag". + iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Htag_lookup". + destruct Htag_interp as (Htag_interp & Ht_dom & Hs_dom). + destruct (Htag_interp _ _ Htag_lookup) as (_ & _ & Ht & Hs & Hagree). + iPoseProof (ghost_map_lookup with "Htag_t_auth Hp") as "%Ht_lookup". + specialize (Ht _ _ Ht_lookup) as Hcontrol. + specialize (loc_controlled_local _ _ _ _ Hcontrol) as (Hstack & Hmem). + + iMod (ghost_map_update sc' with "Htag_t_auth Hp") as "[Htag_t_auth $]". + iModIntro. iFrame "Htag". rewrite /bor_interp. + iExists M_call, M_tag, (<[(t, l):=sc']> M_t), M_s. + iFrame. cbn. iSplitL "Hsrel". + { iApply (state_rel_upd_priv_target with "Hsrel"). + - eauto. + - exists tk_local. split_and!; [done | by eauto | by left ]. + } + iSplitL; first last. + { repeat iSplitL; [ done.. | ]. + iPureIntro. apply state_wf_upd_mem; [by eauto | done]. + } + + iPureIntro. + split_and!. + - intros t' tk' (? & ? & H')%Htag_interp. do 2 (split; first done). + destruct H' as (Ha_t & Ha_s & Hagree'). + split_and!; [ | done | ]. + + intros l' sc_t. + destruct (decide (t = t')) as [<- | Hneq]; first last. + { rewrite lookup_insert_ne; last congruence. intros Hsc_t. + destruct (decide (l' = l)) as [-> | Hneq_loc]. + { (* this is fine as tag t has local ownership: t' doesn't have any control *) + eapply loc_controlled_local_authoritative; [ | by apply Ha_t | done]. + eapply loc_controlled_mem_insert. done. + } + apply loc_controlled_mem_insert_ne; [done | by apply Ha_t]. + } + revert Ha_t. + destruct (decide (l' = l)) as [-> | Hneq_loc] => Ha_t. + * rewrite lookup_insert => [= ->]. by eapply loc_controlled_mem_insert, Ha_t. + * rewrite lookup_insert_ne; last congruence. intros ?. + eapply loc_controlled_mem_insert_ne; [done | by apply Ha_t]. + + destruct (decide (t = t')) as [<- | Hneq]. + * eapply dom_agree_on_tag_upd_target; eauto. + * eapply dom_agree_on_tag_upd_ne_target; eauto. + - intros t' l'. rewrite lookup_insert_is_Some. intros [[= <- <-] | [_ ?%Ht_dom]]; last done. eauto. + - done. + Qed. + + Lemma bor_interp_writeN_target_local σ_t σ_s (t : ptr_id) l scs scs' : + bor_interp σ_t σ_s -∗ + l ↦t∗[tk_local]{t} scs -∗ + t $$ tk_local -∗ + ⌜length scs' = length scs⌠==∗ + bor_interp (state_upd_mem (write_mem l scs') σ_t) σ_s ∗ + l ↦t∗[tk_local]{t} scs' ∗ + t $$ tk_local. + Proof. + iInduction scs' as [ | sc' scs'] "IH" forall (l scs). + - iIntros "Hbor Hp Ht %Hlen". destruct scs; last done. iFrame "Ht Hp". iModIntro. destruct σ_t; eauto. + - iIntros "Hbor Hp Ht %Hlen". destruct scs as [ | sc scs]; first done. + iPoseProof (big_sepL_cons with "Hp") as "[Hh Hp]". + iMod ("IH" $! (l +â‚— 1) scs with "Hbor [Hp] Ht []") as "(Hbor & Hp & Ht)". + { iApply (big_sepL_mono with "Hp"). intros i sc0 Hsc0. cbn. + rewrite shift_loc_assoc. replace (1 + i)%Z with (Z.of_nat $ S i) by lia. done. } + { cbn in Hlen. iPureIntro. lia. } + iMod (bor_interp_write_target_local _ _ _ _ _ sc' with "Hbor Hh Ht") as "(Hbor & Hh & Ht)". + iModIntro. iFrame "Ht". iSplitL "Hbor". + { rewrite state_upd_mem_compose. rewrite shift_loc_0_nat. by rewrite state_upd_write_mem_head. } + iApply big_sepL_cons. iFrame "Hh". iApply (big_sepL_mono with "Hp"). + intros i sc0 Hsc0. cbn. + rewrite shift_loc_assoc. replace (1 + i)%Z with (Z.of_nat $ S i) by lia. done. + Qed. + + Lemma bor_interp_writeN_source_local σ_t σ_s (t : ptr_id) l scs scs' : + bor_interp σ_t σ_s -∗ + l ↦s∗[tk_local]{t} scs -∗ + t $$ tk_local -∗ + ⌜length scs' = length scs⌠==∗ + bor_interp σ_t (state_upd_mem (write_mem l scs') σ_s) ∗ + l ↦s∗[tk_local]{t} scs' ∗ + t $$ tk_local. + Proof. + Admitted. + + (** TODO: write lemmas for protectors *) + + (** Dealloc lemmas *) + Lemma loc_controlled_dealloc_update σ l l' (bor : tag) n (α' : stacks) (t : ptr_id) (tk : tag_kind) sc : + memory_deallocated σ.(sst) σ.(scs) l bor n = Some α' → + state_wf σ → + (bor = Tagged t ∧ (∃ i:nat, l' = l +â‚— i ∧ (i < n)%nat) → tk = tk_pub) → + loc_controlled l' t tk sc σ → + loc_controlled l' t tk sc (mkState (free_mem l n σ.(shp)) α' σ.(scs) σ.(snp) σ.(snc)). + Proof. + intros Hdealloc Hwf Hpub Hcontrol Hpre. + destruct tk. + - (* public *) + destruct Hpre as (stk & pm & opro & Hstk & Hit & Hpm). simpl in *. + destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Hdealloc _ _ Hstk) as [Hneq Hstk']. + destruct Hcontrol as [Hown Hshp]. { exists stk, pm, opro. done. } + destruct Hown as (stk' & Hstk'' & Hsro). + split. + + simplify_eq. exists stk. done. + + destruct (free_mem_lookup_case l' l n σ.(shp)) as [(_ & ->) | (i & Hi & -> & _)]; first done. + specialize (Hneq i Hi). congruence. + - (* unique *) + destruct Hpre as (stk & pm & opro & Hstk & Hit & Hpm). simpl in *. + destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Hdealloc _ _ Hstk) as [Hneq Hstk']. + destruct Hcontrol as [Hown Hshp]. { exists stk, pm, opro. done. } + destruct Hown as (stk' & Hstk'' & (opro' & ? & ->)). + split. + + simplify_eq. exists stk. split; first done. rewrite Hstk' in Hstk''. + injection Hstk'' as ->. eauto. + + destruct (free_mem_lookup_case l' l n σ.(shp)) as [(_ & ->) | (i & Hi & -> & _)]; first done. + specialize (Hneq i Hi). congruence. + - (* local *) clear Hpre. destruct Hcontrol as [Hown Hshp]; first done. simpl. + destruct (free_mem_lookup_case l' l n σ.(shp)) as [(Hi & ->) | (i & Hi & -> & Hfree)]. + + split; last done. destruct (for_each_dealloc_lookup _ _ _ _ _ Hdealloc) as (_ & Heq). + rewrite Heq; done. + + exfalso. destruct (for_each_true_lookup_case_2 _ _ _ _ _ Hdealloc) as [Heq _]. + specialize (Heq _ Hi) as (stk & stk' & Hstk & Hstk' & Hd1). + rewrite Hown in Hstk. injection Hstk as <-. + destruct (dealloc1 _ _ _) eqn:Heq; [ | done]. + destruct (dealloc1_singleton_Some _ _ _ ltac:(eauto)) as (<- & _). + enough (tk_local = tk_pub) by congruence. apply Hpub. eauto. + Qed. + + + (** Retag *) + Lemma loc_controlled_retag_ref σ c l ot T mut α' rk i sc : + let nt := σ.(snp) in + let pk := RefPtr mut in + let tk := match mut with Mutable => tk_unq | Immutable => tk_pub end in + (if mut is Immutable then is_freeze T else True) → + retag σ.(sst) σ.(snp) σ.(scs) c l ot rk pk T = Some (Tagged nt, α', S σ.(snp)) → + (is_two_phase rk = false) → + (i < tsize T)%nat → + σ.(shp) !! (l +â‚— i) = Some sc → + loc_controlled (l +â‚— i) nt tk sc (mkState σ.(shp) α' σ.(scs) (S σ.(snp)) σ.(snc)). + Proof. + intros nt pk tk Hfreeze Hretag Hrk Hi Hsc Hpre. split; last done. + destruct mut. + * (* unique *) + destruct Hpre as (st & pm' & opro & Hst & Hit & Hpm'). exists st. split; first done. + rewrite /retag Hrk in Hretag. + have EqRT': + retag_ref σ.(sst) σ.(scs) σ.(snp) l ot T (UniqueRef false) (adding_protector rk c) = + Some (Tagged nt, α', S nt) by done. + destruct (tag_on_top_retag_ref_uniq _ _ _ _ _ _ _ _ _ _ EqRT' i ltac:(lia)) + as [pro1 Eqstk1]. rewrite Hst /= in Eqstk1. + clear -Eqstk1. destruct st as [|? stk1]; [done|]. + simpl in Eqstk1. simplify_eq. by exists pro1, stk1. + * (* shared *) + destruct Hpre as (stk' & pm' & pro & Eqstk' & In' & NDIS). simpl in Eqstk'. + exists stk'. split; [done|]. + have EqRT': + retag_ref σ.(sst) σ.(scs) σ.(snp) l ot T SharedRef (adding_protector rk c) = Some (Tagged nt, α', S nt) by done. + have HTOP := (tag_on_top_retag_ref_shr _ _ _ _ _ _ _ _ _ _ Hfreeze EqRT' i ltac:(lia)). + clear -HTOP Eqstk'. + apply tag_on_top_shr_active_SRO in HTOP as (?&?&?). by simplify_eq. + Qed. + + Lemma loc_controlled_retag_update σ c l l' t tk' ot T pk rk α' nt nxtp' sc : + state_wf σ → + retag σ.(sst) σ.(snp) σ.(scs) c l ot rk pk T = Some (nt, α', nxtp') → + (Tagged t = ot → tk' = tk_pub) → + (t < σ.(snp))%nat → + loc_controlled l' t tk' sc σ → + loc_controlled l' t tk' sc (mkState σ.(shp) α' σ.(scs) nxtp' σ.(snc)). + Proof. + intros Hwf Hretag Hneq Hlt Hcontrolled. + intros Hpre. destruct tk'. + * destruct Hpre as (stk' & pm' & pro & Eqstk' & In' & ND). + destruct (retag_item_in _ _ _ _ _ _ _ _ _ _ _ _ Hretag _ _ t _ Eqstk' In') + as (stk & Eqstk & In); [done..|]. + + destruct Hcontrolled as (Hown & Hl'). { simpl; naive_solver. } + cbn. split; last done. + exists stk'. split; [done|]. + destruct Hown as (stk1 & Eqstk1 & HTOP). + rewrite Eqstk1 in Eqstk. simplify_eq. + move : HTOP. + have ND2 := proj2 (state_wf_stack_item _ Hwf _ _ Eqstk1). + by apply (retag_item_active_SRO_preserving _ _ _ _ _ _ _ _ _ _ _ _ Hretag _ _ _ _ _ ND2 Eqstk1 Eqstk' In In'). + * destruct Hpre as (stk' & pm' & pro & Eqstk' & In' & ND). + destruct (retag_item_in _ _ _ _ _ _ _ _ _ _ _ _ Hretag _ _ t _ Eqstk' In') + as (stk & Eqstk & In); [done..|]. + destruct Hcontrolled as (Hown & Hl'); [simpl; naive_solver|]. + split; last done. cbn. + exists stk'. split; [done|]. + destruct Hown as (stk1 & Eqstk1 & opro1 & HTOP). + rewrite Eqstk1 in Eqstk. simplify_eq. + have ND2 := proj2 (state_wf_stack_item _ Hwf _ _ Eqstk1). + assert (opro1 = pro ∧ pm' = Unique) as []. + { have In1 : mkItem Unique (Tagged t) opro1 ∈ stk. + { destruct HTOP as [? HTOP]. rewrite HTOP. by left. } + have EQ := stack_item_tagged_NoDup_eq _ _ _ t ND2 In1 In eq_refl eq_refl. + by simplify_eq. } subst opro1 pm'. exists pro. + have NEq: Tagged t ≠ot. + { intros <-. specialize (Hneq eq_refl). congruence. } + move : HTOP. + by apply (retag_item_head_preserving _ _ _ _ _ _ _ _ _ _ _ _ Hretag + _ _ _ _ _ ND2 Eqstk1 Eqstk' NEq In'). + * clear Hpre. specialize (Hcontrolled I) as (Hown & Hl'). split; last done. + move : Hown. cbn. + have NEq: ot ≠Tagged t. + { intros ->. specialize (Hneq eq_refl). congruence. } + move : NEq. by eapply retag_Some_local. + Qed. + +End lemmas. + +(* accessing a local location is only possible with the same tag, retaining the same stack for the access *) +Lemma local_access_eq l t t' stk n stk' kind σ_s σ_t M_tag M_t M_s : + σ_t.(sst) !! l = Some stk → + access1 stk kind t' σ_t.(scs) = Some (n, stk') → + M_tag !! t = Some (tk_local, ()) → + is_Some (M_t !! (t, l)) → + tag_interp M_tag M_t M_s σ_t σ_s → + t' = Tagged t ∧ stk' = stk. +Proof. + intros Hst Haccess Htag Ht Htag_interp. + specialize (access1_in_stack _ _ _ _ _ _ Haccess) as (it & Hin_stack & <- & Henabled). + destruct Htag_interp as (Htag_interp & _ & _). + specialize (Htag_interp _ _ Htag) as (_ & _ & Htl & Hsl & Hdom). + destruct Ht as (sc_t & Ht). + specialize (Htl _ _ Ht) as Hcontrol. + apply loc_controlled_local in Hcontrol as (Hcontrol & _). + destruct (tag_unique_head_access σ_t.(scs) _ (Tagged t) None kind ltac:(by exists [])) as (n' & Hn). + move : Hst Hin_stack Haccess . + rewrite Hcontrol => [= <-]. rewrite elem_of_list_singleton => ->. + rewrite Hn => [= _ <-]. done. +Qed. + +Lemma protector_access_eq l t t' stk n stk' kind σ_s σ_t M_tag Mcall M_t M_s : + σ_t.(sst) !! l = Some stk → + access1 stk kind t' σ_t.(scs) = Some (n, stk') → + M_tag !! t = Some (tk_unq, ()) → + is_Some (M_t !! (t, l)) → + (∃ (c: call_id), call_set_in' Mcall c t l) → + tag_interp M_tag M_t M_s σ_t σ_s → + call_set_interp Mcall σ_t → + state_wf σ_t → + t' = Tagged t. +Proof. + intros Hst Haccess Htag Ht (c & Hcall) Htag_interp Hcall_interp Hwf. + specialize (call_set_interp_access _ _ _ _ _ Hcall_interp Hcall) as (Hc_in & _ & (stk'' & pm & Hstk'' & Hin & Hpm)). + destruct Htag_interp as (Htag_interp & _ & _). + specialize (Htag_interp _ _ Htag) as (_ & _ & Htl & Hsl & Hdom). + destruct Ht as (sc_t & Ht). + specialize (Htl _ _ Ht) as Hcontrol. + specialize (loc_controlled_unq _ _ _ _ _ Hcontrol Hstk'' ltac:(eauto)) as ((stk''' & opro & ->) & Hmem). + move : Hstk'' Hin Haccess. rewrite Hst => [= Heq]. move : Hst. rewrite Heq => Hst Hi. + have ->: opro = Some c. + { destruct (state_wf_stack_item _ Hwf _ _ Hst) as [_ ND]. + have [=] := stack_item_tagged_NoDup_eq _ _ _ t ND Hi ltac:(by left) eq_refl eq_refl. + done. + } + eapply access1_incompatible_head_protector; [by (eexists; eauto) | done]. +Qed. + +(* successfully accesses with a private location are only possible when the tag is equal *) +Lemma priv_loc_UB_access_eq l kind σ_s σ_t t t' stk M_tag M_t M_s Mcall : + σ_t.(sst) !! l = Some stk → + is_Some (access1 stk kind t' σ_t.(scs)) → + priv_loc M_tag M_t Mcall t l → + tag_interp M_tag M_t M_s σ_t σ_s → + call_set_interp Mcall σ_t → + state_wf σ_t → + t' = Tagged t. +Proof. + intros Hs ([? ?] & Haccess) Hpriv Htag_interp Hcall_interp Hwf. + destruct Hpriv as (tk & Htag & Ht & [-> | [-> Hc]]). + - by eapply local_access_eq. + - eapply protector_access_eq; done. +Qed. + +Definition untagged_or_public (M_tag : gmap ptr_id (tag_kind * unit)) t := + match t with + | Tagged t2 => M_tag !! t2 = Some (tk_pub, ()) + | Untagged => True + end. +Lemma priv_pub_access_UB l kind σ_s σ_t t t' stk M_tag Mcall M_t M_s : + σ_t.(sst) !! l = Some stk → + is_Some (access1 stk kind t' σ_t.(scs)) → + priv_loc M_tag M_t Mcall t l → + tag_interp M_tag M_t M_s σ_t σ_s → + call_set_interp Mcall σ_t → + state_wf σ_t → + untagged_or_public M_tag t' → + False. +Proof. + intros Hs Haccess Hpriv Htag_interp Hcall_interp Hwf. + rewrite (priv_loc_UB_access_eq _ _ _ _ _ _ _ _ _ _ _ Hs Haccess Hpriv Htag_interp Hcall_interp Hwf). + destruct Hpriv as (tk & Hl & _ & [-> | [-> _]]); cbn; intros; simplify_eq. +Qed. + +Lemma priv_loc_UB_retag_access_eq σ_s σ_t c l old new mut T kind α' nxtp' M_tag M_t M_s Mcall + (FRZ: if mut is Immutable then is_freeze T else True) + (N2P: kind ≠TwoPhase) : + retag σ_t.(sst) σ_t.(snp) σ_t.(scs) c l old kind (RefPtr mut) T = Some (new, α', nxtp') → + ∀ i t, (i < tsize T)%nat → + priv_loc M_tag M_t Mcall t (l +â‚— i) → + tag_interp M_tag M_t M_s σ_t σ_s → + call_set_interp Mcall σ_t → + state_wf σ_t → + untagged_or_public M_tag old → + False. +Proof. + intros Hrt i t Hi. + have NZST: (0 < tsize T)%nat by lia. + destruct (retag_change_ref_NZST _ _ _ _ _ _ _ _ _ _ _ _ NZST Hrt); + subst new nxtp'. + destruct (retag_Some_Ref _ _ _ _ _ _ _ _ _ _ _ _ NZST FRZ N2P Hrt _ Hi) + as (stk & stk' & Eqstk & Eqstk' & GR). + apply grant_access1 in GR; [|by destruct mut]. + revert Eqstk GR. by apply priv_pub_access_UB. +Qed. + + +(** TODO: these lemmas need a new home *) +Section lemmas. +Context `{!sborGS Σ}. +Implicit Types P Q : iProp Σ. +Implicit Types Φ : expr → expr → iProp Σ. +Implicit Types σ σ_s σ_t : state. +Implicit Types r r_s r_t : result. +Implicit Types l : loc. +Implicit Types f : fname. + +Context (Ω : result → result → iProp Σ). + + +Lemma memory_read_access1 (stks : stacks) l n t calls : + (∀ i: nat, (i < n)%nat → ∃ stk, stks !! (l +â‚— i) = Some stk ∧ ∃ m, access1 stk AccessRead (Tagged t) calls = Some (m, stk)) → + memory_read stks calls l (Tagged t) n = Some stks. +Proof. + induction n as [ | n IH]; cbn; first done. + intros Hacc1. destruct (Hacc1 n ltac:(lia)) as (stkn & Hl & (m & Hacc1_n)). rewrite Hl. + cbn. rewrite Hacc1_n. cbn. + rewrite insert_id; last done. apply IH. intros i Hi. apply Hacc1. lia. +Qed. + +Lemma bor_state_own_access1_read l t tk stk σ : + bor_state_own l t tk σ → + σ.(sst) !! l = Some stk → + ∃ n, access1 stk AccessRead (Tagged t) σ.(scs) = Some (n, stk). +Proof. + intros Hown. destruct tk; cbn in *. + - destruct Hown as (st & -> & Hsro). move => [= <-]. by apply tag_SRO_top_access. + - destruct Hown as (st & Hsst & (opro & st' & H)). simplify_eq. rewrite Hsst => [= <-]. + eapply tag_unique_head_access. eexists; eauto. + - rewrite Hown => [= <-]. + eapply tag_unique_head_access. eexists; eauto. +Qed. + + +End lemmas. + diff --git a/theories/stacked_borrows/logical_state.v b/theories/stacked_borrows/logical_state.v new file mode 100644 index 0000000000000000000000000000000000000000..227d622dfc48d10c07918ce894e47ba57d29a859 --- /dev/null +++ b/theories/stacked_borrows/logical_state.v @@ -0,0 +1,1003 @@ +(** This file provides the basic heap and ghost state support for the BorIngLang program logic. *) +From iris.proofmode Require Export tactics. +From iris.bi.lib Require Import fractional. +From iris.base_logic.lib Require Import ghost_map. +From simuliris.base_logic Require Export gen_sim_prog. +From simuliris.simulation Require Export slsls. +From simuliris.simulation Require Import lifting. +From iris.prelude Require Import options. +From simuliris.stacked_borrows Require Import tkmap_view. +From simuliris.stacked_borrows Require Export defs. +From simuliris.stacked_borrows Require Import steps_progress steps_retag. + +(** * BorLang ghost state *) +Class bor_stateGS Σ := { + (* Maintaining the locations protected by each call id *) + call_inG :> ghost_mapG Σ call_id (gmap ptr_id (gset loc)); + call_name : gname; + + (* tag ownership *) + tag_inG :> tkmapG Σ ptr_id unit; + tag_name : gname; + + (* A view of parts of the heap, conditional on the ptr_id *) + heap_view_inG :> ghost_mapG Σ (ptr_id * loc) scalar; + heap_view_source_name : gname; + heap_view_target_name : gname; + + (* Tainted tags: a set of tag * source location *) + tainted_tag_collection :> ghost_mapG Σ (ptr_id * loc) unit; + tainted_tags_name : gname; +}. + +Section state_bijection. + Context `{bor_stateGS Σ}. + + Context (sc_rel : scalar → scalar → iProp Σ). + + Section defs. + (* We need all the maps from the tag interpretation here.... + TODO: can we make that more beautiful? all the different invariants are interleaved in subtle ways, which makes modular reasoning really hard... *) + Context (M_tag : gmap ptr_id (tag_kind * unit)) (M_t M_s : gmap (ptr_id * loc) scalar) (Mcall_t : gmap call_id (gmap ptr_id (gset loc))). + + + Definition call_set_in (M : gmap ptr_id (gset loc)) t l := + ∃ L, M !! t = Some L ∧ l ∈ L. + Definition call_set_in' (M : gmap call_id (gmap ptr_id (gset loc))) c t l := + ∃ M', M !! c = Some M' ∧ call_set_in M' t l. + Definition pub_loc σ_t σ_s (l : loc) : iProp Σ := + ∀ sc_t, ⌜σ_t.(shp) !! l = Some sc_t⌠→ ∃ sc_s, ⌜σ_s.(shp) !! l = Some sc_s⌠∗ sc_rel sc_t sc_s. + Definition priv_loc t (l : loc) : Prop := + ∃ tk, M_tag !! t = Some (tk, tt) ∧ is_Some (M_t !! (t, l)) ∧ + (* local *) + (tk = tk_local ∨ + (* unique with protector *) + (tk = tk_unq ∧ ∃ c, call_set_in' Mcall_t c t l)). + + (* This definition enforces quite strict requirements on the state: + - the domains of the heaps shp are the same + - the stacks are the same + - the call counter is the same + - the tag counter is the same + - the set of ongoing calls is the same + - there's a relation on the scalars stored at locations ([pub_loc]), except when the location is currently controlled by a tag ([priv_loc]). + + Note that, while the definition may appear asymmetric in source and target, due to the well-formedness on states [state_wf] and the relation of the tag maps enforced below, it really is symmetric in practice. + *) + Definition state_rel σ_t σ_s : iProp Σ := + ⌜dom (gset loc) σ_s.(shp) = dom (gset loc) σ_t.(shp)⌠∗ + ⌜σ_s.(sst) = σ_t.(sst)⌠∗ + ⌜σ_s.(snp) = σ_t.(snp)⌠∗ + ⌜σ_s.(snc) = σ_t.(snc)⌠∗ + ⌜σ_s.(scs) = σ_t.(scs)⌠∗ + (* private / public locations of the target *) + ∀ l, ⌜is_Some (σ_t.(shp) !! l)⌠→ pub_loc σ_t σ_s l ∨ ⌜∃ t, priv_loc t lâŒ. + + Global Instance state_rel_persistent σ_t σ_s `{∀ sc_t sc_s, Persistent (sc_rel sc_t sc_s)} : + Persistent (state_rel σ_t σ_s). + Proof. intros. apply _. Qed. + End defs. +End state_bijection. + +Section bijection_lemmas. + Context `{bor_stateGS Σ}. + Context (sc_rel : scalar → scalar → iProp Σ). + Local Notation state_rel := (state_rel sc_rel). + + Lemma state_rel_get_pure Mtag Mt Mcall σ_t σ_s : + state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜σ_s.(sst) = σ_t.(sst) ∧ + σ_s.(snp) = σ_t.(snp) ∧ σ_s.(snc) = σ_t.(snc) ∧ σ_s.(scs) = σ_t.(scs)âŒ. + Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. + Lemma state_rel_stacks_eq Mtag Mt Mcall σ_t σ_s : + state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜σ_s.(sst) = σ_t.(sst)âŒ. + Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. + Lemma state_rel_snp_eq Mtag Mt Mcall σ_t σ_s : + state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜σ_s.(snp) = σ_t.(snp)âŒ. + Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. + Lemma state_rel_snc_eq Mtag Mt Mcall σ_t σ_s : + state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜σ_s.(snc) = σ_t.(snc)âŒ. + Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. + Lemma state_rel_calls_eq Mtag Mt Mcall σ_t σ_s : + state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜σ_s.(scs) = σ_t.(scs)âŒ. + Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. + Lemma state_rel_dom_eq Mtag Mt Mcall σ_t σ_s : + state_rel Mtag Mt Mcall σ_t σ_s -∗ ⌜dom (gset loc) σ_t.(shp) = dom (gset loc) σ_s.(shp)âŒ. + Proof. iIntros "(% & % & % & % & % & ?)". eauto. Qed. + + Lemma state_rel_upd_pub_both M_tag M_t Mcall_t σ_t σ_s l sc_t sc_s : + sc_rel sc_t sc_s -∗ + state_rel M_tag M_t Mcall_t σ_t σ_s -∗ + state_rel M_tag M_t Mcall_t (state_upd_mem (<[l := sc_t]>) σ_t) (state_upd_mem (<[l := sc_s]>) σ_s). + Proof. + iIntros "Hs (%Hshp & % & % & % & % & Hrel)". rewrite /state_rel /=. + iSplitR. { iPureIntro. by rewrite !dom_insert_L Hshp. } + do 4 (iSplitR; first done). + iIntros (l') "%Hsome". destruct (decide (l = l')) as [<- | Hneq]. + - iLeft. iIntros (sc_t') "%Hsc_t'". iExists sc_s. + iSplitR. { iPureIntro. by rewrite lookup_insert. } + move :Hsc_t'; rewrite lookup_insert => [= <-] //. + - rewrite lookup_insert_ne in Hsome; last done. + iDestruct ("Hrel" $! l' with "[//]") as "[Hpub | Hpriv]". + + iLeft. iIntros (sc_t'). rewrite !lookup_insert_ne; [ | done | done]. iApply "Hpub". + + iRight. done. + Qed. + + Lemma priv_loc_upd_insert Mtag Mt Mcall t l t' l' sc : + priv_loc Mtag Mt Mcall t l → + priv_loc Mtag (<[(t',l') := sc]> Mt) Mcall t l. + Proof. + rewrite /priv_loc. intros (tk & Ht & Hs & Hinv). exists tk. + split_and!; [ done | | done]. + apply lookup_insert_is_Some. destruct (decide ((t', l') = (t, l))); eauto. + Qed. + + Lemma state_rel_upd_priv_target M_tag M_t Mcall σ_t σ_s l t sc : + is_Some (σ_t.(shp) !! l) → + priv_loc M_tag M_t Mcall t l → + state_rel M_tag M_t Mcall σ_t σ_s -∗ + state_rel M_tag (<[(t, l) := sc]> M_t) Mcall (state_upd_mem (<[l := sc]>) σ_t) σ_s. + Proof. + iIntros (Hs Hpriv) "(%Hshp & % & % & % & % & Hrel)". rewrite /state_rel /=. + iSplitR. { iPureIntro. rewrite dom_insert_lookup_L; done. } + do 4 (iSplitR; first done). + iIntros (l') "%Hsome". destruct (decide (l = l')) as [<- | Hneq]. + - iRight. iExists t. iPureIntro. apply priv_loc_upd_insert. done. + - rewrite lookup_insert_ne in Hsome; last done. + iDestruct ("Hrel" $! l' with "[//]") as "[Hpub | %Hpriv']". + + iLeft. iIntros (sc_t'). rewrite !lookup_insert_ne; [ | done ]. iApply "Hpub". + + iRight. iPureIntro. destruct Hpriv' as (t' & Hpriv'). exists t'. + by eapply priv_loc_upd_insert. + Qed. + + Lemma state_rel_upd_priv_source M_tag M_t Mcall σ_t σ_s l t sc : + ⌜is_Some (σ_t.(shp) !! l)⌠-∗ + ⌜priv_loc M_tag M_t Mcall t l⌠-∗ + state_rel M_tag M_t Mcall σ_t σ_s -∗ + state_rel M_tag M_t Mcall σ_t (state_upd_mem (<[l := sc]>) σ_s). + Proof. + iIntros (Hs Hpriv) "(%Hshp & % & % & % & % & Hrel)". rewrite /state_rel /=. + iSplitR. { iPureIntro. rewrite dom_insert_lookup_L; [ by rewrite Hshp| ]. + rewrite lookup_lookup_total_dom; first by eauto. + rewrite Hshp. by apply elem_of_dom. + } + do 4 (iSplitR; first done). + iIntros (l') "%Hsome". destruct (decide (l = l')) as [<- | Hneq]. + - iRight. iExists t. done. + - iDestruct ("Hrel" $! l' with "[//]") as "[Hpub | %Hpriv']". + + iLeft. iIntros (sc_t'). rewrite !lookup_insert_ne; [ | done ]. iApply "Hpub". + + iRight. iPureIntro. destruct Hpriv' as (t' & Hpriv'). exists t'. done. + Qed. + + Lemma state_rel_pub_if_not_priv M_tag M_t Mcall σ_t σ_s l : + ⌜is_Some (σ_t.(shp) !! l)⌠-∗ + state_rel M_tag M_t Mcall σ_t σ_s -∗ + ⌜∀ t, ¬ priv_loc M_tag M_t Mcall t l⌠-∗ + pub_loc sc_rel σ_t σ_s l. + Proof. + iIntros (Hs) "(%& % & % & % & % & Hrel) %Hnpriv". + iPoseProof ("Hrel" $! l with "[//]") as "[Hpub | %Hpriv]"; first done. + destruct Hpriv as (t & Hpriv). exfalso; by eapply Hnpriv. + Qed. + + Lemma state_rel_heap_lookup_Some M_tag M_t Mcall σ_t σ_s : + state_rel M_tag M_t Mcall σ_t σ_s -∗ + ∀ l, ⌜is_Some (σ_t.(shp) !! l)⌠↔ ⌜is_Some (σ_s.(shp) !! l)âŒ. + Proof. + iIntros "(%Hshp & _)". iPureIntro. move => l. cbn. by rewrite -!elem_of_dom Hshp. + Qed. + + Lemma state_rel_pub_or_priv M_tag M_t Mcall σ_t σ_s l : + ⌜is_Some (σ_t.(shp) !! l)⌠-∗ + state_rel M_tag M_t Mcall σ_t σ_s -∗ + pub_loc sc_rel σ_t σ_s l ∨ ⌜∃ t, priv_loc M_tag M_t Mcall t lâŒ. + Proof. + iIntros "Hsome Hstate". iDestruct "Hstate" as "(_ & _ & _ & _ & _ & Hl)". + by iApply "Hl". + Qed. + + Lemma pub_loc_lookup σ_t σ_s l : + ⌜is_Some (σ_t.(shp) !! l)⌠-∗ + pub_loc sc_rel σ_t σ_s l -∗ + ∃ sc_t sc_s, ⌜σ_t.(shp) !! l = Some sc_t ∧ σ_s.(shp) !! l = Some sc_s⌠∗ sc_rel sc_t sc_s. + Proof. + iIntros (Hs) "Hpub". destruct Hs as (sc_t & Ht). + iDestruct ("Hpub" $! sc_t with "[//]") as (sc_s) "[%Hs Hsc]". + iExists sc_t, sc_s. eauto. + Qed. + +End bijection_lemmas. + +(** Interpretation for call ids *) +Section call_defs. + Context {Σ} (call_gname : gname) {call_inG : ghost_mapG Σ (call_id) (gmap ptr_id (gset loc))}. + + Implicit Types (c : call_id) (pid : ptr_id) (pm : permission). + + Definition call_set_is (c : call_id) (M : gmap ptr_id (gset loc)) := + ghost_map_elem call_gname c (DfracOwn 1) M. + + (* This does not assert ownership of the authoritative part. Instead, this is owned by bor_interp below. *) + Definition call_set_interp (M : gmap call_id (gmap ptr_id (gset loc))) (σ : state) : Prop := + ∀ c (M' : gmap ptr_id (gset loc)), M !! c = Some M' → + c ∈ σ.(scs) ∧ + (* for every ptr_id *) + ∀ t (L : gset loc), M' !! t = Some L → + (t < σ.(snp))%nat ∧ + (* for every protected location [l], there needs to be a protector in the stack *) + ∀ (l : loc), l ∈ L → ∃ s pm, σ.(sst) !! l = Some s ∧ + mkItem pm (Tagged t) (Some c) ∈ s ∧ pm ≠Disabled. + + Definition loc_protected_by σ t l c := + c ∈ σ.(scs) ∧ (t < σ.(snp))%nat ∧ ∃ stk pm, σ.(sst) !! l = Some stk ∧ + mkItem pm (Tagged t) (Some c) ∈ stk ∧ pm ≠Disabled. + Lemma call_set_interp_access M σ c t l : + call_set_interp M σ → + call_set_in' M c t l → + loc_protected_by σ t l c. + Proof. + intros Hinterp (M' & HM_some & L & HM'_some & Hin). + specialize (Hinterp _ _ HM_some) as (? & Hinterp). + specialize (Hinterp _ _ HM'_some) as (? & Hinterp). + specialize (Hinterp _ Hin). done. + Qed. + + Lemma call_set_interp_remove c M σ : + call_set_interp M σ → + call_set_interp (delete c M) (state_upd_calls (.∖ {[c]}) σ). + Proof. + intros Hinterp c' M' Hsome. destruct (decide (c' = c)) as [-> | Hneq]. + { rewrite lookup_delete in Hsome. done. } + rewrite lookup_delete_ne in Hsome; last done. + apply Hinterp in Hsome as (Hin & Hpid). + split. + { destruct σ; cbn in *. apply elem_of_difference; split; first done. by apply not_elem_of_singleton. } + intros t S HS. + apply Hpid in HS as (Ht & Hlookup). split; first by destruct σ. + intros l Hl. apply Hlookup in Hl as (s & pm & Hsst & Hs & Hpm). + exists s, pm. split_and!; [ | done..]. by destruct σ. + Qed. +End call_defs. + +Notation "c '@@' M" := (call_set_is call_name c M) (at level 50). + + +(** Interpretation for heap assertions under control of tags. + The interpretation of the tag map and the "heap view" fragments are interlinked. + *) +Section heap_defs. + (** The assumption on the location still being valid for tag [t], i.e., [t] not being disabled. *) + (* Note: That the stack is still there needs to be part of the precondition [bor_state_pre]. + Otherwise, we will not be able to prove reflexivity for deallocation: + that needs to be able to remove stacks from the state without updating all the ghost state that may still make assumptions about it. + *) + Definition bor_state_pre (l : loc) (t : ptr_id) (tk : tag_kind) (σ : state) := + match tk with + | tk_local => True + | _ => ∃ st pm pro, σ.(sst) !! l = Some st ∧ + mkItem pm (Tagged t) pro ∈ st ∧ pm ≠Disabled + end. + + Lemma loc_protected_bor_state_pre l t c σ tk : + loc_protected_by σ t l c → bor_state_pre l t tk σ. + Proof. + intros (_ & _ & (stk & pm & ?)). destruct tk; [| | done]; rewrite /bor_state_pre; eauto. + Qed. + + Definition bor_state_own (l : loc) (t : ptr_id) (tk : tag_kind) (σ : state) := + match tk with + | tk_local => σ.(sst) !! l = Some ([mkItem Unique (Tagged t) None]) + | tk_unq => ∃ st, σ.(sst) !! l = Some st ∧ ∃ opro st', + st = mkItem Unique (Tagged t) opro :: st' + | tk_pub => ∃ st, σ.(sst) !! l = Some st ∧ t ∈ active_SRO st + end. + + Lemma bor_state_own_some_stack l t tk σ : + bor_state_own l t tk σ → ∃ stk, σ.(sst) !! l = Some stk. + Proof. rewrite /bor_state_own. destruct tk; naive_solver. Qed. + + (** Location [l] is controlled by tag [t] at kind [tk] with scalar [sc]. *) + Definition loc_controlled (l : loc) (t : ptr_id) (tk : tag_kind) (sc : scalar) (σ : state) := + (bor_state_pre l t tk σ → bor_state_own l t tk σ ∧ σ.(shp) !! l = Some sc). + + Lemma loc_controlled_local l t sc σ : + loc_controlled l t tk_local sc σ → + σ.(sst) !! l = Some [mkItem Unique (Tagged t) None] ∧ + σ.(shp) !! l = Some sc. + Proof. intros Him. specialize (Him I) as (Hbor & Hmem). split;done. Qed. + + Lemma loc_controlled_unq l t sc s σ : + loc_controlled l t tk_unq sc σ → + σ.(sst) !! l = Some s → + (∃ pm opro, mkItem pm (Tagged t) opro ∈ s ∧ pm ≠Disabled) → + (∃ s' op, s = (mkItem Unique (Tagged t) op) :: s') ∧ + σ.(shp) !! l = Some sc. + Proof. + intros Him Hstk (pm & opro & Hpm). + edestruct Him as (Hown & ?). { rewrite /bor_state_pre. eauto. } + split; last done. + destruct Hown as (st' & opro' & st'' & Hst' & ->). simplify_eq. eauto. + Qed. + + Lemma loc_controlled_pub l t sc σ s : + loc_controlled l t tk_pub sc σ → + σ.(sst) !! l = Some s → + (∃ pm opro, mkItem pm (Tagged t) opro ∈ s ∧ pm ≠Disabled) → + t ∈ active_SRO s ∧ + σ.(shp) !! l = Some sc. + Proof. + intros Him Hst (pm & opro & Hin & Hpm). + edestruct Him as (Hown & ?). { rewrite /bor_state_pre; eauto 8. } + split; last done. destruct Hown as (st' & Hst' & Hsro). + simplify_eq. eauto. + Qed. + + Lemma loc_controlled_mem_insert_ne l l' t tk sc sc' σ : + l ≠l' → + loc_controlled l t tk sc σ → + loc_controlled l t tk sc (state_upd_mem <[l' := sc']> σ). + Proof. + intros Hneq Him Hpre. + apply Him in Hpre as [Hown Hmem]. split; first done. + rewrite lookup_insert_ne; done. + Qed. + Lemma loc_controlled_mem_insert l t tk sc sc' σ : + loc_controlled l t tk sc σ → + loc_controlled l t tk sc' (state_upd_mem <[l := sc']> σ). + Proof. + intros Him Hpre. apply Him in Hpre as [Hown Hmem]. split; first done. + rewrite lookup_insert; done. + Qed. + + Section local. + (** Facts about local tags *) + Lemma loc_controlled_local_unique l t t' sc sc' σ : + loc_controlled l t tk_local sc σ → + loc_controlled l t' tk_local sc' σ → + t' = t ∧ sc' = sc. + Proof. + intros Hcontrol Hcontrol'. specialize (Hcontrol I) as [Hown Hmem]. + specialize (Hcontrol' I) as [Hown' Hmem']. + split; last by simplify_eq. + move : Hown Hown'. rewrite /bor_state_own // => -> [=] //. + Qed. + + Lemma loc_controlled_local_pre l t t' tk' sc σ : + loc_controlled l t tk_local sc σ → + bor_state_pre l t' tk' σ → + tk' = tk_local ∨ t' = t. + Proof. + intros [Heq _]%loc_controlled_local. + destruct tk'; last by eauto. + - intros (st' & pm & opro & Hst & Hin & Hpm). + move : Hst Hin. rewrite Heq. + move => [= <-] /elem_of_list_singleton [=]; eauto. + - intros (st' & pm & opro & Hst & Hin & Hpm). + move : Hst Hin. rewrite Heq. + move => [= <-] /elem_of_list_singleton [=]; eauto. + Qed. + Lemma loc_controlled_local_own l t t' tk' sc σ : + loc_controlled l t tk_local sc σ → + bor_state_own l t' tk' σ → + (tk' = tk_unq ∨ tk' = tk_local) ∧ t = t'. + Proof. + intros [Heq _]%loc_controlled_local. destruct tk'. + - move => [st' []]. rewrite Heq => [= <-] //. + - move => [st' [Heq' [opro [st'' ]]]]. move : Heq'. rewrite Heq => [= <-] [= ->] //; eauto. + - rewrite /bor_state_own Heq => [=]; eauto. + Qed. + + (* having local ownership of a location is authoritative, in the sense that we can update memory without hurting other tags that control this location. *) + Lemma loc_controlled_local_authoritative l t t' tk' sc sc' σ f : + loc_controlled l t tk_local sc (state_upd_mem f σ) → + loc_controlled l t' tk' sc' σ → + t ≠t' → + loc_controlled l t' tk' sc' (state_upd_mem f σ). + Proof. + intros Hcontrol Hcontrol' Hneq [Hown Hmem]%Hcontrol'. split; first done. + by edestruct (loc_controlled_local_own l t t' tk' sc (state_upd_mem f σ)) as [_ <-]. + Qed. + End local. + + (** Domain agreement for the two heap views for source and target *) + Definition dom_agree_on_tag (M_t M_s : gmap (ptr_id * loc) scalar) (t : ptr_id) := + (∀ l, is_Some (M_t !! (t, l)) → is_Some (M_s !! (t, l))) ∧ + (∀ l, is_Some (M_s !! (t, l)) → is_Some (M_t !! (t, l))). + + Lemma dom_agree_on_tag_upd_ne_target M_t M_s t t' l sc : + t ≠t' → + dom_agree_on_tag M_t M_s t' → + dom_agree_on_tag (<[(t, l) := sc]> M_t) M_s t'. + Proof. + intros Hneq [Htgt Hsrc]. split => l'' Hsome. + - apply Htgt. move : Hsome. rewrite lookup_insert_is_Some. by intros [[= -> <-] | [_ ?]]. + - apply lookup_insert_is_Some. right. split; first congruence. by apply Hsrc. + Qed. + Lemma dom_agree_on_tag_upd_ne_source M_t M_s t t' l sc : + t ≠t' → + dom_agree_on_tag M_t M_s t' → + dom_agree_on_tag M_t (<[(t, l) := sc]> M_s) t'. + Proof. + intros Hneq [Htgt Hsrc]. split => l'' Hsome. + - apply lookup_insert_is_Some. right. split; first congruence. by apply Htgt. + - apply Hsrc. move : Hsome. rewrite lookup_insert_is_Some. by intros [[= -> <-] | [_ ?]]. + Qed. + Lemma dom_agree_on_tag_upd_target M_t M_s t l sc : + is_Some (M_t !! (t, l)) → + dom_agree_on_tag M_t M_s t → + dom_agree_on_tag (<[(t, l) := sc]> M_t) M_s t. + Proof. + intros Hs [Htgt Hsrc]. split => l''. + - rewrite lookup_insert_is_Some. intros [[= <-] | [_ ?]]; by apply Htgt. + - intros Hsome. rewrite lookup_insert_is_Some'. right; by apply Hsrc. + Qed. + Lemma dom_agree_on_tag_upd_source M_t M_s t l sc : + is_Some (M_s !! (t, l)) → + dom_agree_on_tag M_t M_s t → + dom_agree_on_tag M_t (<[(t, l) := sc]> M_s) t. + Proof. + intros Hs [Htgt Hsrc]. split => l''. + - intros Hsome. rewrite lookup_insert_is_Some'. right; by apply Htgt. + - rewrite lookup_insert_is_Some. intros [[= <-] | [_ ?]]; by apply Hsrc. + Qed. + Lemma dom_agree_on_tag_lookup_target M_t M_s t l : + dom_agree_on_tag M_t M_s t → is_Some (M_t !! (t, l)) → is_Some (M_s !! (t, l)). + Proof. intros Hag Hsome. apply Hag, Hsome. Qed. + Lemma dom_agree_on_tag_lookup_source M_t M_s t l : + dom_agree_on_tag M_t M_s t → is_Some (M_s !! (t, l)) → is_Some (M_t !! (t, l)). + Proof. intros Hag Hsome. apply Hag, Hsome. Qed. + + Lemma dom_agree_on_tag_not_elem M_t M_s t : + (∀ l, M_t !! (t, l) = None) → (∀ l, M_s !! (t, l) = None) → + dom_agree_on_tag M_t M_s t. + Proof. intros Ht Hs. split; intros l; rewrite Ht Hs; congruence. Qed. + + (* TODO: move somewhere? *) + Lemma lookup_difference_is_Some `{Countable K} (V : Type) (M1 M2 : gmap K V) (k : K) : + is_Some ((M1 ∖ M2) !! k) ↔ is_Some (M1 !! k) ∧ M2 !! k = None. + Proof. rewrite /is_Some. setoid_rewrite lookup_difference_Some. naive_solver. Qed. + + Lemma dom_agree_on_tag_difference M1_t M1_s M2_t M2_s t : + dom_agree_on_tag M1_t M1_s t → dom_agree_on_tag M2_t M2_s t → + dom_agree_on_tag (M1_t ∖ M2_t) (M1_s ∖ M2_s) t. + Proof. + intros [H1a H1b] [H2a H2b]. split; intros l. + all: rewrite !lookup_difference_is_Some !eq_None_not_Some; naive_solver. + Qed. + + (* TODO: move? *) + Lemma lookup_union_Some_l' `{EqDecision K} `{Countable K} V (M1 M2 : gmap K V) (k : K) (v : V) : + (M1 ∪ M2) !! k = Some v → M2 !! k = None → M1 !! k = Some v. + Proof. + destruct (M1 !! k) as [ v' | ] eqn:Hv'. + - specialize (lookup_union_Some_l M1 M2 _ _ Hv') as ->. move => [= ->]. done. + - rewrite lookup_union_r; last done. congruence. + Qed. + (* TODO: move? *) + Lemma lookup_union_is_Some `{EqDecision K} `{Countable K} V (M1 M2 : gmap K V) (k : K) : + is_Some ((M1 ∪ M2) !! k) ↔ is_Some (M1 !! k) ∨ is_Some (M2 !! k). + Proof. + split. + - intros (v & Hv). destruct (M1 !! k) eqn:HM1; first by eauto. + right. erewrite <-lookup_union_r; eauto. + - intros [(v & HM1) | (v & HM2)]. + + rewrite (lookup_union_Some_l _ _ _ _ HM1); eauto. + + destruct (M1 !! k) eqn:HM1. { rewrite (lookup_union_Some_l _ _ _ _ HM1); eauto. } + rewrite lookup_union_r; eauto. + Qed. + + Lemma dom_agree_on_tag_union M1_t M1_s M2_t M2_s t : + dom_agree_on_tag M1_t M1_s t → dom_agree_on_tag M2_t M2_s t → + dom_agree_on_tag (M1_t ∪ M2_t) (M1_s ∪ M2_s) t. + Proof. + intros [H1a H1b] [H2a H2b]. split; intros l; rewrite !lookup_union_is_Some; naive_solver. + Qed. + + + (** The main interpretation for tags *) + Definition tag_interp (M : gmap ptr_id (tag_kind * unit)) (M_t M_s : gmap (ptr_id * loc) scalar) σ_t σ_s : Prop := + (∀ (t : ptr_id) tk, M !! t = Some (tk, ()) → + (* tags are valid *) + (t < σ_t.(snp))%nat ∧ (t < σ_s.(snp))%nat ∧ + (* at all locations, the values agree, and match the physical state assuming the tag currently has control over the location *) + (∀ l sc_t, M_t !! (t, l) = Some sc_t → loc_controlled l t tk sc_t σ_t) ∧ + (∀ l sc_s, M_s !! (t, l) = Some sc_s → loc_controlled l t tk sc_s σ_s) ∧ + dom_agree_on_tag M_t M_s t) ∧ + (∀ (t : ptr_id) (l : loc), is_Some (M_t !! (t, l)) → is_Some (M !! t)) ∧ + (∀ (t : ptr_id) (l : loc), is_Some (M_s !! (t, l)) → is_Some (M !! t)). +End heap_defs. + + +Notation "p '$$' tk" := (tkmap_elem tag_name p tk ()) (at level 50). + +Definition tk_to_frac (tk : tag_kind) := + match tk with + | tk_pub => DfracDiscarded + | _ => DfracOwn 1 + end. +Notation "l '↦t[' tk ']{' t } sc" := (ghost_map_elem heap_view_target_name (t, l) (tk_to_frac tk) sc) + (at level 20, format "l ↦t[ tk ]{ t } sc") : bi_scope. +Notation "l '↦s[' tk ']{' t } sc" := (ghost_map_elem heap_view_source_name (t, l) (tk_to_frac tk) sc) + (at level 20, format "l ↦s[ tk ]{ t } sc") : bi_scope. + + +Section tainted_tags. + Context `{bor_stateGS Σ}. + (** Interpretation for tainted tags. + A tag [t] is tainted for a location [l] when invariantly, the stack for [l] can never contain + an item tagged with [t] again. *) + + Definition tag_tainted_for (t : ptr_id) (l : loc) := + ghost_map_elem tainted_tags_name (t, l) DfracDiscarded tt. + (* tag [t] is not in [l]'s stack, and can never be in that stack again *) + Definition tag_tainted_interp (σ_s : state) : iProp Σ := + ∃ (M : gmap (ptr_id * loc) unit), ghost_map_auth tainted_tags_name 1 M ∗ + ∀ (t : ptr_id) (l : loc), ⌜is_Some (M !! (t, l))⌠-∗ + ⌜(t < σ_s.(snp))%nat⌠∗ + (* we have a persistent element here to remove sideconditions from the insert lemma *) + tag_tainted_for t l ∗ + ⌜∀ (stk : stack) (it : item), σ_s.(sst) !! l = Some stk → it ∈ stk → + tg it ≠Tagged t ∨ perm it = DisabledâŒ. + + (* the result of a read in the target: either the tag was invalid, and it now must be invalid for the source, too, + or the result [v_t'] agrees with what we expected to get ([v_t]). *) + Definition deferred_read (v_t v_t' : value) l t : iProp Σ := + (∃ i : nat, ⌜(i < length v_t)%nat ∧ length v_t = length v_t'⌠∗ tag_tainted_for t (l +â‚— i)) ∨ ⌜v_t' = v_tâŒ. + + Lemma tag_tainted_interp_insert σ_s t l : + (t < σ_s.(snp))%nat → + (∀ (stk : stack) (it : item), σ_s.(sst) !! l = Some stk → it ∈ stk → tg it ≠Tagged t ∨ perm it = Disabled) → + tag_tainted_interp σ_s ==∗ + tag_tainted_interp σ_s ∗ tag_tainted_for t l. + Proof. + iIntros (Ht Hnot_in) "(%M & Hauth & #Hinterp)". + destruct (M !! (t, l)) as [[] | ] eqn:Hlookup. + - iModIntro. iPoseProof ("Hinterp" $! t l with "[]") as "(_ & $ & _)"; first by eauto. + iExists M. iFrame "Hauth Hinterp". + - iMod (ghost_map_insert (t, l) () Hlookup with "Hauth") as "[Hauth He]". + iMod (ghost_map_elem_persist with "He") as "#He". iFrame "He". + iModIntro. iExists (<[(t, l) := ()]> M). iFrame "Hauth". + iIntros (t' l' [[= <- <-] | [Hneq Hsome]]%lookup_insert_is_Some). + { iFrame "He". eauto. } + iApply "Hinterp". done. + Qed. + + Lemma tag_tainted_interp_lookup σ_s t l : + tag_tainted_for t l -∗ + tag_tainted_interp σ_s -∗ + ⌜(t < σ_s.(snp))%nat⌠∗ + ⌜∀ (stk : stack) (it : item), σ_s.(sst) !! l = Some stk → it ∈ stk → tg it ≠Tagged t ∨ perm it = DisabledâŒ. + Proof. + iIntros "Helem (%M & Hauth & Hinterp)". + iPoseProof (ghost_map_lookup with "Hauth Helem") as "%Hlookup". + iPoseProof ("Hinterp" $! t l with "[]") as "(% & _ & %)"; by eauto. + Qed. + + Definition is_fresh_tag σ tg := + match tg with + | Untagged => True + | Tagged t => σ.(snp) ≤ t + end. + Lemma tag_tainted_interp_preserve σ_s σ_s' : + σ_s'.(snp) ≥ σ_s.(snp) → + (∀ l stk', σ_s'.(sst) !! l = Some stk' → ∀ it, it ∈ stk' → + is_fresh_tag σ_s it.(tg) ∨ it.(perm) = Disabled ∨ + ∃ stk, σ_s.(sst) !! l = Some stk ∧ it ∈ stk) → + tag_tainted_interp σ_s -∗ tag_tainted_interp σ_s'. + Proof. + iIntros (Hge Hupd) "(%M & Hauth & Hinterp)". + iExists M. iFrame "Hauth". iIntros (t l Hsome). + iDestruct ("Hinterp" $! t l with "[//]") as "(%Hlt & $ & %Hsst)". + iSplit; iPureIntro; first lia. + intros stk' it Hstk' Hit. + specialize (Hupd _ _ Hstk' _ Hit) as [Hfresh | [Hdisabled | (stk & Hstk & Hit')]]. + - left. destruct (tg it) as [t' | ]; last done. intros [= ->]. + simpl in Hfresh. lia. + - right; done. + - eapply Hsst; done. + Qed. + + Lemma tag_tainted_interp_tagged_sublist σ_s σ_s' : + σ_s'.(snp) ≥ σ_s.(snp) → + (∀ l stk', σ_s'.(sst) !! l = Some stk' → + ∃ stk, σ_s.(sst) !! l = Some stk ∧ + tagged_sublist stk' stk) → + tag_tainted_interp σ_s -∗ tag_tainted_interp σ_s'. + Proof. + iIntros (Hge Hupd). iApply tag_tainted_interp_preserve; first done. + intros l stk' Hstk' it Hit. + destruct (Hupd _ _ Hstk') as (stk & Hstk & Hsubl). + destruct (Hsubl _ Hit) as (it' & Hit' & Htg & Hprot & Hperm). + destruct (decide (perm it = Disabled)) as [ | Hperm'%Hperm]; first by eauto. + right; right. exists stk. split; first done. + destruct it, it'; simpl in *; simplify_eq. done. + Qed. + + Lemma tag_tainted_interp_retag σ_s c l old rk pk T new α' nxtp' : + retag σ_s.(sst) σ_s.(snp) σ_s.(scs) c l old rk pk T = Some (new, α', nxtp') → + tag_tainted_interp σ_s -∗ tag_tainted_interp (mkState σ_s.(shp) α' σ_s.(scs) nxtp' σ_s.(snc)). + Proof. + iIntros (Hretag). + iApply (tag_tainted_interp_preserve); simpl. + { specialize (retag_change_nxtp _ _ _ _ _ _ _ _ _ _ _ _ Hretag). lia. } + intros l' stk' Hstk' it Hit. + specialize (retag_item_in _ _ _ _ _ _ _ _ _ _ _ _ Hretag l' stk') as Ht. + destruct (decide (perm it = Disabled)) as [Hdisabled | Hndisabled]; first by eauto. + destruct (tg it) as [t | ] eqn:Htg; last by (left; done). + destruct (decide (t < σ_s.(snp))%nat) as [Hlt | Hnlt]. + - right; right. eapply (Ht t it); done. + - left. simpl. lia. + Qed. + + Lemma tag_tainted_interp_alloc σ l n : + let nt := Tagged σ.(snp) in + tag_tainted_interp σ -∗ tag_tainted_interp (mkState (init_mem l n σ.(shp)) (init_stacks σ.(sst) l n nt) σ.(scs) (S σ.(snp)) σ.(snc)). + Proof. + intros nt. iIntros "Htainted". + iApply (tag_tainted_interp_preserve σ with "Htainted"). { simpl. lia. } + intros l' stk' Hstk' it Hit. + specialize (init_stacks_lookup_case _ _ _ _ _ _ Hstk') as [(Hstk'' & Hi) | (i & Hi & ->)]. + + right. right. eauto. + + left. simpl. move : Hstk'. rewrite (proj1 (init_stacks_lookup _ _ _ _)); last done. + intros [= <-]. move : Hit. rewrite elem_of_list_singleton => -> /=. lia. + Qed. +End tainted_tags. + + +Section state_interp. + Context `{bor_stateGS Σ} (sc_rel : scalar → scalar → iProp Σ). + (** The main combined interpretation for the borrow semantics *) + + (* Ownership of the authoritative parts. *) + Definition bor_auth (M_call : gmap call_id (gmap ptr_id (gset loc))) (M_tag : gmap ptr_id (tag_kind * unit)) (M_t M_s : gmap (ptr_id * loc) scalar) : iProp Σ := + ghost_map_auth call_name 1 M_call ∗ + tkmap_auth tag_name 1 M_tag ∗ + ghost_map_auth heap_view_target_name 1 M_t ∗ + ghost_map_auth heap_view_source_name 1 M_s. + + Definition bor_interp (σ_t : state) (σ_s : state) : iProp Σ := + (* since multiple parts of the interpretation need access to these maps, + we own the authoritative parts here and not in the interpretations below *) + ∃ (M_call : gmap call_id (gmap ptr_id (gset loc))) + (M_tag : gmap ptr_id (tag_kind * unit)) + (M_t M_s : gmap (ptr_id * loc) scalar), + bor_auth M_call M_tag M_t M_s ∗ + + tag_tainted_interp σ_s ∗ + + state_rel sc_rel M_tag M_t M_call σ_t σ_s ∗ + (* due to the [state_rel], enforcing this on [σ_t] also does the same for [σ_s] *) + ⌜call_set_interp M_call σ_t⌠∗ + ⌜tag_interp M_tag M_t M_s σ_t σ_s⌠∗ + + ⌜state_wf σ_s⌠∗ + ⌜state_wf σ_tâŒ. + + Lemma bor_interp_get_pure σ_t σ_s : + bor_interp σ_t σ_s -∗ ⌜σ_s.(sst) = σ_t.(sst) ∧ σ_s.(snp) = σ_t.(snp) ∧ + σ_s.(snc) = σ_t.(snc) ∧ σ_s.(scs) = σ_t.(scs) ∧ state_wf σ_s ∧ state_wf σ_t ∧ + dom (gset loc) σ_s.(shp) = dom (gset loc) σ_t.(shp)âŒ. + Proof. + iIntros "(% & % & % & % & ? & _ & Hstate & _ & _ & % & %)". + iPoseProof (state_rel_get_pure with "Hstate") as "%". + iPoseProof (state_rel_dom_eq with "Hstate") as "<-". + iPureIntro. tauto. + Qed. + + Lemma bor_interp_get_state_wf σ_t σ_s : + bor_interp σ_t σ_s -∗ + ⌜state_wf σ_t⌠∗ ⌜state_wf σ_sâŒ. + Proof. iIntros "(% & % & % & % & ? & ? & Hstate & _ & _ & % & %)". eauto. Qed. + +End state_interp. + + +(** Array generalizes pointsto connectives to lists of scalars *) +Definition array_tag `{!bor_stateGS Σ} γh (t : ptr_id) (l : loc) (dq : dfrac) (scs : list scalar) : iProp Σ := + ([∗ list] i ↦ sc ∈ scs, ghost_map_elem γh (t, l +â‚— i) dq sc)%I. +Notation "l '↦t∗[' tk ']{' t } scs" := (array_tag heap_view_target_name t l (tk_to_frac tk) scs) + (at level 20, format "l ↦t∗[ tk ]{ t } scs") : bi_scope. +Notation "l '↦s∗[' tk ']{' t } scs" := (array_tag heap_view_source_name t l (tk_to_frac tk) scs) + (at level 20, format "l ↦s∗[ tk ]{ t } scs") : bi_scope. + + +(** [array_tag_map] is the main way we interface with [array_tag] by having a representation of + the stored memory fragment. *) +Fixpoint array_tag_map (l : loc) (t : ptr_id) (v : list scalar) : gmap (ptr_id * loc) scalar := + match v with + | [] => ∅ + | sc :: v' => <[(t, l) := sc]> (array_tag_map (l +â‚— 1) t v') + end. +Lemma array_tag_map_lookup1 l t v t' l' : + is_Some (array_tag_map l t v !! (t', l')) → + t' = t ∧ l.1 = l'.1 ∧ l.2 ≤ l'.2 < l.2 + length v. +Proof. + induction v as [ | sc v IH] in l |-*. + - simpl. rewrite lookup_empty. intros [? [=]]. + - simpl. move => [sc0 ]. rewrite lookup_insert_Some. move => [[[= <- <-] Heq] | [Hneq Ht]]; first lia. + move : (IH (l +â‚— 1) ltac:(eauto)). destruct l. simpl. lia. +Qed. +Lemma array_tag_map_lookup2 l t v t' l' : + is_Some (array_tag_map l t v !! (t', l')) → + t' = t ∧ ∃ i, (i < length v)%nat ∧ l' = l +â‚— i. +Proof. + intros (-> & H1 & H2)%array_tag_map_lookup1. + split; first done. exists (Z.to_nat (l'.2 - l.2)). + destruct l, l'; rewrite /shift_loc; simpl in *. split. + - lia. + - apply pair_equal_spec. split; lia. +Qed. + +Lemma array_tag_map_lookup_Some l t v (i : nat) : + (i < length v)%nat → + array_tag_map l t v !! (t, l +â‚— i) = v !! i. +Proof. + induction v as [ | sc v IH] in l, i |-*. + - simpl. lia. + - simpl. intros Hi. destruct i as [ | i]. + + rewrite shift_loc_0_nat. rewrite lookup_insert. done. + + rewrite lookup_insert_ne; first last. { destruct l; simpl; intros [= ?]; lia. } + move : (IH (l +â‚— 1) i ltac:(lia)). rewrite shift_loc_assoc. + by replace (Z.of_nat (S i)) with (1 + i) by lia. +Qed. + +Lemma array_tag_map_lookup_None t t' l v : + t ≠t' → ∀ l', array_tag_map l t v !! (t', l') = None. +Proof. + intros Hneq l'. destruct (array_tag_map l t v !! (t', l')) eqn:Harr; last done. + specialize (array_tag_map_lookup1 l t v t' l' ltac:(eauto)) as [Heq _]; congruence. +Qed. + +Lemma array_tag_map_lookup_None' l t v l' : + (∀ i:nat, (i < length v)%nat → l +â‚— i ≠l') → + array_tag_map l t v !! (t, l') = None. +Proof. + intros Hneq. destruct (array_tag_map _ _ _ !! _) eqn:Heq; last done. exfalso. + specialize (array_tag_map_lookup2 l t v t l' ltac:(eauto)) as [_ (i & Hi & ->)]. + eapply Hneq; last reflexivity. done. +Qed. + +Lemma array_tag_map_lookup_None2 l t t' v l' : + array_tag_map l t v !! (t', l') = None → + t ≠t' ∨ (∀ i: nat, (i < length v)%nat → l +â‚— i ≠l'). +Proof. +Admitted. + +Lemma dom_agree_on_tag_array_tag_map l t v_t v_s : + length v_t = length v_s → + dom_agree_on_tag (array_tag_map l t v_t) (array_tag_map l t v_s) t. +Proof. + intros Hlen. split; intros l'. + - intros (_ & (i & Hi & ->))%array_tag_map_lookup2. rewrite array_tag_map_lookup_Some; last lia. + apply lookup_lt_is_Some_2. lia. + - intros (_ & (i & Hi & ->))%array_tag_map_lookup2. rewrite array_tag_map_lookup_Some; last lia. + apply lookup_lt_is_Some_2. lia. +Qed. + +(** Array update lemmas for the heap views *) +Lemma ghost_map_array_tag_lookup `{!bor_stateGS Σ} (γh : gname) (q : Qp) (M : gmap (ptr_id * loc) scalar) (scs : list scalar) (t : ptr_id) (l : loc) dq : + ghost_map_auth γh q M -∗ + ([∗ list] i ↦ sc ∈ scs, ghost_map_elem γh (t, l +â‚— i) dq sc) -∗ + ⌜∀ i : nat, (i < length scs)%nat → M !! (t, l +â‚— i) = scs !! iâŒ. +Proof. + iIntros "Hauth Helem". iInduction scs as [ |sc scs ] "IH" forall (l) "Hauth Helem". + - iPureIntro; cbn. lia. + - rewrite big_sepL_cons. iDestruct "Helem" as "[Hsc Hscs]". + iPoseProof (ghost_map_lookup with "Hauth Hsc") as "%Hl". + iDestruct ("IH" $! (l +â‚— 1) with "Hauth [Hscs]") as "%IH". + { iApply (big_sepL_mono with "Hscs"). intros i sc' Hs. cbn. rewrite shift_loc_assoc. + replace (Z.of_nat $ S i) with (1 + i)%Z by lia. done. } + iPureIntro. intros i Hle. destruct i; first done. + replace (Z.of_nat $ S i) with (1 + i)%Z by lia. cbn in *. rewrite -(IH i); last lia. + by rewrite shift_loc_assoc. +Qed. + +Lemma ghost_map_array_tag_update `{!bor_stateGS Σ} (γh : gname) (M : gmap (ptr_id * loc) scalar) (v v' : list scalar) (t : ptr_id) (l : loc) : + ghost_map_auth γh 1 M -∗ + ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +â‚— i) (DfracOwn 1) sc) ==∗ + ([∗ list] i ↦ sc' ∈ v', ghost_map_elem γh (t, l +â‚— i) (DfracOwn 1) sc') ∗ + ghost_map_auth γh 1 (array_tag_map l t v' ∪ M). +Proof. +Admitted. + +Lemma ghost_map_array_tag_insert `{!bor_stateGS Σ} (γh : gname) (M : gmap (ptr_id * loc) scalar) (v : list scalar) (t : ptr_id) (l : loc) : + (∀ i : nat, (i < length v)%nat → M !! (t, l +â‚— i) = None) → + ghost_map_auth γh 1 M ==∗ + ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +â‚— i) (DfracOwn 1) sc) ∗ + ghost_map_auth γh 1 (array_tag_map l t v ∪ M). +Proof. +Admitted. + +Lemma ghost_map_array_tag_delete `{!bor_stateGS Σ} (γh : gname) (M : gmap (ptr_id * loc) scalar) (v : list scalar) (t : ptr_id) (l : loc) : + ghost_map_auth γh 1 M -∗ + ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +â‚— i) (DfracOwn 1) sc) ==∗ + ghost_map_auth γh 1 (M ∖ array_tag_map l t v). +Proof. + iIntros "Hauth Helems". + iApply (ghost_map_delete_big (array_tag_map l t v) with "Hauth [Helems]"). + iInduction v as [ | sc v] "IH" forall (l); first done. + simpl. iApply big_sepM_insert. + { destruct (_ !! _) eqn:Heq; last done. + specialize (array_tag_map_lookup2 (l +â‚— 1) t v t l ltac:(eauto)) as [_ (i & _ & Hl)]. + destruct l. injection Hl. lia. + } + rewrite shift_loc_0_nat. iDestruct "Helems" as "[$ Helems]". + iApply "IH". iApply (big_sepL_mono with "Helems"). + iIntros (i sc' Hi). simpl. + rewrite shift_loc_assoc. replace (Z.of_nat (S i)) with (1 + i) by lia; done. +Qed. + +Lemma ghost_map_array_tag_tk `{!bor_stateGS Σ} (γh : gname) (v : list scalar) (t : ptr_id) (l : loc) tk : + ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +â‚— i) (DfracOwn 1) sc) ==∗ + ([∗ list] i ↦ sc ∈ v, ghost_map_elem γh (t, l +â‚— i) (tk_to_frac tk) sc). +Proof. + destruct tk; cbn; [ | by eauto | by eauto]. + iInduction v as [| sc v] "IH" forall (l); first by eauto. + rewrite !big_sepL_cons. iIntros "[Hh Hr]". + iMod (ghost_map_elem_persist with "Hh") as "$". + iMod ("IH" $! (l +â‚— 1) with "[Hr]") as "Hr". + - iApply (big_sepL_mono with "Hr"). intros i sc' Hs. simpl. rewrite shift_loc_assoc. + by replace (Z.of_nat (S i)) with (1 + i) by lia. + - iModIntro. + iApply (big_sepL_mono with "Hr"). intros i sc' Hs. simpl. rewrite shift_loc_assoc. + by replace (Z.of_nat (S i)) with (1 + i) by lia. +Qed. + + +Section val_rel. + Context `{bor_stateGS Σ}. + (** Value relation *) + + Definition sc_rel (sc1 sc2 : scalar) : iProp Σ := + match sc1, sc2 with + | ScInt z1, ScInt z2 => ⌜z1 = z2⌠+ | ScFnPtr f1, ScFnPtr f2 => ⌜f1 = f2⌠+ | ScPtr l1 p1, ScPtr l2 p2 => + (* through [state_rel]: + * the stacks are the same, + * the allocation size is the same, + * and the locations are related (i.e.: if tagged, then it is public) + *) + ⌜l1 = l2⌠∗ + (⌜p1 = Untagged⌠∗ ⌜p2 = Untagged⌠∨ + (∃ t1 t2, ⌜p1 = Tagged t1⌠∗ ⌜p2 = Tagged t2⌠∗ + ⌜t1 = t2⌠∗ + t1 $$ tk_pub)) + (* what the [tk_pub] gives us is that the locations store related values *) + | ScCallId c, ScCallId c' => ⌜c = c'⌠+ (* [ScPoison] can be refined by anything *) + | _ , ScPoison => True + | _, _ => False + end. + + Definition value_rel (v1 v2 : value) : iProp Σ := [∗ list] sc_t; sc_s ∈ v1; v2, sc_rel sc_t sc_s. + + Definition rrel (r1 r2 : result) : iProp Σ := + match r1, r2 with + | ValR v1, ValR v2 => value_rel v1 v2 + | PlaceR l1 bor1 T1, PlaceR l2 bor2 T2 => + (* places must be related in a similar way as pointers: either untagged or public. Types should be equal. *) + sc_rel (ScPtr l1 bor1) (ScPtr l2 bor2) ∧ ⌜T1 = T2⌠+ | _, _ => False + end. + + Global Instance sc_rel_persistent sc_t sc_s : Persistent (sc_rel sc_t sc_s). + Proof. destruct sc_t, sc_s; apply _. Qed. + Global Instance value_rel_persistent v_t v_s : Persistent (value_rel v_t v_s). + Proof. apply _. Qed. + Global Instance rrel_persistent r_t r_s : Persistent (rrel r_t r_s). + Proof. destruct r_t, r_s; apply _. Qed. + + (* Inversion lemmas *) + Lemma sc_rel_ptr_source sc_t l_s t_s : + sc_rel sc_t (ScPtr l_s t_s) -∗ ⌜sc_t = ScPtr l_s t_s⌠∗ (if t_s is Tagged t then t $$ tk_pub else True). + Proof. + iIntros "Hrel". destruct sc_t; [done | done | | done | done ]. + iDestruct "Hrel" as "(-> & [[-> ->] | (% & %t & -> & -> & -> & ?)])"; iFrame; done. + Qed. + Lemma sc_rel_fnptr_source sc_t fn : + sc_rel sc_t (ScFnPtr fn) -∗ ⌜sc_t = ScFnPtr fnâŒ. + Proof. + iIntros "Hrel". destruct sc_t; [done | done | done | | done]. + by iDestruct "Hrel" as "->". + Qed. + Lemma sc_rel_int_source sc_t z : + sc_rel sc_t (ScInt z) -∗ ⌜sc_t = ScInt zâŒ. + Proof. + iIntros "Hrel". destruct sc_t; [ done | | done..]. + by iDestruct "Hrel" as "->". + Qed. + Lemma sc_rel_cid_source sc_t c : + sc_rel sc_t (ScCallId c) -∗ ⌜sc_t = ScCallId câŒ. + Proof. iIntros "Hrel"; destruct sc_t; [done.. | ]. by iDestruct "Hrel" as "->". Qed. + + Lemma sc_rel_poison_target sc_s : + sc_rel (ScPoison) sc_s -∗ ⌜sc_s = ScPoisonâŒ. + Proof. iIntros "Hrel". destruct sc_s; done. Qed. + + Lemma rrel_place_source r_t l_s t_s T : + rrel r_t (PlaceR l_s t_s T) -∗ + ∃ l_t, ⌜r_t = PlaceR l_t t_s T⌠∗ (if t_s is Tagged t then t $$ tk_pub else True). + Proof. + iIntros "Hrel". + destruct r_t as [ | l_t t' T']; first done. iDestruct "Hrel" as "(#H & ->)". + iDestruct (sc_rel_ptr_source with "H") as "[%Heq Htag]". + injection Heq as [= -> ->]. iExists l_s. eauto. + Qed. + Lemma rrel_value_source r_t v_s : + rrel r_t (ValR v_s) -∗ + ∃ v_t, ⌜r_t = ValR v_t⌠∗ value_rel v_t v_s. + Proof. + iIntros "Hrel". destruct r_t as [ v_t | ]; last done. + iExists v_t. iFrame "Hrel". done. + Qed. + + Lemma value_rel_length v_t v_s : + value_rel v_t v_s -∗ ⌜length v_t = length v_sâŒ. + Proof. iApply big_sepL2_length. Qed. + Lemma value_rel_empty : + ⊢ value_rel [] []. + Proof. by iApply big_sepL2_nil. Qed. + + Lemma value_rel_singleton_source v_t sc_s : + value_rel v_t [sc_s] -∗ ∃ sc_t, ⌜v_t = [sc_t]⌠∗ sc_rel sc_t sc_s. + Proof. + iIntros "Hv". iPoseProof (value_rel_length with "Hv") as "%Hlen". + destruct v_t as [ | sc_t []]; [done | | done ]. + iExists sc_t. iSplitR "Hv"; first done. iRevert "Hv". rewrite /value_rel big_sepL2_singleton. eauto. + Qed. + + Lemma value_rel_lookup v_t v_s (i : nat) : + i < length v_t → + value_rel v_t v_s -∗ + ∃ sc_t sc_s, ⌜v_t !! i = Some sc_t⌠∗ ⌜v_s !! i = Some sc_s⌠∗ sc_rel sc_t sc_s. + Proof. + iIntros (Hi) "Hvrel". rewrite /value_rel big_sepL2_forall. + iDestruct "Hvrel" as "[%Hlen Hvrel]". + iSpecialize ("Hvrel" $! i (v_t !!! i) (v_s !!! i)). iExists (v_t !!! i), (v_s !!! i). + assert (v_t !! i = Some (v_t !!! i)) as Heq. + { apply list_lookup_lookup_total. apply lookup_lt_is_Some_2. lia. } + assert (v_s !! i = Some (v_s !!! i)) as Heq'. + { apply list_lookup_lookup_total. apply lookup_lt_is_Some_2. lia. } + iSplit; first done. iSplit; first done. iApply "Hvrel"; done. + Qed. + + Lemma value_rel_lookup_total (v_t v_s : list scalar) (i : nat) : + i < length v_t → value_rel v_t v_s -∗ sc_rel (v_t !!! i) (v_s !!! i). + Proof. + iIntros (Hi) "Hvrel". rewrite /value_rel big_sepL2_forall. + iDestruct "Hvrel" as "[%Hlen Hvrel]". + iApply ("Hvrel" $! i (v_t !!! i) (v_s !!! i)). + all: iPureIntro; apply list_lookup_lookup_total; apply lookup_lt_is_Some_2; lia. + Qed. +End val_rel. + +Class sborGS (Σ: gFunctors) := SBorG { + (* program assertions *) + sborG_gen_progG :> gen_sim_progGS string ectx ectx Σ; + sborG_stateG :> bor_stateGS Σ; +}. + +Global Program Instance sborGS_simulirisG `{!sborGS Σ} : simulirisG (iPropI Σ) bor_lang := { + state_interp P_t σ_t P_s σ_s T_s := + (gen_prog_interp (hG := gen_prog_inG_target) P_t ∗ + gen_prog_interp (hG := gen_prog_inG_source) P_s ∗ + bor_interp sc_rel σ_t σ_s + )%I; +}. +Next Obligation. +Admitted. + + +(** Program assertions *) +Notation "f '@t' Kt" := (hasfun (hG:=gen_prog_inG_target) f Kt) + (at level 20, format "f @t Kt") : bi_scope. +Notation "f '@s' Ks" := (hasfun (hG:=gen_prog_inG_source) f Ks) + (at level 20, format "f @s Ks") : bi_scope. + +Lemma hasfun_target_agree `{sborGS Σ} f K_t1 K_t2 : f @t K_t1 -∗ f @t K_t2 -∗ ⌜K_t1 = K_t2âŒ. +Proof. apply hasfun_agree. Qed. + +Lemma hasfun_source_agree `{sborGS Σ} f K_s1 K_s2 : f @s K_s1 -∗ f @s K_s2 -∗ ⌜K_s1 = K_s2âŒ. +Proof. apply hasfun_agree. Qed. + + diff --git a/theories/stacked_borrows/primitive_laws.v b/theories/stacked_borrows/primitive_laws.v index 99177186e810c07e4e5f2f1ed06caf7ba48951a5..896fa72276611dc019a260b9a4cfaef76df129af 100644 --- a/theories/stacked_borrows/primitive_laws.v +++ b/theories/stacked_borrows/primitive_laws.v @@ -1,42 +1,5 @@ -(** This file proves the basic laws of the BorIngLang program logic by applying -the Simuliris lifting lemmas. *) - +(* Re-export steps *) From iris.proofmode Require Export tactics. -From iris.bi.lib Require Import fractional. -From iris.base_logic.lib Require Import ghost_map. From simuliris.base_logic Require Export gen_sim_heap gen_sim_prog. From simuliris.simulation Require Export slsls. -From simuliris.simulation Require Import lifting. -From simuliris.stacked_borrows Require Export class_instances tactics notation heap steps_refl steps_opt. -From iris.prelude Require Import options. - - - -(** Program assertions *) -Notation "f '@t' Kt" := (hasfun (hG:=gen_prog_inG_target) f Kt) - (at level 20, format "f @t Kt") : bi_scope. -Notation "f '@s' Ks" := (hasfun (hG:=gen_prog_inG_source) f Ks) - (at level 20, format "f @s Ks") : bi_scope. - - -Section lifting. -Context `{!sborG Σ}. -Implicit Types P Q : iProp Σ. -Implicit Types Φ : result → result → iProp Σ. -Implicit Types σ σ_s σ_t : state. -Implicit Types r r_s r_t : result. -Implicit Types l : loc. -Implicit Types f : fname. - -Context (Ω : result → result → iProp Σ). - - -(** Program for target *) -Lemma hasfun_target_agree f K_t1 K_t2 : f @t K_t1 -∗ f @t K_t2 -∗ ⌜K_t1 = K_t2âŒ. -Proof. apply hasfun_agree. Qed. - -(** Program for source *) -Lemma hasfun_source_agree f K_s1 K_s2 : f @s K_s1 -∗ f @s K_s2 -∗ ⌜K_s1 = K_s2âŒ. -Proof. apply hasfun_agree. Qed. - -End lifting. +From simuliris.stacked_borrows Require Export class_instances tactics notation defs logical_state steps_refl steps_opt. diff --git a/theories/stacked_borrows/proofmode.v b/theories/stacked_borrows/proofmode.v index 4b1c278c858a93c3ca2b8eb31c374e825af94bcf..76574d293104336d861b87c272c64696726e2712 100644 --- a/theories/stacked_borrows/proofmode.v +++ b/theories/stacked_borrows/proofmode.v @@ -11,7 +11,7 @@ From simuliris.stacked_borrows Require Export primitive_laws notation. Section sim. -Context `{!sborG Σ}. +Context `{!sborGS Σ}. Context (Ω : result → result → iProp Σ). (*Local Notation "et '⪯' es {{ Φ }}" := (et ⪯{Ω} es {{Φ}})%I (at level 40, Φ at level 200) : bi_scope.*) (*Local Notation "et '⪯' es [{ Φ }]" := (et ⪯{Ω} es [{Φ}])%I (at level 40, Φ at level 200) : bi_scope.*) @@ -133,9 +133,6 @@ Proof. iIntros "H". iApply source_red_bind. by iApply Hs. Qed. -(* TODO: heap tactics *) - - (** Switching between judgments *) Lemma tac_to_target Δ e_t e_s Φ Ï€ : diff --git a/theories/stacked_borrows/steps_opt.v b/theories/stacked_borrows/steps_opt.v index 5bed884a5524021b3b2e901668055363930ef9de..a591919f8b6aa75af934d24e8f8f2cacb563a8e2 100644 --- a/theories/stacked_borrows/steps_opt.v +++ b/theories/stacked_borrows/steps_opt.v @@ -1,17 +1,18 @@ From iris.proofmode Require Export tactics. -From iris.bi.lib Require Import fractional. From iris.base_logic.lib Require Import ghost_map. From simuliris.base_logic Require Export gen_sim_prog. From simuliris.simulation Require Export slsls. From simuliris.simulation Require Import lifting. -From iris.prelude Require Import options. From simuliris.stacked_borrows Require Import tkmap_view. From simuliris.stacked_borrows Require Export defs. From simuliris.stacked_borrows Require Import steps_progress steps_retag steps_inv. -From simuliris.stacked_borrows Require Import heap. +From simuliris.stacked_borrows Require Import logical_state inv_accessors. +From iris.prelude Require Import options. + +(** * Simulation lemmas using the ghost state for proving optimizations *) Section lifting. -Context `{!sborG Σ}. +Context `{!sborGS Σ}. Implicit Types P Q : iProp Σ. Implicit Types Φ : expr → expr → iProp Σ. Implicit Types σ σ_s σ_t : state. @@ -22,7 +23,8 @@ Implicit Types f : fname. Context (Ω : result → result → iProp Σ). -(** Retags *) +(** ** Retags *) +(** *** Retags without protectors *) Lemma bor_interp_retag_default σ_t σ_s c l ot T α' mut : let pk : pointer_kind := RefPtr mut in let pm := match mut with Mutable => Unique | Immutable => SharedReadOnly end in @@ -114,7 +116,7 @@ Proof. (* re-establishing the interpretation *) iExists M_call, (<[ nt := (tk, ()) ]> M_tag), (array_tag_map l nt v_t ∪ M_t), (array_tag_map l nt v_s ∪ M_s). iFrame. iSplitL. - { (* tainted *) iApply (tag_tainted_interp_retag with "Htainted"); done. } + { (* tainted *) iApply (tag_tainted_interp_retag with "Htainted"); done. } iSplitL. { (* state relation *) rewrite /state_rel. simpl. iDestruct "Hsrel" as "(-> & %Hs_eq & -> & -> & -> & Hsrel)". @@ -153,11 +155,11 @@ Proof. - cbn. split_and!; [lia | lia | | |]. + intros l' sc_t Ha%lookup_union_Some_l'; last done. specialize (array_tag_map_lookup2 l nt v_t nt l' ltac:(eauto)) as [_ (i & Hi & ->)]. - eapply retag_mut_loc_controlled; [ done | done | done | lia | ]. + eapply loc_controlled_retag_ref; [ done | done | done | lia | ]. move : Ha. rewrite array_tag_map_lookup_Some; last done. move => <-. apply Hshp_t. lia. + intros l' sc_s Ha%lookup_union_Some_l'; last done. specialize (array_tag_map_lookup2 l nt v_s nt l' ltac:(eauto)) as [_ (i & Hi & ->)]. - subst nt. rewrite -Hsnp. eapply retag_mut_loc_controlled; [ done | done | done | lia | ]. + subst nt. rewrite -Hsnp. eapply loc_controlled_retag_ref; [ done | done | done | lia | ]. move : Ha. rewrite array_tag_map_lookup_Some; last done. move => <-. apply Hshp_s. lia. + apply dom_agree_on_tag_union. { apply dom_agree_on_tag_array_tag_map. lia. } apply dom_agree_on_tag_not_elem; done. @@ -166,11 +168,11 @@ Proof. split_and!; [ lia | lia | | | ]. + intros l' sc_t Ha. rewrite lookup_union_r in Ha; last by apply array_tag_map_lookup_None. apply Hcontrolled_t in Ha. - eapply retag_loc_controlled_preserved; [done | done | | done | done]. + eapply loc_controlled_retag_update; [done | done | | done | done]. intros <-. destruct tk'; [ done | | ]; move : Hsome_t Hpub; congruence. + intros l' sc_s Ha. rewrite lookup_union_r in Ha; last by apply array_tag_map_lookup_None. apply Hcontrolled_s in Ha. - eapply retag_loc_controlled_preserved; [done | done | | done | done]. + eapply loc_controlled_retag_update; [done | done | | done | done]. intros <-. destruct tk'; [ done | | ]; move : Hsome_t Hpub; congruence. + apply dom_agree_on_tag_union; last done. apply dom_agree_on_tag_not_elem; apply array_tag_map_lookup_None; done. @@ -237,6 +239,22 @@ Proof. iApply ("Hsim" with "[] [] Hval Htag Ht Hs Hpub"); [done | done | ..]. Qed. +(** *** Retags with protectors *) +Fixpoint seq_loc_set (l : loc) (n : nat) : gset loc := + match n with + | O => ∅ + | S n => {[ l +â‚— n ]} ∪ seq_loc_set l n + end. +Lemma seq_loc_set_elem l n l' : + l' ∈ seq_loc_set l n ↔ (∃ (i : nat), (i < n)%nat ∧ l' = l +â‚— i). +Proof. + induction n as [ | n IH]; simpl. + - rewrite elem_of_empty. split; first done. intros (i & Hi & _). lia. + - rewrite elem_of_union elem_of_singleton. split. + + intros [-> | (i & Hi & ->)%IH]; [ exists n; naive_solver | exists i; naive_solver]. + + intros (i & Hi & ->). destruct (decide (i = n)) as [-> | Hneq]; first by left. + right. apply IH. exists i. split; [lia | done]. +Qed. Lemma bor_interp_retag_fnentry σ_t σ_s l ot c T α' M mut : let pk : pointer_kind := RefPtr mut in @@ -335,8 +353,8 @@ Proof. (* re-establishing the interpretation *) iExists (<[c:=M']> M_call), (<[ nt := (tk, ()) ]> M_tag), (array_tag_map l nt v_t ∪ M_t), (array_tag_map l nt v_s ∪ M_s). iFrame. iSplitL. - { (* tainted *) iApply (tag_tainted_interp_retag with "Htainted"); done. } - iSplitL. + { (* tainted *) iApply (tag_tainted_interp_retag with "Htainted"); done. } + iSplitL. { (* state relation *) rewrite /state_rel. simpl. iDestruct "Hsrel" as "(-> & %Hs_eq & -> & -> & -> & Hsrel)". do 5 (iSplitL; first done). iIntros (l' Hsl'). @@ -394,11 +412,11 @@ Proof. - cbn. split_and!; [lia | lia | | |]. + intros l' sc_t Ha%lookup_union_Some_l'; last done. specialize (array_tag_map_lookup2 l nt v_t nt l' ltac:(eauto)) as [_ (i & Hi & ->)]. - eapply retag_mut_loc_controlled; [ done | done | done | lia | ]. + eapply loc_controlled_retag_ref; [ done | done | done | lia | ]. move : Ha. rewrite array_tag_map_lookup_Some; last done. move => <-. apply Hshp_t. lia. + intros l' sc_s Ha%lookup_union_Some_l'; last done. specialize (array_tag_map_lookup2 l nt v_s nt l' ltac:(eauto)) as [_ (i & Hi & ->)]. - subst nt. rewrite -Hsnp. eapply retag_mut_loc_controlled; [ done | done | done | lia | ]. + subst nt. rewrite -Hsnp. eapply loc_controlled_retag_ref; [ done | done | done | lia | ]. move : Ha. rewrite array_tag_map_lookup_Some; last done. move => <-. apply Hshp_s. lia. + apply dom_agree_on_tag_union. { apply dom_agree_on_tag_array_tag_map. lia. } apply dom_agree_on_tag_not_elem; done. @@ -407,11 +425,11 @@ Proof. split_and!; [ lia | lia | | | ]. + intros l' sc_t Ha. rewrite lookup_union_r in Ha; last by apply array_tag_map_lookup_None. apply Hcontrolled_t in Ha. - eapply retag_loc_controlled_preserved; [done | done | | done | done]. + eapply loc_controlled_retag_update; [done | done | | done | done]. intros <-. destruct tk'; [ done | | ]; move : Hsome_t Hpub; congruence. + intros l' sc_s Ha. rewrite lookup_union_r in Ha; last by apply array_tag_map_lookup_None. apply Hcontrolled_s in Ha. - eapply retag_loc_controlled_preserved; [done | done | | done | done]. + eapply loc_controlled_retag_update; [done | done | | done | done]. intros <-. destruct tk'; [ done | | ]; move : Hsome_t Hpub; congruence. + apply dom_agree_on_tag_union; last done. apply dom_agree_on_tag_not_elem; apply array_tag_map_lookup_None; done. @@ -481,7 +499,7 @@ Proof. iApply ("Hsim" with "[] [] Hval Hcid Htag Ht Hs Hpub"); [done | done | ..]. Qed. -(** Updates for calls sets *) +(** ** Updates for calls sets *) (* TODO: maybe formulate that with [update_si] instead *) Lemma sim_protected_unprotectN M L l c t tk v_t v_s Ï€ Φ e_t e_s : (∀ i : nat, (i < length v_t)%nat → (l +â‚— i) ∈ L) → @@ -494,55 +512,55 @@ Lemma sim_protected_unprotectN M L l c t tk v_t v_s Ï€ Φ e_t e_s : (c @@ (<[t := L ∖ (seq_loc_set l (length v_t)) ]> M) -∗ t $$ tk -∗ l ↦t∗[tk]{t} v_t -∗ l ↦s∗[tk]{t} v_s -∗ e_t ⪯{Ï€, Ω} e_s [{ Φ }]) -∗ e_t ⪯{Ï€, Ω} e_s [{ Φ }]. Proof. - iIntros (Hl HL) "Hc Htag Ht Hs #Hvrel Hsim". + iIntros (Hl HL) "Hc Htag Ht Hs #Hvrel Hsim". iApply sim_update_si. rewrite /update_si. iIntros (?????) "(HP_t & HP_s & Hbor)". set (L' := L ∖ seq_loc_set l (length v_t)). set (M' := <[ t := L' ]> M). iPoseProof (value_rel_length with "Hvrel") as "%Hlen". - iPoseProof (heap_protected_readN_source with "Hbor Hs Htag Hc") as "(%Hv_s & %)". - { intros i Hi. exists L. split; first done. apply Hl. lia. } - iPoseProof (heap_protected_readN_target with "Hbor Ht Htag Hc") as "(%Hv_t & %)". - { intros i Hi. exists L. split; first done. apply Hl. lia. } + iPoseProof (bor_interp_readN_source_protected with "Hbor Hs Htag Hc") as "(%Hv_s & %)". + { intros i Hi. exists L. split; first done. apply Hl. lia. } + iPoseProof (bor_interp_readN_target_protected with "Hbor Ht Htag Hc") as "(%Hv_t & %)". + { intros i Hi. exists L. split; first done. apply Hl. lia. } - iDestruct "Hbor" as "(% & % & % & % & (Hcall_auth & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & #Hsrel & %Hcall_interp & %Htag_interp & %Hwf_s & %Hwf_t)". + iDestruct "Hbor" as "(% & % & % & % & (Hcall_auth & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & #Hsrel & %Hcall_interp & %Htag_interp & %Hwf_s & %Hwf_t)". iPoseProof (ghost_map_lookup with "Hcall_auth Hc") as "%HcM". iMod (ghost_map_update M' with "Hcall_auth Hc") as "[Hcall_auth Hc]". iModIntro. iFrame "HP_t HP_s". iSplitR "Hsim Hc Ht Htag Hs"; last by iApply ("Hsim" with "Hc Htag Ht Hs"). - iExists (<[ c := M' ]> M_call), M_tag, M_t, M_s. iFrame. - iSplitL "Hsrel". - { iDestruct "Hsrel" as "(%Hdom_eq & %Hsst_eq & %Hsnp_eq & %Hsnc_eq & %Hscs_eq & Hloc)". + iExists (<[ c := M' ]> M_call), M_tag, M_t, M_s. iFrame. + iSplitL "Hsrel". + { iDestruct "Hsrel" as "(%Hdom_eq & %Hsst_eq & %Hsnp_eq & %Hsnc_eq & %Hscs_eq & Hloc)". do 5 (iSplitR; first done). iIntros (l' Hl'). iDestruct ("Hloc" $! l' with "[//]") as "[Hpub | %Hpriv]"; first by iLeft. - destruct (decide (l' ∈ seq_loc_set l (length v_t))) as [(i & Hi & ->)%seq_loc_set_elem | Hnotin]. + destruct (decide (l' ∈ seq_loc_set l (length v_t))) as [(i & Hi & ->)%seq_loc_set_elem | Hnotin]. - (* location is made public *) - iLeft. iIntros (sc_t' Hsc_t'). - specialize (Hv_t i Hi) as Heq. rewrite Heq in Hsc_t'. - iExists (v_s !!! i). iSplitR. - + iPureIntro. rewrite Hv_s; last lia. apply list_lookup_lookup_total, lookup_lt_is_Some_2. lia. + iLeft. iIntros (sc_t' Hsc_t'). + specialize (Hv_t i Hi) as Heq. rewrite Heq in Hsc_t'. + iExists (v_s !!! i). iSplitR. + + iPureIntro. rewrite Hv_s; last lia. apply list_lookup_lookup_total, lookup_lt_is_Some_2. lia. + iPoseProof (value_rel_lookup_total v_t v_s i with "Hvrel") as "Hsc"; first lia. rewrite -(list_lookup_total_correct _ _ _ Hsc_t'). done. - (* location is still private *) iRight. iPureIntro. destruct Hpriv as (t' & tk' & Htk' & Hsome & Hpriv). - exists t', tk'. split; first done. split; first done. + exists t', tk'. split; first done. split; first done. destruct Hpriv as [-> | [-> Hpriv]]; first by left. right; split; first done. destruct Hpriv as (c' & M'' & Hc' & Hin'). destruct (decide (c' = c)) as [-> | Hneq]; first last. - { exists c', M''. rewrite lookup_insert_ne; done. } - exists c, M'. rewrite lookup_insert. split; first done. - destruct (decide (t' = t)) as [-> | Hneq']; first last. - { destruct Hin' as (L'' & HL'' & Hl''). exists L''. split; last done. - simplify_eq. rewrite lookup_insert_ne; done. - } - destruct Hin' as (L'' & HL'' & Hl''). exists L'. split; first by rewrite lookup_insert. - simplify_eq. subst L'. apply elem_of_difference. done. - } + { exists c', M''. rewrite lookup_insert_ne; done. } + exists c, M'. rewrite lookup_insert. split; first done. + destruct (decide (t' = t)) as [-> | Hneq']; first last. + { destruct Hin' as (L'' & HL'' & Hl''). exists L''. split; last done. + simplify_eq. rewrite lookup_insert_ne; done. + } + destruct Hin' as (L'' & HL'' & Hl''). exists L'. split; first by rewrite lookup_insert. + simplify_eq. subst L'. apply elem_of_difference. done. + } iSplitL; last done. iPureIntro. intros c' M''. rewrite lookup_insert_Some. intros [[<- <-] | [Hneq Hsome]]. - apply Hcall_interp in HcM as [Hc HcM]. split; first done. intros t' L''. subst M'. rewrite lookup_insert_Some. intros [[<- <-] | [Hneq' Hsome']]. - + specialize (HcM t L HL) as (Ht & HsL). split; first done. - intros l'. rewrite elem_of_difference. intros [Hl'%HsL _]. done. + + specialize (HcM t L HL) as (Ht & HsL). split; first done. + intros l'. rewrite elem_of_difference. intros [Hl'%HsL _]. done. + specialize (HcM _ _ Hsome') as (Ht & HsL). done. - - apply Hcall_interp in Hsome as [Hc' Hsome]. done. + - apply Hcall_interp in Hsome as [Hc' Hsome]. done. Qed. Lemma sim_protected_unprotect M L l c t tk sc_t sc_s Ï€ Φ e_t e_s : @@ -556,60 +574,61 @@ Lemma sim_protected_unprotect M L l c t tk sc_t sc_s Ï€ Φ e_t e_s : (c @@ (<[t := L ∖ {[ l ]} ]> M) -∗ t $$ tk -∗ l ↦t[tk]{t} sc_t -∗ l ↦s[tk]{t} sc_s -∗ e_t ⪯{Ï€, Ω} e_s [{ Φ }]) -∗ e_t ⪯{Ï€, Ω} e_s [{ Φ }]. Proof. - iIntros (Hin HL) "Hc Htag Ht Hs Hrel Hsim". - iApply (sim_protected_unprotectN M L l c t tk [sc_t] [sc_s] with "Hc Htag [Ht] [Hs] [Hrel] [Hsim]"). - - simpl. intros i Hi. replace i with O by lia. rewrite shift_loc_0_nat. done. - - done. - - iApply big_sepL_singleton. rewrite shift_loc_0_nat. done. - - iApply big_sepL_singleton. rewrite shift_loc_0_nat. done. - - iApply big_sepL2_singleton. done. + iIntros (Hin HL) "Hc Htag Ht Hs Hrel Hsim". + iApply (sim_protected_unprotectN M L l c t tk [sc_t] [sc_s] with "Hc Htag [Ht] [Hs] [Hrel] [Hsim]"). + - simpl. intros i Hi. replace i with O by lia. rewrite shift_loc_0_nat. done. + - done. + - iApply big_sepL_singleton. rewrite shift_loc_0_nat. done. + - iApply big_sepL_singleton. rewrite shift_loc_0_nat. done. + - iApply big_sepL2_singleton. done. - simpl. rewrite shift_loc_0_nat union_empty_r_L. - rewrite /array_tag !big_sepL_singleton !shift_loc_0_nat. done. + rewrite /array_tag !big_sepL_singleton !shift_loc_0_nat. done. Qed. -Lemma sim_remove_empty_calls t L M c e_t e_s Ï€ Φ : +Lemma sim_remove_empty_calls t L M c e_t e_s Ï€ Φ : M !! t = Some L → L = ∅ → c @@ M -∗ (c @@ (delete t M) -∗ e_t ⪯{Ï€, Ω} e_s [{ Φ }]) -∗ e_t ⪯{Ï€, Ω} e_s [{ Φ }]. -Proof. - iIntros (Ht ->) "Hc Hsim". +Proof. + iIntros (Ht ->) "Hc Hsim". iApply sim_update_si. rewrite /update_si. iIntros (?????) "(HP_t & HP_s & Hbor)". set (M' := delete t M). - iDestruct "Hbor" as "(% & % & % & % & (Hcall_auth & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & #Hsrel & %Hcall_interp & %Htag_interp & %Hwf_s & %Hwf_t)". + iDestruct "Hbor" as "(% & % & % & % & (Hcall_auth & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & #Hsrel & %Hcall_interp & %Htag_interp & %Hwf_s & %Hwf_t)". iPoseProof (ghost_map_lookup with "Hcall_auth Hc") as "%HcM". iMod (ghost_map_update M' with "Hcall_auth Hc") as "[Hcall_auth Hc]". iModIntro. iFrame "HP_t HP_s". iSplitR "Hsim Hc"; last by iApply ("Hsim" with "Hc"). - iExists (<[ c := M' ]> M_call), M_tag, M_t, M_s. iFrame. - iSplitL "Hsrel". - { iDestruct "Hsrel" as "(%Hdom_eq & %Hsst_eq & %Hsnp_eq & %Hsnc_eq & %Hscs_eq & Hloc)". + iExists (<[ c := M' ]> M_call), M_tag, M_t, M_s. iFrame. + iSplitL "Hsrel". + { iDestruct "Hsrel" as "(%Hdom_eq & %Hsst_eq & %Hsnp_eq & %Hsnc_eq & %Hscs_eq & Hloc)". do 5 (iSplitR; first done). iIntros (l' Hl'). iDestruct ("Hloc" $! l' with "[//]") as "[Hpub | %Hpriv]"; first by iLeft. iRight. iPureIntro. destruct Hpriv as (t' & tk' & Htk' & Hsome & Hpriv). - exists t', tk'. split; first done. split; first done. + exists t', tk'. split; first done. split; first done. destruct Hpriv as [-> | [-> Hpriv]]; first by left. right; split; first done. destruct Hpriv as (c' & M'' & Hc' & Hin'). destruct (decide (c' = c)) as [-> | Hneq]; first last. - { exists c', M''. rewrite lookup_insert_ne; done. } - exists c, M'. rewrite lookup_insert. split; first done. - destruct (decide (t' = t)) as [-> | Hneq']; first last. - { destruct Hin' as (L'' & HL'' & Hl''). exists L''. split; last done. - simplify_eq. rewrite lookup_delete_ne; done. - } + { exists c', M''. rewrite lookup_insert_ne; done. } + exists c, M'. rewrite lookup_insert. split; first done. + destruct (decide (t' = t)) as [-> | Hneq']; first last. + { destruct Hin' as (L'' & HL'' & Hl''). exists L''. split; last done. + simplify_eq. rewrite lookup_delete_ne; done. + } exfalso. destruct Hin' as (L'' & HL'' & Hl''). simplify_eq. done. - } + } iSplitL; last done. iPureIntro. intros c' M''. rewrite lookup_insert_Some. intros [[<- <-] | [Hneq Hsome]]. - apply Hcall_interp in HcM as [Hc HcM]. split; first done. - intros t' L''. subst M'. rewrite lookup_delete_Some. intros [Hneq' Hsome']. naive_solver. - - apply Hcall_interp in Hsome as [Hc' Hsome]. done. + intros t' L''. subst M'. rewrite lookup_delete_Some. intros [Hneq' Hsome']. naive_solver. + - apply Hcall_interp in Hsome as [Hc' Hsome]. done. Qed. -(** Write lemmas *) +(** ** Write lemmas *) (* note: this is a new lemma. we do not care about relating the values - we only care for the source expression requiring that [t] is still on top! TODO: can we make that more general/nicer? + One option (not needed for our optimizations, though): also use deferred UB, but would require changing op sem. *) Lemma sim_write_unique_unprotected Ï€ l_t l_s t T v_t v_s v_t' v_s' Φ : t $$ tk_unq -∗ @@ -663,7 +682,7 @@ Lemma source_write_unique v_s v_s' T l t Ψ Ï€ : Proof. Admitted. -(** Copy lemmas *) +(** ** Copy lemmas *) Lemma target_copy_local v_t T l t Ψ : length v_t = tsize T → t $$ tk_local -∗ @@ -674,7 +693,7 @@ Proof. iIntros (Hlen) "Htag Ht Hsim". iApply target_red_lift_head_step. iIntros (?????) "(HP_t & HP_s & Hbor)". iModIntro. - iPoseProof (heap_local_readN_target with "Hbor Ht Htag") as "(%Hd & %Hstack)". + iPoseProof (bor_interp_readN_target_local with "Hbor Ht Htag") as "(%Hd & %Hstack)". rewrite Hlen in Hd Hstack. have READ_t : read_mem l (tsize T) σ_t.(shp) = Some v_t. { apply read_mem_values'; done. } @@ -704,7 +723,7 @@ Proof. iApply source_red_lift_head_step. iIntros (??????) "[(HP_t & HP_s & Hbor) _]". iModIntro. iPoseProof (bor_interp_get_state_wf with "Hbor") as "[% %Hwf_s]". - iPoseProof (heap_local_readN_source with "Hbor Hs Htag") as "(%Hd & %Hstack)". + iPoseProof (bor_interp_readN_source_local with "Hbor Hs Htag") as "(%Hd & %Hstack)". rewrite Hlen in Hd Hstack. have READ_s : read_mem l (tsize T) σ_s.(shp) = Some v_s. { apply read_mem_values'; done. } @@ -734,7 +753,7 @@ Proof. iIntros (Hlen Hprotected) "Hcall Htag Ht Hsim". iApply target_red_lift_head_step. iIntros (?????) "(HP_t & HP_s & Hbor)". iModIntro. - iPoseProof (heap_protected_readN_target with "Hbor Ht Htag Hcall") as "(%Hd & %Hown)". + iPoseProof (bor_interp_readN_target_protected with "Hbor Ht Htag Hcall") as "(%Hd & %Hown)". { by rewrite Hlen. } rewrite Hlen in Hd Hown. have READ_t : read_mem l (tsize T) σ_t.(shp) = Some v_t. @@ -757,7 +776,7 @@ Proof. destruct σ_t; done. Qed. -(* Since copies without granting tags are not UB in the source but yield poison, +(* Since copies without granting tags are not UB in the source but yield poison, we also need protection here to gain any knowledge about the value. *) Lemma source_copy_protected v_s T l t tk Ψ c M Ï€ : length v_s = tsize T → @@ -771,7 +790,7 @@ Proof. iIntros (Hlen Hprotected) "Hcall Htag Hs Hsim". iApply source_red_lift_head_step. iIntros (??????) "[(HP_t & HP_s & Hbor) %Hsafe]". iModIntro. - iPoseProof (heap_protected_readN_source with "Hbor Hs Htag Hcall") as "(%Hd & %Hown)". + iPoseProof (bor_interp_readN_source_protected with "Hbor Hs Htag Hcall") as "(%Hd & %Hown)". { by rewrite Hlen. } rewrite Hlen in Hd Hown. have READ_t : read_mem l (tsize T) σ_s.(shp) = Some v_s. @@ -783,7 +802,7 @@ Proof. specialize (Hown i Hi). destruct (bor_state_own_some_stack _ _ _ _ Hown) as (stk & Hs_stk). exists stk. split; first done. eapply bor_state_own_access1_read; done. } - iExists (#v_s)%E, _. + iExists (#v_s)%E, _. iSplitR. { iPureIntro. eapply copy_head_step'; [done | eapply read_mem_values'; eauto | eauto]. } iModIntro. iFrame "HP_t HP_s". @@ -791,7 +810,7 @@ Proof. destruct σ_s; done. Qed. -(* We can also read from unprotected source locations. +(* We can also read from unprotected source locations. But then we may get poison if the value isn't there anymore. *) Lemma source_copy_any v_s T l t tk Ψ Ï€ : length v_s = tsize T → @@ -800,28 +819,21 @@ Lemma source_copy_any v_s T l t tk Ψ Ï€ : (∀ v_s', ⌜v_s' = v_s ∨ v_s' = replicate (length v_s) ScPoison⌠-∗ l ↦s∗[tk]{t} v_s -∗ t $$ tk -∗ source_red #v_s' Ï€ Ψ)%E -∗ source_red (Copy (Place l (Tagged t) T)) Ï€ Ψ. Proof. -Admitted. - -Definition exists_dec_unique {A} (x : A) (P : _ → Prop) : (∀ y, P y → P x) → Decision (P x) → Decision (∃ y, P y). -Proof. - intros Hx Hdec. - refine (cast_if (decide (P x))). - - abstract by eexists _. - - abstract naive_solver. -Defined. +Admitted. -Lemma list_in_dec {X} (P : X → Prop) (l : list X) : - (∀ x, Decision (P x)) → +(** TODO: move *) +Lemma list_in_dec {X} (P : X → Prop) (l : list X) : + (∀ x, Decision (P x)) → Decision (∃ it, P it ∧ it ∈ l). -Proof. - intros HdecP. induction l as [ | it l IH]. +Proof. + intros HdecP. induction l as [ | it l IH]. - right. intros (it & _ & []%elem_of_nil). - - destruct IH as [ IH | IH]. + - destruct IH as [ IH | IH]. + left. destruct IH as (it' & Hit' & Hin). exists it'. split; first done. right. done. - + destruct (HdecP it) as [Hit | Hnit]. - { left. exists it. split; first done. by left. } + + destruct (HdecP it) as [Hit | Hnit]. + { left. exists it. split; first done. by left. } right. intros (it' & Hit' & [-> | Hin]%elem_of_cons); first done. - apply IH. eauto. + apply IH. eauto. Qed. Lemma target_copy_deferred v_t T l t tk Ψ : @@ -830,70 +842,73 @@ Lemma target_copy_deferred v_t T l t tk Ψ : l ↦t∗[tk]{t} v_t -∗ (∀ v_t', deferred_read v_t v_t' l t -∗ l ↦t∗[tk]{t} v_t -∗ t $$ tk -∗ target_red #v_t' Ψ)%E -∗ target_red (Copy (Place l (Tagged t) T)) Ψ. -Proof. +Proof. iIntros (Hlen) "Htag Ht Hsim". iApply target_red_lift_head_step. iIntros (?????) "(HP_t & HP_s & Hbor)". iModIntro. - iPoseProof (heap_readN_target with "Hbor Ht Htag") as "%Hcontrolled". + iPoseProof (bor_interp_readN_target with "Hbor Ht Htag") as "%Hcontrolled". - (* either: - - one of the preconditions is not fulfilled anymore. - In that case, we know that the item is not in the stack. - This means that memory_read = None, and the CopyFail rule works. + (* either: + - one of the preconditions is not fulfilled anymore. + In that case, we know that the item is not in the stack. + This means that memory_read = None, and the CopyFail rule works. In that case, we allocate with tag_tainted_interp_insert at that i. - - all of the preconditions are fulfilled. In that case, we proceed similarly - to the protected case. + - all of the preconditions are fulfilled. In that case, we proceed similarly + to the protected case. *) iPoseProof (bor_interp_get_state_wf with "Hbor") as "[%Hwf_t %]". - assert ((∀ i, (i < length v_t)%nat → shp σ_t !! (l +â‚— i) = v_t !! i ∧ bor_state_own (l +â‚— i) t tk σ_t) ∨ (∃ i, (i < length v_t)%nat ∧ ∀ st pm opro, σ_t.(sst) !! (l +â‚— i) = Some st → mkItem pm (Tagged t) opro ∉ st ∨ pm = Disabled)) as [Hsuccess | Hnosuccess]. - { - revert Hcontrolled. clear Hlen. - set (n' := length v_t). assert (n' = length v_t) as Heq by done. revert Heq. + assert ((∀ i, (i < length v_t)%nat → shp σ_t !! (l +â‚— i) = v_t !! i ∧ bor_state_own (l +â‚— i) t tk σ_t) ∨ + (∃ i, (i < length v_t)%nat ∧ ∀ st pm opro, σ_t.(sst) !! (l +â‚— i) = Some st → + mkItem pm (Tagged t) opro ∉ st ∨ pm = Disabled)) as [Hsuccess | Hnosuccess]. + { + revert Hcontrolled. clear Hlen. + set (n' := length v_t). assert (n' = length v_t) as Heq by done. revert Heq. generalize n' as n => n. clear n'. induction n as [ | n IH] in l, v_t |-* => Hlen Hcontrolled. { left. intros i Hi. lia. } destruct v_t as [ | sc v_t]; first done. specialize (IH v_t (l +â‚— 1)) as [IH | IH]. - - naive_solver. - - intros i Hi. specialize (Hcontrolled (S i) ltac:(lia)). + - naive_solver. + - intros i Hi. specialize (Hcontrolled (S i) ltac:(lia)). rewrite shift_loc_assoc. replace (1 + i)%Z with (Z.of_nat (S i))%Z by lia. done. - - setoid_rewrite shift_loc_assoc in IH. + - setoid_rewrite shift_loc_assoc in IH. destruct (σ_t.(sst) !! (l +â‚— O)) as [stk | ] eqn:Hstk; first last. - { right; exists O. split; first lia. intros ????; congruence. } - assert (Decision (∃ pm opro, mkItem pm (Tagged t) opro ∈ stk)) as [Hin | Hnotin]. - { destruct (list_in_dec (λ it, tg it = Tagged t) stk) as [Hit | Hnit]; first apply _. - - left. destruct Hit as (it & Htg & Hit). exists (perm it), (protector it). + { right; exists O. split; first lia. intros ????; congruence. } + assert (Decision (∃ pm opro, mkItem pm (Tagged t) opro ∈ stk)) as [Hin | Hnotin]. + { destruct (list_in_dec (λ it, tg it = Tagged t) stk) as [Hit | Hnit]; first apply _. + - left. destruct Hit as (it & Htg & Hit). exists (perm it), (protector it). destruct it; naive_solver. - right. contradict Hnit. destruct Hnit as (pm & opro & Hit). exists (mkItem pm (Tagged t) opro). split; done. - } - 2: { right. exists O. split; first lia. intros st pm opro Hst. simplify_eq. - left. contradict Hnotin. eauto. } - destruct Hin as (pm & opro & Hit). - destruct (decide (pm = Disabled)) as [-> | Hen]. - { right. exists O. split; first lia. intros st pm' opro' ?; simplify_eq. + } + 2: { right. exists O. split; first lia. intros st pm opro Hst. simplify_eq. + left. contradict Hnotin. eauto. } + destruct Hin as (pm & opro & Hit). + destruct (decide (pm = Disabled)) as [-> | Hen]. + { right. exists O. split; first lia. intros st pm' opro' ?; simplify_eq. destruct (decide (pm' = Disabled)) as [Heq | Hneq]; first by eauto. - left. intros Hit'. + left. intros Hit'. assert (stack_item_tagged_NoDup stk) as Hnodup. - { by eapply Hwf_t. } - specialize (stack_item_tagged_NoDup_eq stk _ _ t Hnodup Hit Hit' eq_refl eq_refl). - intros [= <-]. done. - } - left. + { by eapply Hwf_t. } + specialize (stack_item_tagged_NoDup_eq stk _ _ t Hnodup Hit Hit' eq_refl eq_refl). + intros [= <-]. done. + } + left. destruct (Hcontrolled O ltac:(lia)) as [Hown Hshp]. - { destruct tk; [ | | done]; exists stk, pm, opro; eauto. } - intros i Hi. - destruct (decide (i = O)) as [-> | Hneq]; first done. - simpl. specialize (IH (pred i) ltac:(lia)). - replace ((1 + Z.of_nat (pred i))) with (Z.of_nat i) in IH by lia. + { destruct tk; [ | | done]; exists stk, pm, opro; eauto. } + intros i Hi. + destruct (decide (i = O)) as [-> | Hneq]; first done. + simpl. specialize (IH (pred i) ltac:(lia)). + replace ((1 + Z.of_nat (pred i))) with (Z.of_nat i) in IH by lia. destruct IH as [IH1 IH2]; split; last done. - rewrite IH1. destruct i; done. - - destruct IH as (i & Hi & IH). - right; exists (S i). split; first lia. - replace (Z.of_nat (S i))%Z with (1 + i)%Z by lia. rewrite -shift_loc_assoc. - done. - } - - rewrite Hlen in Hsuccess. + rewrite IH1. destruct i; done. + - destruct IH as (i & Hi & IH). + right; exists (S i). split; first lia. + replace (Z.of_nat (S i))%Z with (1 + i)%Z by lia. rewrite -shift_loc_assoc. + done. + } + - (** success! just proceed with the read *) + rewrite Hlen in Hsuccess. have READ_t : read_mem l (tsize T) σ_t.(shp) = Some v_t. { apply read_mem_values'; first done. by apply Hsuccess. } have Eq_stk : memory_read σ_t.(sst) σ_t.(scs) l (Tagged t) (tsize T) = Some σ_t.(sst). @@ -909,40 +924,41 @@ Proof. rewrite READ in READ_t. simplify_eq. iModIntro. iSplitR; first done. iFrame "HP_t HP_s". - iSplitL "Hbor"; first by destruct σ_t. + iSplitL "Hbor"; first by destruct σ_t. iApply ("Hsim" with "[] Ht Htag"). - iRight. done. - - destruct Hnosuccess as (i & Hi & Hst). + iRight. done. + - (** oh no, the tag isn't there anymore. allocate the tainted ghost state *) + destruct Hnosuccess as (i & Hi & Hst). assert (memory_read σ_t.(sst) σ_t.(scs) l (Tagged t) (tsize T) = None) as Hnone. - { destruct memory_read as [ α' | ] eqn:Hread; last done. - specialize (for_each_lookup_case_2 _ _ _ _ _ Hread) as [Hs _]. - specialize (Hs i ltac:(lia)) as (stk & stk' & Hstk & Hstk' & Hacc1'). + { destruct memory_read as [ α' | ] eqn:Hread; last done. + specialize (for_each_lookup_case_2 _ _ _ _ _ Hread) as [Hs _]. + specialize (Hs i ltac:(lia)) as (stk & stk' & Hstk & Hstk' & Hacc1'). destruct access1 as [[] | ] eqn:Hacc1; last done. - specialize (access1_in_stack _ _ _ _ _ _ Hacc1) as (it & Hit & Htg & Hperm). + specialize (access1_in_stack _ _ _ _ _ _ Hacc1) as (it & Hit & Htg & Hperm). destruct it as [perm tg opro]. - specialize (Hst _ perm opro Hstk) as [Hnotin | ->]; last done. - exfalso. apply Hnotin. naive_solver. - } - iDestruct "Hbor" as "(% & % & % & % & (Hcall_auth & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & #Hsrel & %Hcall_interp & %Htag_interp & %Hwf_s & _)". + specialize (Hst _ perm opro Hstk) as [Hnotin | ->]; last done. + exfalso. apply Hnotin. naive_solver. + } + iDestruct "Hbor" as "(% & % & % & % & (Hcall_auth & Htag_auth & Htag_t_auth & Htag_s_auth) & Htainted & #Hsrel & %Hcall_interp & %Htag_interp & %Hwf_s & _)". iSplitR. { iPureIntro. do 3 eexists. eapply failed_copy_head_step'; done. } iIntros (e_t' efs_t σ_t') "%Hhead_t". specialize (head_copy_inv _ _ _ _ _ _ _ _ Hhead_t) as [-> [(? & ? & _ & ? & _) | (-> & ? & ->)]]; first congruence. - iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Hl". apply Htag_interp in Hl as (? & ? & _). + iPoseProof (tkmap_lookup with "Htag_auth Htag") as "%Hl". apply Htag_interp in Hl as (? & ? & _). iPoseProof (state_rel_stacks_eq with "Hsrel") as "%Heq". iMod (tag_tainted_interp_insert σ_s t (l +â‚— i) with "Htainted") as "[Htainted Htfor]"; first done. { rewrite Heq. intros stk it Hstk Hit. specialize (Hst stk (perm it) (protector it) Hstk) as [Hnotin | ->]; last by right. left. intros Heq'. simplify_eq. destruct it; naive_solver. - } + } iModIntro. iSplitR; first done. - iSplitR "Hsim Htfor Htag Ht"; first last. - { iApply ("Hsim" with "[Htfor] Ht Htag"). + iSplitR "Hsim Htfor Htag Ht"; first last. + { iApply ("Hsim" with "[Htfor] Ht Htag"). iLeft. iExists i. iFrame "Htfor". - iPureIntro. rewrite replicate_length. split; lia. - } - iFrame "HP_t HP_s". + iPureIntro. rewrite replicate_length. split; lia. + } + iFrame "HP_t HP_s". iExists M_call, M_tag, M_t, M_s. iFrame. iFrame "Hsrel". repeat (iSplit; done). Qed. @@ -951,72 +967,73 @@ Lemma source_copy_resolve_deferred v_s v_t v_t' T l t Ψ tk Ï€ : length v_s = tsize T → t $$ tk -∗ l ↦s∗[tk]{t} v_s -∗ - deferred_read v_t v_t' l t -∗ + deferred_read v_t v_t' l t -∗ value_rel v_t v_s -∗ (∀ v_s', value_rel v_t' v_s' -∗ l ↦s∗[tk]{t} v_s -∗ t $$ tk -∗ source_red #v_s' Ï€ Ψ)%E -∗ source_red (Copy (Place l (Tagged t) T)) Ï€ Ψ. Proof. iIntros (Hlen) "Htag Hs Hdef #Hv Hsim". iApply source_red_lift_head_step. iIntros (??????) "[(HP_t & HP_s & Hbor) %Hsafe]". - iModIntro. + iModIntro. iPoseProof (bor_interp_get_state_wf with "Hbor") as "[% %Hwf_s]". destruct Hsafe as [Hpool Hsafe]. specialize (pool_safe_irred _ _ _ _ _ _ _ Hsafe Hpool ltac:(done)) as [(v_s' & Hread_s & (α' & Hstack_s)) | Hfail]; first last. - { iExists _, _. iSplitR. { iPureIntro. eapply failed_copy_head_step'; done. } - iModIntro. iFrame. iApply ("Hsim" with "[Hdef] Hs Htag"). - iApply big_sepL2_forall. rewrite replicate_length. iSplit. + { (* unsuccessful read, but poison is refined by anything *) + iExists _, _. iSplitR. { iPureIntro. eapply failed_copy_head_step'; done. } + iModIntro. iFrame. iApply ("Hsim" with "[Hdef] Hs Htag"). + iApply big_sepL2_forall. rewrite replicate_length. iSplit. - iPoseProof (value_rel_length with "Hv") as "%". - iDestruct "Hdef" as "[(%i & % & _) | ->]"; iPureIntro; lia. - - iIntros (i sc_s ?). rewrite lookup_replicate. iIntros "_ (-> & _)". - destruct sc_s; done. - } - (* successful read -- so this has to match what the ghost state says, since the - preconditions are fulfilled. Moreover, this means we must be in the second + iDestruct "Hdef" as "[(%i & % & _) | ->]"; iPureIntro; lia. + - iIntros (i sc_s ?). rewrite lookup_replicate. iIntros "_ (-> & _)". + destruct sc_s; done. + } + (* successful read -- so this has to match what the ghost state says, since the + preconditions are fulfilled. Moreover, this means we must be in the second case of [deferred_read]. *) - iPoseProof (heap_readN_source with "Hbor Hs Htag") as "%Hcontrolled". + iPoseProof (bor_interp_readN_source with "Hbor Hs Htag") as "%Hcontrolled". assert (∀ i, (i < length v_s)%nat → shp σ_s !! (l +â‚— i) = v_s !! i ∧ bor_state_own (l +â‚— i) t tk σ_s) as Hcontrol'. { - intros i Hi. + intros i Hi. destruct (Hcontrolled i Hi) as [Hown Hshp]. - { specialize (for_each_lookup_case_2 _ _ _ _ _ Hstack_s) as [Hs _]. - specialize (Hs i ltac:(lia)) as (stk0 & stk' & Hstk0 & Hstk' & Hacc1'). + { specialize (for_each_lookup_case_2 _ _ _ _ _ Hstack_s) as [Hs _]. + specialize (Hs i ltac:(lia)) as (stk0 & stk' & Hstk0 & Hstk' & Hacc1'). destruct access1 as [[] | ] eqn:Hacc1; last done. - specialize (access1_in_stack _ _ _ _ _ _ Hacc1) as (it & Hit & Htg & Hperm). - destruct it as [perm tg opro]. simpl in *. simplify_eq. - destruct tk; last done. - all: exists stk0, perm, opro; done. - } + specialize (access1_in_stack _ _ _ _ _ _ Hacc1) as (it & Hit & Htg & Hperm). + destruct it as [perm tg opro]. simpl in *. simplify_eq. + destruct tk; last done. + all: exists stk0, perm, opro; done. + } split; last done. rewrite Hshp list_lookup_lookup_total; first done. - apply lookup_lt_is_Some_2. lia. - } + apply lookup_lt_is_Some_2. lia. + } have READ_s : read_mem l (tsize T) σ_s.(shp) = Some v_s. { apply read_mem_values'; first lia. rewrite -Hlen. apply Hcontrol'. } have Eq_stk : memory_read σ_s.(sst) σ_s.(scs) l (Tagged t) (tsize T) = Some σ_s.(sst). { apply memory_read_access1. intros i Hi. - specialize (Hcontrol' i ltac:(lia)) as (_ & Hown). - destruct (bor_state_own_some_stack _ _ _ _ Hown) as (stk & Heq). + specialize (Hcontrol' i ltac:(lia)) as (_ & Hown). + destruct (bor_state_own_some_stack _ _ _ _ Hown) as (stk & Heq). eexists; split; first done. eapply bor_state_own_access1_read; done. - } - iExists _, _. iSplitR. { iPureIntro. eapply copy_head_step'; done. } - iModIntro. - iFrame. - iDestruct "Hdef" as "[(%i & %Hi & Htainted) | ->]"; first last. - { iSplitL "Hbor"; first by destruct σ_s. iApply ("Hsim" with "Hv Hs Htag"). } - iDestruct "Hbor" as "(% & % & % & % & (Hcall_auth & Htag_auth & Htag_t_auth & Htag_s_auth) & Htaint_interp & #Hsrel & %Hcall_interp & %Htag_interp & _ & %Hwf_t)". + } + iExists _, _. iSplitR. { iPureIntro. eapply copy_head_step'; done. } + iModIntro. + iFrame. + iDestruct "Hdef" as "[(%i & %Hi & Htainted) | ->]"; first last. + { iSplitL "Hbor"; first by destruct σ_s. iApply ("Hsim" with "Hv Hs Htag"). } + iDestruct "Hbor" as "(% & % & % & % & (Hcall_auth & Htag_auth & Htag_t_auth & Htag_s_auth) & Htaint_interp & #Hsrel & %Hcall_interp & %Htag_interp & _ & %Hwf_t)". iPoseProof (tag_tainted_interp_lookup with "Htainted Htaint_interp") as "[%Ht %Hstk]". iPoseProof (value_rel_length with "Hv") as "%". - exfalso. - specialize (for_each_lookup_case_2 _ _ _ _ _ Hstack_s) as [Hs _]. - specialize (Hs i ltac:(lia)) as (stk0 & stk' & Hstk0 & Hstk' & Hacc1'). + exfalso. + specialize (for_each_lookup_case_2 _ _ _ _ _ Hstack_s) as [Hs _]. + specialize (Hs i ltac:(lia)) as (stk0 & stk' & Hstk0 & Hstk' & Hacc1'). destruct access1 as [[] | ] eqn:Hacc1; last done. - specialize (access1_in_stack _ _ _ _ _ _ Hacc1) as (it & Hit & Htg & Hperm). + specialize (access1_in_stack _ _ _ _ _ _ Hacc1) as (it & Hit & Htg & Hperm). destruct it as [perm tg opro]. simpl in *. - specialize (Hstk stk0 _ Hstk0 Hit) as [Hneq | Hdis]; last done. - simpl in Hneq. congruence. + specialize (Hstk stk0 _ Hstk0 Hit) as [Hneq | Hdis]; last done. + simpl in Hneq. congruence. Qed. -(** Alloc *) +(** ** Alloc *) Lemma sim_alloc_local T Φ Ï€ : (∀ t l, t $$ tk_local -∗ l ↦t∗[tk_local]{t} replicate (tsize T) ScPoison -∗ @@ -1034,11 +1051,11 @@ Proof. specialize (head_alloc_inv _ _ _ _ _ _ Hhead_t) as (-> & -> & ->). set (l_s := (fresh_block σ_s.(shp), 0)). set (σ_s' := (mkState (init_mem l_s (tsize T) σ_s.(shp)) (init_stacks σ_s.(sst) l_s (tsize T) (Tagged σ_t.(snp))) σ_s.(scs) (S σ_s.(snp)) σ_s.(snc))). - assert (Hhead_s : language.head_step P_s (Alloc T) σ_s (Place l_s (Tagged σ_t.(snp)) T) σ_s' []). + assert (Hhead_s : language.head_step P_s (Alloc T) σ_s (Place l_s (Tagged σ_t.(snp)) T) σ_s' []). { subst σ_s'. destruct Hp as (_ & <- & _). econstructor 2; econstructor. } - iMod (heap_local_alloc _ _ T with "Hbor") as "(Hbor & Htag & Htarget & Hsource)". + iMod (bor_interp_alloc_local _ _ T with "Hbor") as "(Hbor & Htag & Htarget & Hsource)". { eapply head_step_wf; [ apply Hhead_t | apply Hwf]. } - { eapply head_step_wf; last apply (proj2 Hwf). apply Hhead_s. } + { eapply head_step_wf; last apply (proj2 Hwf). apply Hhead_s. } iModIntro. iExists (Place l_s (Tagged (σ_t.(snp))) T), [], σ_s'. iFrame. iSplitR; first done. @@ -1047,8 +1064,9 @@ Proof. iApply ("Hsim" with "Htag Htarget Hsource"). Qed. - -Lemma bor_interp_free_local t v_t v_s l σ_t σ_s α' n : +(** ** Free *) +(* local ownership makes strong assertions: we also have to deallocate the corresponding ghost state. *) +Lemma bor_interp_free_local t v_t v_s l σ_t σ_s α' n : memory_deallocated (sst σ_t) (scs σ_t) l (Tagged t) n = Some α' → memory_deallocated (sst σ_s) (scs σ_s) l (Tagged t) n = Some α' → length v_t = n → @@ -1057,132 +1075,131 @@ Lemma bor_interp_free_local t v_t v_s l σ_t σ_s α' n : let σ_s' := mkState (free_mem l n σ_s.(shp)) α' σ_s.(scs) σ_s.(snp) σ_s.(snc) in state_wf σ_t' → state_wf σ_s' → - t $$ tk_local -∗ + t $$ tk_local -∗ l ↦t∗[tk_local]{t} v_t -∗ l ↦s∗[tk_local]{t} v_s -∗ bor_interp sc_rel σ_t σ_s ==∗ t $$ tk_local ∗ bor_interp sc_rel σ_t' σ_s'. -Proof. +Proof. intros Hstack_t Hstack_s Hlen_t Hlen_s σ_t' σ_s' Hwf_t' Hwf_s'. - iIntros "Htag Ht Hs Hbor". + iIntros "Htag Ht Hs Hbor". iDestruct "Hbor" as "(% & % & % & % & (Hcall_auth & Htag_auth & Htag_t_auth & Htag_s_auth) & Htaint_interp & #Hsrel & %Hcall_interp & %Htag_interp & %Hwf_s & %Hwf_t)". - iMod (ghost_map_array_tag_delete with "Htag_t_auth Ht") as "Htag_t_auth". + iMod (ghost_map_array_tag_delete with "Htag_t_auth Ht") as "Htag_t_auth". iMod (ghost_map_array_tag_delete with "Htag_s_auth Hs") as "Htag_s_auth". - iModIntro. iFrame "Htag". + iModIntro. iFrame "Htag". iExists M_call, M_tag, (M_t ∖ array_tag_map l t v_t), (M_s ∖ array_tag_map l t v_s). iFrame. - iSplitL. + iSplitL. { (* tainted *) - iApply (tag_tainted_interp_preserve σ_s with "Htaint_interp"). { simpl. lia. } - intros l' stk' Hstk' it Hit. right. right. + iApply (tag_tainted_interp_preserve σ_s with "Htaint_interp"). { simpl. lia. } + intros l' stk' Hstk' it Hit. right. right. specialize (for_each_dealloc_lookup_Some _ _ _ _ _ Hstack_s _ _ Hstk') as (_ & Hstk). eauto. - } - iSplitL. + } + iSplitL. { (* state rel *) (* TODO: partially duplicated from the refl lemma. prove more general lemma? *) - iDestruct "Hsrel" as "(%Hdom_eq & %Hsst_eq & %Hsnp_eq & %Hsnc_eq & %Hscs_eq & Hsrel)". - iSplitR. { iPureIntro. simpl. apply free_mem_dom. done. } - simpl. do 4 (iSplitR; first done). - iIntros (l' (sc & Hsome)). - destruct (free_mem_lookup_case l' l n σ_t.(shp)) as [[Hi Heq] | (i & _ & -> & ?)]; last congruence. + iDestruct "Hsrel" as "(%Hdom_eq & %Hsst_eq & %Hsnp_eq & %Hsnc_eq & %Hscs_eq & Hsrel)". + iSplitR. { iPureIntro. simpl. apply free_mem_dom. done. } + simpl. do 4 (iSplitR; first done). + iIntros (l' (sc & Hsome)). + destruct (free_mem_lookup_case l' l n σ_t.(shp)) as [[Hi Heq] | (i & _ & -> & ?)]; last congruence. rewrite Heq in Hsome. iDestruct ("Hsrel" $! l' with "[]") as "[Hpubl | (%t' & %Hprivl)]"; first by eauto. - + iLeft. iIntros (sc_t Hsc_t). simpl in *. + + iLeft. iIntros (sc_t Hsc_t). simpl in *. rewrite Heq in Hsc_t. rewrite Hsome in Hsc_t. injection Hsc_t as <-. iDestruct ("Hpubl" $! sc Hsome) as (sc_s) "[%Hsc_s Hscr]". iExists sc_s. iSplitR; last done. - iPureIntro. + iPureIntro. destruct (free_mem_lookup_case l' l n σ_s.(shp)) as [[_ Heq'] | (i' & Hi' & -> & _)]. 2: { specialize (Hi i' Hi'). congruence. } - rewrite Heq' Hsc_s. done. - + iRight. iPureIntro. exists t'. + rewrite Heq' Hsc_s. done. + + iRight. iPureIntro. exists t'. destruct Hprivl as (tk & Htk & (s & Hs) & Hpriv). exists tk. split_and!; [done | | done]. exists s. apply lookup_difference_Some. split; first done. destruct (decide (t = t')) as [<- | Hneq]; last by apply array_tag_map_lookup_None. - apply array_tag_map_lookup_None'. intros i Hi'. rewrite Hlen_t in Hi'. + apply array_tag_map_lookup_None'. intros i Hi'. rewrite Hlen_t in Hi'. specialize (Hi i Hi'); done. - } - iSplitL. + } + iSplitL. { (* call interp *) (* TODO: duplicated with the refl lemma *) - iPureIntro. iIntros (c M' Hc). - destruct (Hcall_interp c M' Hc) as (? & HM'). split; first done. + iPureIntro. iIntros (c M' Hc). + destruct (Hcall_interp c M' Hc) as (? & HM'). split; first done. intros t' L Ht'. specialize (HM' t' L Ht') as (? & HL). split; first done. intros l' (stk & pm & Hstk & Hit & Hpm)%HL. exists stk, pm. split_and!; [ | done..]. destruct (for_each_true_lookup_case_2 _ _ _ _ _ Hstack_t) as [EQ1 EQ2]. (* from Hstack_s, l cannot be in the affected range because it is protected by c, so α' !! l = σt.(sst) !! l. *) destruct (block_case l l' n) as [Hneq|(i & Hi & ->)]. - + rewrite EQ2//. + + rewrite EQ2//. + exfalso. clear EQ2. specialize (EQ1 _ Hi) as (stk1 & stk' & Eqstk1 & Eqstk' & Hdealloc). rewrite Eqstk1 in Hstk. simplify_eq. - move : Hdealloc. destruct (dealloc1 stk (Tagged t) σ_t.(scs)) eqn:Eqd; last done. + move : Hdealloc. destruct (dealloc1 stk (Tagged t) σ_t.(scs)) eqn:Eqd; last done. intros _. destruct (dealloc1_Some stk (Tagged t) σ_t.(scs)) as (it & Eqit & ? & FA & GR). { by eexists. } rewrite ->Forall_forall in FA. apply (FA _ Hit). rewrite /is_active_protector /= /is_active bool_decide_true //. - } - iSplitL. + } + iSplitL. { (* tag interp *) destruct Htag_interp as (Htag_interp & Hdom_t & Hdom_s). iPureIntro. split_and!. { intros t' tk Ht. simpl. specialize (Htag_interp _ _ Ht) as (? & ? & Hcontrol_t & Hcontrol_s & Hag). split_and!; [done | done | | | ]. - + intros l' sc_t. + + intros l' sc_t. rewrite lookup_difference_Some. intros [Hsc_t%Hcontrol_t Hnotin%array_tag_map_lookup_None2]. eapply loc_controlled_dealloc_update; [ apply Hstack_t | done | | done]. - intros [[= <-] (i & -> & Hi)]. - destruct Hnotin as [? | Hi']; first congruence. - rewrite Hlen_t in Hi'. apply Hi' in Hi. congruence. - + intros l' sc_s. + intros [[= <-] (i & -> & Hi)]. + destruct Hnotin as [? | Hi']; first congruence. + rewrite Hlen_t in Hi'. apply Hi' in Hi. congruence. + + intros l' sc_s. rewrite lookup_difference_Some. intros [Hsc_t%Hcontrol_s Hnotin%array_tag_map_lookup_None2]. eapply loc_controlled_dealloc_update; [ apply Hstack_s | done | | done]. - intros [[= <-] (i & -> & Hi)]. - destruct Hnotin as [? | Hi']; first congruence. - rewrite Hlen_s in Hi'. apply Hi' in Hi. congruence. + intros [[= <-] (i & -> & Hi)]. + destruct Hnotin as [? | Hi']; first congruence. + rewrite Hlen_s in Hi'. apply Hi' in Hi. congruence. + apply dom_agree_on_tag_difference; first done. destruct (decide (t = t')) as [<- | Hneq]. - * apply dom_agree_on_tag_array_tag_map. lia. + * apply dom_agree_on_tag_array_tag_map. lia. * apply dom_agree_on_tag_not_elem; apply array_tag_map_lookup_None; done. - } + } all: intros t' l'; rewrite lookup_difference_is_Some; intros [? _]; eauto. - } + } eauto. Qed. -(* local ownership makes strong assertions: we also have to deallocate the corresponding ghost state. *) -Lemma sim_free_local l t T v_t v_s Φ Ï€ : - length v_t = tsize T → +Lemma sim_free_local l t T v_t v_s Φ Ï€ : + length v_t = tsize T → length v_s = tsize T → - t $$ tk_local -∗ + t $$ tk_local -∗ l ↦t∗[tk_local]{t} v_t -∗ - l ↦s∗[tk_local]{t} v_s -∗ + l ↦s∗[tk_local]{t} v_s -∗ (t $$ tk_local -∗ #[☠] ⪯{Ï€, Ω} #[☠] [{ Φ }]) -∗ Free (Place l (Tagged t) T) ⪯{Ï€, Ω} Free (Place l (Tagged t) T) [{ Φ }]. -Proof. - iIntros (Hlen_t Hlen_s) "Htag Ht Hs Hsim". +Proof. + iIntros (Hlen_t Hlen_s) "Htag Ht Hs Hsim". iApply sim_lift_head_step_both. iIntros (??????) "[(HP_t & HP_s & Hbor) %Hsafe]". destruct Hsafe as [Hthread Hsafe]. specialize (pool_safe_irred _ _ _ _ _ _ _ Hsafe Hthread ltac:(done)) as (Hmem_s & (α' & Hstack_s)). iPoseProof (bor_interp_get_pure with "Hbor") as "%Hp". destruct Hp as (Hsst_eq & Hsnp_eq & Hsnc_eq & Hscs_eq & Hwf_s & Hwf_t & Hdom_eq). - iModIntro. + iModIntro. iSplitR. - { iPureIntro. eexists _, _, _. eapply dealloc_head_step'; first apply Hwf_t. - - intros i. rewrite -Hmem_s. rewrite -!elem_of_dom Hdom_eq. done. - - erewrite <-Hstack_s. rewrite Hsst_eq Hscs_eq. done. + { iPureIntro. eexists _, _, _. eapply dealloc_head_step'; first apply Hwf_t. + - intros i. rewrite -Hmem_s. rewrite -!elem_of_dom Hdom_eq. done. + - erewrite <-Hstack_s. rewrite Hsst_eq Hscs_eq. done. } iIntros (e_t' efs_t σ_t' Hhead_t). - specialize (head_free_inv _ _ _ _ _ _ _ _ Hhead_t) as (α'_t & Hstack_t & Hmem_t & -> & -> & ->). + specialize (head_free_inv _ _ _ _ _ _ _ _ Hhead_t) as (α'_t & Hstack_t & Hmem_t & -> & -> & ->). assert (α'_t = α') as ->. { move : Hstack_t Hstack_s. rewrite Hsst_eq Hscs_eq => -> [= ->] //. } iMod (bor_interp_free_local with "Htag Ht Hs Hbor") as "[Htag Hbor]"; [done | done | done | done | ..]. - { eapply head_step_wf; done. } + { eapply head_step_wf; done. } { eapply head_step_wf; [eapply (dealloc_head_step' P_s); done | done ]. } - iModIntro. iExists _, _, _. + iModIntro. iExists _, _, _. iSplitR. { iPureIntro. eapply dealloc_head_step'; done. } iFrame. iSplitL; last done. by iApply "Hsim". Qed. diff --git a/theories/stacked_borrows/steps_refl.v b/theories/stacked_borrows/steps_refl.v index 04b21ee35d72eded51b493c451289700e19298bf..2d658a71309d7b2e866759c768245cd9ea967f4c 100644 --- a/theories/stacked_borrows/steps_refl.v +++ b/theories/stacked_borrows/steps_refl.v @@ -1,17 +1,16 @@ From iris.proofmode Require Export tactics. -From iris.bi.lib Require Import fractional. From iris.base_logic.lib Require Import ghost_map. From simuliris.base_logic Require Export gen_sim_prog. From simuliris.simulation Require Export slsls. From simuliris.simulation Require Import lifting. -From iris.prelude Require Import options. From simuliris.stacked_borrows Require Import tkmap_view. From simuliris.stacked_borrows Require Export defs. From simuliris.stacked_borrows Require Import steps_progress steps_retag steps_inv. -From simuliris.stacked_borrows Require Import heap. +From simuliris.stacked_borrows Require Import logical_state inv_accessors. +From iris.prelude Require Import options. Section lifting. -Context `{!sborG Σ}. +Context `{!sborGS Σ}. Implicit Types P Q : iProp Σ. Implicit Types Φ : expr → expr → iProp Σ. Implicit Types σ σ_s σ_t : state. @@ -67,10 +66,10 @@ Proof. - (* state rel *) rewrite -{2}(map_empty_union M_t). subst σ_s' α' nt. rewrite -{2}Hsst_eq. - iApply sim_alloc_state_rel_update; last done. + iApply state_rel_alloc_update; last done. intros t (s & Hs) ->. congruence. - (* call interp *) - iPureIntro. apply sim_alloc_call_set_interp_update; done. + iPureIntro. apply call_set_interp_alloc_update; done. - (* tag interp *) iPureIntro. destruct Htag_interp as (Htag_interp & Hdom_t & Hdom_s). split_and!. { simpl. intros t tk. rewrite lookup_insert_Some. intros [[<- [= <-]] | [Hneq Hsome]]. @@ -199,6 +198,7 @@ Proof. - iPureIntro. by eapply head_step_wf. Qed. +(** TODO: generalize, move, and use it for the opt lemmas too *) Lemma sim_copy_public_controlled_update σ l l' (bor : tag) (T : type) (α' : stacks) (t : ptr_id) (tk : tag_kind) sc : memory_read σ.(sst) σ.(scs) l bor (tsize T) = Some α' → state_wf σ → @@ -392,6 +392,7 @@ Proof. Qed. (** Write *) +(* TODO: generalize, move, and use for opt steps too *) Lemma loc_controlled_write_public σ bor tk l l' T α' sc v t : state_wf σ → (bor = Tagged t → tk = tk_pub) → @@ -647,9 +648,9 @@ Proof. - (* old tags are preserved *) simpl. specialize (Htag_interp _ _ Hsome') as (? & ? & Hcontrolled_t & Hcontrolled_s & Hdom). split_and!; [lia | lia | | | ]. - + intros. eapply retag_loc_controlled_preserved; [ done | done | | done | by apply Hcontrolled_t]. + + intros. eapply loc_controlled_retag_update; [ done | done | | done | by apply Hcontrolled_t]. intros <-. move : Hpub. rewrite /untagged_or_public. congruence. - + intros. eapply retag_loc_controlled_preserved; [ done | done | | done | by apply Hcontrolled_s]. + + intros. eapply loc_controlled_retag_update; [ done | done | | done | by apply Hcontrolled_s]. intros <-. move : Hpub. rewrite /untagged_or_public. congruence. + done. }