Theory CIMP_vcg
theory CIMP_vcg
imports
CIMP_lang
begin
section‹ State-based invariants \label{sec:cimp-invariants} ›
text‹
We provide a simple-minded verification condition generator (VCG) for this language, providing
support for establishing state-based invariants. It is just one way of reasoning about CIMP programs
and is proven sound wrt to the CIMP semantics.
Our approach follows \<^citet>‹"DBLP:journals/acta/Lamport80" and "DBLP:journals/toplas/LamportS84"›
(and the later \<^citet>‹"Lamport:2002"›) and closely
related work by \<^citet>‹"AptFrancezDeRoever:1980"›,
\<^citet>‹"CousotCousot:1980"› and \<^citet>‹"DBLP:journals/acta/LevinG81"›, who suggest the
incorporation of a history variable. \<^citet>‹"CousotCousot:1980"› apparently contains a completeness proof.
Lamport mentions that this technique was well-known in the mid-80s
when he proposed the use of prophecy variables\footnote{@{url
"https://lamport.azurewebsites.net/pubs/pubs.html"}}. See also \<^citet>‹"deRoeverEtAl:2001"› for an extended discussion of
some of this.
›
declare small_step.intros[intro]
inductive_cases small_step_inv:
"(⦃l⦄ Request action val # cs, ls) →⇘a⇙ s'"
"(⦃l⦄ Response action # cs, ls) →⇘a⇙ s'"
"(⦃l⦄ LocalOp R # cs, ls) →⇘a⇙ s'"
"(⦃l⦄ IF b THEN c FI # cs, ls) →⇘a⇙ s'"
"(⦃l⦄ IF b THEN c1 ELSE c2 FI # cs, ls) →⇘a⇙ s'"
"(⦃l⦄ WHILE b DO c OD # cs, ls) →⇘a⇙ s'"
"(LOOP DO c OD # cs, ls) →⇘a⇙ s'"
lemma small_step_stuck:
"¬ ([], s) →⇘α⇙ c'"
by (auto elim: small_step.cases)
declare system_step.intros[intro]
text‹
By default we ask the simplifier to rewrite @{const "atS"} using
ambient @{const "AT"} information.
›
lemma atS_state_weak_cong[cong]:
"AT s p = AT s' p ⟹ atS p ls s ⟷ atS p ls s'"
by (auto simp: atS_def)
text‹
We provide an incomplete set of basic rules for label sets.
›
lemma atS_simps:
"¬atS p {} s"
"atS p {l} s ⟷ at p l s"
"⟦at p l s; l ∈ ls⟧ ⟹ atS p ls s"
"(∀l. at p l s ⟶ l ∉ ls) ⟹ ¬atS p ls s"
by (auto simp: atS_def)
lemma atS_mono:
"⟦atS p ls s; ls ⊆ ls'⟧ ⟹ atS p ls' s"
by (auto simp: atS_def)
lemma atS_un:
"atS p (l ∪ l') s ⟷ atS p l s ∨ atS p l' s"
by (auto simp: atS_def)
lemma atLs_disj_union[simp]:
"(atLs p label0 ❙∨ atLs p label1) = atLs p (label0 ∪ label1)"
unfolding atLs_def by simp
lemma atLs_insert_disj:
"atLs p (insert l label0) = (atL p l ❙∨ atLs p label0)"
by simp
lemma small_step_terminated:
"s →⇘x⇙ s' ⟹ atCs (fst s) = {} ⟹ atCs (fst s') = {}"
by (induct pred: small_step) auto
lemma atC_not_empty:
"atC c ≠ {}"
by (induct c) auto
lemma atCs_empty:
"atCs cs = {} ⟷ cs = []"
by (induct cs) (auto simp: atC_not_empty)
lemma terminated_no_commands:
assumes "terminated p sh"
shows "∃s. GST sh p = ([], s)"
using assms unfolding atLs_def AT_def by (metis atCs_empty prod.collapse singletonD)
lemma terminated_GST_stable:
assumes "system_step q sh' sh"
assumes "terminated p sh"
shows "GST sh p = GST sh' p"
using assms by (auto dest!: terminated_no_commands simp: small_step_stuck elim!: system_step.cases)
lemma terminated_stable:
assumes "system_step q sh' sh"
assumes "terminated p sh"
shows "terminated p sh'"
using assms unfolding atLs_def AT_def
by (fastforce split: if_splits prod.splits
dest: small_step_terminated
elim!: system_step.cases)
lemma system_step_pls_nonempty:
assumes "system_step pls sh' sh"
shows "pls ≠ {}"
using assms by cases simp_all
lemma system_step_no_change:
assumes "system_step ps sh' sh"
assumes "p ∉ ps"
shows "GST sh' p = GST sh p"
using assms by cases simp_all
lemma initial_stateD:
assumes "initial_state sys s"
shows "AT (⦇GST = s, HST = []⦈) = atC ∘ PGMs sys ∧ INIT sys (⦇GST = s, HST = []⦈)↓ ∧ (∀p l. ¬taken p l ⦇GST = s, HST = []⦈)"
using assms unfolding initial_state_def split_def o_def LST_def AT_def taken_def by simp
lemma initial_states_initial[iff]:
assumes "initial_state sys s"
shows "at p l (⦇GST = s, HST = []⦈) ⟷ l ∈ atC (PGMs sys p)"
using assms unfolding initial_state_def split_def AT_def by simp
definition
reachable_state :: "('answer, 'location, 'proc, 'question, 'state, 'ext) pre_system_ext
⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred"
where
"reachable_state sys s ⟷ (∃σ i. prerun sys σ ∧ σ i = s)"
lemma reachable_stateE:
assumes "reachable_state sys sh"
assumes "⋀σ i. prerun sys σ ⟹ P (σ i)"
shows "P sh"
using assms unfolding reachable_state_def by blast
lemma prerun_reachable_state:
assumes "prerun sys σ"
shows "reachable_state sys (σ i)"
using assms unfolding prerun_def LTL.defs system_step_reflclp_def reachable_state_def by auto
lemma reachable_state_induct[consumes 1, case_names init LocalStep CommunicationStep, induct set: reachable_state]:
assumes r: "reachable_state sys sh"
assumes i: "⋀s. initial_state sys s ⟹ P ⦇GST = s, HST = []⦈"
assumes l: "⋀sh ls' p. ⟦reachable_state sys sh; P sh; GST sh p →⇘τ⇙ ls'⟧ ⟹ P ⦇GST = (GST sh)(p := ls'), HST = HST sh⦈"
assumes c: "⋀sh ls1' ls2' p1 p2 α β.
⟦reachable_state sys sh; P sh;
GST sh p1 →⇘«α, β»⇙ ls1'; GST sh p2 →⇘»α, β«⇙ ls2'; p1 ≠ p2 ⟧
⟹ P ⦇GST = (GST sh)(p1 := ls1', p2 := ls2'), HST = HST sh @ [(α, β)]⦈"
shows "P sh"
using r
proof(rule reachable_stateE)
fix σ i assume "prerun sys σ" show "P (σ i)"
proof(induct i)
case 0 from ‹prerun sys σ› show ?case
unfolding prerun_def by (metis (full_types) i old.unit.exhaust system_state.surjective)
next
case (Suc i) with ‹prerun sys σ› show ?case
unfolding prerun_def LTL.defs system_step_reflclp_def reachable_state_def
apply clarsimp
apply (drule_tac x=i in spec)
apply (erule disjE; clarsimp)
apply (erule system_step.cases; clarsimp)
apply (metis (full_types) ‹prerun sys σ› l old.unit.exhaust prerun_reachable_state system_state.surjective)
apply (metis (full_types) ‹prerun sys σ› c old.unit.exhaust prerun_reachable_state system_state.surjective)
done
qed
qed
lemma prerun_valid_TrueI:
shows "sys ⊨⇘pre⇙ ⟨True⟩"
unfolding prerun_valid_def by simp
lemma prerun_valid_conjI:
assumes "sys ⊨⇘pre⇙ P"
assumes "sys ⊨⇘pre⇙ Q"
shows "sys ⊨⇘pre⇙ P ❙∧ Q"
using assms unfolding prerun_valid_def always_def by simp
lemma valid_prerun_lift:
assumes "sys ⊨⇘pre⇙ I"
shows "sys ⊨ □⌈I⌉"
using assms unfolding prerun_valid_def valid_def run_def by blast
lemma prerun_valid_induct:
assumes "⋀σ. prerun sys σ ⟹ ⌈I⌉ σ"
assumes "⋀σ. prerun sys σ ⟹ (⌈I⌉ ❙↪ (○⌈I⌉)) σ"
shows "sys ⊨⇘pre⇙ I"
unfolding prerun_valid_def using assms by (simp add: always_induct)
lemma prerun_validI:
assumes "⋀s. reachable_state sys s ⟹ I s"
shows "sys ⊨⇘pre⇙ I"
unfolding prerun_valid_def using assms by (simp add: alwaysI prerun_reachable_state)
lemma prerun_validE:
assumes "reachable_state sys s"
assumes "sys ⊨⇘pre⇙ I"
shows "I s"
using assms unfolding prerun_valid_def
by (metis alwaysE reachable_stateE suffix_state_prop)
subsubsection‹Relating reachable states to the initial programs \label{sec:cimp-decompose-small-step}›
text‹
To usefully reason about the control locations presumably embedded in
the single global invariant, we need to link the programs we have in
reachable state ‹s› to the programs in the initial states. The
‹fragments› function decomposes the program into statements
that can be directly executed (\S\ref{sec:cimp-decompose}). We also
compute the locations we could be at after executing that statement as
a function of the process's local state.
Eliding the bodies of ‹IF› and ‹WHILE› statements
yields smaller (but equivalent) proof obligations.
›
type_synonym ('answer, 'location, 'question, 'state) loc_comp
= "'state ⇒ 'location set"
fun lconst :: "'location set ⇒ ('answer, 'location, 'question, 'state) loc_comp" where
"lconst lp s = lp"
definition lcond :: "'location set ⇒ 'location set ⇒ 'state bexp
⇒ ('answer, 'location, 'question, 'state) loc_comp" where
"lcond lp lp' b s = (if b s then lp else lp')"
lemma lcond_split:
"Q (lcond lp lp' b s) ⟷ (b s ⟶ Q lp) ∧ (¬b s ⟶ Q lp')"
unfolding lcond_def by (simp split: if_splits)
lemma lcond_split_asm:
"Q (lcond lp lp' b s) ⟷ ¬ ((b s ∧ ¬Q lp) ∨ (¬b s ∧ ¬ Q lp'))"
unfolding lcond_def by (simp split: if_splits)
lemmas lcond_splits = lcond_split lcond_split_asm
fun
fragments :: "('answer, 'location, 'question, 'state) com
⇒ 'location set
⇒ ( ('answer, 'location, 'question, 'state) com
× ('answer, 'location, 'question, 'state) loc_comp ) set"
where
"fragments (⦃l⦄ IF b THEN c FI) aft
= { (⦃l⦄ IF b THEN c' FI, lcond (atC c) aft b) |c'. True }
∪ fragments c aft"
| "fragments (⦃l⦄ IF b THEN c1 ELSE c2 FI) aft
= { (⦃l⦄ IF b THEN c1' ELSE c2' FI, lcond (atC c1) (atC c2) b) |c1' c2'. True }
∪ fragments c1 aft ∪ fragments c2 aft"
| "fragments (LOOP DO c OD) aft = fragments c (atC c)"
| "fragments (⦃l⦄ WHILE b DO c OD) aft
= fragments c {l} ∪ { (⦃l⦄ WHILE b DO c' OD, lcond (atC c) aft b) |c'. True }"
| "fragments (c1;; c2) aft = fragments c1 (atC c2) ∪ fragments c2 aft"
| "fragments (c1 ⊕ c2) aft = fragments c1 aft ∪ fragments c2 aft"
| "fragments c aft = { (c, lconst aft) }"
fun
fragmentsL :: "('answer, 'location, 'question, 'state) com list
⇒ ( ('answer, 'location, 'question, 'state) com
× ('answer, 'location, 'question, 'state) loc_comp ) set"
where
"fragmentsL [] = {}"
| "fragmentsL [c] = fragments c {}"
| "fragmentsL (c # c' # cs) = fragments c (atC c') ∪ fragmentsL (c' # cs)"
abbreviation
fragmentsLS :: "('answer, 'location, 'question, 'state) local_state
⇒ ( ('answer, 'location, 'question, 'state) com
× ('answer, 'location, 'question, 'state) loc_comp ) set"
where
"fragmentsLS s ≡ fragmentsL (cPGM s)"
text‹
We show that taking system steps preserves fragments.
›
lemma small_step_fragmentsLS:
assumes "s →⇘α⇙ s'"
shows "fragmentsLS s' ⊆ fragmentsLS s"
using assms by induct (case_tac [!] cs, auto)
lemma reachable_state_fragmentsLS:
assumes "reachable_state sys sh"
shows "fragmentsLS (GST sh p) ⊆ fragments (PGMs sys p) {}"
using assms
by (induct rule: reachable_state_induct)
(auto simp: initial_state_def dest: subsetD[OF small_step_fragmentsLS])
inductive
basic_com :: "('answer, 'location, 'question, 'state) com ⇒ bool"
where
"basic_com (⦃l⦄ Request action val)"
| "basic_com (⦃l⦄ Response action)"
| "basic_com (⦃l⦄ LocalOp R)"
| "basic_com (⦃l⦄ IF b THEN c FI)"
| "basic_com (⦃l⦄ IF b THEN c1 ELSE c2 FI)"
| "basic_com (⦃l⦄ WHILE b DO c OD)"
lemma fragments_basic_com:
assumes "(c', aft') ∈ fragments c aft"
shows "basic_com c'"
using assms by (induct c arbitrary: aft) (auto intro: basic_com.intros)
lemma fragmentsL_basic_com:
assumes "(c', aft') ∈ fragmentsL cs"
shows "basic_com c'"
using assms
apply (induct cs)
apply simp
apply (case_tac cs)
apply (auto simp: fragments_basic_com)
done
text‹
To reason about system transitions we need to identify which basic
statement gets executed next. To that end we factor out the recursive
cases of the @{term "small_step"} semantics into \emph{contexts},
which isolate the ‹basic_com› commands with immediate
externally-visible behaviour. Note that non-determinism means that
more than one ‹basic_com› can be enabled at a time.
The representation of evaluation contexts follows \<^citet>‹"DBLP:journals/jar/Berghofer12"›. This style of
operational semantics was originated by \<^citet>‹"FelleisenHieb:1992"›.
›
type_synonym ('answer, 'location, 'question, 'state) ctxt
= "(('answer, 'location, 'question, 'state) com ⇒ ('answer, 'location, 'question, 'state) com)
× (('answer, 'location, 'question, 'state) com ⇒ ('answer, 'location, 'question, 'state) com list)"
inductive_set
ctxt :: "('answer, 'location, 'question, 'state) ctxt set"
where
C_Hole: "(id, ⟨[]⟩) ∈ ctxt"
| C_Loop: "(E, fctxt) ∈ ctxt ⟹ (λc1. LOOP DO E c1 OD, λc1. fctxt c1 @ [LOOP DO E c1 OD]) ∈ ctxt"
| C_Seq: "(E, fctxt) ∈ ctxt ⟹ (λc1. E c1;; c2, λc1. fctxt c1 @ [c2]) ∈ ctxt"
| C_Choose1: "(E, fctxt) ∈ ctxt ⟹ (λc1. E c1 ⊕ c2, fctxt) ∈ ctxt"
| C_Choose2: "(E, fctxt) ∈ ctxt ⟹ (λc2. c1 ⊕ E c2, fctxt) ∈ ctxt"
text‹
We can decompose a small step into a context and a @{const "basic_com"}.
›
fun
decompose_com :: "('answer, 'location, 'question, 'state) com
⇒ ( ('answer, 'location, 'question, 'state) com
× ('answer, 'location, 'question, 'state) ctxt ) set"
where
"decompose_com (LOOP DO c1 OD) = { (c, λt. LOOP DO ictxt t OD, λt. fctxt t @ [LOOP DO ictxt t OD]) |c fctxt ictxt. (c, ictxt, fctxt) ∈ decompose_com c1 }"
| "decompose_com (c1;; c2) = { (c, λt. ictxt t;; c2, λt. fctxt t @ [c2]) |c fctxt ictxt. (c, ictxt, fctxt) ∈ decompose_com c1 }"
| "decompose_com (c1 ⊕ c2) = { (c, λt. ictxt t ⊕ c2, fctxt) |c fctxt ictxt. (c, ictxt, fctxt) ∈ decompose_com c1 }
∪ { (c, λt. c1 ⊕ ictxt t, fctxt) |c fctxt ictxt. (c, ictxt, fctxt) ∈ decompose_com c2 }"
| "decompose_com c = {(c, id, ⟨[]⟩)}"
definition
decomposeLS :: "('answer, 'location, 'question, 'state) local_state
⇒ ( ('answer, 'location, 'question, 'state) com
× (('answer, 'location, 'question, 'state) com ⇒ ('answer, 'location, 'question, 'state) com)
× (('answer, 'location, 'question, 'state) com ⇒ ('answer, 'location, 'question, 'state) com list) ) set"
where
"decomposeLS s = (case cPGM s of c # _ ⇒ decompose_com c | _ ⇒ {})"
lemma ctxt_inj:
assumes "(E, fctxt) ∈ ctxt"
assumes "E x = E y"
shows "x = y"
using assms by (induct set: ctxt) auto
lemma decompose_com_non_empty: "decompose_com c ≠ {}"
by (induct c) auto
lemma decompose_com_basic_com:
assumes "(c', ctxts) ∈ decompose_com c"
shows "basic_com c'"
using assms by (induct c arbitrary: c' ctxts) (auto intro: basic_com.intros)
lemma decomposeLS_basic_com:
assumes "(c', ctxts) ∈ decomposeLS s"
shows "basic_com c'"
using assms unfolding decomposeLS_def by (simp add: decompose_com_basic_com split: list.splits)
lemma decompose_com_ctxt:
assumes "(c', ctxts) ∈ decompose_com c"
shows "ctxts ∈ ctxt"
using assms by (induct c arbitrary: c' ctxts) (auto intro: ctxt.intros)
lemma decompose_com_ictxt:
assumes "(c', ictxt, fctxt) ∈ decompose_com c"
shows "ictxt c' = c"
using assms by (induct c arbitrary: c' ictxt fctxt) auto
lemma decompose_com_small_step:
assumes as: "(c' # fctxt c' @ cs, s) →⇘α⇙ s'"
assumes ds: "(c', ictxt, fctxt) ∈ decompose_com c"
shows "(c # cs, s) →⇘α⇙ s'"
using decompose_com_ctxt[OF ds] as decompose_com_ictxt[OF ds]
by (induct ictxt fctxt arbitrary: c cs)
(cases s', fastforce simp: fun_eq_iff dest: ctxt_inj)+
theorem context_decompose:
"s →⇘α⇙ s' ⟷ (∃(c, ictxt, fctxt) ∈ decomposeLS s.
cPGM s = ictxt c # tl (cPGM s)
∧ (c # fctxt c @ tl (cPGM s), cTKN s, cLST s) →⇘α⇙ s'
∧ (∀l∈atC c. cTKN s' = Some l))" (is "?lhs = ?rhs")
proof(rule iffI)
assume ?lhs then show ?rhs
unfolding decomposeLS_def
proof(induct rule: small_step.induct)
case (Choose1 c1 cs s α cs' s' c2) then show ?case
apply clarsimp
apply (rename_tac c ictxt fctxt)
apply (rule_tac x="(c, λt. ictxt t ⊕ c2, fctxt)" in bexI)
apply auto
done
next
case (Choose2 c2 cs s α cs' s' c1) then show ?case
apply clarsimp
apply (rename_tac c ictxt fctxt)
apply (rule_tac x="(c, λt. c1 ⊕ ictxt t, fctxt)" in bexI)
apply auto
done
qed fastforce+
next
assume ?rhs then show ?lhs
unfolding decomposeLS_def
by (cases s) (auto split: list.splits dest: decompose_com_small_step)
qed
text‹
While we only use this result left-to-right (to decompose a small step
into a basic one), this equivalence shows that we lose no information
in doing so.
Decomposing a compound command preserves @{const ‹fragments›} too.
›
fun
loc_compC :: "('answer, 'location, 'question, 'state) com
⇒ ('answer, 'location, 'question, 'state) com list
⇒ ('answer, 'location, 'question, 'state) loc_comp"
where
"loc_compC (⦃l⦄ IF b THEN c FI) cs = lcond (atC c) (atCs cs) b"
| "loc_compC (⦃l⦄ IF b THEN c1 ELSE c2 FI) cs = lcond (atC c1) (atC c2) b"
| "loc_compC (LOOP DO c OD) cs = lconst (atC c)"
| "loc_compC (⦃l⦄ WHILE b DO c OD) cs = lcond (atC c) (atCs cs) b"
| "loc_compC c cs = lconst (atCs cs)"
lemma decompose_fragments:
assumes "(c, ictxt, fctxt) ∈ decompose_com c0"
shows "(c, loc_compC c (fctxt c @ cs)) ∈ fragments c0 (atCs cs)"
using assms
proof(induct c0 arbitrary: c ictxt fctxt cs)
case (Loop c01 c ictxt fctxt cs)
from Loop.prems Loop.hyps(1)[where cs="ictxt c # cs"] show ?case by (auto simp: decompose_com_ictxt)
next
case (Seq c01 c02 c ictxt fctxt cs)
from Seq.prems Seq.hyps(1)[where cs="c02 # cs"] show ?case by auto
qed auto
lemma at_decompose:
assumes "(c, ictxt, fctxt) ∈ decompose_com c0"
shows "atC c ⊆ atC c0"
using assms by (induct c0 arbitrary: c ictxt fctxt; fastforce)
lemma at_decomposeLS:
assumes "(c, ictxt, fctxt) ∈ decomposeLS s"
shows "atC c ⊆ atCs (cPGM s)"
using assms unfolding decomposeLS_def by (auto simp: at_decompose split: list.splits)
lemma decomposeLS_fragmentsLS:
assumes "(c, ictxt, fctxt) ∈ decomposeLS s"
shows "(c, loc_compC c (fctxt c @ tl (cPGM s))) ∈ fragmentsLS s"
using assms
proof(cases "cPGM s")
case (Cons d ds)
with assms decompose_fragments[where cs="ds"] show ?thesis
by (cases ds) (auto simp: decomposeLS_def)
qed (simp add: decomposeLS_def)
lemma small_step_loc_compC:
assumes "basic_com c"
assumes "(c # cs, ls) →⇘α⇙ ls'"
shows "loc_compC c cs (snd ls) = atCs (cPGM ls')"
using assms by (fastforce elim: basic_com.cases elim!: small_step_inv split: lcond_splits)
text‹
The headline result allows us to constrain the initial and final states
of a given small step in terms of the original programs, provided the
initial state is reachable.
›
theorem decompose_small_step:
assumes "GST sh p →⇘α⇙ ps'"
assumes "reachable_state sys sh"
obtains c cs aft
where "(c, aft) ∈ fragments (PGMs sys p) {}"
and "atC c ⊆ atCs (cPGM (GST sh p))"
and "aft (cLST (GST sh p)) = atCs (cPGM ps')"
and "(c # cs, cTKN (GST sh p), cLST (GST sh p)) →⇘α⇙ ps'"
and "∀l∈atC c. cTKN ps' = Some l"
using assms
apply -
apply (frule iffD1[OF context_decompose])
apply clarsimp
apply (frule decomposeLS_fragmentsLS)
apply (frule at_decomposeLS)
apply (frule (1) subsetD[OF reachable_state_fragmentsLS])
apply (frule decomposeLS_basic_com)
apply (frule (1) small_step_loc_compC)
apply simp
done
text‹
Reasoning by induction over the reachable states
with @{thm [source] "decompose_small_step"} is quite tedious. We
provide a very simple VCG that generates friendlier local proof
obligations in \S\ref{sec:vcg}.
›
subsection‹Simple-minded Hoare Logic/VCG for CIMP \label{sec:vcg}›
text‹
\label{sec:cimp-vcg}
We do not develop a proper Hoare logic or full VCG for CIMP: this
machinery merely packages up the subgoals that arise from induction
over the reachable states (\S\ref{sec:cimp-invariants}). This is
somewhat in the spirit of \<^citet>‹"Ridge:2009"›.
Note that this approach is not compositional: it consults the original
system to find matching communicating pairs, and ‹aft›
tracks the labels of possible successor statements. More serious Hoare
logics are provided by \<^citet>‹"DBLP:journals/acta/Lamport80" and "DBLP:journals/toplas/LamportS84"
and "CousotCousot89-IC"›.
Intuitively we need to discharge a proof obligation for either @{const
"Request"}s or @{const "Response"}s but not both. Here we choose to
focus on @{const "Request"}s as we expect to have more local
information available about these.
›
inductive
vcg :: "('answer, 'location, 'proc, 'question, 'state) programs
⇒ 'proc
⇒ ('answer, 'location, 'question, 'state) loc_comp
⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred
⇒ ('answer, 'location, 'question, 'state) com
⇒ ('answer, 'location, 'proc, 'question, 'state) state_pred
⇒ bool" ("_, _, _ ⊢/ ⦃_⦄/ _/ ⦃_⦄" [11,0,0,0,0,0] 11)
where
"⟦ ⋀aft' action' s ps' p's' l' β s' p'.
⟦ pre s; (⦃l'⦄ Response action', aft') ∈ fragments (coms p') {}; p ≠ p';
ps' ∈ val β (s↓ p); (p's', β) ∈ action' (action (s↓ p)) (s↓ p');
at p l s; at p' l' s;
AT s' = (AT s)(p := aft (s↓ p), p' := aft' (s↓ p'));
s'↓ = s↓(p := ps', p' := p's');
taken p l s';
HST s' = HST s @ [(action (s↓ p), β)];
∀p''∈-{p,p'}. GST s' p'' = GST s p''
⟧ ⟹ post s'
⟧ ⟹ coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ Request action val ⦃post⦄"
| "⟦ ⋀s ps' s'.
⟦ pre s; ps' ∈ f (s↓ p);
at p l s;
AT s' = (AT s)(p := aft (s↓ p));
s'↓ = s↓(p := ps');
taken p l s';
HST s' = HST s;
∀p''∈-{p}. GST s' p'' = GST s p''
⟧ ⟹ post s'
⟧ ⟹ coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ LocalOp f ⦃post⦄"
| "⟦ ⋀s s'.
⟦ pre s;
at p l s;
AT s' = (AT s)(p := aft (s↓ p));
s'↓ = s↓;
taken p l s';
HST s' = HST s;
∀p''∈-{p}. GST s' p'' = GST s p''
⟧ ⟹ post s'
⟧ ⟹ coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ IF b THEN t FI ⦃post⦄"
| "⟦ ⋀s s'.
⟦ pre s;
at p l s;
AT s' = (AT s)(p := aft (s↓ p));
s'↓ = s↓;
taken p l s';
HST s' = HST s;
∀p''∈-{p}. GST s' p'' = GST s p''
⟧ ⟹ post s'
⟧ ⟹ coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ IF b THEN t ELSE e FI ⦃post⦄"
| "⟦ ⋀s s'.
⟦ pre s;
at p l s;
AT s' = (AT s)(p := aft (s↓ p));
s'↓ = s↓;
taken p l s';
HST s' = HST s;
∀p''∈-{p}. GST s' p'' = GST s p''
⟧ ⟹ post s'
⟧ ⟹ coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ WHILE b DO c OD ⦃post⦄"
| "coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ Response action ⦃post⦄"
| "coms, p, aft ⊢ ⦃pre⦄ c1 ;; c2 ⦃post⦄"
| "coms, p, aft ⊢ ⦃pre⦄ LOOP DO c OD ⦃post⦄"
| "coms, p, aft ⊢ ⦃pre⦄ c1 ⊕ c2 ⦃post⦄"
text‹
We abbreviate invariance with one-sided validity syntax.
›
abbreviation valid_inv ("_, _, _ ⊢/ ⦃_⦄/ _" [11,0,0,0,0] 11) where
"coms, p, aft ⊢ ⦃I⦄ c ≡ coms, p, aft ⊢ ⦃I⦄ c ⦃I⦄"
inductive_cases vcg_inv:
"coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ Request action val ⦃post⦄"
"coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ LocalOp f ⦃post⦄"
"coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ IF b THEN t FI ⦃post⦄"
"coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ IF b THEN t ELSE e FI ⦃post⦄"
"coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ WHILE b DO c OD ⦃post⦄"
"coms, p, aft ⊢ ⦃pre⦄ LOOP DO c OD ⦃post⦄"
"coms, p, aft ⊢ ⦃pre⦄ ⦃l⦄ Response action ⦃post⦄"
"coms, p, aft ⊢ ⦃pre⦄ c1 ;; c2 ⦃post⦄"
"coms, p, aft ⊢ ⦃pre⦄ Choose c1 c2 ⦃post⦄"
text‹
We tweak @{const "fragments"} by omitting @{const "Response"}s,
yielding fewer obligations
›
fun
vcg_fragments' :: "('answer, 'location, 'question, 'state) com
⇒ 'location set
⇒ ( ('answer, 'location, 'question, 'state) com
× ('answer, 'location, 'question, 'state) loc_comp ) set"
where
"vcg_fragments' (⦃l⦄ Response action) aft = {}"
| "vcg_fragments' (⦃l⦄ IF b THEN c FI) aft
= vcg_fragments' c aft
∪ { (⦃l⦄ IF b THEN c' FI, lcond (atC c) aft b) |c'. True }"
| "vcg_fragments' (⦃l⦄ IF b THEN c1 ELSE c2 FI) aft
= vcg_fragments' c2 aft ∪ vcg_fragments' c1 aft
∪ { (⦃l⦄ IF b THEN c1' ELSE c2' FI, lcond (atC c1) (atC c2) b) |c1' c2'. True }"
| "vcg_fragments' (LOOP DO c OD) aft = vcg_fragments' c (atC c)"
| "vcg_fragments' (⦃l⦄ WHILE b DO c OD) aft
= vcg_fragments' c {l} ∪ { (⦃l⦄ WHILE b DO c' OD, lcond (atC c) aft b) |c'. True }"
| "vcg_fragments' (c1 ;; c2) aft = vcg_fragments' c2 aft ∪ vcg_fragments' c1 (atC c2)"
| "vcg_fragments' (c1 ⊕ c2) aft = vcg_fragments' c1 aft ∪ vcg_fragments' c2 aft"
| "vcg_fragments' c aft = {(c, lconst aft)}"
abbreviation
vcg_fragments :: "('answer, 'location, 'question, 'state) com
⇒ ( ('answer, 'location, 'question, 'state) com
× ('answer, 'location, 'question, 'state) loc_comp ) set"
where
"vcg_fragments c ≡ vcg_fragments' c {}"
fun isResponse :: "('answer, 'location, 'question, 'state) com ⇒ bool" where
"isResponse (⦃l⦄ Response action) ⟷ True"
| "isResponse _ ⟷ False"
lemma fragments_vcg_fragments':
"⟦ (c, aft) ∈ fragments c' aft'; ¬isResponse c ⟧ ⟹ (c, aft) ∈ vcg_fragments' c' aft'"
by (induct c' arbitrary: aft') auto
lemma vcg_fragments'_fragments:
"vcg_fragments' c' aft' ⊆ fragments c' aft'"
by (induct c' arbitrary: aft') (auto 10 0)
lemma VCG_step:
assumes V: "⋀p. ∀(c, aft) ∈ vcg_fragments (PGMs sys p). PGMs sys, p, aft ⊢ ⦃pre⦄ c ⦃post⦄"
assumes S: "system_step p sh' sh"
assumes R: "reachable_state sys sh"
assumes P: "pre sh"
shows "post sh'"
using S
proof cases
case LocalStep with P show ?thesis
apply -
apply (erule decompose_small_step[OF _ R])
apply (frule fragments_basic_com)
apply (erule basic_com.cases)
apply (fastforce dest!: fragments_vcg_fragments' V[rule_format]
elim: vcg_inv elim!: small_step_inv
simp: LST_def AT_def taken_def fun_eq_iff)+
done
next
case CommunicationStep with P show ?thesis
apply -
apply (erule decompose_small_step[OF _ R])
apply (erule decompose_small_step[OF _ R])
subgoal for c cs aft c' cs' aft'
apply (frule fragments_basic_com[where c'=c])
apply (frule fragments_basic_com[where c'=c'])
apply (elim basic_com.cases; clarsimp elim!: small_step_inv)
apply (drule fragments_vcg_fragments')
apply (fastforce dest!: V[rule_format]
elim: vcg_inv elim!: small_step_inv
simp: LST_def AT_def taken_def fun_eq_iff)+
done
done
qed
text‹
The user sees the conclusion of ‹V› for each element of @{const ‹vcg_fragments›}.
›
lemma VCG_step_inv_stable:
assumes V: "⋀p. ∀(c, aft) ∈ vcg_fragments (PGMs sys p). PGMs sys, p, aft ⊢ ⦃I⦄ c"
assumes "prerun sys σ"
shows "(⌈I⌉ ❙↪ ○⌈I⌉) σ"
apply (rule alwaysI)
apply clarsimp
apply (rule nextI)
apply clarsimp
using assms(2) unfolding prerun_def
apply clarsimp
apply (erule_tac i=i in alwaysE)
unfolding system_step_reflclp_def
apply clarsimp
apply (erule disjE; clarsimp)
using VCG_step[where pre=I and post=I] V assms(2) prerun_reachable_state
apply blast
done
lemma VCG:
assumes I: "∀s. initial_state sys s ⟶ I (⦇GST = s, HST = []⦈)"
assumes V: "⋀p. ∀(c, aft) ∈ vcg_fragments (PGMs sys p). PGMs sys, p, aft ⊢ ⦃I⦄ c"
shows "sys ⊨⇘pre⇙ I"
apply (rule prerun_valid_induct)
apply (clarsimp simp: prerun_def state_prop_def)
apply (metis (full_types) I old.unit.exhaust system_state.surjective)
using VCG_step_inv_stable[OF V] apply blast
done
lemmas VCG_valid = valid_prerun_lift[OF VCG, of sys I] for sys I
end