Commit f734ecf1 authored by Hai Dang's avatar Hai Dang
Browse files

add cmra for local var

parent 3476c8a5
......@@ -25,22 +25,24 @@ Definition cmapUR := gmapUR call_id callStateR.
Definition to_cmapUR (cm: cmap) : cmapUR := fmap to_callStateR cm.
Definition ptrmap := gmap ptr_id (tag_kind * mem).
Definition tmap := gmap ptr_id (tag_kind * mem).
Definition heapletR := gmapR loc (agreeR scalarC).
(* ptr_id TagKid x (loc Ag(Scalar)) *)
Definition ptrmapUR := gmapUR ptr_id (prodR tagKindR heapletR).
Definition tmapUR := gmapUR ptr_id (prodR tagKindR heapletR).
Definition to_heapletR (h: mem) : heapletR := fmap to_agree h.
Definition to_ptrmapUR (pm: ptrmap) : ptrmapUR :=
Definition to_tmapUR (pm: tmap) : tmapUR :=
fmap (λ tm, (to_tagKindR tm.1, to_heapletR tm.2)) pm.
Definition lmap := gmap loc (scalar * stack).
Definition lmapUR := gmapR loc (csumR (exclR (leibnizO (scalar * stack))) (agreeR unitO)).
Definition lmapUR := gmapUR loc (csumR (exclR (leibnizO (scalar * stack))) (agreeR unitO)).
Definition res := (ptrmap * cmap)%type.
Definition resUR := prodUR ptrmapUR cmapUR.
Definition to_resUR (r: res) : resUR := (to_ptrmapUR r.1, to_cmapUR r.2).
Definition res := (tmap * cmap * lmap)%type.
Definition resUR := prodUR (prodUR tmapUR cmapUR) lmapUR.
Definition rtm (r: resUR) : tmapUR := r.1.1.
Definition rcm (r: resUR) : cmapUR := r.1.2.
Definition rlm (r: resUR) : lmapUR := r.2.
Lemma local_update_discrete_valid_frame `{CmraDiscrete A} (r_f r r' : A) :
(r_f r) (r_f r, r) ~l~> (r_f r', r') (r_f r').
......@@ -167,8 +169,8 @@ Proof.
- inversion Eq.
Qed.
(** ptrmap properties *)
Lemma ptrmap_insert_op_r (pm1 pm2: ptrmapUR) t h0 kh (VALID: (pm1 pm2)):
(** tmap properties *)
Lemma tmap_insert_op_r (pm1 pm2: tmapUR) t h0 kh (VALID: (pm1 pm2)):
pm2 !! t = Some (to_tagKindR tkUnique, h0)
pm1 <[t:=kh]> pm2 = <[t:=kh]> (pm1 pm2).
Proof.
......@@ -182,7 +184,7 @@ Proof.
+ do 2 (rewrite lookup_insert_ne //). by rewrite lookup_op.
Qed.
Lemma ptrmap_lookup_op_r (pm1 pm2: ptrmapUR) t h0 (VALID: (pm1 pm2)):
Lemma tmap_lookup_op_r (pm1 pm2: tmapUR) t h0 (VALID: (pm1 pm2)):
pm2 !! t = Some (to_tagKindR tkUnique, h0)
(pm1 pm2) !! t = Some (to_tagKindR tkUnique, h0).
Proof.
......@@ -191,7 +193,7 @@ Proof.
rewrite -Some_op pair_op. intros [?%exclusive_r]; [done|apply _].
Qed.
Lemma ptrmap_lookup_op_l_unique_equiv (pm1 pm2: ptrmapUR) t h0
Lemma tmap_lookup_op_l_unique_equiv (pm1 pm2: tmapUR) t h0
(VALID: (pm1 pm2)):
pm1 !! t Some (to_tagKindR tkUnique, h0)
(pm1 pm2) !! t Some (to_tagKindR tkUnique, h0).
......@@ -201,16 +203,16 @@ Proof.
rewrite -Some_op pair_op. intros [?%exclusive_l]; [done|apply _].
Qed.
Lemma ptrmap_lookup_op_unique_included (pm1 pm2: ptrmapUR) t h0
Lemma tmap_lookup_op_unique_included (pm1 pm2: tmapUR) t h0
(VALID: pm2) (INCL: pm1 pm2):
pm1 !! t Some (to_tagKindR tkUnique, h0)
pm2 !! t Some (to_tagKindR tkUnique, h0).
Proof.
destruct INCL as [cm' Eq]. rewrite Eq. apply ptrmap_lookup_op_l_unique_equiv.
destruct INCL as [cm' Eq]. rewrite Eq. apply tmap_lookup_op_l_unique_equiv.
by rewrite -Eq.
Qed.
Lemma ptrmap_lookup_op_r_equiv_pub (pm1 pm2: ptrmapUR) t h2 (VALID: (pm1 pm2)):
Lemma tmap_lookup_op_r_equiv_pub (pm1 pm2: tmapUR) t h2 (VALID: (pm1 pm2)):
pm2 !! t Some (to_tagKindR tkPub, h2)
h1, (pm1 pm2) !! t Some (to_tagKindR tkPub, h1 h2).
Proof.
......@@ -222,17 +224,17 @@ Proof.
- intros _. exists (: gmap loc _). by rewrite 2!left_id HL.
Qed.
Lemma ptrmap_valid (r_f r: ptrmapUR) t h0 kh
Lemma tmap_valid (r_f r: tmapUR) t h0 kh
(Eqtg: r !! t = Some (to_tagKindR tkUnique, h0)) (VN: kh) :
(r_f r) (r_f (<[t:= kh]> r)).
Proof.
intros VALID.
apply (local_update_discrete_valid_frame _ _ _ VALID).
have EQ := (ptrmap_insert_op_r _ _ _ _ kh VALID Eqtg). rewrite EQ.
have EQ := (tmap_insert_op_r _ _ _ _ kh VALID Eqtg). rewrite EQ.
eapply (insert_local_update _ _ _
(to_tagKindR tkUnique, h0) (to_tagKindR tkUnique, h0));
[|exact Eqtg|by apply exclusive_local_update].
by rewrite (ptrmap_lookup_op_r _ _ _ _ VALID Eqtg).
by rewrite (tmap_lookup_op_r _ _ _ _ VALID Eqtg).
Qed.
(** heaplet *)
......@@ -266,7 +268,7 @@ Proof.
by destruct (h !! l) as [s|] eqn:Eql; rewrite Eql.
Qed.
Lemma ptrmap_lookup_core_pub (pm: ptrmapUR) t h:
Lemma tmap_lookup_core_pub (pm: tmapUR) t h:
pm !! t Some (to_tagKindR tkPub, h)
core pm !! t Some (to_tagKindR tkPub, h).
Proof. intros Eq. rewrite lookup_core Eq /core /= core_id //. Qed.
......@@ -92,7 +92,7 @@ Proof.
econs 3; eauto.
Qed.
Lemma adequacy
Lemma adequacy_classical
prog_src
prog_tgt idx conf_src conf_tgt
`{NSD: e σ, never_stuck prog_src e σ \/
......
......@@ -16,13 +16,13 @@ Definition arel (r: resUR) (s1 s2: scalar) : Prop :=
l1 = l2 tg1 = tg2
match tg1 with
| Untagged => True
| Tagged t => h, r.1 !! t Some (to_tagKindR tkPub, h)
| Tagged t => h, r.(rtm) !! t Some (to_tagKindR tkPub, h)
end
| _, _ => False
end.
Definition ptrmap_inv (r: resUR) (σ: state) : Prop :=
(t: ptr_id) (k: tag_kind) h, r.1 !! t Some (to_tagKindR k, h)
Definition tmap_inv (r: resUR) (σ: state) : Prop :=
(t: ptr_id) (k: tag_kind) h, r.(rtm) !! t Some (to_tagKindR k, h)
(t < σ.(snp))%nat
( (l: loc) (s: scalar), h !! l Some (to_agree s)
(stk: stack), σ.(sst) !! l = Some stk
......@@ -38,7 +38,7 @@ Definition ptrmap_inv (r: resUR) (σ: state) : Prop :=
end).
Definition cmap_inv (r: resUR) (σ: state) : Prop :=
(c: call_id) (cs: callStateR), r.2 !! c Some cs
(c: call_id) (cs: callStateR), r.(rcm) !! c Some cs
match cs with
(* if c is a private call id *)
| Cinl (Excl T) =>
......@@ -47,7 +47,7 @@ Definition cmap_inv (r: resUR) (σ: state) : Prop :=
(t: ptr_id), t T
t < σ.(snp)
(* that protects the heaplet [h] *)
k h, r.1 !! t Some (k, h)
k h, r.(rtm) !! t Some (k, h)
(* if [l] is in that heaplet [h] *)
(l: loc), l dom (gset loc) h
(* then a c-protector must be in the stack of l *)
......@@ -62,8 +62,8 @@ Definition cmap_inv (r: resUR) (σ: state) : Prop :=
by some call id [c] and [l] is in [t]'s heaplet [h]. *)
Definition priv_loc (r: resUR) (l: loc) (t: ptr_id) :=
(c: call_id) (T: gset ptr_id) h,
r.2 !! c Some (Cinl (Excl T)) t T
r.1 !! t Some (to_tagKindR tkUnique, h) l dom (gset loc) h.
r.(rcm) !! c Some (Cinl (Excl T)) t T
r.(rtm) !! t Some (to_tagKindR tkUnique, h) l dom (gset loc) h.
(** State relation *)
Definition srel (r: resUR) (σs σt: state) : Prop :=
......@@ -77,7 +77,7 @@ Definition wsat (r: resUR) (σs σt: state) : Prop :=
(* Wellformedness *)
Wf σs Wf σt r
(* Invariants *)
ptrmap_inv r σt cmap_inv r σt srel r σs σt.
tmap_inv r σt cmap_inv r σt srel r σs σt.
(** Value relation for function arguments/return values *)
(* Values passed among functions are public *)
......@@ -89,20 +89,20 @@ Definition vrel_expr (r: resUR) (e1 e2: expr) :=
(** Condition for resource before EndCall *)
(* Any private location w.r.t to the current call id ownership must be related *)
Definition end_call_sat (r: resUR) (σs σt: state) : Prop :=
c, hd_error σt.(scs) = Some c is_Some (r.2 !! c)
c, hd_error σt.(scs) = Some c is_Some (r.(rcm) !! c)
( r_f, (r_f r)
T, (r_f r).2 !! c Some (Cinl (Excl T)) (t: ptr_id), t T
h, (r_f r).1 !! t Some (to_tagKindR tkUnique, h)
T, (r_f r).(rcm) !! c Some (Cinl (Excl T)) (t: ptr_id), t T
h, (r_f r).(rtm) !! t Some (to_tagKindR tkUnique, h)
l st, l dom (gset loc) h σt.(shp) !! l = Some st
ss, σs.(shp) !! l = Some ss arel (r_f r) ss st).
Definition init_res : resUR := (ε, {[O := to_callStateR csPub]}).
Definition init_res : resUR := ((ε, {[O := to_callStateR csPub]}), ε).
Lemma wsat_init_state : wsat init_res init_state init_state.
Proof.
split; last split; last split; last split; last split.
- apply wf_init_state.
- apply wf_init_state.
- split; [done|]. intros ?; simpl. destruct i.
- split; [|done]. split; [done|]. intros ?; simpl. destruct i.
+ rewrite lookup_singleton //.
+ rewrite lookup_singleton_ne //.
- intros ??? HL. exfalso. move : HL. rewrite /= lookup_empty. inversion 1.
......@@ -158,8 +158,9 @@ Proof.
intros [Eql [Eqt PV]]. subst. repeat split.
destruct t2 as [t2|]; [|done].
destruct PV as [h HL].
have HL1: Some (to_tagKindR tkPub, h) r2.1 !! t2.
{ rewrite -HL. by apply lookup_included, prod_included, Le. }
have HL1: Some (to_tagKindR tkPub, h) r2.(rtm) !! t2.
{ rewrite -HL. apply lookup_included, prod_included.
by apply prod_included in Le as []. }
apply option_included in HL1 as [?|[th1 [[tk2 h2] [? [Eq1 INCL]]]]]; [done|].
simplify_eq. exists h2. rewrite Eq1 (_: tk2 to_tagKindR tkPub) //.
apply tag_kind_incl_eq; [done|].
......@@ -167,7 +168,7 @@ Proof.
- apply csum_included. naive_solver.
- have VL2: tk2.
{ apply (pair_valid tk2 h2). rewrite -pair_valid.
apply (lookup_valid_Some r2.1 t2); [apply VAL|]. by rewrite Eq1. }
apply (lookup_valid_Some r2.(rtm) t2); [apply VAL|]. by rewrite Eq1. }
destruct Eq as [|[|Eq]]; [by subst|naive_solver|].
destruct Eq as [?[ag[? [? ?]]]]. simplify_eq.
apply to_agree_uninj in VL2 as [[] Eq]. rewrite -Eq.
......@@ -188,29 +189,33 @@ Lemma priv_loc_mono (r1 r2 : resUR) (VAL: ✓ r2) :
r1 r2 l t, priv_loc r1 l t priv_loc r2 l t.
Proof.
intros LE l t (c & T & h & Eq2 & InT & Eq1 & InD).
apply prod_included in LE as []. apply pair_valid in VAL as [].
do 2 (apply prod_included in LE as [LE ]).
do 2 (apply pair_valid in VAL as [VAL ]).
exists c, T, h. repeat split; [|done| |done].
- by apply (cmap_lookup_op_unique_included r1.2).
- by apply (ptrmap_lookup_op_unique_included r1.1).
- by apply (cmap_lookup_op_unique_included r1.(rcm)).
- by apply (tmap_lookup_op_unique_included r1.(rtm)).
Qed.
Instance ptrmap_inv_proper : Proper (() ==> (=) ==> iff) ptrmap_inv.
Instance tmap_inv_proper : Proper (() ==> (=) ==> iff) tmap_inv.
Proof.
intros r1 r2 Eqr ? σ ?. subst. rewrite /ptrmap_inv. by setoid_rewrite Eqr.
intros r1 r2 [[Eqt Eqc] Eqm] ? σ ?. subst. rewrite /tmap_inv /rtm.
by setoid_rewrite Eqt.
Qed.
Instance cmap_inv_proper : Proper (() ==> (=) ==> iff) cmap_inv.
Proof.
intros r1 r2 Eqr ? σ ?. subst. rewrite /cmap_inv. setoid_rewrite Eqr.
split; intros EQ ?? Eq; specialize (EQ _ _ Eq); destruct cs as [[]| |]; eauto;
[by setoid_rewrite <- Eqr|by setoid_rewrite Eqr].
intros r1 r2 [[Eqt Eqc] Eqm] ? σ ?. subst. rewrite /cmap_inv /rcm /rtm.
setoid_rewrite Eqc.
split; intros EQ ?? Eq; specialize (EQ _ _ Eq);
destruct cs as [[]| |]; eauto;
[by setoid_rewrite <- Eqt|by setoid_rewrite Eqt].
Qed.
Instance arel_proper : Proper (() ==> (=) ==> (=) ==> iff) arel.
Proof. solve_proper. Qed.
Proof. rewrite /arel /rtm. solve_proper. Qed.
Instance priv_loc_proper : Proper (() ==> (=) ==> (=) ==> iff) priv_loc.
Proof. solve_proper. Qed.
Proof. rewrite /priv_loc /rcm /rtm. solve_proper. Qed.
Instance srel_proper : Proper (() ==> (=) ==> (=) ==> iff) srel.
Proof.
......@@ -227,7 +232,7 @@ Instance wsat_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) wsat.
Proof. solve_proper. Qed.
Lemma cinv_lookup_in (r: resUR) (σ: state) c cs:
Wf σ cmap_inv r σ r.2 !! c Some cs (c < σ.(snc))%nat.
Wf σ cmap_inv r σ r.(rcm) !! c Some cs (c < σ.(snc))%nat.
Proof.
intros WF CINV EQ. specialize (CINV c cs EQ).
destruct cs as [[]| |]; [|done..].
......@@ -235,7 +240,7 @@ Proof.
Qed.
Lemma cinv_lookup_in_eq (r: resUR) (σ: state) c cs:
Wf σ cmap_inv r σ r.2 !! c = Some cs (c < σ.(snc))%nat.
Wf σ cmap_inv r σ r.(rcm) !! c = Some cs (c < σ.(snc))%nat.
Proof.
intros WF CINV EQ. eapply cinv_lookup_in; eauto. by rewrite EQ.
Qed.
......
......@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
Lemma sim_body_copy_left_1
fs ft (r: resUR) k (h: heapletR) n l t et σs σt Φ
(UNIQUE: r.1 !! t Some (k, h))
(UNIQUE: r.(rtm) !! t Some (k, h))
(InD: l dom (gset loc) h) :
( s, σs.(shp) !! l = Some s r {n,fs,ft} (#[s%S], σs) (et, σt) : Φ : Prop)
r {n,fs,ft} (Copy (Place l (Tagged t) int), σs) (et, σt) : Φ.
......
......@@ -3,7 +3,7 @@ From Paco Require Import paco.
From stbor.lang Require Import steps_wf steps_inversion.
From stbor.sim Require Import sflib behavior global local.
From stbor.sim Require Import invariant global_adequacy refl_step.
From stbor.sim Require Import invariant refl_step.
Set Default Proof Using "Type".
......@@ -141,10 +141,11 @@ Proof.
σt.(scs) = c2 :: cids2
σs2 = mkState σs.(shp) σs.(sst) cids1 σs.(snp) σs.(snc)
σt2 = mkState σt.(shp) σt.(sst) cids2 σt.(snp) σt.(snc)
r2 = (r'.1, match (r'.2 !! c2) with
| Some (Cinl (Excl T)) => <[c2 := to_callStateR csPub]> r'.2
| _ => r'.2
end).
r2 = ((r'.(rtm),
match (r'.(rcm) !! c2) with
| Some (Cinl (Excl T)) => <[c2 := to_callStateR csPub]> r'.(rcm)
| _ => r'.(rcm)
end), r'.(rlm)).
have SIMEND : r' {idx',fns,fnt} (EndCall vs1, σs) (EndCall vt1, σt) : Φ.
{ apply sim_body_end_call; auto.
clear. intros. rewrite /Φ. naive_solver. }
......
......@@ -4,7 +4,7 @@ From stbor.sim Require Import global_adequacy local_adequacy refl_step.
Set Default Proof Using "Type".
Lemma sim_prog_sim
Lemma sim_prog_sim_classical
prog_src
prog_tgt
`{NSD: e σ, never_stuck prog_src e σ \/
......@@ -19,7 +19,8 @@ Proof.
destruct (FUNS _ _ Eqt) as ([xls ebs HCs] & Eqs & Eql & SIMf).
apply nil_length_inv in Eql. subst xls.
specialize (SIMf ε ebs ebt [] [] init_state init_state) as [idx SIM]; [done..|].
unfold behave_prog. eapply (adequacy _ _ idx); [apply NSD| |by apply wf_init_state..].
unfold behave_prog.
eapply (adequacy_classical _ _ idx); [apply NSD| |by apply wf_init_state..].
eapply sim_local_conf_sim; eauto.
econs; swap 2 4.
- econs 1.
......@@ -37,10 +38,10 @@ Proof.
{ exists O. by rewrite -STACK. }
rewrite /end_call_sat -STACK.
intros c Eq. simpl in Eq. simplify_eq.
have HL: (init_res r').2 !! 0%nat Some (to_callStateR csPub).
have HL: (init_res r').(rcm) !! 0%nat Some (to_callStateR csPub).
{ apply cmap_lookup_op_l_equiv_pub; [apply VALID|].
by rewrite /= lookup_singleton. }
split. { destruct ((init_res r').2 !! 0%nat). by eexists. by inversion HL. }
split. { destruct ((init_res r').(rcm) !! 0%nat). by eexists. by inversion HL. }
intros r_f VALIDf T HL2. exfalso.
move : HL2. rewrite lookup_op HL. apply callStateR_exclusive_2.
- instantiate (1:=ε). rewrite right_id left_id. apply wsat_init_state.
......
......@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
(** Alloc *)
Lemma sim_body_alloc fs ft r n T σs σt Φ :
Lemma sim_body_alloc_shared fs ft r n T σs σt Φ :
let ls := (fresh_block σs.(shp), 0) in
let lt := (fresh_block σt.(shp), 0) in
let ts := (Tagged σs.(snp)) in
......@@ -21,7 +21,8 @@ Lemma sim_body_alloc fs ft r n T σs σt Φ :
(init_stacks σt.(sst) lt (tsize T) tgt) σt.(scs)
(S σt.(snp)) σt.(snc) in
let r' : resUR :=
({[σt.(snp) := (to_tagKindR tkUnique, to_heapletR $ init_mem lt (tsize T) )]}, ε) in
(({[σt.(snp) := (to_tagKindR tkUnique, to_heapletR $ init_mem lt (tsize T) )]},
ε), ε) in
(ls = lt ts = tgt
Φ (r r') n (PlaceR ls ts T) σs' (PlaceR lt tgt T) σt' : Prop)
r {n,fs,ft} (Alloc T, σs) (Alloc T, σt) : Φ.
......@@ -43,15 +44,15 @@ Proof.
{ subst ls σs' ts. eapply (head_step_fill_tstep _ []), alloc_head_step. }
eexists _, σs', (r r'), (S n). split; last split.
{ left. by apply tc_once. }
{ have HLF : (r_f r).1 !! σt.(snp) = None.
{ destruct ((r_f r).1 !! σt.(snp)) as [[k h]|] eqn:Eqkh; [|done]. exfalso.
{ have HLF : (r_f r).(rtm) !! σt.(snp) = None.
{ destruct ((r_f r).(rtm) !! σt.(snp)) as [[k h]|] eqn:Eqkh; [|done]. exfalso.
destruct (tagKindR_valid k) as [k' Eqk'].
{ apply (Some_valid (k,h)). rewrite -Some_valid -Eqkh. apply VALID. }
destruct (PINV σt.(snp) k' h) as [Lt _]; [by rewrite Eqkh Eqk'|lia]. }
have VALID': (r_f r r').
{ apply (local_update_discrete_valid_frame _ ε r'); [by rewrite right_id|].
apply prod_local_update_1. rewrite /= right_id.
rewrite -(cmra_comm _ (r_f.1 r.1)) -insert_singleton_op //.
do 2 apply prod_local_update_1. rewrite /= right_id.
rewrite -(cmra_comm _ (r_f.(rtm) r.(rtm))) -insert_singleton_op //.
apply alloc_singleton_local_update; [done|]. split; [done|].
by apply to_heapletR_valid. }
have INCL: r_f r r_f r r' by apply cmra_included_l.
......@@ -98,7 +99,7 @@ Proof.
specialize (EQ _ Lti'). rewrite Z2Nat.id // in EQ. rewrite Eql EQ.
intros. inversion Eqstk. clear Eqstk. subst stk.
move : Instk. rewrite elem_of_list_singleton. by inversion 1.
- intros c cs. rewrite /= right_id => /CINV.
- intros c cs. rewrite /rcm /= right_id => /CINV.
destruct cs as [[T0|]| |]; [|done..]. intros [InT Eqh].
split; [done|]. intros t2 InT2. specialize (Eqh t2 InT2) as [Lt2 Eqh].
split; [lia|]. intros k2 h2. rewrite lookup_op.
......@@ -138,7 +139,7 @@ Qed.
(** Copy *)
Lemma sim_body_copy_public fs ft r n l t Ts Tt σs σt Φ
(EQS: tsize Ts = tsize Tt)
(PUBLIC: (h: heapletR), r.1 !! t Some (to_tagKindR tkPub, h)) :
(PUBLIC: (h: heapletR), r.(rtm) !! t Some (to_tagKindR tkPub, h)) :
( vs vt r',
read_mem l (tsize Ts) σs.(shp) = Some vs
read_mem l (tsize Tt) σt.(shp) = Some vt
......@@ -178,7 +179,7 @@ Proof.
have CORE : (r_f r) r_f r core (r_f r) by rewrite cmra_core_r.
assert (VREL': vrel (core (r_f r)) vs vt).
{ destruct PUBLIC as [h PUB].
destruct (ptrmap_lookup_op_r_equiv_pub r_f.1 r.1 t h) as [h0 Eqh0];
destruct (tmap_lookup_op_r_equiv_pub r_f.(rtm) r.(rtm) t h) as [h0 Eqh0];
[apply VALID|done|].
destruct (PINV _ _ _ Eqh0) as [Lt PB].
destruct SREL as (Eqst & Eqnp & Eqcs & Eqnc & PRIV).
......@@ -193,14 +194,14 @@ Proof.
{ rewrite HLs in Eqss'. symmetry in Eqss'. simplify_eq. move: AREL.
destruct ss as [| |l1 [t1|]|], st as [| |l2 [t2|]|]; auto; simpl; [|by intros [?[]]].
intros [? [? [h' Eqh']]]. simplify_eq. do 2 (split; [done|]).
exists h'. by apply ptrmap_lookup_core_pub. }
exists h'. by apply tmap_lookup_core_pub. }
destruct PV as (c' & T' & h' & Eqci & InT' & Eqh' & Inl).
(* impossible: t' is protected by c' which is still active.
So t t' and protected(t',c') is on top of (l + i), so access with t is UB *)
exfalso.
have NEQ: t' t.
{ intros ?. subst t'.
apply (ptrmap_lookup_op_r_equiv_pub r_f.1) in PUB as [? PUB];
apply (tmap_lookup_op_r_equiv_pub r_f.(rtm)) in PUB as [? PUB];
[|by apply VALID].
rewrite -> PUB in Eqh'. apply Some_equiv_inj in Eqh' as [Eqk' ?].
inversion Eqk'. }
......@@ -424,13 +425,14 @@ Qed.
Lemma sim_body_write_related_values
fs ft (r: resUR) k0 h0 n l tg Ts Tt v σs σt Φ
(EQS: tsize Ts = tsize Tt)
(Eqtg: r.1 !! tg = Some (to_tagKindR k0, h0))
(Eqtg: r.(rtm) !! tg = Some (to_tagKindR k0, h0))
(* assuming to-write values are related.
TODO: this is strong, since we should be able to write unrelated values
if we privately owns the heaplet we're writing to. *)
(PUBWRITE: s, s v arel r s s) :
let r' := if k0 then
(<[tg := (to_tagKindR tkUnique, write_heaplet l v h0)]> r.1, r.2)
((<[tg := (to_tagKindR tkUnique, write_heaplet l v h0)]> r.(rtm),
r.(rcm)), r.(rlm))
else r in
( α', memory_written σt.(sst) σt.(scs) l (Tagged tg) (tsize Tt) = Some α'
let σs' := mkState (write_mem l v σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
......@@ -464,35 +466,36 @@ Proof.
rewrite -Eqst -Eqcs -EQS in Eqα'. rewrite -EQS in EQL.
rewrite EQL in EqD. rewrite -Eqnp in IN.
eapply (head_step_fill_tstep _ []), write_head_step'; eauto. }
have HL: if k0 then kh, r_f.1 <[tg:=kh]> r.1 = <[tg:=kh]> (r_f.1 r.1) else True.
have HL: if k0 then kh, r_f.(rtm) <[tg:=kh]> r.(rtm) = <[tg:=kh]> (r_f.(rtm) r.(rtm)) else True.
{ destruct k0; [|done]. intros.
rewrite (ptrmap_insert_op_r r_f.1 r.1 tg h0) //. apply VALID. }
have HL2: if k0 then (r_f.1 r.1) !! tg = Some (to_tagKindR tkUnique, h0) else True.
rewrite (tmap_insert_op_r r_f.(rtm) r.(rtm) tg h0) //. apply VALID. }
have HL2: if k0 then (r_f.(rtm) r.(rtm)) !! tg = Some (to_tagKindR tkUnique, h0) else True.
{ destruct k0; [|done].
by apply (ptrmap_lookup_op_r _ _ _ _ (proj1 VALID) Eqtg). }
by apply (tmap_lookup_op_r _ _ _ _ (proj1 (proj1 VALID)) Eqtg). }
exists (#[])%V, σs', r', (S n). split; last split.
{ left. by constructor 1. }
{ split; last split; last split; last split; last split.
- by apply (tstep_wf _ _ _ STEPS WFS).
- by apply (tstep_wf _ _ _ STEPT WFT).
- (* valid *)
rewrite /r'. destruct k0; [|done]. split; simpl; [|apply VALID].
eapply ptrmap_valid; eauto; [|apply VALID]. split; [done|].
rewrite /r'. destruct k0; [|done]. do 2 (split; [|apply VALID]).
eapply tmap_valid; eauto; [|apply VALID]. split; [done|].
apply write_heaplet_valid.
have VL := (proj1 (cmra_valid_op_r _ _ VALID) tg).
have VL := (proj1 (proj1 (cmra_valid_op_r _ _ VALID)) tg).
rewrite Eqtg in VL. apply VL.
- (* ptrmap_inv *)
- (* tmap_inv *)
intros t k h Eqt.
have Eqttg: t = tg k0 = tkUnique k = k0 h write_heaplet l v h0.
{ intros. subst t k0. move : Eqt. rewrite /= HL lookup_insert.
{ intros. subst t k0. move : Eqt. rewrite /rtm /= HL lookup_insert.
intros [Eq1 Eq2]%Some_equiv_inj.
simpl in Eq1, Eq2. rewrite Eq2. repeat split; [|done].
destruct k; [done|inversion Eq1]. }
have CASEt : (t = tg k0 = tkUnique k = k0 h write_heaplet l v h0
(r_f r).1 !! t Some (to_tagKindR k, h) (k = tkUnique t tg)).
(r_f r).(rtm) !! t Some (to_tagKindR k, h)
(k = tkUnique t tg)).
{ move : Eqt. rewrite /r'.
destruct k0; simpl.
- rewrite /= HL.
- rewrite /rtm /= HL.
case (decide (t = tg)) => ?; [subst t|rewrite lookup_insert_ne //].
+ left. by destruct Eqttg.
+ right. naive_solver.
......@@ -537,7 +540,7 @@ Proof.
rewrite Eqs0.
destruct (to_agree_uninj s0) as [s1 Eq1]; [|by exists s1; rewrite -Eq1].
apply (lookup_valid_Some h0 (l + i)); [|by rewrite Eqs0].
apply (lookup_valid_Some (r_f.1 r.1) tg (to_tagKindR tkUnique, h0));
apply (lookup_valid_Some (r_f.(rtm) r.(rtm)) tg (to_tagKindR tkUnique, h0));
[by apply (proj1 VALID)|by rewrite HL2]. }
destruct (PINV tg tkUnique h0) as [Lt PI]; [by rewrite HL2|].
destruct (PI _ _ Eq0 _ Eqstk it2.(perm) opro) as [Eql' HTOP].
......@@ -577,7 +580,7 @@ Proof.
eapply (access1_write_remove_incompatible_active_SRO _ tg t _ _ _ ND); eauto.
- (* cmap_inv : make sure tags in the new resource are still on top *)
intros c cs Eqc'.
have Eqc: (r_f r).2 !! c Some cs.
have Eqc: (r_f r).(rcm) !! c Some cs.
{ move : Eqc'. rewrite /r'. by destruct k0. }
specialize (CINV _ _ Eqc). subst σt'. simpl.
clear -Eqα' CINV Eqtg VALID HL HL2. destruct cs as [[T|]| |]; [|done..].
......@@ -587,11 +590,11 @@ Proof.
(* TODO: duplicated proofs *)
rewrite /r'. destruct k0.
+ (* if tg was unique *)
rewrite HL.
rewrite /rtm /= HL.
case (decide (t = tg)) => ?.
{ subst tg. rewrite lookup_insert.
intros [Eqk Eqh]%Some_equiv_inj. simpl in Eqk, Eqh.
have Eqt : (r_f r).1 !! t Some (k, h0) by rewrite HL2 -Eqk.
have Eqt : (r_f r).(rtm) !! t Some (k, h0) by rewrite HL2 -Eqk.
intros l'. rewrite -Eqh write_heaplet_dom. intros Inh.
destruct (CINV _ _ Eqt _ Inh) as (stk' & pm' & Eqstk' & Instk' & NDIS).
destruct (for_each_access1_active_preserving _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
......@@ -630,19 +633,20 @@ Proof.
intros [? [? Eqt0]]. repeat split; [done..|].
destruct t0 as [t0|]; [|done].
repeat split. destruct Eqt0 as [ht0 Eqt0].
destruct (ptrmap_lookup_op_r_equiv_pub r_f.1 r.1 _ _ (proj1 VALID) Eqt0)
as [h' Eq'].
exists (h' ht0). rewrite HL lookup_insert_ne //.
destruct (tmap_lookup_op_r_equiv_pub r_f.(rtm) r.(rtm)
_ _ (proj1 (proj1 VALID)) Eqt0) as [h' Eq'].
exists (h' ht0). rewrite /rtm /= HL lookup_insert_ne //.
intros ?; subst t0. rewrite Eqtg in Eqt0.
apply Some_equiv_inj in Eqt0 as [Eqt0 _]. inversion Eqt0. }
{ destruct PV as (c & T & h & Eqc & InT & Eqt & Inh).
right. exists t, c, T.
case (decide (t = tg)) => ?; [subst t|].
- exists (write_heaplet l v h0). do 2 (split; [done|]). split.
by rewrite /= HL lookup_insert. rewrite write_heaplet_dom.
by rewrite /rtm /= HL lookup_insert.
rewrite write_heaplet_dom.
rewrite HL2 in Eqt. apply Some_equiv_inj in Eqt as [? Eqt].
simpl in Eqt. by rewrite Eqt.
- exists h. rewrite /= HL. do 2 (split; [done|]).
- exists h. rewrite /rtm /= HL. do 2 (split; [done|]).
rewrite lookup_insert_ne //. }
* (* tg was public, and (l + i) was written to *)
left. exists s. split; [done|].
......@@ -659,7 +663,7 @@ Proof.
intros [? [? Eqt]]. subst l3 t3. repeat split.
destruct t0 as [t0|]; [|done].
destruct Eqt as [h Eqt]. exists h.
rewrite /= HL (lookup_insert_ne _ tg) //.
rewrite /rtm /= HL (lookup_insert_ne _ tg) //.
intros ?. subst t0. move : Eqt. rewrite lookup_op Eqtg.
by apply tagKindR_exclusive.
* (* tg was public, and l1 was NOT written to *)
......@@ -667,10 +671,10 @@ Proof.
exists t, c, T. simpl.
case (decide (t = tg)