Commit 65419b4f authored by Hai Dang's avatar Hai Dang
Browse files

WIP: copy public

parent a2c75761
......@@ -2,6 +2,43 @@ From stbor.lang Require Export defs.
Set Default Proof Using "Type".
Lemma init_mem_foldr' l n h (m: nat):
init_mem (l + m) n h =
fold_right (λ (i: nat) hi, <[(l + i):=%S]> hi) h (seq m n).
Proof.
revert m. induction n as [|n IHn]; intros m; [done|]. simpl. f_equal.
by rewrite shift_loc_assoc -(Nat2Z.inj_add m 1) Nat.add_1_r IHn.
Qed.
Lemma init_mem_foldr l n h:
init_mem l n h =
fold_right (λ (i: nat) hi, <[(l + i):=%S]> hi) h (seq 0 n).
Proof. by rewrite -init_mem_foldr' shift_loc_0. Qed.
Lemma free_mem_foldr' l n h (m: nat):
free_mem (l + m) n h =
fold_right (λ (i: nat) hi, delete (l + i) hi) h (seq m n).
Proof.
revert m. induction n as [|n IHn]; intros m; [done|]. simpl. f_equal.
by rewrite shift_loc_assoc -(Nat2Z.inj_add m 1) Nat.add_1_r IHn.
Qed.
Lemma free_mem_foldr l n h:
free_mem l n h =
fold_right (λ (i: nat) hi, delete (l + i) hi) h (seq 0 n).
Proof. by rewrite -free_mem_foldr' shift_loc_0. Qed.
Lemma init_stacks_foldr' α l n si (m: nat):
init_stacks α (l + m) n si =
fold_right (λ (i: nat) hi, <[(l + i):=[mkItem Unique si None]]> hi) α (seq m n).
Proof.
revert m. induction n as [|n IHn]; intros m; [done|]. simpl. f_equal.
by rewrite shift_loc_assoc -(Nat2Z.inj_add m 1) Nat.add_1_r IHn.
Qed.
Lemma init_stacks_foldr α l n si:
init_stacks α l n si =
fold_right (λ (i: nat) hi, <[(l + i):=[mkItem Unique si None]]> hi) α (seq 0 n).
Proof. by rewrite -init_stacks_foldr' shift_loc_0. Qed.
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',
......@@ -188,8 +225,7 @@ Proof.
Qed.
Lemma for_each_dom α l n f α' :
for_each α l n false f = Some α'
dom (gset loc) α dom (gset loc) α'.
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].
......
......@@ -311,6 +311,7 @@ Proof.
by eexists.
Qed.
(* Writing *)
Lemma find_first_write_incompatible_head stk pm idx t opro pmi
(HD: is_stack_head (mkItem pmi t opro) stk)
(NSRW: pmi SharedReadWrite) :
......@@ -377,6 +378,79 @@ Proof.
(mkItem Unique (Tagged ti) oproi) O ti ND); done.
Qed.
(* Reading *)
Lemma replace_check'_incompatible_items cids acc stk stk' stk0 it t
(ND: stack_item_tagged_NoDup (acc ++ stk ++ stk0)) :
it.(tg) = Tagged t it.(perm) = Unique it stk
replace_check' cids acc stk = Some stk'
it', it'.(tg) = Tagged t it' (stk' ++ stk0) it'.(perm) = Disabled.
Proof.
intros Eqt IU IN. revert acc ND.
induction stk as [|it0 stk IH]; simpl; intros acc ND; [set_solver|].
case decide => ?; [case check_protector; [|done]|]; last first.
{ move => /(IH ltac:(set_solver)).
rewrite -(app_assoc acc [it0] (stk ++ stk0)).
intros IH1 it' Eqit' Init'. apply IH1; [done..|]. clear -Init'. set_solver. }
move => RC.
have ND3: stack_item_tagged_NoDup
((acc ++ [mkItem Disabled it0.(tg) it0.(protector)]) ++ stk ++ stk0).
{ move : ND. clear.
rewrite (app_assoc acc [it0]) 2!(Permutation_app_comm acc) -2!app_assoc.
rewrite /stack_item_tagged_NoDup 2!filter_cons /=.
case decide => ?; [rewrite decide_True //|rewrite decide_False //]. }
have IN1:= (replace_check'_acc_result _ _ _ _ RC).
have IN': mkItem Disabled it0.(tg) it0.(protector) stk' ++ stk0 by set_solver.
have ND4 := replace_check'_stack_item_tagged_NoDup_2 _ _ _ _ _ RC ND3.
apply elem_of_cons in IN as [|IN].
{ intros it' Eqt' Init'. subst it0.
have ? : it' = mkItem Disabled it.(tg) it.(protector).
{ apply (stack_item_tagged_NoDup_eq _ _ _ t ND4 Init' IN' Eqt').
by rewrite Eqt. }
by subst it'. }
apply (IH IN _ ND3 RC).
Qed.
Lemma replace_check_incompatible_items cids stk stk' stk0 it t
(ND: stack_item_tagged_NoDup (stk ++ stk0)) :
it.(tg) = Tagged t it.(perm) = Unique it stk
replace_check cids stk = Some stk'
it', it'.(tg) = Tagged t it' (stk' ++ stk0) it'.(perm) = Disabled.
Proof. intros ????. eapply (replace_check'_incompatible_items _ []); eauto. Qed.
Lemma access1_read_replace_incompatible_head stk t ti cids n stk'
(ND: stack_item_tagged_NoDup stk) :
( oproi, is_stack_head (mkItem Unique (Tagged ti) oproi) stk)
access1 stk AccessRead (Tagged t) cids = Some (n, stk')
t ti
pm opro, (mkItem pm (Tagged ti) opro) stk' pm = Disabled.
Proof.
intros HD. rewrite /access1.
case find_granting as [[n' pm']|] eqn:GRANT; [|done]. simpl.
case replace_check as [stk1|] eqn:Eq; [|done].
simpl. intros ?. simplify_eq.
intros NEQ pm opro. destruct HD as [oproi HD].
rewrite -{1}(take_drop n stk) in ND.
eapply (replace_check_incompatible_items _ _ _ _ (mkItem Unique (Tagged ti) oproi) ti ND);
try done.
have HD' := find_granting_incompatible_head _ _ _ _ _ _ _ _ HD NEQ GRANT.
clear -HD'. destruct HD' as [? EqD]. rewrite EqD. by left.
Qed.
Lemma access1_read_replace_incompatible_head_protector stk t ti cids n stk' c :
(is_stack_head (mkItem Unique (Tagged ti) (Some c)) stk)
c cids
access1 stk AccessRead (Tagged t) cids = Some (n, stk')
t ti False.
Proof.
intros HD ACTIVE. rewrite /access1.
case find_granting as [[n' pm']|] eqn:GRANT; [|done]. simpl.
case replace_check as [stk1|] eqn:Eq; [|done].
simpl. intros ?. simplify_eq. intros NEQ.
have HD' := find_granting_incompatible_head _ _ _ _ _ _ _ _ HD NEQ GRANT.
destruct HD' as [stk' Eqs].
move : Eq. rewrite Eqs /replace_check /= /check_protector /=.
Abort.
Lemma active_SRO_elem_of t stk :
t active_SRO stk i it, stk !! i = Some it it.(tg) = Tagged t
it.(perm) = SharedReadOnly
......
......@@ -3,42 +3,6 @@ From stbor.lang Require Export defs steps_foreach steps_list.
Set Default Proof Using "Type".
Lemma init_mem_foldr' l n h (m: nat):
init_mem (l + m) n h =
fold_right (λ (i: nat) hi, <[(l + i):=%S]> hi) h (seq m n).
Proof.
revert m. induction n as [|n IHn]; intros m; [done|]. simpl. f_equal.
by rewrite shift_loc_assoc -(Nat2Z.inj_add m 1) Nat.add_1_r IHn.
Qed.
Lemma init_mem_foldr l n h:
init_mem l n h =
fold_right (λ (i: nat) hi, <[(l + i):=%S]> hi) h (seq 0 n).
Proof. by rewrite -init_mem_foldr' shift_loc_0. Qed.
Lemma free_mem_foldr' l n h (m: nat):
free_mem (l + m) n h =
fold_right (λ (i: nat) hi, delete (l + i) hi) h (seq m n).
Proof.
revert m. induction n as [|n IHn]; intros m; [done|]. simpl. f_equal.
by rewrite shift_loc_assoc -(Nat2Z.inj_add m 1) Nat.add_1_r IHn.
Qed.
Lemma free_mem_foldr l n h:
free_mem l n h =
fold_right (λ (i: nat) hi, delete (l + i) hi) h (seq 0 n).
Proof. by rewrite -free_mem_foldr' shift_loc_0. Qed.
Lemma init_stacks_foldr' α l n si (m: nat):
init_stacks α (l + m) n si =
fold_right (λ (i: nat) hi, <[(l + i):=[mkItem Unique si None]]> hi) α (seq m n).
Proof.
revert m. induction n as [|n IHn]; intros m; [done|]. simpl. f_equal.
by rewrite shift_loc_assoc -(Nat2Z.inj_add m 1) Nat.add_1_r IHn.
Qed.
Lemma init_stacks_foldr α l n si:
init_stacks α l n si =
fold_right (λ (i: nat) hi, <[(l + i):=[mkItem Unique si None]]> hi) α (seq 0 n).
Proof. by rewrite -init_stacks_foldr' shift_loc_0. Qed.
Lemma wf_init_state : Wf init_state.
Proof.
constructor; simpl; try (intros ?; set_solver).
......
......@@ -198,6 +198,12 @@ Proof.
(* impossible: t' is protected by c' which is still active.
So t t' and protected(t',c') is on top of (l + i), so access with t is UB *)
exfalso.
have NEQ: t' t.
{ intros ?. subst t'.
apply (ptrmap_lookup_op_r_equiv_pub r_f.1) in PUB as [? PUB];
[|by apply VALID].
rewrite -> PUB in Eqh'. apply Some_equiv_inj in Eqh' as [Eqk' ?].
inversion Eqk'. }
specialize (CINV _ _ Eqci) as [Inc' CINV].
specialize (CINV _ InT') as [Ltt' CINV].
specialize (CINV _ _ Eqh' _ Inl) as (stk & pm & Eqstk & Instk & NDIS).
......@@ -207,6 +213,12 @@ Proof.
rewrite -Some_valid -Eqh'. apply VALID. }
destruct (heapletR_elem_of_dom _ _ VALh' Inl) as [s Eqs].
specialize (PINV _ _ Eqs _ Eqstk _ _ Instk NDIS) as (Eqss & HD).
destruct (for_each_lookup _ _ _ _ _ Eqα') as [EQ1 _].
rewrite Eqlt in HLLt.
specialize (EQ1 _ _ HLLt Eqstk) as (stk' & Eqstk' & EQ2).
move : EQ2. case access1 as [[n1 stk1]|] eqn:EQ3; [|done].
simpl. inversion 1. subst stk1.
have ND := proj2 (state_wf_stack_item _ WFT _ _ Eqstk).
admit.
}
exists (Val vs), σs', (r (core (r_f r))), (S n). split; last split.
......
Supports Markdown
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