Commit f6a84ee7 authored by Hai Dang's avatar Hai Dang

rule for Free

parent d881c0ba
...@@ -159,6 +159,72 @@ Proof. ...@@ -159,6 +159,72 @@ Proof.
+ move => ??. apply Lt. lia. + move => ??. apply Lt. lia.
Qed. Qed.
Lemma for_each_dealloc_lookup_Some α l n f α' :
for_each α l n true f = Some α'
l' stk', α' !! l' = Some stk'
( i : nat, (i < n)%nat l' l + i) α !! l' = Some stk'.
Proof.
intros EQ. destruct (for_each_dealloc_lookup _ _ _ _ _ EQ) as [EQ1 EQ2].
intros l1 stk1 Eq1.
destruct (block_case l l1 n) as [NEql|Eql].
- rewrite -EQ2 //.
- destruct Eql as (i & Lt & ?). subst l1. destruct Lt.
move : (EQ1 (Z.to_nat i)). rewrite Z2Nat.id //. intros EQ'.
rewrite EQ' // in Eq1.
rewrite -(Nat2Z.id n) -Z2Nat.inj_lt //. lia.
Qed.
Lemma free_mem_lookup l n h :
( (i: nat), (i < n)%nat free_mem l n h !! (l + i) = None)
( (l': loc), ( (i: nat), (i < n)%nat l' l + i)
free_mem l n h !! l' = h !! l').
Proof.
revert l. induction n as [|n IH]; intros l; simpl.
{ split; intros ??; by [lia|]. } split.
- intros i Lt. destruct i.
+ rewrite shift_loc_0 lookup_delete //.
+ rewrite lookup_delete_ne.
* specialize (IH (l + 1))as [IH _].
rewrite (_: l + S i = l + 1 + i).
{ apply IH. lia. }
{ rewrite shift_loc_assoc. f_equal. lia. }
* rewrite -{1}(shift_loc_0 l).
move => /shift_loc_inj ?. lia.
- intros l' Lt.
rewrite lookup_delete_ne.
+ apply IH. intros i Lti.
rewrite (_: l + 1 + i = l + S i).
* apply Lt. lia.
* rewrite shift_loc_assoc. f_equal. lia.
+ rewrite -(shift_loc_0_nat l). intros ?. subst l'. apply (Lt O); [lia|done].
Qed.
Lemma free_mem_lookup_case l' l n h :
( i : nat, (i < n)%nat l' l + i) free_mem l n h !! l' = h !! l'
i, (0 i < n) l' = l + i free_mem l n h !! (l + i) = None.
Proof.
destruct (free_mem_lookup l n h) as [EQ1 EQ2].
destruct (block_case l l' n) as [NEql|Eql].
- left. rewrite -EQ2 //.
- right. destruct Eql as (i & Lt & ?). exists i. do 2 (split; [done|]).
subst l'. destruct Lt.
move : (EQ1 (Z.to_nat i)). rewrite Z2Nat.id //. intros EQ'.
apply EQ'.
rewrite -(Nat2Z.id n) -Z2Nat.inj_lt //. lia.
Qed.
Lemma free_mem_dom l' l n h:
l' dom (gset loc) (free_mem l n h)
l' dom (gset loc) h
( i : nat, (i < n)%nat l' l + i) free_mem l n h !! l' = h !! l'.
Proof.
intros [? EqD]%elem_of_dom.
destruct (free_mem_lookup_case l' l n h) as [Eqn|(i & Lt & ? & EqN)].
- split; [|done]. apply elem_of_dom. destruct Eqn as [? Eqn].
rewrite -Eqn. by eexists.
- exfalso. subst l'. by rewrite EqD in EqN.
Qed.
Lemma memory_deallocated_delete' α nxtc l bor n α' (m: nat): Lemma memory_deallocated_delete' α nxtc l bor n α' (m: nat):
memory_deallocated α nxtc (l + m) bor n = Some α' memory_deallocated α nxtc (l + m) bor n = Some α'
α' = fold_right (λ (i: nat) α, delete (l + i) α) α (seq m n). α' = fold_right (λ (i: nat) α, delete (l + i) α) α (seq m n).
...@@ -178,3 +244,27 @@ Lemma memory_deallocated_delete α nxtc l bor n α': ...@@ -178,3 +244,27 @@ Lemma memory_deallocated_delete α nxtc l bor n α':
memory_deallocated α nxtc l bor n = Some α' memory_deallocated α nxtc l bor n = Some α'
α' = fold_right (λ (i: nat) α, delete (l + i) α) α (seq O n). α' = fold_right (λ (i: nat) α, delete (l + i) α) α (seq O n).
Proof. intros. eapply memory_deallocated_delete'. rewrite shift_loc_0. by eauto. Qed. Proof. intros. eapply memory_deallocated_delete'. rewrite shift_loc_0. by eauto. Qed.
Lemma dealloc1_Some stk t cids :
is_Some (dealloc1 stk t cids)
it, it stk it.(tg) = t
Forall (λ x : item, ¬ is_active_protector cids x) stk
grants it.(perm) AccessWrite.
Proof.
rewrite /dealloc1. move => [[]].
case find_granting eqn:GR; [|done]. simpl.
apply fmap_Some_1 in GR as [[i it'] [[GR [? ?]]%list_find_Some ?]]. simplify_eq.
rewrite /find_top_active_protector.
case list_find eqn:EqF; [done|]. intros _.
apply list_find_None in EqF. exists it'.
have ?: it' stk by eapply elem_of_list_lookup_2. done.
Qed.
Lemma dealloc1_singleton_Some it t cids:
is_Some (dealloc1 [it] t cids)
it.(tg) = t (¬ is_active_protector cids it) grants it.(perm) AccessWrite.
Proof.
move => /dealloc1_Some [it' [/elem_of_list_singleton In' [? [FA ?]]]].
subst. split; last split; [done| |done].
rewrite ->Forall_forall in FA. apply FA. by left.
Qed.
...@@ -86,6 +86,21 @@ Proof. ...@@ -86,6 +86,21 @@ Proof.
+ move => ??. apply Lt. lia. + move => ??. apply Lt. lia.
Qed. Qed.
Lemma block_case l l' n :
( i : nat, (i < n)%nat l' l + i)
i, (0 i < n) l' = l + i.
Proof.
case (decide (l'.1 = l.1)) => [Eql|NEql];
[case (decide (l.2 l'.2 < l.2 + n)) => [[Le Lt]|NIN]|].
- have Eql2: l' = l + Z.of_nat (Z.to_nat (l'.2 - l.2)). {
destruct l, l'. move : Eql Le => /= -> ?.
rewrite /shift_loc /= Z2Nat.id; [|lia]. f_equal. lia. }
right. rewrite Eql2. rewrite Eql2 /= in Lt.
eexists. split; [|done]. lia.
- left. intros i Lt Eq3. apply NIN. rewrite Eq3 /=. lia.
- left. intros i Lt Eq3. apply NEql. by rewrite Eq3.
Qed.
Lemma for_each_lookup_case α l n f α' : Lemma for_each_lookup_case α l n f α' :
for_each α l n false f = Some α' for_each α l n false f = Some α'
l' stk stk', α !! l' = Some stk α' !! l' = Some stk' l' stk stk', α !! l' = Some stk α' !! l' = Some stk'
...@@ -93,20 +108,15 @@ Lemma for_each_lookup_case α l n f α' : ...@@ -93,20 +108,15 @@ Lemma for_each_lookup_case α l n f α' :
Proof. Proof.
intros EQ. destruct (for_each_lookup _ _ _ _ _ EQ) as [EQ1 [EQ2 EQ3]]. intros EQ. destruct (for_each_lookup _ _ _ _ _ EQ) as [EQ1 [EQ2 EQ3]].
intros l1 stk stk' Eq Eq'. intros l1 stk stk' Eq Eq'.
case (decide (l1.1 = l.1)) => [Eql|NEql]; destruct (block_case l l1 n) as [NEql|Eql].
[case (decide (l.2 l1.2 < l.2 + n)) => [[Le Lt]|NIN]|].
- have Eql2: l1 = l + Z.of_nat (Z.to_nat (l1.2 - l.2)). {
destruct l, l1. move : Eql Le => /= -> ?.
rewrite /shift_loc /= Z2Nat.id; [|lia]. f_equal. lia. }
destruct (EQ2 (Z.to_nat (l1.2 - l.2)) stk') as [stk1 [Eq1 Eq2]];
[rewrite -(Nat2Z.id n) -Z2Nat.inj_lt; lia|by rewrite -Eql2 |].
rewrite -Eql2 in Eq1. simplify_eq. right. split; [done|].
exists (Z.to_nat (l1.2 - l.2)). rewrite -Eql2. split; [|done].
rewrite Z2Nat.id; lia.
- left. rewrite EQ3 in Eq'; [by simplify_eq|].
intros i Lt Eq3. apply NIN. rewrite Eq3 /=. lia.
- left. rewrite EQ3 in Eq'; [by simplify_eq|]. - left. rewrite EQ3 in Eq'; [by simplify_eq|].
intros i Lt Eq3. apply NEql. by rewrite Eq3. intros i Lt Eq3. by apply (NEql i).
- right. split; [|done].
destruct Eql as (i & [] & Eql). subst l1.
destruct (EQ2 (Z.to_nat i) stk') as [stk1 [Eq1 Eq2]].
+ rewrite -(Nat2Z.id n) -Z2Nat.inj_lt; lia.
+ rewrite Z2Nat.id //.
+ rewrite Z2Nat.id // Eq in Eq1. by simplify_eq.
Qed. Qed.
Lemma for_each_lookup_case_2 α l n f α' : Lemma for_each_lookup_case_2 α l n f α' :
...@@ -132,6 +142,29 @@ Proof. ...@@ -132,6 +142,29 @@ Proof.
+ move => ??. apply Lt. lia. + move => ??. apply Lt. lia.
Qed. Qed.
Lemma for_each_true_lookup_case_2 α l n f α' :
for_each α l n true f = Some α'
( (i: nat), (i < n)%nat stk stk',
α !! (l + i) = Some stk α' !! (l + i) = None f stk = Some stk' )
( (l': loc), ( (i: nat), (i < n)%nat l' l + i) α' !! l' = α !! l').
Proof.
revert α. induction n as [|n IH]; intros α; simpl.
{ move => [<-]. split; intros ??; [lia|done]. }
case (α !! (l + n)) as [stkn|] eqn:Eqn; [|done] => /=.
case (f stkn) as [stkn'|] eqn: Eqn'; [|done] => /= /IH [IH1 IH2].
split.
- intros i Lt.
case (decide (i = n)) => Eq'; [subst i|].
+ rewrite Eqn. rewrite IH2; [rewrite lookup_delete; naive_solver|].
move => ?? /shift_loc_inj /Z_of_nat_inj ?. by lia.
+ destruct (IH1 i) as (stk & stk' & Eqs & ?); [lia|].
rewrite lookup_delete_ne in Eqs; [naive_solver|].
by move => /shift_loc_inj /Z_of_nat_inj ? //.
- intros l' Lt. rewrite IH2.
+ rewrite lookup_delete_ne; [done|]. move => Eql'. apply (Lt n); by [lia|].
+ move => ??. apply Lt. lia.
Qed.
Lemma init_mem_lookup l n h : Lemma init_mem_lookup l n h :
( (i: nat), (i < n)%nat init_mem l n h !! (l + i) = Some %S) ( (i: nat), (i < n)%nat init_mem l n h !! (l + i) = Some %S)
( (l': loc), ( (i: nat), (i < n)%nat l' l + i) ( (l': loc), ( (i: nat), (i < n)%nat l' l + i)
...@@ -164,21 +197,9 @@ Lemma init_mem_lookup_case l n h : ...@@ -164,21 +197,9 @@ Lemma init_mem_lookup_case l n h :
Proof. Proof.
destruct (init_mem_lookup l n h) as [EQ1 EQ2]. destruct (init_mem_lookup l n h) as [EQ1 EQ2].
intros l1 s1 Eq'. intros l1 s1 Eq'.
case (decide (l1.1 = l.1)) => [Eql|NEql]; destruct (block_case l l1 n) as [NEql|Eql].
[case (decide (l.2 l1.2 < l.2 + n)) => [[Le Lt]|NIN]|]. - left. rewrite EQ2 // in Eq'.
- have Eql2: l1 = l + Z.of_nat (Z.to_nat (l1.2 - l.2)). { - by right.
destruct l, l1. move : Eql Le => /= -> ?.
rewrite /shift_loc /= Z2Nat.id; [|lia]. f_equal. lia. }
right. rewrite Eql2. eexists; split; [|done].
rewrite Eql2 /= in Lt. lia.
- left.
have ?: i : nat, (i < n)%nat l1 l + i.
{ intros i Lt Eq3. apply NIN. rewrite Eq3 /=. lia. }
rewrite EQ2 // in Eq'.
- left.
have ?: i : nat, (i < n)%nat l1 l + i.
{ intros i Lt Eq3. apply NEql. by rewrite Eq3. }
rewrite EQ2 // in Eq'.
Qed. Qed.
Lemma init_mem_lookup_empty l n : Lemma init_mem_lookup_empty l n :
...@@ -219,21 +240,9 @@ Lemma init_stacks_lookup_case α l n t : ...@@ -219,21 +240,9 @@ Lemma init_stacks_lookup_case α l n t :
Proof. Proof.
destruct (init_stacks_lookup α l n t) as [EQ1 EQ2]. destruct (init_stacks_lookup α l n t) as [EQ1 EQ2].
intros l1 s1 Eq'. intros l1 s1 Eq'.
case (decide (l1.1 = l.1)) => [Eql|NEql]; destruct (block_case l l1 n) as [NEql|Eql].
[case (decide (l.2 l1.2 < l.2 + n)) => [[Le Lt]|NIN]|]. - left. rewrite EQ2 // in Eq'.
- have Eql2: l1 = l + Z.of_nat (Z.to_nat (l1.2 - l.2)). { - by right.
destruct l, l1. move : Eql Le => /= -> ?.
rewrite /shift_loc /= Z2Nat.id; [|lia]. f_equal. lia. }
right. rewrite Eql2. eexists; split; [|done].
rewrite Eql2 /= in Lt. lia.
- left.
have ?: i : nat, (i < n)%nat l1 l + i.
{ intros i Lt Eq3. apply NIN. rewrite Eq3 /=. lia. }
rewrite EQ2 // in Eq'.
- left.
have ?: i : nat, (i < n)%nat l1 l + i.
{ intros i Lt Eq3. apply NEql. by rewrite Eq3. }
rewrite EQ2 // in Eq'.
Qed. Qed.
Lemma init_stacks_lookup_case_2 α l n t : Lemma init_stacks_lookup_case_2 α l n t :
...@@ -244,23 +253,12 @@ Lemma init_stacks_lookup_case_2 α l n t : ...@@ -244,23 +253,12 @@ Lemma init_stacks_lookup_case_2 α l n t :
Proof. Proof.
destruct (init_stacks_lookup α l n t) as [EQ1 EQ2]. destruct (init_stacks_lookup α l n t) as [EQ1 EQ2].
intros l1 s1 Eq'. intros l1 s1 Eq'.
case (decide (l1.1 = l.1)) => [Eql|NEql]; destruct (block_case l l1 n) as [NEql|Eql].
[case (decide (l.2 l1.2 < l.2 + n)) => [[Le Lt]|NIN]|]. - left. rewrite EQ2 //.
- have Eql2: l1 = l + Z.of_nat (Z.to_nat (l1.2 - l.2)). { - right. destruct Eql as (i & Lt & ?).
destruct l, l1. move : Eql Le => /= -> ?. exists i. do 2 (split; [done|]). subst l1. destruct Lt.
rewrite /shift_loc /= Z2Nat.id; [|lia]. f_equal. lia. } move : (EQ1 (Z.to_nat i)). rewrite Z2Nat.id //. intros EQ'. apply EQ'.
right. rewrite Eql2. rewrite Eql2 /= in Lt. rewrite -(Nat2Z.id n). by apply Z2Nat.inj_lt; lia.
eexists; split; last split; [|done|].
+ lia.
+ rewrite EQ1 //. lia.
- left.
have ?: i : nat, (i < n)%nat l1 l + i.
{ intros i Lt Eq3. apply NIN. rewrite Eq3 /=. lia. }
rewrite EQ2 //.
- left.
have ?: i : nat, (i < n)%nat l1 l + i.
{ intros i Lt Eq3. apply NEql. by rewrite Eq3. }
rewrite EQ2 //.
Qed. Qed.
Lemma for_each_dom α l n f α' : Lemma for_each_dom α l n f α' :
......
...@@ -726,6 +726,39 @@ Proof. ...@@ -726,6 +726,39 @@ Proof.
inversion STT as [?? STT2|?[]? STT2]; by apply result_tstep_stuck in STT2. inversion STT as [?? STT2|?[]? STT2]; by apply result_tstep_stuck in STT2.
Qed. Qed.
(** Free *)
Lemma fill_free_decompose K e e':
fill K e = Free e'
K = [] e = Free e' ( K', K = K' ++ [FreeCtx] fill K' e = e').
Proof.
revert e e'.
induction K as [|Ki K IH]; [by left|]. simpl.
intros e e' EqK. right.
destruct (IH _ _ EqK) as [[? _]|[K0 [? Eq0]]].
- subst. simpl in *. destruct Ki; try done.
simpl in EqK. simplify_eq. exists []. naive_solver.
- subst K. by exists (Ki :: K0).
Qed.
Lemma tstep_free_inv (pl: result) e' σ σ'
(STEP: (Free pl, σ) ~{fns}~> (e', σ')) :
l tg T α',
pl = PlaceR l tg T
e' = #[%S]%E
( m, is_Some (σ.(shp) !! (l + m)) 0 m < tsize T)
memory_deallocated σ.(sst) σ.(scs) l tg (tsize T) = Some α'
σ' = mkState (free_mem l (tsize T) σ.(shp)) α' σ.(scs) σ.(snp) σ.(snc).
Proof.
inv_tstep. symmetry in Eq.
destruct (fill_free_decompose _ _ _ Eq) as [[]|[K' [? Eq']]]; subst.
- clear Eq. simpl in HS. inv_head_step.
have Eq1 := to_of_result pl. rewrite -H /to_result in Eq1. simplify_eq.
naive_solver.
- exfalso. apply val_head_stuck in HS. destruct (fill_val K' e1') as [? Eq1'].
+ rewrite /= Eq' to_of_result. by eexists.
+ by rewrite Eq1' in HS.
Qed.
(** Copy *) (** Copy *)
Lemma fill_copy_decompose K e e': Lemma fill_copy_decompose K e e':
fill K e = Copy e' fill K e = Copy e'
......
...@@ -79,6 +79,16 @@ Proof. ...@@ -79,6 +79,16 @@ Proof.
case protector; naive_solver. case protector; naive_solver.
Qed. Qed.
Lemma dealloc_head_step' fns (σ: state) l bor T α (WF: Wf σ) :
( m : Z, is_Some (σ.(shp) !! (l + m)) 0 m m < tsize T)
memory_deallocated σ.(sst) σ.(scs) l bor (tsize T) = Some α
let σ' := mkState (free_mem l (tsize T) σ.(shp)) α σ.(scs) σ.(snp) σ.(snc) in
head_step fns (Free (Place l bor T)) σ
[DeallocEvt l bor T] #[] σ' [].
Proof.
intros DOM MD. econstructor; econstructor; eauto.
Qed.
Lemma dealloc_head_step fns (σ: state) T l bor Lemma dealloc_head_step fns (σ: state) T l bor
(WF: Wf σ) (WF: Wf σ)
(BLK: m : Z, l + m dom (gset loc) σ.(shp) 0 m m < tsize T) (BLK: m : Z, l + m dom (gset loc) σ.(shp) 0 m m < tsize T)
......
...@@ -285,7 +285,13 @@ Proof using Type*. ...@@ -285,7 +285,13 @@ Proof using Type*.
split; first done. split; first done.
simpl. split; last done. constructor; last done. simpl. split; last done. constructor; last done.
eapply arel_mono, arel_ptr; auto. eapply arel_mono, arel_ptr; auto.
- (* Free *) admit. - (* Free *)
move=>Hwf xs Hxswf /=.
sim_bind (subst_map _ e) (subst_map _ e).
eapply sim_simple_post_mono, IHe; [|by auto..].
intros r' n' rs rt (-> & Hrel). simpl.
eapply sim_simple_dealloc; eauto.
split; first done. constructor; done.
- (* Retag *) admit. - (* Retag *) admit.
- (* Let *) - (* Let *)
move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1). move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
......
...@@ -283,6 +283,144 @@ Proof. ...@@ -283,6 +283,144 @@ Proof.
apply POST; eauto. apply POST; eauto.
Qed. Qed.
(** Free *)
Lemma sim_body_free fs ft r n (pl: result) σs σt Φ
(RREL: rrel r pl pl) :
( l t T,
pl = PlaceR l t T
( m, is_Some (σs.(shp) !! (l + m)) 0 m < tsize T)
( m, is_Some (σt.(shp) !! (l + m)) 0 m < tsize T)
α', memory_deallocated σt.(sst) σt.(scs) l t (tsize T) = Some α'
let σs' := mkState (free_mem l (tsize T) σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
let σt' := mkState (free_mem l (tsize T) σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc) in
Φ r n (ValR [%S]) σs' (ValR [%S]) σt')
r {n,fs,ft} (Free pl, σs) (Free pl, σt) : Φ.
Proof.
intros POST. pfold. intros NT. intros.
have WSAT1 := WSAT. (* backup *)
(* making a step *)
destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
split; [|done|].
{ right.
destruct (NT (Free pl) σs) as [[]|[es' [σs' STEPS]]];
[done..|].
destruct (tstep_free_inv _ _ _ _ _ STEPS)
as (l&t&T & α' & EqH & ? & Eqh & Eqα' & ?). symmetry in EqH. simplify_eq.
have Eqh' : ( m, is_Some (σt.(shp) !! (l + m)) 0 m < tsize T).
{ intros m. rewrite -(Eqh m). rewrite -2!(elem_of_dom (D:=gset loc)).
rewrite (wsat_heap_dom _ _ _ WSAT1) //. }
have Eqα'2: memory_deallocated σt.(sst) σt.(scs) l t (tsize T) = Some α'.
{ destruct SREL as (Eqst&?&Eqcs&?). by rewrite -Eqst -Eqcs. }
exists (#[%S])%E, (mkState (free_mem l (tsize T) σt.(shp)) α'
σt.(scs) σt.(snp) σt.(snc)).
by eapply (head_step_fill_tstep _ []), dealloc_head_step'. }
constructor 1. intros.
destruct (tstep_free_inv _ _ _ _ _ STEPT)
as (l&t&T& α' & EqH & ? & Eqh & Eqα' & ?). symmetry in EqH. simplify_eq.
have Eqh' : ( m, is_Some (σs.(shp) !! (l + m)) 0 m < tsize T).
{ intros m. rewrite -(Eqh m). rewrite -2!(elem_of_dom (D:=gset loc)).
rewrite (wsat_heap_dom _ _ _ WSAT1) //. }
have Eqα'2: memory_deallocated σs.(sst) σs.(scs) l t (tsize T) = Some α'.
{ destruct SREL as (Eqst&?&Eqcs&?). by rewrite Eqst Eqcs. }
set σs' := mkState (free_mem l (tsize T) σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc).
have STEPS: (Free (Place l t T), σs) ~{fs}~> ((#[%S])%E, σs').
{ by eapply (head_step_fill_tstep _ []), dealloc_head_step'. }
(* unfolding rrel for place *)
simpl in RREL. destruct RREL as [VREL _].
inversion VREL as [|???? AREL U]; subst; simplify_eq. clear U VREL.
destruct AREL as (_ & _ & AREL).
(* reestablishing WSAT *)
destruct (free_mem_lookup l (tsize T) σt.(shp)) as [Hmst1 Hmst2].
destruct (free_mem_lookup l (tsize T) σs.(shp)) as [Hmss1 Hmss2].
exists (#[%S])%E, σs', r, 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).
- done.
- intros t' k' h' Eqt'.
specialize (PINV _ _ _ Eqt') as [? PINV].
split; [done|]. intros l1 ss1 st1 Eql1.
specialize (PINV _ _ _ Eql1).
destruct k'; simpl in *.
+ specialize (PINV I) as (Eqst & Eqss & HTOP). intros _.
destruct (free_mem_lookup_case l1 l (tsize T) σt.(shp))
as [[NEql Eql]|(i & Lti & ? & Eql)].
* destruct (for_each_dealloc_lookup _ _ _ _ _ Eqα') as [_ EQ2].
rewrite Eql (Hmss2 _ NEql) (EQ2 _ NEql) //.
* subst l1. exfalso.
destruct (for_each_true_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 _].
destruct Lti as [Lei Lti].
destruct (EQ1 (Z.to_nat i)) as (stk1 & stk' & Eqstk & EqN & DA).
{ rewrite -(Nat2Z.id (tsize T)). by apply Z2Nat.inj_lt; lia. }
rewrite Z2Nat.id // in Eqstk. rewrite Eqstk in HTOP. simplify_eq.
move : DA. clear -AREL Eqt'.
destruct (dealloc1 (init_stack (Tagged t')) t σt.(scs))
eqn:Eqd; [|done]. intros _.
destruct (dealloc1_singleton_Some (mkItem Unique (Tagged t') None)
t σt.(scs)) as [Eqt _]. { by eexists. }
simpl in Eqt. subst t. move : Eqt'.
destruct AREL as [h AREL]. rewrite lookup_op AREL.
by apply tagKindR_local_exclusive_r.
+ intros (stk1 & pm & opro & Eqstk1 & ?).
destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Eqα' _ _ Eqstk1)
as [NEQ EQ].
destruct PINV as [Eqst [Eqss PO]].
{ by exists stk1, pm, opro. }
destruct PO as (stk' & Eqstk' & PO).
rewrite Eqstk' in EQ. simplify_eq. split; last split.
* by rewrite Hmst2.
* by rewrite Hmss2.
* by exists stk1.
+ intros (stk1 & pm & opro & Eqstk1 & ?).
destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Eqα' _ _ Eqstk1)
as [NEQ EQ].
destruct PINV as [Eqst [Eqss PO]].
{ by exists stk1, pm, opro. }
destruct PO as (stk' & Eqstk' & PO).
rewrite Eqstk' in EQ. simplify_eq. split; last split.
* by rewrite Hmst2.
* by rewrite Hmss2.
* by exists stk1.
- intros c Tc Eqc. specialize (CINV _ _ Eqc) as [? CINV].
split; [done|]. intros tc L InL. specialize (CINV _ _ InL) as [? CINV].
split; [done|]. intros l1 Inl1.
specialize (CINV _ Inl1). simpl.
destruct (for_each_true_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 EQ2].
(* from Eqα', l1 cannot be in l because it is protected by c,
so α' !! l1 = σt.(sst) !! l1. *)
destruct (block_case l l1 (tsize T)) as [NEql|(i & [Lei Lti] & Eql)].
+ rewrite EQ2 //.
+ exfalso. clear EQ2.
subst l1. destruct CINV as (stk & pm & Eqstk & Instk & ?).
specialize (EQ1 (Z.to_nat i)) as (stk1 & stk' & Eqstk').
{ rewrite -(Nat2Z.id (tsize T)). by apply Z2Nat.inj_lt; lia. }
rewrite Z2Nat.id // in Eqstk'.
destruct Eqstk' as (Eqstk1 & Eqstk' & DA).
rewrite Eqstk1 in Eqstk. simplify_eq.
move : DA. destruct (dealloc1 stk t σt.(scs)) eqn:Eqd; [|done].
intros _.
destruct (dealloc1_Some stk t σt.(scs)) as (it & Eqit & ? & FA & GR).
{ by eexists. }
rewrite ->Forall_forall in FA. apply (FA _ Instk).
rewrite /is_active_protector /= /is_active bool_decide_true //.
- rewrite /srel /=. destruct SREL as (?&?&?&?&PB).
do 4 (split; [done|]).
intros l1 Inl1.
destruct (for_each_true_lookup_case_2 _ _ _ _ _ Eqα') as [_ EQ2].
destruct (free_mem_dom _ _ _ _ Inl1) as (InD & NEql & EqM).
specialize (EQ2 _ NEql).
destruct (PB _ InD) as [PP|PV]; [left|by right].
intros ?. simpl. rewrite (Hmst2 _ NEql) (Hmss2 _ NEql). by apply PP. }
left.
apply: sim_body_result. intros. eapply POST; eauto.
Qed.
(** Copy *) (** Copy *)
Lemma sim_body_copy_public fs ft r n (pl: result) σs σt Φ Lemma sim_body_copy_public fs ft r n (pl: result) σs σt Φ
(RREL: rrel r pl pl) : (RREL: rrel r pl pl) :
......
...@@ -341,6 +341,14 @@ Proof. ...@@ -341,6 +341,14 @@ Proof.
intros HH σs σt. apply sim_body_alloc_public=>/=; eauto. intros HH σs σt. apply sim_body_alloc_public=>/=; eauto.
Qed. Qed.
Lemma sim_simple_dealloc fs ft r rs rt n Φ :
rrel r rs rt
Φ r n (ValR [%S]) (ValR [%S])
r ⊨ˢ{n,fs,ft} Free rs Free rt : Φ.
Proof.
intros [Hrel <-]%rrel_with_eq HH σs σt. eapply sim_body_free; eauto.
Qed.
Lemma sim_simple_write_public fs ft r n (rs1 rs2 rt1 rt2: result) Φ : Lemma sim_simple_write_public fs ft r n (rs1 rs2 rt1 rt2: result) Φ :
rrel r rs1 rt1 rrel r rs1 rt1
rrel r rs2 rt2 rrel r rs2 rt2
......
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