Theory Exec_Int_DG_Run

theory Exec_Int_DG_Run
  imports
    "Voblint_Analysis_Int.Int_Exec"
    "Voblint_VIMP.VIMP_Notation"
begin

section ‹The composite domain carried through a real solver run›

text ‹
  Everything else in this folder calls a composite operation directly. Here the
  guard ‹y + 1 = 3› arrives the way it does in production: compiled from VIMP
  source into a CFG, turned into a D/G equation system, and handed to the
  vendored TD solver. The two runs cover the modes the CLI cannot select:
  ‹Refine_Never› and ‹Refine_Once›. The production CLI fixes
  ‹Refine_Fixpoint›, whose result is covered by its CLI regression.
  Each lemma below projects its node result directly from ‹solve_c›, so
  termination and the observed value require one solver evaluation together.
  Vocabulary: an ‹eqs› constant is the equation system one mode generates,
  ‹int_ex_read› projects one variable's abstract value out of a node's local
  unknown, and ‹Statement 1› names the point after the true-branch guard.
›

definition int_ex_prog :: imp_prog where
  "int_ex_prog = program { fun main() { if (y + 1 == 3) { x = 1; } else { x = 0; } } }"

abbreviation int_ex_gs :: "vname => bool" where
  "int_ex_gs == declared_global int_ex_prog"

definition int_ex_pi :: proc_table where
  "int_ex_pi = prog_table int_ex_prog"

definition gExI :: cfg where
  "gExI = compile_prog int_ex_pi (prog_procs int_ex_prog)"

text ‹
  The Base construction routes the whole abstract state through the local
  unknown, reachability-lifted: ‹int_ex_read› reads a computed ‹default_st
  lifted› value back through \<^const>‹default_st_to_fun›, matching
  ‹parity_lookup›'s role in Parity's own DG flagship -- a genuinely
  unreachable local unknown (‹Bot›) reads back as ‹top›, never spuriously
  observed here since every inspected node below is reachable.
›

abbreviation int_ex_read :: "int_dom default_st lifted => vname => int_dom" where
  "int_ex_read d x ==
     (case ρ⇘int_ex_gs⇙ d of
        Lifted f => f x | Bot => top)"

abbreviation int_ex_result where
  "int_ex_result eqs ==
     map_option
       (λ(_, sol). int_ex_read (dg_local (sol (Inl (Statement 1, ())))) (STR ''y''))
       (TD_side_always_join_Interp_solve_c eqs (cfg_exit gExI, ()))"

subsection ‹Computed post-solutions for the non-CLI modes›

text ‹
  ‹y + 1 = 3› is a composite guard, reached through a real compiled ‹if› and
  the vendored solver. ‹Statement 1› is the interior node right after
  the true branch's guard and before the branches rejoin at ‹Statement 3›
  (a join would erase the refinement, since the false branch never
  constrains ‹y›), so that is where ‹y›'s mode-dependent precision is
  observable in the solver's own computed result.

  Each mode is registered on the generic Base construction
  \<^const>‹exec_dg_spec› (\<^theory>‹Voblint_Exec.DG_Local_State_Exec›),
  matching Sign's own production route: the local unknown carries the whole
  reachability-lifted ‹int_dom default_st›, with no separate local/global
  split for ‹int_ex_prog›'s (empty) set of declared globals to route through.
›

definition dgExI_never_eqs ::
    "pp * unit => (pp * unit, (unit, unit) global_unknown,
       (int_dom default_st lifted, int_dom default_st lifted) dg_state) strategy_tree"
where
  "dgExI_never_eqs = compiled_routed_eqs_for (Analysis_Global ()) (λ_. Analysis_Global ()) Activation_Seed route_unit
     (exec_dg_spec int_ex_gs
       (default_st_is_bot_for (declared_global_vars int_ex_prog))
       (generic_tf_st_for (int_dom_ops Refine_Never) int_ex_gs) (generic_enter_st_for (int_dom_ops Refine_Never) int_ex_gs))
     gExI (Lifted cinit_int_dom_st) (Lifted cinit_int_dom_st)"

lemma dgExI_never_result:
  "int_ex_result dgExI_never_eqs =
   Some (int_dom_sipc STop top PEven (congruence_of_int 2))"
  by eval

definition dgExI_once_eqs ::
    "pp * unit => (pp * unit, (unit, unit) global_unknown,
       (int_dom default_st lifted, int_dom default_st lifted) dg_state) strategy_tree"
where
  "dgExI_once_eqs = compiled_routed_eqs_for (Analysis_Global ()) (λ_. Analysis_Global ()) Activation_Seed route_unit
     (exec_dg_spec int_ex_gs
       (default_st_is_bot_for (declared_global_vars int_ex_prog))
       (generic_tf_st_for (int_dom_ops Refine_Once) int_ex_gs) (generic_enter_st_for (int_dom_ops Refine_Once) int_ex_gs))
     gExI (Lifted cinit_int_dom_st) (Lifted cinit_int_dom_st)"

lemma dgExI_once_result:
  "int_ex_result dgExI_once_eqs =
   Some (int_dom_sipc SPos (Ivl (Fin 2) (Fin 2)) PEven (congruence_of_int 2))"
  by eval

text ‹
  The retained mode contrast comes from two real solver runs on the same
  compiled program. ‹Refine_Never› narrows only the Parity and Congruence
  components, through their own inverses of ‹+›. ‹Refine_Once› propagates
  that information to Sign and Interval and reaches the exact singleton.
›

corollary dgExI_never_ne_once:
  "int_ex_result dgExI_never_eqs ≠ int_ex_result dgExI_once_eqs"
  apply (simp only: dgExI_never_result dgExI_once_result option.inject)
  apply (rule notI)
  apply (drule arg_cong[where f = int_sign])
  by (simp add: int_dom_sipc_def)


end