Theory Example_Interval_DG_Ctx_Collect

theory Example_Interval_DG_Ctx_Collect
  imports
    Example_Interval_DG_Ctx_Flagship
    "Voblint_Analysis_Interval.Interval_Point_Digest"
begin

unbundle default_st_syntax

section ‹Activation-indexed collecting soundness for the routed interval solution›

text ‹
  \<^const>‹twice_program› as a concrete instance of the production entry-state soundness
  theorem ‹entry_state_activation_collect_sound› of Interval's entry-state registration
  ‹interval_es_rule› at \<^const>‹Globals_Warrow›: the hypotheses that theorem
  carries --- solver termination and four coverage facts about the solved system (the
  compiled entry, intra-edge closure, the routed callee entry, and the call
  continuation) --- are discharged here for ‹twice›, so the abstract statement becomes
  an unconditional fact about this program.

  What the instance witnesses is separation: the two call sites route to two distinct
  contexts \<^const>‹ctx_call1› / \<^const>‹ctx_call2›, and the collecting semantics is
  bounded at each of them independently.
›

subsection ‹The solved-system coverage facts›

text ‹The four coverage hypotheses are properties of the ∗‹solved› system --- which
  keys the executable solver actually covers, given its own seed and routing
  behavior --- so each is checked by evaluation against the terminated solve.›

lemma twice_entry_covered: "(cfg_entry twice_cfg, []) ∈ fst twice_ctx_sol"
  unfolding twice_ctx_sol_def twice_cfg_def by eval

text ‹❙‹Forward closure along intra edges.›  Every \<^const>‹intra› successor of a solved
  node stays solved ∗‹at the same context›.  This is not a generic solver invariant ---
  it holds because every ‹twice› node reaches the exit, so the exit query's backward
  cone materialises the whole intra-context chain.  It is a decidable closed check over
  the finite solved domain and the finite edge set (❙‹all› solved contexts, not just the
  two observed by ‹eval›).›
lemma twice_fwd_closed_all:
  "∀(u, c) ∈ fst twice_ctx_sol. ∀(u', a, v) ∈ intra twice_cfg.
      u = u' ⟶ (v, c) ∈ fst twice_ctx_sol"
  unfolding twice_ctx_sol_def twice_cfg_def by eval

lemma twice_ctx_fwd_ok:
  assumes "(u, ctx) ∈ fst twice_ctx_sol" and "(u, a, v) ∈ intra twice_cfg"
  shows "(v, ctx) ∈ fst twice_ctx_sol"
  using twice_fwd_closed_all assms by fastforce

text ‹Both call sites are reached only under the root context: ‹main› is the root
  activation, and nothing routes back into it.›
lemma twice_call_callers_only_root:
  "∀(p, ctx) ∈ fst twice_ctx_sol.
     (p = Statement 2 ∨ p = Statement 3) ⟶ ctx = []"
  unfolding twice_ctx_sol_def by eval

lemma twice_covered_cont3: "(Statement 3, []) ∈ fst twice_ctx_sol"
  unfolding twice_ctx_sol_def by eval

lemma twice_covered_cont4: "(Statement 4, []) ∈ fst twice_ctx_sol"
  unfolding twice_ctx_sol_def by eval

lemma twice_comb_fwd_ok:
  assumes "(cl, c1) ∈ fst twice_ctx_sol"
    and "(cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls twice_cfg"
  shows "(cont, c1) ∈ fst twice_ctx_sol"
  using assms twice_calls_shape twice_call_callers_only_root twice_covered_cont3 twice_covered_cont4
  by fastforce

text ‹The routed callee entry the solved system selects is the executable context the
  flagship computes: the route reads the caller's solved state from the solver's own
  table, which is exactly how \<^const>‹ctx_call1› / \<^const>‹ctx_call2› are defined.›

lemma twice_route_at_call1:
  "exec_formals_route twice_gs (Statement 2) []
     (transfer_lift twice_empty_pred
        (generic_enter_st_for ivl_ops twice_gs
           (call_info_of (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3])
             (STR ''twice'')))
        (dg_local (snd twice_ctx_sol (Inl (Statement 2, [])))))
     (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3])
   = ctx_call1"
  unfolding twice_ctx_sol_def twice_empty_pred_def ctx_call1_def interval_es_rule.ctx_succ_def
    interval_es_rule.sol_env_def interval_es_rule.entry_of_exec
  by (rule refl)

