Theory DG_Analysis_Adapter

theory DG_Analysis_Adapter
  imports Routed_Context Contextual_Check_Report
begin

section ‹Public result and check-report adapter for a routed DG analysis›

text ‹
  Every concrete routed-context analysis needs the same public
  type‹solved_table›/check report/soundness triple, and each one follows
  the identical shape once a routed D/G equation system is solved: read the
  local unknown at every covered ‹(node, context)› pair, together with the
  analysis-wide global unknown, into an type‹solved_table›, classify every
  compiled check against it via const‹classify_checks_verdicts›, and
  discharge that report's own soundness from the activation-indexed collecting
  semantics
  (theory‹Voblint_Framework.Activation_Backbone›) already available once
  EDGE/CALL/COMB are in hand from locale‹routed_context›.
  ‹dg_analysis_adapter› derives that whole triple once, generic in a domain
  instance (a ‹classify› function with its own soundness obligations), a
  context instance (an interpretation of locale‹routed_context›),
  and the published value (a publication map ‹rd› from a local and a global
  value of the solver's carrier into a value type ‹'v› with its own
  concretization ‹γV› and exact emptiness test ‹emptyV›; a
  non-relational analysis publishes its abstract store),
  leaving solver choice orthogonal: which concrete solver produced
  ‹sigma›/‹sg› is an interpretation-site argument, never a locale parameter,
  matching how Interval's own Warrow/join/per-origin solver choice is already
  orthogonal to its context.

  ‹gammaDG_rd› asks that publishing a local value together with a global one
  keeps exactly the stores the pair denotes,
  ‹γDG d g' = gamma_lift γV (rd d g')›. The global value the table
  pairs with every local one is the solved global unknown at
  ‹Inr buffer_key›, the pairing the coverage assumption ‹sg_cov› of
  locale‹dg_context_activation› concretizes. A concretization that reads both
  components, an ownership split say, therefore interprets this locale
  directly. An analysis whose concretization ignores the global half
  instantiates ‹rd› at a function constant in its second argument.
›

locale dg_analysis_adapter =
  routed_context S γDG 𝒢 g buffer_key global_of route bot0 d0 g0 sigma vars x0 sg
    seed
    "static_resolve g" is_bot γM adm
  for S :: "(pp × 'c, 'k, 'n, 'D::bounded_semilattice_sup_bot,
              'G::bounded_semilattice_sup_bot) dg_spec"
    and γDG :: "'D ⇒ ('n ⇒ 'G) ⇒ store set"
    and 𝒢 :: "vname ⇒ bool"
    and g buffer_key and global_of :: "'n ⇒ 'k"
    and route :: "pp ⇒ 'c ⇒ 'D ⇒ call_action ⇒ 'c"
    and bot0 d0 :: 'D and g0 :: 'G
    and sigma :: "pp × 'c + 'k ⇒ ('D, 'G) dg_state"
    and vars :: "(pp × 'c) set"
    and x0 :: "pp × 'c"
    and sg :: "pp × 'c + 'k ⇒ 'M"
    and seed :: "pp ⇒ 'c ⇒ 'k"
    and is_bot :: "'D ⇒ bool"
    and γM :: "'M ⇒ store set"
    and adm :: "'c context_policy" +
  fixes rd :: "'D ⇒ ('n ⇒ 'G) ⇒ 'v lifted"
    and γV :: "'v ⇒ store set"
    and emptyV :: "'v ⇒ bool"
    and classify :: "exp ⇒ 'v ⇒ check_result"
  assumes gammaDG_rd: "⋀d g'. γDG d g' = gamma_lift γV (rd d g')"
    and empty_sound: "⋀v. emptyV v ⟹ γV v = {}"
    and classify_proved:
    "⋀c d s. classify c d = Check_Proved ⟹ s ∈ γV d ⟹ truthy (⟦c⟧e s)"
    and classify_refuted:
    "⋀c d s. classify c d = Check_Refuted ⟹ s ∈ γV d ⟹ ¬ truthy (⟦c⟧e s)"
    and vars_finite: "finite vars"
begin


subsection ‹The public result table›

text ‹
  Built from the locale's own solved ‹vars›/‹sigma› pair, mirroring how
  ‹dg_result_for› builds an
  type‹solved_table› from an already-solved key set and reader.
  The solved local unknown and the solved global at ‹Inr buffer_key› are
  published into typ‹'v lifted› by ‹rd›, and the
  one collapse this table then needs is const‹canonicalize_lift› against
  ‹emptyV›, so a const‹Lifted› payload that denotes no store without
  the solver's own const‹Bot› tag reads as const‹Bot› here, matching const‹classify_point›'s
  documented discipline of never fabricating a vacuous const‹Check_Proved›
  off an empty state.
