Theory Voblint_Examples_Interval.Example_Interval_DG_Ctx_Flagship

theory Example_Interval_DG_Ctx_Flagship
  imports
    Example_Interval_DG_IP_Flagship
begin

unbundle default_st_syntax

section ‹Context-sensitive interval analysis of ‹twice› (executable)›

text ‹
  The production entry-state analysis
  (\<^theory>‹Voblint_Analysis_Interval.Interval_Analyses›) run on
  \<^const>‹twice_program›.  Each call to ‹twice› receives the abstract entry state
  of formal ‹p› as its context:

  ▪ ‹twice(3)› uses context ‹[3,3]› and computes ‹#ret = [6,6]› and ‹x = [6,6]›;
  ▪ ‹twice(10)› uses context ‹[10,10]› and computes ‹#ret = [20,20]› and ‹y = [20,20]›.

  The two repeated calls stay separate, whereas the monovariant baseline of
  \<^theory>‹Voblint_Examples_Interval.Example_Interval_DG_IP_Flagship› forces one shared entry
  state and reports ‹p = [3,10]›, ‹#ret = [6,20]›, and ‹x = y = [6,20]›.  This
  entry-value key is finite for the two constant call sites.  A general interval
  analysis needs a finite canonical context representation because arbitrary interval
  states may grow under recursion and widening.

  Nothing solver-shaped is owned here: the equation system, its routing hook, the
  solver-global key type \<^type>‹global_unknown›, and the solved projection all come from the
  production analysis.  The local unknown carries the whole abstract state on the
  lifted carrier \<^typ>‹ivl default_st lifted›, so a global is read where a local is
  and there is no separate solver-global slot holding program state.
›

subsection ‹The executable bottom predicate›

text ‹The equation system reads the program's own declared globals for its bottom
  test. At a concrete program it is \<^const>‹default_st_is_bot_for› on those
  globals, which is exact for \<^const>‹is_empty_state›.›

definition twice_empty_pred :: "ivl default_st ⇒ bool" where
  "twice_empty_pred = default_st_is_bot_for (declared_global_vars twice_program)"

lemma twice_exact: "twice_empty_pred s = is_empty_state (ρ⇘twice_gs⇙ s)"
  unfolding twice_empty_pred_def by (rule default_st_is_bot_for_iff) simp

text ‹Reading one variable off a lifted whole-state local unknown: an unreachable
  point (\<^const>‹Bot›) reads ‹bot› at every variable.›
abbreviation twice_ctx_lookup :: "ivl default_st lifted ⇒ vname ⇒ ivl" where
  "twice_ctx_lookup d x ≡
     (case d of Bot ⇒ bot | Lifted d0 ⇒ d0⟨location_of twice_gs x⟩)"

subsection ‹The routed equation system and its solution›

text ‹Every value below is Interval's entry-state registration ‹interval_es_rule› at
  \<^const>‹Globals_Warrow›. The main context is ‹[]› (‹main› is the root
  activation, no formal binds it).›

definition twice_ctx_sol ::
  "(pp × ivl list) set
     × (pp × ivl list + (unit, ivl list) global_unknown ⇒ (ivl default_st lifted, ivl default_st lifted) dg_state)" where
  "twice_ctx_sol = interval_es_rule.solution Globals_Warrow twice_gs twice_program"

lemma twice_ctx_terminates_c:
  "TD_side_rule_Interp_solve_c Globals_Warrow
     (interval_es_rule.equations twice_gs twice_program)
     (interval_es_rule.root_query twice_program) ≠ None"
  unfolding interval_es_rule.root_query_def by eval

lemma twice_ctx_terminates:
  "interval_es_rule.terminates Globals_Warrow twice_gs twice_program"
  by (rule interval_es_rule.terminates_of_solve_c[OF twice_ctx_terminates_c])

subsection ‹The two calling contexts are distinct›

text ‹The routed callee context is \<^const>‹dg_pipeline.ctx_succ›, whose type
  omits the domain, so evaluation inlines its body rather than looking for a code
  equation of its own.›


definition ctx_call1 :: "ivl list" where
  "ctx_call1 = interval_es_rule.ctx_succ Globals_Warrow twice_gs twice_program
                 (Statement 2) [] (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3])
                 (STR ''twice'')"

definition ctx_call2 :: "ivl list" where
  "ctx_call2 = interval_es_rule.ctx_succ Globals_Warrow twice_gs twice_program
                 (Statement 3) [] (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10])
                 (STR ''twice'')"

lemma ctx_call1_val: "ctx_call1 = [Ivl (Fin 3) (Fin 3)]"
  unfolding ctx_call1_def twice_ctx_sol_def twice_empty_pred_def by eval

