Commit 611faf3a authored by Hai Dang's avatar Hai Dang

WIP: retag mut ref

parent 0f7cd46e
......@@ -684,3 +684,25 @@ Proof.
simpl. intros. simplify_eq/=. eexists. rewrite lookup_insert.
simpl. done.
Qed.
Lemma tag_on_top_grant_unique stk old it cids stk'
(UNIQ: it.(perm) = Unique) :
grant stk old it cids = Some stk' is_stack_head it stk'.
Proof.
rewrite /grant.
case find_granting as [gip|]; [|done].
rewrite /= UNIQ /=. case access1 => [[n1 stk1]/=|//].
destruct stk1; [|case decide => ?]; intros; simplify_eq; by eexists.
Qed.
Lemma tag_on_top_reborrowN α cids l n to tn α' (NZST: (0 < n)%nat):
reborrowN α cids l n to (Tagged tn) Unique None = Some α'
tag_on_top α' l tn.
Proof.
intros RB.
destruct (for_each_lookup_case_2 _ _ _ _ _ RB) as [EQ _].
specialize (EQ O ltac:(lia)) as (stk & stk' & Eq & Eq' & GR).
rewrite shift_loc_0_nat in Eq, Eq'.
apply tag_on_top_grant_unique in GR as [stk1 Eq1]; [|done].
rewrite /tag_on_top Eq' Eq1 /=. by eexists.
Qed.
......@@ -47,7 +47,7 @@ Proof.
destruct args as [|args args']; first by inversion AREL.
apply Forall2_cons_inv in AREL as [AREL ATAIL].
destruct args' as [|]; last by inversion ATAIL. clear ATAIL.
sim_apply sim_simple_retag_local; [solve_sim..|].
sim_apply sim_simple_retag_local; [simpl; lia|solve_sim..|].
move=>l_i tg_i hplt /= Hl_i.
(* Call *)
sim_apply sim_simple_let=>/=.
......
......@@ -960,7 +960,7 @@ Proof.
destruct (tstep_retag_inv _ _ _ _ _ _ _ _ _ STEPT)
as (c & cids & h' & α' & nxtp' & Eqs & EqT & ? & ?). subst et'.
apply retag_ref_change in EqT as (li & to & Eqx' & Eqh' & Eqp' & RB); [|done..].
subst h' nxtp'. rewrite Eqhs in Eqx'. simplify_eq.
subst h' nxtp'. rewrite Eqhs in Eqx'. simplify_eq. simpl in RB.
set tn := σt.(snp).
set tk := tkUnique.
......@@ -1011,9 +1011,8 @@ Proof.
specialize (EQ1 O). rewrite Eqlv shift_loc_0_nat in EQ1.
rewrite (EQ1 NZST). apply lookup_lt_is_Some_2. by rewrite Eqlv.
- (* tag on top as result of retagging Unique *)
rewrite /tag_on_top.
admit.
Abort.
eapply tag_on_top_reborrowN; [|eauto]. done.
Admitted.
(** InitCall *)
......
......@@ -297,6 +297,7 @@ Proof.
Qed.
Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg ty css cst Φ :
(0 < tsize ty)%nat
r r' res_mapsto l [s] tg
arel rs s' s
r' r'' rs
......@@ -316,7 +317,8 @@ Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg ty css cst Φ :
(Retag (Place l (Tagged tg) (Reference (RefPtr Mutable) ty)) Default, cst)
: Φ.
Proof.
Admitted.
intros ???? HH σs σt <- <-. eapply sim_body_retag_local_mut_ref; eauto.
Qed.
(** * Memory: shared *)
Lemma sim_simple_alloc_public fs ft r n T css cst Φ :
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment