Theory Voblint_Examples_Sign.Example_Sign_DG_CallString_K2

theory Example_Sign_DG_CallString_K2
  imports
    Example_Sign_DG_CallString_K1
begin

section ‹A computed 2-call-string context, routed by truncated call history›

text ‹
  The ‹k = 2› sibling of \<^theory>‹Voblint_Examples_Sign.Example_Sign_DG_CallString_K1›, same
  ‹sign_nest› program and same Base-style storage: ‹g›'s single call site is reached from
  two different ‹f› activations. At ‹k = 1› both collapse into one merged context and
  ‹g›'s entry parameter joins to ‹STop›; at ‹k = 2› the call string also records which
  ‹f› call led there, so the two activations stay separate and ‹g›'s entry parameter is
  ‹SPos› in one context, ‹SNeg› in the other. Only the bound changes --- the
  specification, the transport, and the routed locale are the ones ‹k = 1› already fixed.
›

subsection ‹The routed equation system and its computed solution›

text ‹Reuses \<^type>‹call_string_gk› from \<^theory>‹Voblint_Framework.Call_String_Context› rather
  than minting its own global-key type: the key shape never depended on ‹k›, only the
  ‹Seed› payload's context length did.›

definition sign_nest_2_eqs ::
  "(pp × cfg_node list, call_string_gk,
     (sign default_st lifted, sign default_st lifted) dg_state) eqsT" where
  "sign_nest_2_eqs =
     routed_node_rhs intra_predecessor_addr_list call_site_list (λ_. Global) (cs_route 2)
       (λctx' src a. dg_spec_edge_program sign_nest_S_st a src (λ_. Global))
       (routed_call_program sign_nest_S_st (λ_. Global) Seed (static_resolve sign_nest_cfg)
          (λd. d = Bot))
       (routed_entry_seed_programs Seed)
       sign_nest_cfg Bot (Lifted cinit_sign_st) Bot"

definition sign_nest_2_sol ::
  "(pp × cfg_node list) set
     × (pp × cfg_node list + call_string_gk
          ⇒ (sign default_st lifted, sign default_st lifted) dg_state)" where
  "sign_nest_2_sol = TD_side_always_join_Interp_solve sign_nest_2_eqs
                       (cfg_exit sign_nest_cfg, [])"

lemma sign_nest_2_terminates:
  "TD_side_always_join_Interp_solve_c sign_nest_2_eqs (cfg_exit sign_nest_cfg, []) ≠ None"
  by eval

subsection ‹Coverage›

text ‹The full solved node set, computed once; every membership fact below is a
  ‹simp› lookup into this literal set instead of a separate ‹eval› re-derivation.›

definition sign_nest_2_nodes :: "(pp × cfg_node list) set" where
  "sign_nest_2_nodes = {
     (FunctionEntry (STR ''main''), []), (Statement 5, []), (Statement 6, []), (Statement 7, []),
     (FunctionEntry (STR ''f''), [Statement 5]), (Statement 2, [Statement 5]),
     (Statement 3, [Statement 5]), (FunctionResult (STR ''f''), [Statement 5]),
     (FunctionEntry (STR ''f''), [Statement 6]), (Statement 2, [Statement 6]),
     (Statement 3, [Statement 6]), (FunctionResult (STR ''f''), [Statement 6]),
     (FunctionEntry (STR ''g''), [Statement 2, Statement 5]), (Statement 0, [Statement 2, Statement 5]),
     (FunctionResult (STR ''g''), [Statement 2, Statement 5]),
     (FunctionEntry (STR ''g''), [Statement 2, Statement 6]), (Statement 0, [Statement 2, Statement 6]),
     (FunctionResult (STR ''g''), [Statement 2, Statement 6]),
     (Statement 4, [Statement 5]), (Statement 4, [Statement 6]),
     (Statement 1, [Statement 2, Statement 5]), (Statement 1, [Statement 2, Statement 6]),
     (FunctionResult (STR ''main''), [])}"

lemma sign_nest_2_nodes_eq: "fst sign_nest_2_sol = sign_nest_2_nodes"
  unfolding sign_nest_2_sol_def sign_nest_2_eqs_def sign_nest_2_nodes_def by eval

