Theory CAVA_Impl
section ‹Actual Implementation of the CAVA Model Checker›
theory CAVA_Impl
imports
CAVA_Abstract
CAVA_Automata.Automata_Impl
LTL.Rewriting
LTL_to_GBA.LTL_to_GBA_impl
Gabow_SCC.Gabow_GBG_Code
"Nested_DFS/NDFS_SI"
"BoolProgs/BoolProgs"
"BoolProgs/Programs/BoolProgs_Programs"
"BoolProgs/BoolProgs_LTL_Conv"
Promela.PromelaLTL
Promela.PromelaLTLConv
"HOL-Library.AList_Mapping"
CAVA_Base.CAVA_Code_Target
SM.SM_Wrapup
begin
hide_const (open) SM_Cfg.cfg
subsection ‹Miscellaneous Lemmata›
instantiation uint32 :: hashable begin
definition "hashcode x = x"
definition "def_hashmap_size (T::uint32 itself) ≡ 8"
instance
apply intro_classes
unfolding def_hashmap_size_uint32_def
by auto
end
subsection ‹Exporting Graphs›
definition "frv_edge_set G ≡ g_E G ∩ (g_V G × UNIV)"
definition "frv_edge_set_aimpl G ≡ FOREACHi (λit r. r = g_E G ∩ ((g_V G - it) × UNIV))
(g_V G)
(λu r. do {
let E = (λv. (u,v))`(succ_of_E (g_E G) u);
ASSERT (E ∩ r = {});
RETURN (E ∪ r)
})
{}"
lemma frv_edge_set_aimpl_correct:
"finite (g_V G) ⟹ frv_edge_set_aimpl G ≤ SPEC (λr. r = frv_edge_set G)"
unfolding frv_edge_set_aimpl_def frv_edge_set_def
apply (refine_rcg refine_vcg)
apply auto []
apply auto []
apply (auto simp: succ_of_E_def) []
apply auto []
done
schematic_goal frv_edge_set_impl_aux:
assumes [autoref_rules]: "(eq,(=))∈R → R → bool_rel"
assumes [relator_props]: "single_valued R"
shows "(?c, frv_edge_set_aimpl) ∈ ⟨Rx,R⟩frgv_impl_rel_ext → ⟨⟨R ×⇩r R⟩list_set_rel⟩nres_rel"
unfolding frv_edge_set_aimpl_def[abs_def]
apply (autoref (trace,keep_goal))
done
concrete_definition frv_edge_set_impl uses frv_edge_set_impl_aux
lemmas [autoref_rules] = frv_edge_set_impl.refine[OF GEN_OP_D PREFER_sv_D]
schematic_goal frv_edge_set_code_aux: "RETURN ?c ≤ frv_edge_set_impl eq G"
unfolding frv_edge_set_impl_def by (refine_transfer (post))
concrete_definition frv_edge_set_code for eq G uses frv_edge_set_code_aux
lemmas [refine_transfer] = frv_edge_set_code.refine
lemma frv_edge_set_autoref[autoref_rules]:
assumes EQ[unfolded autoref_tag_defs]: "GEN_OP eq (=) (R → R → bool_rel)"
assumes SV[unfolded autoref_tag_defs]: "PREFER single_valued R"
shows "(frv_edge_set_code eq,frv_edge_set) ∈ ⟨Rx,R⟩frgv_impl_rel_ext → ⟨R ×⇩r R⟩list_set_rel"
proof (intro fun_relI)
fix Gi G
assume Gr: "(Gi, G) ∈ ⟨Rx, R⟩frgv_impl_rel_ext"
hence [simp]: "finite (g_V G)"
unfolding frgv_impl_rel_ext_def g_impl_rel_ext_def
gen_g_impl_rel_ext_def
apply (simp add: list_set_rel_def br_def)
apply fastforce
done
note frv_edge_set_code.refine
also note frv_edge_set_impl.refine[OF EQ SV, THEN fun_relD, OF Gr, THEN nres_relD]
also note frv_edge_set_aimpl_correct
finally show "(frv_edge_set_code eq Gi, frv_edge_set G) ∈ ⟨R ×⇩r R⟩list_set_rel"
by (rule RETURN_ref_SPECD) simp_all
qed
definition "frv_export G ≡ do {
nodes ← SPEC (λl. set l = g_V G ∧ distinct l);
V0 ← SPEC (λl. set l = g_V0 G ∧ distinct l);
E ← SPEC (λl. set l = frv_edge_set G ∧ distinct l);
RETURN (nodes,V0,E)
}"
schematic_goal frv_export_impl_aux:
fixes R :: "('vi × 'v) set"
notes [autoref_tyrel] = TYRELI[where R = "⟨R ×⇩r R⟩list_set_rel"]
assumes EQ[autoref_rules]: "(eq,(=))∈R → R → bool_rel"
assumes SVR[relator_props]: "single_valued R"
shows "(?c, frv_export)
∈ ⟨Rx,R⟩frgv_impl_rel_ext
→ ⟨⟨R⟩list_rel ×⇩r ⟨R⟩list_rel ×⇩r ⟨R ×⇩r R⟩list_rel⟩nres_rel"
unfolding frv_export_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal, trace))
done
concrete_definition frv_export_impl for eq uses frv_export_impl_aux
lemmas [autoref_rules] = frv_export_impl.refine[OF GEN_OP_D PREFER_sv_D]
schematic_goal frv_export_code_aux: "RETURN ?c ≤ frv_export_impl eq G"
unfolding frv_export_impl_def
apply (refine_transfer (post))
done
concrete_definition frv_export_code for eq G uses frv_export_code_aux
lemmas [refine_transfer] = frv_export_code.refine
subsection ‹Setup›
subsubsection ‹LTL to GBA conversion›
text ‹In the following, we set up the algorithms for LTL to GBA conversion.›
definition is_ltl_to_gba_algo
:: "('a ltlc ⇒ (nat, 'a ⇒ bool, unit) igbav_impl_scheme) ⇒ bool"
where
"is_ltl_to_gba_algo algo ≡ (algo, ltl_to_gba_spec)
∈ ltl_rel
→ ⟨igbav_impl_rel_ext unit_rel nat_rel (⟨Id⟩fun_set_rel)⟩plain_nres_rel"
definition gerth_ltl_to_gba
where "gerth_ltl_to_gba φ ≡ create_name_igba (ltln_to_ltlr (simplify Slow (ltlc_to_ltln φ)))"
lemma gerth_ltl_to_gba_refine:
"gerth_ltl_to_gba φ ≤ ⇓Id (ltl_to_gba_spec φ)"
apply simp
unfolding ltl_to_gba_spec_def gerth_ltl_to_gba_def
apply (rule order_trans[OF create_name_igba_correct])
apply (rule SPEC_rule)
proof (safe del: equalityI)
fix G :: "(nat, 'a set) igba_rec"
assume "igba G"
interpret igba G by fact
assume 1: "finite (g_V G)"
assume 2: "∀ ξ. accept ξ ⟷ ξ ⊨⇩r ltln_to_ltlr (simplify Slow (ltlc_to_ltln φ))"
show "lang = language_ltlc φ"
using 2 unfolding lang_def language_ltlc_def ltln_to_ltlr_semantics simplify_correct ltlc_to_ltln_semantics by auto
show "finite ((g_E G)⇧* `` g_V0 G)" using 1 reachable_V by auto
qed
definition "gerth_ltl_to_gba_code φ ≡ create_name_igba_code (ltln_to_ltlr (simplify Slow (ltlc_to_ltln φ)))"
lemma gerth_ltl_to_gba_code_refine: "is_ltl_to_gba_algo gerth_ltl_to_gba_code"
proof -
have "⋀φ. RETURN (gerth_ltl_to_gba_code φ)
≤ ⇓(igbav_impl_rel_ext unit_rel nat_rel (⟨Id⟩fun_set_rel))
(gerth_ltl_to_gba φ)"
unfolding gerth_ltl_to_gba_def[abs_def] gerth_ltl_to_gba_code_def[abs_def]
apply (rule order_trans[OF create_name_igba_code.refine])
apply (rule create_name_igba_impl.refine[THEN fun_relD, THEN nres_relD])
apply simp
apply simp
done
also note gerth_ltl_to_gba_refine
finally show ?thesis
unfolding is_ltl_to_gba_algo_def
by (blast intro: plain_nres_relI)
qed
text ‹We define a function that chooses between the possible conversion
algorithms. (Currently there is only one)›
datatype config_l2b = CFG_L2B_GERTHS
definition "ltl_to_gba_code cfg
≡ case cfg of CFG_L2B_GERTHS ⇒ gerth_ltl_to_gba_code"
lemma ltl_to_gba_code_refine:
"is_ltl_to_gba_algo (ltl_to_gba_code cfg)"
apply (cases cfg)
unfolding ltl_to_gba_code_def
using gerth_ltl_to_gba_code_refine
apply simp
done
subsubsection ‹Counterexample Search›
definition is_find_ce_algo
:: "(('a, unit)igbg_impl_scheme ⇒ 'a lasso option option) ⇒ bool"
where
"is_find_ce_algo algo ≡ (algo, find_ce_spec)
∈ igbg_impl_rel_ext unit_rel Id
→ ⟨⟨⟨⟨Id⟩lasso_run_rel⟩Relators.option_rel⟩Relators.option_rel⟩plain_nres_rel"
definition gabow_find_ce_code :: "_ ⇒ 'a::hashable lasso option option"
where "gabow_find_ce_code
≡ map_option (Some o lasso_of_prpl) o Gabow_GBG_Code.find_lasso_tr (=) bounded_hashcode_nat (def_hashmap_size TYPE('a))"
lemma gabow_find_ce_code_refine: "is_find_ce_algo
(gabow_find_ce_code
:: ('a::hashable, unit) igbg_impl_scheme ⇒ 'a lasso option option)"
proof -
have AUX_EQ:
"⋀gbgi::('a, unit) igbg_impl_scheme. RETURN (gabow_find_ce_code gbgi)
= (do {
l ← RETURN (find_lasso_tr (=) bounded_hashcode_nat (def_hashmap_size TYPE('a)) gbgi);
RETURN (map_option (Some ∘ lasso_of_prpl) l)
})" by (auto simp: gabow_find_ce_code_def)
show ?thesis
unfolding is_find_ce_algo_def
apply (intro fun_relI plain_nres_relI)
unfolding find_ce_spec_def AUX_EQ
apply (refine_rcg)
apply (rule order_trans[
OF bind_mono(1)[OF Gabow_GBG_Code.find_lasso_tr_correct order_refl]])
apply assumption
apply (simp; fail)
apply (rule autoref_ga_rules;simp; fail)
apply (rule autoref_ga_rules;simp; fail)
apply (rule igb_fr_graphI)
apply assumption
apply assumption
unfolding igb_graph.find_lasso_spec_def
apply (simp add: pw_le_iff refine_pw_simps)
apply (clarsimp simp: lasso_run_rel_sv option_rel_sv split: option.split_asm)
apply (metis igb_graph.is_lasso_prpl_of_lasso igb_graph.accepted_lasso
prod.exhaust)
apply (simp add: option_rel_def lasso_run_rel_def br_def)
by (metis igb_graph.is_lasso_prpl_conv igb_graph.lasso_accepted)
qed
definition ndfs_find_ce
:: "('q::hashable,_) igb_graph_rec_scheme ⇒ 'q lasso option option nres"
where
"ndfs_find_ce G ≡ do {
ASSERT (igb_graph G);
let G = igb_graph.degeneralize G;
l ← blue_dfs G;
case l of
None ⇒ RETURN None
| Some l ⇒ do {
ASSERT (snd l ≠ []);
RETURN (Some (Some (map_lasso fst (lasso_of_prpl l))))
}
}"
lemma ndfs_find_ce_refine: "(G',G)∈Id ⟹
ndfs_find_ce G' ≤ ⇓(⟨⟨⟨Id⟩lasso_run_rel⟩option_rel⟩option_rel) (find_ce_spec G)"
apply simp
unfolding find_ce_spec_def
proof (refine_rcg SPEC_refine refine_vcg)
assume [simp]: "igb_graph G"
then interpret igb_graph G .
assume fr: "finite ((g_E G)⇧* `` g_V0 G)"
have [simp]: "b_graph degeneralize" by (simp add: degen_invar)
show "ndfs_find_ce G
≤
(SPEC (λres. ∃res'.
(res,res')∈(⟨⟨⟨Id⟩lasso_run_rel⟩Relators.option_rel⟩Relators.option_rel)
∧ (case res' of None ⇒ ∀r. ¬ is_acc_run r
| Some None ⇒ Ex is_acc_run
| Some (Some x) ⇒ is_acc_run x)))"
unfolding ndfs_find_ce_def find_lasso_spec_def ce_correct_def
apply (refine_rcg refine_vcg order_trans[OF blue_dfs_correct])
apply (clarsimp_all)
apply (auto intro: degen_finite_reachable fr) []
apply (auto
elim!: degen_acc_run_complete[where m="λ_. ()"]
dest!: degen.accepted_lasso[OF degen_finite_reachable[OF fr]]
simp: degen.is_lasso_prpl_of_lasso[symmetric] prpl_of_lasso_def
simp del: degen.is_lasso_prpl_of_lasso) []
apply (auto
simp: b_graph.is_lasso_prpl_def graph.is_lasso_prpl_pre_def) []
apply (auto split: option.split
simp: degen.is_lasso_prpl_conv lasso_run_rel_def br_def
dest: degen.lasso_accepted degen_acc_run_sound
) []
done
qed
schematic_goal ndfs_find_ce_impl_aux: "(?c, ndfs_find_ce)
∈ igbg_impl_rel_ext Rm Id
→ ⟨
⟨⟨⟨unit_rel,Id::('a::hashable×_) set⟩lasso_rel_ext⟩option_rel⟩option_rel
⟩ nres_rel"
unfolding ndfs_find_ce_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (trace, keep_goal))
done
concrete_definition ndfs_find_ce_impl uses ndfs_find_ce_impl_aux
schematic_goal ndfs_find_ce_code_aux: "RETURN ?c ≤ ndfs_find_ce_impl G"
unfolding ndfs_find_ce_impl_def
by (refine_transfer (post))
concrete_definition ndfs_find_ce_code uses ndfs_find_ce_code_aux
lemma ndfs_find_ce_code_refine: "is_find_ce_algo ndfs_find_ce_code"
unfolding is_find_ce_algo_def
proof (intro fun_relI plain_nres_relI)
fix gbgi :: "('a,unit) igbg_impl_scheme" and gbg :: "'a igb_graph_rec"
assume R: "(gbgi, gbg) ∈ igbg_impl_rel_ext unit_rel Id"
note ndfs_find_ce_code.refine
also note ndfs_find_ce_impl.refine[param_fo, THEN nres_relD, OF R]
also note ndfs_find_ce_refine[OF IdI]
finally show "RETURN (ndfs_find_ce_code gbgi)
≤ ⇓ (⟨⟨⟨Id⟩lasso_run_rel⟩Relators.option_rel⟩Relators.option_rel)
(find_ce_spec gbg)"
by (simp add: lasso_rel_ext_id)
qed
text ‹We define a function that chooses between the emptiness check
algorithms›
datatype config_ce = CFG_CE_SCC_GABOW | CFG_CE_NDFS
definition find_ce_code where "find_ce_code cfg ≡ case cfg of
CFG_CE_SCC_GABOW ⇒ gabow_find_ce_code
| CFG_CE_NDFS ⇒ ndfs_find_ce_code"
lemma find_ce_code_refine: "is_find_ce_algo (find_ce_code cfg)"
apply (cases cfg)
unfolding find_ce_code_def
using gabow_find_ce_code_refine ndfs_find_ce_code_refine
apply (auto split: config_ce.split)
done
subsection ‹System-Agnostic Model-Checker›
text ‹
In this section, we implement the part of the model-checker that does not
depend on the language used to describe the system to be checked.
›
subsubsection ‹Default Implementation of Lazy Intersection›
locale cava_inter_impl_loc =
igba_sys_prod_precond G S
for S :: "('s, 'l set) sa_rec"
and G :: "('q,'l set) igba_rec" +
fixes Gi Si Rq Rs Rl eqq
assumes [autoref_rules]: "(eqq,(=)) ∈ Rq → Rq → bool_rel"
assumes [autoref_rules]: "(Gi,G) ∈ igbav_impl_rel_ext unit_rel Rq Rl"
assumes [autoref_rules]: "(Si,S) ∈ sa_impl_rel_ext unit_rel Rs Rl"
begin
lemma cava_inter_impl_loc_this: "cava_inter_impl_loc S G Gi Si Rq Rs Rl eqq"
by unfold_locales
text ‹TODO/FIXME:
Some black-magic is going on here: The performance of the mc seems to depend on the ordering of states,
so we do some adjustments of the ordering here.
›
lemma prod_impl_aux_alt_cava_reorder:
"prod = (⦇
g_V = Collect (λ(q,s). q ∈ igba.V ∧ s ∈ sa.V),
g_E = E_of_succ (λ(q,s).
if igba.L q (sa.L s) then
(λ(s,q). (q,s))`(LIST_SET_REV_TAG (succ_of_E (sa.E) s)
× (succ_of_E (igba.E) q))
else
{}
),
g_V0 = igba.V0 × sa.V0,
igbg_num_acc = igba.num_acc,
igbg_acc = λ(q,s). if s∈sa.V then igba.acc q else {}
⦈)"
unfolding prod_def
apply (auto simp: succ_of_E_def E_of_succ_def split: if_split_asm)
done
schematic_goal vf_prod_impl_aux_cava_reorder:
shows "(?c, prod) ∈ igbg_impl_rel_ext unit_rel (Rq ×⇩r Rs)"
unfolding prod_impl_aux_alt_cava_reorder[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (trace, keep_goal))
done
lemma (in -) map_concat_map_map_opt:
"map f (concat (map (λxa. map (f' xa) (l1 xa)) l2))
= List.maps (λxa. map (f o f' xa) (l1 xa)) l2"
"((λ(xd, xe). (xe, xd)) ∘ Pair xa) = (λx. (x,xa))"
apply -
apply (induction l2)
apply (auto simp: List.maps_def) [2]
apply auto []
done
concrete_definition (in -) gbav_sys_prod_impl_cava_reorder
for eqq Gi Si
uses cava_inter_impl_loc.vf_prod_impl_aux_cava_reorder[
param_fo, unfolded map_concat_map_map_opt]
lemmas [autoref_rules] =
gbav_sys_prod_impl_cava_reorder.refine[OF cava_inter_impl_loc_this]
context begin interpretation autoref_syn .
lemma [autoref_op_pat]: "prod ≡ OP prod" by simp
end
definition dflt_inter :: "('q × 's) igb_graph_rec × ('q × 's ⇒ 's)"
where "dflt_inter ≡ (prod, snd)"
lemma dflt_inter_refine:
shows "RETURN dflt_inter ≤ inter_spec S G"
unfolding inter_spec_def dflt_inter_def
apply (refine_rcg le_ASSERTI refine_vcg)
proof clarsimp_all
show "igb_graph prod" by (rule prod_invar)
fix r
assume "finite (igba.E⇧* `` igba.V0)" "finite ((g_E S)⇧* `` g_V0 S)"
thus "finite ((g_E prod)⇧* `` g_V0 prod)" using prod_finite_reachable by auto
show "(∃r'. prod.is_acc_run r' ∧ r = snd ∘ r') ⟷
(sa.is_run r ∧ sa.L ∘ r ∈ igba.lang)"
using gsp_correct1 gsp_correct2
apply (auto simp: comp_assoc)
done
qed
schematic_goal dflt_inter_impl_aux:
shows "(?c, dflt_inter)
∈ igbg_impl_rel_ext unit_rel (Rq ×⇩r Rs) ×⇩r (Rq ×⇩r Rs → Rs)"
unfolding dflt_inter_def[abs_def]
using [[autoref_trace_failed_id]]
apply (autoref (keep_goal))
done
concrete_definition (in -) dflt_inter_impl
for eqq Si Gi
uses cava_inter_impl_loc.dflt_inter_impl_aux
lemmas [autoref_rules] = dflt_inter_impl.refine[OF cava_inter_impl_loc_this]
end
definition [simp]: "op_dflt_inter ≡ cava_inter_impl_loc.dflt_inter"
lemma [autoref_op_pat]: "cava_inter_impl_loc.dflt_inter ≡ op_dflt_inter"
by simp
context begin interpretation autoref_syn .
lemma dflt_inter_autoref[autoref_rules]:
fixes G :: "('q,'l set) igba_rec"
fixes S :: "('s, 'l set) sa_rec"
fixes Gi Si Rq Rs Rl eqq
assumes "SIDE_PRECOND (igba G)"
assumes "SIDE_PRECOND (sa S)"
assumes "GEN_OP eqq (=) (Rq → Rq → bool_rel)"
assumes "(Gi,G) ∈ igbav_impl_rel_ext unit_rel Rq Rl"
assumes "(Si,S) ∈ sa_impl_rel_ext unit_rel Rs Rl"
shows "(dflt_inter_impl eqq Si Gi,
(OP op_dflt_inter
::: sa_impl_rel_ext unit_rel Rs Rl
→ igbav_impl_rel_ext unit_rel Rq Rl
→ igbg_impl_rel_ext unit_rel (Rq ×⇩r Rs) ×⇩r (Rq ×⇩r Rs → Rs))$S$G
) ∈ igbg_impl_rel_ext unit_rel (Rq ×⇩r Rs) ×⇩r (Rq ×⇩r Rs → Rs)"
proof -
from assms interpret igba: igba G by simp
from assms interpret sa: sa S by simp
from assms interpret cava_inter_impl_loc S G Gi Si Rq Rs Rl eqq
by unfold_locales simp_all
show ?thesis
apply simp
apply (rule dflt_inter_impl.refine)
apply unfold_locales
done
qed
end
lemma inter_spec_refineI:
assumes "⟦ sa S; igba G ⟧ ⟹ m ≤ ⇓R (inter_spec S G)"
shows "m ≤ ⇓R (inter_spec S G)"
using assms
unfolding inter_spec_def
apply refine_rcg
apply simp
done
lemma dflt_inter_impl_refine:
fixes Rs :: "('si × 's) set"
fixes Rq :: "('qi × 'q) set"
fixes Rprop :: "('pi × 'p) set"
assumes [relator_props]: "single_valued Rs" "Range Rs = UNIV"
"single_valued Rq" "Range Rq = UNIV"
assumes EQ: "(eqq,(=)) ∈ Rq → Rq → bool_rel"
shows "(dflt_inter_impl eqq, inter_spec)
∈ sa_impl_rel_ext unit_rel Rs (⟨Rprop⟩fun_set_rel) →
igbav_impl_rel_ext unit_rel Rq (⟨Rprop⟩fun_set_rel) →
⟨igbg_impl_rel_ext unit_rel (Rq ×⇩r Rs) ×⇩r ((Rq ×⇩r Rs) → Rs)⟩plain_nres_rel"
apply (intro fun_relI plain_nres_relI)
apply (rule inter_spec_refineI)
proof -
fix Si S Gi G
assume R:"(Si,S) ∈ sa_impl_rel_ext unit_rel Rs (⟨Rprop⟩fun_set_rel)"
"(Gi, G) ∈ igbav_impl_rel_ext unit_rel Rq (⟨Rprop⟩fun_set_rel)"
assume "sa S" and "igba G"
then interpret sa: sa S + igba: igba G .
interpret cava_inter_impl_loc S G Gi Si Rq Rs "⟨Rprop⟩fun_set_rel" eqq
apply unfold_locales
using EQ R by simp_all
note RETURN_refine[OF dflt_inter_impl.refine[OF cava_inter_impl_loc_this]]
also note dflt_inter_refine
finally show "RETURN (dflt_inter_impl eqq Si Gi)
≤ ⇓ (igbg_impl_rel_ext unit_rel (Rq ×⇩r Rs) ×⇩r (Rq ×⇩r Rs → Rs))
(inter_spec S G)" .
qed
subsubsection ‹Definition of Model-Checker›
text ‹In this section, we instantiate the parametrized model checker
with the actual implementations.›
setup Locale_Code.open_block
interpretation cava_sys_agn: impl_model_checker
"sa_impl_rel_ext unit_rel Id (⟨Id⟩fun_set_rel)"
"igbav_impl_rel_ext unit_rel Id (⟨Id⟩fun_set_rel)"
"igbg_impl_rel_ext unit_rel (Id ×⇩r Id)"
"⟨Id ×⇩r Id⟩lasso_run_rel" "⟨Id⟩lasso_run_rel"
"ltl_to_gba_code"
"λ_::unit. dflt_inter_impl (=)"
"find_ce_code"
"map_lasso"
apply unfold_locales
apply tagged_solver
apply (rule ltl_to_gba_code_refine[unfolded is_ltl_to_gba_algo_def])
using dflt_inter_impl_refine[of Id Id "(=)" Id] apply simp
using find_ce_code_refine[unfolded is_find_ce_algo_def]
apply simp apply assumption
using map_lasso_run_refine[of Id Id] apply simp
done
setup Locale_Code.close_block
definition "cava_sys_agn ≡ cava_sys_agn.impl_model_check"
text ‹The correctness theorem states correctness of the model checker wrt.\
a model given as system automata. In the following sections, we will then
refine the model description to Boolean programs and Promela.›
theorem cava_sys_agn_correct:
fixes sysi :: "('s::hashable, 'p::linorder ⇒ bool, unit) sa_impl_scheme"
and sys :: "('s, 'p set) sa_rec"
and φ :: "'p ltlc"
and cfg :: "config_l2b × unit × config_ce"
assumes "(sysi, sys) ∈ sa_impl_rel_ext unit_rel Id (⟨Id⟩fun_set_rel)"
and "sa sys" "finite ((g_E sys)⇧* `` g_V0 sys)"
shows "case cava_sys_agn cfg sysi φ of
None ⇒ sa.lang sys ⊆ language_ltlc φ
| Some None ⇒ ¬ sa.lang sys ⊆ language_ltlc φ
| Some (Some L) ⇒
graph_defs.is_run sys (run_of_lasso L)
∧ sa_L sys ∘ (run_of_lasso L) ∉ language_ltlc φ"
using cava_sys_agn.impl_model_check_correct[OF assms, of φ cfg]
unfolding cava_sys_agn_def
by (auto split: option.splits simp: lasso_run_rel_def br_def)
subsection ‹Model Checker for Boolean Programs›
definition bpc_to_sa
:: "bprog × BoolProgs.config ⇒ (BoolProgs.config,nat set) sa_rec"
where
"bpc_to_sa bpc ≡ let (bp,c0)=bpc in
⦇
g_V = UNIV,
g_E = E_of_succ (set o BoolProgs.nexts bp),
g_V0 = {c0},
sa_L = λc. bs_α (snd c)
⦈"
definition bpc_to_sa_impl
:: "bprog × BoolProgs.config
⇒ (BoolProgs.config,nat ⇒ bool,unit) sa_impl_scheme"
where
"bpc_to_sa_impl bpc ≡ let (bp,c0)=bpc in
⦇ gi_V = λ_. True,
gi_E = remdups o BoolProgs.nexts bp,
gi_V0 = [c0],
sai_L = λc i. bs_mem i (snd c)
⦈"
lemma bpc_to_sa_impl_refine: "(bpc_to_sa_impl bpc, bpc_to_sa bpc)
∈ sa_impl_rel_ext unit_rel Id (⟨nat_rel⟩fun_set_rel)"
unfolding bpc_to_sa_impl_def bpc_to_sa_def
unfolding sa_impl_rel_eext_def g_impl_rel_ext_def
unfolding gen_sa_impl_rel_eext_def gen_g_impl_rel_ext_def
apply (clarsimp split: prod.split)
apply (intro conjI)
apply (auto simp: fun_set_rel_def br_def) []
apply (rule E_of_succ_refine[param_fo])
apply (auto simp: list_set_rel_def br_def) []
apply (auto simp: list_set_rel_def br_def) []
apply (auto simp: fun_set_rel_def br_def) []
done
lemma
shows bpc_to_sa_invar: "sa (bpc_to_sa bpc)"
and bpc_to_sa_fr: "finite ((g_E (bpc_to_sa bpc))⇧* `` g_V0 (bpc_to_sa bpc))"
proof -
obtain bp c where [simp]: "bpc = (bp,c)" by (cases bpc)
show "sa (bpc_to_sa bpc)"
apply unfold_locales
apply (simp add: bpc_to_sa_def)
apply (simp add: bpc_to_sa_def)
done
show "finite ((g_E (bpc_to_sa bpc))⇧* `` g_V0 (bpc_to_sa bpc))"
apply (simp add: bpc_to_sa_def)
apply (rule finite_subset[OF _ BoolProgs.reachable_configs_finite[of bp c]])
apply (rule rtrancl_reachable_induct)
apply (auto
intro: BoolProgs.reachable_configs.intros
simp: E_of_succ_def)
done
qed
interpretation bpc_to_sa: sa "bpc_to_sa bpc"
using bpc_to_sa_invar .
lemma bpc_to_sa_run_conv[simp]:
"graph_defs.is_run (bpc_to_sa bpc) = bpc_is_run bpc"
apply (rule ext)
unfolding graph_defs.is_run_def
unfolding bpc_to_sa_def bpc_is_run_def
ipath_def E_of_succ_def
by auto
lemma bpc_to_sa_L_conv[simp]: "sa_L (bpc_to_sa bpc) = bpc_props"
apply (rule ext)
unfolding bpc_to_sa_def bpc_props_def
apply (auto simp: E_of_succ_def split: prod.split)
done
lemma bpc_to_sa_lang_conv[simp]: "sa.lang (bpc_to_sa bpc) = bpc_lang bpc"
unfolding bpc_to_sa.lang_def bpc_to_sa.accept_def[abs_def] bpc_lang_def
by auto
definition "cava_bpc cfg bpc φ ≡ cava_sys_agn cfg (bpc_to_sa_impl bpc) φ"
text ‹
Correctness theorem for the model checker on boolean programs.
Note that the semantics of Boolean programs is given
by @{const "bpc_lang"}.
›
theorem cava_bpc_correct:
"case cava_bpc cfg bpc φ of
None ⇒ bpc_lang bpc ⊆ language_ltlc φ
| Some None ⇒ (¬(bpc_lang bpc ⊆ language_ltlc φ))
| Some (Some ce) ⇒
bpc_is_run bpc (run_of_lasso ce)
∧ bpc_props o run_of_lasso ce ∉ language_ltlc φ"
using cava_sys_agn_correct[OF bpc_to_sa_impl_refine bpc_to_sa_invar bpc_to_sa_fr,
of bpc φ cfg]
unfolding cava_bpc_def
by (auto split: option.split simp: lasso_run_rel_def br_def)
export_code cava_bpc checking SML
subsection ‹Model Checker for Promela Programs›
definition promela_to_sa
:: "PromelaDatastructures.program × APs × gState ⇒ (gState, nat set) sa_rec"
where "promela_to_sa promg ≡ let (prog,APs,g⇩0)=promg in
⦇
g_V = UNIV,
g_E = E_of_succ (ls.α o Promela.nexts_code prog),
g_V0 = {g⇩0},
sa_L = promela_props_ltl APs
⦈"
definition promela_to_sa_impl
:: "PromelaDatastructures.program × APs × gState
⇒ (gState, nat ⇒ bool, unit) sa_impl_scheme" where
"promela_to_sa_impl promg ≡ let (prog,APs,g⇩0)=promg in
⦇ gi_V = λ_. True,
gi_E = ls.to_list o Promela.nexts_code prog,
gi_V0 = [g⇩0],
sai_L = propValid APs
⦈"
lemma promela_to_sa_impl_refine:
shows "(promela_to_sa_impl promg, promela_to_sa promg)
∈ sa_impl_rel_ext unit_rel Id (⟨nat_rel⟩fun_set_rel)"
unfolding promela_to_sa_impl_def promela_to_sa_def
unfolding sa_impl_rel_eext_def g_impl_rel_ext_def
unfolding gen_sa_impl_rel_eext_def gen_g_impl_rel_ext_def
apply (clarsimp split: prod.split)
apply (intro conjI)
apply (auto simp: fun_set_rel_def br_def) []
apply (rule E_of_succ_refine[param_fo])
apply (auto simp: list_set_rel_def br_def ls.correct) []
apply (auto simp: list_set_rel_def br_def) []
apply (auto simp: fun_set_rel_def br_def in_set_member promela_props_ltl_def) []
done
definition "cava_promela cfg ast φ ≡
let
(promg,φ⇩i) = PromelaLTL.prepare cfg ast φ
in
cava_sys_agn (fst cfg) (promela_to_sa_impl promg) φ⇩i"
text ‹
The next theorem states correctness of the Promela model checker.
The correctness is specified for some AST.
›
lemma cava_promela_correct:
shows
"case cava_promela cfg ast φ of
None ⇒ promela_language ast ⊆ language_ltlc φ
| Some None ⇒ (¬(promela_language ast ⊆ language_ltlc φ))
| Some (Some ce) ⇒ promela_is_run ast (run_of_lasso ce)
∧ promela_props o run_of_lasso ce ∉ language_ltlc φ"
proof -
obtain APs φ⇩i where conv: "PromelaLTL.ltl_convert φ = (APs,φ⇩i)"
by (metis prod.exhaust)
obtain prog g⇩0 where ast: "Promela.setUp ast = (prog,g⇩0)"
by (metis prod.exhaust)
let ?promg = "(prog,APs,g⇩0)"
have promela_to_sa_invar: "sa (promela_to_sa ?promg)"
apply unfold_locales
apply (simp add: promela_to_sa_def)
apply (simp add: promela_to_sa_def)
done
have promela_to_sa_fr: "finite ((g_E (promela_to_sa ?promg))⇧* `` g_V0 (promela_to_sa ?promg))"
apply (simp add: promela_to_sa_def)
apply (rule
finite_subset[OF _ Promela.reachable_states_finite[of prog g⇩0]])
apply (rule rtrancl_reachable_induct)
apply (auto
intro: Promela.reachable_states.intros
simp: E_of_succ_def) [2]
apply (fact setUp_program_inv[OF ast])
apply (fact setUp_gState_inv[OF ast])
done
interpret promela_to_sa: sa "promela_to_sa ?promg"
using promela_to_sa_invar .
have promela_to_sa_run_conv[simp]:
"graph_defs.is_run (promela_to_sa ?promg) = promela_is_run_ltl ?promg"
apply (rule ext)
unfolding graph_defs.is_run_def
unfolding promela_to_sa_def promela_is_run_ltl_def promela_is_run'_def ipath_def E_of_succ_def
by auto
have promela_to_sa_L_conv[simp]:
"sa_L (promela_to_sa ?promg) = promela_props_ltl APs"
apply (rule ext)
unfolding promela_to_sa_def promela_props_ltl_def[abs_def]
by (auto simp: E_of_succ_def)
have promela_to_sa_lang_conv[simp]:
"sa.lang (promela_to_sa ?promg) = promela_language_ltl ?promg"
unfolding promela_to_sa.lang_def promela_to_sa.accept_def[abs_def]
promela_language_ltl_def
by auto
show ?thesis
using cava_sys_agn_correct[OF
promela_to_sa_impl_refine promela_to_sa_invar promela_to_sa_fr, of φ⇩i "fst cfg"]
using promela_language_sub_iff[OF conv ast] promela_run_in_language_iff[OF conv]
unfolding cava_promela_def PromelaLTL.prepare_def
by (auto split: option.split prod.splits simp: lasso_run_rel_def br_def conv ast promela_is_run_ltl_def)
qed
export_code cava_promela checking SML
subsection ‹Model Checker for SM›
definition test_aprop_impl :: "exp ⇒ valuation_impl ⇒ bool" where
"test_aprop_impl e s ≡ case eval_exp_impl e (⦇ local_state_impl.variables = vi_empty ⦈,
⦇ global_state_impl.variables = s ⦈) of None ⇒ False | Some v ⇒ bool_of_val_impl v"
definition sm_to_sa
:: "program ⇒ (ident ⇒ bool) ⇒ (pid_global_config_impl,exp set) sa_rec"
where
"sm_to_sa prog is_vis_var ≡ let
cinf = comp_info_of prog
in
⦇
g_V = UNIV,
g_E = E_of_succ (set o impl4_succ_impl prog cinf is_vis_var),
g_V0 = {pid_init_gc_impl_impl prog cinf},
sa_L = λv. {e. test_aprop_impl e (global_state_impl.variables (pid_global_config.state v))}
⦈"
lemma local_state_rel:
assumes "(s', s) ∈ vi_rel"
shows "(⦇ local_state_impl.variables = s' ⦈, ⦇ local_state.variables = s ⦈) ∈ local_state_rel"
using assms vi_rel_rew unfolding local_state_rel_def by blast
lemma global_state_rel:
assumes "(s', s) ∈ vi_rel"
shows "(⦇ global_state_impl.variables = s' ⦈, ⦇ global_state.variables = s ⦈) ∈ global_state_rel"
using assms vi_rel_rew unfolding global_state_rel_def by blast
lemma test_aprop_impl: "(test_aprop_impl, test_aprop) ∈ Id → vi_rel → bool_rel"
proof clarsimp
fix e s' s
have 0: "(vi_empty, Map.empty) ∈ (vi_rel :: (valuation_impl × valuation) set)"
using vi_rel_rew vi_empty_correct by blast
assume 1: "(s', s) ∈ (vi_rel :: (valuation_impl × valuation) set)"
have 2: "(test_aprop_impl e s', test_aprop e s) ∈ bool_rel"
unfolding test_aprop_def test_aprop_impl_def
apply (parametricity add: eval_exp_impl bool_of_val_impl)
apply (intro IdI)
apply (intro local_state_rel 0)
apply (intro global_state_rel 1)
done
show "test_aprop_impl e s' ⟷ test_aprop e s" using 2 by simp
qed
lemma restrict_parametric:
includes lifting_syntax
assumes [transfer_rule]: "bi_unique A"
shows "((A ===> rel_option B) ===> rel_set A ===> (A ===> rel_option B)) (|`) (|`)"
apply rule
apply rule
apply rule
by (metis (full_types) assms bi_uniqueDl bi_uniqueDr option.rel_intros(1)
rel_funD rel_setD1 rel_setD2 restrict_map_def)
lift_definition restrict :: "('a, 'b) mapping ⇒ 'a set ⇒ ('a, 'b) mapping"
is "(|`)" parametric restrict_parametric .
lift_definition vi_restrict :: "valuation_impl ⇒ ident set ⇒ valuation_impl"
is "(|`) :: valuation ⇒ ident set ⇒ valuation" by this
lemma [code]: "vi_restrict = restrict" by transfer simp
lemma vi_restrict_correct: "vi_α (vi_restrict s A) = vi_α s |` A"
unfolding vi_α_def by transfer (simp add: Fun.comp_def option.map_ident)
definition (in -) pid_test_gc_impl
:: "pid_global_config_impl ⇒ exp ⇒ bool"
where
"pid_test_gc_impl gci ap ≡ test_aprop_impl ap
((global_state_impl.variables (pid_global_config.state gci)))"
definition sm_to_sa_impl
:: "program ⇒ (ident ⇒ bool)
⇒ (pid_global_config_impl,exp ⇒ bool,unit) sa_impl_scheme"
where
"sm_to_sa_impl prog is_vis_var ≡ let
cinf = comp_info_of prog
in
⦇ gi_V = λ_. True,
gi_E = remdups o impl4_succ_impl prog cinf is_vis_var,
gi_V0 = [pid_init_gc_impl_impl prog cinf],
sai_L = pid_test_gc_impl
⦈"
lemma sm_to_sa_impl_refine: "(sm_to_sa_impl prog is_vis_var, sm_to_sa prog is_vis_var)
∈ sa_impl_rel_ext unit_rel Id (⟨Id⟩fun_set_rel)"
unfolding sm_to_sa_impl_def sm_to_sa_def
unfolding sa_impl_rel_eext_def g_impl_rel_ext_def
unfolding gen_sa_impl_rel_eext_def gen_g_impl_rel_ext_def
apply (clarsimp split: prod.split)
apply (intro conjI)
apply (auto simp: fun_set_rel_def br_def) []
apply (rule E_of_succ_refine[param_fo])
apply (auto simp: list_set_rel_def br_def) []
apply (auto simp: list_set_rel_def br_def) []
apply (auto simp: fun_set_rel_def br_def pid_test_gc_impl_def) []
done
lemma E_of_succ_is_rel_of_succ: "E_of_succ = rel_of_succ"
by (auto intro!: ext simp: E_of_succ_def rel_of_succ_def)
definition vi_γ :: "valuation ⇒ valuation_impl" where
"vi_γ v = (Mapping.Mapping (map_option Abs_uint32 ∘ v))"
lemma [simp]: "vi_α (vi_γ v) = v"
unfolding vi_α_def vi_γ_def
apply (rule ext)
apply (auto simp: Mapping_inverse option.map_comp option.map_ident Abs_uint32_inverse o_def)
done
lemma [simp]: "vi_γ (vi_α v) = v"
unfolding vi_α_def vi_γ_def
apply (auto simp: Mapping.rep_inverse option.map_comp option.map_ident Rep_uint32_inverse o_def)
done
definition lsi_α :: "local_state_impl ⇒ local_state" where
"lsi_α lsi ≡ ⦇ local_state.variables = vi_α (local_state_impl.variables lsi) ⦈"
definition lsi_γ :: "local_state ⇒ local_state_impl" where
"lsi_γ lsi ≡ ⦇ local_state_impl.variables = vi_γ (local_state.variables lsi) ⦈"
lemma [simp]:
"lsi_α (lsi_γ ls) = ls"
"lsi_γ (lsi_α lsi) = lsi"
unfolding lsi_α_def lsi_γ_def
by auto
lemma local_state_rel_as_br: "local_state_rel = br lsi_α (λ_. True)"
by (force simp: local_state_rel_def br_def lsi_α_def)
definition gsi_α :: "global_state_impl ⇒ global_state" where
"gsi_α gsi ≡ ⦇ global_state.variables = vi_α (global_state_impl.variables gsi) ⦈"
definition gsi_γ :: "global_state ⇒ global_state_impl" where
"gsi_γ gs ≡ ⦇ global_state_impl.variables = vi_γ (global_state.variables gs) ⦈"
lemma [simp]:
"gsi_α (gsi_γ gs) = gs"
"gsi_γ (gsi_α gsi) = gsi"
unfolding gsi_α_def gsi_γ_def
by auto
lemma global_state_rel_as_br: "global_state_rel = br gsi_α (λ_. True)"
by (force simp: global_state_rel_def br_def gsi_α_def)
definition map_local_config
:: "('a⇒'c) ⇒ ('b⇒'d) ⇒ ('a,'b) Gen_Scheduler.local_config ⇒ ('c,'d) Gen_Scheduler.local_config"
where
"map_local_config mc ms ls ≡ ⦇
local_config.command = mc (local_config.command ls),
local_config.state = ms (local_config.state ls)
⦈"
lemma [simp]:
"map_local_config (λx. x) (λx. x) = (λx. x)"
"map_local_config f g (map_local_config f' g' lc) = map_local_config (f o f') (g o g') lc"
by (auto simp: map_local_config_def)
definition map_pid_global_config
:: "('a⇒'d) ⇒ ('b⇒'e) ⇒ ('c⇒'f) ⇒ ('a,'b,'c) Pid_Scheduler.pid_global_config ⇒ ('d,'e,'f) Pid_Scheduler.pid_global_config"
where
"map_pid_global_config mp ml mg gc ≡ ⦇
pid_global_config.processes = map (map_local_config mp ml) (pid_global_config.processes gc),
pid_global_config.state = mg (pid_global_config.state gc)
⦈"
lemma [simp]:
"map_pid_global_config (λx. x) (λx. x) (λx. x) = (λx. x)"
"map_pid_global_config f g h (map_pid_global_config f' g' h' gc)
= map_pid_global_config (f o f') (g o g') (h o h') gc"
by (auto simp: map_pid_global_config_def)
abbreviation lci_α :: "local_config_impl ⇒ local_config"
where "lci_α ≡ map_local_config (λx. x) lsi_α"
abbreviation lci_γ :: "local_config ⇒ local_config_impl"
where "lci_γ ≡ map_local_config (λx. x) lsi_γ"
abbreviation gci_α :: "pid_global_config_impl ⇒ pid_global_config"
where "gci_α ≡ map_pid_global_config (λx. x) lsi_α gsi_α"
abbreviation gci_γ :: "pid_global_config ⇒ pid_global_config_impl"
where "gci_γ ≡ map_pid_global_config (λx. x) lsi_γ gsi_γ"
lemma local_config_rel_as_br: "local_config_rel = br lci_α (λ_. True)"
by (force simp: local_config_rel_def br_def map_local_config_def local_state_rel_as_br)
thm list_all2_induct
lemma list_all2_map_conv[simp]:
"list_all2 (λx y. x=f y) xs ys ⟷ xs = map f ys"
"list_all2 (λx y. y=f x) ys xs ⟷ xs = map f ys"
apply (rule iffI)
apply (induction rule: list_all2_induct, auto) []
apply (induction ys arbitrary: xs, auto) []
apply (rule iffI)
apply (induction rule: list_all2_induct, auto) []
apply (induction ys arbitrary: xs, auto) []
done
lemma pid_global_config_rel_as_br: "global_config_rel = br gci_α (λ_. True)"
by (force
simp: global_config_rel_def br_def map_pid_global_config_def
simp: global_state_rel_as_br local_config_rel_as_br
simp: list_rel_def)
lemma global_config_rel_inv_sv: "single_valued (global_config_rel¯)"
apply (rule single_valuedI)
apply (clarsimp simp: pid_global_config_rel_as_br br_def)
proof -
fix x y
assume "gci_α x = gci_α y"
hence "gci_γ (gci_α x) = gci_γ (gci_α y)" by simp
thus "x=y" by (simp add: o_def)
qed
lemma pred_of_enex_mono:
assumes "en c ⊆ en' c"
assumes "pred_of_enex (en,ex) c c'"
shows "pred_of_enex (en',ex) c c'"
using assms
by (auto)
lemma finite_ample_reachable[simp, intro!]:
assumes "ty_program prog"
shows "finite
((E_of_succ ((set ∘∘ impl4_succ_impl prog (comp_info_of prog)) is_vis_var))⇧* ``
{pid_init_gc_impl_impl prog (comp_info_of prog)})" (is "finite ?S")
proof -
interpret visible_prog prog is_vis_var using assms by unfold_locales
have "E_of_succ ((set ∘∘ impl4_succ_impl prog (comp_info_of prog)) is_vis_var)
= ample_step_impl4 is_vis_var"
by (simp
add: impl4_succ_pred[symmetric] E_of_succ_is_rel_of_succ
add: impl4_succ_impl)
also note ample_step_impl4[simplified]
finally have "E_of_succ ((set ∘∘ impl4_succ_impl prog (comp_info_of prog)) is_vis_var)
= ample_step_impl3" .
hence S_eq: "?S = ample_step_impl3⇧* `` {pid_init_gc_impl}"
by (simp add: pid_init_gc_impl_impl)
interpret impl2: sa "⦇ g_V = UNIV, g_E = ample_step_impl2,
g_V0 = {pid_init_gc}, sa_L = pid_interp_gc ⦈" by unfold_locales auto
have 1: "ample_step_impl2 = rel_of_enex (cr_ample_impl1, ga_ex)"
unfolding ample_step_impl2_def cr_ample_impl1_def cr_ample_impl2_def
unfolding ga_gample_mi2_impl[abs_def]
by simp
{
fix gc :: pid_global_config
have "cr_ample ≤ SPEC (λr. r gc ⊆ ga_en gc)"
unfolding cr_ample_def
apply (refine_vcg order_trans[OF find_fas_init_correct])
apply unfold_locales[]
apply simp
proof -
fix sticky_E
show "ga_ample sticky_E gc ⊆ ga_en gc"
apply (cases "ga_ample sticky_E gc = ga_en gc")
apply simp
apply (drule ga_ample_neq_en_eq[of sticky_E gc])
using ga_gample_subset[of sticky_E gc]
apply auto
done
qed
from order_trans[OF cr_ample_impl1.refine[THEN nres_relD, simplified] this]
have "cr_ample_impl1 gc ⊆ ga_en gc" by simp
} note aux1=this
interpret simulation Id
"⦇ g_V = UNIV, g_E = rel_of_enex (cr_ample_impl1,ga_ex), g_V0 = {pid_init_gc} ⦈"
"⦇ g_V = UNIV, g_E = ga_step, g_V0 = {pid_init_gc} ⦈"
unfolding ga_step_alt
apply unfold_locales
using pred_of_enex_mono[of cr_ample_impl1 _ ga_en ga_ex,OF aux1]
apply auto
done
have FIN2: "finite (ample_step_impl2⇧* `` {pid_init_gc})"
unfolding 1
unfolding graph_rec.simps
apply (rule reachable_finite_sim[unfolded graph_rec.simps])
using jsys.reachable_finite
using reachable_alt
apply simp
apply simp
done
show "finite ?S"
unfolding S_eq
using impl3_sim.s1.reachable_finite_sim FIN2 finite_Image_sv[OF global_config_rel_inv_sv]
by simp
qed
lemma
assumes "ty_program prog"
shows sm_to_sa_invar: "sa (sm_to_sa prog is_vis_var)"
and sm_to_sa_fr: "finite ((g_E (sm_to_sa prog is_vis_var))⇧* `` g_V0 (sm_to_sa prog is_vis_var))"
unfolding sm_to_sa_def by (unfold_locales, auto intro: assms)
definition "mapping_val_hashcode m ≡ ∑((hashcode o Mapping.lookup m)`Mapping.keys m)"
instantiation local_config_ext :: (hashable,hashable,hashable)hashable begin
definition "hashcode lc ≡
hashcode (local_config.command lc)
+ hashcode (local_config.state lc)
+ hashcode (local_config.more lc)"
definition "def_hashmap_size (T::('a,'b,'c) local_config_ext itself) ≡ 8"
instance
apply intro_classes
unfolding def_hashmap_size_local_config_ext_def
by auto
end
instantiation Pid_Scheduler.pid_global_config_ext :: (hashable,hashable,hashable,hashable) hashable begin
definition "hashcode gc ≡
hashcode (pid_global_config.processes gc)
+ hashcode (pid_global_config.state gc)
+ hashcode (pid_global_config.more gc)"
definition "def_hashmap_size (T::('a,'b,'c,'d) pid_global_config_ext itself) ≡ 8"
instance
apply intro_classes
unfolding def_hashmap_size_pid_global_config_ext_def
by auto
end
instantiation local_state_impl_ext :: (hashable)hashable begin
term "rm.iterate r (λ(k,v) s. hashcode k + hashcode v + s) 0"
definition "hashcode ls
≡ mapping_val_hashcode (local_state_impl.variables ls)
+ hashcode (local_state_impl.more ls)"
definition "def_hashmap_size (T::('a) local_state_impl_ext itself) ≡ 8"
instance
apply intro_classes
unfolding def_hashmap_size_local_state_impl_ext_def
by auto
end
instantiation global_state_impl_ext :: (hashable)hashable begin
term "rm.iterate r (λ(k,v) s. hashcode k + hashcode v + s) 0"
definition "hashcode gs
≡ mapping_val_hashcode (global_state_impl.variables gs)
+ hashcode (global_state_impl.more gs)"
definition "def_hashmap_size (T::('a) global_state_impl_ext itself) ≡ 8"
instance
apply intro_classes
unfolding def_hashmap_size_global_state_impl_ext_def
by auto
end
local_setup ‹
Comparator_Generator.register_foreign_comparator @{typ String.literal}
@{term "comparator_of :: String.literal ⇒ _"}
@{thm comparator_of[where 'a=String.literal]}
›
derive linorder un_op
derive linorder bin_op
derive linorder exp