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

restructure steps_wf.v

parent e06cf26f
......@@ -8,9 +8,12 @@ theories/lang/expr_semantics.v
theories/lang/bor_semantics.v
theories/lang/lang.v
theories/lang/defs.v
theories/lang/steps_foreach.v
theories/lang/steps_list.v
theories/lang/steps_wf.v
theories/lang/steps_progress.v
theories/lang/steps_inversion.v
theories/lang/steps_retag.v
theories/lang/examples.v
theories/sim/behavior.v
theories/sim/global.v
......
......@@ -140,3 +140,63 @@ Proof.
apply IH. split; last split; [done..|]. intros j y Lt Eq.
apply (Lt1 (S j) y); [lia|done].
Qed.
(* TODO: move *)
Lemma list_subseteq_nil_sublist {A: Type} (x: list A):
x [] sublist x [].
Proof. destruct x; set_solver. Qed.
Lemma list_subseteq_nil_inv {A: Type} (x: list A):
x [] x = [].
Proof.
intros. apply : anti_symm.
by apply list_subseteq_nil_sublist. by apply sublist_nil_l.
Qed.
Lemma NoDup_sublist {A: Type} (x y: list A) (SUB: sublist x y) :
NoDup y NoDup x.
Proof.
induction SUB as [|???? IH|???? IH].
- done.
- move => /NoDup_cons [NI /IH ND]. apply NoDup_cons. split; [|done].
move => In1. apply NI. move : In1. by apply elem_of_list_sublist_proper.
- move => /NoDup_cons [NI /IH //].
Qed.
Instance NoDup_sublist_proper {A: Type} :
Proper (sublist ==> flip impl) (@NoDup A).
Proof. intros ????. by eapply NoDup_sublist. Qed.
Lemma filter_sublist {A: Type} (P : A Prop)
`{ x, Decision (P x)} (x y: list A) :
sublist x y sublist (filter P x) (filter P y).
Proof.
induction 1 as [|???? IH|???? IH].
- done.
- rewrite 2!filter_cons. case decide => ? //. by constructor 2.
- rewrite filter_cons. case decide => ? //. by constructor 3.
Qed.
Lemma filter_app {A: Type} (P : A Prop)
`{ x, Decision (P x)} (x y: list A) :
filter P (x ++ y) = filter P x ++ filter P y.
Proof.
induction x as [|a x IH]; [done|].
rewrite -app_comm_cons 2!filter_cons.
case decide => ? //. by rewrite -app_comm_cons IH.
Qed.
Lemma reserve_lookup {A: Type} (l: list A) (i : nat) (a: A) :
l !! i = Some a j, reverse l !! j = Some a (i + j + 1)%nat = length l.
Proof.
revert i. induction l as [|b l IH]; simpl; intros i; [naive_solver|].
rewrite reverse_cons.
destruct i.
- simpl. intros. simplify_eq. exists (length l). split; [|lia].
rewrite lookup_app_r; rewrite reverse_length //.
by rewrite Nat.sub_diag.
- simpl. intros Eqi. have Lt := lookup_lt_Some _ _ _ Eqi.
move : Eqi => /IH [j [Eqj Eql]].
exists j. rewrite Eql. split; [|done]. rewrite lookup_app_l //.
rewrite reverse_length. lia.
Qed.
From stbor.lang Require Export defs.
Set Default Proof Using "Type".
Lemma for_each_lookup α l n f α' :
for_each α l n false f = Some α'
( (i: nat) stk, (i < n)%nat α !! (l + i) = Some stk stk',
α' !! (l + i) = Some stk' f stk = Some stk' )
( (i: nat) stk', (i < n)%nat α' !! (l + i) = Some stk' stk,
α !! (l + i) = Some stk 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; last split; intros ??; [lia|lia|done]. }
case (α !! (l + n)) as [stkn|] eqn:Eqn; [|done] => /=.
case f as [stkn'|] eqn: Eqn'; [|done] => /= /IH [IH1 [IH2 IH3]].
split; last split.
- intros i stk Lt Eqi. case (decide (i = n)) => Eq'; [subst i|].
+ rewrite Eqi in Eqn. simplify_eq.
rewrite Eqn' IH3; [by rewrite lookup_insert; eexists|].
move => ?? /shift_loc_inj /Z_of_nat_inj ?. by lia.
+ apply IH1; [lia|]. rewrite lookup_insert_ne; [done|].
by move => /shift_loc_inj /Z_of_nat_inj ? //.
- intros i stk Lt Eqi. case (decide (i = n)) => Eq'; [subst i|].
+ move : Eqi. rewrite IH3.
* rewrite lookup_insert. intros. simplify_eq. naive_solver.
* move => ?? /shift_loc_inj /Z_of_nat_inj ?. by lia.
+ destruct (IH2 i stk) as [stk0 [Eq0 Eqf0]]; [lia|done|].
exists stk0. split; [|done]. move : Eq0. rewrite lookup_insert_ne; [done|].
by move => /shift_loc_inj /Z_of_nat_inj ? //.
- intros l' Lt. rewrite IH3.
+ rewrite lookup_insert_ne; [done|]. move => Eql'. apply (Lt n); by [lia|].
+ move => ??. apply Lt. lia.
Qed.
Lemma for_each_lookup_case α l n f α' :
for_each α l n false f = Some α'
l' stk stk', α !! l' = Some stk α' !! l' = Some stk'
stk = stk' f stk = Some stk' i, (0 i < n) l' = l + i.
Proof.
intros EQ. destruct (for_each_lookup _ _ _ _ _ EQ) as [EQ1 [EQ2 EQ3]].
intros l1 stk stk' Eq Eq'.
case (decide (l1.1 = l.1)) => [Eql|NEql];
[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|].
intros i Lt Eq3. apply NEql. by rewrite Eq3.
Qed.
Lemma init_mem_lookup l n h :
( (i: nat), (i < n)%nat init_mem l n h !! (l + i) = Some %S)
( (l': loc), ( (i: nat), (i < n)%nat l' l + i)
init_mem l n h !! l' = h !! l').
Proof.
revert l h. induction n as [|n IH]; intros l h; simpl.
{ split; intros ??; [lia|done]. }
destruct (IH (l + 1) h) as [IH1 IH2].
split.
- intros i Lt. destruct i as [|i].
+ rewrite shift_loc_0_nat lookup_insert //.
+ have Eql: l + S i = (l + 1) + i.
{ rewrite shift_loc_assoc. f_equal. lia. }
rewrite lookup_insert_ne.
* rewrite Eql. destruct (IH (l + 1) h) as [IH' _].
apply IH'; lia.
* rewrite -{1}(shift_loc_0_nat l). intros ?%shift_loc_inj. lia.
- intros l' Lt. rewrite lookup_insert_ne.
+ apply IH2. intros i Lt'.
rewrite (_: (l + 1) + i = l + S i); last first.
{ rewrite shift_loc_assoc. f_equal. lia. }
apply Lt. lia.
+ specialize (Lt O ltac:(lia)). by rewrite shift_loc_0_nat in Lt.
Qed.
Lemma init_mem_lookup_case l n h :
l' s', init_mem l n h !! l' = Some s'
h !! l' = Some s' ( i : nat, (i < n)%nat l' l + i)
i, (0 i < n) l' = l + i.
Proof.
destruct (init_mem_lookup l n h) as [EQ1 EQ2].
intros l1 s1 Eq'.
case (decide (l1.1 = l.1)) => [Eql|NEql];
[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. }
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.
Lemma init_mem_lookup_empty l n :
l' s', init_mem l n !! l' = Some s'
i, (0 i < n) l' = l + i.
Proof. move => l' s' /init_mem_lookup_case [[//]|//]. Qed.
Lemma init_stacks_lookup α l n t :
( (i: nat), (i < n)%nat
init_stacks α l n t !! (l + i) = Some [mkItem Unique t None])
( (l': loc), ( (i: nat), (i < n)%nat l' l + i)
init_stacks α l n t !! l' = α !! l').
Proof.
revert l α. induction n as [|n IH]; intros l α; simpl.
{ split; intros ??; [lia|done]. }
destruct (IH (l + 1) α) as [IH1 IH2].
split.
- intros i Lt. destruct i as [|i].
+ rewrite shift_loc_0_nat lookup_insert //.
+ have Eql: l + S i = (l + 1) + i.
{ rewrite shift_loc_assoc. f_equal. lia. }
rewrite lookup_insert_ne.
* rewrite Eql. destruct (IH (l + 1) α) as [IH' _].
apply IH'; lia.
* rewrite -{1}(shift_loc_0_nat l). intros ?%shift_loc_inj. lia.
- intros l' Lt. rewrite lookup_insert_ne.
+ apply IH2. intros i Lt'.
rewrite (_: (l + 1) + i = l + S i); last first.
{ rewrite shift_loc_assoc. f_equal. lia. }
apply Lt. lia.
+ specialize (Lt O ltac:(lia)). by rewrite shift_loc_0_nat in Lt.
Qed.
Lemma init_stacks_lookup_case α l n t :
l' s', init_stacks α l n t !! l' = Some s'
α !! l' = Some s' ( i : nat, (i < n)%nat l' l + i)
i, (0 i < n) l' = l + i.
Proof.
destruct (init_stacks_lookup α l n t) as [EQ1 EQ2].
intros l1 s1 Eq'.
case (decide (l1.1 = l.1)) => [Eql|NEql];
[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. }
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.
Lemma init_stacks_lookup_case_2 α l n t :
l' s', α !! l' = Some s'
init_stacks α l n t !! l' = Some s' ( i : nat, (i < n)%nat l' l + i)
i, (0 i < n) l' = l + i
init_stacks α l n t !! l' = Some [mkItem Unique t None].
Proof.
destruct (init_stacks_lookup α l n t) as [EQ1 EQ2].
intros l1 s1 Eq'.
case (decide (l1.1 = l.1)) => [Eql|NEql];
[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. }
right. rewrite Eql2. rewrite Eql2 /= in Lt.
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.
Lemma for_each_dom α l n f α' :
for_each α l n false f = Some α'
dom (gset loc) α dom (gset loc) α'.
Proof.
revert α. induction n as [|n IH]; intros α; [by move => /= [-> //]|].
simpl. destruct (α !! (l + n)) eqn:Eq; [|done].
simpl. case f => stack' /=; [|done]. move => /IH <-.
symmetry. apply dom_map_insert_is_Some. rewrite Eq. by eexists.
Qed.
From stbor.lang Require Export defs.
Set Default Proof Using "Type".
Definition tagged_sublist (stk1 stk2: stack) :=
it1, it1 stk1 it2,
it2 stk2 it1.(tg) = it2.(tg) it1.(protector) = it2.(protector)
(it1.(perm) Disabled it2.(perm) = it1.(perm)).
Instance tagged_sublist_preorder : PreOrder tagged_sublist.
Proof.
constructor.
- intros ??. naive_solver.
- move => ??? H1 H2 ? /H1 [? [/H2 Eq [-> [-> ND]]]].
destruct Eq as (it2 &?&?&?&ND2). exists it2. repeat split; auto.
intros ND3. specialize (ND ND3). rewrite ND2 // ND //.
Qed.
Instance tagged_sublist_proper stk : Proper (() ==> impl) (tagged_sublist stk).
Proof. move => ?? SUB H1 ? /H1 [? [/SUB ? ?]]. naive_solver. Qed.
Lemma tagged_sublist_app l1 l2 k1 k2 :
tagged_sublist l1 l2 tagged_sublist k1 k2
tagged_sublist (l1 ++ k1) (l2 ++ k2).
Proof.
move => H1 H2 it. setoid_rewrite elem_of_app.
move => [/H1|/H2]; naive_solver.
Qed.
Lemma remove_check_tagged_sublist cids stk stk' idx:
remove_check cids stk idx = Some stk' tagged_sublist stk' stk.
Proof.
revert idx.
induction stk as [|it stk IH]; intros idx; simpl.
{ destruct idx; [|done]. intros. by simplify_eq. }
destruct idx as [|idx]; [intros; by simplify_eq|].
case check_protector eqn:Eq; [|done].
move => /IH. apply tagged_sublist_proper. set_solver.
Qed.
Lemma replace_check'_tagged_sublist cids acc stk stk':
replace_check' cids acc stk = Some stk' tagged_sublist stk' (acc ++ stk).
Proof.
revert acc.
induction stk as [|it stk IH]; intros acc; simpl.
{ intros. simplify_eq. by rewrite app_nil_r. }
case decide => ?; [case check_protector; [|done]|];
move => /IH; [|by rewrite -app_assoc].
move => H1 it1 /H1 [it2 [IN2 [Eq1 [Eq2 ND]]]].
setoid_rewrite elem_of_app. setoid_rewrite elem_of_cons.
move : IN2 => /elem_of_app [/elem_of_app [?|/elem_of_list_singleton Eq]|?];
[..|naive_solver].
- exists it2. naive_solver.
- subst it2. exists it. naive_solver.
Qed.
Lemma replace_check_tagged_sublist cids stk stk':
replace_check cids stk = Some stk' tagged_sublist stk' stk.
Proof. move => /replace_check'_tagged_sublist. by rewrite app_nil_l. Qed.
(** NoDup for tagged item *)
Lemma stack_item_tagged_NoDup_singleton it:
stack_item_tagged_NoDup [it].
Proof.
rewrite /stack_item_tagged_NoDup filter_cons filter_nil.
case decide => ? /=. apply NoDup_singleton. apply NoDup_nil_2.
Qed.
Lemma stack_item_tagged_NoDup_cons_1 it stk :
stack_item_tagged_NoDup (it :: stk) stack_item_tagged_NoDup stk.
Proof.
rewrite /stack_item_tagged_NoDup filter_cons.
case decide => [NT|IT //]. rewrite fmap_cons. by apply NoDup_cons_12.
Qed.
Lemma stack_item_tagged_NoDup_sublist stk1 stk2:
sublist stk1 stk2 stack_item_tagged_NoDup stk2 stack_item_tagged_NoDup stk1.
Proof.
intros SUB. rewrite /stack_item_tagged_NoDup.
by apply NoDup_sublist, fmap_sublist, filter_sublist.
Qed.
Lemma replace_check'_stack_item_tagged_NoDup cids acc stk stk':
replace_check' cids acc stk = Some stk'
stack_item_tagged_NoDup (acc ++ stk) stack_item_tagged_NoDup stk'.
Proof.
revert acc.
induction stk as [|it stk IH]; intros acc; simpl.
{ intros ?. simplify_eq. by rewrite app_nil_r. }
case decide => ?; [case check_protector; [|done]|];
move => /IH; [|by rewrite -app_assoc].
move => IH1 ND. apply IH1. clear IH1. move : ND.
rewrite /stack_item_tagged_NoDup 3!filter_app 2!filter_cons.
case decide => [IT|NT].
- by rewrite decide_True // 3!fmap_app 2!fmap_cons /= -assoc.
- by rewrite decide_False // /= filter_nil app_nil_r.
Qed.
Lemma replace_check'_stack_item_tagged_NoDup_2 cids acc stk stk' stk0:
replace_check' cids acc stk = Some stk'
stack_item_tagged_NoDup (acc ++ stk ++ stk0) stack_item_tagged_NoDup (stk' ++ stk0).
Proof.
revert acc.
induction stk as [|it stk IH]; intros acc; simpl.
{ intros ?. by simplify_eq. }
case decide => ?; [case check_protector; [|done]|];
move => /IH; [|rewrite (app_assoc acc [it] (stk ++ stk0)); naive_solver].
move => IH1 ND. apply IH1. clear IH1. move : ND.
rewrite /stack_item_tagged_NoDup 3!filter_app 2!filter_cons.
case decide => [IT|NT].
- by rewrite decide_True // 3!fmap_app 2!fmap_cons /= -assoc.
- by rewrite decide_False // /= filter_nil app_nil_r.
Qed.
Lemma replace_check_stack_item_tagged_NoDup cids stk stk' :
replace_check cids stk = Some stk'
stack_item_tagged_NoDup stk stack_item_tagged_NoDup stk'.
Proof. intros. eapply replace_check'_stack_item_tagged_NoDup; eauto. Qed.
Lemma replace_check_stack_item_tagged_NoDup_2 cids stk stk' stk0:
replace_check cids stk = Some stk'
stack_item_tagged_NoDup (stk ++ stk0) stack_item_tagged_NoDup (stk' ++ stk0).
Proof. intros; eapply replace_check'_stack_item_tagged_NoDup_2; eauto. Qed.
Lemma replace_check'_acc_result cids acc stk stk' :
replace_check' cids acc stk = Some stk' acc stk'.
Proof.
revert acc.
induction stk as [|it stk IH]; intros acc; simpl; [by intros; simplify_eq|].
case decide => ?; [case check_protector; [|done]|];
move => /IH; set_solver.
Qed.
Lemma remove_check_stack_item_tagged_NoDup cids stk stk' idx:
remove_check cids stk idx = Some stk'
stack_item_tagged_NoDup stk stack_item_tagged_NoDup stk'.
Proof.
revert idx.
induction stk as [|it stk IH]; intros idx; simpl.
{ destruct idx; [|done]. intros ??. by simplify_eq. }
destruct idx as [|idx]; [intros ??; by simplify_eq|].
case check_protector eqn:Eq; [|done].
move => /IH IH' ND. apply IH'. by eapply stack_item_tagged_NoDup_cons_1.
Qed.
Lemma remove_check_stack_item_tagged_NoDup_2 cids stk stk' stk0 idx:
remove_check cids stk idx = Some stk'
stack_item_tagged_NoDup (stk ++ stk0) stack_item_tagged_NoDup (stk' ++ stk0).
Proof.
revert idx.
induction stk as [|it stk IH]; intros idx; simpl.
{ destruct idx; [|done]. intros ??. by simplify_eq. }
destruct idx as [|idx]; [intros ??; by simplify_eq|].
case check_protector eqn:Eq; [|done].
move => /IH IH' ND. apply IH'. by eapply stack_item_tagged_NoDup_cons_1.
Qed.
Lemma remove_check_sublist cids stk idx stk' :
remove_check cids stk idx = Some stk' sublist stk' stk.
Proof.
revert idx.
induction stk as [|it stk IH]; intros idx; simpl.
{ destruct idx; [|done]. intros ?. by simplify_eq. }
destruct idx as [|idx]; [intros ?; by simplify_eq|].
case check_protector eqn:Eq; [|done].
move => /IH IH'. by constructor 3.
Qed.
Lemma stack_item_tagged_NoDup_app stk1 stk2 :
stack_item_tagged_NoDup (stk1 ++ stk2)
stack_item_tagged_NoDup stk1 stack_item_tagged_NoDup stk2.
Proof. rewrite /stack_item_tagged_NoDup filter_app fmap_app NoDup_app. naive_solver. Qed.
Instance stack_item_tagged_NoDup_proper :
Proper (Permutation ==> iff) stack_item_tagged_NoDup.
Proof. intros stk1 stk2 PERM. by rewrite /stack_item_tagged_NoDup PERM. Qed.
Lemma stack_item_tagged_NoDup_eq stk it1 it2 t :
stack_item_tagged_NoDup stk
it1 stk it2 stk it1.(tg) = Tagged t it2.(tg) = Tagged t
it1 = it2.
Proof.
induction stk as [|it stk IH]; [set_solver|].
intros ND. specialize (IH (stack_item_tagged_NoDup_cons_1 _ _ ND)).
rewrite 2!elem_of_cons.
move => [?|In1] [?|In2]; subst; [done|..]; intros Eq1 Eq2.
- exfalso. apply elem_of_Permutation in In2 as [stk' Eq'].
move : ND. rewrite Eq'.
rewrite /stack_item_tagged_NoDup filter_cons decide_True; last by rewrite /is_tagged Eq1.
rewrite filter_cons decide_True; last by rewrite /is_tagged Eq2.
rewrite 2!fmap_cons Eq1 Eq2 NoDup_cons. set_solver.
- exfalso. apply elem_of_Permutation in In1 as [stk' Eq'].
move : ND. rewrite Eq'.
rewrite /stack_item_tagged_NoDup filter_cons decide_True; last by rewrite /is_tagged Eq2.
rewrite filter_cons decide_True; last by rewrite /is_tagged Eq1.
rewrite 2!fmap_cons Eq1 Eq2 NoDup_cons. set_solver.
- by apply IH.
Qed.
From stbor.lang Require Export defs steps_foreach steps_list.
Set Default Proof Using "Type".
(** Active protector preserving *)
Definition active_preserving (cids: call_id_stack) (stk stk': stack) :=
pm t c, c cids mkItem pm t (Some c) stk mkItem pm t (Some c) stk'.
Instance active_preserving_preorder cids : PreOrder (active_preserving cids).
Proof.
constructor.
- intros ??. done.
- intros ??? AS1 AS2 ?????. naive_solver.
Qed.
Lemma active_preserving_app_mono (cids: call_id_stack) (stk1 stk2 stk': stack) :
active_preserving cids stk1 stk2
active_preserving cids (stk1 ++ stk') (stk2 ++ stk').
Proof.
intros AS pm t c Inc. rewrite 2!elem_of_app.
specialize (AS pm t c Inc). set_solver.
Qed.
Lemma remove_check_active_preserving cids stk stk' idx:
remove_check cids stk idx = Some stk' active_preserving cids stk stk'.
Proof.
revert idx.
induction stk as [|it stk IH]; intros idx; simpl.
{ destruct idx; [|done]. intros ??. by simplify_eq. }
destruct idx as [|idx]; [intros ??; by simplify_eq|].
case check_protector eqn:Eq; [|done].
move => /IH AS pm t c IN /elem_of_cons [?|]; [|by apply AS].
subst it. exfalso. move : Eq.
by rewrite /check_protector /= /is_active bool_decide_true //.
Qed.
Lemma replace_check'_active_preserving cids acc stk stk':
replace_check' cids acc stk = Some stk' active_preserving cids stk stk'.
Proof.
revert acc.
induction stk as [|it stk IH]; intros acc; simpl.
{ intros. simplify_eq. by intros ?????%not_elem_of_nil. }
case decide => ?; [case check_protector eqn:Eq; [|done]|].
- move => /IH AS pm t c IN /elem_of_cons [?|]; [|by apply AS].
subst it. exfalso. move : Eq.
by rewrite /check_protector /= /is_active bool_decide_true //.
- move => Eq pm t c IN /elem_of_cons [?|].
+ apply (replace_check'_acc_result _ _ _ _ Eq), elem_of_app. right.
by apply elem_of_list_singleton.
+ by apply (IH _ Eq).
Qed.
Lemma replace_check_active_preserving cids stk stk':
replace_check cids stk = Some stk' active_preserving cids stk stk'.
Proof. by apply replace_check'_active_preserving. Qed.
Lemma access1_active_preserving stk stk' kind tg cids n:
access1 stk kind tg cids = Some (n, stk')
active_preserving cids stk stk'.
Proof.
rewrite /access1. case find_granting as [gip|]; [|done]. simpl.
destruct kind.
- case replace_check as [stk1|] eqn:Eq; [|done].
simpl. intros. simplify_eq.
rewrite -{1}(take_drop gip.1 stk).
by apply active_preserving_app_mono, replace_check_active_preserving.
- case find_first_write_incompatible as [idx|]; [|done]. simpl.
case remove_check as [stk1|] eqn:Eq; [|done].
simpl. intros. simplify_eq.
rewrite -{1}(take_drop gip.1 stk).
by eapply active_preserving_app_mono, remove_check_active_preserving.
Qed.
Lemma for_each_access1_active_preserving α cids l n tg kind α':
for_each α l n false
(λ stk, nstk' access1 stk kind tg cids; Some nstk'.2) = Some α'
l stk, α !! l = Some stk
stk', α' !! l = Some stk' active_preserving cids stk stk'.
Proof.
intros EQ. destruct (for_each_lookup _ _ _ _ _ EQ) as [EQ1 [EQ2 EQ3]].
intros l1 stk1 Eq1.
case (decide (l1.1 = l.1)) => [Eql|NEql];
[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 (EQ1 (Z.to_nat (l1.2 - l.2)) stk1)