Theory Promela.PromelaInvariants
section "Invariants for Promela data structures"
theory PromelaInvariants
imports PromelaDatastructures
begin
text ‹
The different data structures used in the Promela implementation require different invariants,
which are specified in this file. As there is no (useful) way of specifying \emph{correctness} of the implementation,
those invariants are tailored towards proving the finitness of the generated state-space.
›
lemma foldli_set:
"set (foldli list (λ_. True) (#) xs) = set xs ∪ set list"
by (induct list arbitrary: xs) simp_all
lemma foldli_conj:
"foldli list id (λkv σ. P kv) b ⟷ b ∧ (∀x ∈ set list. P x)"
by (induct list arbitrary: b) simp_all
lemma lm_ball_Assoc_List_set:
"lm.ball m P ⟷ (∀x ∈ Assoc_List.set m. P x)"
unfolding Assoc_List.set_def
by (simp add: icf_rec_unf lm_basic.g_ball_def
poly_map_iteratei_defs.iteratei_def it_to_it_def Assoc_List.iteratei_def
foldli_conj)
lemma lm_to_list_Assoc_List_set:
"set (lm.to_list l) = Assoc_List.set l"
unfolding Assoc_List.set_def
by (simp add: icf_rec_unf lm_basic.g_to_list_def
poly_map_iteratei_defs.iteratei_def it_to_it_def Assoc_List.iteratei_def
foldli_set)
lemma dom_lm_α_Assoc_List_set:
"dom (lm.α v) = fst ` (Assoc_List.set v)"
by (simp add: icf_rec_unf Assoc_List.lookup_def Assoc_List.set_def
dom_map_of_conv_image_fst)
lemma ran_lm_α_Assoc_List_set:
"ran (lm.α v) = snd ` (Assoc_List.set v)"
by (simp add: icf_rec_unf Assoc_List.lookup_def Assoc_List.set_def
ran_distinct)
lemma lm_ball_eq_ran:
"lm.ball v (λ(k,v). P v) ⟷ ran (lm.α v) ⊆ Collect P"
by (auto simp add: ran_lm_α_Assoc_List_set lm_ball_Assoc_List_set)
lemma lm_ball_lm_to_map_map_weaken:
"∀x ∈ f ` set xs. P x ⟹ lm.ball (lm.to_map (map f xs)) P"
by (induct xs) (simp_all add: lm.correct)
lemma Assoc_List_set_eq_lookup:
"(k,v) ∈ Assoc_List.set vs ⟷ Assoc_List.lookup vs k = Some v"
by (simp add: Assoc_List.lookup_def Assoc_List.set_def)
subsection ‹Bounds›
text ‹
Finiteness requires that possible variable ranges are finite, as is the maximium number of processes.
Currently, they are supplied here as constants. In a perfect world, they should be able to be set dynamically.
›
definition min_var_value :: "integer" where
"min_var_value = -(2^31)"
definition max_var_value :: "integer" where
"max_var_value = (2^31) - 1"
lemma min_max_var_value_simps [simp, intro!]:
"min_var_value < max_var_value"
"min_var_value < 0"
"min_var_value ≤ 0"
"max_var_value > 0"
"max_var_value ≥ 0"
by (simp_all add: min_var_value_def max_var_value_def)
definition "max_procs ≡ 255"
definition "max_channels ≡ 65535"
definition "max_array_size = 65535"
subsection ‹Variables and similar›
fun varType_inv :: "varType ⇒ bool" where
"varType_inv (VTBounded l h)
⟷ l ≥ min_var_value ∧ h ≤ max_var_value ∧ l < h"
| "varType_inv VTChan ⟷ True"
fun variable_inv :: "variable ⇒ bool" where
"variable_inv (Var t val)
⟷ varType_inv t ∧ val ∈ {min_var_value..max_var_value}"
| "variable_inv (VArray t sz ar)
⟷ varType_inv t
∧ sz ≤ max_array_size
∧ IArray.length ar = sz
∧ set (IArray.list_of ar) ⊆ {min_var_value..max_var_value}"
fun channel_inv :: "channel ⇒ bool" where
"channel_inv (Channel cap ts q)
⟷ cap ≤ max_array_size
∧ cap ≥ 0
∧ set ts ⊆ Collect varType_inv
∧ length ts ≤ max_array_size
∧ length q ≤ max_array_size
∧ (∀x ∈ set q. length x = length ts
∧ set x ⊆ {min_var_value..max_var_value})"
| "channel_inv (HSChannel ts)
⟷ set ts ⊆ Collect varType_inv ∧ length ts ≤ max_array_size"
| "channel_inv InvChannel ⟷ True"
lemma varTypes_finite:
"finite (Collect varType_inv)"
proof (rule finite_subset)
show "Collect (varType_inv) ⊆
{VTChan}
∪ (λ(l,h). VTBounded l h)
` ({min_var_value..max_var_value} × {min_var_value..max_var_value})"
apply (rule subsetI)
apply (case_tac x)
apply auto
done
show "finite ..." by auto
qed
lemma variables_finite:
"finite (Collect variable_inv)"
proof (rule finite_subset)
let ?mm = "{min_var_value..max_var_value}"
let ?V1 = "(λ(t,val). Var t val) ` ({vt. varType_inv vt} × ?mm)"
let ?V2 = "(λ(t,sz,ar). VArray t sz ar)
` ({vt. varType_inv vt}
× {0..max_array_size}
× {ar. IArray.length ar ≤ max_array_size
∧ set (IArray.list_of ar) ⊆ ?mm})"
{
fix A :: "'a set"
let ?LS = "{xs. set xs ⊆ A ∧ length xs ≤ max_array_size }"
let ?AS = "{ar. IArray.length ar ≤ max_array_size
∧ set (IArray.list_of ar) ⊆ A}"
assume "finite A"
hence "finite ?LS" by (simp add: finite_lists_length_le)
moreover have "?AS ⊆ IArray ` ?LS"
apply (auto simp: image_def)
apply (rule_tac x = "IArray.list_of x" in exI)
apply auto
apply (metis iarray.exhaust list_of.simps)
done
ultimately have "finite ?AS" by (auto simp add: finite_subset)
} note finite_arr = this
show "Collect variable_inv ⊆ (?V1 ∪ ?V2)"
apply (rule subsetI)
apply (case_tac x)
apply (auto simp add: image_def)
done
show "finite ..." by (blast intro: varTypes_finite finite_arr)
qed
lemma channels_finite:
"finite (Collect channel_inv)"
proof (rule finite_subset)
let ?C1 =
"(λ(cap,ts,q). Channel cap ts q)
` ({0..max_array_size}
× {ts. set ts ⊆ Collect varType_inv ∧ length ts ≤ max_array_size}
× {q. set q ⊆ {x. set x ⊆ {min_var_value..max_var_value}
∧ length x ≤ max_array_size}
∧ length q ≤ max_array_size})"
let ?C2 =
"HSChannel ` {ts. set ts ⊆ Collect varType_inv ∧ length ts ≤ max_array_size}"
let ?C3 = "{InvChannel}"
show "(Collect channel_inv) ⊆ ?C1 ∪ ?C2 ∪ ?C3"
apply (rule subsetI)
apply (case_tac x)
apply (auto simp add: image_def)
done
show "finite ..." by (blast intro: finite_lists_length_le varTypes_finite)+
qed
text ‹To give an upper bound of variable names, we need a way to calculate it.›
primrec procArgName :: "procArg ⇒ String.literal" where
"procArgName (ProcArg _ name) = name"
primrec varDeclName :: "varDecl ⇒ String.literal" where
"varDeclName (VarDeclNum _ _ name _ _) = name"
| "varDeclName (VarDeclChan name _ _) = name"
primrec procVarDeclName :: "procVarDecl ⇒ String.literal" where
"procVarDeclName (ProcVarDeclNum _ _ name _ _) = name"
| "procVarDeclName (ProcVarDeclChan name _) = name"
definition edgeDecls :: "edge ⇒ procVarDecl set" where
"edgeDecls e = (
case effect e of
EEDecl p ⇒ {p}
| _ ⇒ {})"
lemma edgeDecls_finite:
"finite (edgeDecls e)"
by (simp add: edgeDecls_def split: edgeEffect.split)
definition edgeSet :: "states ⇒ edge set" where
"edgeSet s = set (concat (map snd (IArray.list_of s)))"
lemma edgeSet_finite:
"finite (edgeSet s)"
by (simp add: edgeSet_def)
definition statesDecls :: "states ⇒ procVarDecl set" where
"statesDecls s = ⋃(edgeDecls ` (edgeSet s))"
definition statesNames :: "states ⇒ String.literal set" where
"statesNames s = procVarDeclName ` statesDecls s"
lemma statesNames_finite:
"finite (statesNames s)"
by (simp add: edgeSet_finite edgeDecls_finite statesNames_def statesDecls_def)
fun process_names :: "states ⇒ process ⇒ String.literal set" where
"process_names ss (_, _, args, decls) =
statesNames ss
∪ procArgName ` set args
∪ varDeclName ` set decls
∪ {STR ''_'', STR ''__assert__'', STR ''_pid''}"
lemma process_names_finite:
"finite (process_names ss p)"
by (cases p) (simp add: statesNames_finite)
definition vardict_inv :: "states ⇒ process ⇒ var_dict ⇒ bool" where
"vardict_inv ss p vs
⟷ lm.ball vs (λ(k,v). k ∈ process_names ss p ∧ variable_inv v)"
lemma vardicts_finite:
"finite (Collect (vardict_inv ss p))"
proof -
have "Assoc_List.set ` Collect (vardict_inv ss p) ⊆
Pow (process_names ss p × {v. variable_inv v})"
by (auto simp add: lm_ball_Assoc_List_set vardict_inv_def)
moreover have "finite ..."
using process_names_finite variables_finite
by simp
ultimately show ?thesis by (metis finite_Assoc_List_set_image finite_subset)
qed
lemma lm_to_map_vardict_inv:
assumes "∀(k,v) ∈ set xs. k ∈ process_names ss proc ∧ variable_inv v"
shows "vardict_inv ss proc (lm.to_map xs)"
using assms
unfolding vardict_inv_def
by (auto simp add: lm.correct dest: map_of_SomeD)
subsection ‹Invariants of a process›
definition pState_inv :: "program ⇒ pState ⇒ bool" where
"pState_inv prog p
⟷ pid p ≤ max_procs
∧ pState.idx p < IArray.length (states prog)
∧ IArray.length (states prog) = IArray.length (processes prog)
∧ pc p < IArray.length ((states prog) !! pState.idx p)
∧ set (pState.channels p) ⊆ {-1..<integer_of_nat max_channels}
∧ length (pState.channels p) ≤ max_channels
∧ vardict_inv ((states prog) !! pState.idx p)
((processes prog) !! pState.idx p)
(pState.vars p)"
lemma pStates_finite:
"finite (Collect (pState_inv prog))"
proof -
let ?P1 = "{..max_procs::nat}"
let ?P2 = "{..IArray.length (states prog)}"
let ?P3 = "{..Max (IArray.length ` (set (IArray.list_of (states prog))))}"
let ?P4 = "{cs. set cs ⊆ {-1..<integer_of_nat max_channels}
∧ length cs ≤ max_channels}"
let ?P5 = "⋃x∈{..IArray.length (states prog)}.
Collect (vardict_inv (states prog !! x) (processes prog !! x))"
let ?P = "?P1 × ?P2 × ?P3 × ?P4 × ?P5"
have "{p. pState_inv prog p} ⊆
(λ(pid,idx,pc,channels,vars). pState.make pid vars pc channels idx) ` ?P"
unfolding pState_inv_def image_def [of _ ?P]
apply (clarsimp simp add: pState.defs)
apply (tactic ‹Record.split_simp_tac @{context} [] (K ~1) 1›)
apply auto
apply (rule order_trans [OF less_imp_le])
apply (auto intro!: Max_ge)
done
moreover
have "finite ?P4" by (fastforce intro: finite_lists_length_le)
hence "finite ?P" by (auto intro: finite_cartesian_product simp: vardicts_finite)
ultimately show ?thesis by (elim finite_subset) (rule finite_imageI)
qed
text ‹
Throughout the calculation of the semantic engine, a modified process is not necessarily part of @{term "procs g"}.
Hence we need to establish an additional constraint for the relation between a global and a process state.›
definition cl_inv :: "('a gState_scheme * pState) ⇒ bool" where
"cl_inv gp = (case gp of (g,p) ⇒
length (pState.channels p) ≤ length (gState.channels g))"
lemma cl_inv_lengthD:
"cl_inv (g,p) ⟹ length (pState.channels p) ≤ length (gState.channels g)"
unfolding cl_inv_def
by auto
lemma cl_invI:
"length (pState.channels p) ≤ length (gState.channels g) ⟹ cl_inv (g,p)"
unfolding cl_inv_def by auto
lemma cl_inv_trans:
"length (channels g) ≤ length (channels g') ⟹ cl_inv (g,p) ⟹ cl_inv (g',p)"
by (simp add: cl_inv_def)
lemma cl_inv_vars_update[intro!]:
"cl_inv (g,p) ⟹ cl_inv (g, pState.vars_update vs p)"
"cl_inv (g,p) ⟹ cl_inv (gState.vars_update vs g, p)"
by (simp_all add: cl_inv_def)
lemma cl_inv_handshake_update[intro!]:
"cl_inv (g,p) ⟹ cl_inv (g⦇handshake := h⦈,p)"
by (simp add: cl_inv_def)
lemma cl_inv_hsdata_update[intro!]:
"cl_inv (g,p) ⟹ cl_inv (g⦇hsdata := h⦈,p)"
by (simp add: cl_inv_def)
lemma cl_inv_procs_update[intro!]:
"cl_inv (g,p) ⟹ cl_inv (g⦇procs := ps⦈,p)"
by (simp add: cl_inv_def)
lemma cl_inv_channels_update:
assumes "cl_inv (g,p)"
shows "cl_inv (gState.channels_update (λcs. cs[i:=c]) g, p)"
using assms unfolding cl_inv_def
by simp
subsection ‹Invariants of the global state›
text ‹Note that @{term gState_inv} must be defined in a way to be applicable to both @{typ gState} and @{typ gState⇩I}.›
definition gState_inv :: "program ⇒ 'a gState_scheme ⇒ bool" where
"gState_inv prog g
⟷ length (procs g) ≤ max_procs
∧ (∀p ∈ set (procs g). pState_inv prog p ∧ cl_inv (g,p))
∧ length (channels g) ≤ max_channels
∧ set (channels g) ⊆ Collect channel_inv
∧ lm.ball (vars g) (λ(k,v). variable_inv v)"
text ‹The set of global states adhering to the terms of @{const gState_inv} is not finite.
But the set of all global states that can be constructed by the semantic engine from one starting state is.
Thus we establish a progress relation, \ie all successors of a state @{term g} relate to @{term g} under this specification.›
definition gState_progress_rel :: "program ⇒ ('a gState_scheme) rel" where
"gState_progress_rel p = {(g,g'). gState_inv p g ∧ gState_inv p g'
∧ length (channels g) ≤ length (channels g')
∧ dom (lm.α (vars g)) = dom (lm.α (vars g'))}"
lemma gState_progress_rel_gState_invI1[intro]:
"(g,g') ∈ gState_progress_rel prog ⟹ gState_inv prog g"
by (simp add: gState_progress_rel_def)
lemma gState_progress_rel_gState_invI2[intro]:
"(g,g') ∈ gState_progress_rel prog ⟹ gState_inv prog g'"
by (simp add: gState_progress_rel_def)
lemma gState_progress_relI:
assumes "gState_inv prog g"
and "gState_inv prog g'"
and "length (channels g) ≤ length (channels g')"
and "dom (lm.α (vars g)) = dom (lm.α (vars g'))"
shows "(g,g') ∈ gState_progress_rel prog"
unfolding gState_progress_rel_def
using assms
by auto
lemma gState_progress_refl[simp,intro!]:
"gState_inv prog g ⟹ (g,g) ∈ (gState_progress_rel prog)"
unfolding gState_progress_rel_def
by auto
lemma refl_on_gState_progress_rel:
"refl_on (Collect (gState_inv prog)) (gState_progress_rel prog)"
by (auto intro!: refl_onI)
lemma trans_gState_progress_rel[simp]:
"trans (gState_progress_rel prog)"
by (intro transI) (simp add: gState_progress_rel_def)
lemmas gState_progress_rel_trans [trans] = trans_gState_progress_rel[THEN transD]
lemma gState_progress_rel_trancl_id[simp]:
"(gState_progress_rel prog)⇧+ = gState_progress_rel prog"
by simp
lemma gState_progress_rel_rtrancl_absorb:
assumes "gState_inv prog g"
shows "(gState_progress_rel prog)⇧* `` {g} = gState_progress_rel prog `` {g}"
using assms refl_on_gState_progress_rel
by (intro Image_absorb_rtrancl) auto
text ‹
The main theorem: The set of all global states reachable from an initial state, is finite.
›
lemma gStates_finite:
fixes g :: "gState"
shows "finite ((gState_progress_rel prog)⇧* `` {g})"
proof (cases "gState_inv prog g")
case False hence "(gState_progress_rel prog)⇧* `` {g} = {g}"
by (intro Image_empty_rtrancl_Image_id)
(auto simp add: gState_progress_rel_def)
thus ?thesis by simp
next
case True
let ?G1 = "{m. dom (lm.α m) = dom (lm.α (vars g))
∧ ran (lm.α m) ⊆ Collect variable_inv }"
let ?G2 = "{cs. set cs ⊆ Collect channel_inv
∧ length cs ≤ max_channels}"
let ?G3 = "{True, False}"
let ?G4 = "{ps. set ps ⊆ Collect (pState_inv prog)
∧ length ps ≤ max_procs}"
let ?G = "?G1 × ?G2 × ?G3 × ?G4"
let ?G' = "(λ(vars,chans,t,ps). gState.make vars chans t ps) ` ?G"
have G1: "finite ?G1"
proof (rule finite_subset)
show "?G1 ⊆ {v'. fst ` Assoc_List.set v' = fst ` Assoc_List.set (vars g)
∧ snd ` Assoc_List.set v' ⊆ Collect variable_inv}"
by (simp add: dom_lm_α_Assoc_List_set ran_lm_α_Assoc_List_set)
show "finite ..." (is "finite ?X")
proof (rule finite_Assoc_List_set_image, rule finite_subset)
show "Assoc_List.set ` ?X ⊆
Pow (fst ` Assoc_List.set (vars g) × Collect variable_inv)"
by auto
show "finite ..." by (auto simp add: variables_finite dom_lm_α_Assoc_List_set[symmetric])
qed
qed
have "finite ((gState_progress_rel prog) `` {g})"
proof (rule finite_subset)
show "(gState_progress_rel prog) `` {g} ⊆
(λ(vars,chans,t,ps). gState.make vars chans t ps) ` ?G"
apply (clarsimp simp add: image_def gState_inv_def gState.defs gState_progress_rel_def)
apply (rule_tac x = "vars x" in exI)
apply (simp add: lm_ball_eq_ran)
apply (rule_tac x = "channels x" in exI)
apply (case_tac "timeout x")
apply clarsimp
apply (rule_tac x="procs x" in exI)
apply auto
done
show "finite ..." using G1
by (blast intro: finite_lists_length_le channels_finite pStates_finite)
qed
with gState_progress_rel_rtrancl_absorb[OF True] show ?thesis by simp
qed
lemma gState_progress_rel_channels_update:
assumes "gState_inv prog g"
and "channel_inv c"
and "i < length (channels g)"
shows "(g,gState.channels_update (λcs. cs[i:=c]) g) ∈ gState_progress_rel prog"
using assms
by (auto intro!: gState_progress_relI
simp add: gState_inv_def cl_inv_def
dest!: subsetD[OF set_update_subset_insert])
lemma gState_progress_rel_channels_update_step:
assumes "gState_inv prog g"
and step: "(g,g') ∈ gState_progress_rel prog"
and "channel_inv c"
and "i < length (channels g')"
shows "(g,gState.channels_update (λcs. cs[i:=c]) g') ∈ gState_progress_rel prog"
proof -
note step
also hence "gState_inv prog g'" by blast
note gState_progress_rel_channels_update[OF this assms(3,4)]
finally show ?thesis .
qed
subsection ‹Invariants of the program›
text ‹
Naturally, we need our program to also adhere to certain invariants. Else we can't show, that
the generated states are correct according to the invariants above.
›
definition program_inv where
"program_inv prog
⟷ IArray.length (states prog) > 0
∧ IArray.length (states prog) = IArray.length (processes prog)
∧ (∀s ∈ set (IArray.list_of (states prog)). IArray.length s > 0)
∧ lm.ball (proc_data prog)
(λ(_,sidx).
sidx < IArray.length (processes prog)
∧ fst (processes prog !! sidx) = sidx)
∧ (∀(sidx,start,procArgs,args) ∈ set (IArray.list_of (processes prog)).
(∃s. start = Index s ∧ s < IArray.length (states prog !! sidx)))"
lemma program_inv_length_states:
assumes "program_inv prog"
and "n < IArray.length (states prog)"
shows "IArray.length (states prog !! n) > 0"
using assms by (simp add: program_inv_def)
lemma program_invI:
assumes "0 < IArray.length (states prog)"
and "IArray.length (states prog) = IArray.length (processes prog)"
and "⋀s. s ∈ set (IArray.list_of (states prog))
⟹ 0 < IArray.length s"
and "⋀sidx. sidx ∈ ran (lm.α (proc_data prog))
⟹ sidx < IArray.length (processes prog)
∧ fst (processes prog !! sidx) = sidx"
and "⋀sidx start procArgs args.
(sidx,start,procArgs,args) ∈ set (IArray.list_of (processes prog))
⟹ ∃s. start = Index s ∧ s < IArray.length (states prog !! sidx)"
shows "program_inv prog"
unfolding program_inv_def
using assms
by (auto simp add: lm_ball_eq_ran)
end