Theory Example_Relational_DG_Demo

theory Example_Relational_DG_Demo
  imports
    "Voblint_Analysis_Relational.Rel_Order_Domain"
    "Voblint_Analysis_Interval.Interval_Exec"
    "Voblint_VIMP.VIMP_Notation"
begin

unbundle default_st_syntax

section ‹End-to-end demo: a relational analysis on the same executable pipeline as Interval›

text ‹
  @{theory Voblint_Analysis_Relational.Rel_Order_Domain} interprets
  \<^locale>‹analysis_contract› over ‹relc›, a non-‹abs_state› relational carrier,
  with zero DG-framework changes -- the mathematical half of the claim.
  This file is the executable half: the same CFG, the same generic
  ‹compiled_routed_eqs_for› generator, and the same vendored solver that runs Interval
  also run ‹relc›, end to end, with a genuinely different observable result.

  ❙‹Program.› ‹if (x < y) { z = 1; } else { z = 0; }›, with ‹x›/‹y› left
  entirely unconstrained at entry (no prior assignment).  This is deliberately
  the case where Interval learns nothing from the guard: ‹x < y› narrows
  ‹x›'s interval only using ‹y›'s ∗‹current› upper bound, and vice versa;
  with both at ‹[-inf,+inf]›, the guard supplies no new bound for either
  variable.  ‹relc› instead records the pair ‹(x,y)› directly, because
  ‹assume_step› reads the guard's syntactic shape, not either variable's
  current abstract value.
›

subsection ‹The VIMP source program -- a full program block, not an inline stub›

definition demo_program :: imp_prog where
  "demo_program = program { 
   fun main() { 
     if (x < y) 
        { z = 1; } 
     else 
        { z = 0; }
     } 
}"

subsection ‹CFG construction›

text ‹No ‹global› declarations, so the classifier this program's own source gives
  is trivially false everywhere.›
abbreviation demo_gs :: "vname ⇒ bool" where
  "demo_gs ≡ declared_global demo_program"

lemma demo_program_declared_global_vars [simp]:
  "declared_global_vars demo_program = []"
  by (simp add: demo_program_def)

text ‹Local shorthand for the executable state's lookup projection, fixed at this
  file's own ‹demo_gs› classifier.›
abbreviation demo_lookup :: "('a::bot) default_st ⇒ vname ⇒ 'a" where
  "demo_lookup s x ≡ s⟨location_of demo_gs x⟩"

definition demo_pi :: proc_table where
  "demo_pi = prog_table demo_program"

definition demo_cfg :: cfg where
  "demo_cfg = compile_prog demo_pi (prog_procs demo_program)"

interpretation demo: compiled_cfg demo_pi "prog_procs demo_program" demo_cfg
  by (unfold_locales; unfold demo_cfg_def; simp add: compile_prog_finite)

text ‹‹Statement 1› is the true branch of the guard, right after the
  ‹assume› and before ‹z := 1› -- exactly where ‹x < y› is freshly known
  and nothing else has happened yet.  This is the read point both analyses
  are compared at.›

subsection ‹Interval, on the same CFG, same generator, same solver menu›

definition demo_ivl_eqs ::
  "pp × unit ⇒ (pp × unit, (unit, unit) global_unknown, (ivl default_st, ivl default_st) dg_state) strategy_tree"
    where
  "demo_ivl_eqs =
     compiled_routed_eqs_for (Analysis_Global ()) (λ_. Analysis_Global ()) Activation_Seed route_unit
       (ownership_split_dg_spec_st_for demo_gs (generic_tf_st_for ivl_ops demo_gs) (generic_enter_st_for ivl_ops demo_gs))
       demo_cfg (initial_default_st ivl_top ivl_top)
       (restrict_global_default_st (initial_default_st ivl_top ivl_top))"

definition demo_ivl_sol ::
  "(pp × unit) set × (pp × unit + (unit, unit) global_unknown ⇒ (ivl default_st, ivl default_st) dg_state)"
    where
  "demo_ivl_sol = TD_side_always_join_Interp_solve demo_ivl_eqs (cfg_exit demo_cfg, ())"