lemma ctx_call2_val: "ctx_call2 = [Ivl (Fin 10) (Fin 10)]"
  unfolding ctx_call2_def twice_ctx_sol_def twice_empty_pred_def by eval

lemma contexts_distinct: "ctx_call1 ≠ ctx_call2"
  by (simp add: ctx_call1_val ctx_call2_val)

subsection ‹Per-context exact results›

text ‹Callee entry parameter, per context --- against the monovariant ‹p = [3,10]›.›
lemma call1_p_at_entry:
  "twice_ctx_lookup (dg_local (snd twice_ctx_sol (Inl (FunctionEntry (STR ''twice''), ctx_call1)))) (STR ''p'')
     = Ivl (Fin 3) (Fin 3)"
  unfolding twice_ctx_sol_def twice_empty_pred_def ctx_call1_def by eval

lemma call2_p_at_entry:
  "twice_ctx_lookup (dg_local (snd twice_ctx_sol (Inl (FunctionEntry (STR ''twice''), ctx_call2)))) (STR ''p'')
     = Ivl (Fin 10) (Fin 10)"
  unfolding twice_ctx_sol_def twice_empty_pred_def ctx_call2_def by eval

text ‹Callee result return channel, per context --- ∗‹not› merged into the monovariant
  ‹#ret = [6,20]›.›
lemma call1_ret_at_exit:
  "twice_ctx_lookup (dg_local (snd twice_ctx_sol (Inl (FunctionResult (STR ''twice''), ctx_call1)))) (STR ''#ret'')
     = Ivl (Fin 6) (Fin 6)"
  unfolding twice_ctx_sol_def twice_empty_pred_def ctx_call1_def by eval

lemma call2_ret_at_exit:
  "twice_ctx_lookup (dg_local (snd twice_ctx_sol (Inl (FunctionResult (STR ''twice''), ctx_call2)))) (STR ''#ret'')
     = Ivl (Fin 20) (Fin 20)"
  unfolding twice_ctx_sol_def twice_empty_pred_def ctx_call2_def by eval

text ‹Caller destinations after each return, where the monovariant baseline reports
  ‹x = y = [6,20]›.›
lemma x_computed:
  "twice_ctx_lookup (dg_local (snd twice_ctx_sol (Inl (Statement 3, [])))) (STR ''x'') = Ivl (Fin 6) (Fin 6)"
  unfolding twice_ctx_sol_def twice_empty_pred_def by eval

lemma y_computed:
  "twice_ctx_lookup (dg_local (snd twice_ctx_sol (Inl (Statement 4, [])))) (STR ''y'') = Ivl (Fin 20) (Fin 20)"
  unfolding twice_ctx_sol_def twice_empty_pred_def by eval

subsection ‹Seed slots and coverage›

text ‹Each call publishes the entered store into its own context's seed slot.  The
  heterogeneous seed channel (\<^const>‹routed_call_program› / \<^const>‹routed_entry_seed_programs›)
  carries that store in the seed unknown's \<^const>‹dg_local› half, the same carrier the
  callee entry reads it back on.›
lemma seed_call1:
  "twice_ctx_lookup
     (dg_local (snd twice_ctx_sol
       (Inr (Activation_Seed (FunctionEntry (STR ''twice'')) ctx_call1))))
     (STR ''p'')
     = Ivl (Fin 3) (Fin 3)"
  unfolding twice_ctx_sol_def twice_empty_pred_def ctx_call1_def by eval

lemma seed_call2:
  "twice_ctx_lookup
     (dg_local (snd twice_ctx_sol
       (Inr (Activation_Seed (FunctionEntry (STR ''twice'')) ctx_call2))))
     (STR ''p'')
     = Ivl (Fin 10) (Fin 10)"
  unfolding twice_ctx_sol_def twice_empty_pred_def ctx_call2_def by eval

text ‹The callee entry is materialized once per routed context and never under the
  main context: the two calls are analyzed separately.›
lemma callee_covered_call1: "(FunctionEntry (STR ''twice''), ctx_call1) ∈ fst twice_ctx_sol"
  unfolding twice_ctx_sol_def twice_empty_pred_def ctx_call1_def by eval

lemma callee_covered_call2: "(FunctionEntry (STR ''twice''), ctx_call2) ∈ fst twice_ctx_sol"
  unfolding twice_ctx_sol_def twice_empty_pred_def ctx_call2_def by eval

lemma callee_not_under_main: "(FunctionEntry (STR ''twice''), []) ∉ fst twice_ctx_sol"
  unfolding twice_ctx_sol_def twice_empty_pred_def by eval

unbundle no default_st_syntax

end