Theory Exec_Sign_DG_Run

theory Exec_Sign_DG_Run
  imports
    "Voblint_Analysis_Sign.Sign_Analyses"
    "Voblint_VIMP.VIMP_Notation"
    "Voblint_Examples_CFG.Example_Compile_Call_Free"
begin

section ‹Running the verified solver on the native D/G spine (Sign)›

text ‹
  A concrete call-free Sign program is compiled to a CFG, its equation system is handed to
  the vendored TD-side solver under the always-join global update rule, and what the solver
  computes is turned into a guarantee about every source run of that program: whatever
  store a run reaches, the analysis result at the matching node describes it.

  Nothing here is registered locally. The equation system, the solve and every soundness
  endpoint are Sign's unit-context registration ‹sign_rule›, at
  \<^const>‹Globals_Join›. This file supplies only the program, one ▩‹by eval›
  termination fact and one coverage fact.

  The final theorem ‹dgEx_source_run_sound› turns that single solver success into the
  source-level guarantee, and it rests on the ∗‹computed› table, not on a hand-written
  candidate solution.
›

subsection ‹The concrete program and its compiled CFG›

text ‹
  A minimal call-free program ▩‹x := 1; y := x› inside ‹main›: the body occupies
  ‹Statement 0›--‹Statement 2› between ‹FunctionEntry (STR ''main'')› and
  ‹FunctionResult (STR ''main'')›, and ‹calls› is empty.
›

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

text ‹The storage classifier: ‹sign_ex_prog› declares no globals, so ‹sign_ex_gs›
  classifies every variable this chain touches as local.›
abbreviation sign_ex_gs :: "vname ⇒ bool" where
  "sign_ex_gs ≡ declared_global sign_ex_prog"

definition sign_ex_pi :: proc_table where
  "sign_ex_pi = prog_table sign_ex_prog"

definition gEx :: cfg where
  "gEx = compile_prog sign_ex_pi (prog_procs sign_ex_prog)"

lemma gEx_prog_cfg: "gEx = prog_cfg sign_ex_prog"
  by (simp add: gEx_def sign_ex_pi_def prog_cfg_def)

lemma gEx_calls: "calls gEx = {}"
  unfolding gEx_def sign_ex_pi_def
  by (rule compile_prog_calls_empty)
     (simp_all add: sign_ex_prog_def main_body_def prog_main_name_def)
interpretation gEx: compiled_cfg sign_ex_pi "prog_procs sign_ex_prog" gEx
  by (unfold_locales; unfold gEx_def; simp add: compile_prog_finite)

subsection ‹The equation system and its solve›

text ‹‹dgEx_eqs› is the registered equation system at this program. The executable
  option-valued solver terminates on it --- a code-generated ▩‹by eval› fact --- which
  is the solver-domain predicate the registration's endpoints take.›

definition dgEx_eqs ::
  "pp × unit
   ⇒ (pp × unit, (unit, unit) global_unknown,
        (sign default_st lifted, sign default_st lifted) dg_state) strategy_tree" where
  "dgEx_eqs = sign_rule.equations sign_ex_gs sign_ex_prog"

lemma dgEx_terminates_c:
  "TD_side_rule_Interp_solve_c Globals_Join dgEx_eqs (cfg_exit gEx, ()) ≠ None"
  by eval

lemma dgEx_terminates: "sign_rule.terminates Globals_Join sign_ex_gs sign_ex_prog"
  unfolding sign_rule.terminates_code
  using TD_side_rule_Interp.solve_dom_of_solve_c[OF dgEx_terminates_c]
  by (simp add: dgEx_eqs_def gEx_prog_cfg)

subsection ‹Well-formedness of the compiled input›

text ‹
  ‹dgEx_wf›: the compiled example meets ‹wf_compile_input›, the premise the
  source-level soundness theorem below needs.
›

lemma dgEx_wf:
  "wf_compile_input sign_ex_gs sign_ex_pi (prog_procs sign_ex_prog)"
  unfolding wf_compile_input_def
  by (auto simp: wf_compile_input_simps sign_ex_pi_def sign_ex_prog_def split: if_splits)

subsection ‹Collecting-semantics over-approximation from the computed result›

text ‹The unit route names the one context ‹()› at every call, so the routed
  endpoint for a route that is a function of the call site applies, and the state
  published at ‹()› bounds every run.›

theorem dgEx_source_run_sound:
  assumes run: "sign_ex_gs, sign_ex_pi ⊢ (prog_main sign_ex_prog, s, [])
                     →⇩p⇧* (residual, t, frs)"
      and init: "s ∈ cinit_stores sign_ex_gs"
  shows "∃v stk. sign_ex_pi, gEx, prog_main_name ⊢ (residual, t, frs) ≈ (v, t, stk)
                 ∧ t ∈ γ (sign_rule.state_at Globals_Join sign_ex_gs sign_ex_prog () v)"
proof -
  have run':
    "sign_ex_gs, prog_table sign_ex_prog ⊢ (main_body (prog_table sign_ex_prog), s, []) →⇩p⇧* (residual, t, frs)"
    using run by (simp add: sign_ex_pi_def)
  have wf: "wf_compile_input sign_ex_gs (prog_table sign_ex_prog) (prog_procs sign_ex_prog)"
    using dgEx_wf by (simp add: sign_ex_pi_def)
  have unit_route: "⋀u ctx d ca s. route_unit u ctx d ca = enterc_unit u ctx s" by simp
  show ?thesis
    using sign_rule.fun_route_source_sound[OF unit_route wf dgEx_terminates init run']
    by (simp add: gEx_prog_cfg sign_ex_pi_def)
qed

subsection ‹Inspecting the computed result›

text ‹The unit registration routes the whole abstract state through the local unknown,
  reachability-lifted: the local answer at the exit is exactly ‹Lifted› of a state
  mapping ‹x› to ‹SPos›, with no separate global/side slot to inspect for a purely
  local name. Nothing further consumes this equation --- it is the readable form of what
  the solver computed, beside the theorem above that quantifies over every run.›

lemma dgEx_inspect:
  "map_option (λsol. case ρ⇘sign_ex_gs⇙
                            (dg_local (snd sol (Inl (Statement 2, ()))))
                      of Lifted s ⇒ Some (s (STR ''x'')) | Bot ⇒ None)
     (TD_side_rule_Interp_solve_c Globals_Join dgEx_eqs (cfg_exit gEx, ())) = Some (Some SPos)"
  by eval

end