Theory Abstract_Checks
theory Abstract_Checks
imports Check_Result Checks "Voblint_Domain.Numeric_Queries"
"Voblint_Domain.Forward_Domain" "Voblint_Domain.Three_Valued"
begin
section ‹A domain-generic sound decision procedure for compiled checks›
text ‹
A check needs two capabilities every domain with an ‹exp› evaluator already
has: ‹aval_abs_sound›-shaped soundness (\<^locale>‹sound_evaluator›, the same
reuse point the ‹sound_refinement› locale takes for its own ‹aval_abs›) and the
relational queries of \<^locale>‹sound_numeric_queries›
(\<^theory>‹Voblint_Domain.Numeric_Queries›). Extending
‹sound_numeric_queries› directly, rather than fixing four raw
entailment/refutation predicates here, means there is exactly one relational
query interface in this codebase -- ‹less›/‹eq› -- and every check-discharge
consumer of it inherits whatever a domain already proved for
\<^locale>‹sound_numeric_queries› instead of restating it.
The per-domain guard machinery (the ‹sound_refinement› locale's
‹bfilter›/‹afilter›) would also decide a check: if ‹bfilter c False d›
represents no states, ‹c› is soundly established on ‹d›, whenever
‹gamma bot = {}› --- a sound sufficient condition, not an iff, since no
completeness result for ‹bfilter› is proved here. It is not usable as an
executable decision procedure over ‹'a abs_state›, though: that is a raw
function ‹vname ⇒ 'a› over the infinite type ‹vname›, so its emptiness test
is not code-generable.
This layer decides entailment directly off ‹aval_abs› results via ‹less›/
‹eq›. The judgments are sound but intentionally incomplete: two atomic
values with overlapping concretizations are neither provably related nor
provably unrelated, and are reported ‹None›/‹Check_Unknown›, never
misclassified.
›
locale sound_check_query =
sound_numeric_queries less eq + sound_evaluator γ⇩S aval_abs
for less :: "'a::numeric_domain ⇒ 'a ⇒ bool option"
and eq :: "'a ⇒ 'a ⇒ bool option"
and γ⇩S :: "'d ⇒ store set"
and aval_abs :: "exp ⇒ 'd ⇒ 'a" ("⟦_⟧⇧♯")
begin
subsection ‹A single three-valued decision procedure over \<^typ>‹exp››
text ‹
‹check_query› replaces a mutually recursive true/false judgment pair with
one function into \<^typ>‹bool option›, matching the shape
\<^locale>‹sound_numeric_queries› already gives its two atomic queries:
‹Some True› means definitely true, ‹Some False› definitely false, ‹None›
undecided. ‹Not› negates through @{const map_option}; ‹And›/‹Or› combine
through @{const and_opt}/@{const or_opt}; ‹Less›/‹Eq› read ‹less›/‹eq›
directly; every other expression falls back to testing it against zero
through ‹eq›, negated -- \<^const>‹truthy› is C's non-zero test, so an
expression is true exactly when it is not equal to zero.
›
definition truthy_query :: "exp ⇒ 'd ⇒ bool option" where
[code]: "truthy_query e d = map_option HOL.Not (eq (⟦e⟧⇧♯ d) (⟦N 0⟧⇧♯ d))"
lemma truthy_query_sound:
assumes mem: "s ∈ γ⇩S d"
and query: "truthy_query e d = Some r"
shows "truthy (⟦e⟧⇩e s) = r"
using assms aval_abs_sound eq_sound truthy_query_def
by fastforce
fun check_query :: "exp ⇒ 'd ⇒ bool option" where
"check_query (Not b) d = map_option HOL.Not (check_query b d)"
| "check_query (And b1 b2) d = and_opt (check_query b1 d) (check_query b2 d)"
| "check_query (Or b1 b2) d = or_opt (check_query b1 d) (check_query b2 d)"
| "check_query (Less a b) d = less (⟦a⟧⇧♯ d) (⟦b⟧⇧♯ d)"
| "check_query (LessEq a b) d = map_option HOL.Not (less (⟦b⟧⇧♯ d) (⟦a⟧⇧♯ d))"
| "check_query (Greater a b) d = less (⟦b⟧⇧♯ d) (⟦a⟧⇧♯ d)"
| "check_query (GreaterEq a b) d = map_option HOL.Not (less (⟦a⟧⇧♯ d) (⟦b⟧⇧♯ d))"
| "check_query (Eq a b) d = eq (⟦a⟧⇧♯ d) (⟦b⟧⇧♯ d)"
| "check_query (NotEq a b) d = map_option HOL.Not (eq (⟦a⟧⇧♯ d) (⟦b⟧⇧♯ d))"
| "check_query e d = truthy_query e d"
text ‹Soundness of the arithmetic fallback, proved once and cited by every
induction case it covers (‹N›/‹V›/‹Plus›/‹Minus›/‹Times›). Naming the
fallback ‹truthy_query› rather than inlining the ‹map_option› expression
keeps ‹check_query.simps› a plain one-step rewrite for these five cases, so
‹auto› can chain straight into this lemma instead of first landing on
‹map_option›'s own case split.›
theorem check_query_sound:
assumes mem: "s ∈ γ⇩S d"
shows "check_query c d = Some r ⟹ truthy (⟦c⟧⇩e s) = r"
using truthy_query_sound[OF mem] proof (induction c arbitrary: r)
case (And b1 b2)
then show ?case
using and_opt_sound by auto
next
case (Or b1 b2)
text ‹Unlike ‹And›, this case names the two concrete disjuncts: ‹or_opt_sound›
quantifies over the propositions its two options stand for, and nothing in
the goal determines them by unification.›
then show ?case
using or_opt_sound[of "check_query b1 d" "check_query b2 d" r
"truthy (⟦b1⟧⇩e s)" "truthy (⟦b2⟧⇩e s)"]
by auto
next
case (Less a b)
then show ?case using aval_abs_sound mem less_sound by auto
next
case (Eq a b)
then show ?case using aval_abs_sound mem eq_sound by auto
next
case (LessEq a b)
have query: "less (⟦b⟧⇧♯ d) (⟦a⟧⇧♯ d) = Some (¬ r)"
using LessEq.prems by (auto split: option.splits)
have relation: "(⟦b⟧⇩e s < ⟦a⟧⇩e s) = (¬ r)"
by (rule less_sound[OF query aval_abs_sound[OF mem] aval_abs_sound[OF mem]])
show ?case using relation by auto
next
case (Greater a b)
have query: "less (⟦b⟧⇧♯ d) (⟦a⟧⇧♯ d) = Some r"
using Greater.prems by simp
have relation: "(⟦b⟧⇩e s < ⟦a⟧⇩e s) = r"
by (rule less_sound[OF query aval_abs_sound[OF mem] aval_abs_sound[OF mem]])
show ?case using relation by simp
next
case (GreaterEq a b)
have query: "less (⟦a⟧⇧♯ d) (⟦b⟧⇧♯ d) = Some (¬ r)"
using GreaterEq.prems by (auto split: option.splits)
have relation: "(⟦a⟧⇩e s < ⟦b⟧⇩e s) = (¬ r)"
by (rule less_sound[OF query aval_abs_sound[OF mem] aval_abs_sound[OF mem]])
show ?case using relation by auto
next
case (NotEq a b)
have query: "eq (⟦a⟧⇧♯ d) (⟦b⟧⇧♯ d) = Some (¬ r)"
using NotEq.prems by (auto split: option.splits)
have relation: "(⟦a⟧⇩e s = ⟦b⟧⇩e s) = (¬ r)"
by (rule eq_sound[OF query aval_abs_sound[OF mem] aval_abs_sound[OF mem]])
show ?case using relation by auto
qed (fastforce+)
subsection ‹Executable three-way classification›
text ‹
‹classify_check› turns the check query into proved, refuted or unknown.
A proved check holds in every concretized store and a refuted one fails in each.
›
definition classify_check :: "exp ⇒ 'd ⇒ check_result" where
"classify_check c d =
(case check_query c d of
Some True ⇒ Check_Proved
| Some False ⇒ Check_Refuted
| None ⇒ Check_Unknown)"
lemma classify_check_proved:
assumes "classify_check c d = Check_Proved" and "s ∈ γ⇩S d"
shows "truthy (⟦c⟧⇩e s)"
using assms check_query_sound
unfolding classify_check_def
by (fastforce split: option.splits bool.splits)
lemma classify_check_refuted:
assumes "classify_check c d = Check_Refuted" and "s ∈ γ⇩S d"
shows "¬ truthy (⟦c⟧⇩e s)"
using assms check_query_sound
unfolding classify_check_def
by (fastforce split: option.splits bool.splits)
text ‹‹Check_Unknown› carries no semantic claim: no lemma concludes ‹truthy
(⟦c⟧⇩e s)› or its negation from it, by design.›
subsection ‹Node-indexed bridge to \<^const>‹checks_proven››
definition abstract_checks_proven :: "checks ⇒ (pp ⇒ 'd) ⇒ bool" where
"abstract_checks_proven ck env ⟷ (∀v c. (v, c) ∈ ck ⟶ check_query c (env v) = Some True)"
lemma abstract_checks_provenI [intro]:
"(⋀v c. (v, c) ∈ ck ⟹ check_query c (env v) = Some True) ⟹ abstract_checks_proven ck env"
unfolding abstract_checks_proven_def by blast
lemma abstract_checks_provenD [dest]:
"abstract_checks_proven ck env ⟹ (v, c) ∈ ck ⟹ check_query c (env v) = Some True"
unfolding abstract_checks_proven_def by blast
theorem abstract_checks_proven_sound:
assumes node_sound: "⋀v c. (v, c) ∈ ck ⟹ reach v ≤ γ⇩S (env v)"
and checked: "abstract_checks_proven ck env"
shows "checks_proven ck reach"
proof (rule checks_provenI)
fix v c s
assume ck': "(v, c) ∈ ck" and mem: "s ∈ reach v"
have proven: "check_query c (env v) = Some True"
using checked ck' by blast
have in_gamma: "s ∈ γ⇩S (env v)"
using node_sound[OF ck'] mem by blast
show "truthy (⟦c⟧⇩e s)"
using check_query_sound[OF in_gamma proven] by simp
qed
end
end