Theory Congruence_Transfer
theory Congruence_Transfer
imports
Congruence_Backward
Congruence_Special
"Voblint_Nonrelational.Nonrelational_Transfer"
begin
section ‹What each kind of edge does to a map from variables to residue classes›
text ‹
One operation per edge the framework can hand a domain: an assignment writes the
evaluated right-hand side, a guard runs the backward branch, a call binds the
actuals into a fresh frame, a return publishes its expression into the return
variable, and skip, body entry and check observation leave the map alone. None
of that is about modular arithmetic, so none of it is stated here: it is
\<^locale>‹sound_nonrelational_ops›, proved sound and monotone once for every
domain that gives one abstract value per variable.
What is Congruence's own are the primitive choices. ‹congruence_ops› collects
the evaluator, the comparison tables, \<^const>‹congruence_refine_ops› --- whose
inverses make ‹x + 1 == 3› narrow ‹x› to a single integer --- the special calls,
and \<^const>‹top›. The one interpretation below derives the guard filters, the
branch, the check classifier and the transfer from that bundle, and rewrites the
locale's special-call dispatch to \<^const>‹special_congruence›, Congruence's own
‹fun›, rather than introducing a second name for it.
›
lemma congruence_check_domain:
"sound_check_query congruence_lt congruence_eqb gamma_state aval_congruence"
by unfold_locales (rule congruence_arith.aval_abs_sound)
definition congruence_ops :: "congruence nonrelational_ops" where
"congruence_ops =
⦇ n_aval = aval_congruence, n_query = ⦇q_less = congruence_lt, q_eq = congruence_eqb⦈,
n_refine = congruence_refine_ops, n_special = congruence_special_ops ⦈"
lemma congruence_ops_simps [simp]:
"n_aval congruence_ops = aval_congruence"
"q_less (n_query congruence_ops) = congruence_lt"
"q_eq (n_query congruence_ops) = congruence_eqb"
"n_refine congruence_ops = congruence_refine_ops"
"n_special congruence_ops = congruence_special_ops"
by (simp_all add: congruence_ops_def)