›

definition analyse_result :: "('c, 'v) solved_table" where
  "analyse_result = Solved_Table vars
     (λv ctx. canonicalize_lift emptyV
        (rd (dg_local (sigma (Inl (v, ctx)))) (genv global_of sigma)))"

lemma lookup_table_analyse_result:
  "lookup_table analyse_result v ctx =
     (if (v, ctx) ∈ vars
      then canonicalize_lift emptyV
             (rd (dg_local (sigma (Inl (v, ctx)))) (genv global_of sigma))
      else Bot)"
  unfolding lookup_table_def analyse_result_def by simp

text ‹Canonicality holds unconditionally here: const‹canonicalize_lift› is
  exactly what rules out a const‹Lifted› payload that is secretly empty, and
  it runs on every entry the table publishes.

  Finiteness cannot be proved here, because ‹vars› is a fixed arbitrary set and
  this locale deliberately does not know which solver produced it --- that is
  what keeps it independent of solver choice. It is therefore an assumption,
  ‹vars_finite›, and an interpretation discharges it from the solver it actually
  ran: ‹finite_stabl_solve› says a terminating solve stabilizes finitely many
  unknowns, and the interpretation site is the only place that knows ‹vars› is
  that stable set.

  Nothing about the context type enters, which is why entry-state contexts are
  covered as readily as monovariant ones despite their context space being
  unbounded.›

lemma analyse_result_canonical:
  assumes "lookup_table analyse_result v ctx = Lifted st"  shows "¬ emptyV st"
  using assms
  unfolding lookup_table_analyse_result
  by (cases "rd (dg_local (sigma (Inl (v, ctx)))) (genv global_of sigma)")
     (auto simp: normalize_lift_def split: if_splits)

theorem wf_analyse_result: "wf_solved_table emptyV analyse_result"
  unfolding wf_solved_table_def finite_solved_table_def
  using vars_finite analyse_result_canonical by (simp add: analyse_result_def)

text ‹
  The soundness bridge ‹γM (sg (Inl (v, ctx)))› steps need: a covered
  point's guarded reading agrees exactly with ‹analyse_result›'s own
  const‹lookup_table› answer at the same key, const‹Bot›
  concretizing to the empty set and const‹Lifted› to ‹γV› of its
  payload.
›

text ‹Collapsing a payload that denotes nothing to const‹Bot› does not change
  what the value denotes.›

lemma gamma_lift_canonicalize [simp]:
  "gamma_lift γV (canonicalize_lift emptyV x) = gamma_lift γV x"
  by (cases x) (simp_all add: normalize_lift_def empty_sound)

lemma gammaM_sg_eq_lookup_table:
  assumes cov: "(v, ctx) ∈ vars"
  shows "γM (sg (Inl (v, ctx))) = gamma_lift γV (lookup_table analyse_result v ctx)"
proof -
  have "γM (sg (Inl (v, ctx))) = γDG (dg_local (sigma (Inl (v, ctx))))
          (genv global_of sigma)"
    using cov by simp
  also have "… = gamma_lift γV
                        (rd (dg_local (sigma (Inl (v, ctx)))) (genv global_of sigma))"
    by (rule gammaDG_rd)
  also have "… = gamma_lift γV (lookup_table analyse_result v ctx)"
    using cov unfolding lookup_table_analyse_result by simp
  finally show ?thesis .
qed


text ‹
  The node-soundness bridge a concrete instance's own report-soundness proof
  needs, phrased directly against const‹analyse_result› rather than against
  ‹analyse_report_ctx› (defined below): every activation-collected store at ‹v› is
  concretized by const‹analyse_result›'s own reading, const‹bot› when
  uncovered or witness-bottom, its const‹Lifted› payload otherwise ---
  composing ‹activation_collect_dg_sound› with ‹gammaM_sg_eq_lookup_table›,
  case-split on coverage. A concrete instance whose own public result reads
  through this same ‹analyse_result› (up to a proved value equality) gets its
  own node-soundness bridge from this lemma directly, instead of re-deriving
  it from ‹routed_context›'s primitives by hand.
›

