Commit d51d5e9b authored by Hai Dang's avatar Hai Dang

WIP: public retag

parent c69ae521
......@@ -168,10 +168,7 @@ Proof.
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.
- destruct Eql as (i & Lt & ?). subst l1. rewrite EQ1 // in Eq1.
Qed.
Lemma free_mem_lookup l n h :
......@@ -201,16 +198,13 @@ 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.
i : nat, (i < n)%nat 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.
subst l'. by apply EQ1.
Qed.
Lemma free_mem_dom l' l n h:
......
......@@ -88,7 +88,7 @@ Qed.
Lemma block_case l l' n :
( i : nat, (i < n)%nat l' l + i)
i, (0 i < n) l' = l + i.
i : nat, (i < n)%nat l' = l + i.
Proof.
case (decide (l'.1 = l.1)) => [Eql|NEql];
[case (decide (l.2 l'.2 < l.2 + n)) => [[Le Lt]|NIN]|].
......@@ -104,7 +104,7 @@ 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.
stk = stk' f stk = Some stk' i : nat, (i < n)%nat l' = l + i.
Proof.
intros EQ. destruct (for_each_lookup _ _ _ _ _ EQ) as [EQ1 [EQ2 EQ3]].
intros l1 stk stk' Eq Eq'.
......@@ -112,11 +112,9 @@ Proof.
- left. rewrite EQ3 in Eq'; [by simplify_eq|].
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.
destruct Eql as (i & Lt & Eql). subst l1.
destruct (EQ2 _ _ Lt Eq') as [stk1 [Eq1 Eq2]].
rewrite Eq in Eq1. by simplify_eq.
Qed.
Lemma for_each_lookup_case_2 α l n f α' :
......@@ -145,7 +143,7 @@ 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 + 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.
......@@ -193,7 +191,7 @@ 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.
i : nat, (i < n)%nat l' = l + i.
Proof.
destruct (init_mem_lookup l n h) as [EQ1 EQ2].
intros l1 s1 Eq'.
......@@ -204,7 +202,7 @@ Qed.
Lemma init_mem_lookup_empty l n :
l' s', init_mem l n !! l' = Some s'
i, (0 i < n) l' = l + i.
i : nat, (i < n)%nat l' = l + i.
Proof. move => l' s' /init_mem_lookup_case [[//]|//]. Qed.
Lemma init_stacks_lookup α l n t :
......@@ -236,7 +234,7 @@ 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.
i : nat, (i < n)%nat l' = l + i.
Proof.
destruct (init_stacks_lookup α l n t) as [EQ1 EQ2].
intros l1 s1 Eq'.
......@@ -248,7 +246,7 @@ 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
i : nat, (i < n)%nat l' = l + i
init_stacks α l n t !! l' = Some $ init_stack t.
Proof.
destruct (init_stacks_lookup α l n t) as [EQ1 EQ2].
......@@ -256,9 +254,7 @@ Proof.
destruct (block_case l l1 n) as [NEql|Eql].
- left. rewrite EQ2 //.
- right. destruct Eql as (i & Lt & ?).
exists i. do 2 (split; [done|]). subst l1. destruct Lt.
move : (EQ1 (Z.to_nat i)). rewrite Z2Nat.id //. intros EQ'. apply EQ'.
rewrite -(Nat2Z.id n). by apply Z2Nat.inj_lt; lia.
exists i. do 2 (split; [done|]). subst l1. by apply EQ1.
Qed.
Lemma for_each_dom α l n f α' :
......
......@@ -726,52 +726,6 @@ Proof.
move => /reborrowN_lookup [_ [_ HL]]. by apply HL.
Qed.
Lemma item_insert_dedup_lookup stk it i (IS: is_Some (stk !! i)):
j, (item_insert_dedup stk it i) !! j = Some it
(j = i (1 i j = i - 1)%nat)
( j', (j' < j)%nat (item_insert_dedup stk it i) !! j' = stk !! j').
Proof.
destruct i as [|i]; simpl.
- destruct stk as [|it' stk']; [by destruct IS|]. case decide => [->|?].
+ exists O. naive_solver.
+ exists O. split; [done|]. split;[by left| intros; lia].
- destruct IS as [it1 Eq1]. rewrite Eq1.
destruct (stk !! i) as [it2|] eqn:Eq2; last first.
{ apply lookup_ge_None_1 in Eq2. apply lookup_lt_Some in Eq1. lia. }
case decide => [->|?]; [|case decide => [->|?]].
+ exists i. split; [done|]. rewrite Nat.sub_0_r. split; [right; lia|done].
+ exists (S i). split; [done|]. split; [by left|done].
+ exists (S i). rewrite Nat.sub_0_r. split; last split; [|by left|].
* rewrite list_lookup_middle // take_length_le //.
by eapply Nat.lt_le_incl, lookup_lt_Some.
* intros j' Lt'. rewrite lookup_app_l; [apply lookup_take; lia|].
rewrite take_length_le //. by eapply Nat.lt_le_incl, lookup_lt_Some.
Qed.
Lemma find_granting_Some stk kind bor i pi :
find_granting stk kind bor = Some (i, pi)
is_Some (stk !! i)
j jt, (j < i)%nat stk !! j = Some jt
¬ (grants jt.(perm) kind jt.(tg) = bor).
Proof.
move => /fmap_Some [[i' pi'] [/list_find_Some_not_earlier [Eq1 [MG LT]] Eq2]].
simplify_eq. simpl. split; [by eexists|by apply LT].
Qed.
Lemma item_insert_dedup_new stk new i (NIN: new stk) (IS: is_Some (stk !! i)):
item_insert_dedup stk new i = take i stk ++ new :: drop i stk.
Proof.
destruct i as [|i]; simpl.
- destruct stk as [|it stk]; [done|]. rewrite decide_False //.
intros ?. subst. apply NIN. by left.
- destruct IS as [its Eqs]. rewrite Eqs.
destruct (stk !! i) as [it|] eqn:Eq; last first.
{ apply lookup_ge_None_1 in Eq. apply lookup_lt_Some in Eqs. lia. }
rewrite decide_False; last first.
{ intros ?. subst. by eapply NIN, elem_of_list_lookup_2. }
rewrite decide_False //.
intros ?. subst. by eapply NIN, elem_of_list_lookup_2.
Qed.
Lemma retag_ref_is_freeze_is_Some α cids nxtp l old T kind prot
(BLK: n, (n < tsize T)%nat l + n dom (gset loc) α)
......
This diff is collapsed.
......@@ -538,13 +538,11 @@ Proof.
move => it /elem_of_cons [-> //|] / (proj1 (WF _ _ Eq)) [Lt ?].
split; [|done]. move : Lt. destruct it.(tg); [lia|done].
- destruct (for_each_lookup_case _ _ _ _ _ ACC _ _ _ Eq Eq')
as [?|[Eqf [i [[Le Lt] ?]]]].
as [?|[Eqf [i [Lt ?]]]].
{ subst. by apply (WF _ _ Eq). }
eapply grant_stack_item_tagged_NoDup; eauto.
+ destruct new.(tg); [|done].
subst l'. intros it. apply (NEW (Z.to_nat i)).
* rewrite -(Nat2Z.id n) -Z2Nat.inj_lt; by lia.
* by rewrite Z2Nat.id.
subst l'. intros it. by apply (NEW i).
+ by apply (WF _ _ Eq).
Qed.
......
This diff is collapsed.
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