lemma entry_covered_2: "(cfg_entry sign_nest_cfg, []) ∈ fst sign_nest_2_sol"
  unfolding sign_nest_entry sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp

lemma sign_nest_fwd_closed_all_2:
  "∀(u, c)∈fst sign_nest_2_sol. ∀(u', a, v)∈intra sign_nest_cfg.
      u = u' ⟶ (v, c) ∈ fst sign_nest_2_sol"
  unfolding sign_nest_2_sol_def sign_nest_2_eqs_def by eval

lemma sign_nest_fwd_closed_2:
  assumes "(u, ctx) ∈ fst sign_nest_2_sol" and "(u, a, v) ∈ intra sign_nest_cfg"
  shows "(v, ctx) ∈ fst sign_nest_2_sol"
  using sign_nest_fwd_closed_all_2 assms by fastforce

text ‹Unlike ‹k = 1›, ‹g›'s call site is now covered at two ∗‹distinct› two-element
  contexts, one per ‹f› activation that reaches it.›

lemma enter_callers_only_root_main_2:
  "∀(p, ctx)∈fst sign_nest_2_sol.
     (p = Statement 5 ∨ p = Statement 6) ⟶ ctx = []"
  unfolding sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp

lemma enter_callers_g_2:
  "∀(p, ctx)∈fst sign_nest_2_sol.
     p = Statement 2 ⟶ ctx = [Statement 5] ∨ ctx = [Statement 6]"
  unfolding sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp

lemma callee_covered_fpos_2: "(FunctionEntry (STR ''f''), [Statement 5]) ∈ fst sign_nest_2_sol"
  unfolding sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp
lemma callee_covered_fneg_2: "(FunctionEntry (STR ''f''), [Statement 6]) ∈ fst sign_nest_2_sol"
  unfolding sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp
lemma callee_covered_g_fpos_2:
  "(FunctionEntry (STR ''g''), [Statement 2, Statement 5]) ∈ fst sign_nest_2_sol"
  unfolding sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp
lemma callee_covered_g_fneg_2:
  "(FunctionEntry (STR ''g''), [Statement 2, Statement 6]) ∈ fst sign_nest_2_sol"
  unfolding sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp

lemma covered_ret6_2: "(Statement 6, []) ∈ fst sign_nest_2_sol"
  unfolding sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp
lemma covered_ret7_2: "(Statement 7, []) ∈ fst sign_nest_2_sol"
  unfolding sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp
lemma covered_ret3_fpos_2: "(Statement 3, [Statement 5]) ∈ fst sign_nest_2_sol"
  unfolding sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp
lemma covered_ret3_fneg_2: "(Statement 3, [Statement 6]) ∈ fst sign_nest_2_sol"
  unfolding sign_nest_2_nodes_eq sign_nest_2_nodes_def by simp


section ‹The solver's post-solution›

text ‹
  As at ‹k = 1›: termination of ‹sign_nest_2_eqs› gives a solve domain, and the
  solver's ‹partial_post_solution› gives ‹sign_nest_2_pp_st›.
›

lemma sign_nest_2_solve_dom:
  "TD_side_always_join_Interp.solve_dom TYPE(call_string_gk)
     TYPE((sign default_st lifted, sign default_st lifted) dg_state)
     sign_nest_2_eqs (cfg_exit sign_nest_cfg, [])"
  by (rule TD_side_always_join_Interp.solve_dom_of_solve_c[OF sign_nest_2_terminates])

lemma sign_nest_2_pp_st:
  "part_post_solution sign_nest_2_eqs (cfg_exit sign_nest_cfg, [])
     (snd sign_nest_2_sol) (fst sign_nest_2_sol)"
  using TD_side_always_join_Interp.partial_post_solution
          [OF sign_nest_2_solve_dom, of "fst sign_nest_2_sol" "snd sign_nest_2_sol"]
  unfolding sign_nest_2_sol_def by simp

abbreviation sigma_2 ::
  "pp × cfg_node list + call_string_gk
     ⇒ (sign default_st lifted, sign default_st lifted) dg_state" where
  "sigma_2 ≡ snd sign_nest_2_sol"

section ‹Activation-indexed collecting soundness for the 2-call-string-routed solution›

text ‹
  ‹sign_ctx_sg_2› reads the solved local state at each key; the interpretation
  ‹sign_nest_2_cs› instantiates ‹call_string_routed_context› at ‹k = 2›.
