Theory Unreachability_Certification
theory Unreachability_Certification
imports
Simulation_Graphs_Certification
Worklist_Algorithms.Leadsto_Impl
Munta_Base.Printing
Difference_Bound_Matrices.DBM_Imperative_Loops
Munta_Base.Trace_Timing
Unreachability_Misc
begin
context
fixes K :: "'k ⇒ ('ki :: {heap}) ⇒ assn"
assumes pure_K: "is_pure K"
assumes left_unique_K: "IS_LEFT_UNIQUE (the_pure K)"
assumes right_unique_K: "IS_RIGHT_UNIQUE (the_pure K)"
begin
lemma pure_equality_impl:
"(uncurry (return oo (=)), uncurry (RETURN oo (=))) ∈ (K⇧k *⇩a K⇧k) →⇩a bool_assn"
proof -
have 1: "K = pure (the_pure K)"
using pure_K by auto
have [dest]: "a = b" if "(bi, b) ∈ the_pure K" "(bi, a) ∈ the_pure K" for bi a b
using that right_unique_K by (elim single_valuedD) auto
have [dest]: "a = b" if "(a, bi) ∈ the_pure K" "(b, bi) ∈ the_pure K" for bi a b
using that left_unique_K unfolding IS_LEFT_UNIQUE_def by (elim single_valuedD) auto
show ?thesis
by (subst 1, subst (2) 1, sepref_to_hoare, sep_auto)
qed
definition
"is_member x L ≡ do {
xs ← SPEC (λxs. set xs = L);
monadic_list_ex (λy. RETURN (y = x)) xs
}"
lemma is_member_refine:
"is_member x L ≤ mop_set_member x L"
unfolding mop_set_member_alt is_member_def
by (refine_vcg monadic_list_ex_rule) (auto simp: list_ex_iff)
lemma is_member_correct:
"(uncurry is_member, uncurry (RETURN ∘∘ op_set_member)) ∈ Id ×⇩r Id → ⟨bool_rel⟩nres_rel"
using is_member_refine by (force simp: pw_le_iff pw_nres_rel_iff)
lemmas [sepref_fr_rules] = lso_id_hnr
sepref_definition is_member_impl is
"uncurry is_member" :: "K⇧k *⇩a (lso_assn K)⇧k →⇩a bool_assn"
supply [sepref_fr_rules] = pure_equality_impl
supply [safe_constraint_rules] = pure_K left_unique_K right_unique_K
unfolding is_member_def monadic_list_ex_def list_of_set_def[symmetric] by sepref
lemmas op_set_member_lso_hnr = is_member_impl.refine[FCOMP is_member_correct]
end
paragraph ‹Concrete Implementations›
context Reachability_Impl
begin
definition
"check_invariant' L' M' ≡ do {
monadic_list_all (λl.
do {
case op_map_lookup l M' of None ⇒ RETURN True | Some xs ⇒ do {
let succs = PR_CONST succs l xs;
monadic_list_all (λ(l', xs). do {
xs ← SPEC (λxs'. set xs' = xs);
if xs = [] then RETURN True
else do {
case op_map_lookup l' M' of None ⇒ RETURN False | Some ys ⇒ do {
ys ← SPEC (λxs. set xs = ys);
monadic_list_all (λx'.
monadic_list_ex (λy. RETURN (PR_CONST less_eq x' y)) ys
) xs
}
}
}) succs
}
}) L'
}"
lemma succs_listD:
assumes "(l', S') ∈ set (succs l S)" "finite S"
shows "∃ xs. set xs = S'"
using assms succs_finite by (force intro!: finite_list)
lemma check_invariant'_refine:
"check_invariant' L_part M ≤ check_invariant L_part" if "L = dom M" "set L_part ⊆ L"
unfolding check_invariant_def check_invariant'_def
unfolding PR_CONST_def
apply refine_mono
apply (clarsimp split: option.splits simp: succs_empty)
apply refine_mono
apply (clarsimp split: option.splits)
apply safe
subgoal
by refine_mono (auto simp: bind_RES monadic_list_all_False dest: M_listD)
subgoal
apply refine_mono
apply clarsimp
apply refine_mono
apply clarsimp
subgoal for xs1 xs2
using monadic_list_all_list_ex_is_RETURN[of "λ x y. less_eq x y" xs2 xs1]
by (auto simp: bind_RES ‹L = dom M›)
done
done
lemma check_invariant'_no_fail:
"nofail (check_invariant' L' M')"
unfolding check_invariant'_def
by (intro monadic_list_all_nofailI monadic_list_ex_nofailI no_fail_RES_bindI
| clarsimp split: option.splits)+
lemma check_invariant'_correct_pre:
"check_invariant' L_part M ≤ RETURN (check_invariant_spec_pre L_part)"
if "L = dom M" "set L_part ⊆ L"
by (rule check_invariant_correct_pre check_invariant'_refine[OF that] Orderings.order.trans)+
definition check_invariant_spec_pre1 where
"check_invariant_spec_pre1 L' M' ≡
∀l ∈ set L'. ∀(l',ys) ∈ set (succs l (M' l)). ∀s' ∈ ys. (∃s'' ∈ M' l'. s' ≼ s'')"
lemma check_invariant'_correct_pre1:
"check_invariant' L' M'
≤ RETURN (check_invariant_spec_pre1 L' (λl. case M' l of None ⇒ {} | Some S ⇒ S))"
unfolding check_invariant'_def check_invariant_spec_pre1_def
by (refine_vcg monadic_list_all_rule monadic_list_ex_rule)
(auto simp: list_all_iff list_ex_iff succs_empty)
lemmas [safe_constraint_rules] = pure_K left_unique_K right_unique_K
lemmas [sepref_fr_rules] = lso_id_hnr
sepref_register
"PR_CONST L" "list_of_set" "PR_CONST P'" "PR_CONST F" "PR_CONST succs" "PR_CONST less_eq"
"PR_CONST M" :: "('k, 'b set) i_map"
lemma [sepref_import_param]: "(id, id) ∈ (Id :: (bool × bool) set) → Id"
by simp
sepref_definition check_prop_impl_wrong is
"uncurry check_prop'" :: "(lso_assn K)⇧k *⇩a (hm.hms_assn' K (lso_assn A))⇧k →⇩a id_assn"
unfolding check_prop'_alt_def list_of_set_def[symmetric]
unfolding monadic_list_all_def
apply sepref_dbg_keep
oops
sepref_decl_impl "map_lookup":
copy_list_lso_assn_refine[OF copyi, THEN hms_hm.hms_lookup_hnr]
uses op_map_lookup.fref[where V = Id] .
abbreviation "table_assn ≡ hm.hms_assn' K (lso_assn A)"
sepref_thm check_prop_impl is
"uncurry (PR_CONST check_prop')" :: "(lso_assn K)⇧k *⇩a table_assn⇧k →⇩a id_assn"
unfolding PR_CONST_def
unfolding check_prop'_def list_of_set_def[symmetric]
unfolding monadic_list_all_def
by sepref
concrete_definition (in -) check_prop_impl
uses Reachability_Impl.check_prop_impl.refine_raw is "(uncurry ?f,_)∈_"
sepref_thm check_final_impl is
"uncurry (PR_CONST check_final')" :: "(lso_assn K)⇧k *⇩a table_assn⇧k →⇩a id_assn"
unfolding PR_CONST_def
unfolding check_final'_def list_of_set_def[symmetric]
unfolding monadic_list_all_def
by sepref
concrete_definition (in -) check_final_impl
uses Reachability_Impl.check_final_impl.refine_raw is "(uncurry ?f,_)∈_"
lemma K_equality[sepref_fr_rules]:
"(uncurry (return oo (=)), uncurry (RETURN oo (=))) ∈ (K⇧k *⇩a K⇧k) →⇩a bool_assn"
proof -
have 1: "K = pure (the_pure K)"
using pure_K by auto
have [dest]: "a = b" if "(bi, b) ∈ the_pure K" "(bi, a) ∈ the_pure K" for bi a b
using that right_unique_K by (elim single_valuedD) auto
have [dest]: "a = b" if "(a, bi) ∈ the_pure K" "(b, bi) ∈ the_pure K" for bi a b
using that left_unique_K unfolding IS_LEFT_UNIQUE_def by (elim single_valuedD) auto
show ?thesis
by (subst 1, subst (2) 1, sepref_to_hoare, sep_auto)
qed
sepref_definition is_K_eq_impl is
"uncurry (RETURN oo (=))" :: "(K⇧k *⇩a K⇧k) →⇩a bool_assn"
unfolding is_member_def monadic_list_ex_def list_of_set_def[symmetric] by sepref
lemmas [sepref_fr_rules] = op_set_member_lso_hnr[OF pure_K left_unique_K right_unique_K]
sepref_definition check_invariant_impl is
"uncurry (PR_CONST check_invariant')" :: "(list_assn K)⇧k *⇩a table_assn⇧k →⇩a id_assn"
unfolding PR_CONST_def
unfolding check_invariant'_def list_of_set_def[symmetric]
unfolding monadic_list_all_def monadic_list_ex_def
by sepref
lemma check_invariant_impl_ht:
"<table_assn M bi * list_assn K a ai>
check_invariant_impl ai bi
<λr. table_assn M bi * list_assn K a ai * ↑(r ⟶ check_invariant_spec (set a))>⇩t"
if "nofail (check_invariant' a M)" "L = dom M" "set a ⊆ L" "∀l ∈ L. ∀s ∈ the (M l). P (l, s)"
apply (rule cons_post_rule)
apply (rule check_invariant_impl.refine[
to_hnr, unfolded hn_refine_def hn_ctxt_def, simplified, rule_format])
subgoal
by (rule that)
using that
apply sep_auto
apply (drule Orderings.order.trans,
rule Orderings.order.trans[OF check_invariant'_refine check_invariant_correct])
apply (sep_auto simp: pure_def split: option.splits)+
done
definition
"check_all_pre' L' M' ≡ do {
b1 ← RETURN (PR_CONST l⇩0 ∈ L');
b2 ← RETURN (PR_CONST P' (PR_CONST l⇩0, PR_CONST s⇩0));
let S = op_map_lookup (PR_CONST l⇩0) M';
case S of None ⇒ RETURN False | Some S ⇒ do {
xs ← SPEC (λxs. set xs = S);
b3 ← monadic_list_ex (λs. RETURN (PR_CONST less_eq (PR_CONST s⇩0) s)) xs;
b4 ← PR_CONST check_prop' L' M';
PRINT_CHECK STR ''Start state is in state list'' b1;
PRINT_CHECK STR ''Start state fulfills property'' b2;
PRINT_CHECK STR ''Start state is subsumed'' b3;
PRINT_CHECK STR ''Check property'' b4;
RETURN (b1 ∧ b2 ∧ b3 ∧ b4)
}
}
"
definition
"check_all' L' M' ≡ do {
b ← check_all_pre' L' M';
if b
then do {
r ← SPEC (λr. r⟶ check_invariant_spec L');
PRINT_CHECK STR ''State set invariant check'' r;
RETURN r
}
else RETURN False
}
"
definition check_init' where
"check_init' S ≡
case S of None ⇒ RETURN False | Some S ⇒ do {
xs ← SPEC (λxs. set xs = S);
monadic_list_ex (λs. RETURN (PR_CONST less_eq (PR_CONST s⇩0) s)) xs
}
"
lemma check_all_pre'_refine:
"check_all_pre' L M ≤ check_all_pre l⇩0 s⇩0"
unfolding check_all_pre_def check_all_pre'_def PR_CONST_def Let_def
using check_prop_gt_SUCCEED
apply (cases "op_map_lookup l⇩0 M"; simp add: bind_RES)
apply (cases "check_prop P'")
apply (clarsimp_all intro: less_eq_Sup simp: bind_RES check_prop_alt_def)
apply (rule less_eq_Sup)
subgoal for a v
apply clarsimp
apply (rule Sup_least)
apply clarsimp
supply [refine_mono] = monadic_list_ex_mono monadic_list_ex_RETURN_mono
apply refine_mono
apply (simp add: PRINT_CHECK_def)
done
subgoal
by (auto dest: M_listD)
done
lemma check_all'_refine:
"check_all' L M ≤ check_all"
supply [refine_mono] = check_all_pre'_refine
unfolding check_all_def check_all'_def PRINT_CHECK_def by refine_mono auto
sepref_register
"PR_CONST check_invariant'" :: "'k list ⇒ ('k, 'b set) i_map ⇒ bool nres"
"PR_CONST check_all_pre'" :: "'k set ⇒ ('k, 'b set) i_map ⇒ bool nres"
"PR_CONST check_prop'" :: "'k set ⇒ ('k, 'b set) i_map ⇒ bool nres"
"PR_CONST check_all'" :: "'k set ⇒ ('k, 'b set) i_map ⇒ bool nres"
"PR_CONST check_final'" :: "'k set ⇒ ('k, 'b set) i_map ⇒ bool nres"
"PR_CONST check_init"
"PR_CONST l⇩0" "PR_CONST s⇩0"
sepref_definition check_init_impl is
"check_init'" :: "(option_assn (lso_assn A))⇧d →⇩a bool_assn"
unfolding check_init'_def list_of_set_def[symmetric]
unfolding monadic_list_all_def monadic_list_ex_def
by sepref
definition
"L_member L' ≡ PR_CONST l⇩0 ∈ L'"
sepref_thm L_member_impl is
"RETURN o PR_CONST L_member" :: "(lso_assn K)⇧k →⇩a id_assn"
unfolding PR_CONST_def unfolding L_member_def by sepref
lemma L_member_fold:
"PR_CONST l⇩0 ∈ L' ≡ PR_CONST L_member L'"
unfolding L_member_def PR_CONST_def .
definition
"lookup (M' :: 'k ⇒ 'a set option) = op_map_lookup (PR_CONST l⇩0) M'"
lemma looukp_fold:
"op_map_lookup (PR_CONST l⇩0) = PR_CONST lookup"
unfolding lookup_def PR_CONST_def ..
sepref_register L_member lookup :: "('k, 'b set) i_map ⇒ 'b set option"
definition check2 where
"check2 b = PR_CONST check_init' (PR_CONST lookup b)"
lemma check2_fold:
"PR_CONST check_init' (PR_CONST lookup b) = PR_CONST check2 b"
unfolding check2_def PR_CONST_def ..
sepref_register check2 :: "('k, 'b set) i_map ⇒ bool nres"
definition check1 where
"check1 = PR_CONST P' (PR_CONST l⇩0, PR_CONST s⇩0)"
lemma check1_fold:
"PR_CONST check1 = PR_CONST P' (PR_CONST l⇩0, PR_CONST s⇩0)"
unfolding check1_def PR_CONST_def ..
sepref_register check1
sepref_thm check1_impl is
"uncurry0 (RETURN (PR_CONST check1))" :: "id_assn⇧k →⇩a id_assn"
unfolding PR_CONST_def unfolding check1_def by sepref
sepref_thm check2_impl is
"PR_CONST check2" :: "table_assn⇧k →⇩a id_assn"
unfolding PR_CONST_def
unfolding check2_def
unfolding PR_CONST_def
unfolding check_init'_def lookup_def
unfolding list_of_set_def[symmetric]
unfolding monadic_list_all_def monadic_list_ex_def
by sepref
lemmas [sepref_fr_rules] =
L_member_impl.refine_raw
check1_impl.refine_raw
check2_impl.refine_raw
check_prop_impl.refine_raw
context
fixes splitter :: "'k list ⇒ 'k list list" and splitteri :: "'ki list ⇒ 'ki list list"
assumes full_split: "set xs = (⋃xs ∈ set (splitter xs). set xs)"
and same_split:
"⋀L Li. list_assn (list_assn K) (splitter L) (splitteri Li) = list_assn K L Li"
begin
definition
"check_invariant_all_impl L' M' ≡ do {
bs ← parallel_fold_map (λL. check_invariant_impl L M') (splitteri L');
return (list_all id bs)
}"
definition
"split_spec ≡ λL M. RETURN (list_all (λx. RETURN True ≤ check_invariant' x M) (splitter L))"
lemma check_invariant_all_impl_refine:
"(uncurry check_invariant_all_impl, uncurry (PR_CONST split_spec))
∈ (list_assn K)⇧k *⇩a table_assn⇧k →⇩a bool_assn"
unfolding split_spec_def PR_CONST_def
apply sepref_to_hoare
apply sep_auto
subgoal for M Mi L Li
unfolding check_invariant_all_impl_def parallel_fold_map_def
apply sep_auto
apply (rule Hoare_Triple.cons_pre_rule[rotated])
apply (rule fold_map_ht2[
where Q = "λL r. RETURN r ≤ check_invariant' L M"
and R = "list_assn K" and A = "table_assn M Mi" and xs = "splitter L"
])
apply (rule Hoare_Triple.cons_post_rule)
apply (rule frame_rule)
apply (rule check_invariant_impl.refine[to_hnr, unfolded hn_refine_def hn_ctxt_def, simplified, rule_format])
subgoal
by (rule check_invariant'_no_fail)
apply (sep_auto simp: pure_def; fail)
subgoal
unfolding same_split by solve_entails
apply sep_auto
subgoal
unfolding list_all_length list_all2_conv_all_nth by auto
subgoal for x
unfolding list_all_length list_all2_conv_all_nth
using check_invariant'_correct_pre1 nres_order_simps(20) Orderings.order.trans
by fastforce
subgoal
unfolding same_split by solve_entails
done
done
sepref_definition check_all_pre_impl is
"uncurry (PR_CONST check_all_pre')" :: "(lso_assn K)⇧k *⇩a table_assn⇧k →⇩a id_assn"
unfolding PR_CONST_def
unfolding check_all_pre'_def list_of_set_def[symmetric]
unfolding monadic_list_all_def monadic_list_ex_def
by sepref
lemma check_all_pre_impl_ht:
"<table_assn b bi * lso_assn K a ai>
check_all_pre_impl ai bi
<λr. table_assn b bi * lso_assn K a ai * ↑ (RETURN r ≤ check_all_pre' a b)>⇩t"
if "nofail (check_all_pre' a b)"
apply (rule cons_post_rule)
apply (rule check_all_pre_impl.refine[to_hnr, unfolded hn_refine_def hn_ctxt_def, simplified, rule_format])
subgoal
by (rule that)
apply (sep_auto simp: pure_def)
done
definition
"check_all'' L' M' ≡ do {
b ← PR_CONST check_all_pre' L' M';
if b
then do {
xs ← SPEC (λxs. set xs = L');
r ← PR_CONST split_spec xs M';
PRINT_CHECK STR ''State set invariant check'' r;
RETURN r
}
else RETURN False
}
"
sepref_register split_spec :: "'k list ⇒ (('k, 'b set) i_map) ⇒ bool nres"
lemmas [sepref_fr_rules] =
check_all_pre_impl.refine_raw
check_invariant_all_impl_refine
sepref_thm check_all_impl is
"uncurry (PR_CONST check_all'')" :: "(lso_assn K)⇧k *⇩a table_assn⇧k →⇩a id_assn"
unfolding PR_CONST_def
unfolding check_all''_def list_of_set_def[symmetric]
by sepref
lemma split_spec_correct:
"split_spec L' M ≤ SPEC (λr. r ⟶ check_invariant_spec_pre L')"
if assms: "dom M = L" "set L' ⊆ L"
proof -
let ?M = "(λl. case M l of None ⇒ {} | Some S ⇒ S)"
have "RETURN True ≤ check_invariant' L_part M ⟶ check_invariant_spec_pre L_part"
if "L_part ∈ set (splitter L')" for L_part
proof -
have "check_invariant' L_part M ≤ RETURN (check_invariant_spec_pre L_part)"
using full_split[of L'] that assms by - (rule check_invariant'_correct_pre, auto)
then show ?thesis
using Orderings.order.trans nres_order_simps(20) by metis
qed
then have "list_all (λx. RETURN True ≤ check_invariant' x M) (splitter L')
⟶ list_all (λxs. check_invariant_spec_pre xs) (splitter L')"
using list.pred_mono_strong by force
moreover have "… ⟶ check_invariant_spec_pre L'"
using full_split[of L'] unfolding list_all_def check_invariant_spec_pre_def by auto
ultimately show ?thesis
unfolding split_spec_def nres_order_simps by simp
qed
lemma
assumes "dom M = L"
shows check_all''_refine1: "check_all'' L M ≤ check_all" (is "?A")
and check_all''_refine2: "check_all'' L M ≤ check_all' L M" (is "?B")
proof -
have *[refine_mono]: "check_invariant_spec L"
if "RETURN True ≤ check_all_pre' L M" "check_invariant_spec_pre xs" "set xs = L" for xs
proof -
note that(1)
also note check_all_pre'_refine
also note check_all_pre_correct
finally show ?thesis
using that P'_P
by (auto simp: check_all_pre_spec_def check_invariant_spec_pre_eq_check_invariant_spec)
qed
note [refine_mono] = check_all_pre'_refine split_spec_correct
show ?A
using assms
unfolding check_all''_def check_all_def PR_CONST_def
apply -
apply (rule Refine_Basic.bind_mono, refine_mono)
apply refine_mono
apply (rule specify_left, refine_mono)
apply (rule specify_left, refine_mono, (simp; fail))
apply (simp add: PRINT_CHECK_def)
using * by clarsimp
show ?B
using assms
unfolding check_all''_def check_all'_def PR_CONST_def
apply -
apply (rule Refine_Basic.bind_mono, refine_mono)
apply refine_mono
apply (rule specify_left, refine_mono)
apply refine_mono
apply (rule Orderings.order.trans, refine_mono)
using * by clarsimp+
qed
sepref_thm check_all_impl is
"uncurry (PR_CONST check_all')" :: "(lso_assn K)⇧k *⇩a table_assn⇧k →⇩a id_assn"
unfolding PR_CONST_def
unfolding check_all'_def list_of_set_def[symmetric]
unfolding monadic_list_all_def monadic_list_ex_def
oops
sepref_thm check_all_impl is
"uncurry (PR_CONST check_all')" :: "(lso_assn K)⇧k *⇩a table_assn⇧k →⇩a id_assn"
unfolding PR_CONST_def
unfolding check_all'_def check_all_pre'_def list_of_set_def[symmetric]
unfolding monadic_list_all_def monadic_list_ex_def
oops
lemma certify_unreachable_alt_def:
"certify_unreachable ≡ do {
b1 ← PR_CONST check_all;
b2 ← PR_CONST check_final;
RETURN (b1 ∧ b2)
}"
unfolding certify_unreachable_def PR_CONST_def .
definition certify_unreachable' where
"certify_unreachable' L' M' ≡ do {
START_TIMER ();
b1 ← PR_CONST check_all'' L' M';
SAVE_TIME STR ''Time for state space invariant check'';
START_TIMER ();
b2 ← PR_CONST check_final' L' M';
SAVE_TIME STR ''Time to check final state predicate'';
PRINT_CHECK STR ''All check: '' b1;
PRINT_CHECK STR ''Target property check: '' b2;
RETURN (b1 ∧ b2)
}"
lemma certify_unreachable'_refine:
"certify_unreachable' L M ≤ certify_unreachable" if "L = dom M"
unfolding certify_unreachable'_def certify_unreachable_def PR_CONST_def check_final_alt_def
unfolding PRINT_CHECK_def START_TIMER_def SAVE_TIME_def
using check_all''_refine1 that by simp refine_mono
sepref_register
"PR_CONST check_all''" :: "'k set ⇒ (('k, 'b set) i_map) ⇒ bool nres"
"PR_CONST check_final"
lemmas [sepref_fr_rules] =
check_all_impl.refine_raw
check_final_impl.refine_raw
sepref_thm certify_unreachable_impl' is
"uncurry (PR_CONST certify_unreachable')" :: "(lso_assn K)⇧k *⇩a table_assn⇧k →⇩a id_assn"
unfolding PR_CONST_def unfolding certify_unreachable'_def
by sepref
lemma certify_unreachable_correct':
"(uncurry0 (certify_unreachable' L M), uncurry0 (SPEC (λr. r ⟶ (∄s'. E⇧*⇧* (l⇩0, s⇩0) s' ∧ F s'))))
∈ Id → ⟨bool_rel⟩nres_rel" if "L = dom M"
using certify_unreachable_correct' certify_unreachable'_refine[OF that]
by (clarsimp simp: pw_le_iff pw_nres_rel_iff) fast
lemmas certify_unreachable_impl'_refine =
certify_unreachable_impl'.refine_raw[
unfolded is_member_impl_def[OF pure_K left_unique_K right_unique_K]
check_invariant_all_impl_def check_invariant_impl_def
]
definition certify_unreachable_new where
"certify_unreachable_new L_list M_table ≡ let
_ = start_timer ();
b1 = run_heap (do {M' ← M_table; check_all_pre_impl L_list M'});
_ = save_time STR ''Time for checking basic preconditions'';
_ = start_timer ();
xs = run_map_heap (λLi. do {M' ← M_table; check_invariant_impl Li M'}) (splitteri L_list);
b2 = list_all id xs;
_ = save_time STR ''Time for state space invariant check'';
_ = print_check STR ''State set invariant check'' b2;
_ = start_timer ();
b3 = run_heap (do {M' ← M_table; check_final_impl Fi copyi L_list M'});
_ = save_time STR ''Time to check final state predicate'';
_ = print_check STR ''All check: '' (b1 ∧ b2);
_ = print_check STR ''Target property check: '' b3
in b1 ∧ b2 ∧ b3"
lemmas certify_unreachable_new_alt_def =
certify_unreachable_new_def[unfolded
check_invariant_impl_def
check_all_pre_impl_def
is_member_impl_def[OF pure_K left_unique_K right_unique_K]
]
end
concrete_definition (in -) check_all_impl
uses Reachability_Impl.check_all_impl.refine_raw is "(uncurry ?f,_)∈_"
concrete_definition (in -) certify_unreachable_impl_inner
uses Reachability_Impl.certify_unreachable_impl'_refine is "(uncurry ?f,_)∈_"
lemmas certify_unreachable'_impl_hnr =
certify_unreachable_impl_inner.refine[OF Reachability_Impl_axioms]
concrete_definition (in -) certify_unreachable_impl2
uses Reachability_Impl.certify_unreachable_new_alt_def
context
fixes L_list and M_table
assumes L_impl[sepref_fr_rules]:
"(uncurry0 (return L_list), uncurry0 (RETURN (PR_CONST L))) ∈ id_assn⇧k →⇩a lso_assn K"
assumes M_impl[sepref_fr_rules]:
"(uncurry0 M_table, uncurry0 (RETURN (PR_CONST M))) ∈ id_assn⇧k →⇩a hm.hms_assn' K (lso_assn A)"
fixes splitter :: "'k list ⇒ 'k list list" and splitteri :: "'ki list ⇒ 'ki list list"
assumes full_split: "set xs = (⋃xs ∈ set (splitter xs). set xs)"
and same_split:
"⋀L Li. list_assn (list_assn K) (splitter L) (splitteri Li) = list_assn K L Li"
begin
lemmas [sepref_fr_rules] = certify_unreachable'_impl_hnr[OF full_split same_split]
sepref_register
"certify_unreachable' splitter" :: "'k set ⇒ ('k, 'b set) i_map ⇒ bool nres"
sepref_thm certify_unreachable_impl is
"uncurry0 (PR_CONST (certify_unreachable' splitter) (PR_CONST L) (PR_CONST M))"
:: "id_assn⇧k →⇩a id_assn"
by sepref_dbg_keep
lemmas certify_unreachable_impl_refine =
certify_unreachable_impl.refine_raw[
unfolded PR_CONST_def is_member_impl_def[OF pure_K left_unique_K right_unique_K],
FCOMP certify_unreachable_correct'[OF full_split same_split]
]
lemma certify_unreachable_new_correct:
assumes "dom M = L"
shows "certify_unreachable_new splitteri L_list M_table ⟶ (∄s'. E⇧*⇧* (l⇩0, s⇩0) s' ∧ F s')"
proof -
have [sep_heap_rules]: "<emp> M_table <λr. hm.hms_assn' K (lso_assn A) M r>⇩t"
by (sep_auto simp: pure_def heap: M_impl[to_hnr, unfolded hn_refine_def, simplified])
have true_emp: "true = emp * true"
by simp
have *: "emp ⟹⇩A lso_assn K L L_list * true"
using L_impl[to_hnr, unfolded hn_refine_def, simplified]
apply -
apply (drule return_htD)
apply (erule ent_trans)
apply (sep_auto simp: pure_def)
done
then have *: "true ⟹⇩A lso_assn K L L_list * true"
by (subst true_emp) (erule ent_true_drop)
have check_all_pre'_refine: "check_all_pre' L M ≤ RETURN (check_all_pre_spec l⇩0 s⇩0)"
by (blast intro: check_all_pre_correct check_all_pre'_refine Orderings.order.trans)
have list_assn_K_eq: "list_assn K = pure (⟨the_pure K⟩list_rel)"
using pure_K by (simp add: list_assn_pure_conv[symmetric])
have 1: "
<emp>
do {M' ← M_table; check_all_pre_impl L_list M'}
<λr. ↑ (r ⟶ check_all_pre_spec l⇩0 s⇩0)>⇩t"
apply sep_auto
subgoal for Mi
apply (rule cons_rule[rotated 2])
apply (rule frame_rule[where R = true])
apply (rule check_all_pre_impl_ht[OF full_split same_split, where a = L and b = M])
subgoal
using check_all_pre'_refine unfolding RETURN_def by (rule le_RES_nofailI)
subgoal
using * by (elim ent_frame_fwd) solve_entails+
subgoal
apply sep_auto
apply (drule Orderings.order.trans, rule check_all_pre'_refine)
apply auto
done
done
done
have 3: "
<emp>
do {M' ← M_table; check_final_impl Fi copyi L_list M'}
<λr. ↑(r ⟶ check_final_spec)>⇩t"
apply (sep_auto)
subgoal for Mi
apply (rule cons_rule[rotated 2])
apply (rule frame_rule[where R = true])
apply (rule check_final_impl.refine[
OF Reachability_Impl_axioms, to_hnr, unfolded hn_refine_def hn_ctxt_def, simplified,
rule_format, where a = L and b = M])
subgoal
using check_final_nofail unfolding check_final_alt_def .
subgoal
using * by (elim ent_frame_fwd) solve_entails+
subgoal
apply sep_auto
unfolding check_final_alt_def
apply (drule Orderings.order.trans, rule check_final_correct)
apply (sep_auto simp: pure_def)
done
done
done
have 2: "
<emp>
do {M' ← M_table; check_invariant_impl Li M'}
<λr. ↑(r ⟶ check_invariant_spec (set L'))>⇩t
" if
"∀l∈L. ∀s∈the (M l). P (l, s)"
"Li ∈ set (splitteri L_list)" "(Li, L') ∈ ⟨(the_pure K)⟩list_rel" "set L' ⊆ L"
for Li L'
apply sep_auto
subgoal for Mi
apply (rule cons_rule[rotated 2])
apply (rule frame_rule[where R = true])
apply (rule check_invariant_impl_ht[where bi = Mi and a = L'])
using that check_invariant'_no_fail ‹dom M = L› by (auto simp: list_assn_K_eq pure_def)
done
have "
emp ⟹⇩A ∃⇩ALL. ↑(list_all2 (λLi Lp. list_all2 (λxi x. (xi, x) ∈ the_pure K) Li Lp)
(splitteri L_list) (splitter LL)
∧ set LL = L) * true"
using ‹emp ⟹⇩A lso_assn K L L_list * true›
apply (rule ent_trans)
apply (sep_auto simp: br_def lso_assn_def hr_comp_def same_split[symmetric])
apply (sep_auto simp: list_assn_K_eq list_assn_pure_conv)
apply (sep_auto simp: pure_def list_rel_def; fail)
apply simp
done
then obtain LL where LL: "set LL = L" "length (splitter LL) = length (splitteri L_list)"
"∀n < length (splitter LL). (splitteri L_list ! n, splitter LL ! n) ∈ ⟨the_pure K⟩list_rel"
by (simp add: list_rel_def list_all2_conv_all_nth)
(smt (verit) ent_ex_preI ent_iffI ent_pure_pre_iff ent_pure_pre_iff_sng pure_assn_eq_emp_iff)
have 2: "check_invariant_spec L"
if "check_all_pre_spec l⇩0 s⇩0"
"list_all id (run_map_heap (λLi. M_table ⤜ check_invariant_impl Li) (splitteri L_list))"
proof -
let ?c = "(λLi. M_table ⤜ check_invariant_impl Li)"
have A: "∀l∈L. ∀s∈the (M l). P (l, s)"
using ‹check_all_pre_spec l⇩0 s⇩0› ‹dom M = L›
unfolding check_all_pre_spec_def by (force intro: P'_P)
have
"list_all2 (λL' r. r ⟶ check_invariant_spec (set L'))
(splitter LL) (run_map_heap ?c (splitteri L_list))"
using LL
apply -
apply (rule hoare_triple_run_map_heapD')
apply (rule list_all2_all_nthI, assumption)
apply (rule 2[OF A]; simp)
unfolding ‹set LL = L›[symmetric] by (subst (2) full_split) force
then have "list_all (λL'. check_invariant_spec (set L')) (splitter LL)"
using that(2) unfolding list_all2_conv_all_nth list_all_length by simp
with full_split[of LL] show ?thesis
unfolding list_all_iff check_invariant_spec_def ‹set LL = L› by auto
qed
show ?thesis
apply standard
apply (rule certify_unreachableI[rule_format])
using hoare_triple_run_heapD[OF 1] hoare_triple_run_heapD[OF 3]
unfolding certify_unreachable_new_def[OF full_split same_split] check_all_spec_def
by (auto intro: 2)
qed
lemmas certify_unreachable_impl2_refine =
certify_unreachable_new_correct[
unfolded certify_unreachable_impl2.refine[OF Reachability_Impl_axioms full_split same_split]
]
end
concrete_definition (in -) certify_unreachable_impl
uses Reachability_Impl.certify_unreachable_impl_refine is "(uncurry0 ?f,_)∈_"
paragraph ‹Debugging›
definition (in -)
"mk_st_string s1 s2 ≡ STR ''<'' + s1 + STR '', '' + s2 + STR ''>''"
lemma [sepref_import_param]: "(mk_st_string, mk_st_string) ∈ Id → Id → Id"
by simp
definition (in -)
"PRINTLN = RETURN o println"
lemma (in -) [sepref_import_param]:
"(println, println) ∈ Id → Id"
by simp
sepref_definition (in -) print_line_impl is
"PRINTLN" :: " id_assn⇧k →⇩a id_assn"
unfolding PRINTLN_def by sepref
sepref_register (in -) PRINTLN
lemmas [sepref_fr_rules] = print_line_impl.refine
context
fixes show_loc :: "'k ⇒ String.literal nres" and show_dbm :: "'a ⇒ String.literal nres"
and show_dbm_impl and show_loc_impl
assumes show_dbm_impl: "(show_dbm_impl, show_dbm) ∈ A⇧d →⇩a id_assn"
assumes show_loc_impl: "(show_loc_impl, show_loc) ∈ K⇧d →⇩a id_assn"
begin
lemma [sepref_fr_rules]: "(show_dbm_impl, PR_CONST show_dbm) ∈ A⇧d →⇩a id_assn"
using show_dbm_impl unfolding PR_CONST_def .
lemma [sepref_fr_rules]: "(show_loc_impl, PR_CONST show_loc) ∈ K⇧d →⇩a id_assn"
using show_loc_impl unfolding PR_CONST_def .
definition
"show_st ≡ λ (l, M). do {
s1 ← PR_CONST show_loc l;
s2 ← PR_CONST show_dbm M;
RETURN (mk_st_string s1 s2)
}"
sepref_register "PR_CONST show_st" "PR_CONST show_loc" "PR_CONST show_dbm"
sepref_thm show_st_impl is
"PR_CONST show_st" :: "(K ×⇩a A)⇧d →⇩a id_assn"
unfolding PR_CONST_def unfolding show_st_def by sepref
lemmas [sepref_fr_rules] = show_st_impl.refine_raw
definition check_prop_fail where
"check_prop_fail L' M' = do {
l ← SPEC (λxs. set xs = L');
r ← monadic_list_all_fail' (λl. do {
let S = op_map_lookup l M';
case S of None ⇒ RETURN None | Some S ⇒ do {
xs ← SPEC (λxs. set xs = S);
r ← monadic_list_all_fail (λs.
RETURN (PR_CONST P' (l, s))
) xs;
RETURN (case r of None ⇒ None | Some r ⇒ Some (l, r))
}
}
) l;
case r of None ⇒ RETURN None |
Some (l, M) ⇒ do {
s ← PR_CONST show_st (l, COPY M);
PRINTLN (STR ''Prop failed for: '');
PRINTLN s;
RETURN (Some (l, M))
}
}"
sepref_thm check_prop_fail_impl is
"uncurry check_prop_fail" :: "(lso_assn K)⇧k *⇩a table_assn⇧d →⇩a option_assn (K ×⇩a A)"
unfolding check_prop_fail_def list_of_set_def[symmetric]
unfolding monadic_list_all_fail'_alt_def monadic_list_all_fail_alt_def
by sepref
end
definition
"check_invariant_fail L' M' ≡ do {
l ← SPEC (λxs. set xs = L');
monadic_list_all_fail' (λl.
do {
case op_map_lookup l M' of None ⇒ RETURN None | Some as ⇒ do {
let succs = PR_CONST succs l as;
monadic_list_all_fail' (λ(l', xs). do {
xs ← SPEC (λxs'. set xs' = xs);
if xs = [] then RETURN None
else do {
b1 ← RETURN (l' ∈ L');
if b1 then do {
case op_map_lookup l' M' of None ⇒ RETURN (Some (Inl (Inr (l, l', xs)))) | Some ys ⇒ do {
ys ← SPEC (λxs. set xs = ys);
b2 ← monadic_list_all_fail (λx'.
monadic_list_ex (λy. RETURN (PR_CONST less_eq x' y)) ys
) xs;
case b2 of None ⇒ RETURN None | Some M ⇒ do {
case op_map_lookup l M' of
None ⇒ RETURN (Some (Inl (Inr (l, l', ys))))
| Some as ⇒ do {
as ← SPEC (λxs'. set xs' = as);
RETURN (Some (Inr (l, as, l', M, ys)))}
}
}
}
else RETURN (Some (Inl (Inl (l, l', xs))))
}
}) succs
}
}
) l
}"
sepref_thm check_invariant_fail_impl is
"uncurry check_invariant_fail"
:: "(lso_assn K)⇧k *⇩a table_assn⇧k →⇩a
option_assn ((K ×⇩a K ×⇩a list_assn A +⇩a K ×⇩a K ×⇩a list_assn A) +⇩a K ×⇩a list_assn A ×⇩a K ×⇩a A ×⇩a list_assn A)"
unfolding PR_CONST_def
unfolding check_invariant_fail_def list_of_set_def[symmetric]
unfolding monadic_list_all_fail'_alt_def monadic_list_all_fail_alt_def
unfolding monadic_list_all_def monadic_list_ex_def
by sepref
lemmas check_invariant_fail_impl_refine = check_invariant_fail_impl.refine_raw[
unfolded is_member_impl_def[OF pure_K left_unique_K right_unique_K]
]
end
concrete_definition (in -) check_prop_fail_impl
uses Reachability_Impl.check_prop_fail_impl.refine_raw is "(uncurry ?f,_)∈_"
concrete_definition (in -) check_invariant_fail_impl
uses Reachability_Impl.check_invariant_fail_impl_refine is "(uncurry ?f,_)∈_"
export_code
certify_unreachable_impl certify_unreachable_impl2 check_prop_fail_impl check_invariant_fail_impl
in SML module_name Test
end