Theory Voblint_Examples_Congruence.Example_Congruence_DG_Run

theory Example_Congruence_DG_Run
  imports
    "Voblint_Analysis_Congruence.Congruence_Analyses"
    "Voblint_VIMP.VIMP_Notation"
begin

section ‹End-to-end Congruence analysis on the D/G pipeline›

text ‹
  This straight-line program keeps the witness small while exercising the full
  route: VIMP compilation, D/G equation generation, the verified solver, and
  the published Congruence result table of the unit-context registration
  ‹congruence_rule› at \<^const>‹Globals_Join›.  Reading both variables through one
  option distinguishes a live exit from ‹Bot› and pins informative values.
›

definition congruence_dg_program :: imp_prog where
  "congruence_dg_program = program {
     fun main() {
       x = 1;
       y = x + 2;
     }
   }"

abbreviation congruence_dg_gs :: "vname ⇒ bool" where
  "congruence_dg_gs ≡ declared_global congruence_dg_program"

definition congruence_dg_exit_xy :: "(congruence × congruence) option" where
  "congruence_dg_exit_xy =
     (case lookup_table
         (congruence_rule.result Globals_Join congruence_dg_gs congruence_dg_program)
         (cfg_exit (prog_cfg congruence_dg_program)) () of
        Bot ⇒ None
      | Lifted st ⇒ Some (st (STR ''x''), st (STR ''y'')))"

lemma congruence_dg_terminates:
  "congruence_rule.terminates Globals_Join congruence_dg_gs congruence_dg_program"
  unfolding congruence_rule.terminates_code
  by (rule TD_side_rule_Interp.solve_dom_of_solve_c;
      unfold congruence_dg_program_def; eval)

lemma congruence_dg_exit_informative:
  "congruence_dg_exit_xy =
     Some (congruence_of_int 1, congruence_of_int 3)"
  unfolding congruence_dg_exit_xy_def congruence_dg_program_def
  by eval

end