lemma twice_route_at_call2:
  "exec_formals_route twice_gs (Statement 3) []
     (transfer_lift twice_empty_pred
        (generic_enter_st_for ivl_ops twice_gs
           (call_info_of (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10])
             (STR ''twice'')))
        (dg_local (snd twice_ctx_sol (Inl (Statement 3, [])))))
     (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10])
   = ctx_call2"
  unfolding twice_ctx_sol_def twice_empty_pred_def ctx_call2_def interval_es_rule.ctx_succ_def
    interval_es_rule.sol_env_def interval_es_rule.entry_of_exec
  by (rule refl)

lemma twice_call_fwd_ok:
  assumes cov: "(u, ctx) ∈ fst twice_ctx_sol"
    and ce: "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls twice_cfg"
  shows "(FunctionEntry p,
            exec_formals_route twice_gs u ctx
              (transfer_lift twice_empty_pred
                 (generic_enter_st_for ivl_ops twice_gs (call_info_of (CallEdge dst pars args) p))
                 (dg_local (snd twice_ctx_sol (Inl (u, ctx)))))
              (CallEdge dst pars args))
         ∈ fst twice_ctx_sol"
proof -
  from ce twice_calls_shape consider
      (c1) "u = Statement 2" "dst = Some (STR ''x'')" "pars = [(STR ''p'')]"
           "args = [VIMP_Syntax.N 3]" "p = (STR ''twice'')"
    | (c2) "u = Statement 3" "dst = Some (STR ''y'')" "pars = [(STR ''p'')]"
           "args = [VIMP_Syntax.N 10]" "p = (STR ''twice'')"
    by fastforce
  thus ?thesis
  proof cases
    case c1
    have root: "ctx = []" using cov c1 twice_call_callers_only_root by fastforce
    show ?thesis
      unfolding c1 root twice_route_at_call1 by (rule callee_covered_call1)
  next
    case c2
    have root: "ctx = []" using cov c2 twice_call_callers_only_root by fastforce
    show ?thesis
      unfolding c2 root twice_route_at_call2 by (rule callee_covered_call2)
  qed
qed

subsection ‹The production soundness theorem, instantiated›

text ‹The hypotheses ‹entry_state_activation_collect_sound› carries, discharged for
  \<^const>‹twice_program›.  Every fact the production context states about this program ---
  the theorem itself, and the context-local definitions it is phrased in --- is
  conditional on exactly this bundle, so citing it once here makes each of them
  unconditional below.›

lemma twice_cfg_alt: "prog_cfg twice_program = compile_prog twice_pi twice_procs"
  by (simp add: prog_cfg_def twice_pi_def twice_procs_def)

lemmas twice_routed_hyps =
  twice_ctx_terminates
  twice_ctx_fwd_ok[unfolded twice_ctx_sol_def twice_cfg_def,
    folded interval_es_rule.sol_vars_def twice_cfg_alt]
  twice_call_fwd_ok[unfolded twice_ctx_sol_def twice_cfg_def twice_empty_pred_def,
    folded interval_es_rule.entry_of_exec[where r = Globals_Warrow],
    folded interval_es_rule.sol_vars_def interval_es_rule.sol_env_def twice_cfg_alt]
  twice_comb_fwd_ok[unfolded twice_ctx_sol_def twice_cfg_def,
    folded interval_es_rule.sol_vars_def twice_cfg_alt]

lemmas twice_entry_state_hyps =
  twice_routed_hyps
  twice_entry_covered[unfolded twice_ctx_sol_def twice_cfg_def,
    folded interval_es_rule.sol_vars_def twice_cfg_alt]