›

abbreviation sign_ctx_sg_2 ::
  "pp × cfg_node list + call_string_gk ⇒ sign default_st lifted" where
  "sign_ctx_sg_2 ≡ solved_local_reader (fst sign_nest_2_sol) sigma_2"

text ‹Unlike ‹k = 1›, ‹call_fwd›'s ‹Statement 2› case now genuinely splits: ‹g›'s call site
  is covered at two distinct one-element contexts, and ‹take 2› keeps them apart after
  routing, so each needs its own coverage witness. Everything else the routed locale asks
  for is discharged generically at \<^const>‹cs_route›, exactly as at ‹k = 1›.›

interpretation sign_nest_2_cs: call_string_routed_context
    sign_nest_S_st sign_nest_gamma sign_nest_gs sign_nest_pi sign_nest_procs 2
    Bot "Lifted cinit_sign_st" Bot
    sigma_2 "fst sign_nest_2_sol" "(cfg_exit sign_nest_cfg, [])" sign_ctx_sg_2
    "λd. d = Bot"
    "gamma_lift (default_st_gamma sign_nest_gs)"
proof (unfold_locales, unfold sign_nest_cfg_compile,
       goal_cases CmbWf ExtraWf FinE PP SgCov SgUncov Fwd IsBotBot IsBotSound
       EnterComplete CallFwd CombFwd)
  case CmbWf
  show ?case by (rule sp_wf_routed_call_program) (simp add: sign_nest_S_st_def)
next
  case ExtraWf
  then show ?case by (rule sp_wf_routed_entry_seed_programs)
next
  case FinE
  show ?case by (rule sign_nest.finite_intra)
next
  case PP
  show ?case
    by (rule post_bounded_of_part_post_solution
          [OF sign_nest_2_pp_st[unfolded sign_nest_2_eqs_def]])
next
  case (SgCov v c)
  show ?case using SgCov by (simp add: sign_nest_gamma_def)
next
  case (SgUncov v c)
  show ?case using SgUncov by simp
next
  case (Fwd u a v c)
  show ?case using Fwd(1,3) by (rule sign_nest_fwd_closed_2)
next
  case IsBotBot show ?case by simp
next
  case (IsBotSound d gv) then show ?case by (simp add: sign_nest_gamma_eq)
next
  case (EnterComplete u ctx dst pars args p cont s)
  let ?ci = "call_info_of (CallEdge dst pars args) p"
  let ?caller = "dg_local (sigma_2 (Inl (u, ctx)))"
  have cov: "entry_pairs_cover (λd. sign_nest_gamma d (dg_global (sigma_2 (Inr Global)))) s
      (call_enter sign_nest_gs (CallEdge dst pars args) s)
      [(?caller, transfer_lift sign_nest_empty_pred (generic_enter_st_for sign_ops sign_nest_gs ?ci)
                   ?caller)]"
    using sign_nest_domain.entry_pairs_cover_st
            [OF sign_tf.is_sound_nonrelational_transfer, where ci = ?ci and d = ?caller]
      EnterComplete(3)
    by (simp add: sign_nest_gamma_eq sign_nest_domain.gamma_exec_def)
  show ?case
    unfolding sign_nest_S_st_def dgs_enter_exec_dg_spec
    using enter_runs_local_enter_transfer enter_deps_local_enter_transfer cov by fastforce
next
  case (CallFwd u ctx dst pars args p cont)
  note covU = CallFwd(1) and ce = CallFwd(2)
  from ce sign_nest_calls_shape have
    "(u = Statement 2 ∧ p = (STR ''g'') ∧ cont = Statement 3) ∨
     (u = Statement 5 ∧ p = (STR ''f'') ∧ cont = Statement 6) ∨
     (u = Statement 6 ∧ p = (STR ''f'') ∧ cont = Statement 7)"
    by fastforce
  then consider
      (c1) "u = Statement 2" "p = (STR ''g'')"
    | (c2) "u = Statement 5" "p = (STR ''f'')"
    | (c3) "u = Statement 6" "p = (STR ''f'')"
    by blast
  thus ?case
  proof cases
    case c1
    from covU c1 enter_callers_g_2 have "ctx = [Statement 5] ∨ ctx = [Statement 6]" by fastforce
    thus ?thesis
    proof
      assume "ctx = [Statement 5]"
      thus ?thesis using c1 callee_covered_g_fpos_2 by (simp add: cs_route_def)
    next
      assume "ctx = [Statement 6]"
      thus ?thesis using c1 callee_covered_g_fneg_2 by (simp add: cs_route_def)
    qed
  next
    case c2
    have ctx0: "ctx = []" using covU c2 enter_callers_only_root_main_2 by fastforce
    thus ?thesis using c2 callee_covered_fpos_2 by (simp add: cs_route_def)
  next
    case c3
    have ctx0: "ctx = []" using covU c3 enter_callers_only_root_main_2 by fastforce
    thus ?thesis using c3 callee_covered_fneg_2 by (simp add: cs_route_def)
  qed
