Theory Combined
section ‹Combined Progress Tracking Protocol\label{sec:combined}›
theory Combined
imports
Exchange
Propagate
begin
lemma fold_invar:
assumes "finite M"
and "P z"
and "∀z. ∀x∈M. P z ⟶ P (f x z)"
and "comp_fun_commute f"
shows "P (Finite_Set.fold f z M)"
proof -
interpret commute: comp_fun_commute f
by (fact ‹comp_fun_commute f›)
from assms show ?thesis
by (induct M arbitrary: z rule: finite_induct) auto
qed
subsection‹Could-result-in Relation›
context dataflow_topology begin
definition cri_less_eq :: "('loc × 't) ⇒ ('loc × 't) ⇒ bool" ("_≤⇩p_" [51,51] 50) where
"cri_less_eq =
(λ(loc1,t1) (loc2,t2). (∃s. s ∈⇩A path_summary loc1 loc2 ∧ results_in t1 s ≤ t2))"
definition cri_less :: "('loc × 't) ⇒ ('loc × 't) ⇒ bool" ("_<⇩p_" [51,51] 50) where
"cri_less x y = (x ≤⇩p y ∧ x ≠ y)"
lemma cri_asym1: "x <⇩p y ⟶ ¬ y <⇩p x"
for x y apply (cases x; cases y)
proof (rule ccontr)
fix loc1 t1 loc2 t2
assume as: "¬ (x <⇩p y ⟶ ¬ y <⇩p x)" "x = (loc1, t1)" "y = (loc2, t2)"
then have as1: "loc1 ≠ loc2"
unfolding cri_less_def cri_less_eq_def
by clarsimp
(metis add.right_neutral order.antisym order.trans le_plus(2) results_in_mono(2) results_in_zero)
from as obtain s1 where s1: "s1 ∈⇩A path_summary loc1 loc2"
"results_in t1 s1 ≤ t2"
using cri_less_def cri_less_eq_def by auto
then obtain path1 where path1: "flow.path loc1 loc2 path1"
"s1 = flow.sum_path_weights path1"
"path1 ≠ []"
using as1 flow.path_weight_conv_path flow.path0E by blast
from as obtain s2 where s2: "s2 ∈⇩A path_summary loc2 loc1"
"results_in t2 s2 ≤ t1"
using cri_less_def cri_less_eq_def by auto
then obtain path2 where path2: "flow.path loc2 loc1 path2"
"s2 = flow.sum_path_weights path2"
"path2 ≠ []"
using as1 flow.path_weight_conv_path flow.path0E by blast
with path1 have path_total: "flow.path loc1 loc1 (path1@path2)"
using flow.path_trans path2(3) by blast
then obtain s3 where s3: "s3 = flow.sum_path_weights (path1@path2)" by auto
then have s3_sum: "s3 = followed_by s1 s2"
using path1 path2 flow.sum_weights_append by auto
have "¬ t1 < results_in t1 s3"
using s3_sum s1(2) s2(2) followed_by_summary
by (metis le_less_trans less_le_not_le results_in_mono(1))
then show False using path_total no_zero_cycle s3 path1(3) path2(3) by blast
qed
lemma cri_asym2: "x <⇩p y ⟶ x ≠ y"
by (simp add: cri_less_def)
sublocale cri: order cri_less_eq cri_less
apply standard
subgoal
using cri_asym1 cri_asym2 cri_less_def by blast
subgoal for x
unfolding cri_less_eq_def
using flow.path_weight_refl results_in_zero by fastforce
subgoal
for x y z apply (cases x; cases y; cases z)
proof -
fix a b aa ba ab bb
assume as: "x ≤⇩p y" "y ≤⇩p z" "x = (a, b)" "y = (aa, ba)" "z = (ab, bb)"
then obtain s1 where s1: "s1 ∈⇩A path_summary a aa" "results_in b s1 ≤ ba"
using cri_less_eq_def by auto
from as(2,4,5) obtain s2 where s2: "s2 ∈⇩A path_summary aa ab" "results_in ba s2 ≤ bb"
using cri_less_eq_def by auto
with s1 obtain s3 where s3: "s3 ∈⇩A path_summary a ab" "s3 ≤ followed_by s1 s2"
using flow.path_weight_elem_trans by blast
with s1 s2 have "results_in b s3 ≤ bb"
proof -
have "∀s. results_in (results_in b s1) s ≤ results_in ba s"
by (meson results_in_mono(1) s1(2))
then show ?thesis
by (metis (no_types) results_in_mono(2) followed_by_summary order_trans s2(2) s3(2))
qed
with as s3 show ?thesis unfolding cri_less_eq_def by blast
qed
using cri_asym1 cri_asym2 cri_less_def by blast
lemma wf_cri: "wf {(l, l'). (l, t) <⇩p (l', t)}"
by (rule finite_acyclic_wf)
(auto intro: cri.acyclicI_order[THEN acyclic_converse[THEN iffD1]])
end
subsection‹Specification›
subsubsection‹Configuration›
record ('p::finite, 't::order, 'loc) configuration =
exchange_config :: "('p, ('loc × 't)) Exchange.configuration"
prop_config :: "'p ⇒ ('loc, 't) Propagate.configuration"
init :: "'p ⇒ bool"
type_synonym ('p, 't, 'loc) computation = "('p, 't, 'loc) configuration stream"
context dataflow_topology begin
definition the_cm where
"the_cm c loc t n = (THE c'. next_change_multiplicity' c c' loc t n)"
text‹@{term the_cm} is not commutative in general, only if the necessary conditions hold. It can be converted
to @{term apply_cm} for which we prove @{term comp_fun_commute}.›
definition apply_cm where
"apply_cm c loc t n =
(let new_pointstamps = (λloc'.
(if loc' = loc then update_zmultiset (c_pts c loc') t n
else c_pts c loc')) in
c ⦇ c_pts := new_pointstamps ⦈
⦇ c_work :=
(λloc'. c_work c loc' + frontier_changes (new_pointstamps loc') (c_pts c loc'))⦈)"
definition cm_all' where
"cm_all' c0 Δ =
Finite_Set.fold (λ(loc, t) c. apply_cm c loc t (zcount Δ (loc,t))) c0 (set_zmset Δ)"
definition cm_all where
"cm_all c0 Δ =
Finite_Set.fold (λ(loc, t) c. the_cm c loc t (zcount Δ (loc,t))) c0 (set_zmset Δ)"
definition "propagate_all c0 = while_option (λc. ∃loc. (c_work c loc) ≠ {#}⇩z)
(λc. SOME c'. ∃loc t. next_propagate' c c' loc t) c0"
subsubsection‹Initial state and state transitions›
definition InitConfig :: "('p::finite, 't::order, 'loc) configuration ⇒ bool" where
"InitConfig c =
((∀p. init c p = False)
∧ cri.init_config (exchange_config c)
∧ (∀p loc t. zcount (c_pts (prop_config c p) loc) t
= zcount (c_glob (exchange_config c) p) (loc, t))
∧ (∀w. init_config (prop_config c w)))"
definition NextPerformOp' :: "('p::finite, 't::order, 'loc) configuration ⇒ ('p, 't, 'loc) configuration
⇒ 'p ⇒ ('loc × 't) multiset ⇒ ('p × ('loc × 't)) multiset ⇒ ('loc × 't) multiset ⇒ bool" where
"NextPerformOp' c0 c1 p Δneg Δmint_msg Δmint_self = (
cri.next_performop' (exchange_config c0) (exchange_config c1) p Δneg Δmint_msg Δmint_self
∧ unchanged prop_config c0 c1
∧ unchanged init c0 c1)"
abbreviation NextPerformOp where
"NextPerformOp c0 c1 ≡ ∃p Δneg Δmint_msg Δmint_self. NextPerformOp' c0 c1 p Δneg Δmint_msg Δmint_self"
definition NextRecvCap'
:: "('p::finite, 't::order, 'loc) configuration ⇒ ('p, 't, 'loc) configuration ⇒ 'p ⇒ 'loc × 't ⇒ bool" where
"NextRecvCap' c0 c1 p t = (
cri.next_recvcap' (exchange_config c0) (exchange_config c1) p t
∧ unchanged prop_config c0 c1
∧ unchanged init c0 c1)"
abbreviation NextRecvCap where
"NextRecvCap c0 c1 ≡ ∃p t. NextRecvCap' c0 c1 p t"
definition NextSendUpd' :: "('p::finite, 't::order, 'loc) configuration ⇒ ('p, 't, 'loc) configuration
⇒ 'p ⇒ ('loc × 't) set ⇒ bool" where
"NextSendUpd' c0 c1 p tt = (
cri.next_sendupd' (exchange_config c0) (exchange_config c1) p tt
∧ unchanged prop_config c0 c1
∧ unchanged init c0 c1)"
abbreviation NextSendUpd where
"NextSendUpd c0 c1 ≡ ∃p tt. NextSendUpd' c0 c1 p tt"
definition NextRecvUpd' :: "('p::finite, 't::order, 'loc) configuration ⇒ ('p, 't, 'loc) configuration
⇒ 'p ⇒ 'p ⇒ bool" where
"NextRecvUpd' c0 c1 p q = (
init c0 q
∧ cri.next_recvupd' (exchange_config c0) (exchange_config c1) p q
∧ unchanged init c0 c1
∧ (∀p'. prop_config c1 p' =
(if p' = q
then cm_all (prop_config c0 q) (hd (c_msg (exchange_config c0) p q))
else prop_config c0 p')))"
abbreviation NextRecvUpd where
"NextRecvUpd c0 c1 ≡ ∃p q. NextRecvUpd' c0 c1 p q"
definition NextPropagate' :: "('p::finite, 't::order, 'loc) configuration ⇒ ('p, 't, 'loc) configuration
⇒ 'p ⇒ bool" where
"NextPropagate' c0 c1 p = (
unchanged exchange_config c0 c1
∧ init c1 = (init c0)(p := True)
∧ (∀p'. Some (prop_config c1 p') =
(if p' = p
then propagate_all (prop_config c0 p')
else Some (prop_config c0 p'))))"
abbreviation NextPropagate where
"NextPropagate c0 c1 ≡ ∃p. NextPropagate' c0 c1 p"
definition "Next'" where
"Next' c0 c1 = (NextPerformOp c0 c1 ∨ NextSendUpd c0 c1 ∨ NextRecvUpd c0 c1 ∨ NextPropagate c0 c1 ∨ NextRecvCap c0 c1 ∨ c1 = c0)"
abbreviation "Next" where
"Next s ≡ Next' (shd s) (shd (stl s))"
definition FullSpec :: "('p :: finite, 't :: order, 'loc) computation ⇒ bool" where
"FullSpec s = (holds InitConfig s ∧ alw Next s)"
lemma NextPerformOpD:
assumes "NextPerformOp' c0 c1 p Δneg Δmint_msg Δmint_self"
shows
"cri.next_performop' (exchange_config c0) (exchange_config c1) p Δneg Δmint_msg Δmint_self"
"unchanged prop_config c0 c1"
"unchanged init c0 c1"
using assms unfolding NextPerformOp'_def by simp_all
lemma NextSendUpdD:
assumes "NextSendUpd' c0 c1 p tt"
shows
"cri.next_sendupd' (exchange_config c0) (exchange_config c1) p tt"
"unchanged prop_config c0 c1"
"unchanged init c0 c1"
using assms unfolding NextSendUpd'_def by simp_all
lemma NextRecvUpdD:
assumes "NextRecvUpd' c0 c1 p q"
shows
"init c0 q"
"cri.next_recvupd' (exchange_config c0) (exchange_config c1) p q"
"unchanged init c0 c1"
"(∀p'. prop_config c1 p' =
(if p' = q
then cm_all (prop_config c0 q) (hd (c_msg (exchange_config c0) p q))
else prop_config c0 p'))"
using assms unfolding NextRecvUpd'_def by simp_all
lemma NextPropagateD:
assumes "NextPropagate' c0 c1 p"
shows
"unchanged exchange_config c0 c1"
"init c1 = (init c0)(p := True)"
"(∀p'. Some (prop_config c1 p') =
(if p' = p
then propagate_all (prop_config c0 p')
else Some (prop_config c0 p')))"
using assms unfolding NextPropagate'_def by simp_all
lemma NextRecvCapD:
assumes "NextRecvCap' c0 c1 p t"
shows
"cri.next_recvcap' (exchange_config c0) (exchange_config c1) p t"
"unchanged prop_config c0 c1"
"unchanged init c0 c1"
using assms unfolding NextRecvCap'_def by simp_all
subsection‹Auxiliary Lemmas›
subsubsection‹Auxiliary Lemmas for CM Conversion›
lemma apply_cm_is_cm:
"∃t'. t' ∈⇩A frontier (c_imp c loc) ∧ t' ≤ t ⟹ n ≠ 0 ⟹ next_change_multiplicity' c (apply_cm c loc t n) loc t n"
by (auto simp: next_change_multiplicity'_def apply_cm_def
intro!: Propagate.configuration.equality)
lemma update_zmultiset_commute:
"update_zmultiset (update_zmultiset M t' n') t n = update_zmultiset (update_zmultiset M t n) t' n'"
by transfer (auto simp: equiv_zmset_def split: if_splits)
lemma apply_cm_commute: "apply_cm (apply_cm c loc t n) loc' t' n' = apply_cm (apply_cm c loc' t' n') loc t n"
unfolding apply_cm_def Let_def
by (auto intro!: Propagate.configuration.equality simp: update_zmultiset_commute)
lemma comp_fun_commute_apply_cm[simp]: "comp_fun_commute (λ(loc, t) c. apply_cm c loc t (f loc t))"
by (auto intro!: Propagate.configuration.equality simp: update_zmultiset_commute comp_fun_commute_def o_def apply_cm_commute)
lemma ex_cm_imp_conds:
assumes "∃c'. next_change_multiplicity' c c' loc t n"
shows "∃t'. t' ∈⇩A frontier (c_imp c loc) ∧ t' ≤ t" "n ≠ 0"
using assms by (auto simp: next_change_multiplicity'_def)
lemma the_cm_eq_apply_cm:
assumes "∃c'. next_change_multiplicity' c c' loc t n"
shows "the_cm c loc t n = apply_cm c loc t n"
proof -
from assms have cond: "∃t'. t' ∈⇩A frontier (c_imp c loc) ∧ t' ≤ t" "n ≠ 0"
using ex_cm_imp_conds by blast+
show ?thesis
unfolding the_cm_def
apply (rule the1_equality)
apply (rule next_change_multiplicity'_unique[OF cond(2,1)])
unfolding apply_cm_def next_change_multiplicity'_def
using cond apply (auto intro!: Propagate.configuration.equality)
done
qed
lemma apply_cm_preserves_cond:
assumes "∀(loc,t)∈set_zmset Δ. ∃t'. t' ∈⇩A frontier (c_imp c0 loc) ∧ t' ≤ t"
shows "∀(loc,t)∈set_zmset Δ. ∃t'. t' ∈⇩A frontier (c_imp (apply_cm c0 loc' t'' n) loc) ∧ t' ≤ t"
using assms by (auto simp: apply_cm_def)
lemma cm_all_eq_cm_all':
assumes "∀(loc,t)∈set_zmset Δ. ∃t'. t' ∈⇩A frontier (c_imp c0 loc) ∧ t' ≤ t"
shows "cm_all c0 Δ = cm_all' c0 Δ"
unfolding cm_all_def cm_all'_def
apply (rule fold_closed_eq[where B = "{c. ∀(loc,t)∈set_zmset Δ. ∃t'. t' ∈⇩A frontier (c_imp c loc) ∧ t' ≤ t}"])
subgoal for a Δ
apply (cases a)
apply simp
apply (rule the_cm_eq_apply_cm)
apply (rule ex1_implies_ex)
apply (rule next_change_multiplicity'_unique)
apply auto
done
subgoal for a Δ
apply (cases a)
apply simp
apply (rule apply_cm_preserves_cond)
apply auto
done
subgoal
using assms by simp
done
lemma cm_eq_the_cm:
assumes "next_change_multiplicity' c c' loc t n"
shows "the_cm c loc t n = c'"
proof -
from assms have cond: "∃u. u ∈⇩A frontier (c_imp c loc) ∧ u ≤ t" "n ≠ 0"
unfolding next_change_multiplicity'_def by auto
then show ?thesis
using next_change_multiplicity'_unique[OF cond(2,1)] assms the_cm_def
by auto
qed
lemma zcount_ps_apply_cm:
"zcount (c_pts (apply_cm c loc t n) loc') t' = zcount (c_pts c loc') t' + (if loc = loc' ∧ t = t' then n else 0)"
by (auto simp: apply_cm_def zcount_update_zmultiset)
lemma zcount_pointstamps_update: "zcount (c_pts (c⦇c_pts:=M⦈) loc) x = zcount (M loc) x"
by auto
lemma nop: "loc1 ≠ loc2 ∨ t1 ≠ t2 ⟶
zcount (c_pts (apply_cm c loc2 t2 (zcount Δ (loc2, t2))) loc1) t1 =
zcount (c_pts c loc1) t1"
apply (simp add: apply_cm_def)
using zcount_update_zmultiset
by (simp add: zcount_update_zmultiset)
lemma fold_nop:
"zcount (c_pts (Finite_Set.fold (λ(loc', t') c. apply_cm c loc' t' (zcount Δ' (loc', t'))) c
(set_zmset Δ - {(loc, t)})) loc) t
= zcount (c_pts c loc) t"
proof -
have "finite (set_zmset Δ- {(loc, t)})" using finite_set_zmset by blast
then show ?thesis
proof (induct "set_zmset Δ - {(loc, t)}" arbitrary: Δ rule: finite_induct)
case empty
then show ?case using fold_empty by auto
next
let ?f = "(λ(loc', t') c. apply_cm c loc' t' (zcount Δ' (loc',t')))"
case (insert x F)
obtain loc' t' where x_pair: "x = (loc', t')" by (meson surj_pair)
from insert have nonmember: "x ≠ (loc, t)" by auto
then have finite_s: "finite F" using insert by auto
interpret commute: comp_fun_commute ?f
by (simp add: comp_fun_commute_def comp_def apply_cm_commute)
from finite_s have step1:
"Finite_Set.fold ?f c (insert x F) = ?f x (Finite_Set.fold ?f c F)"
by (metis (mono_tags, lifting) commute.fold_insert insert.hyps(1) insert.hyps(2))
from nonmember have step2:
"zcount (c_pts (?f x (Finite_Set.fold ?f c F)) loc) t
= zcount (c_pts (Finite_Set.fold ?f c F) loc) t"
using x_pair
by (metis (mono_tags, lifting) case_prod_conv nop)
with step1 and x_pair have final:
"zcount (c_pts (Finite_Set.fold ?f c (insert x F)) loc) t
= zcount (c_pts (Finite_Set.fold ?f c F) loc) t"
by simp
from insert(2,4) obtain Δ2 where Δ2: "Δ2 = filter_zmset (λy. y≠x) Δ" by blast
then have "F = set_zmset Δ2 - {(loc, t)}"
proof -
from Δ2 have *: "x ∉#⇩z Δ2" by (simp add: not_in_iff_zmset)
from insert(4) and nonmember have **: "x ∈#⇩z Δ" by blast
from Δ2 ** have ***: "∀y. y ∈#⇩z Δ ⟷ (y ∈#⇩z Δ2 ∨ y = x)"
by (metis (mono_tags, lifting) count_filter_zmset zcount_ne_zero_iff)
with *** have "∀y. (y ∈ set_zmset Δ = (y ∈ (set_zmset Δ2 ∪ {x})))" by blast
then have "set_zmset Δ = set_zmset Δ2 ∪ {x}" by (auto simp add: set_eq_iff)
with insert(2,3,4) * show ?thesis
by (metis (mono_tags, lifting) Diff_insert Diff_insert2 Diff_insert_absorb Un_empty_right Un_insert_right)
qed
with final insert show ?case by metis
qed
qed
lemma zcount_pointstamps_cm_all':
"zcount (c_pts (cm_all' c Δ) loc) x
= zcount (c_pts c loc) x + zcount Δ (loc,x)"
proof -
let ?f = "(λ(loc', t') c. apply_cm c loc' t' (zcount Δ (loc',t')))"
have ?thesis
proof (cases "zcount Δ (loc,x) = 0")
case case_nonmember: True
then have set_zmsetΔ: "set_zmset Δ - {(loc, x)} = set_zmset Δ" using zcount_eq_zero_iff by fastforce
have "zcount (c_pts (cm_all' c Δ) loc) x
= zcount (c_pts c loc) x"
unfolding cm_all'_def
apply (subst set_zmsetΔ[symmetric])
apply (simp add: fold_nop)
done
with case_nonmember show ?thesis by auto
next
case case_member: False
then have fold_rec: "Finite_Set.fold ?f c (set_zmset Δ)
= ?f (loc, x) (Finite_Set.fold ?f c (set_zmset Δ - {(loc, x)}))"
proof -
interpret commute: comp_fun_commute "(λ(loc, t) c. apply_cm c loc t (f loc t))" for f
by (fact comp_fun_commute_apply_cm)
have "(loc, x) ∈#⇩z Δ"
by (meson case_member zcount_inI)
then show ?thesis
by (intro commute.fold_rec) simp_all
qed
have "zcount (c_pts (Finite_Set.fold ?f c (set_zmset Δ - {(loc, x)})) loc) x
= zcount (c_pts c loc) x" by (simp add: fold_nop)
then have "zcount (c_pts (Finite_Set.fold ?f c (set_zmset Δ)) loc) x
= zcount (c_pts (?f (loc, x) c) loc) x"
using fold_nop fold_rec by (simp add: zcount_ps_apply_cm)
then show ?thesis
by (simp add: zcount_ps_apply_cm cm_all'_def)
qed
then show ?thesis ..
qed
lemma implications_apply_cm[simp]: "c_imp (apply_cm c loc t n) = c_imp c"
by (auto simp: apply_cm_def)
lemma implications_cm_all[simp]:
"c_imp (cm_all' c Δ) = c_imp c"
unfolding cm_all'_def Let_def
apply (rule fold_invar[OF finite_set_zmset])
apply auto
done
lemma lift_cm_inv_cm_all':
assumes "(⋀c0 c1 loc t n. P c0 ⟹ next_change_multiplicity' c0 c1 loc t n ⟹ P c1)"
and "∀(loc,t)∈#⇩zΔ. ∃t'. t' ∈⇩A frontier (c_imp c0 loc) ∧ t' ≤ t"
and "P c0"
shows "P (cm_all' c0 Δ)"
proof -
let ?cond_invar = "λc. ∀(loc, t)∈#⇩zΔ. ∃t'. t' ∈⇩A frontier (c_imp c loc) ∧ t' ≤ t"
let ?invar = "λc. ?cond_invar c ∧ P c"
show ?thesis
unfolding cm_all'_def
apply (rule conjunct2[OF fold_invar[OF finite_set_zmset, of ?invar]])
using assms(2,3) apply simp
subgoal
apply safe
apply auto []
apply (rule assms(1))
apply simp
apply (rule apply_cm_is_cm)
apply auto
done
apply simp
done
qed
lemma lift_cm_inv_cm_all:
assumes "⋀c0 c1 loc t n. P c0 ⟹ next_change_multiplicity' c0 c1 loc t n ⟹ P c1"
and "∀(loc,t)∈#⇩zΔ. ∃t'. t' ∈⇩A frontier (c_imp c0 loc) ∧ t' ≤ t"
and "P c0"
shows "P (cm_all c0 Δ)"
apply (subst cm_all_eq_cm_all')
using assms(2) apply simp
using assms apply (rule lift_cm_inv_cm_all')
apply simp_all
done
lemma obtain_min_worklist:
assumes "(a (loc'::(_ :: finite))::(('t :: order) zmultiset)) ≠ {#}⇩z"
obtains loc t
where "t ∈#⇩z a loc"
and "∀t' loc'. t' ∈#⇩z a loc' ⟶ ¬ t' < t"
using assms
proof atomize_elim
obtain f where f: "f = minimal_antichain (⋃loc'. set_zmset (a loc'))"
by blast
from assms obtain x' where x': "x' ∈ (⋃loc'. set_zmset (a loc'))"
using pos_zcount_in_zmset by fastforce
from assms have "finite (⋃loc'. set_zmset (a loc'))"
using finite_UNIV by blast
with x' have "f ≠ {}" unfolding f
using minimal_antichain_nonempty by blast
then obtain t where t: "t ∈ f" "(∀s∈f. ¬ s < t)"
using ex_min_if_finite f minimal_antichain_def by fastforce
with f have thesis1: "∀t' loc'. t' ∈#⇩z a loc' ⟶ ¬ t' < t" "∃loc. t ∈#⇩z a loc"
by (simp add: minimal_antichain_def)+
then show "∃t loc. t ∈#⇩z a loc ∧ (∀t' loc'. t' ∈#⇩z a loc' ⟶ ¬ t' < t)" by blast
qed
lemma propagate_pointstamps_eq:
assumes "c_work c loc ≠ {#}⇩z"
shows "c_pts c = c_pts (SOME c'. ∃loc t. next_propagate' c c' loc t)"
proof -
from assms obtain loc' t where loc't: "t ∈#⇩z c_work c loc'"
"∀t' loc'. t' ∈#⇩z c_work c loc' ⟶ ¬ t' < t"
apply (rule obtain_min_worklist[of "c_work c" "loc"]) by blast
let ?imps = "λlocX. if locX = loc' then c_imp c locX + {#t' ∈#⇩z c_work c locX. t' = t#}
else c_imp c locX"
let ?wl = "λlocX. if locX = loc' then {#t' ∈#⇩z c_work c locX. t' ≠ t#}
else c_work c locX
+ after_summary
(frontier_changes (?imps loc') (c_imp c loc'))
(summary loc' locX)"
let ?c = "c⦇c_imp := ?imps, c_work := ?wl⦈"
from loc't assms have propagate: "∃c'. ∃loc t. next_propagate' c c' loc t"
by (intro exI[of _ ?c] exI[of _ loc'] exI[of _ t])
(auto simp add: next_propagate'_def intro!: Propagate.configuration.equality)
{ fix c' loc t
assume "next_propagate' c c' loc t"
then have "c_pts c = c_pts c'"
by (simp add: next_propagate'_def)
}
with propagate show ?thesis
by (simp add: verit_sko_ex')
qed
lemma propagate_all_imp_InvGlobPointstampsEq:
"Some c1 = propagate_all c0 ⟹ c_pts c0 = c_pts c1"
unfolding propagate_all_def
using while_option_rule[where P="(λc. c_pts c0 = c_pts c)"
and b="(λc. ∃loc. c_work c loc ≠ {#}⇩z)"
and c="(λc. SOME c'. ∃loc t. next_propagate' c c' loc t)"]
propagate_pointstamps_eq by (metis (no_types, lifting))
lemma exists_next_propagate':
assumes "c_work c loc ≠ {#}⇩z"
shows "∃c' loc t. next_propagate' c c' loc t"
proof -
from assms obtain loc' t where loc't:
"t ∈#⇩z c_work c loc'"
"∀t' loc'. t' ∈#⇩z c_work c loc' ⟶ ¬ t' < t"
by (rule obtain_min_worklist)
let ?imps = "λlocX. if locX = loc' then c_imp c locX + {#t' ∈#⇩z c_work c locX. t' = t#}
else c_imp c locX"
let ?wl = "λlocX. if locX = loc' then {#t' ∈#⇩z c_work c locX. t' ≠ t#}
else c_work c locX
+ after_summary
(frontier_changes (?imps loc') (c_imp c loc'))
(summary loc' locX)"
let ?c = "c⦇c_imp := ?imps, c_work := ?wl⦈"
from loc't assms show ?thesis
by (intro exI[of _ ?c] exI[of _ loc'] exI[of _ t])
(auto simp: next_propagate'_def intro!: Propagate.configuration.equality)
qed
lemma lift_propagate_inv_propagate_all:
assumes "(⋀c0 c1 loc t. P c0 ⟹ next_propagate' c0 c1 loc t ⟹ P c1)"
and "P c0"
and "propagate_all c0 = Some c1"
shows "P c1"
apply (rule while_option_rule[of P _, rotated, OF assms(3)[unfolded propagate_all_def], OF assms(2)])
apply clarify
subgoal for c loc
apply (drule exists_next_propagate')
apply (simp add: assms(1) verit_sko_ex')
done
done
subsection‹Exchange is a Subsystem of Tracker›
text‹Steps in the Tracker are valid steps in the Exchange protocol.›
lemma next_imp_exchange_next:
"Next' c0 c1 ⟹ cri.next' (exchange_config c0) (exchange_config c1)"
unfolding Next'_def cri.next'_def NextPerformOp'_def NextRecvUpd'_def NextSendUpd'_def NextPropagate'_def NextRecvCap'_def
by auto
lemma alw_next_imp_exchange_next: "alw Next s ⟹ alw cri.next (smap exchange_config s)"
by (coinduction arbitrary: s rule: alw.coinduct) (auto dest: alwD next_imp_exchange_next)
text‹Any Tracker trace is a valid Exchange trace›
lemma spec_imp_exchange_spec: "FullSpec s ⟹ cri.spec (smap exchange_config s)"
unfolding cri.spec_def FullSpec_def
by (auto simp: InitConfig_def intro: alw_next_imp_exchange_next)
lemma lift_exchange_invariant:
assumes "⋀s. cri.spec s ⟹ alw (holds P) s"
shows "FullSpec s ⟹ alw (λs. P (exchange_config (shd s))) s"
proof -
assume "FullSpec s"
note spec_imp_exchange_spec[OF this]
note assms[OF this]
then show ?thesis
by (auto simp: alw_holds_smap_conv_comp)
qed
text‹Lifted Exchange invariants›
lemmas
exch_alw_InvCapsNonneg = lift_exchange_invariant[OF cri.alw_InvCapsNonneg, unfolded atomize_imp, simplified, folded atomize_imp] and
exch_alw_InvRecordCount = lift_exchange_invariant[OF cri.alw_InvRecordCount, simplified atomize_imp, simplified, folded atomize_imp] and
exch_alw_InvRecordsNonneg = lift_exchange_invariant[OF cri.alw_InvRecordsNonneg, simplified atomize_imp, simplified, folded atomize_imp] and
exch_alw_InvGlobVacantImpRecordsVacant = lift_exchange_invariant[OF cri.alw_InvGlobVacantImpRecordsVacant, simplified atomize_imp, simplified, folded atomize_imp] and
exch_alw_InvGlobNonposImpRecordsNonpos = lift_exchange_invariant[OF cri.alw_InvGlobNonposImpRecordsNonpos, simplified atomize_imp, simplified, folded atomize_imp] and
exch_alw_InvJustifiedGII = lift_exchange_invariant[OF cri.alw_InvJustifiedGII, simplified atomize_imp, simplified, folded atomize_imp] and
exch_alw_InvJustifiedII = lift_exchange_invariant[OF cri.alw_InvJustifiedII, simplified atomize_imp, simplified, folded atomize_imp] and
exch_alw_InvGlobNonposEqVacant = lift_exchange_invariant[OF cri.alw_InvGlobNonposEqVacant, simplified atomize_imp, simplified, folded atomize_imp] and
exch_alw_InvMsgInGlob = lift_exchange_invariant[OF cri.alw_InvMsgInGlob, simplified atomize_imp, simplified, folded atomize_imp] and
exch_alw_InvTempJustified = lift_exchange_invariant[OF cri.alw_InvTempJustified, simplified atomize_imp, simplified, folded atomize_imp]
subsection‹Definitions›
definition safe_combined :: "('p::finite, 't::order, 'loc) configuration ⇒ bool" where
"safe_combined c ≡ ∀loc1 loc2 t s p.
zcount (cri.records (exchange_config c)) (loc1, t) > 0 ∧ s ∈⇩A path_summary loc1 loc2 ∧ init c p
⟶ (∃t'. t' ∈⇩A frontier (c_imp (prop_config c p) loc2) ∧ t' ≤ results_in t s)"
definition safe_combined2 :: "('p::finite, 't::order, 'loc) configuration ⇒ bool" where
"safe_combined2 c ≡ ∀loc1 loc2 t s p1 p2.
zcount (c_caps (exchange_config c) p1) (loc1, t) > 0 ∧ s ∈⇩A path_summary loc1 loc2 ∧ init c p2
⟶ (∃t'. t' ∈⇩A frontier (c_imp (prop_config c p2) loc2) ∧ t' ≤ results_in t s)"
definition InvGlobPointstampsEq :: "('p :: finite, 't :: order, 'loc) configuration ⇒ bool" where
"InvGlobPointstampsEq c = (
(∀p loc t. zcount (c_pts (prop_config c p) loc) t
= zcount (c_glob (exchange_config c) p) (loc, t)))"
lemma safe_combined_implies_safe_combined2:
assumes "cri.InvCapsNonneg (exchange_config c)"
and "safe_combined c"
shows "safe_combined2 c"
unfolding safe_combined2_def
apply clarify
subgoal for loc1 loc2 t s p1 p2
apply (rule assms(2)[unfolded safe_combined_def, rule_format, of loc1 t s loc2 p2])
apply (simp add: cri.records_def)
apply (rule add_pos_nonneg)
apply (subst zcount_sum)
apply (rule sum_pos[where y = p1])
using assms(1)
apply (simp_all add: cri.InvCapsNonneg_def)
done
done
subsection‹Propagate is a Subsystem of Tracker›
subsubsection‹CM Conditions›
definition InvMsgCMConditions where
"InvMsgCMConditions c = (∀p q.
init c q ⟶ c_msg (exchange_config c) p q ≠ [] ⟶
(∀(loc,t) ∈#⇩z (hd (c_msg (exchange_config c) p q)). ∃t'. t' ∈⇩A frontier (c_imp (prop_config c q) loc) ∧ t' ≤ t))"
text‹Pointstamps in incoming messages all satisfy the CM premise, which is required during NextRecvUpd' steps.›
lemma msg_is_cm_safe:
fixes c :: "('p::finite, 't::order, 'loc) configuration"
assumes "safe (prop_config c q)"
and "InvGlobPointstampsEq c"
and "cri.InvMsgInGlob (exchange_config c)"
and "c_msg (exchange_config c) p q ≠ []"
shows "∀(loc,t) ∈#⇩z (hd (c_msg (exchange_config c) p q)). ∃t'. t' ∈⇩A frontier (c_imp (prop_config c q) loc) ∧ t' ≤ t"
using assms(3)[unfolded cri.InvMsgInGlob_def, rule_format, OF assms(4)] assms(1)[unfolded safe_def, rule_format]
apply (clarsimp simp: cri_less_eq_def assms(2)[unfolded InvGlobPointstampsEq_def, rule_format, symmetric])
using order_trans apply blast
done
subsubsection‹Propagate Safety and InvGlobPointstampsEq›
text‹To be able to use the @{thm[source] msg_is_cm_safe} lemma at all times and show that Propagate is a
subsystem we need to prove that the specification implies Propagate's safe and the
InvGlobPointstampsEq. Both of these depend on the CM conditions being satisfied during the
NextRecvUpd' step and the safety proof additionally depends on other Propagate invariants, which
means that we need to prove all of these jointly.›
abbreviation prop_invs where
"prop_invs c ≡ inv_implications_nonneg c ∧ inv_imps_work_sum c"
abbreviation prop_safe where
"prop_safe c ≡ impl_safe c ∧ safe c"
definition inv_init_imp_prop_safe where
"inv_init_imp_prop_safe c = (∀p. init c p ⟶ prop_safe (prop_config c p))"
lemma NextRecvUpd'_preserves_prop_safe:
assumes "prop_safe (prop_config c0 q)"
and "InvGlobPointstampsEq c0"
and "cri.InvMsgInGlob (exchange_config c0)"
and "NextRecvUpd' c0 c1 p q"
shows "prop_safe (prop_config c1 q)"
proof -
have safe: "safe (prop_config c0 q)"
using assms(1) by blast
note recvupd_change = cri.next_recvupdD(1)[OF NextRecvUpdD(2)[OF assms(4)]]
note cm_conds = msg_is_cm_safe[OF safe assms(2,3) recvupd_change]
have safes:
"prop_safe c0 ⟹ next_change_multiplicity' c0 c1 loc t n ⟹ prop_safe c1" for c0 c1 loc t n
using
cm_preserves_safe
cm_preserves_impl_safe
by auto
show "prop_safe (prop_config c1 q)"
using
lift_cm_inv_cm_all[rotated, OF cm_conds, of prop_safe, OF assms(1)]
safes
NextRecvUpdD(4)[OF assms(4)]
by metis
qed
lemma NextRecvUpd'_preserves_InvGlobPointstampsEq:
assumes "impl_safe (prop_config c0 q) ∧ safe (prop_config c0 q)"
and "InvGlobPointstampsEq c0"
and "cri.InvMsgInGlob (exchange_config c0)"
and "NextRecvUpd' c0 c1 p q"
shows "InvGlobPointstampsEq c1"
proof -
have safe: "safe (prop_config c0 q)"
using assms(1) by blast
note recvupd_change = cri.next_recvupdD(1)[OF NextRecvUpdD(2)[OF assms(4)]]
note cm_conds = msg_is_cm_safe[OF safe assms(2,3) recvupd_change]
show "InvGlobPointstampsEq c1"
using
assms(2,4)
cm_conds
unfolding NextRecvUpd'_def cri.next_recvupd'_def Let_def InvGlobPointstampsEq_def
by (clarsimp simp: zcount_pointstamps_cm_all' cm_all_eq_cm_all')+
qed
lemma NextPropagate'_causes_safe:
assumes "NextPropagate' c0 c1 p"
and "inv_imps_work_sum (prop_config c1 p)"
and "inv_implications_nonneg (prop_config c1 p)"
shows "safe (prop_config c1 p)" "impl_safe (prop_config c1 p)"
proof -
from assms(1) have "Some (prop_config c1 p) = propagate_all (prop_config c0 p)"
by (simp add: NextPropagate'_def)
then have wl: "c_work (prop_config c1 p) loc = {#}⇩z" for loc
unfolding propagate_all_def
by (subst (asm) eq_commute) (auto dest: while_option_stop)
show "safe (prop_config c1 p)" "impl_safe (prop_config c1 p)"
by (rule safe[OF assms(2,3) wl]) (rule impl_safe[OF assms(2,3) wl])
qed
lemma NextPropagate'_preserves_safe:
assumes "NextPropagate' c0 c1 q"
and "inv_imps_work_sum (prop_config c1 p)"
and "inv_implications_nonneg (prop_config c1 p)"
and "safe (prop_config c0 p)"
shows "safe (prop_config c1 p)"
apply (cases "p=q")
subgoal
using assms(1-3) by (auto intro: NextPropagate'_causes_safe)
subgoal
using assms(1,4) by (auto dest: spec[of _ p] simp: NextPropagate'_def)
done
lemma NextPropagate'_preserves_impl_safe:
assumes "NextPropagate' c0 c1 q"
and "inv_imps_work_sum (prop_config c1 p)"
and "inv_implications_nonneg (prop_config c1 p)"
and "impl_safe (prop_config c0 p)"
shows "impl_safe (prop_config c1 p)"
apply (cases "p=q")
subgoal
using assms(1-3) by (auto intro: NextPropagate'_causes_safe)
subgoal
using assms(1,4) by (auto dest: spec[of _ p] simp: NextPropagate'_def)
done
lemma NextRecvUpd'_preserves_inv_init_imp_prop_safe:
assumes "cri.InvMsgInGlob (exchange_config c0)"
and "inv_init_imp_prop_safe c0"
and "InvGlobPointstampsEq c0"
and "NextRecvUpd' c0 c1 p q"
shows "inv_init_imp_prop_safe c1"
using assms(2) unfolding inv_init_imp_prop_safe_def
apply clarify
subgoal for p
apply (cases "p=q")
subgoal
apply (drule spec[of _p])
apply (simp add: NextRecvUpdD(1)[OF assms(4)])
apply (drule NextRecvUpd'_preserves_prop_safe[OF _ assms(3,1,4)])
apply simp
done
subgoal
using NextRecvUpdD(3,4)[OF assms(4)] by fastforce
done
done
lemma NextRecvUpd'_preserves_prop_invs:
assumes "cri.InvMsgInGlob (exchange_config c0)"
and "inv_init_imp_prop_safe c0"
and "∀p. prop_invs (prop_config c0 p)"
and "InvGlobPointstampsEq c0"
and "NextRecvUpd' c0 c1 p q"
shows "∀p. prop_invs (prop_config c1 p)"
proof -
have safe: "safe (prop_config c0 q)"
using NextRecvUpdD(1) assms(2,5) inv_init_imp_prop_safe_def by blast
note recvupd_change = cri.next_recvupdD(1)[OF NextRecvUpdD(2)[OF assms(5)]]
note cm_conds = msg_is_cm_safe[OF safe assms(4,1) recvupd_change]
have invs:
"prop_invs c0 ⟹ next_change_multiplicity' c0 c1 loc t n ⟹ prop_invs c1" for c0 c1 loc t n
using
cm_preserves_inv_imps_work_sum
cm_preserves_inv_implications_nonneg
by auto
show "∀q. prop_invs (prop_config c1 q)"
apply rule
subgoal for q'
apply (cases "q'=q")
subgoal
using
lift_cm_inv_cm_all[rotated, OF cm_conds, of prop_invs, OF assms(3)[rule_format]]
invs
NextRecvUpdD(4)[OF assms(5)]
by metis
subgoal
using NextRecvUpdD(4) assms(3) assms(5) by fastforce
done
done
qed
lemma NextPropagate'_preserves_prop_invs:
assumes "prop_invs (prop_config c0 q)"
and "NextPropagate' c0 c1 p"
shows "prop_invs (prop_config c1 q)"
apply (cases "p=q")
subgoal
using
assms(1)
lift_propagate_inv_propagate_all[
of prop_invs,
rotated 2,
OF NextPropagateD(3)[OF assms(2), rule_format, of p, simplified, symmetric]]
by (simp add: iiws_imp_iipwn p_preserves_inv_implications_nonneg p_preserves_inv_imps_work_sum)
subgoal
by (metis NextPropagateD(3) assms(1) assms(2) option.simps(1))
done
lemma NextPropagate'_preserves_inv_init_imp_prop_safe:
assumes "prop_invs (prop_config c0 p)"
and "inv_init_imp_prop_safe c0"
and "NextPropagate' c0 c1 p"
shows "inv_init_imp_prop_safe c1"
using assms(2) unfolding inv_init_imp_prop_safe_def
apply clarsimp
subgoal for p'
apply (cases "p'=p")
subgoal
using NextPropagate'_preserves_prop_invs[OF assms(1,3)]
using NextPropagate'_causes_safe(1,2)[OF assms(3)] by blast
subgoal
using NextPropagateD(2,3)[OF assms(3)]
by (auto dest: spec[of _ p'])
done
done
lemma Next'_preserves_invs:
assumes "cri.InvMsgInGlob (exchange_config c0)"
and "inv_init_imp_prop_safe c0"
and "InvGlobPointstampsEq c0"
and "Next' c0 c1"
and "∀p. prop_invs (prop_config c0 p)"
shows
"inv_init_imp_prop_safe c1"
"∀p. prop_invs (prop_config c1 p)"
"InvGlobPointstampsEq c1"
subgoal
using assms(4) unfolding Next'_def
using assms(2)
apply (elim disjE)
subgoal
unfolding inv_init_imp_prop_safe_def
using NextPerformOpD(2,3) by fastforce
subgoal
unfolding inv_init_imp_prop_safe_def
using NextSendUpdD(2,3) by fastforce
subgoal
using NextRecvUpd'_preserves_inv_init_imp_prop_safe[OF assms(1,2,3)]
by blast
subgoal
using NextPropagate'_preserves_inv_init_imp_prop_safe assms(5) by blast
subgoal
unfolding inv_init_imp_prop_safe_def
using NextRecvCapD(2,3) by fastforce
subgoal by simp
done
subgoal
using assms(4) unfolding Next'_def
using assms(5)
apply (elim disjE)
subgoal
using NextPerformOpD(2) by fastforce
subgoal
using NextSendUpdD(2) by fastforce
subgoal
using assms(1,2,3) NextRecvUpd'_preserves_prop_invs by blast
subgoal
using NextPropagate'_preserves_prop_invs by blast
subgoal
unfolding inv_init_imp_prop_safe_def
using NextRecvCapD(2,3) by fastforce
subgoal by simp
done
subgoal
using assms(4) unfolding Next'_def
using assms(3)
apply (elim disjE)
subgoal
by (metis InvGlobPointstampsEq_def NextPerformOpD(1,2) cri.next_performopD(7))
subgoal
by (metis InvGlobPointstampsEq_def NextSendUpdD(1,2) cri.next_sendupdD(5))
subgoal
using NextRecvUpdD(1) NextRecvUpd'_preserves_InvGlobPointstampsEq assms(1,2) inv_init_imp_prop_safe_def by blast
subgoal
unfolding NextPropagate'_def InvGlobPointstampsEq_def
using propagate_all_imp_InvGlobPointstampsEq
by (metis option.inject)
subgoal
by (metis InvGlobPointstampsEq_def NextRecvCapD(1) NextRecvCapD(2) cri.next_recvcapD(4))
subgoal by simp
done
done
lemma init_imp_InvGlobPointstampsEq: "InitConfig c ⟹ InvGlobPointstampsEq c"
by (simp add: InitConfig_def cri.init_config_def InvGlobPointstampsEq_def)
lemma init_imp_inv_init_imp_prop_safe: "InitConfig c ⟹ inv_init_imp_prop_safe c"
by (simp add: inv_init_imp_prop_safe_def InitConfig_def)
lemma init_imp_prop_invs: "InitConfig c ⟹ ∀p. prop_invs (prop_config c p)"
by (simp add: InitConfig_def init_imp_inv_implications_nonneg init_imp_inv_imps_work_sum)
abbreviation all_invs where
"all_invs c ≡ InvGlobPointstampsEq c ∧ inv_init_imp_prop_safe c ∧ (∀p. prop_invs (prop_config c p))"
lemma alw_Next'_alw_invs:
assumes "holds all_invs s"
and "alw (holds (λc. cri.InvMsgInGlob (exchange_config c))) s"
and "alw Next s"
shows "alw (holds all_invs) s"
using assms
apply (coinduction arbitrary: s)
apply clarsimp
apply safe
apply (metis (mono_tags, lifting) alw_holds2 Next'_preserves_invs(3) alwD)
apply (metis (mono_tags, lifting) alw_holds2 Next'_preserves_invs(1) alwD)
apply (metis (mono_tags, lifting) alw_holds2 Next'_preserves_invs(2) alwD)
apply (metis (mono_tags, lifting) alw_holds2 Next'_preserves_invs(2) alwD)
apply auto
done
lemma alw_invs: "FullSpec s ⟹ alw (holds all_invs) s"
apply (frule exch_alw_InvMsgInGlob)
unfolding FullSpec_def
apply clarsimp
apply (frule init_imp_InvGlobPointstampsEq)
apply (frule init_imp_inv_init_imp_prop_safe)
apply (drule init_imp_prop_invs)
by (simp add: alw_Next'_alw_invs alw_mono)
lemma alw_InvGlobPointstampsEq: "FullSpec s ⟹ alw (holds InvGlobPointstampsEq) s"
using alw_invs alw_mono holds_mono by blast
lemma alw_inv_init_imp_prop_safe: "FullSpec s ⟹ alw (holds inv_init_imp_prop_safe) s"
using alw_invs alw_mono holds_mono by blast
lemma alw_holds_conv_shd: "alw (holds φ) s = alw (λs. φ (shd s)) s"
by (simp add: alw_iff_sdrop)
lemma alw_prop_invs: "FullSpec s ⟹ alw (holds (λc. ∀p. prop_invs (prop_config c p))) s"
by (auto
intro: alw_mono[of "holds all_invs" s "holds (λc. ∀p. prop_invs (prop_config c p))"]
dest: alw_invs)
lemma nrec_pts_delayed:
assumes "cri.InvGlobNonposImpRecordsNonpos (exchange_config c)"
and "zcount (cri.records (exchange_config c)) x > 0"
shows "∃x'. x' ≤⇩p x ∧ zcount (c_glob (exchange_config c) p) x' > 0"
proof -
from assms have r: "∀p. ¬ cri.nonpos_upto (c_glob (exchange_config c) p) x"
unfolding cri.InvGlobNonposImpRecordsNonpos_def cri.nonpos_upto_def
by (metis linorder_not_less cri.order.order_iff_strict)
show ?thesis
using r[rule_format, of p]
by (auto simp: cri.nonpos_upto_def not_le)
qed
lemma help_lemma:
assumes "0 < zcount (c_pts (prop_config c p) loc0) t0"
and "(loc0, t0) ≤⇩p (loc1, t1)"
and "s2 ∈⇩A path_summary loc1 loc2"
and "safe (prop_config c p)"
shows "∃ t2. (t2 ≤ results_in t1 s2
∧ t2 ∈⇩A frontier (c_imp (prop_config c p) loc2))"
proof -
from assms(2) obtain s1 where s1: "s1 ∈⇩A path_summary loc0 loc1" "results_in t0 s1 ≤ t1"
by (auto simp add: cri_less_eq_def)
from s1(1) assms(3) obtain s_full where s_full: "s_full ∈⇩A path_summary loc0 loc2" "s_full ≤ followed_by s1 s2"
using flow.path_weight_elem_trans by blast
from s_full(1) assms(1,4) obtain t2 where t2:
"t2 ∈⇩A frontier (c_imp (prop_config c p) loc2)" "t2 ≤ results_in t0 s_full"
unfolding safe_def by blast
from t2(2) and s_full(2) have "t2 ≤ results_in (results_in t0 s1) s2"
by (metis followed_by_summary order_trans results_in_mono(2))
with s1(2) have "t2 ≤ results_in t1 s2" by (meson order.trans results_in_mono(1))
with t2(1) show ?thesis by auto
qed
lemma lift_prop_inv_NextPropagate':
assumes "(⋀c0 c1 loc t. P c0 ⟹ next_propagate' c0 c1 loc t ⟹ P c1)"
shows "P (prop_config c0 p') ⟹ NextPropagate' c0 c1 p ⟹ P (prop_config c1 p')"
proof -
assume pc0: "P (prop_config c0 p')"
assume np: "NextPropagate' c0 c1 p"
have n_p: "(⋀c0 c1. P c0 ⟹ next_propagate c0 c1 ⟹ P c1)"
using assms by auto
let ?f = "λc. SOME c'. next_propagate c c'"
let ?b = "λc. ∃loc. c_work c loc ≠ {#}⇩z"
from np have pc1: "Some (prop_config c1 p) = propagate_all (prop_config c0 p)"
by (simp add: NextPropagate'_def)
show ?thesis
apply (cases "p'=p")
subgoal
apply (rule while_option_rule[of P ?b ?f "prop_config c0 p"])
apply (rule n_p)
apply assumption
apply (rule iffD1[OF verit_sko_ex])
apply (elim exE)
apply (rule exists_next_propagate')
apply assumption
using pc1 apply (simp add: propagate_all_def)
using pc0 apply simp
done
subgoal
using np pc0 by (auto simp: NextPropagate'_def dest!: spec[of _ p'])
done
qed
subsubsection‹Propagate is a Subsystem›
lemma NextRecvUpd'_next':
assumes "safe (prop_config c0 q)"
and "InvGlobPointstampsEq c0"
and "cri.InvMsgInGlob (exchange_config c0)"
and "NextRecvUpd' c0 c1 p q"
shows "next'⇧+⇧+ (prop_config c0 q') (prop_config c1 q')"
apply (subst NextRecvUpdD(4)[OF assms(4), rule_format])
apply simp
apply safe
subgoal
apply (subst cm_all_eq_cm_all')
apply clarsimp
apply (drule assms(3)[unfolded cri.InvMsgInGlob_def, rule_format, OF cri.next_recvupdD(1)[OF NextRecvUpdD(2)[OF assms(4)]]])
apply clarsimp
subgoal for loc t loc' t'
apply (subst (asm) assms(2)[unfolded InvGlobPointstampsEq_def, rule_format, symmetric])
apply (clarsimp simp: cri_less_eq_def)
subgoal for s
using assms(1)[unfolded safe_def, rule_format, of loc' t' s loc]
apply -
apply (drule meta_mp)
apply simp
apply clarsimp
subgoal for t''
apply (clarsimp intro!: exI[of _ t''])
using order_trans apply blast
done
done
done
apply (rule lift_cm_inv_cm_all')
apply (rule tranclp.intros(2))
apply (auto simp: next'_def) [2]
apply clarsimp
apply (drule assms(3)[unfolded cri.InvMsgInGlob_def, rule_format, OF cri.next_recvupdD(1)[OF NextRecvUpdD(2)[OF assms(4)]]])
apply clarsimp
subgoal for loc t loc' t'
apply (subst (asm) assms(2)[unfolded InvGlobPointstampsEq_def, rule_format, symmetric])
apply (clarsimp simp: cri_less_eq_def)
subgoal for s
using assms(1)[unfolded safe_def, rule_format, of loc' t' s loc]
apply -
apply (drule meta_mp)
apply simp
apply clarsimp
subgoal for t''
apply (clarsimp intro!: exI[of _ t''])
using order_trans apply blast
done
done
done
apply (auto simp: next'_def)
done
apply (auto simp: next'_def)
done
lemma NextPropagate'_next':
assumes "NextPropagate' c0 c1 p"
shows "next'⇧+⇧+ (prop_config c0 q) (prop_config c1 q)"
apply (cases "p=q")
subgoal
apply (rule lift_propagate_inv_propagate_all[of _ "prop_config c0 p"])
apply (rule tranclp.intros(2))
apply (auto simp: next'_def NextPropagateD(3)[OF assms, rule_format])
done
subgoal
by (metis NextPropagateD(3) assms next'_def option.simps(1) tranclp.intros(1))
done
lemma next_imp_propagate_next:
assumes "inv_init_imp_prop_safe c0"
and "InvGlobPointstampsEq c0"
and "cri.InvMsgInGlob (exchange_config c0)"
shows "Next' c0 c1 ⟹ next'⇧+⇧+ (prop_config c0 p) (prop_config c1 p)"
unfolding Next'_def NextPerformOp'_def NextSendUpd'_def NextRecvCap'_def
apply safe
subgoal by (auto simp: next'_def)
subgoal by (auto simp: next'_def)
subgoal for p' q
using assms(1)[unfolded inv_init_imp_prop_safe_def, rule_format, of q]
apply -
apply (drule meta_mp)
apply (rule NextRecvUpdD(1))
apply simp
apply (cases "q=p")
apply (auto dest!: NextRecvUpd'_next'[rotated, OF assms(2-)]) []
apply (auto simp add: NextRecvUpd'_def next'_def)
done
subgoal by (rule NextPropagate'_next')
subgoal by (auto simp: next'_def)
subgoal by (auto simp: next'_def)
done
lemma alw_next_imp_propagate_next:
assumes "alw (holds inv_init_imp_prop_safe) s"
and "alw (holds InvGlobPointstampsEq) s"
and "alw (holds cri.InvMsgInGlob) (smap exchange_config s)"
and "alw Next s"
shows "alw (relates (next'⇧+⇧+)) (smap (λs. prop_config s p) s)"
using assms by (coinduction arbitrary: s rule: alw.coinduct) (auto intro!: next_imp_propagate_next simp: relates_def alw_holds_smap_conv_comp)
text‹Any Tracker trace is a valid Propagate trace (using the transitive closure of next, since
tracker may take multiple propagate steps at once).›
lemma spec_imp_propagate_spec: "FullSpec s ⟹ (holds init_config aand alw (relates (next'⇧+⇧+))) (smap (λc. prop_config c p) s)"
apply (frule alw_inv_init_imp_prop_safe)
apply (frule alw_InvGlobPointstampsEq)
apply (frule spec_imp_exchange_spec)
apply (drule cri.alw_InvMsgInGlob)
apply (auto intro!: alw_next_imp_propagate_next simp: FullSpec_def InitConfig_def)
done
subsection‹Safety Proofs›
lemma safe_satisfied:
assumes "cri.InvGlobNonposImpRecordsNonpos (exchange_config c)"
and "inv_init_imp_prop_safe c"
and "InvGlobPointstampsEq c"
shows "safe_combined c"
proof -
{
fix loc1 loc2 t s p
assume as: "0 < zcount (cri.records (exchange_config c)) (loc1, t)"
"s ∈⇩A path_summary loc1 loc2" "init c p"
obtain loc0 t0 where delayed:
"(loc0, t0) ≤⇩p (loc1, t)" "0 < zcount (c_glob (exchange_config c) p) (loc0, t0)"
using nrec_pts_delayed[OF assms(1) as(1)]
by fast
with as(2,3) assms(2) have
"∃t2. t2 ≤ results_in t s ∧ t2 ∈⇩A frontier (c_imp (prop_config c p) loc2)"
using help_lemma delayed
by (metis InvGlobPointstampsEq_def assms(3) inv_init_imp_prop_safe_def)
}
then show ?thesis
unfolding safe_combined_def by blast
qed
lemma alw_safe_combined: "FullSpec s ⟹ alw (holds safe_combined) s"
apply (frule alw_inv_init_imp_prop_safe)
apply (frule exch_alw_InvGlobNonposImpRecordsNonpos)
apply (drule alw_InvGlobPointstampsEq)
apply (coinduction arbitrary: s rule: alw.coinduct)
apply clarsimp
apply (rule conjI)
apply (metis alwD alw_holds2 safe_satisfied)
apply (rule disjI1)
apply blast
done
lemma alw_safe_combined2: "FullSpec s ⟹ alw (holds safe_combined2) s"
apply (frule exch_alw_InvCapsNonneg)
apply (drule alw_safe_combined)
apply (simp add: alw_iff_sdrop safe_combined_implies_safe_combined2)
done
lemma alw_implication_frontier_eq_implied_frontier:
"FullSpec s ⟹
alw (holds (λc. worklists_vacant_to (prop_config c p) b ⟶
b ∈⇩A frontier (c_imp (prop_config c p) loc) ⟷ b ∈⇩A implied_frontier (c_pts (prop_config c p)) loc)) s"
by (drule alw_prop_invs)
(auto simp: implication_frontier_iff_implied_frontier_vacant all_imp_alw elim: alw_mp)
end
end