theorem twice_activation_collect_sound:
  "𝒜⇘twice_gs,
     interval_es_rule.admitted_contexts Globals_Warrow twice_gs twice_program,
     [],compile_prog twice_pi twice_procs,cinit_stores twice_gs⇙ v ctx
   ⊆ gamma_lift (default_st_gamma twice_gs)
       (interval_es_rule.reader Globals_Warrow twice_gs twice_program (Inl (v, ctx)))"
  unfolding twice_cfg_alt[symmetric] gamma_lift_default_st_gamma_to_fun
  by (rule interval_es_rule.entry_state_activation_collect_sound[OF twice_entry_state_hyps])

subsection ‹The context each call site selects›

text ‹\<^const>‹dg_analysis.admitted_contexts› admits a routed context relationally
  rather than computing one from the concrete store, so at each call site it admits
  exactly the constant the flagship computed.›


lemma twice_call_site_action1:
  "call_action_at_call_site (compile_prog twice_pi twice_procs) (Statement 2)
     = CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3]"
proof (rule call_action_at_call_site_eq
    [OF twice.finite_calls[unfolded twice_cfg_def] compile_prog_calls_source_unique])
  show "(Statement 2, CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3],
          FunctionEntry (STR ''twice''), Statement 3)
          ∈ calls (compile_prog twice_pi twice_procs)"
    by eval
qed

lemma twice_call_site_action2:
  "call_action_at_call_site (compile_prog twice_pi twice_procs) (Statement 3)
     = CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10]"
proof (rule call_action_at_call_site_eq
    [OF twice.finite_calls[unfolded twice_cfg_def] compile_prog_calls_source_unique])
  show "(Statement 3, CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10],
          FunctionEntry (STR ''twice''), Statement 4)
          ∈ calls (compile_prog twice_pi twice_procs)"
    by eval
qed

text ‹The admitted-context relation is a relation, not a function: it admits a context
  rather than picking one, so what holds at \<^const>‹ctx_call1›/\<^const>‹ctx_call2› is
  membership under any store the call site actually covers.›

lemma twice_context_at_call1:
  assumes sin: "s ∈ γ (ρ⇘twice_gs⇙ (dg_local (snd twice_ctx_sol (Inl (Statement 2, [])))))"
  shows "ctx_call1 ∈ interval_es_rule.admitted_contexts Globals_Warrow twice_gs twice_program
           (Statement 2) []
           (call_info_of (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3])
             (STR ''twice''))
           s (call_enter twice_gs (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3]) s)"
proof -
  let ?ci = "call_info_of (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3])
               (STR ''twice'')"
  let ?d = "dg_local (snd twice_ctx_sol (Inl (Statement 2, [])))"
  let ?entry = "transfer_lift twice_empty_pred (generic_enter_st_for ivl_ops twice_gs ?ci) ?d"
  have cov: "entry_pairs_cover
      (λd'. γ (ρ⇘twice_gs⇙ d'))
      s (call_enter twice_gs (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3]) s)
      [(?d, ?entry)]"
    using ivl_tf.entry_cover_exec[OF twice_exact sin, where ci = ?ci] by simp
  have ecov: "call_enter twice_gs (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3]) s
                ∈ γ (ρ⇘twice_gs⇙ ?entry)"
    using cov unfolding entry_pairs_cover_def by simp
  have base: "exec_formals_route twice_gs (Statement 2) [] ?entry
         (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3])
      ∈ interval_es_rule.admitted_contexts Globals_Warrow twice_gs twice_program
      (Statement 2) [] ?ci s
      (call_enter twice_gs (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3]) s)"
    unfolding twice_empty_pred_def twice_ctx_sol_def
      interval_es_rule.entry_of_exec[where r = Globals_Warrow, symmetric]
      interval_es_rule.sol_env_def[symmetric]
    by (rule interval_es_rule.admitted_contextsI_call)
       (use sin ecov in
          ‹simp_all add: gamma_lift_default_st_gamma_to_fun
             twice_empty_pred_def twice_ctx_sol_def interval_es_rule.sol_env_def
             interval_es_rule.entry_of_exec dg_pipeline.entry_alt_def Let_def›)
  thus ?thesis    by (simp add: twice_route_at_call1)
qed