lemma analyse_result_node_sound:
  fixes S0 :: "store set" and c0 :: 'c
  assumes entry_cov: "(cfg_entry g, c0) ∈ vars"
    and init_sound: "S0 ⊆ γDG d0 e0"
    and init_env_le: "e0 ≤ genv global_of sigma"
  shows "𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx
           ⊆ gamma_lift γV (lookup_table analyse_result v ctx)"
proof -
  have "𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx
          ⊆ γM (sg (Inl (v, ctx)))"
    by (rule activation_collect_dg_sound[OF entry_cov init_sound init_env_le])
  also have "… = gamma_lift γV (lookup_table analyse_result v ctx)"
  proof (cases "(v, ctx) ∈ vars")
    case True
    show ?thesis by (rule gammaM_sg_eq_lookup_table[OF True])
  next
    case False
    hence "γM (sg (Inl (v, ctx))) = {}" by simp
    moreover from False have "lookup_table analyse_result v ctx = Bot"
      unfolding lookup_table_analyse_result by simp
    ultimately show ?thesis by simp
  qed
  finally show ?thesis by simp
qed

text ‹
  ‹analyse_result_node_sound› is stated in the vocabulary
  theory‹Voblint_Framework.Solved_Table› states its lookup facts in: every
  covered lookup safely abstracts the activation-collected stores at its key.  It
  is the general statement, with no bottom case baked in --- the unreachability
  reading is one instantiation of it, below.

  Note what the coverage case split above establishes and this inherits: inside
  this locale an ∗‹uncovered› key is not merely uninformative, since
  term‹γM (sg (Inl (v, ctx)))› is empty off term‹vars› and the collect is
  contained in it either way.  That is a property of a solve satisfying this
  locale's assumptions, not of const‹lookup_table›, which is why the
  unreachability corollary still demands term‹Covered Bot›: a caller reading a
  result table without these assumptions in hand has no such guarantee.
›

lemma analyse_result_covered_unreachable:
  fixes S0 :: "store set" and c0 :: 'c
  assumes entry_cov: "(cfg_entry g, c0) ∈ vars"
    and init_sound: "S0 ⊆ γDG d0 e0"
    and init_env_le: "e0 ≤ genv global_of sigma"
    and dead: "lookup_coverage analyse_result v ctx = Covered Bot"
  shows "𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx = {}"
  by (rule reported_covered_unreachable_empty
      [OF dead analyse_result_node_sound[OF entry_cov init_sound init_env_le]])

lemma covered_keys_analyse_result [simp]: "covered_keys analyse_result = vars"
  unfolding analyse_result_def by simp

text ‹
  The node-level statement, one activation bucket at a time.  A covered context
  is const‹Bot› by the node predicate; an uncovered one reads const‹Bot› from
  const‹lookup_table› anyway, and here that is not a shrug --- this locale's
  own soundness already puts the collect inside an empty concretization there.
  So every bucket is empty and so is their union.

  term‹node_collect› decomposes into those buckets only for a context relation
  that comes from a function, which this locale does not assume of term‹adm›;
  the decomposition is therefore a hypothesis, discharged by
  ‹node_collect_eq_Union_activation_of_fun› at every instance whose relation has
  that shape.
›

lemma analyse_result_node_unreachable:
  fixes S0 :: "store set" and c0 :: 'c
  assumes entry_cov: "(cfg_entry g, c0) ∈ vars"
    and init_sound: "S0 ⊆ γDG d0 e0"
    and init_env_le: "e0 ≤ genv global_of sigma"
    and union: "𝒞⇘𝒢,g,S0⇙ v
                  = (⋃ctx. 𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx)"
    and dead: "result_node_is_bottom analyse_result v"
  shows "𝒞⇘𝒢,g,S0⇙ v = {}"
proof -
  have bucket: "𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx = {}" for ctx
  proof -
    have bot: "lookup_table analyse_result v ctx = Bot"
    proof (cases "(v, ctx) ∈ vars")
      case True
      have "lookup_coverage analyse_result v ctx = Covered Bot"
        using True by (intro result_node_is_bottomD[OF dead]) simp
      then show ?thesis unfolding lookup_table_eq_or_bot by simp
    next
      case False
      then show ?thesis unfolding lookup_table_analyse_result by simp
    qed
    have "𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx
            ⊆ gamma_lift γV (lookup_table analyse_result v ctx)"
      by (rule analyse_result_node_sound[OF entry_cov init_sound init_env_le])
    then show ?thesis unfolding bot by simp
  qed
  show ?thesis unfolding union using bucket by simp
qed

