Theory Find_Path_Impl
section ‹Implementation of Safety Property Model Checker \label{sec:find_path_impl}›
theory Find_Path_Impl
imports
Find_Path
CAVA_Automata.Digraph_Impl
begin
section ‹Workset Algorithm›
text ‹A simple implementation is by a workset algorithm.›
definition "ws_update E u p V ws ≡ RETURN (
V ∪ E``{u},
ws ++ (λv. if (u,v)∈E ∧ v∉V then Some (u#p) else None))"
definition "s_init U0 ≡ RETURN (None,U0,λu. if u∈U0 then Some [] else None)"
definition "wset_find_path E U0 P ≡ do {
ASSERT (finite U0);
s0 ← s_init U0;
(res,_,_) ← WHILET
(λ(res,V,ws). res=None ∧ ws≠Map.empty)
(λ(res,V,ws). do {
ASSERT (ws≠Map.empty);
(u,p) ← SPEC (λ(u,p). ws u = Some p);
let ws=ws |` (-{u});
if P u then
RETURN (Some (rev p,u),V,ws)
else do {
ASSERT (finite (E``{u}));
ASSERT (dom ws ⊆ V);
(V,ws) ← ws_update E u p V ws;
RETURN (None,V,ws)
}
}) s0;
RETURN res
}"
lemma wset_find_path_correct:
fixes E :: "('v×'v) set"
shows "wset_find_path E U0 P ≤ find_path E U0 P"
proof -
define inv where "inv = (λ(res,V,ws). case res of
None ⇒
dom ws⊆V
∧ finite (dom ws)
∧ V⊆E⇧*``U0
∧ E``(V-dom ws) ⊆ V
∧ (∀v∈V-dom ws. ¬ P v)
∧ U0 ⊆ V
∧ (∀v p. ws v = Some p
⟶ ((∀v∈set p. ¬P v) ∧ (∃u0∈U0. path E u0 (rev p) v)))
| Some (p,v) ⇒ (∃u0∈U0. path E u0 p v ∧ P v ∧ (∀v∈set p. ¬P v)))"
define var where "var = inv_image
(brk_rel (finite_psupset (E⇧*``U0) <*lex*> measure (card o dom)))
(λ(res::('v list × 'v) option,V::'v set,ws::'v⇀'v list).
(res≠None,V,ws))"
have [simp]: "⋀u p V. dom (λv. if (u, v) ∈ E ∧ v ∉ V then Some (u # p)
else None) = E``{u} - V"
by (auto split: if_split_asm)
{
fix V ws u p
assume INV: "inv (None,V,ws)"
assume WSU: "ws u = Some p"
from INV WSU have
[simp]: "V ⊆ E⇧*``U0"
and [simp]: "u ∈ V"
and UREACH: "∃u0∈U0. (u0,u)∈E⇧*"
and [simp]: "finite (dom ws)"
unfolding inv_def
apply simp_all
apply auto []
apply clarsimp
apply blast
done
have "(V ∪ E `` {u}, V) ∈ finite_psupset (E⇧* `` U0) ∨
V ∪ E `` {u} = V ∧
card (E `` {u} - V ∪ (dom ws - {u})) < card (dom ws)"
proof (subst disj_commute, intro disjCI conjI)
assume "(V ∪ E `` {u}, V) ∉ finite_psupset (E⇧* `` U0)"
thus "V ∪ E `` {u} = V" using UREACH
by (auto simp: finite_psupset_def intro: rev_ImageI)
hence [simp]: "E``{u} - V = {}" by force
show "card (E `` {u} - V ∪ (dom ws - {u})) < card (dom ws)"
using WSU
by (auto intro: card_Diff1_less)
qed
} note wf_aux=this
{
fix V ws u p
assume FIN: "finite (E⇧*``U0)"
assume "inv (None,V,ws)" "ws u = Some p"
then obtain u0 where "u0∈U0" "(u0,u)∈E⇧*" unfolding inv_def
by clarsimp blast
hence "E``{u} ⊆ E⇧*``U0" by (auto intro: rev_ImageI)
hence "finite (E``{u})" using FIN(1) by (rule finite_subset)
} note succs_finite=this
{
fix V ws u p
assume FIN: "finite (E⇧*``U0)"
assume INV: "inv (None,V,ws)"
assume WSU: "ws u = Some p"
assume NVD: "¬ P u"
have "inv (None, V ∪ E `` {u},
ws |` (- {u}) ++
(λv. if (u, v) ∈ E ∧ v ∉ V then Some (u # p)
else None))"
unfolding inv_def
apply (simp, intro conjI)
using INV WSU apply (auto simp: inv_def) []
using INV WSU apply (auto simp: inv_def) []
using INV WSU apply (auto simp: succs_finite FIN) []
using INV apply (auto simp: inv_def) []
using INV apply (auto simp: inv_def) []
using INV WSU apply (auto
simp: inv_def
intro: rtrancl_image_advance
) []
using INV WSU apply (auto simp: inv_def) []
using INV NVD apply (auto simp: inv_def) []
using INV NVD apply (auto simp: inv_def) []
using INV WSU NVD apply (fastforce
simp: inv_def restrict_map_def
intro!: path_conc path1
split: if_split_asm
) []
done
} note ip_aux=this
show ?thesis
unfolding wset_find_path_def find_path_def ws_update_def s_init_def
apply (refine_rcg refine_vcg le_ASSERTI
WHILET_rule[where
R = var and I = inv]
)
using [[goals_limit = 1]]
apply (auto simp: var_def) []
apply (auto
simp: inv_def dom_def
split: if_split_asm) []
apply simp
apply (auto simp: inv_def) []
apply (auto simp: var_def brk_rel_def) []
apply (simp add: succs_finite)
apply (auto simp: inv_def) []
apply clarsimp
apply (simp add: ip_aux)
apply clarsimp
apply (simp add: var_def brk_rel_def wf_aux) []
apply (fastforce
simp: inv_def
split: option.splits
intro: rev_ImageI
dest: Image_closed_trancl) []
done
qed
text ‹We refine the algorithm to use a foreach-loop›
definition "ws_update_foreach E u p V ws ≡
FOREACH (LIST_SET_REV_TAG (E``{u})) (λv (V,ws).
if v∈V then
RETURN (V,ws)
else do {
ASSERT (v∉dom ws);
RETURN (insert v V,ws( v ↦ u#p))
}
) (V,ws)"
lemma ws_update_foreach_refine[refine]:
assumes FIN: "finite (E``{u})"
assumes WSS: "dom ws ⊆ V"
assumes ID: "(E',E)∈Id" "(u',u)∈Id" "(p',p)∈Id" "(V',V)∈Id" "(ws',ws)∈Id"
shows "ws_update_foreach E' u' p' V' ws' ≤ ⇓Id (ws_update E u p V ws)"
unfolding ID[simplified]
unfolding ws_update_foreach_def ws_update_def LIST_SET_REV_TAG_def
apply (refine_rcg refine_vcg FIN
FOREACH_rule[where I="λit (V',ws').
V'=V ∪ (E``{u}-it)
∧ dom ws' ⊆ V'
∧ ws' = ws ++ (λv. if (u,v)∈E ∧ v∉it ∧ v∉V then Some (u#p) else None)"]
)
using WSS
apply (auto
simp: Map.map_add_def
split: option.splits if_split_asm
intro!: ext[where 'a='a and 'b="'b list option"])
done
definition "s_init_foreach U0 ≡ do {
(U0,ws) ← FOREACH U0 (λx (U0,ws).
RETURN (insert x U0,ws(x↦[]))) ({},Map.empty);
RETURN (None,U0,ws)
}"
lemma s_init_foreach_refine[refine]:
assumes FIN: "finite U0"
assumes ID: "(U0',U0)∈Id"
shows "s_init_foreach U0' ≤⇓Id (s_init U0)"
unfolding s_init_foreach_def s_init_def ID[simplified]
apply (refine_rcg refine_vcg
FOREACH_rule[where
I = "λit (U,ws).
U = U0-it
∧ ws = (λx. if x∈U0-it then Some [] else None)"]
)
apply (auto
simp: FIN
intro!: ext
)
done
definition "wset_find_path' E U0 P ≡ do {
ASSERT (finite U0);
s0←s_init_foreach U0;
(res,_,_) ← WHILET
(λ(res,V,ws). res=None ∧ ws≠Map.empty)
(λ(res,V,ws). do {
ASSERT (ws≠Map.empty);
((u,p),ws) ← op_map_pick_remove ws;
if P u then
RETURN (Some (rev p,u),V,ws)
else do {
(V,ws) ← ws_update_foreach E u p V ws;
RETURN (None,V,ws)
}
})
s0;
RETURN res
}"
lemma wset_find_path'_refine:
"wset_find_path' E U0 P ≤ ⇓Id (wset_find_path E U0 P)"
unfolding wset_find_path'_def wset_find_path_def
unfolding op_map_pick_remove_alt
apply (refine_rcg IdI)
apply assumption
apply simp_all
done
section ‹Refinement to efficient data structures›
schematic_goal wset_find_path'_refine_aux:
fixes U0::"'a set" and P::"'a ⇒ bool" and E::"('a×'a) set"
and Pimpl :: "'ai ⇒ bool"
and node_rel :: "('ai × 'a) set"
and node_eq_impl :: "'ai ⇒ 'ai ⇒ bool"
and node_hash_impl
and node_def_hash_size
assumes [autoref_rules]:
"(succi,E)∈⟨node_rel⟩slg_rel"
"(Pimpl,P)∈node_rel → bool_rel"
"(node_eq_impl, (=)) ∈ node_rel → node_rel → bool_rel"
"(U0',U0)∈⟨node_rel⟩list_set_rel"
assumes [autoref_ga_rules]:
"is_bounded_hashcode node_rel node_eq_impl node_hash_impl"
"is_valid_def_hm_size TYPE('ai) node_def_hash_size"
notes [autoref_tyrel] =
TYRELI[where
R="⟨node_rel,⟨node_rel⟩list_rel⟩list_map_rel"]
TYRELI[where R="⟨node_rel⟩map2set_rel (ahm_rel node_hash_impl)"]
shows "(?c::?'c,wset_find_path' E U0 P) ∈ ?R"
unfolding wset_find_path'_def ws_update_foreach_def s_init_foreach_def
using [[autoref_trace_failed_id]]
using [[autoref_trace_intf_unif]]
using [[autoref_trace_pat]]
apply (autoref (keep_goal))
done
concrete_definition wset_find_path_impl for node_eq_impl succi U0' Pimpl
uses wset_find_path'_refine_aux
section ‹Autoref Setup›
context begin interpretation autoref_syn .
lemma [autoref_itype]:
"find_path ::⇩i ⟨I⟩⇩ii_slg →⇩i ⟨I⟩⇩ii_set →⇩i (I→⇩ii_bool)
→⇩i ⟨⟨⟨⟨I⟩⇩ii_list, I⟩⇩ii_prod⟩⇩ii_option⟩⇩ii_nres" by simp
lemma wset_find_path_autoref[autoref_rules]:
fixes node_rel :: "('ai × 'a) set"
assumes eq: "GEN_OP node_eq_impl (=) (node_rel→node_rel→bool_rel)"
assumes hash: "SIDE_GEN_ALGO (is_bounded_hashcode node_rel node_eq_impl node_hash_impl)"
assumes hash_dsz: "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('ai) node_def_hash_size)"
shows "(
wset_find_path_impl node_hash_impl node_def_hash_size node_eq_impl,
find_path)
∈ ⟨node_rel⟩slg_rel → ⟨node_rel⟩list_set_rel → (node_rel→bool_rel)
→ ⟨⟨⟨node_rel⟩list_rel×⇩rnode_rel⟩option_rel⟩nres_rel"
proof -
note EQI = GEN_OP_D[OF eq]
note HASHI = SIDE_GEN_ALGO_D[OF hash]
note DSZI = SIDE_GEN_ALGO_D[OF hash_dsz]
note wset_find_path_impl.refine[THEN nres_relD, OF _ _ EQI _ HASHI DSZI]
also note wset_find_path'_refine
also note wset_find_path_correct
finally show ?thesis
by (fastforce intro!: nres_relI)
qed
end
schematic_goal wset_find_path_transfer_aux:
"RETURN ?c ≤ wset_find_path_impl hashi dszi eqi E U0 P"
unfolding wset_find_path_impl_def
by (refine_transfer (post))
concrete_definition wset_find_path_code
for E ?U0.0 P uses wset_find_path_transfer_aux
lemmas [refine_transfer] = wset_find_path_code.refine
export_code wset_find_path_code checking SML
section ‹Nontrivial paths›
definition "find_path1_gen E u0 P ≡ do {
res ← find_path E (E``{u0}) P;
case res of None ⇒ RETURN None
| Some (p,v) ⇒ RETURN (Some (u0#p,v))
}"
lemma find_path1_gen_correct: "find_path1_gen E u0 P ≤ find_path1 E u0 P"
unfolding find_path1_gen_def find_path_def find_path1_def
apply (refine_rcg refine_vcg le_ASSERTI)
apply (auto
intro: path_prepend
dest: tranclD
elim: finite_subset[rotated]
)
done
schematic_goal find_path1_impl_aux:
fixes node_rel :: "('ai × 'a) set"
assumes [autoref_rules]: "(node_eq_impl, (=)) ∈ node_rel → node_rel → bool_rel"
assumes [autoref_ga_rules]:
"is_bounded_hashcode node_rel node_eq_impl node_hash_impl"
"is_valid_def_hm_size TYPE('ai) node_def_hash_size"
shows "(?c,find_path1_gen::(_×_) set ⇒ _) ∈ ⟨node_rel⟩slg_rel → node_rel → (node_rel → bool_rel) → ⟨⟨⟨node_rel⟩list_rel ×⇩r node_rel⟩option_rel⟩nres_rel"
unfolding find_path1_gen_def[abs_def]
apply (autoref (trace,keep_goal))
done
lemma [autoref_itype]:
"find_path1 ::⇩i ⟨I⟩⇩ii_slg →⇩i I →⇩i (I→⇩ii_bool)
→⇩i ⟨⟨⟨⟨I⟩⇩ii_list, I⟩⇩ii_prod⟩⇩ii_option⟩⇩ii_nres" by simp
concrete_definition find_path1_impl uses find_path1_impl_aux
lemma find_path1_autoref[autoref_rules]:
fixes node_rel :: "('ai × 'a) set"
assumes eq: "GEN_OP node_eq_impl (=) (node_rel→node_rel→bool_rel)"
assumes hash: "SIDE_GEN_ALGO (is_bounded_hashcode node_rel node_eq_impl node_hash_impl)"
assumes hash_dsz: "SIDE_GEN_ALGO (is_valid_def_hm_size TYPE('ai) node_def_hash_size)"
shows "(find_path1_impl node_eq_impl node_hash_impl node_def_hash_size,find_path1)
∈ ⟨node_rel⟩slg_rel →node_rel → (node_rel → bool_rel) →
⟨⟨⟨node_rel⟩list_rel ×⇩r node_rel⟩Relators.option_rel⟩nres_rel"
proof -
note EQI = GEN_OP_D[OF eq]
note HASHI = SIDE_GEN_ALGO_D[OF hash]
note DSZI = SIDE_GEN_ALGO_D[OF hash_dsz]
note R = find_path1_impl.refine[param_fo, THEN nres_relD, OF EQI HASHI DSZI]
note R
also note find_path1_gen_correct
finally show ?thesis by (blast intro: nres_relI)
qed
schematic_goal find_path1_transfer_aux:
"RETURN ?c ≤ find_path1_impl eqi hashi dszi E u P"
unfolding find_path1_impl_def
by refine_transfer
concrete_definition find_path1_code for E u P uses find_path1_transfer_aux
lemmas [refine_transfer] = find_path1_code.refine
end