lemma twice_context_at_call2:
  assumes sin: "s ∈ γ (ρ⇘twice_gs⇙ (dg_local (snd twice_ctx_sol (Inl (Statement 3, [])))))"
  shows "ctx_call2 ∈ interval_es_rule.admitted_contexts Globals_Warrow twice_gs twice_program
           (Statement 3) []
           (call_info_of
             (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10])
             (STR ''twice''))
           s (call_enter twice_gs (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10]) s)"
proof -
  let ?ci = "call_info_of (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10])
               (STR ''twice'')"
  let ?d = "dg_local (snd twice_ctx_sol (Inl (Statement 3, [])))"
  let ?entry = "transfer_lift twice_empty_pred (generic_enter_st_for ivl_ops twice_gs ?ci) ?d"
  have cov: "entry_pairs_cover
      (λd'. γ (ρ⇘twice_gs⇙ d'))
      s (call_enter twice_gs (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10]) s)
      [(?d, ?entry)]"
    using ivl_tf.entry_cover_exec[OF twice_exact sin, where ci = ?ci] by simp
  have ecov: "call_enter twice_gs (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10]) s
                ∈ γ (ρ⇘twice_gs⇙ ?entry)"
    using cov unfolding entry_pairs_cover_def by simp
  have base: "exec_formals_route twice_gs (Statement 3) [] ?entry
         (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10])
      ∈ interval_es_rule.admitted_contexts Globals_Warrow twice_gs twice_program
      (Statement 3) [] ?ci s
      (call_enter twice_gs (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10]) s)"
    unfolding twice_empty_pred_def twice_ctx_sol_def
      interval_es_rule.entry_of_exec[where r = Globals_Warrow, symmetric]
      interval_es_rule.sol_env_def[symmetric]
    by (rule interval_es_rule.admitted_contextsI_call)
       (use sin ecov in
          ‹simp_all add: gamma_lift_default_st_gamma_to_fun
             twice_empty_pred_def twice_ctx_sol_def interval_es_rule.sol_env_def
             interval_es_rule.entry_of_exec dg_pipeline.entry_alt_def Let_def›)
  thus ?thesis    by (simp add: twice_route_at_call2)
qed


subsection ‹The concrete store-decoding context, and its agreement with the analysis›

text ‹
  ‹ivl_context› decodes the entered store's formals, and the lemmas below show it
  agrees with the analysis's routed context at both calls of ‹twice›.
›

definition ivl_context :: "cfg_node ⇒ ivl list ⇒ store ⇒ ivl list" where
  "ivl_context = formals_context_sem twice_cfg ivl_decode"

text ‹\<^const>‹ivl_context› is the ∗‹semantic› reading of the same partial-tabulation policy
  (Seidl et al., ∗‹Mixed Flow-Sensitive Static Analysis›, FM 2026, Example 8):
  it decodes the concrete entered store's formals
  through \<^const>‹ivl_decode›, looking its formals up from the call site via
  \<^const>‹formals_at_call_site›.  \<^const>‹dg_analysis.admitted_contexts›
  instead ignores the store and
  recomputes the routed value from the caller's solved abstract state.  The two are
  distinct functions; for ‹twice›'s two constant-argument calls they agree, which is
  exactly why this program's abstract contexts are the exact point abstractions of the
  values actually entered.›

text ‹The formals of each call site, computed directly from \<^const>‹twice_cfg› via
  \<^const>‹formals_at_call_site› rather than assumed.›
lemma twice_formals_at_call_site2: "formals_at_call_site twice_cfg (Statement 2) = [(STR ''p'')]"
  unfolding formals_at_call_site_def by eval

lemma twice_formals_at_call_site3: "formals_at_call_site twice_cfg (Statement 3) = [(STR ''p'')]"
  unfolding formals_at_call_site_def by eval

lemma enter_route_exact_call1:
  assumes "u = Statement 2"
    and "s' = call_enter twice_gs (CallEdge dst [(STR ''p'')] [VIMP_Syntax.N 3]) s"
  shows "ivl_context u ctx s' = ctx_call1"
