section ‹Rely-guarantee-based Safety Reasoning›
theory PiCore_RG_Invariant
imports PiCore_Hoare
begin
type_synonym 's invariant = "'s ⇒ bool"
context event_hoare
begin
definition invariant_presv_pares::"'Env ⇒ 's invariant ⇒ ('l,'k,'s,'prog) paresys ⇒ 's set ⇒ ('s × 's) set ⇒ bool"
where "invariant_presv_pares Γ invar pares init R ≡
∀s0 x0 pesl. s0∈init ∧ pesl ∈ (cpts_from (pestran Γ) (pares, s0, x0) ∩ assume (lift_state_set init) (lift_state_pair_set R))
⟶ (∀i<length pesl. invar (fst (snd (pesl!i))))"
definition invariant_presv_pares2::"'Env ⇒ 's invariant ⇒ ('l,'k,'s,'prog) paresys ⇒ 's set ⇒ ('s × 's) set ⇒ bool"
where "invariant_presv_pares2 Γ invar pares init R ≡
∀s0 x0 pesl. pesl ∈ (cpts_from (pestran Γ) (pares, s0, x0) ∩ assume (lift_state_set init) (lift_state_pair_set R))
⟶ (∀i<length pesl. invar (fst (snd (pesl!i))))"
lemma "invariant_presv_pares Γ invar pares init R = invariant_presv_pares2 Γ invar pares init R"
by (auto simp add:invariant_presv_pares_def invariant_presv_pares2_def assume_def lift_state_set_def)
theorem invariant_theorem:
assumes parsys_sat_rg: "Γ ⊢ pesf SAT⇩e [init, R, G, pst]"
and stb_rely: "stable (Collect invar) R"
and stb_guar: "stable (Collect invar) G"
and init_in_invar: "init ⊆ (Collect invar)"
shows "invariant_presv_pares Γ invar (par_com pesf) init R"
proof -
let ?init = ‹lift_state_set init›
let ?R = ‹lift_state_pair_set R›
let ?G = ‹lift_state_pair_set G›
let ?pst = ‹lift_state_set pst›
from parsys_sat_rg have "Γ ⊨ par_com pesf SAT⇩e [init, R, G, pst]" using rghoare_pes_sound by fast
hence cpts_pes: "∀s. (cpts_from (pestran Γ) (par_com pesf, s)) ∩ assume ?init ?R ⊆ commit (pestran Γ) par_fin ?G ?pst" by simp
show ?thesis
proof -
{
fix s0 x0 pesl
assume a0: "s0∈init"
and a1: "pesl∈cpts_from (pestran Γ) (par_com pesf, s0, x0) ∩ assume ?init ?R"
from a1 have a3: "pesl!0 = (par_com pesf, s0, x0) ∧ pesl∈cpts (pestran Γ)" using hd_conv_nth cpts_nonnil by force
from a1 cpts_pes have pesl_in_comm: "pesl ∈ commit (pestran Γ) par_fin ?G ?pst" by auto
{
fix i
assume b0: "i<length pesl"
then have "fst (snd (pesl!i)) ∈ (Collect invar)"
proof(induct i)
case 0
with a3 have "snd (pesl!0) = (s0,x0)" by simp
with a0 init_in_invar show ?case by auto
next
case (Suc ni)
assume c0: "ni < length pesl ⟹ fst (snd (pesl ! ni)) ∈ (Collect invar)"
and c1: "Suc ni < length pesl"
then have c2: "fst (snd (pesl ! ni)) ∈ (Collect invar)" by auto
from c1 have c3: "ni < length pesl" by simp
with c0 have c4: "fst (snd (pesl ! ni)) ∈ (Collect invar)" by simp
from a3 c1 have "pesl ! ni ─e→ pesl ! Suc ni ∨ (pesl ! ni, pesl ! Suc ni) ∈ pestran Γ"
using ctran_or_etran_par by blast
then show ?case
proof
assume d0: "pesl ! ni ─e→ pesl ! Suc ni"
then show ?thesis using c3 c4 a1 c1 stb_rely by(simp add:assume_def stable_def lift_state_set_def lift_state_pair_set_def case_prod_unfold)
next
assume "(pesl ! ni, pesl ! Suc ni) ∈ pestran Γ"
then obtain et where d0: "Γ ⊢ pesl ! ni ─pes[et]→ pesl ! Suc ni" by (auto simp add: pestran_def)
then show ?thesis using c3 c4 c1 pesl_in_comm stb_guar
apply(simp add:commit_def stable_def lift_state_set_def lift_state_pair_set_def case_prod_unfold)
using ‹(pesl ! ni, pesl ! Suc ni) ∈ pestran Γ› by blast
qed
qed
}
}
then show ?thesis using invariant_presv_pares_def by blast
qed
qed
end
end