Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps rslassn rslassnlemmas rslmodel rslhmap.
Set Implicit Arguments.
We develop the following helper lemma in order to simplify the proofs of
various RSL proof rules.
Lemma triple_helper_start mt P e QQ :
(∀ res acts_cmd lab sb fst lst
(SEM : exp_sem e res acts_cmd lab sb fst lst) a
(MT : mt = Model_standard_c11)
(IN : In a acts_cmd) (RW : is_rlx_write (lab a)), False) →
(∀ res acts_cmd lab sb fst lst
(SEM : exp_sem e res acts_cmd lab sb fst lst) acts_ctx rf mo sc
(CONS : weakConsistent (acts_cmd ++ acts_ctx) lab sb rf mo sc mt)
(UNIQ : NoDup (acts_cmd ++ acts_ctx))
prev (FST : unique (sb^~ fst) prev)
next (LST : unique (sb lst) next)
n V (V_PREV : In prev V)
(V_CTX : ∀ x : actid, In x V → In x acts_ctx)
(HC : hist_closed mt lab sb rf mo V)
hmap
(VALID : ∀ e, In e V → hmap_valid lab sb rf hmap e)
(pDEF : hmap (hb_sb prev fst) ≠ Hundef) hp hFR
(pEQ : hmap (hb_sb prev fst) = hp +!+ hFR)
(pSAT : assn_sem P hp)
(NIN : ¬ In fst V)
(HC : hist_closed mt lab sb rf mo (fst :: V))
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(NOREL : with_mt mt (no_rlx_writes_global lab) True),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (fst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (fst :: V) hmap' lst
(with_opt res
(fun res h ⇒ ∃ hq, h ≠ Hundef ∧ h = hq +!+ hFR
∧ assn_sem (QQ res) hq))) →
triple mt P e QQ.
Configuration safety is invariant over Permutations of acts_cmd.
Lemma Permutation_safe1 :
∀ l l' (P : Permutation l l') mt acts lab sb rf mo n V hmap lst Q,
safe mt l acts lab sb rf mo n V hmap lst Q →
safe mt l' acts lab sb rf mo n V hmap lst Q.
We now develop a number of lemmas for establishing configuration safety of
final configurations.
Definition mclearw h x (exn : list actid) := fun y ⇒
match y with
| hb_sw a b ⇒ if a == x then if b \in exn then h y else hemp else h y
| hb_sb _ _ ⇒ h y
end.
Definition mclears h x := fun y ⇒
match y with
| hb_sw _ _ ⇒ h y
| hb_sb a b ⇒ if a == x then hemp else h y
end.
Definition mupd_sw h x y z := fun t ⇒
match t with
| hb_sw a b ⇒ if b == y then if a == x then z else hemp else h t
| hb_sb _ _ ⇒ h t
end.
Lemma map_upd_irr (A: eqType) B C (hmap : A → B) x y f (l : list C) :
(∀ a, In a l → f a ≠ x) →
map (mupd hmap x y) (map f l) = map hmap (map f l).
Lemma map_clearw_irr A hmap x exn f (l : list A) :
(∀ a b, In a l → f a = hb_sw x b → In b exn) →
map (mclearw hmap x exn) (map f l) = map hmap (map f l).
Lemma map_clears_irr A hmap x f (l : list A) :
(∀ a b, In a l → f a = hb_sb x b → False) →
map (mclears hmap x) (map f l) = map hmap (map f l).
Lemma map_upd_sw_irr C hmap x y z f (l : list C) :
(∀ a b, In a l → f a ≠ hb_sw b y) →
map (mupd_sw hmap x y z) (map f l) = map hmap (map f l).
Lemma map_upd_sw_same hmap a b h l :
NoDup l →
In a l →
hsum (map (mupd_sw hmap a b h) (map (hb_sw^~ b) l)) = h.
Lemma map_upd_sw_same2 hmap a b h l :
NoDup l →
In b l →
hsum (map (mupd_sw hmap a b h) (map (hb_sw a) l)) =
h +!+ hsum (map (mupd hmap (hb_sw a b) hemp) (map (hb_sw a) l)).
Lemma map_upd_sw_same3 hmap a b h l :
NoDup l →
In b l →
hmap (hb_sw a b) = hemp →
hsum (map (mupd_sw hmap a b h) (map (hb_sw a) l)) =
h +!+ hsum (map hmap (map (hb_sw a) l)).
Lemma map_clearw_sws :
∀ hmap x l, hsum (map (mclearw hmap x nil) (map (hb_sw x) l)) = hemp.
Lemma map_clears_edges :
∀ hmap x l, hsum (map (mclears hmap x) (map (hb_sb x) l)) = hemp.
Lemma valid_ext :
∀ mt lab sb rf mo hmap e V
(VAL : hmap_valid lab sb rf hmap e) (IN: In e V)
(HC : hist_closed mt lab sb rf mo V) a (NIN: ¬ In a V) b h,
hmap_valid lab sb rf (mupd hmap (hb_sb a b) h) e.
Lemma valid_ext_sw_helper :
∀ hmap a b h e l hsink (NEQ: e ≠ a),
∃ hsink' : heap,
hsum (map (mupd_sw hmap a b h) (map (hb_sw e) l)) +!+ hsink' =
hsum (map hmap (map (hb_sw e) l)) +!+ hsink.
Lemma valid_ext_sw :
∀ mt lab sb rf mo hmap e V
(VAL: hmap_valid lab sb rf hmap e) (IN: In e V)
(HC : hist_closed mt lab sb rf mo V) b
(NIN: ¬ In b V) a (NEQ': e ≠ a) h,
hmap_valid lab sb rf (mupd_sw hmap a b h) e.
Lemma valid_ext_clearw :
∀ mt lab sb rf mo hmap e V
(VAL : hmap_valid lab sb rf hmap e)
(HC : hist_closed mt lab sb rf mo V) a (NIN: ¬ In a V) (IN: In e V) exn,
hmap_valid lab sb rf (mclearw hmap a exn) e.
Lemma valid_ext_clearw_helper :
∀ hmap a V e l hsink,
∃ hsink' : heap,
hsum (map (mclearw hmap a V) (map (hb_sw e) l)) +!+ hsink' =
hsum (map hmap (map (hb_sw e) l)) +!+ hsink.
Lemma valid_ext_clearw2 :
∀ mt lab sb rf mo hmap w e V
(ACYC: IrreflexiveHB lab sb rf mo)
(VAL : hmap_valid lab sb rf hmap e) (IN : In e V)
(HC : hist_closed mt lab sb rf mo V),
hmap_valid lab sb rf (mclearw hmap w V) e.
Lemma valid_ext_clears :
∀ mt lab sb rf mo hmap e V
(VAL : hmap_valid lab sb rf hmap e)
(HC : hist_closed mt lab sb rf mo V) (IN: In e V) a (NIN: ¬ In a V),
hmap_valid lab sb rf (mclears hmap a) e.
Lemma safe_mod :
∀ mt acts_cmd acts_ctx lab sb rf mo n V hmap lst QQ
(H : safe mt acts_cmd acts_ctx lab sb rf mo n V hmap lst QQ)
acts_cmd' (E1: ∀ x (NIN: ¬ In x V) (IN: In x acts_cmd'), In x acts_cmd)
acts_ctx' (E2: ∀ x (NIN: ¬ In x V) (IN: In x acts_ctx'), In x acts_ctx),
safe mt acts_cmd' acts_ctx' lab sb rf mo n V hmap lst QQ.
Lemma safe_final1 :
∀ mt acts_cmd acts_ctx lab sb rf mo lst
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
V Q n hmap
(HC: hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap e)
(POST: ∀ next (SB: sb lst next), Q (hmap (hb_sb lst next)) : Prop),
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap lst Q.
Lemma safe_final_plain :
∀ mt acts_cmd acts_ctx lab sb rf mo n V lst hmap Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd hmap (hb_sb lst next) h) lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Lemma safe_final_plain2 :
∀ mt acts_cmd acts_ctx lab sb mo rf n V lst hmap Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mupd_sw hmap lst lst hemp)
(hb_sb lst next) h) lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Lemma safe_final3 :
∀ mt exn acts_cmd acts_ctx lab sb rf mo n V lst hmap Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mclearw hmap lst exn) (hb_sb lst next) h) lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Lemma safe_final4a :
∀ mt acts_cmd acts_ctx lab sb rf mo n V lst hmap Q wri next h h'
(ACYC: IrreflexiveHB lab sb rf mo)
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mupd_sw
(mclearw hmap wri V) wri lst h')
(hb_sb lst next) h) lst)
(VALID'': hmap_valid lab sb rf (mupd_sw (mclearw hmap wri V) wri lst h') wri)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Lemma safe_final4b :
∀ mt acts_cmd acts_ctx lab sb rf mo n V lst hmap Q wri next h h'
(ACYC: IrreflexiveHB lab sb rf mo)
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mclearw (mupd (mupd_sw
(mclearw hmap wri V) wri lst h')
(hb_sb lst next) h) lst nil) lst)
(VALID'': hmap_valid lab sb rf (mupd_sw (mclearw hmap wri V) wri lst h') wri)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Lemma safe_final4 :
∀ mt acts_cmd acts_ctx lab sb rf mo n V lst hmap Q wri next h h'
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mupd_sw hmap wri lst h')
(hb_sb lst next) h) lst)
(VALID': hmap_valid lab sb rf (mupd_sw hmap wri lst h') wri)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Lemma safe_final5 :
∀ mt acts_cmd acts_ctx lab sb mo rf n V lst hmap Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mupd_sw hmap lst lst hemp)
(hb_sb lst next) h) lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst Q.
Lemma has_sb_succs acts lab sb a :
ExecutionFinite acts lab sb →
∃ posts,
<< qND: NoDup posts >> ∧
<< qIN: ∀ x, In x posts ↔ sb a x >>.
Lemma safe_nt :
∀ mt acts_cmd acts_ctx lab sb mo rf n V lst hmap
(FIN: ExecutionFinite (acts_cmd ++ acts_ctx) lab sb)
(IRR: IrreflexiveHB lab sb rf mo)
(CONS_A: ConsistentAlloc lab)
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed mt lab sb rf mo V)
(HC': hist_closed mt lab sb rf mo (lst :: V))
(VALID: ∀ e (IN: In e V), hmap_valid lab sb rf hmap e)
(LAB: lab lst = Askip)
(NIN: ¬ In lst V),
∃ hmap',
agrees lab sb rf V hmap hmap' ∧
(∀ e (IN: In e (lst :: V)), hmap_valid lab sb rf hmap' e) ∧
safe mt acts_cmd acts_ctx lab sb rf mo n (lst :: V) hmap' lst (fun _ ⇒ True).
This page has been generated by coqdoc Imprint | Data protection