next
  case (CombFwd cl c1 dst pars args p cont)
  show ?case
    using CombFwd enter_callers_only_root_main_2 enter_callers_g_2
          covered_ret3_fpos_2 covered_ret3_fneg_2 covered_ret6_2 covered_ret7_2
          sign_nest_calls_shape
    by fastforce
qed

section ‹The headline theorem: 2-call-string activation collecting soundness›

text ‹
  ‹sign_nest_2_activation_collect_sound›, from ‹sign_nest_2_cs› and the
  initial-store bound shared with ‹k = 1›.
›

theorem sign_nest_2_activation_collect_sound:
  "𝒜⇘sign_nest_gs,context_policy_of_fun (cs_context 2),[],sign_nest_cfg,
     cinit_stores sign_nest_gs⇙ v ctx
     ⊆ gamma_lift (default_st_gamma sign_nest_gs)
           (sign_ctx_sg_2 (Inl (v, ctx)))"
  by (rule sign_nest_2_cs.routed.activation_collect_dg_sound[unfolded sign_nest_cfg_compile,
            OF entry_covered_2 sign_nest_cinit_le_cinit_sign_st])
     (simp add: le_fun_def)


section ‹The precision comparison: k=2 keeps ‹g›'s two activations separated where k=1 merges them›

text ‹
  A concrete, executable precision statement for this program and this D/G analysis: the
  1-call-string context collapses ‹g›'s two activations to one context and their join at
  ‹STop› loses all sign information, while the 2-call-string context keeps them apart and each
  retains its own exact sign. This is not a general "call strings always improve precision"
  claim --- it is the concrete forcing witness the sign lattice's finiteness lets us compute
  and verify outright, in the style of the paper's context-sensitivity discussion (Tilscher/
  Grass/Seidl, "Verifying a Solver for Mixed Flow-Sensitive Analyses").
›

lemma sign_k2_g_entry_fpos:
  "sign_nest_lookup
     (dg_local (sigma_2 (Inl (FunctionEntry (STR ''g''), [Statement 2, Statement 5]))))
     (STR ''p'') = SPos"
  unfolding sign_nest_2_sol_def sign_nest_2_eqs_def by eval

lemma sign_k2_g_entry_fneg:
  "sign_nest_lookup
     (dg_local (sigma_2 (Inl (FunctionEntry (STR ''g''), [Statement 2, Statement 6]))))
     (STR ''p'') = SNeg"
  unfolding sign_nest_2_sol_def sign_nest_2_eqs_def by eval

theorem sign_k2_strictly_more_precise_than_k1_at_g:
  "sign_nest_lookup
     (dg_local (sigma_2 (Inl (FunctionEntry (STR ''g''), [Statement 2, Statement 5]))))
     (STR ''p'')
     < sign_nest_lookup
         (dg_local (sigma_1 (Inl (FunctionEntry (STR ''g''), [Statement 2]))))
         (STR ''p'')"
  "sign_nest_lookup
     (dg_local (sigma_2 (Inl (FunctionEntry (STR ''g''), [Statement 2, Statement 6]))))
     (STR ''p'')
     < sign_nest_lookup
         (dg_local (sigma_1 (Inl (FunctionEntry (STR ''g''), [Statement 2]))))
         (STR ''p'')"
  by (simp_all add: sign_nest_1_g_entry_merged sign_k2_g_entry_fpos sign_k2_g_entry_fneg
                    less_sign_def sign_le_refl)

end