Commit 64421169 authored by Hai Dang's avatar Hai Dang

WIP: ex1_down

parent 186f3def
......@@ -593,39 +593,6 @@ Proof.
rewrite /= /check_protector /= /is_active bool_decide_true //.
Qed.
(* Property of [t] that when used to access [stk], it will not change [stk] *)
Definition stack_preserving_tag
(stk: stack) (t: ptr_id) (k: access_kind) : Prop :=
n pm, find_granting stk k (Tagged t) = Some (n, pm)
match k with
| AccessRead => it, it take n stk it.(perm) Unique
| AccessWrite => find_first_write_incompatible (take n stk) pm = Some O
end.
Lemma stack_preserving_tag_elim stk t kind :
stack_preserving_tag stk t kind
cids, n stk',
access1 stk kind (Tagged t) cids = Some (n, stk') stk' = stk.
Proof.
Abort.
Lemma stack_preserving_tag_intro stk kind t cids n stk' :
access1 stk kind (Tagged t) cids = Some (n, stk')
stack_preserving_tag stk' t kind.
Proof.
Abort.
Lemma stack_preserving_tag_unique_head stk t opro kind :
is_stack_head (mkItem Unique (Tagged t) opro) stk
stack_preserving_tag stk t kind.
Proof.
Abort.
Lemma stack_preserving_tag_active_SRO stk t :
t active_SRO stk stack_preserving_tag stk t AccessRead.
Proof.
Abort.
Lemma tag_unique_head_access cids stk t opro kind :
is_stack_head (mkItem Unique t opro) stk
......@@ -1156,6 +1123,41 @@ Proof.
specialize (EQ _ Lti) as (?&?&?&_); by eexists.
Qed.
Lemma retag_Some_Ref α nxtp c cids l old rk T mut new α' nxtp'
(NZST: (0 < tsize T)%nat)
(FRZ: if mut is Immutable then is_freeze T else True)
(N2P: rk TwoPhase) :
retag α nxtp cids c l old rk (RefPtr mut) T = Some (new, α', nxtp')
( i, (i < tsize T)%nat stk stk',
α !! (l + i) = Some stk
α' !! (l + i) = Some stk'
let protector := adding_protector rk c in
let pm := if mut is Immutable then SharedReadOnly else Unique in
grant stk old (mkItem pm new protector) cids = Some stk').
Proof.
assert ( n, tsize T = S n) as [n EqT].
{ destruct (tsize T); [lia|by eexists]. }
rewrite /retag /retag_ref EqT /=; destruct mut; rewrite -EqT.
- rewrite (_: is_two_phase rk = false); [|by destruct rk].
case reborrow as [α1|] eqn:RB; [|done]. simpl. intros ?. simplify_eq.
by apply reborrowN_lookup_case.
- case reborrow as [α1|] eqn:RB; [|done]. simpl. intros ?. simplify_eq.
move : RB => /=. rewrite visit_freeze_sensitive_is_freeze; [|done].
apply reborrowN_lookup_case.
Qed.
Lemma grant_access1 stk old new cids stk' :
new.(perm) SharedReadWrite
grant stk old new cids = Some stk'
let kind := if grants new.(perm) AccessWrite then AccessWrite else AccessRead in
is_Some (access1 stk kind old cids).
Proof.
intros NSRW. rewrite /grant.
case find_granting as [[]|]; [|done].
simpl. destruct new.(perm); [|done|..];
(case access1; [by eexists|done]).
Qed.
Lemma grant_singleton_eq (it it': item) old cids stk' :
grant [it] old it' cids = Some stk'
old = it.(tg).
......@@ -1713,3 +1715,75 @@ Proof.
exists stk2. split; [done|].
move : Inc' GR IN. by apply grant_active_preserving.
Qed.
Lemma item_insert_dedup_new_elem_of stk new n :
new item_insert_dedup stk new n.
Proof.
destruct n as [|n]; simpl.
- destruct stk; simpl.
+ set_solver.
+ case decide => ?; [subst; set_solver|set_solver].
- case (lookup n) as [?|] eqn:Eq1; case (lookup (S n)) as [?|] eqn:Eq2;
[..|set_solver];
(case decide => ?; [subst|]).
+ by eapply elem_of_list_lookup_2.
+ case decide => ?; [subst|set_solver].
by eapply elem_of_list_lookup_2.
+ by eapply elem_of_list_lookup_2.
+ set_solver.
+ by eapply elem_of_list_lookup_2.
+ set_solver.
Qed.
Lemma grant_elem_of_SRW stk old new cids stk'
(SRW: new.(perm) = SharedReadWrite) :
grant stk old new cids = Some stk' new stk'.
Proof.
rewrite /grant. case find_granting as [[n1 p1]|]; [|done].
rewrite SRW. cbn -[item_insert_dedup].
case find_first_write_incompatible as [n2|]; [|done].
cbn -[item_insert_dedup]. intros. simplify_eq.
by apply item_insert_dedup_new_elem_of.
Qed.
Lemma grant_elem_of_non_SRW stk old new cids stk'
(SRW: new.(perm) SharedReadWrite) :
grant stk old new cids = Some stk' new stk'.
Proof.
rewrite /grant. case find_granting as [[n1 p1]|]; [|done].
cbn -[item_insert_dedup].
destruct new.(perm); [|done|..];
(case access1 as [[n2 stk2]|]; [|done]);
cbn -[item_insert_dedup]; intros; simplify_eq;
by apply item_insert_dedup_new_elem_of.
Qed.
Lemma grant_elem_of stk old new cids stk' :
grant stk old new cids = Some stk' new stk'.
Proof.
case (decide (new.(perm) = SharedReadWrite)) => ?.
- by apply grant_elem_of_SRW.
- by apply grant_elem_of_non_SRW.
Qed.
Lemma retag_fn_entry_item_active α nxtp c cids l old mut T new α' nxtp' :
retag α nxtp cids c l old FnEntry (RefPtr mut) T = Some (new, α', nxtp')
i, (i < tsize T)%nat stk' pm, α' !! (l + i) = Some stk'
mkItem pm new (Some c) stk' pm Disabled.
Proof.
intros RT i Lti.
destruct (retag_Some _ _ _ _ _ _ _ _ _ _ _ _ RT) as [_ EQ].
assert ( sz, tsize T = S sz) as [sz Eqsz].
{ destruct (tsize T); [lia|by eexists]. }
move : RT. rewrite /retag /= /retag_ref Eqsz.
destruct mut.
- specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & GR).
case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq.
exists stk2, Unique. split; last split; [done| |done].
move : GR. by apply grant_elem_of.
- specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & b & GR).
case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq.
exists stk2, (if b then SharedReadOnly else SharedReadWrite).
split; last split; [done| |by destruct b].
move : GR. by apply grant_elem_of.
Qed.
......@@ -53,7 +53,7 @@ Proof.
(* Retag *)
sim_apply sim_simple_retag_ref; [simpl; lia|done| |eauto|..].
{ eapply arel_mono; [done|..|exact AREL]. solve_res. } clear VALID.
move=>l_i tg_i tg_n hplt /= ? IS_i. subst sarg.
move=>l_i tg_i tg_n hplt /= ?? IS_i. subst sarg.
specialize (IS_i O ltac:(lia)). rewrite shift_loc_0_nat in IS_i.
(* Write local *)
sim_apply sim_simple_write_local; [solve_sim..|].
......
From stbor.sim Require Import local invariant refl_step.
From stbor.sim Require Import tactics simple program.
From stbor.sim Require Import refl_step right_step left_step viewshift.
From stbor.sim Require Import refl_step right_step left_step derived_step viewshift.
Set Default Proof Using "Type".
......@@ -22,94 +22,74 @@ Definition ex1_down_opt : function :=
let: "x" := new_place (&mut int) "i" in
retag_place "x" (RefPtr Mutable) int FnEntry ;;
Call #[ScFnPtr "f"] [] ;;
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
Copy *{int} "x"
"v"
.
Lemma ex1_down_sim_fun : ⊨ᶠ ex1_down ex1_down_opt.
Proof.
apply (sim_fun_simple1 10)=>// fs ft rarg es et arg c LOOK AREL ??.
simplify_eq/=.
(* We can't use sim_simple because we need to track our stack frame id *)
intros fs ft LOOK rarg es et vls vlt σs σt FREL SUBSTs SUBSTt.
(* Substitution *)
move:(subst_l_is_Some_length _ _ _ _ SUBSTs) (subst_l_is_Some_length _ _ _ _ SUBSTt).
rewrite /= => Hls Hlt.
destruct vls as [|vs []]; [done| |done].
destruct vlt as [|arg []]; [done| |done]. clear Hls Hlt.
inversion FREL as [|???? VREL _].
clear FREL. specialize (vrel_eq _ _ _ VREL)=>?.
simplify_eq. simpl in SUBSTs, SUBSTt. simplify_eq/=.
(* Init call *)
exists 10%nat. apply sim_body_init_call=>/= Eqcs.
(* Alloc local *)
sim_apply sim_simple_alloc_local=> l t /=.
sim_apply sim_simple_let=>/=.
sim_apply sim_body_alloc_local => /=.
sim_apply sim_body_let=>/=.
(* Write local *)
sim_apply sim_simple_write_local; [solve_sim..|].
intros sarg ->.
sim_apply sim_simple_let=>/=.
apply: sim_simple_result.
sim_apply sim_body_write_local_1; [solve_sim..|].
intros sarg ? σs1 σt1. subst arg.
sim_apply sim_body_let=>/=.
apply: sim_body_result => _.
(* Retag a local place *)
sim_apply sim_simple_let=>/=.
apply Forall2_cons_inv in AREL as [AREL _].
sim_apply sim_simple_let=>/=.
sim_apply sim_body_let=>/=.
apply Forall2_cons_inv in VREL as [AREL _].
sim_apply sim_body_let=>/=.
(* Copy local place *)
sim_apply sim_simple_copy_local; [solve_sim..|].
apply sim_simple_valid_post.
apply: sim_simple_result. simpl. intros VALID.
(* TODO: need a rule to add a tag to res_cs.
Also need a rule to remove it at the end. *)
sim_apply sim_body_copy_local; [solve_sim..|].
sim_apply sim_body_result => /= VALID.
(* Retag *)
(* sim_apply sim_simple_retag_mut_ref; [simpl; lia| |eauto|..].
sim_apply sim_body_retag_ref_fn_entry; [simpl; lia|eauto| |done|..].
{ rewrite -cmra_assoc (cmra_comm (res_cs _ _)) cmra_assoc. eauto. }
{ eapply arel_mono; [done|..|exact AREL]. solve_res. } clear VALID.
move=>l_i tg_i tg_n hplt /= ? IS_i. subst sarg.
specialize (IS_i O ltac:(lia)). rewrite shift_loc_0_nat in IS_i.
move=> l' told tnew hplt α' nxtp' r0 ? _ IS_i σs2 σt2 s_new tk _ /=.
subst sarg.
specialize (IS_i O ltac:(simpl; lia)). rewrite shift_loc_0_nat in IS_i.
destruct IS_i as [(ss & st & IS_i & Eqss & Eqst) TOP].
(* Write local *)
sim_apply sim_simple_write_local; [solve_sim..|].
intros s ?. simplify_eq.
sim_apply sim_body_write_local_1; [solve_sim..|].
intros s ?. simplify_eq. simpl.
sim_apply sim_body_let=>/=.
(* Copy local left *)
sim_apply_l sim_body_copy_local_l; [solve_sim..|].
apply: sim_body_result=>_ /=.
(* Copy unique left *)
sim_apply_l sim_body_deref_l =>/=.
sim_apply_l sim_body_copy_unique_l; [solve_sim..|].
apply: sim_body_result=>_ /=.
apply: sim_body_let_l=>/=.
(* Call *)
sim_apply sim_simple_let=>/=.
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
intros rf frs frt ??? ? _ _ FREL. simplify_eq/=.
apply: sim_simple_result. simpl.
sim_apply sim_simple_let=>/=.
(* Copy local *)
sim_apply sim_simple_copy_local; [solve_sim..|].
apply: sim_simple_result. simpl.
sim_apply sim_simple_deref=>l' t' ?. simplify_eq/=.
(* Write unique. We need to drop to complex mode, to preserve some local state info. *)
intros σs σt.
sim_apply sim_body_write_unique_1; [solve_sim..|].
intros ?? Htop. simplify_eq/=.
sim_apply sim_body_let. simplify_eq/=.
(* Copy local (right) *)
rewrite -(right_id ε op ( _ res_loc _ _ _)).
sim_apply (sim_body_step_over_call _ _ _ ε _ (ValR _) [] []); [constructor|done|..].
move => rf' ? _ _ frs' frt' σs3 σt3 _ /= Eqs1 Eqs2 ? _ _. simplify_eq.
exists 5%nat.
apply: sim_body_result=>_ /=.
sim_apply sim_body_let=>/=. clear frs' frt'.
(* Copy local right *)
sim_apply_r sim_body_copy_local_r; [solve_sim..|].
apply: sim_body_result=>_. simpl.
(* Copy unique (right) *)
sim_apply_r sim_body_deref_r. simpl.
sim_apply_r sim_body_copy_unique_r; [try solve_sim..|].
{ rewrite lookup_insert. done. }
apply: sim_body_result=>_. simpl.
apply: sim_body_let_r. simpl. (* FIXME: figure out why [sim_apply_r] does the wrong thing here *)
(* We can go back to simple mode! *)
eapply (sim_simplify (fun_post_simple c)). { by eauto. }
simplify_eq/=. clear- AREL FREL LOOK.
(* Call *)
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
intros rf' frs' frt' ??? ? _ _ FREL'. simplify_eq/=.
apply: sim_simple_result. simpl.
sim_apply sim_simple_let=>/=.
(* Copy local (left). We drop to complex just because simple does not support this yet. *)
intros σs σt.
sim_apply_l sim_body_copy_local_l; [solve_sim..|].
apply: sim_body_result=>_. simpl.
(* Copy unique (left) *)
sim_apply_l sim_body_deref_l. simpl.
sim_apply_l sim_body_copy_unique_l; [try solve_sim..|].
{ rewrite lookup_insert. done. }
apply: sim_body_result=>Hval. simpl.
apply: sim_body_let_l. simpl.
(* Free stuff *)
eapply (sim_simplify (fun_post_simple c)). { by eauto. }
sim_apply sim_simple_free_local_1; [solve_sim..|]. simpl.
sim_apply sim_simple_let=>/=.
sim_apply sim_simple_free_public.
{ simpl. constructor; [|by constructor].
apply: arel_mono; last fast_done.
apply: cmra_valid_included; first fast_done.
do 3 apply cmra_mono_r. solve_res. solve_res. }
sim_apply sim_simple_let=>/=.
(* Finishing up. *)
apply: sim_simple_result. split.
- solve_res.
- constructor; simpl; auto. *)
apply: sim_body_result=>_ /=.
(* Copy protected right *)
sim_apply_r sim_body_deref_r =>/=.
sim_apply_r sim_body_copy_protected_r;
[solve_sim..|by rewrite lookup_insert|by eapply elem_of_dom_2|].
apply: sim_body_result=>Hval /=.
apply: sim_body_let_r=>/=.
Abort.
......@@ -46,14 +46,14 @@ Proof.
sim_apply sim_body_let=>/=.
(* Copy local place *)
sim_apply sim_body_copy_local; [solve_sim..|].
sim_apply sim_body_result. simpl. intros VALID.
sim_apply sim_body_result => /= VALID.
(* Retag *)
sim_apply sim_body_retag_ref_default; [simpl; lia|done| |eauto|..].
{ eapply arel_mono; [done|..|exact AREL]. solve_res. } clear VALID.
move=> l' told tnew hplt c' cids α' nxtp' ? _ _ IS_i σs' σt' s_new
tk ARELn /=. subst sarg.
specialize (IS_i O ltac:(simpl; lia)). rewrite shift_loc_0_nat in IS_i.
destruct IS_i as [[[ss st] IS_i] TOP].
destruct IS_i as [(ss & st & IS_i & _) TOP].
(* Write local *)
sim_apply sim_body_write_local_1; [solve_sim..|].
intros s ?. simplify_eq. simpl.
......@@ -85,8 +85,8 @@ Proof.
{ constructor; [|by constructor].
constructor; [done|by constructor]. } clear ARELn.
intros rf' frs' frt' ??? ? _ _ FREL'. simplify_eq/=.
apply: sim_simple_result. simpl.
sim_apply sim_simple_let=>/=. clear σs' σt' nxtp' α' TOP σs σt.
apply: sim_simple_result => /=.
sim_apply sim_simple_let=>/=. clear σs' σt' nxtp' α' TOP σs σt .
(* Copy local (left). We drop to complex just because simple does not support this yet. *)
intros σs σt.
sim_apply_l sim_body_copy_local_l; [solve_sim..|].
......@@ -95,8 +95,8 @@ Proof.
sim_apply_l sim_body_deref_l. simpl.
sim_apply_l sim_body_copy_public_l; [try solve_sim..|].
intros r' AREL'.
apply: sim_body_result=>Hval. simpl.
apply: sim_body_let_l. simpl.
apply: sim_body_result=>Hval/=.
apply: sim_body_let_l=>/=.
(* Free stuff *)
eapply (sim_simplify (fun_post_simple c)). { by eauto. }
sim_apply sim_simple_free_local_1; [solve_sim..|]. simpl.
......
......@@ -496,6 +496,30 @@ Proof.
specialize (EQ _ Lt). by rewrite EQ lookup_lt_is_Some.
Qed.
Lemma write_hpl_elem_of_dom_from_empty l vl l' :
( (i: nat), (i < length vl)%nat l' = l + i)
l' dom (gset loc) (write_hpl l vl ).
Proof.
split.
- naive_solver eauto using write_hpl_elem_of_dom.
- destruct (write_hpl_lookup_case l vl l')
as [(i & Lti & ? & Eql1)|(NEQl1 & Eql1)].
+ naive_solver.
+ rewrite elem_of_dom Eql1 lookup_empty. by intros [].
Qed.
(** For writing to heaplet *)
Instance write_hpl_proper (l: loc) v :
Proper (() ==> ()) (write_hpl l v).
Proof.
intros h1 h2 Eq. revert l h1 h2 Eq.
induction v as [|s v IH]; intros l h1 h2 Eq; simpl; [done|].
apply IH. intros l'.
case (decide (l' = l)) => [->|?].
- by rewrite 2!lookup_insert.
- do 2 (rewrite lookup_insert_ne; [|done]). apply Eq.
Qed.
Lemma res_tag_alloc_local_update lsf t k h
(FRESH: lsf.(rtm) !! t = None) :
(lsf, ε) ~l~> (lsf res_tag t k h, res_tag t k h).
......
......@@ -118,18 +118,6 @@ Proof.
by apply (priv_loc_not_public _ _ _ _ PV PB).
Qed.
(** For writing to heaplet *)
Instance write_hpl_proper (l: loc) v :
Proper (() ==> ()) (write_hpl l v).
Proof.
intros h1 h2 Eq. revert l h1 h2 Eq.
induction v as [|s v IH]; intros l h1 h2 Eq; simpl; [done|].
apply IH. intros l'.
case (decide (l' = l)) => [->|?].
- by rewrite 2!lookup_insert.
- do 2 (rewrite lookup_insert_ne; [|done]). apply Eq.
Qed.
Lemma local_unique_access_head r σs (σt: state) l stk kind n' stk' t ss st k h
(WFT: Wf σt) (LU: k = tkLocal k = tkUnique):
σt.(sst) !! l = Some stk
......@@ -203,3 +191,25 @@ Proof.
destruct (PB _ Eqss) as (st' & Eqst' & AREL). rewrite Eqst' in Eqss'.
by simplify_eq.
Qed.
Lemma priv_loc_UB_retag_access_eq r σs σt c l old new mut T kind α' nxtp'
(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')
wsat r σs σt
i t, (i < tsize T)%nat
priv_loc r (l + i) t
(if old is (Tagged t2)
then (h: heapletR), r.(rtm) !! t2 Some (to_tgkR tkPub, h)
else True)
False.
Proof.
intros RT WSAT i t Lti.
have NZST: (0 < tsize T)%nat by lia.
destruct (retag_change_ref_NZST _ _ _ _ _ _ _ _ _ _ _ _ NZST RT);
subst new nxtp'.
destruct (retag_Some_Ref _ _ _ _ _ _ _ _ _ _ _ _ NZST FRZ N2P RT _ Lti)
as (stk & stk' & Eqstk & Eqstk' & GR).
apply grant_access1 in GR; [|by destruct mut].
revert Eqstk GR WSAT. by apply priv_pub_access_UB.
Qed.
......@@ -78,16 +78,16 @@ Proof.
intros [Eqk1 Eqh1]%Some_equiv_inj. simpl in Eqk1, Eqh1.
intros l1 ss1 st1. rewrite -Eqh1 /to_hplR lookup_fmap.
destruct (write_hpl_lookup_case l vst l1)
as [(i & Lti & ? & Eql1)|(NEQl1 & Eql1)].
* subst l1. rewrite Eql1. rewrite repeat_length in Lti.
rewrite (repeat_lookup_lt_length _ _ _ Lti) /=.
intros ?%Some_equiv_inj%to_agree_inj. simplify_eq.
rewrite (HLmt1 _ Lti) (HLms1 _ Lti).
intros INVPR. do 2 (split; [done|]). destruct k1.
{ by rewrite /= (HLst1 _ Lti). }
{ move : INVPR. simpl. naive_solver. }
{ by inversion Eqk1. }
* rewrite Eql1 lookup_empty. inversion 1.
as [(i & Lti & ? & Eql1)|(NEQl1 & Eql1)]; last first.
{ rewrite Eql1 lookup_empty. inversion 1. }
subst l1. rewrite Eql1. rewrite repeat_length in Lti.
rewrite (repeat_lookup_lt_length _ _ _ Lti) /=.
intros ?%Some_equiv_inj%to_agree_inj. simplify_eq.
rewrite (HLmt1 _ Lti) (HLms1 _ Lti).
intros INVPR. do 2 (split; [done|]). destruct k1.
* by rewrite /= (HLst1 _ Lti).
* move : INVPR. simpl. naive_solver.
* by inversion Eqk1.
+ intros Eqh'.
have Eqh1: (r_f r).(rtm) !! t1 Some (to_tgkR k1, h1).
{ move : Eqh'. rewrite lookup_op lookup_insert_ne // right_id //. }
......@@ -1414,22 +1414,24 @@ Lemma sim_body_retag_ref_default fs ft mut r n ptr T σs σt Φ :
(if mut is Immutable then is_freeze T else True)
(* Ptr(l,otg) comes from the arguments, so [otg] must be a public tag. *)
arel r ptr ptr
(∀ l told tnew hplt c cids α' nxtp',
( l told tnew hplt c cids α' nxtp' r0,
ptr = ScPtr l told
σt.(scs) = c :: cids
retag σt.(sst) σt.(snp) σt.(scs) c l told Default pk T
= Some ((Tagged tnew), α', nxtp')
(* [hplt] contains all [l + i]'s and the new tag [tnew] is on top of the
stack for each [l +ₗ i].
TODO: we can also specify that [hplt] knows the values of [l +ₗ i]'s. *)
stack for each [l + i]. *)
( i: nat, (i < tsize T)%nat
is_Some $ hplt !! (l +ₗ i) ∧ tag_on_top α' (l +ₗ i) tnew pm) →
( ss st, hplt !! (l + i) = Some (ss, st)
σs.(shp) !! (l + i) = Some ss σt.(shp) !! (l + i) = Some st
arel r0 ss st)
tag_on_top α' (l + i) tnew pm)
let σs' := mkState σs.(shp) α' σs.(scs) nxtp' σs.(snc) in
let σt' := mkState σt.(shp) α' σt.(scs) nxtp' σt.(snc) in
let s_new := ScPtr l (Tagged tnew) in
let tk := match mut with Mutable => tkUnique | Immutable => tkPub end in
(if mut is Immutable then arel (res_tag tnew tk hplt) s_new s_new else True)
Φ (r ⋅ res_tag tnew tk hplt) n (ValR [s_new]) σs' (ValR [s_new]) σt') →
Φ (r res_tag tnew tk hplt r0) n (ValR [s_new]) σs' (ValR [s_new]) σt')
r {n,fs,ft}
(Retag #[ptr] pk T Default, σs)
(Retag #[ptr] pk T Default, σt) : Φ.
......@@ -1485,6 +1487,12 @@ Proof.
set hplt : heaplet := write_hpl l (combine vs vt) .
set tk := match mut with Mutable => tkUnique | Immutable => tkPub end.
set r' : resUR := r res_tag tnew tk hplt.
set r0 : resUR := (core ((r_f r).(rtm)), ε).
have Eqr': r_f (r' r0) r_f r'.
{ rewrite /r' /r0 !cmra_assoc /=.
split; simpl; [|by rewrite right_id].
by rewrite -(cmra_assoc (r_f.1 r.1))
(cmra_comm {[ _ := _ ]} (core (r_f.1 r.1))) cmra_assoc cmra_core_r. }
have HNP := wsat_tmap_nxtp _ _ _ WSAT1.
have VALID': (r_f r res_tag tnew tk hplt).
......@@ -1502,10 +1510,10 @@ Proof.
clear NT.
exists (#[ScPtr l (Tagged tnew)])%V, σs', r', n.
exists (#[ScPtr l (Tagged tnew)])%V, σs', (r' r0), n.
split; last split.
{ left. by constructor. }
{ clear POST. rewrite /r' cmra_assoc.
{ clear POST. rewrite Eqr' /r' cmra_assoc.
split; last split; last split; last split; last split.
- by apply (tstep_wf _ _ _ STEPS WFS).
- by apply (tstep_wf _ _ _ STEPT WFT).
......@@ -1623,7 +1631,28 @@ Proof.
left.
apply: sim_body_result. intros VALIDr. eapply POST; eauto.
- intros i Lti. split.
+ clear -Lti EqlT. apply write_hpl_is_Some. by rewrite EqlT.
+ have Lti': (i < length (combine vs vt))%nat by rewrite EqlT.
destruct (write_hpl_is_Some l (combine vs vt) _ Lti') as [[ss st] Eqss].
exists ss, st. split; [done|].
destruct (write_hpl_lookup l (combine vs vt) ) as [EQ _].
rewrite (EQ _ Lti') in Eqss.
apply lookup_combine_Some_eq in Eqss as [Eqvs1 Eqvt1].
specialize (Eqshp _ Lti). rewrite Eqvs1 in Eqshp.
specialize (Eqthp _ Lti). rewrite Eqvt1 in Eqthp.
do 2 (split; [done|]).
destruct (PUBP (l + i)) as [PB|[t' PV]].
* by eapply elem_of_dom_2.
* specialize (PB _ Eqthp) as (ss1 & Eqss1 & AREL1).
clear -Eqshp Eqss1 AREL1 VALIDr.
rewrite Eqss1 in Eqshp. simplify_eq. apply arel_persistent in AREL1.
move : AREL1. apply arel_mono_l; [|done].
apply (cmra_valid_included _ _ VALIDr), cmra_included_r.
* exfalso.
apply (priv_loc_UB_retag_access_eq _ _ _ _ _ _ _ _ _ Default _ _ FRZ
ltac:(done) EqRT WSAT1 _ _ Lti PV).
clear -VALID AREL.
apply (arel_mono _ _ VALID) in AREL; [|apply cmra_included_r].
move : AREL => [_ [_ //]].
+ move : Lti.
destruct mut.
* eapply tag_on_top_retag_ref_uniq. exact EqRT.
......@@ -1641,21 +1670,23 @@ Lemma sim_body_retag_ref_fn_entry n fs ft mut r r' c cids Ts ptr T σs σt Φ :
(if mut is Immutable then is_freeze T else True)
(* Ptr(l,otg) comes from the arguments, so [otg] must be a public tag. *)
arel r ptr ptr
(∀ l told tnew hplt α' nxtp',
( l told tnew hplt α' nxtp' r0,
ptr = ScPtr l told
retag σt.(sst) σt.(snp) σt.(scs) c l told FnEntry pk T
= Some ((Tagged tnew), α', nxtp')
(* [hplt] contains all [l + i]'s and the new tag [tnew] is on top of the
stack for each [l +ₗ i].
TODO: we can also specify that [hplt] knows the values of [l +ₗ i]'s. *)
stack for each [l + i]. *)
( i: nat, (i < tsize T)%nat
is_Some $ hplt !! (l +ₗ i) ∧ tag_on_top α' (l +ₗ i) tnew pm) →
( ss st, hplt !! (l + i) = Some (ss, st)
σs.(shp) !! (l + i) = Some ss σt