Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 exps fslassn fslassnsem fslassnlemmas fslmodel fslhmap.
Require Import GpsSepAlg.
Set Implicit Arguments.
We develop the following helper lemma in order to simplify the proofs of
various RSL proof rules.
Lemma triple_helper_start PS PSg P e QQ :
(∀ 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 Model_hb_rf_acyclic)
(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 sb rf V)
hmap
(VALID : hmap_valids_strong lab sb rf hmap V)
(pDEF : hmap (hb_sb prev fst) ≠ @Hundef PS PSg) hp hFR
(pEQ : hmap (hb_sb prev fst) = hp +!+ hFR)
(pSAT : assn_sem P hp)
(NIN : ¬ In fst V)
(HC : hist_closed sb rf (fst :: V))
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst),
∃ hmap',
agrees sb rf V hmap hmap' ∧
(hmap_valids_strong lab sb rf hmap' (fst :: V)) ∧
safe acts_cmd acts_ctx lab sb rf n (fst :: V) hmap' lst
(with_opt res
(fun res h ⇒ ∃ hFR' hq, h ≠ @Hundef PS PSg ∧ h = hq +!+ hFR +!+ hFR'
∧ assn_sem (QQ res) hq))) →
triple P e QQ.
Configuration safety is invariant over Permutations of acts_cmd.
Lemma Permutation_safe1 PS PSg :
∀ l l' (P : Permutation l l') acts lab sb rf n V hmap lst Q,
@safe PS PSg l acts lab sb rf n V hmap lst Q →
safe l' acts lab sb rf n V hmap lst Q.
We now develop a number of lemmas for establishing configuration safety of
final configurations.
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).
Definition ga_agrees (ga ga': val → option actid) e := ∀ x, ga x = Some e ↔ ga' x = Some e.
Definition ga_clear (ga: val → option actid) e l :=
if excluded_middle_informative(ga l = Some e) then None else ga l.
Lemma ga_agrees_same: ∀ ga e, ga_agrees ga ga e.
Lemma ga_agrees_sym: ∀ ga ga' e, ga_agrees ga ga' e ↔ ga_agrees ga' ga e.
Lemma ga_clear_agrees: ∀ ga e e', e ≠ e' → ga_agrees ga (ga_clear ga e) e'.
Lemma ga_clear_fin ga e:
(∃ max, ∀ n, max < n → ga n = None)
→ ∃ max, ∀ n, max < n → ga_clear ga e n = None.
Lemma valid_ext PS PSg :
∀ lab sb rf hmap ga ga' e V
(VAL : @hmap_valid PS PSg lab sb rf hmap ga e) (IN: In e V)
(GAA : ga_agrees ga ga' e)
(HC : hist_closed sb rf V) a (NIN: ¬ In a V) b h,
hmap_valid lab sb rf (mupd hmap (hb_sb a b) h) ga' e.
Lemma valid_ext_sink PS PSg :
∀ lab sb rf hmap ga ga' e V
(VAL : @hmap_valid PS PSg lab sb rf hmap ga e) (IN: In e V)
(GAA : ga_agrees ga ga' e)
(HC : hist_closed sb rf V) a (NIN: ¬ In a V) h,
hmap_valid lab sb rf (mupd hmap (hb_sink a) h) ga' e.
Lemma hmap_irr_change_valid PS PSg:
∀ lab sb rf hmap hmap' ga ga' e
(VALID: @hmap_valid PS PSg lab sb rf hmap ga e)
(GAA : ga_agrees ga ga' e)
(IRR: ∀ edge, hb_fst edge = e ∨ hb_snd edge = Some e → hmap' edge = hmap edge),
hmap_valid lab sb rf hmap' ga' e.
Lemma safe_mod PS PSg :
∀ acts_cmd acts_ctx lab sb rf n V hmap lst QQ
(H : @safe PS PSg acts_cmd acts_ctx lab sb rf 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 acts_cmd' acts_ctx' lab sb rf n V hmap lst QQ.
Lemma safe_final1 PS PSg :
∀ acts_cmd acts_ctx lab sb rf lst
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
V Q n hmap
(HC: hist_closed sb rf (lst :: V))
(VALID: @hmap_valids_strong PS PSg lab sb rf hmap (lst :: V))
(POST: ∀ next (SB: sb lst next), Q (hmap (hb_sb lst next)) : Prop),
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap lst Q.
Lemma safe_final_plain PS PSg :
∀ acts_cmd acts_ctx lab sb rf n V lst hmap ga ga' Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed sb rf V)
(HC': hist_closed sb rf (lst :: V))
(VLD: ∀ e (IN: In e V), hmap_valid lab sb rf hmap ga e)
(RESTR: ∀ e (NIN: ¬ In e V) edge,
(hb_fst edge = e ∨ (hb_snd edge = Some e ∧ ¬ is_sb_out edge V) → hmap edge = @hemp PS PSg))
(GAA: ∀ e (IN: In e V), ga_agrees ga ga' e)
(GA'fin: ∃ max, ∀ n, max < n → ga' n = None)
(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) ga' lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees sb rf V hmap hmap' ∧
hmap_valids_strong lab sb rf hmap' (lst :: V) ∧
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap' lst Q.
Lemma safe_final_plain2 PS PSg :
∀ acts_cmd acts_ctx lab sb rf n V lst hmap ga ga' Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed sb rf V)
(HC': hist_closed sb rf (lst :: V))
(VLD: ∀ e (IN: In e V), hmap_valid lab sb rf hmap ga e)
(RESTR: ∀ e (NIN: ¬ In e V) edge,
(hb_fst edge = e ∨ (hb_snd edge = Some e ∧ ¬ is_sb_out edge V) → hmap edge = @hemp PS PSg))
(GAA: ∀ e (IN: In e V), ga_agrees ga ga' e)
(GA'fin: ∃ max, ∀ n, max < n → ga' n = None)
(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) ga' lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees sb rf V hmap hmap' ∧
hmap_valids_strong lab sb rf hmap' (lst :: V) ∧
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap' lst Q.
Lemma safe_final3 PS PSg :
∀ acts_cmd acts_ctx lab sb rf n V lst hmap ga ga' Q next h
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed sb rf V)
(HC': hist_closed sb rf (lst :: V))
(VLD: ∀ e (IN: In e V), hmap_valid lab sb rf hmap ga e)
(RESTR: ∀ e (NIN: ¬ In e V) edge,
(hb_fst edge = e ∨ (hb_snd edge = Some e ∧ ¬ is_sb_out edge V) → hmap edge = @hemp PS PSg))
(GAA: ∀ e (IN: In e V), ga_agrees ga ga' e)
(GA'fin: ∃ max, ∀ n, max < n → ga' n = None)
(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) ga' lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees sb rf V hmap hmap' ∧
hmap_valids_strong lab sb rf hmap' (lst :: V) ∧
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap' lst Q.
Lemma safe_final3s PS PSg :
∀ acts_cmd acts_ctx lab sb rf n V lst hmap ga ga' Q next h hs
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed sb rf V)
(HC': hist_closed sb rf (lst :: V))
(VLD: ∀ e (IN: In e V), hmap_valid lab sb rf hmap ga e)
(RESTR: ∀ e (NIN: ¬ In e V) edge,
(hb_fst edge = e ∨ (hb_snd edge = Some e ∧ ¬ is_sb_out edge V) → hmap edge = @hemp PS PSg))
(GAA: ∀ e (IN: In e V), ga_agrees ga ga' e)
(GA'fin: ∃ max, ∀ n, max < n → ga' n = None)
(LST: unique (fun x ⇒ sb lst x) next)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd (mupd hmap (hb_sb lst next) h) (hb_sink lst) hs) ga' lst)
(NIN: ¬ In lst V),
∃ hmap',
agrees sb rf V hmap hmap' ∧
hmap_valids_strong lab sb rf hmap' (lst :: V) ∧
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap' lst Q.
Lemma safe_final4a PS PSg :
∀ acts_cmd acts_ctx lab sb rf n V lst hmap ga ga' Q wri next hr hsinkw h hs
(LR: ∀ x (IN: In x acts_cmd), clos_refl_trans actid sb x lst)
(HC: hist_closed sb rf V)
(HC': hist_closed sb rf (lst :: V))
(VLD: ∀ e (IN: In e V), hmap_valid lab sb rf hmap ga e)
(RESTR: ∀ e (NIN: ¬ In e V) edge,
(hb_fst edge = e ∨ (hb_snd edge = Some e ∧ ¬ is_sb_out edge V) → hmap edge = @hemp PS PSg))
(GAA: ∀ e (IN: In e V), ga_agrees ga ga' e)
(GA'fin: ∃ max, ∀ n, max < n → ga' n = None)
(LST: unique (fun x ⇒ sb lst x) next)
(RF: rf lst = Some wri)
(POST: Q h : Prop)
(VALID': hmap_valid lab sb rf (mupd
(mupd
(mupd
(mupd
hmap
(hb_rf wri lst) hr)
(hb_sink wri) hsinkw)
(hb_sb lst next) h)
(hb_sink lst) hs) ga'
lst)
(VALID'': hmap_valid lab sb rf (mupd (mupd hmap (hb_rf wri lst) hr) (hb_sink wri) hsinkw) ga' wri)
(NIN: ¬ In lst V),
∃ hmap',
agrees sb rf V hmap hmap' ∧
hmap_valids_strong lab sb rf hmap' (lst :: V) ∧
safe acts_cmd acts_ctx lab sb rf n (lst :: V) hmap' lst Q.
This page has been generated by coqdoc