Theory Context_Space_Finite

theory Context_Space_Finite
  imports "Voblint_Framework.Call_String_Context" "Voblint_Compile.Compile_Wellformed"
begin

section ‹Which context policies can have a finite solved key set›

text ‹
  A published result table is well formed only if its key set is finite
  (‹wf_solved_table›, in the framework's result layer). A key is a
  ‹(node, context)› pair, so one way to get there is to exhibit a fixed finite set the
  keys are drawn from and appeal to ‹finite_subset›. This theory builds that set, one per
  context policy.

  What it builds is a candidate space, not a reachability or a termination result. Nothing
  below says which keys a solver run actually produces, and nothing below bounds how often
  the value at one key is raised -- an interval unknown can ascend forever inside a
  one-element key space. Both halves of the containment are therefore hypotheses of every
  result here, not conclusions:

    ▪ ‹fst ` vars ⊆ cfg_nodes (compile_prog Pi ps)› --- the keys are nodes of the program
      the solver was given. There is no theorem here connecting the vendored solver's
      returned key set to the unknowns its equation system mentions.
    ▪ ‹snd ` vars› lies in the policy's context space --- routing never left it. For call
      strings that is a length-and-alphabet condition, and truncation alone does not
      establish it: a starting context whose elements are not nodes of this program stays
      short under \<^const>‹cs_route› without ever entering the space.

  What differs between policies is how cheaply the second hypothesis can be met. Call
  strings bound the length for free: \<^const>‹cs_route› truncates every context to length at
  most ‹k› (‹cs_route_length›, \<^theory>‹Voblint_Framework.Call_String_Context›), and a
  compiled program's CFG has finitely many nodes (‹cfg_nodes_finite›,
  \<^theory>‹Voblint_CFG.CFG_Def›), so with the standard library's own
  ‹finite_lists_length_le› the space is finite for every ‹k› and every domain alike. The
  monovariant policy makes the hypothesis vacuous: its context type is \<^typ>‹unit›, so
  there is no context space to bound and the node half is the whole story.

  An entry-state context is a domain value rather than a bounded-length list over a finite
  alphabet, so it needs a separate argument. A finite value domain together with a fixed
  formals count supplies one -- ‹sign list› at the callee's arity is a finite set -- but an
  infinite-height domain such as ‹ivl› does not, and an ordinary widening policy bounds
  values rather than the context identities keyed by them. Bounding those needs a policy
  that controls key creation or merges keys (a gas budget, a tabulation cap), with real
  precision consequences that nothing here specifies. This development stops at the two
  policies whose context space needs no such decision.

  The concrete analyses reach a finite key set by an unrelated route: they discharge their
  own obligation from the vendored solver's ‹finite_stabl_solve›, which yields a finite
  stable set from a terminating solve. Neither argument implies the other -- a bounded
  candidate space does not make a solve terminate, and a terminating solve says nothing
  about the space its keys were drawn from.
›

lemma call_strings_bounded_finite:
  assumes "finite A"
  shows "finite {cs::call_string. set cs ⊆ A ∧ length cs ≤ k}"
  using assms by (rule finite_lists_length_le)

theorem compiled_call_strings_finite:
  "finite {cs::call_string. set cs ⊆ cfg_nodes (compile_prog Pi ps) ∧ length cs ≤ k}"
  using cfg_nodes_finite[OF compile_prog_finite[THEN conjunct1] compile_prog_finite[THEN conjunct2]]
  by (rule call_strings_bounded_finite)

text ‹
  The practical corollary a ‹call_string_routed_context› instance can cite directly:
  every ‹(node, call-string)› pair a ‹k›-bounded call-string analysis over a compiled
  program could ever solve for lies in a fixed finite set, so ‹vars› --- whatever a
  particular solver run actually populates it with --- is finite because it lies in a
  finite superset, not merely because the run happened to terminate.
›

theorem compiled_call_string_vars_finite:
  assumes nodes: "fst ` vars ⊆ cfg_nodes (compile_prog Pi ps)"
    and ctxs: "snd ` vars ⊆ {cs::call_string. set cs ⊆ cfg_nodes (compile_prog Pi ps)
                                ∧ length cs ≤ k}"
  shows "finite vars"
proof -
  have "vars ⊆ cfg_nodes (compile_prog Pi ps)
          × {cs::call_string. set cs ⊆ cfg_nodes (compile_prog Pi ps) ∧ length cs ≤ k}"
    using nodes ctxs by(auto; force)
  moreover have "finite (cfg_nodes (compile_prog Pi ps)
          × {cs::call_string. set cs ⊆ cfg_nodes (compile_prog Pi ps) ∧ length cs ≤ k})"
    using cfg_nodes_finite compile_prog_finite compiled_call_strings_finite
    by (blast intro: finite_cartesian_product)
  ultimately show ?thesis by (rule finite_subset)
qed

text ‹
  The seed-key space follows the same shape: one \<^const>‹Global› slot plus one \<^const>‹Seed›
  slot per (callee-entry node, call-string) pair. ‹seed_pp› ranges over \<^typ>‹pp›, which is
  \<^typ>‹cfg_node› (\<^theory>‹Voblint_CFG.CFG_Def›) -- a call-string seed is keyed by the
  callee's \<^const>‹FunctionEntry› node, not the raw procedure name -- so this reuses
  ‹cfg_nodes_finite› again rather than needing a separate finiteness fact about ‹ps›.
›

theorem compiled_call_string_gk_finite:
  "finite ({Global} ∪ (⋃p ∈ cfg_nodes (compile_prog Pi ps). Seed p `
        {cs::call_string. set cs ⊆ cfg_nodes (compile_prog Pi ps) ∧ length cs ≤ k}))"
  using compiled_call_strings_finite[of Pi ps k]
    cfg_nodes_finite[OF compile_prog_finite[of Pi ps, THEN conjunct1]
      compile_prog_finite[of Pi ps, THEN conjunct2]]
  by auto

section ‹The monovariant policy›

text ‹
  The same result for the monovariant ‹route_unit› policy, where it needs less: a context is
  \<^typ>‹unit›, so the context factor is a singleton and the node bound is the
  entire hypothesis. Stated over ‹fst ` vars› rather than a product, since with
  one context there is nothing for a product to say.
›

theorem compiled_unit_vars_finite:
  fixes vars :: "(pp × unit) set"
  assumes "fst ` vars ⊆ cfg_nodes (compile_prog Pi ps)"
  shows "finite vars"
proof -
  have "vars ⊆ cfg_nodes (compile_prog Pi ps) × (UNIV :: unit set)"
    using assms by auto
  moreover have "finite (cfg_nodes (compile_prog Pi ps) × (UNIV :: unit set))"
    using cfg_nodes_finite compile_prog_finite by force
  ultimately show ?thesis by (rule finite_subset)
qed

end