Commit e5bcee56 authored by Hai Dang's avatar Hai Dang

WIP: fixing retag semantics

parent efefa48e
......@@ -350,12 +350,36 @@ Definition retag_ref h α cids (nxtp: ptr_id) l (old_tag: tag) T
Definition adding_protector (kind: retag_kind) (c: call_id) : option call_id :=
match kind with FnEntry => Some c | _ => None end.
(* This implements EvalContextExt::retag *)
(* This *partly* implements EvalContextExt::retag *)
(* Assumption: ct cids *)
Definition retag1
h α (nxtp: ptr_id) (cids: call_id_stack) (ct: call_id)
(l: loc) (otag: tag) (kind: retag_kind) pk Tr :
option (tag * stacks * ptr_id) :=
let qualify : option (ref_kind * option call_id) :=
match pk, kind with
(* Mutable reference *)
| RefPtr Mutable, _ =>
Some (UniqueRef (is_two_phase kind), adding_protector kind ct)
(* Immutable reference *)
| RefPtr Immutable, _ => Some (SharedRef, adding_protector kind ct)
(* If is both raw ptr and Raw retagging, no protector *)
| RawPtr mut, RawRt => Some (RawRef (bool_decide (mut = Mutable)), None)
(* Box pointer, no protector *)
| BoxPtr, _ => Some (UniqueRef false, None)
(* Ignore Raw pointer otherwise *)
| RawPtr _, _ => None
end in
match qualify with
| Some (rkind, protector) => retag_ref h α cids nxtp l otag Tr rkind protector
| None => Some (otag, α, nxtp)
end
.
Equations retag
(h: mem) α (nxtp: ptr_id) (cids: call_id_stack) (ct: call_id) (x: loc) (kind: retag_kind) T :
option (mem * stacks * ptr_id) :=
retag h α nxtp cids ct x kind (FixedSize _) := Some (h, α, nxtp) ;
retag h α nxtp cids ct x kind (FixedSize _) := Some (h, α, nxtp) ;
retag h α nxtp cids ct x kind (Union _) := Some (h, α, nxtp) ;
retag h α nxtp cids ct x kind (Unsafe T) := retag h α nxtp cids ct x kind T ;
retag h α nxtp cids ct x kind (Reference pk Tr) with h !! x :=
......@@ -416,7 +440,7 @@ Infix "<<t" := tag_values_included (at level 60, no associativity).
(** Instrumented step for the stacked borrows *)
(* This ignores CAS for now. *)
Inductive bor_step h α (cids: call_id_stack) (nxtp: ptr_id) (nxtc: call_id):
event mem stacks call_id_stack ptr_id call_id Prop :=
event stacks call_id_stack ptr_id call_id Prop :=
(* | SysCallIS id :
bor_step h α β nxtp (SysCallEvt id) h α β nxtp *)
(* This implements EvalContextExt::new_allocation. *)
......@@ -424,30 +448,30 @@ Inductive bor_step h α (cids: call_id_stack) (nxtp: ptr_id) (nxtc: call_id):
(* Tagged nxtp is the first borrow of the variable x,
used when accessing x directly (not through another pointer) *)
bor_step h α cids nxtp nxtc
(AllocEvt x (Tagged nxtp) T) h
(AllocEvt x (Tagged nxtp) T)
(init_stacks α x (tsize T) (Tagged nxtp)) cids (S nxtp) nxtc
(* This implements AllocationExtra::memory_read. *)
| CopyIS α' l lbor T vl
(ACC: memory_read α cids l lbor (tsize T) = Some α')
(* This comes from wellformedness, but for convenience we require it here *)
(BOR: vl <<t nxtp):
bor_step h α cids nxtp nxtc (CopyEvt l lbor T vl) h α' cids nxtp nxtc
bor_step h α cids nxtp nxtc (CopyEvt l lbor T vl) α' cids nxtp nxtc
(* This implements AllocationExtra::memory_written. *)
| WriteIS α' l lbor T vl
(ACC: memory_written α cids l lbor (tsize T) = Some α')
(* This comes from wellformedness, but for convenience we require it here *)
(BOR: vl <<t nxtp) :
bor_step h α cids nxtp nxtc (WriteEvt l lbor T vl) h α' cids nxtp nxtc
bor_step h α cids nxtp nxtc (WriteEvt l lbor T vl) α' cids nxtp nxtc
(* This implements AllocationExtra::memory_deallocated. *)
| DeallocIS α' l lbor T
(ACC: memory_deallocated α cids l lbor (tsize T) = Some α') :
bor_step h α cids nxtp nxtc (DeallocEvt l lbor T) h α' cids nxtp nxtc
bor_step h α cids nxtp nxtc (DeallocEvt l lbor T) α' cids nxtp nxtc
| InitCallIS :
bor_step h α cids nxtp nxtc (InitCallEvt nxtc) h α (nxtc :: cids) nxtp (S nxtc)
bor_step h α cids nxtp nxtc (InitCallEvt nxtc) α (nxtc :: cids) nxtp (S nxtc)
| EndCallIS c cids' v
(TOP: cids = c :: cids') :
bor_step h α cids nxtp nxtc (EndCallEvt c v) h α cids' nxtp nxtc
| RetagIS h' α' nxtp' x T kind c cids'
bor_step h α cids nxtp nxtc (EndCallEvt c v) α cids' nxtp nxtc
| RetagIS α' nxtp' l otag ntag T kind pkind c cids'
(TOP: cids = c :: cids')
(RETAG: retag h α nxtp cids c x kind T = Some (h', α', nxtp')) :
bor_step h α cids nxtp nxtc (RetagEvt x T kind) h' α' cids nxtp' nxtc.
(RETAG: retag1 h α nxtp cids c l otag kind pkind T = Some (ntag, α', nxtp')) :
bor_step h α cids nxtp nxtc (RetagEvt l otag ntag pkind T kind) α' cids nxtp' nxtc.
......@@ -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 *)
......
......@@ -161,7 +161,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 +229,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 +260,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 +352,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 h' σ.(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 +406,14 @@ 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 tag of the place [p] *)
let: "o" := & "p" in
(* retag and update with new tag *)
"p" <- Retag "o" 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,17 +867,17 @@ 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 l otg T pk rk e' σ σ'
(STEP: (Retag #[ScPtr l otg] pk T rk, σ) ~{fns}~> (e', σ')) :
c cids ntg α' nxtp',
σ.(scs) = c :: cids
retag σ.(shp) σ.(sst) σ.(snp) σ.(scs) c x rk (Reference pk T)
= Some (h', α', nxtp')
e' = #[]%V
σ' = mkState h' α' σ.(scs) nxtp' σ.(snc).
retag1 σ.(shp) σ.(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.
destruct (fill_retag_decompose _ _ _ _ _ _ Eq) as [[]|[K' [? Eq']]]; subst.
- clear Eq. simpl in HS. inv_head_step. naive_solver.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
+ rewrite /= Eq'. by eexists.
......
......@@ -991,10 +991,12 @@ Definition pointer_kind_access pk :=
| RefPtr Mutable | RawPtr Mutable | BoxPtr => AccessWrite
| _ => AccessRead
end.
Definition valid_location (h: mem) (α: stacks) cids (x: loc) pk T :=
l tg, h !! x = Some (ScPtr l tg) is_freeze T
Definition valid_block (h: mem) (α: stacks) cids (l: loc) (tg: tag) pk T :=
is_freeze T
( m, (m < tsize T)%nat l + m dom (gset loc) h stk,
α !! (l + m) = Some stk access1_pre cids stk (pointer_kind_access pk) tg).
Definition valid_location (h: mem) (α: stacks) cids (x: loc) pk T :=
l tg, h !! x = Some (ScPtr l tg) valid_block h α cids l tg pk T.
Definition valid_mem_ptr h α cids x T :=
(n: nat) pk Tr, (n, Reference pk Tr) sub_ref_types T
valid_location h α cids (x + n) pk Tr.
......@@ -1002,8 +1004,7 @@ Definition valid_mem_sum (h: mem) l T :=
Ts (n: nat), (n, Sum Ts) sub_sum_types T i,
h !! (l + n) = Some (ScInt i) 0 i < length Ts.
Lemma retag1_is_freeze_is_Some h α nxtp cids c x kind pk T
Lemma retag1_nested_is_freeze_is_Some h α nxtp cids c x kind pk T
(EqD: dom (gset loc) h dom (gset loc) α)
(LOC: valid_location h α cids x pk T) :
is_Some (retag h α nxtp cids c x kind (Reference pk T)).
......@@ -1034,6 +1035,39 @@ Proof.
destruct (EQD _ Lt) as [_ [stk' [Eq' ?]]]. by simplify_eq.
Qed.
Lemma retag1_is_freeze_is_Some h α nxtp cids c l otg kind pk T
(EqD: dom (gset loc) h dom (gset loc) α)
(LOC: valid_block h α cids l otg pk T) :
is_Some (retag1 h α nxtp cids c l otg kind pk T).
Proof.
destruct LOC as (FRZ & EQD).
destruct pk as [[]|mut|]; simpl.
- destruct (retag_ref_is_freeze_is_Some h α cids nxtp l otg T
(UniqueRef (is_two_phase kind)) (adding_protector kind c))
as [bac Eq]; [by apply EQD|done..| |].
+ simpl. clear -EQD. intros m stk Lt Eq.
destruct (EQD _ Lt) as [_ [stk' [Eq' ?]]]. by simplify_eq.
+ destruct kind; rewrite /retag1 Eq; by eexists.
- destruct (retag_ref_is_freeze_is_Some h α cids nxtp l otg T SharedRef
(adding_protector kind c))
as [bac Eq]; [by apply EQD|done..| |].
+ simpl. clear -EQD. intros m stk Lt Eq.
destruct (EQD _ Lt) as [_ [stk' [Eq' ?]]]. by simplify_eq.
+ destruct kind; rewrite /retag1 Eq; by eexists.
- destruct kind; [by eexists..| |by eexists].
destruct (retag_ref_is_freeze_is_Some h α cids nxtp l otg T
(RawRef (bool_decide (mut = Mutable))) None)
as [bac Eq]; [by apply EQD|done..| |rewrite /retag1 Eq; by eexists].
simpl. clear -EQD. intros m stk Lt Eq.
destruct (EQD _ Lt) as [_ [stk' [Eq' ?]]]. simplify_eq. by destruct mut.
- destruct (retag_ref_is_freeze_is_Some h α cids nxtp l otg T
(UniqueRef false) None)
as [bac Eq]; [by apply EQD|done..| |rewrite /retag1 Eq; by eexists].
simpl. clear -EQD. intros m stk Lt Eq.
destruct (EQD _ Lt) as [_ [stk' [Eq' ?]]]. by simplify_eq.
Qed.
(* We assume that :
- the place is freeze
- any memory region pointed to by any pointer in the place is also freeze
......@@ -1081,7 +1115,7 @@ Proof.
[apply sub_ref_types_O_elem_of|].
assert (l0 = l tag0 = tg) as [].
{ rewrite shift_loc_0 Eq0 in Eql0. by simplify_eq. } clear Eql0. subst l0 tag0.
destruct (retag1_is_freeze_is_Some h α nxtp cids c x rkind pkind T WF)
destruct (retag1_nested_is_freeze_is_Some h α nxtp cids c x rkind pkind T WF)
as [? Eq]; [by do 2 eexists|].
move : Eq. rewrite retag_equation_2 Eq0 /= => ->. by eexists.
- clear. intros h x n α _ cids c rk pk T Eq0 REF _ _.
......@@ -1147,40 +1181,42 @@ Proof.
+ move : Lt => /=. lia.
Abort.
Lemma retag_head_step fns σ x xbor T kind :
(* Lemma retag_head_step fns σ x xbor T kind :
σ',
head_step fns (Retag (Place x xbor T) kind ) σ [RetagEvt x T kind] #[] σ' [].
Proof.
eexists.
econstructor 2. { econstructor; eauto. }
econstructor.
Abort.
Abort. *)
Lemma retag1_head_step' fns σ x xbor pk T kind c' cids' h' α' nxtp':
Lemma retag1_head_step' fns σ l otg ntg pk T kind c' cids' α' nxtp':
σ.(scs) = c' :: cids'
retag σ.(shp) σ.(sst) σ.(snp) σ.(scs) c' x kind (Reference pk T) = Some (h', α', nxtp')
let σ' := mkState h' α' σ.(scs) nxtp' σ.(snc) in
head_step fns (Retag (Place x xbor (Reference pk T)) kind) σ
[RetagEvt x (Reference pk T) kind] #[] σ' [].
retag1 σ.(shp) σ.(sst) σ.(snp) σ.(scs) c' l otg kind pk T =
Some (ntg, α', nxtp')
let σ' := mkState σ.(shp) α' σ.(scs) nxtp' σ.(snc) in
head_step fns (Retag #[ScPtr l otg] pk T kind) σ
[RetagEvt l otg ntg pk T kind] #[ScPtr l ntg] σ' [].
Proof.
econstructor. { econstructor; eauto. } simpl.
econstructor; eauto.
Qed.
Lemma retag1_head_step fns σ x xbor pk T kind
Lemma retag1_head_step fns σ l otg pk T kind
(BAR: c, c σ.(scs))
(LOC: valid_location σ.(shp) σ.(sst) σ.(scs) x pk T)
(LOC: valid_block σ.(shp) σ.(sst) σ.(scs) l otg pk T)
(WF: Wf σ) :
c' cids' h' α' nxtp',
c' cids' ntg α' nxtp',
σ.(scs) = c' :: cids'
retag σ.(shp) σ.(sst) σ.(snp) σ.(scs) c' x kind (Reference pk T) = Some (h', α', nxtp')
let σ' := mkState h' α' σ.(scs) nxtp' σ.(snc) in
head_step fns (Retag (Place x xbor (Reference pk T)) kind) σ
[RetagEvt x (Reference pk T) kind] #[] σ' [].
retag1 σ.(shp) σ.(sst) σ.(snp) σ.(scs) c' l otg kind pk T =
Some (ntg, α', nxtp')
let σ' := mkState σ.(shp) α' σ.(scs) nxtp' σ.(snc) in
head_step fns (Retag #[ScPtr l otg] pk T kind) σ
[RetagEvt l otg ntg pk T kind] #[ScPtr l ntg] σ' [].
Proof.
destruct σ as [h α cids nxtp nxtc]; simpl in *.
destruct cids as [|c cids']; [exfalso; move : BAR => [?]; apply not_elem_of_nil|].
destruct (retag1_is_freeze_is_Some h α nxtp (c::cids') c x kind pk T) as [[[h' α'] nxtp'] Eq];
destruct (retag1_is_freeze_is_Some h α nxtp (c::cids') c l otg kind pk T) as [[[h' α'] nxtp'] Eq];
[apply WF|by destruct kind..|done|].
exists c, cids', h', α' , nxtp'. do 2 (split; [done|]).
eapply retag1_head_step'; eauto.
......
......@@ -25,11 +25,11 @@ Lemma wf_mem_tag_mono h :
Proof. move => ??? WF ??? /WF /=. lia. Qed.
(** Alloc *)
Lemma alloc_step_wf (σ σ': state) e e' h0 l bor T:
mem_expr_step σ.(shp) e (AllocEvt l bor T) h0 e'
bor_step h0 σ.(sst) σ.(scs) σ.(snp) σ.(snc)
Lemma alloc_step_wf (σ σ': state) e e' l bor T:
mem_expr_step σ.(shp) e (AllocEvt l bor T) σ'.(shp) e'
bor_step σ'.(shp) σ.(sst) σ.(scs) σ.(snp) σ.(snc)
(AllocEvt l bor T)
σ'.(shp) σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
Wf σ Wf σ'.
Proof.
destruct σ as [h α cids nxtp nxtc].
......@@ -58,17 +58,14 @@ Proof.
by apply (state_wf_non_empty _ WF _ _ Eq).
+ apply WF.
+ apply WF.
(* + intros ??. rewrite init_stacks_foldr.
intros [->|Eq]%foldr_gmap_insert_lookup; [by apply NoDup_singleton|].
by apply (state_wf_no_dup _ WF _ _ Eq). *)
Qed.
(** Dealloc *)
Lemma dealloc_step_wf σ σ' e e' h0 l bor T :
mem_expr_step σ.(shp) e (DeallocEvt l bor T) h0 e'
bor_step h0 σ.(sst) σ.(scs) σ.(snp) σ.(snc)
Lemma dealloc_step_wf σ σ' e e' l bor T :
mem_expr_step σ.(shp) e (DeallocEvt l bor T) σ'.(shp) e'
bor_step σ'.(shp) σ.(sst) σ.(scs) σ.(snp) σ.(snc)
(DeallocEvt l bor T)
σ'.(shp) σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
Wf σ Wf σ'.
Proof.
destruct σ as [h α cids nxtp nxtc].
......@@ -88,16 +85,14 @@ Proof.
apply (state_wf_non_empty _ WF _ _ Eq).
- apply WF.
- apply WF.
(* - intros ?? Eq%foldr_gmap_delete_lookup.
apply (state_wf_no_dup _ WF _ _ Eq). *)
Qed.
(** Copy *)
Lemma copy_step_wf σ σ' e e' h0 l bor T vl :
mem_expr_step σ.(shp) e (CopyEvt l bor T vl) h0 e'
bor_step h0 σ.(sst) σ.(scs) σ.(snp) σ.(snc)
Lemma copy_step_wf σ σ' e e' l bor T vl :
mem_expr_step σ.(shp) e (CopyEvt l bor T vl) σ'.(shp) e'
bor_step σ'.(shp) σ.(sst) σ.(scs) σ.(snp) σ.(snc)
(CopyEvt l bor T vl)
σ'.(shp) σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
Wf σ Wf σ' vl <<t σ'.(snp).
Proof.
destruct σ as [h α cids nxtp nxtc].
......@@ -173,11 +168,11 @@ Proof.
split; [done|]. by apply EQ2.
Qed.
Lemma write_step_wf σ σ' e e' h0 l bor T vl :
mem_expr_step σ.(shp) e (WriteEvt l bor T vl) h0 e'
bor_step h0 σ.(sst) σ.(scs) σ.(snp) σ.(snc)
Lemma write_step_wf σ σ' e e' l bor T vl :
mem_expr_step σ.(shp) e (WriteEvt l bor T vl) σ'.(shp) e'
bor_step σ'.(shp) σ.(sst) σ.(scs) σ.(snp) σ.(snc)
(WriteEvt l bor T vl)
σ'.(shp) σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
Wf σ Wf σ'.
Proof.
destruct σ as [h α cids nxtp nxtc].
......@@ -208,11 +203,11 @@ Proof.
Qed.
(** Call *)
Lemma initcall_step_wf σ σ' e e' h0 n :
mem_expr_step σ.(shp) e (InitCallEvt n) h0 e'
bor_step h0 σ.(sst) σ.(scs) σ.(snp) σ.(snc)
Lemma initcall_step_wf σ σ' e e' n :
mem_expr_step σ.(shp) e (InitCallEvt n) σ'.(shp) e'
bor_step σ'.(shp) σ.(sst) σ.(scs) σ.(snp) σ.(snc)
(InitCallEvt n)
σ'.(shp) σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
Wf σ Wf σ'.
Proof.
destruct σ as [h α cids nxtp nxtc].
......@@ -234,11 +229,11 @@ Proof.
Qed.
(** EndCall *)
Lemma endcall_step_wf σ σ' e e' h0 n v :
mem_expr_step σ.(shp) e (EndCallEvt n v) h0 e'
bor_step h0 σ.(sst) σ.(scs) σ.(snp) σ.(snc)
Lemma endcall_step_wf σ σ' e e' n v :
mem_expr_step σ.(shp) e (EndCallEvt n v) σ'.(shp) e'
bor_step σ'.(shp) σ.(sst) σ.(scs) σ.(snp) σ.(snc)
(EndCallEvt n v)
σ'.(shp) σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
Wf σ Wf σ'.
Proof.
destruct σ as [h α cids nxtp nxtc].
......@@ -889,6 +884,30 @@ Proof.
* intros ???????. by eapply reborrowN_wf_stack.
Qed.
Lemma retag1_ref_wf_stack h α nxtc cids nxtp l old T kind bar bor' α' nxtp'
(BAR : match bar with Some c => (c < nxtc)%nat | _ => True end) :
retag_ref h α cids nxtp l old T kind bar = Some (bor', α', nxtp')
wf_mem_tag h nxtp
wf_stack_item α nxtp nxtc wf_non_empty α
wf_mem_tag h nxtp'
dom (gset loc) α dom (gset loc) α'
wf_stack_item α' nxtp' nxtc wf_non_empty α'.
Proof.
intros RE WF1 WF2 WF3. split.
{ move => x' l' t' /WF1. apply retag_ref_nxtp_mono in RE. lia. }
revert RE WF2 WF3.
rewrite /retag_ref. case tsize eqn:Eq; [by intros; simplify_eq|].
case reborrow as [α1|] eqn:Eq1; [simpl|done].
intros ?. simplify_eq. intros WF2 WF3.
eapply reborrow_wf_stack; eauto; [..|].
- destruct kind; simpl; [lia..|done].
- rewrite /tag_fresh. destruct kind; [..|done];
intros i stk Lt Eqst it IN;
destruct (proj1 (WF2 _ _ Eqst) _ IN);
destruct it.(tg); auto; intros ?; simplify_eq; lia.
- split; [|done]. eapply wf_stack_item_mono; [..|done|exact WF2]. by lia.
Qed.
Lemma retag_ref_wf_stack h α nxtc cids nxtp x l old T kind bar bor' α' nxtp'
(BAR : match bar with Some c => (c < nxtc)%nat | _ => True end)
(Eqx: h !! x = Some (ScPtr l old)) :
......@@ -902,30 +921,19 @@ Lemma retag_ref_wf_stack h α nxtc cids nxtp x l old T kind bar bor' α' nxtp'
Proof.
intros RE WF1 WF2 WF3. split; last split.
{ symmetry; apply dom_map_insert_is_Some; by eexists. }
{ intros x' l' t'. case (decide (x' = x)) => ?; [subst x'|].
{ intros x' l' t'. case (decide (x' = x)) => ?; [subst x'|].
- rewrite lookup_insert => ?. simplify_eq.
move : RE => /retag_ref_nxtp_bor_mono LT. apply LT.
destruct old; [by eapply WF1|done].
- rewrite lookup_insert_ne; [|done].
move => /WF1. apply (tag_value_included_trans (Tagged t')).
by eapply retag_ref_nxtp_mono. }
move : RE WF2 WF3.
rewrite /retag_ref. case tsize eqn:Eq; [by intros; simplify_eq|].
case reborrow as [α1|] eqn:Eq1; [simpl|done].
intros ?. simplify_eq. intros WF2 WF3.
eapply reborrow_wf_stack; eauto; [..|].
- destruct kind; simpl; [lia..|done].
- rewrite /tag_fresh. destruct kind; [..|done];
intros i stk Lt Eqst it IN;
destruct (proj1 (WF2 _ _ Eqst) _ IN);
destruct it.(tg); auto; intros ?; simplify_eq; lia.
- split; [|done]. eapply wf_stack_item_mono; [..|done|exact WF2]. by lia.
eapply retag1_ref_wf_stack; eauto.
Qed.
Definition borrow_barrier_Some nxtc kind c : Prop :=
match kind with FnEntry => (c < nxtc)%nat | _ => True end.
Lemma retag_wf_stack h α nxtp nxtc cids c l kind T h' α' nxtp' :
let Hα h h' α α' nxtp nxtp' cids c kind :=
(borrow_barrier_Some nxtc kind c
......@@ -994,11 +1002,30 @@ Proof.
by rewrite -Eq1 -Eq2; apply WF.
Qed.
Lemma retag_step_wf σ σ' e e' h0 l T kind :
mem_expr_step σ.(shp) e (RetagEvt l T kind) h0 e'
bor_step h0 σ.(sst) σ.(scs) σ.(snp) σ.(snc)
(RetagEvt l T kind)
σ'.(shp) σ'.(sst) σ'.(scs) σ'.(snp) σ'.(snc)
Lemma retag1_wf h α nxtp nxtc c cids l otag rkind pk T ntag α' nxtp' :
retag1 h α nxtp (c::cids) c l otag rkind pk T = Some (ntag, α', nxtp')
Wf (mkState h α (c::cids) nxtp nxtc) Wf (mkState h α' (c::cids) nxtp' nxtc).
Proof.
intros RT WF.
have ?: borrow_barrier_Some nxtc rkind c.
{ destruct rkind; [|done..]. apply WF. by left. }
revert RT.
destruct pk as [[]|[]|