lemma demo_ivl_terminates:
  "TD_side_always_join_Interp_solve_c demo_ivl_eqs (cfg_exit demo_cfg, ()) ≠ None"
  by eval

subsection ‹The relational analysis, on the very same CFG, generator, and solver›

text ‹‹rel_order_spec› is already both the sound ∗‹and› the executable
  specification -- ‹relc› needed no ‹Default_St_Transfer›-style refinement layer,
  so ‹compiled_routed_eqs_for› is applied to it directly, with no bridging step and no
  parallel generator.›

definition demo_rel_eqs ::
  "pp × unit ⇒ (pp × unit, (unit, unit) global_unknown, (relc, relc) dg_state) strategy_tree" where
  "demo_rel_eqs = compiled_routed_eqs_for (Analysis_Global ()) (λ_. Analysis_Global ()) Activation_Seed route_unit
     rel_order_spec demo_cfg ⊤ ⊤"

definition demo_rel_sol ::
  "(pp × unit) set × (pp × unit + (unit, unit) global_unknown ⇒ (relc, relc) dg_state)" where
  "demo_rel_sol = TD_side_always_join_Interp_solve demo_rel_eqs (cfg_exit demo_cfg, ())"

lemma demo_rel_terminates:
  "TD_side_always_join_Interp_solve_c demo_rel_eqs (cfg_exit demo_cfg, ()) ≠ None"
  by eval

subsection ‹The comparison›

text ‹Interval's bound for ‹x› (and, symmetrically, ‹y›) at the true branch
  is unchanged from entry: the guard supplied no new information because
  neither operand had a finite bound for the other to narrow against.›

lemma demo_ivl_x_at_branch:
  "demo_lookup (dg_local (snd demo_ivl_sol (Inl (Statement 1, ())))) (STR ''x'') = Ivl MinInf PlusInf"
  unfolding demo_ivl_sol_def demo_ivl_eqs_def by eval

lemma demo_ivl_y_at_branch:
  "demo_lookup (dg_local (snd demo_ivl_sol (Inl (Statement 1, ())))) (STR ''y'') = Ivl MinInf PlusInf"
  unfolding demo_ivl_sol_def demo_ivl_eqs_def by eval

text ‹‹relc›, at the very same point, has recorded the pair directly.
  The false branch is precise too: ‹assume_not_step› reads ‹¬(x < y)› as
  ‹y ≤ x›, the mirror image of the true branch's transfer -- Interval's
  guard transfer stays uninformative on both branches for the same reason
  it was on the true one.  Each witness also excludes ‹RelBot› explicitly, so
  empty concretization cannot make the relation assertion hold vacuously.›

lemma demo_rel_learns_xy:
  "dg_local (snd demo_rel_sol (Inl (Statement 1, ()))) ≠ RelBot ∧
   relc_has (STR ''x'') (STR ''y'')
     (dg_local (snd demo_rel_sol (Inl (Statement 1, ()))))"
  unfolding demo_rel_sol_def demo_rel_eqs_def by eval

lemma demo_rel_learns_yx:
  "dg_local (snd demo_rel_sol (Inl (Statement 2, ()))) ≠ RelBot ∧
   relc_has (STR ''y'') (STR ''x'')
     (dg_local (snd demo_rel_sol (Inl (Statement 2, ()))))"
  unfolding demo_rel_sol_def demo_rel_eqs_def by eval

text ‹Side by side, the three lemmas above are the comparison: at ‹Statement 1›
  Interval's two bounds stay ‹[-inf,+inf]› while ‹relc› answers ‹True› for the
  pair ‹(x,y)›.›

lemma direct_relational_order_guards:
  "assume_step (Greater (V x) (V y)) (RelC {}) = RelC {(y, x)}"
  "assume_step (LessEq (V x) (V y)) (RelC {}) = RelC {(x, y)}"
  "assume_not_step (GreaterEq (V x) (V y)) (RelC {}) = RelC {(x, y)}"
  "assume_not_step (NotEq (V x) (V y)) (RelC {}) = RelC {(x, y), (y, x)}"
  by (simp_all add: assume_step_def assume_not_step_def)

unbundle no default_st_syntax

end