proof -
  from assms(2) have "s' = (enter_state twice_gs s)((STR ''p'') := 3)"
    by (simp add: call_enter_CallEdge)
  thus ?thesis
    unfolding assms(1) ivl_context_def formals_context_sem_def
    by (simp add: twice_formals_at_call_site2 formals_context_def ivl_decode_def ctx_call1_val)
qed

lemma enter_route_exact_call2:
  assumes "u = Statement 3"
    and "s' = call_enter twice_gs (CallEdge dst [(STR ''p'')] [VIMP_Syntax.N 10]) s"
  shows "ivl_context u ctx s' = ctx_call2"
proof -
  from assms(2) have "s' = (enter_state twice_gs s)((STR ''p'') := 10)"
    by (simp add: call_enter_CallEdge)
  thus ?thesis
    unfolding assms(1) ivl_context_def formals_context_sem_def
    by (simp add: twice_formals_at_call_site3 formals_context_def ivl_decode_def ctx_call2_val)
qed

text ‹The semantic store-decode and the routed relation agree: the value \<^const>‹ivl_context›
  computes from the concrete entered store is itself an admitted context at each call
  site's own edge. The relation depends on the edge that produced the entry, so the
  statement fixes ‹dst› to that edge.›

theorem ivl_context_is_entry_state_context_call1:
  assumes cov: "s ∈ γ (ρ⇘twice_gs⇙ (dg_local (snd twice_ctx_sol (Inl (Statement 2, [])))))"
    and es:
      "s' = call_enter twice_gs (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3]) s"
  shows "ivl_context (Statement 2) [] s' ∈ interval_es_rule.admitted_contexts Globals_Warrow twice_gs twice_program
           (Statement 2) [] (call_info_of (CallEdge (Some (STR ''x'')) [(STR ''p'')] [VIMP_Syntax.N 3]) (STR ''twice''))
           s s'"
proof -
  have "ivl_context (Statement 2) [] s' = ctx_call1"
    by (rule enter_route_exact_call1[OF refl es])
  thus ?thesis using twice_context_at_call1[OF cov] es by simp
qed

theorem ivl_context_is_entry_state_context_call2:
  assumes cov: "s ∈ γ (ρ⇘twice_gs⇙ (dg_local (snd twice_ctx_sol (Inl (Statement 3, [])))))"
    and es:
      "s' = call_enter twice_gs (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10]) s"
  shows "ivl_context (Statement 3) [] s' ∈ interval_es_rule.admitted_contexts Globals_Warrow twice_gs twice_program
           (Statement 3) []
           (call_info_of
             (CallEdge (Some (STR ''y'')) [(STR ''p'')] [VIMP_Syntax.N 10])
             (STR ''twice''))
           s s'"
proof -
  have "ivl_context (Statement 3) [] s' = ctx_call2"
    by (rule enter_route_exact_call2[OF refl es])
  thus ?thesis using twice_context_at_call2[OF cov] es by simp
qed


subsection ‹Shared-state regression facts›

text ‹The local unknown carries the whole abstract state, so a variable that is shared
  across activations is read at the very same slot as a formal.  A name that
  \<^const>‹twice_program› never declares --- ‹Gx› --- therefore reads identically in both
  callee contexts: no name-based convention for globals gives it a separate,
  context-indexed slot.›
lemma global_slot_shared:
  "twice_ctx_lookup (dg_local (snd twice_ctx_sol (Inl (FunctionEntry (STR ''twice''), ctx_call1)))) (STR ''Gx'')
     = twice_ctx_lookup (dg_local (snd twice_ctx_sol (Inl (FunctionEntry (STR ''twice''), ctx_call2)))) (STR ''Gx'')"
  unfolding ctx_call1_val ctx_call2_val twice_ctx_sol_def twice_empty_pred_def by eval

text ‹The solver-global carrier stays inert: every field of the Base-style specification
  threads its incoming ‹g› through unchanged, so the shared \<^const>‹Global› unknown is
  never used to reconstruct program state.›
lemma twice_ctx_global_slot_inert:
  "dg_global (snd twice_ctx_sol (Inr (Analysis_Global ()))) = Bot"
  unfolding twice_ctx_sol_def twice_empty_pred_def by eval


unbundle no default_st_syntax

end