Commit 383206b7 authored by Hai Dang's avatar Hai Dang

Merge branch 'retag_sem'

parents 1a11cc73 4865b710
This diff is collapsed.
......@@ -32,7 +32,7 @@ Fixpoint subst (x : string) (es : expr) (e : expr) : expr :=
| Deref e T => Deref (subst x es e) T
| Ref e => Ref (subst x es e)
(* | Field e path => Field (subst x es e) path *)
| Retag e kind => Retag (subst x es e) kind
| Retag e pkind T kind => Retag (subst x es e) pkind T kind
| Let x1 e1 e2 =>
Let x1 (subst x es e1)
(if bool_decide (BNamed x x1) then subst x es e2 else e2)
......@@ -107,7 +107,7 @@ Inductive ectx_item :=
| DerefCtx (T: type)
| RefCtx
(* | FieldCtx (path : list nat) *)
| RetagCtx (kind: retag_kind)
| RetagCtx (pkind: pointer_kind) (T: type) (kind: retag_kind)
| LetCtx (x: binder) (e2: expr)
| CaseCtx (el : list expr).
......@@ -137,7 +137,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
| DerefCtx T => Deref e T
| RefCtx => Ref e
(* | FieldCtx path => Field e path *)
| RetagCtx kind => Retag e kind
| RetagCtx pk T kind => Retag e pk T kind
| LetCtx x e2 => Let x e e2
| CaseCtx el => Case e el
end.
......@@ -342,11 +342,11 @@ Inductive mem_expr_step (h: mem) : expr → event → mem → expr → Prop :=
h (Free (Place l lbor T))
(DeallocEvt l lbor T)
(free_mem l (tsize T) h) #[]
| RetagBS x xbor T kind :
| RetagBS l otag ntag pkind T kind :
mem_expr_step
h (Retag (Place x xbor T) kind)
(RetagEvt x T kind)
h #[]
h (Retag #[ScPtr l otag] pkind T kind)
(RetagEvt l otag ntag pkind T kind)
h #[ScPtr l ntag]
(* | ForkBS e h:
expr_step (Fork e) h SilentEvt (Lit LitPoison) h [e] *)
(* observable behavior *)
......
......@@ -70,25 +70,6 @@ Lemma of_result_list_expr (vl: list value) :
(of_result <$> (ValR <$> vl)) = Val <$> vl.
Proof. induction vl as [|v vl IH]; [done|]. by rewrite 3!fmap_cons IH. Qed.
(* Lemma subst_is_closed X x es e :
is_closed X es is_closed (x::X) e is_closed X (subst x es e).
Proof.
revert e X. fix FIX 1; destruct e=>X //=; repeat (case_bool_decide=>//=);
try naive_solver; rewrite ?andb_True; intros.
- set_solver.
- split; first naive_solver. induction el; naive_solver.
- (* eauto using is_closed_weaken with set_solver. *)
- eapply is_closed_weaken; first done.
destruct (decide (BNamed x = f)), (decide (BNamed x xl)); set_solver.
- induction el; naive_solver.
- split; first naive_solver. induction el; naive_solver.
Qed.
Lemma subst'_is_closed X b es e :
is_closed X es is_closed (b:b:X) e is_closed X (subst' b es e).
Proof. destruct b; first done. apply subst_is_closed. Qed.
*)
(** Equality and other typeclass stuff *)
Instance bin_op_eq_dec : EqDecision bin_op.
......@@ -161,7 +142,8 @@ Fixpoint expr_beq (e : expr) (e' : expr) : bool :=
bool_decide (l = l') && bool_decide (bor = bor') && bool_decide (T = T')
| Deref e T, Deref e' T' =>
bool_decide (T = T') && expr_beq e e'
| Retag e kind, Retag e' kind' =>
| Retag e pk T kind, Retag e' pk' T' kind' =>
bool_decide (pk = pk') && bool_decide (T = T') &&
bool_decide (kind = kind') && expr_beq e e'
| Copy e, Copy e' | Ref e, Ref e' | InitCall e, InitCall e'
(* | AtomRead e, AtomRead e' *) | EndCall e, EndCall e' => expr_beq e e'
......@@ -228,8 +210,11 @@ Proof.
| Deref e T => GenNode 13 [GenLeaf $ inl $ inr $ inr $ inr T; go e]
| Ref e => GenNode 14 [go e]
(* | Field e path => GenNode 15 [GenLeaf $ inr $ inl $ inl (* $ inl *) path; go e] *)
| Retag e kind => GenNode 15 [GenLeaf $ inr $ inl (* $ inr $ inr *) kind; go e]
| Let x e1 e2 => GenNode 16 [GenLeaf $ inr $ inr x; go e1; go e2]
| Retag e pk T kind =>
GenNode 15 [GenLeaf $ inr $ inl $ inl pk;
GenLeaf $ inr $ inl $ inr T;
GenLeaf $ inr $ inr $ inl kind; go e]
| Let x e1 e2 => GenNode 16 [GenLeaf$ inr $ inr $ inr x; go e1; go e2]
| Case e el => GenNode 17 (go e :: (go <$> el))
(* | Fork e => GenNode 23 [go e]
| SysCall id => GenNode 24 [GenLeaf $ inr $ inr id] *)
......@@ -256,9 +241,11 @@ Proof.
| GenNode 13 [GenLeaf (inl (inr (inr (inr T)))); e] => Deref (go e) T
| GenNode 14 [e] => Ref (go e)
(* | GenNode 15 [GenLeaf (inr (inl (inl (* (inl *) path(* ) *)))); e] => Field (go e) path *)
| GenNode 15 [GenLeaf (inr (inl (* (inr (inr *) kind (* ) ) *))); e] =>
Retag (go e) kind
| GenNode 16 [GenLeaf (inr (inr x)); e1; e2] => Let x (go e1) (go e2)
| GenNode 15 [GenLeaf (inr (inl (inl pk)));
GenLeaf (inr (inl (inr T)));
GenLeaf (inr (inr (inl kind))); e] =>
Retag (go e) pk T kind
| GenNode 16 [GenLeaf (inr (inr (inr x))); e1; e2] => Let x (go e1) (go e2)
| GenNode 17 (e :: el) => Case (go e) (go <$> el)
(* | GenNode 23 [e] => Fork (go e)
| GenNode 24 [GenLeaf (inr (inr id))] => SysCall id *)
......@@ -346,10 +333,10 @@ Inductive head_step :
| HeadPureS σ e e' ev
(ExprStep: pure_expr_step fns σ.(shp) e ev e')
: head_step e σ [ev] e' σ []
| HeadImpureS σ e e' ev h0 h' α' cids' nxtp' nxtc'
(ExprStep : mem_expr_step σ.(shp) e ev h0 e')
(InstrStep: bor_step h0 σ.(sst) σ.(scs) σ.(snp) σ.(snc)
ev h' α' cids' nxtp' nxtc')
| HeadImpureS σ e e' ev h' α' cids' nxtp' nxtc'
(ExprStep : mem_expr_step σ.(shp) e ev h' e')
(InstrStep: bor_step σ.(sst) σ.(scs) σ.(snp) σ.(snc)
ev α' cids' nxtp' nxtc')
: head_step e σ [ev] e' (mkState h' α' cids' nxtp' nxtc') [].
Lemma result_head_stuck e1 σ1 κ e2 σ2 efs :
......@@ -400,4 +387,13 @@ Qed.
(* Allocate a place of type [T] and initialize it with a value [v] *)
Definition new_place T (v: expr) : expr :=
let: "x" := Alloc T in "x" <- v ;; "x".
let: "x" := Alloc T in "x" <- v ;; "x".
(* Retag a place [p] that is a pointer of kind [pk] to a region of type [T],
with retag [kind] *)
Definition retag_place
(p: expr) (pk: pointer_kind) (T: type) (kind: retag_kind) : expr :=
let: "p" := p in
(* read the current pointer stored in the place [p] *)
(* retag and update [p] with the pointer with new tag *)
"p" <- Retag (Copy "p") pk T kind.
......@@ -177,8 +177,9 @@ Inductive expr :=
(* | CAS (e0 e1 e2 : expr) *) (* CAS the value `e2` for `e1` to the place `e0` *)
(* | AtomWrite (e1 e2: expr) *)
(* | AtomRead (e: expr) *)
(* retag *)
| Retag (e : expr) (kind: retag_kind) (* Retag the place `e` with retag kind `kind`. *)
(* retag *) (* Retag the memory pointed to by `e` of type (Reference pk T) with
retag kind `kind`. *)
| Retag (e : expr) (pk: pointer_kind) (T: type) (kind: retag_kind)
(* let binding *)
| Let (x : binder) (e1 e2: expr)
(* case *)
......@@ -209,7 +210,7 @@ Arguments Free _%E.
(* Arguments CAS _%E _%E _%E. *)
(* Arguments AtomWrite _%E _%E. *)
(* Arguments AtomRead _%E. *)
Arguments Retag _%E _.
Arguments Retag _%E _ _ _.
Arguments Let _%binder _%E _%E.
Arguments Case _%E _%E.
(* Arguments Fork _%E. *)
......@@ -225,7 +226,7 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
| Let x e1 e2 => is_closed X e1 && is_closed (x :b: X) e2
| Case e el | Call e el (* | App e el *)
=> is_closed X e && forallb (is_closed X) el
| Copy e | Retag e _ | Deref e _ | Ref e (* | Field e _ *)
| Copy e | Retag e _ _ _ | Deref e _ | Ref e (* | Field e _ *)
| Free e | InitCall e | EndCall e (* | AtomRead e | Fork e *)
=> is_closed X e
(* | CAS e0 e1 e2 => is_closed X e0 && is_closed X e1 && is_closed X e2 *)
......@@ -305,7 +306,7 @@ Inductive event :=
| NewCallEvt (fid: fn_id)
| InitCallEvt (c: call_id)
| EndCallEvt (c: call_id) (v: value)
| RetagEvt (x: loc) (T: type) (kind: retag_kind)
| RetagEvt (l: loc) (otag ntag: tag) (pk: pointer_kind) (T: type) (kind: retag_kind)
(* | SysCallEvt (id: nat) *)
| SilentEvt
.
......@@ -21,7 +21,7 @@ Ltac inv_head_step :=
inversion H ; subst; clear H
| H : pure_expr_step _ _ _ _ _ |- _ =>
inversion H ; subst; clear H
| H : bor_step _ _ _ _ _ _ _ _ _ _ _ |- _ =>
| H : bor_step _ _ _ _ _ _ _ _ _ |- _ =>
inversion H ; subst; clear H
end.
......@@ -853,9 +853,10 @@ Qed.
(** Retag *)
Lemma fill_retag_decompose K e kind e':
fill K e = Retag e' kind
K = [] e = Retag e' kind ( K', K = K' ++ [RetagCtx kind] fill K' e = e').
Lemma fill_retag_decompose K e pkind T kind e':
fill K e = Retag e' pkind T kind
K = [] e = Retag e' pkind T kind
( K', K = K' ++ [RetagCtx pkind T kind] fill K' e = e').
Proof.
revert e e'.
induction K as [|Ki K IH]; [by left|]. simpl.
......@@ -866,20 +867,22 @@ Proof.
- subst K. by exists (Ki :: K0).
Qed.
Lemma tstep_retag_inv x tg T pk rk e' σ σ'
(STEP: (Retag (Place x tg (Reference pk T)) rk, σ) ~{fns}~> (e', σ')) :
c cids h' α' nxtp',
Lemma tstep_retag_inv (ptr: result) T pk rk e' σ σ'
(STEP: (Retag ptr pk T rk, σ) ~{fns}~> (e', σ')) :
l otg c cids ntg α' nxtp',
ptr = ValR [ScPtr l otg]
σ.(scs) = c :: cids
retag σ.(shp) σ.(sst) σ.(snp) σ.(scs) c x rk (Reference pk T)
= Some (h', α', nxtp')
e' = #[]%V
σ' = mkState h' α' σ.(scs) nxtp' σ.(snc).
retag σ.(sst) σ.(snp) σ.(scs) c l otg rk pk T = Some (ntg, α', nxtp')
e' = #[ScPtr l ntg]%V
σ' = mkState σ.(shp) α' σ.(scs) nxtp' σ.(snc).
Proof.
inv_tstep. symmetry in Eq.
destruct (fill_retag_decompose _ _ _ _ Eq) as [[]|[K' [? Eq']]]; subst.
- clear Eq. simpl in HS. inv_head_step. naive_solver.
destruct (fill_retag_decompose _ _ _ _ _ _ Eq) as [[]|[K' [? Eq']]]; subst.
- clear Eq. simpl in HS. inv_head_step.
have Eq1 := to_of_result ptr. rewrite -H0 /to_result in Eq1. simplify_eq.
naive_solver.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
+ rewrite /= Eq'. by eexists.
+ rewrite /= Eq' to_of_result. by eexists.
+ by rewrite Eq1' in HS.
Qed.
......
This diff is collapsed.
This diff is collapsed.
......@@ -17,7 +17,7 @@ Lemma expr_ind (P : expr → Prop):
( e1 e2, P e1 P e2 P (Write e1 e2))
( ty, P (Alloc ty))
( e, P e P (Free e))
( e k, P e P (Retag e k))
( e pk T rk, P e P (Retag e pk T rk))
( b e1 e2, P e1 P e2 P (Let b e1 e2))
( e el, P e Forall P el P (Case e el))
e, P e.
......@@ -26,6 +26,8 @@ Proof.
(* Find head symbol, then find lemma for that symbol.
We have to be this smart because we can't use the unguarded [REC]! *)
match goal with
| |- P (?head _ _ _ _) =>
match goal with H : context[head] |- _ => apply H; try done end
| |- P (?head _ _ _) =>
match goal with H : context[head] |- _ => apply H; try done end
| |- P (?head _ _) =>
......@@ -60,7 +62,7 @@ Fixpoint subst_map (xs : gmap string result) (e : expr) : expr :=
| Free e => Free (subst_map xs e)
| Deref e T => Deref (subst_map xs e) T
| Ref e => Ref (subst_map xs e)
| Retag e kind => Retag (subst_map xs e) kind
| Retag e pk T kind => Retag (subst_map xs e) pk T kind
| Let x1 e1 e2 =>
Let x1
(subst_map xs e1)
......
......@@ -8,7 +8,7 @@ Set Default Proof Using "Type".
Definition ex1_unopt : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in (* put argument into place *)
Retag "x" Default ;;
retag_place "x" (RefPtr Mutable) int Default ;;
Call #[ScFnPtr "f"] [] ;;
*{int} "x" <- #[42] ;;
Call #[ScFnPtr "g"] [] ;;
......@@ -20,7 +20,7 @@ Definition ex1_unopt : function :=
Definition ex1_opt : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" Default ;;
retag_place "x" (RefPtr Mutable) int Default ;;
Call #[ScFnPtr "f"] [] ;;
*{int} "x" <- #[42] ;;
let: "v" := Copy *{int} "x" in
......@@ -42,11 +42,20 @@ Proof.
intros sarg ->.
sim_apply sim_simple_let=>/=.
apply: sim_simple_result.
(* Retag local *)
(* Retag a local place *)
sim_apply sim_simple_let=>/=.
apply Forall2_cons_inv in AREL as [AREL _].
sim_apply sim_simple_retag_local; [simpl; lia|solve_sim..|].
move=>l_i tg_i hplt /= Hl_i.
sim_apply sim_simple_let=>/=.
(* Copy local place *)
sim_apply sim_simple_copy_local; [solve_sim..|].
apply: sim_simple_result. simpl.
(* Retag *)
sim_apply sim_simple_retag_mut_ref; [simpl; lia| |eauto|..]; [solve_sim|].
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..|].
intros s ?. simplify_eq.
(* Call *)
sim_apply sim_simple_let=>/=.
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
......@@ -95,11 +104,10 @@ Proof.
sim_apply sim_simple_let=>/=.
sim_apply sim_simple_free_public.
{ simpl. constructor; [|by constructor].
(* FIXME: fix automation *)
apply: arel_mono; last fast_done.
apply: cmra_valid_included; first fast_done.
do 3 apply cmra_mono_r. solve_res. solve_res. }
simpl. sim_apply sim_simple_let=>/=.
sim_apply sim_simple_let=>/=.
(* Finishing up. *)
apply: sim_simple_result. split.
- solve_res.
......
......@@ -8,17 +8,19 @@ Set Default Proof Using "Type".
Definition ex1_down : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in (* put argument into place *)
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i" ;;
"v"
.
Definition ex1_down_opt : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i" ;;
Copy *{int} "x"
.
......
......@@ -8,19 +8,22 @@ Set Default Proof Using "Type".
Definition ex2 : function :=
fun: ["i"],
let: "x" := new_place (& int) "i" in
Retag "x" Default ;;
retag_place "x" (RefPtr Immutable) int Default ;;
Copy *{int} "x" ;;
Call #[ScFnPtr "f"] ["x"] ;;
Copy *{int} "x"
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
"v"
.
Definition ex2_opt : function :=
fun: ["i"],
let: "x" := new_place (& int) "i" in
Retag "x" Default ;;
retag_place "x" (RefPtr Immutable) int Default ;;
Copy *{int} "x" ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] ["x"] ;;
Free "x" ;; Free "i" ;;
"v"
.
......
......@@ -8,18 +8,21 @@ Set Default Proof Using "Type".
Definition ex2_down : function :=
fun: ["i"],
let: "x" := new_place (& int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Immutable) int FnEntry ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] ["x"] ;;
Free "x" ;; Free "i" ;;
"v"
.
Definition ex2_down_opt : function :=
fun: ["i"],
let: "x" := new_place (& int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Immutable) int FnEntry ;;
Call #[ScFnPtr "f"] ["x"] ;;
Copy *{int} "x"
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
"v"
.
......
......@@ -4,32 +4,36 @@ Set Default Proof Using "Type".
(** Moving a write to a mutable reference up across unknown code. *)
(* TODO: check if Free is in the right place *)
(* Assuming x : &mut i32 *)
Definition ex3 : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
*{int} "x" <- #[42] ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
"v"
.
Definition ex3_opt_1 : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
*{int} "x" <- #[42] ;;
*{int} "x" <- #[13] ;;
Call #[ScFnPtr "f"] []
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i"
.
Definition ex3_opt_2 : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
*{int} "x" <- #[13] ;;
Call #[ScFnPtr "f"] []
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i"
.
Lemma ex3_sim_fun : ⊨ᶠ ex3 ex3_opt_1.
......
......@@ -8,29 +8,32 @@ Set Default Proof Using "Type".
Definition ex3_down : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
*{int} "x" <- #[42] ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
"v"
.
Definition ex3_down_opt_1 : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[42] ;;
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
"v"
.
Definition ex3_down_opt_2 : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in
Retag "x" FnEntry ;;
retag_place "x" (RefPtr Mutable) int FnEntry ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
"v"
.
......
From stbor.lang Require Import steps_retag.
From stbor.lang Require Import steps_retag steps_progress.
From stbor.sim Require Export instance.
Set Default Proof Using "Type".
......
......@@ -27,7 +27,7 @@ Fixpoint expr_wf (e: expr) : Prop :=
| Val v => value_wf v
| Call f args => expr_wf f Forall id (fmap expr_wf args)
| Case e branches => expr_wf e Forall id (fmap expr_wf branches)
| Deref e _ | Ref e | Copy e | Free e | Retag e _ =>
| Deref e _ | Ref e | Copy e | Free e | Retag e _ _ _ =>
expr_wf e
| Proj e1 e2 | Conc e1 e2 | BinOp _ e1 e2 | Let _ e1 e2 | Write e1 e2 =>
expr_wf e1 expr_wf e2
......
......@@ -421,7 +421,7 @@ Proof.
apply: sim_body_result. intros. eapply POST; eauto.
Qed.
(** Freeing to unique/local *)
(** Freeing unique/local *)
(* This one deallocates [l] with [tsize T] and tag [t]. It also deallocates
the logical resource [res_tag t k h0]. In general, we can require that any
locations in [h0] be included in [T]. Here, we prove a simple lemma where
......@@ -430,7 +430,6 @@ Lemma sim_body_free_unique_local_1 fs ft r r' n l t k T s σs σt Φ :
tsize T = 1%nat
r r' res_tag t k {[l := s]}
(k = tkLocal k = tkUnique)
(* is_Some (h0 !! l) *)
(is_Some (σs.(shp) !! l) is_Some (σt.(shp) !! l)
α', memory_deallocated σt.(sst) σt.(scs) l (Tagged t) (tsize T) = Some α'
let σs' := mkState (free_mem l (tsize T) σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
......@@ -1222,43 +1221,119 @@ Proof.
Qed.
(** Retag *)
Lemma sim_body_retag_public fs ft r n ptr pk T kind σs σt Φ
(RREL: rrel r ptr ptr) :
( l otg ntg α' nxtp' c cids,
ptr = ValR [ScPtr l otg]
σt.(scs) = c :: cids
retag σt.(sst) σt.(snp) σt.(scs) c l otg kind pk T = Some (ntg, α', nxtp')
let σs' := mkState σs.(shp) α' σs.(scs) nxtp' σs.(snc) in
let σt' := mkState σt.(shp) α' σt.(scs) nxtp' σt.(snc) in
Φ r n (ValR [ScPtr l ntg]) σs' (ValR [ScPtr l ntg]) σt')
r {n,fs,ft}
(Retag ptr pk T kind, σs)
(Retag ptr pk T kind, σt) : Φ.
Proof.
intros POST. pfold. intros NT. intros.
have WSAT1 := WSAT. (* back up *)
destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Lemma sim_body_retag_local_mut_ref fs ft r r' r'' n x xt xs xs' rs T σs σt Φ :
split; [|done|].
{ (* tgt reducible *)
right.
edestruct NT as [[]|[es' [σs' STEPS]]]; [constructor 1|done|].
(* inversion retag of src *)
destruct (tstep_retag_inv _ _ _ _ _ _ _ _ STEPS)
as (l & otg & c & cids & ntg & α' & nxtp' & ? & Eqs & EqT & ? & ?).
subst ptr es'.
destruct SREL as (Eqsst & Eqnp & Eqcs & Eqnc & PUBP).
exists (#[ScPtr l ntg])%V,
(mkState σt.(shp) α' σt.(scs) nxtp' σt.(snc)).
eapply (head_step_fill_tstep _ []), retag_head_step'.
- rewrite -Eqcs; eauto.
- by rewrite -Eqsst -Eqnp -Eqcs. }
constructor 1.
intros.
(* inversion retag of tgt *)
destruct (tstep_retag_inv _ _ _ _ _ _ _ _ STEPT)
as (l & otg & c & cids & ntg & α' & nxtp' & ? & Eqs & EqT & ? & ?).
subst ptr et'.
exists (#[ScPtr l ntg])%V,
(mkState σs.(shp) α' σs.(scs) nxtp' σs.(snc)),
r, n. subst σt'.
split; last split.
{ left. constructor.
destruct SREL as (Eqsst & Eqnp & Eqcs & Eqnc & PUBP).
eapply (head_step_fill_tstep _ []), retag_head_step'.
- rewrite Eqcs; eauto.
- by rewrite Eqsst Eqnp Eqcs. }
{ (* unfolding rrel for place *)
simpl in RREL.
inversion RREL as [|???? AREL _]; subst; simplify_eq. clear RREL.
destruct AREL as (_ & _ & AREL).
admit. }
left.
apply: sim_body_result. intros. eapply POST; eauto.
Abort.
Lemma sim_body_retag_mut_ref_default fs ft r r' rs n l told T σs σt Φ :
(0 < tsize T)%nat
(* owns local x with tag xt and value xs *)
r r' res_loc x [(xs,xs)] xt
(* xs is supposed to be a Ptr(li,told), and, coming from the arguments, told
must be a public tag. *)
arel rs xs' xs
r' r'' rs
let Tr := (Reference (RefPtr Mutable) T) in
( li told,
xs = ScPtr li told
tnew hplt c cids hs' αs' nps' ht' αt' npt' (STACK: σt.(scs) = c :: cids),
retag σt.(shp) σt.(sst) σt.(snp) σt.(scs) c x Default Tr
= Some (ht', αt', npt')
retag σs.(shp) σs.(sst) σs.(snp) σs.(scs) c x Default Tr
= Some (hs', αs', nps')
let σs' := mkState hs' αs' σs.(scs) nps' σs.(snc) in
let σt' := mkState ht' αt' σt.(scs) npt' σt.(snc) in
let s_new := ScPtr li (Tagged tnew) in
let tk := tkUnique in
is_Some (hplt !! li)
tag_on_top αt' li tnew
Φ (r'' rs res_loc x [(s_new,s_new)] xt res_tag tnew tk hplt)
n (ValR [%S]) σs' (ValR [%S]) σt')
r r' rs
let pk : pointer_kind := (RefPtr Mutable) in
let otg : tag := Tagged told in
let s_old : scalar := ScPtr l otg in
(* Ptr(l,otg) comes from the arguments, so [otg] must be a public tag. *)
arel rs s_old s_old
( tnew hplt c cids αs' nps' αt' npt' (STACK: σt.(scs) = c :: cids),
retag σt.(sst) σt.(snp) σt.(scs) c l otg Default pk T
= Some ((Tagged tnew), αt', npt')
retag σs.(sst) σs.(snp) σs.(scs) c l otg Default pk T
= Some ((Tagged tnew), αs', nps')
(* [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. *)
( i: nat, (i < tsize T)
is_Some $ hplt !! (l + i) tag_on_top αt' (l + i) tnew)
let σs' := mkState σs.(shp) αs' σs.(scs) nps' σs.(snc) in
let σt' := mkState σt.(shp) αt' σt.(scs) npt' σt.(snc) in
let s_new := ScPtr l (Tagged tnew) in
Φ (r res_tag tnew tkUnique hplt) n (ValR [s_new]) σs' (ValR [s_new]) σt')
r {n,fs,ft}
(Retag (Place x (Tagged xt) Tr) Default, σs)
(Retag (Place x (Tagged xt) Tr) Default, σt) : Φ.
(Retag #[s_old] pk T Default, σs)
(Retag #[s_old] pk T Default, σt) : Φ.
Proof.
intros NZST Eqr PTag Eqr' Tr POST. pfold. intros NT. intros.
intros NZST Eqr pk otg s_old AREL POST. pfold. intros NT. intros.
have WSAT1 := WSAT. (* back up *)
destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).