Commit fbb040de by Dan Frumin

### Add support for the prophecy variables (on the LHS)

parent 042fdf1a
 ... ... @@ -4,6 +4,7 @@ theories/prelude/ctx_subst.v theories/prelude/properness.v theories/prelude/asubst.v theories/prelude/bijections.v theories/prelude/steps.v theories/logic/spec_ra.v theories/logic/spec_rules.v ... ... @@ -42,3 +43,4 @@ theories/examples/stack/CG_stack.v theories/examples/stack/FG_stack.v theories/examples/stack/refinement.v theories/examples/various.v theories/examples/lateearlychoice.v
 From iris.heap_lang Require Import lifting. From reloc Require Import reloc. Definition rand: val := λ: "_", let: "y" := ref #false in Fork ("y" <- #true) ;; !"y". Definition earlyChoice: val := λ: "x", let: "r" := rand #() in "x" <- #0 ;; "r". Definition lateChoice': val := λ: "x", let: "p" := NewProph in "x" <- #0 ;; let: "r" := rand #() in resolve_proph: "p" to: "r" ;; "r". Definition lateChoice: val := λ: "x", "x" <- #0 ;; let: "r" := rand #() in "r". Section proof. Context `{relocG Σ}. Lemma refines_rand_r (b : bool) E K e A : nclose relocN ⊆ E → (REL e << fill K (of_val #b) @ E : A) -∗ REL e << fill K (rand #()) @ E : A. Proof. iIntros (?) "He". rel_rec_r. rel_alloc_r y as "Hy". repeat rel_pure_r. rel_fork_r i as "Hi". repeat rel_pure_r. iApply refines_spec_ctx. iDestruct 1 as (ρ) "#Hρ". destruct b. - tp_store i. rel_load_r. iApply "He". - rel_load_r. iApply "He". Qed. Lemma refines_rand_l K t A : ▷ (∀ (b: bool), REL fill K (of_val #b) << t : A) -∗ REL fill K (rand #()) << t : A. Proof. iIntros "He". rel_rec_l. rel_alloc_l y as "Hy". iMod (inv_alloc (nroot.@"randN") _ (∃ (b: bool), y ↦ #b)%I with "[Hy]") as "#Hinv"; first by eauto. repeat rel_pure_l. rel_fork_l. iModIntro. iSplitR. - iNext. iInv (nroot.@"randN") as (b) "Hy" "Hcl"; wp_store; iMod ("Hcl" with "[Hy]") as "_"; eauto with iFrame. - iNext. repeat rel_pure_l. rel_load_l_atomic. iInv (nroot.@"randN") as (b) "Hy" "Hcl". iModIntro. iExists _; iFrame. iNext. iIntros "Hy". iMod ("Hcl" with "[Hy]") as "_"; eauto with iFrame. Qed. Definition val_to_bool (v : option val) : bool := match v with | Some (LitV (LitBool b)) => b | _ => true end. Lemma late'_early_choice : REL lateChoice' << earlyChoice : ref lrel_int → lrel_bool. Proof. unfold lateChoice', earlyChoice. iApply refines_arrow_val. iModIntro. iIntros (x x') "#Hxx". rel_rec_l. rel_rec_r. rel_bind_l NewProph. iApply refines_wp_l. iApply wp_new_proph; first done. iNext. iIntros (v p) "Hp /=". repeat rel_pure_l. rel_apply_r (refines_rand_r (val_to_bool v)). repeat rel_pure_r. iApply (refines_seq lrel_unit). { iApply refines_store. - iApply refines_ret. iApply "Hxx". - rel_values. } rel_apply_l refines_rand_l. iNext. iIntros (b). repeat rel_pure_l. rel_bind_l (resolve_proph: _ to: _)%E. iApply refines_wp_l. iApply (wp_resolve_proph with "Hp"). iNext. iIntros (->). iSimpl. repeat rel_pure_l. rel_values. Qed. Lemma early_late_choice : REL earlyChoice << lateChoice : ref lrel_int → lrel_bool. Proof. unfold lateChoice, earlyChoice. iApply refines_arrow_val. iModIntro. iIntros (x x') "#Hxx". rel_rec_l. rel_rec_r. rel_apply_l refines_rand_l. iNext. iIntros (b). repeat rel_pure_l. iApply (refines_seq lrel_unit). { iApply refines_store. - iApply refines_ret. iApply "Hxx". - rel_values. } rel_apply_r (refines_rand_r b). repeat rel_pure_r. rel_values. Qed. Lemma late_late'_choice : REL lateChoice << lateChoice' : ref lrel_int → lrel_bool. Proof. unfold lateChoice, lateChoice'. iApply refines_arrow_val. iModIntro. iIntros (x x') "#Hxx". rel_rec_l. rel_rec_r. rel_apply_r refines_newproph_r. iIntros (p v) "Hp /=". repeat rel_pure_r. iApply (refines_seq lrel_unit with "[Hxx]"). { iApply refines_store. - iApply refines_ret. iApply "Hxx". - rel_values. } rel_apply_l refines_rand_l. iNext. iIntros (b). repeat rel_pure_l. rel_apply_r (refines_rand_r b). repeat rel_pure_r. rel_apply_r (refines_resolveproph_r with "Hp"). repeat rel_pure_r. rel_values. Qed. End proof. Theorem late_early_ctx_refinement : ∅ ⊨ lateChoice ≤ctx≤ earlyChoice : ref TNat → TBool. Proof. eapply (ctx_refines_transitive ∅ (ref TNat → TBool)). - eapply (refines_sound relocΣ). iIntros (? Δ). iApply late_late'_choice. - eapply (refines_sound relocΣ). iIntros (? Δ). iApply late'_early_choice. Qed. Theorem early_late_ctx_refinement : ∅ ⊨ earlyChoice ≤ctx≤ lateChoice : ref TNat → TBool. Proof. eapply (refines_sound relocΣ). iIntros (? Δ). iApply early_late_choice. Qed.
 ... ... @@ -5,6 +5,7 @@ From iris.base_logic.lib Require Import auth. From iris.proofmode Require Import tactics. From iris.heap_lang Require Export adequacy. From reloc.logic Require Export spec_ra model. From reloc.prelude Require Import steps. Class relocPreG Σ := RelocPreG { reloc_preG_heap :> heapPreG Σ; ... ... @@ -29,16 +30,18 @@ Lemma refines_adequate Σ `{relocPreG Σ} Proof. intros HA Hlog. eapply (heap_adequacy Σ _); iIntros (Hinv). iMod (own_alloc (● (to_tpool [e'], to_gen_heap (heap σ)) ⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅) : cfgUR))) iMod (own_alloc (● (to_tpool [e'], (to_gen_heap (heap σ), to_proph_map ∅)) ⋅ ◯ ((to_tpool [e'] : tpoolUR, ε) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]". { apply auth_valid_discrete_2. split=>//. - apply prod_included. split=>///=. apply: ucmra_unit_least. - split=>//. apply to_tpool_valid. apply to_gen_heap_valid. } - split=>//. apply to_tpool_valid. split=>///=. apply to_gen_heap_valid. } set (Hcfg := RelocG _ _ (CFGSG _ _ γc)). iMod (inv_alloc specN _ (spec_inv ([e'], σ)) with "[Hcfg1]") as "#Hcfg". { iNext. iExists [e'], σ. eauto. } { iNext. iExists [e'], σ, [], ∅. iFrame. iPureIntro. split =>//. exists 0%nat. econstructor. } iApply wp_fupd. iApply wp_wand_r. iSplitL. - iPoseProof (Hlog _) as "Hrel". ... ... @@ -52,15 +55,20 @@ Proof. iDestruct 1 as (v') "[Hj Hinterp]". rewrite HA. iDestruct "Hinterp" as %Hinterp. iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'. iInv specN as (tp σ' κs R) ">(Hown & Hproph & Hsteps)" "Hclose"; iDestruct "Hsteps" as %Hsteps'. rewrite tpool_mapsto_eq /tpool_mapsto_def /=. iDestruct (own_valid_2 with "Hown Hj") as %Hvalid. move: Hvalid=> /auth_valid_discrete_2 [/prod_included [/tpool_singleton_included Hv2 _] _]. destruct tp as [|? tp']; simplify_eq/=. iMod ("Hclose" with "[-]") as "_". { iExists (_ :: tp'), σ'. eauto. } { iExists (_ :: tp'), σ', κs, R. eauto. } iIntros "!> !%"; eauto. destruct Hsteps' as [n Hsteps']. do 3 eexists. split=>//. eapply (relations.nsteps_rtc n). eapply erased_step_nsteps; eauto. Qed. Theorem refines_typesafety Σ `{relocPreG Σ} e e' e1 ... ...
 ... ... @@ -109,6 +109,39 @@ Section rules. by iApply "Hlog". Qed. Lemma refines_newproph_r E K t A (Hmasked : nclose specN ⊆ E) : (∀ (p : proph_id) (v : option val), prophS p v -∗ REL t << fill K (of_val #p) @ E : A)%I -∗ REL t << fill K NewProph @ E : A. Proof. iIntros "Hlog". pose (Φ := (fun w => ∃ (p : proph_id) (v : option val), ⌜w = (# p)⌝ ∗ prophS p v)%I). iApply (refines_step_r Φ); simpl; auto. { cbv[Φ]. iIntros (ρ j K') "#Hs Hj /=". iMod (step_newproph with "[\$Hs \$Hj]") as (p v) "[Hp Hj]". done. iModIntro. iExists _. iFrame. iExists _,_. iFrame. eauto. } iIntros (v') "He'". iDestruct "He'" as (p v) "[% Hp]". subst. by iApply "Hlog". Qed. Lemma refines_resolveproph_r E K t p (v : option val) w A (Hmasked : nclose specN ⊆ E) : prophS p v -∗ (REL t << fill K (of_val #()) @ E : A)%I -∗ REL t << fill K (ResolveProph #p (of_val w)) @ E : A. Proof. iIntros "Hp Hlog". pose (Φ := (fun w => ⌜w = #()⌝ : iProp Σ)%I). iApply (refines_step_r Φ with "[Hp]"); simpl; auto. { cbv[Φ]. iIntros (ρ j K') "#Hs Hj /=". iMod (step_resolveproph with "[\$Hs \$Hj \$Hp]") as "Hj". done. iModIntro. iExists _. iFrame. eauto. } iIntros (v') "He'". iDestruct "He'" as %->. by iApply "Hlog". Qed. Lemma refines_alloc_r E K e v t A (Hmasked : nclose specN ⊆ E) : IntoVal e v → ... ...
 ... ... @@ -12,9 +12,12 @@ Definition specN := relocN .@ "spec". (** The CMRA for the heap of the specification. *) Definition tpoolUR : ucmraT := gmapUR nat (exclR exprC). Definition cfgUR := prodUR tpoolUR (gen_heapUR loc val). Definition cfgUR : ucmraT := prodUR tpoolUR (prodUR (gen_heapUR loc val) (proph_mapUR proph_id val)). (** The CMRA for the thread pool. *) (* DF: would it be better to split this into multiple gFunctors? *) Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }. Class relocG Σ := RelocG { relocG_heapG :> heapG Σ; ... ... @@ -27,14 +30,21 @@ Section definitionsS. Context `{cfgSG Σ, invG Σ}. Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ := own cfg_name (◯ (∅, {[ l := (q, to_agree v) ]})). own cfg_name (◯ (∅, ({[ l := (q, to_agree v) ]}, ∅))). Definition heapS_mapsto_aux : { x | x = @heapS_mapsto_def }. by eexists. Qed. Definition heapS_mapsto := proj1_sig heapS_mapsto_aux. Definition heapS_mapsto_eq : @heapS_mapsto = @heapS_mapsto_def := proj2_sig heapS_mapsto_aux. Definition prophS_def (p : proph_id) (v : option val) : iProp Σ := own cfg_name (◯ (∅, (∅, {[ p := Excl v ]}))). Definition prophS_aux : { x | x = @prophS_def }. by eexists. Qed. Definition prophS := proj1_sig prophS_aux. Definition prophS_eq : @prophS = @prophS_def := proj2_sig prophS_aux. Definition tpool_mapsto_def (j : nat) (e: expr) : iProp Σ := own cfg_name (◯ ({[ j := Excl e ]}, ∅)). own cfg_name (◯ ({[ j := Excl e ]}, ε)). Definition tpool_mapsto_aux : { x | x = @tpool_mapsto_def }. by eexists. Qed. Definition tpool_mapsto := proj1_sig tpool_mapsto_aux. Definition tpool_mapsto_eq : ... ... @@ -43,8 +53,13 @@ Section definitionsS. Definition mkstate (σ : gmap loc val) (κs : gset proph_id) := {| heap := σ; used_proph_id := κs |}. Definition spec_inv ρ : iProp Σ := (∃ tp σ, own cfg_name (● (to_tpool tp, to_gen_heap (heap σ))) ∗ ⌜rtc erased_step ρ (tp,σ)⌝)%I. (∃ tp σ (κs : list (proph_id * val)) R, own cfg_name (● (to_tpool tp, (to_gen_heap (heap σ), to_proph_map R))) ∗ ⌜first_resolve_in_list R κs ∧ dom (gset _) R ⊆ (used_proph_id σ)⌝ ∗ ⌜∃ n, nsteps (Λ:=heap_lang) n ρ (reverse κs) (tp,σ)⌝)%I. Definition spec_ctx (ρ : cfg heap_lang) : iProp Σ := inv specN (spec_inv ρ). ... ... @@ -127,7 +142,7 @@ Section mapsto. Global Instance mapsto_fractional l v : Fractional (λ q, l ↦ₛ{q} v)%I. Proof. intros p q. rewrite heapS_mapsto_eq -own_op -auth_frag_op. by rewrite pair_op op_singleton pair_op agree_idemp right_id. by rewrite !pair_op op_singleton pair_op agree_idemp !right_id. Qed. Global Instance mapsto_as_fractional l q v : AsFractional (l ↦ₛ{q} v) (λ q, l ↦ₛ{q} v)%I q. ... ... @@ -138,8 +153,9 @@ Section mapsto. apply bi.wand_intro_r. rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid. f_equiv=> /auth_own_valid /=. rewrite pair_op op_singleton right_id pair_op. move=> [_ Hv]. move:Hv => /=. (* TODO: this is a bit slow *) rewrite !pair_op op_singleton pair_op !(right_id ∅). move=> [_ [Hv _]]. move:Hv => /=. rewrite singleton_valid. by intros [_ ?%agree_op_invL']. Qed. ... ... @@ -147,7 +163,7 @@ Section mapsto. Lemma mapsto_valid l q v : l ↦ₛ{q} v -∗ ✓ q. Proof. rewrite heapS_mapsto_eq /heapS_mapsto_def own_valid !uPred.discrete_valid. apply pure_mono=> /auth_own_valid /= [_ Hfoo]. apply pure_mono=> /auth_own_valid /= [_ [Hfoo _]]. revert Hfoo. simpl. rewrite singleton_valid. by intros [? _]. Qed. ... ...
 ... ... @@ -2,8 +2,10 @@ (** Rules for updating the specification program. *) From iris.algebra Require Import auth frac agree gmap list. From iris.proofmode Require Import tactics. From iris.heap_lang Require Export lang notation. From iris.heap_lang Require Export lang notation proph_map. From reloc.logic Require Export spec_ra. From reloc.prelude Require Import steps. Import uPred. Section rules. Context `{relocG Σ}. ... ... @@ -19,36 +21,25 @@ Section rules. Local Hint Resolve to_tpool_insert. Local Hint Resolve to_tpool_insert'. Local Hint Resolve tpool_singleton_included. Local Hint Constructors nsteps. (** * Aux. lemmas *) Lemma step_insert K tp j e σ κ e' σ' efs : tp !! j = Some (fill K e) → head_step e σ κ e' σ' efs → erased_step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ'). step (tp, σ) κ (<[j:=fill K e']> tp ++ efs, σ'). Proof. intros. rewrite -(take_drop_middle tp j (fill K e)) //. rewrite insert_app_r_alt take_length_le ?Nat.sub_diag /=; eauto using lookup_lt_Some, Nat.lt_le_incl. rewrite -(assoc_L (++)) /=. eexists. rewrite -(assoc_L (++)) /=. eapply step_atomic; eauto. by apply: Ectx_step'. Qed. Lemma step_insert_no_fork K tp j e σ κ e' σ' : tp !! j = Some (fill K e) → head_step e σ κ e' σ' [] → erased_step (tp, σ) (<[j:=fill K e']> tp, σ'). step (tp, σ) κ (<[j:=fill K e']> tp, σ'). Proof. rewrite -(right_id_L [] (++) (<[_:=_]>_)). by apply step_insert. Qed. Lemma nsteps_inv_r {A} n (R : A → A → Prop) x y : relations.nsteps R (S n) x y → ∃ z, relations.nsteps R n x z ∧ R z y. Proof. revert x y; induction n; intros x y. - inversion 1; subst. match goal with H : relations.nsteps _ 0 _ _ |- _ => inversion H end; subst. eexists; repeat econstructor; eauto. - inversion 1; subst. edestruct IHn as [z [? ?]]; eauto. exists z; split; eauto using relations.nsteps_l. Qed. (** * Main rules *) (** Pure reductions *) Lemma step_pure E ρ j K e e' (P : Prop) n : ... ... @@ -59,26 +50,28 @@ Section rules. Proof. iIntros (HP Hex ?) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=. iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose". iInv specN as (tp σ κs R) ">(Hown & Hproph & Hrtc)" "Hclose". iDestruct "Hrtc" as %Hrtc. iDestruct (own_valid_2 with "Hown Hj") as %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2. iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K e'))). } iFrame "Hj". iApply "Hclose". iNext. iExists (<[j:=fill K e']> tp), σ. iFrame "Hj". iApply "Hclose". iNext. iExists (<[j:=fill K e']> tp), σ, κs, R. rewrite to_tpool_insert'; last eauto. iFrame. iPureIntro. apply rtc_nsteps in Hrtc; destruct Hrtc as [m Hrtc]. specialize (Hex HP). apply (nsteps_rtc (m + n)). eapply nsteps_trans; eauto. iFrame. iPureIntro. destruct Hrtc as [m Hrtc]. specialize (Hex HP). exists (m + n)%nat. change κs with ([] ++ κs). rewrite reverse_app. eapply (nsteps_trans m n ρ (reverse κs) (tp, σ) []); eauto. revert e e' Htpj Hex. induction n => e e' Htpj Hex. - inversion Hex; subst. rewrite list_insert_id; eauto. econstructor. rewrite list_insert_id; eauto. - apply nsteps_inv_r in Hex. destruct Hex as [z [Hex1 Hex2]]. specialize (IHn _ _ Htpj Hex1). change [] with ([] ++ [] : list observation). eapply nsteps_r; eauto. replace (<[j:=fill K e']> tp) with (<[j:=fill K e']> (<[j:=fill K z]> tp)); last first. ... ... @@ -95,6 +88,84 @@ Section rules. { apply list_lookup_insert. apply lookup_lt_is_Some; eauto. } Qed. (** Prophecy variables *) Lemma step_newproph E ρ j K : nclose specN ⊆ E → spec_ctx ρ ∗ j ⤇ fill K NewProph ={E}=∗ ∃ (p : proph_id) (v : option val), j ⤇ fill K #p ∗ prophS p v. Proof. iIntros (?) "[#Hinv Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=. iInv specN as (tp σ κs R) ">(Hown & Hproph & Hstep)" "Hclose". iDestruct "Hstep" as %[n Hstep]. iDestruct "Hproph" as %[? ?]. iDestruct (own_valid_2 with "Hown Hj") as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2. rewrite prophS_eq /prophS_def. destruct (exist_fresh (used_proph_id σ)) as [p Hp]. (* destruct (exist_fresh (dom (gset proph_id) R)) as [p Hp]. *) pose (v:=first_resolve κs p). iMod (own_update with "Hown") as "[Hown Hp]". { eapply auth_update_alloc, prod_local_update_2, prod_local_update_2. eapply (alloc_singleton_local_update _ _ (Excl \$ v))=> //. apply lookup_to_proph_map_None. assert (p ∉ dom (gset proph_id) R) as Hp' by set_solver. apply (iffLR (not_elem_of_dom _ _) Hp'). } iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K #p))). } iExists p, v. iFrame. iApply "Hclose". iNext. iExists (<[j:=fill K #p]> tp), (state_upd_used_proph_id ({[ p ]} ∪) σ), ([]++κs), (<[p:=v]>R). rewrite to_proph_map_insert to_tpool_insert'; last eauto. iFrame. iPureIntro. split. - rewrite app_nil_l. unfold v. split. + apply first_resolve_insert; auto. + rewrite dom_insert_L. apply union_mono_l=>//. - exists (S n). rewrite reverse_app. eapply (nsteps_r n ρ (tp, σ) _ (reverse κs)), step_insert_no_fork; eauto. econstructor; eauto. Qed. Lemma step_resolveproph E ρ j K (p : proph_id) (v : option val) w : nclose specN ⊆ E → spec_ctx ρ ∗ j ⤇ fill K (ResolveProph #p (of_val w)) ∗ prophS p v ={E}=∗ j ⤇ fill K (of_val #()). (* ∗ ⌜v = Some w⌝. *) Proof. iIntros (?) "[#Hinv [Hj Hp]]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=. iInv specN as (tp σ κs R) ">(Hown & Hproph & Hstep)" "Hclose". iDestruct "Hstep" as %[n Hstep]. iDestruct "Hproph" as %[? ?]. rewrite prophS_eq /prophS_def. iDestruct (own_valid_2 with "Hown Hp") as %[[_ [_ ?%proph_map_singleton_included]%prod_included]%prod_included _]%auth_valid_discrete_2. iDestruct (own_valid_2 with "Hown Hj") as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2. iMod (own_update_2 with "Hown Hp") as "Hown". { eapply auth_update_dealloc, prod_local_update_2, prod_local_update_2. eapply (delete_singleton_local_update _ _ _). } iMod (own_update_2 with "Hown Hj") as "[Hown Hj]". { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K (of_val #())))). } iFrame. iApply "Hclose". iNext. iExists (<[j:=fill K (of_val #())]> tp), σ, ((p,w)::κs), (delete p R). rewrite to_proph_map_delete to_tpool_insert'; last eauto. iFrame. iPureIntro. split. - split. + intros p' v' Hv'. assert (p ≠ p'). { intros ->. revert Hv'. rewrite dom_delete_L. set_solver. } rewrite lookup_delete_ne //. intros Hp'. assert (first_resolve κs p' = Some v'). { unfold first_resolve in *. simpl in Hp'. revert Hp'. rewrite lookup_insert_ne //. } apply H1=>//. revert Hv'. rewrite dom_delete_L. set_solver. + rewrite dom_delete_L. set_solver. - exists (S n). rewrite reverse_cons. eapply (nsteps_r n ρ (tp, σ) _ (reverse κs)), step_insert_no_fork; eauto. eapply (ResolveProphS #p _ (of_val w)); eauto. Qed. (** Alloc, load, and store *) Lemma step_alloc E ρ j K e v : IntoVal e v → ... ... @@ -103,7 +174,8 @@ Section rules. Proof. iIntros (<-?) "[#Hinv Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=. iInv specN as (tp σ) ">[Hown %]" "Hclose". iInv specN as (tp σ κs R) ">(Hown & % & Hstep)" "Hclose". iDestruct "Hstep" as %[n Hstep]. destruct (exist_fresh (dom (gset loc) (heap σ))) as [l Hl%not_elem_of_dom]. iDestruct (own_valid_2 with "Hown Hj") as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2. ... ... @@ -111,14 +183,16 @@ Section rules. { by eapply auth_update, prod_local_update_1, singleton_local_update, (exclusive_local_update _ (Excl (fill K (#l)%E))). } iMod (own_update with "Hown") as "[Hown Hl]". { eapply auth_update_alloc, prod_local_update_2, { eapply auth_update_alloc, prod_local_update_2, prod_local_update_1, (alloc_singleton_local_update _ l (1%Qp,to_agree v)); last done. by apply lookup_to_gen_heap_None. } rewrite heapS_mapsto_eq /heapS_mapsto_def /=. iExists l. iFrame "Hj Hl". iApply "Hclose". iNext. iExists (<[j:=fill K (# l)]> tp), (state_upd_heap <[l:=v]> σ). iExists (<[j:=fill K (# l)]> tp), (state_upd_heap <[l:=v]> σ), ([]++κs), R. rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro. eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto. split=>//. exists (S n). rewrite reverse_app. eapply (nsteps_r n ρ (tp, σ) _ (reverse κs)), step_insert_no_fork; eauto. econstructor; eauto. Qed. Lemma step_load E ρ j K l q v: ... ... @@ -129,17 +203,21 @@ Section rules. iIntros (?) "(#Hinv & Hj & Hl)". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.