subsection ‹The context-indexed check report›

text ‹The report the CLI prints, defined at the context-indexed level rather than after the
  join: one verdict per check, aggregated over exactly the contexts the solved table covers
  at that node.  Aggregating first would classify against a joined state and lose the
  precision each context carries.›
definition analyse_report_ctx :: "(pp × exp × contextual_verdict) list" where
  "analyse_report_ctx = classify_checks_verdicts g analyse_result classify"

subsection ‹Report soundness›

text ‹
  ‹S0› and ‹c0› are the two facts genuinely external to this
  locale: which concrete stores the analysis actually starts from, and which
  context the solved system covers the entry point under. Every existing
  concrete instance (e.g. Interval's entry-state and call-string contexts)
  discharges both as per-instance facts about its own solved system, not as
  locale theorems, since they depend on which keys a terminated solve
  actually reached --- ‹entry_cov› mirrors those instances' own ‹entry_cov›
  context assumption, and ‹init_sound› is the initial-store premise every
  activation-trace-level soundness theorem in this development already takes.
›
text ‹Both endpoints below reach their classifier obligation the same way, and
  that route is this lemma: a collected store at a decided check sits inside
  some reachable state the report classified, and the report's verdict is what
  the classifier said about that very state. Only the appeal to
  ‹classify_proved› or ‹classify_refuted› afterwards differs.›

lemma analyse_report_ctx_decided:
  fixes S0 :: "store set" and c0 :: 'c and v :: cfg_node and c :: exp
  assumes mem: "(v, c, Decided r) ∈ set analyse_report_ctx"
    and entry_cov: "(cfg_entry g, c0) ∈ vars"
    and init_sound: "S0 ⊆ γDG d0 e0"
    and init_env_le: "e0 ≤ genv global_of sigma"
    and smem: "s ∈ 𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx"
    and known: "r ≠ Check_Unknown"
  obtains st where "s ∈ γV st" and "classify c st = r"
proof -
  have node_sound: "𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx
      ⊆ gamma_lift γV (lookup_table analyse_result v ctx)"
    by (rule analyse_result_node_sound[OF entry_cov init_sound init_env_le])
  obtain st where reach: "lookup_table analyse_result v ctx = Lifted st"
    and sst: "s ∈ γV st"
    using smem node_sound by (cases "lookup_table analyse_result v ctx") auto
  have "classify c st = r"
    using classify_checks_ctx_decided_sound[OF finE
            mem[unfolded analyse_report_ctx_def] reach known] .
  with sst show ?thesis by (rule that)
qed

theorem analyse_report_ctx_proved_sound:
  fixes S0 :: "store set" and c0 :: 'c and v :: cfg_node and c :: exp
  assumes mem: "(v, c, Decided Check_Proved) ∈ set analyse_report_ctx"
    and entry_cov: "(cfg_entry g, c0) ∈ vars"
    and init_sound: "S0 ⊆ γDG d0 e0"
    and init_env_le: "e0 ≤ genv global_of sigma"
  shows "⋀ctx s. s ∈ 𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx
           ⟹ truthy (⟦c⟧e s)"
proof -
  fix ctx s
  assume smem: "s ∈ 𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx"
  obtain st where sst: "s ∈ γV st" and "classify c st = Check_Proved"
    by (rule analyse_report_ctx_decided[OF mem entry_cov init_sound init_env_le smem]) simp
  thus "truthy (⟦c⟧e s)" using classify_proved[OF _ sst] by blast
qed

theorem analyse_report_ctx_refuted_sound:
  fixes S0 :: "store set" and c0 :: 'c and v :: cfg_node and c :: exp
  assumes mem: "(v, c, Decided Check_Refuted) ∈ set analyse_report_ctx"
    and entry_cov: "(cfg_entry g, c0) ∈ vars"
    and init_sound: "S0 ⊆ γDG d0 e0"
    and init_env_le: "e0 ≤ genv global_of sigma"
  shows "⋀ctx s. s ∈ 𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx
           ⟹ ¬ truthy (⟦c⟧e s)"
proof -
  fix ctx s
  assume smem: "s ∈ 𝒜⇘𝒢,adm,c0,g,S0⇙ v ctx"
  obtain st where sst: "s ∈ γV st" and "classify c st = Check_Refuted"
    by (rule analyse_report_ctx_decided[OF mem entry_cov init_sound init_env_le smem]) simp
  thus "¬ truthy (⟦c⟧e s)" using classify_refuted[OF _ sst] by blast
qed

end

end