Theory Normalized_Zone_Semantics_Certification_Impl2
theory Normalized_Zone_Semantics_Certification_Impl2
imports
Normalized_Zone_Semantics_Certification_Impl
Unreachability_Certification
begin
context Reachability_Problem_Impl_Precise
begin
context
fixes L_list :: "'si list" and P_loc and M_list :: "('si × int DBMEntry list list) list"
assumes state_impl_abstract: "⋀li. P_loc li ⟹ ∃l. (li, l) ∈ loc_rel"
assumes P_loc: "list_all (λx. P_loc x ∧ states_mem_impl x) L_list"
assumes M_list_covered: "fst ` set M_list ⊆ set L_list"
and M_dbm_len: "list_all (λ(l, xs). list_all (λM. length M = Suc n * Suc n) xs) M_list"
begin
lemmas table_axioms = state_impl_abstract P_loc M_list_covered M_dbm_len
context
fixes splitter :: "'s list ⇒ 's list list" and splitteri :: "'si list ⇒ 'si list list"
assumes full_split: "set xs = (⋃xs ∈ set (splitter xs). set xs)"
and same_split:
"⋀L Li.
list_assn (list_assn location_assn) (splitter L) (splitteri Li) = list_assn location_assn L Li"
begin
lemma certify_unreachable_impl_hnr:
assumes "set (L L_list) = dom (M M_list)"
shows
"(uncurry0
(certify_unreachable_impl F_impl P_impl amtx_copy (dbm_subset_impl n) succs_precise'_impl
(return l⇩0i) init_dbm_impl L_list (M_table M_list) splitteri),
uncurry0 (SPEC (λr. r ⟶
(∄u l' u'. (∀c≤n. u c = 0) ∧ conv_A A ⊢' ⟨l⇩0, u⟩ →* ⟨l', u'⟩ ∧ F' (l', u')))))
∈ unit_assn⇧k →⇩a bool_assn"
by (rule certify_unreachable_impl_hnr)
(rule table_axioms full_split same_split L_dom_M_eqI[symmetric] assms | assumption)+
definition
"unreachability_checker' ≡
let
Fi = F_impl;
Pi = P_impl;
copyi = amtx_copy;
Lei = dbm_subset_impl n;
l⇩0i = Heap_Monad.return l⇩0i;
s⇩0i = init_dbm_impl;
succsi = succs_precise'_impl;
M_table = M_table M_list
in
certify_unreachable_impl Fi Pi copyi Lei succsi l⇩0i s⇩0i L_list M_table splitteri"
lemma unreachability_checker_alt_def:
"unreachability_checker' ≡
let
Fi = F_impl;
Pi = P_impl;
copyi = amtx_copy;
Lei = dbm_subset_impl n;
l⇩0i = Heap_Monad.return l⇩0i;
s⇩0i = init_dbm_impl;
succsi = succs_precise'_impl
in do {
M_table ← M_table M_list;
certify_unreachable_impl_inner Fi Pi copyi Lei succsi l⇩0i s⇩0i splitteri L_list M_table
}"
unfolding unreachability_checker'_def certify_unreachable_impl_def Let_def .
lemmas unreachability_checker_hnr =
certify_unreachable_impl_hnr[folded unreachability_checker'_def[unfolded Let_def]]
lemmas unreachability_checker_alt_def' = unreachability_checker_alt_def[unfolded M_table_def]
definition
"unreachability_checker2' ≡
let
Fi = F_impl;
Pi = P_impl;
copyi = amtx_copy;
Lei = dbm_subset_impl n;
l⇩0i = Heap_Monad.return l⇩0i;
s⇩0i = init_dbm_impl;
succsi = succs_precise'_impl;
M_table = M_table M_list
in
certify_unreachable_impl2 Fi Pi copyi Lei succsi l⇩0i s⇩0i splitteri L_list M_table"
lemma unreachability_checker2_refine:
assumes "fst ` set M_list = set L_list" "unreachability_checker2 L_list M_list splitteri"
shows "∄u l' u'. (∀c≤n. u c = 0) ∧ conv_A A ⊢' ⟨l⇩0, u⟩ →* ⟨l', u'⟩ ∧ F' (l', u')"
by (rule unreachability_checker2_refine table_axioms assms full_split same_split | assumption)+
lemma unreachability_checker2'_is_unreachability_checker2:
"unreachability_checker2' = unreachability_checker2 L_list M_list splitteri"
unfolding unreachability_checker2'_def
by (subst unreachability_checker2_def)
(rule table_axioms full_split same_split HOL.refl | assumption)+
end
end
end
context TA_Impl_Precise
begin
lemma (in TA_Impl) dbm_subset_correct:
assumes "wf_dbm D" and "wf_dbm M"
shows "[curry (conv_M D)]⇘v,n⇙ ⊆ [curry (conv_M M)]⇘v,n⇙ ⟷ dbm_subset n D M"
unfolding dbm_subset_correct''[OF assms] using dbm_subset_conv_rev dbm_subset_conv ..
lemma empty_steps_states':
"l' ∈ states'" if "op_precise.E_from_op_empty⇧*⇧* (l, D) (l', D')" "l ∈ states'"
using that
proof (induction "(l, D)" "(l', D')" arbitrary: l' D')
case rtrancl_refl
then show ?case
by simp
next
case (rtrancl_into_rtrancl b)
then show ?case
by (cases b) (auto simp add: op_precise.E_from_op_empty_def intro: E_from_op_states)
qed
interpretation deadlock: Reachability_Problem_Impl_Precise where
F = "λ(l, D). ¬ (check_deadlock_dbm l D)" and
F1 = "λ(l, Z). ¬ (TA.check_deadlock l Z)" and
F' = deadlocked and
F_impl = "λ(l, M). do {r ← check_deadlock_impl l M; return (¬ r)}"
apply standard
subgoal for a b
apply clarsimp
apply (auto dest: TA.check_deadlock_anti_mono simp:
dbm_subset_correct[symmetric] check_deadlock_dbm_correct'[symmetric, unfolded wf_state_def])
done
subgoal
using
Bisimulation_Invariant.B_steps_invariant[OF op_precise.step_z_dbm'_E_from_op_bisim_empty]
wf_state_init states'_states
unfolding a⇩0_def
by simp (subst check_deadlock_dbm_correct'[symmetric], auto elim: empty_steps_states')
subgoal for l u Z
unfolding TA.check_deadlock_correct_step' deadlocked_def by auto
subgoal
proof -
define location_assn' where "location_assn' = location_assn"
define mtx_assn' :: "_ ⇒ int DBMEntry Heap.array ⇒ _" where "mtx_assn' = mtx_assn n"
note [sep_heap_rules] = check_deadlock_impl.refine[
to_hnr, unfolded hn_refine_def hn_ctxt_def,
folded location_assn'_def mtx_assn'_def, simplified]
show ?thesis
unfolding location_assn'_def[symmetric] mtx_assn'_def[symmetric]
by sepref_to_hoare (sep_auto simp: pure_def)
qed
done
lemma deadlock_unreachability_checker2_hnr:
fixes P_loc :: "'si ⇒ bool"
and L_list :: "'si list"
and M_list :: "('si × int DBMEntry list list) list"
fixes splitter :: "'s list ⇒ 's list list" and splitteri :: "'si list ⇒ 'si list list"
assumes "⋀li. P_loc li ⟹ ∃l. (li, l) ∈ loc_rel"
and "list_all (λx. P_loc x ∧ states_mem_impl x) L_list"
and "list_all (λ(l, xs). list_all (λM. length M = Suc n * Suc n) xs) M_list"
and "fst ` set M_list = set L_list"
assumes full_split: "⋀xs. set xs = (⋃xs ∈ set (splitter xs). set xs)"
and same_split:
"⋀L Li.
list_assn (list_assn location_assn) (splitter L) (splitteri Li) = list_assn location_assn L Li"
shows
"deadlock.unreachability_checker2 L_list M_list splitteri
⟶ (∀u. (∀c≤n. u c = 0) ⟶ ¬ deadlock (l⇩0, u))"
using deadlock.unreachability_checker2_refine[
OF assms(1-2) assms(4)[THEN equalityD1] assms(3) full_split same_split assms(4)
]
unfolding deadlock_def steps'_iff[symmetric] by auto
lemma deadlock_unreachability_checker3_hnr:
fixes P_loc :: "'si ⇒ bool"
and L_list :: "'si list"
and M_list :: "('si × int DBMEntry list list) list"
fixes Li_split :: "'si list list"
assumes "⋀li. P_loc li ⟹ ∃l. (li, l) ∈ loc_rel"
and "list_all (λx. P_loc x ∧ states_mem_impl x) L_list"
and "list_all (λ(l, xs). list_all (λM. length M = Suc n * Suc n) xs) M_list"
and "fst ` set M_list = set L_list"
assumes full_split: "set L_list = (⋃xs ∈ set Li_split. set xs)"
shows
"deadlock.certify_unreachable_pure L_list M_list Li_split
⟶ (∀u. (∀c≤n. u c = 0) ⟶ ¬ deadlock (l⇩0, u))"
using deadlock.certify_unreachable_pure_refine[
OF assms(1-2) assms(4)[THEN equalityD1] assms(3) full_split assms(4)
]
unfolding deadlock_def steps'_iff[symmetric] by auto
lemmas deadlock_unreachability_checker2_def = deadlock.unreachability_checker2_def
lemmas deadlock_unreachability_checker_alt_def = deadlock.unreachability_checker_alt_def
lemmas deadlock_unreachability_checker3_def = deadlock.certify_unreachable_pure_def
lemma deadlock_unreachability_checker_hnr:
fixes P_loc :: "'si ⇒ bool"
and L_list :: "'si list"
and M_list :: "('si × int DBMEntry list list) list"
fixes splitter :: "'s list ⇒ 's list list" and splitteri :: "'si list ⇒ 'si list list"
assumes "⋀li. P_loc li ⟹ ∃l. (li, l) ∈ loc_rel"
and "list_all (λx. P_loc x ∧ states_mem_impl x) L_list"
and "fst ` set M_list ⊆ set L_list"
and "list_all (λ(l, xs). list_all (λM. length M = Suc n * Suc n) xs) M_list"
and "set (deadlock.L L_list) = dom (deadlock.M M_list)"
assumes full_split: "⋀xs. set xs = (⋃xs ∈ set (splitter xs). set xs)"
and same_split:
"⋀L Li.
list_assn (list_assn location_assn) (splitter L) (splitteri Li) = list_assn location_assn L Li"
shows
"(uncurry0
(Reachability_Problem_Impl_Precise.unreachability_checker' n trans_impl l⇩0i op_impl
states_mem_impl (λ(l, M). check_deadlock_impl l M ⤜ (λr. return (¬ r))) L_list M_list splitteri),
uncurry0
(SPEC
(λr. r ⟶ (∀u. (∀c≤n. u c = 0) ⟶ ¬ deadlock (l⇩0, u)))))
∈ unit_assn⇧k →⇩a bool_assn"
using deadlock.unreachability_checker_hnr[OF assms(1-4), OF _ full_split same_split assms(5)]
unfolding deadlock_def steps'_iff[symmetric] by simp linarith
end
concrete_definition (in -) unreachability_checker
uses Reachability_Problem_Impl_Precise.unreachability_checker_alt_def
end