Theory Check_Report

theory Check_Report
  imports Check_Result CFG_Enumeration
begin

section ‹Whole-program executable check report›

text ‹
  A single, domain-generic report over every compiled \<^const>‹EA_Check› edge:
  one entry per check, at its own source node, classified by whatever
  ‹classify› function a domain supplies (‹sign_classify_check› and its
  siblings, or ‹sound_check_query.classify_check› generically).
  Entries are read directly off \<^const>‹intra› through the same deterministic
  order \<^const>‹cfg_intra_list› already gives the TD bridge, rather than
  sorting \<^typ>‹pp› or \<^typ>‹exp› values by hand, so the report has exactly
  one entry per \<^const>‹EA_Check› edge and no separate table can drift from it.

  This layer is deliberately generic in ‹classify›: it depends on neither
  ‹Abstract_Checks› nor a specific domain, only on a plain
  \<^typ>‹exp ⇒ 's ⇒ check_result› function and its own soundness obligations
  below.
›

type_synonym check_report_entry = "pp × exp × check_result"

definition classify_checks ::
    "cfg ⇒ (pp ⇒ 's) ⇒ (exp ⇒ 's ⇒ check_result) ⇒ check_report_entry list" where
  "classify_checks g env classify =
     map (λ(u, a, v). (u, ea_check_cond a, classify (ea_check_cond a) (env u)))
       (filter (λ(u, a, v). is_EA_Check a) (cfg_intra_list g))"

text ‹Membership unfolds to an \<^const>‹EA_Check› edge at the entry's own
  source node, classified there --- the shape every soundness and
  worked-example use of \<^const>‹classify_checks› goes through.›

lemma classify_checks_mem_iff:
  assumes "finite (intra g)"
  shows "(v, c, r) ∈ set (classify_checks g env classify)
     ⟷ (∃l tgt. (v, EA_Check l c, tgt) ∈ intra g) ∧ r = classify c (env v)"
  unfolding classify_checks_def set_map set_filter
  using set_cfg_intra_list[OF assms]
  by (auto simp: image_iff split: edge_action.splits)
     (metis edge_action.collapse surjective_pairing)

text ‹
  Soundness bridge: a \<^term>‹Check_Proved› report entry's condition genuinely
  holds at every reaching store, and a \<^term>‹Check_Refuted› entry's condition
  genuinely fails --- given the same two facts every per-domain instance
  already proves once: a ‹classify_check_proved›/‹classify_check_refuted›-
  shaped soundness obligation for the domain's own ‹classify›, and node-local
  collecting soundness (‹reach v ≤ γ⇩S (env v)›) for the checked
  node. Neither theorem invents new domain reasoning; both only relocate an
  existing per-node fact to every entry of the whole-program report.
  \<^term>‹Check_Unknown› gets no counterpart, matching ‹classify_check› itself.
›

theorem classify_checks_proved_sound:
  fixes γ⇩S :: "'s ⇒ store set"
  assumes fin: "finite (intra g)"
    and mem: "(v, c, Check_Proved) ∈ set (classify_checks g env classify)"
    and classify_proved: "⋀d s. classify c d = Check_Proved ⟹ s ∈ γ⇩S d ⟹ truthy (⟦c⟧⇩e s)"
    and node_sound: "reach v ≤ γ⇩S (env v)"
  shows "∀s ∈ reach v. truthy (⟦c⟧⇩e s)"
proof
  fix s assume s: "s ∈ reach v"
  have "classify c (env v) = Check_Proved"
    using mem classify_checks_mem_iff[OF fin, of v c Check_Proved env classify] by auto
  moreover have "s ∈ γ⇩S (env v)" using node_sound s by blast
  ultimately show "truthy (⟦c⟧⇩e s)" using classify_proved by blast
qed

theorem classify_checks_refuted_sound:
  fixes γ⇩S :: "'s ⇒ store set"
  assumes fin: "finite (intra g)"
    and mem: "(v, c, Check_Refuted) ∈ set (classify_checks g env classify)"
    and classify_refuted: "⋀d s. classify c d = Check_Refuted
                              ⟹ s ∈ γ⇩S d ⟹ ¬ truthy (⟦c⟧⇩e s)"
    and node_sound: "reach v <= γ⇩S (env v)"
  shows "∀s ∈ reach v. ~ truthy (⟦c⟧⇩e s)"
proof
  fix s assume s: "s : reach v"
  have "classify c (env v) = Check_Refuted"
    using mem classify_checks_mem_iff[OF fin, of v c Check_Refuted env classify] by auto
  moreover have "s : γ⇩S (env v)" using node_sound s by blast
  ultimately show "~ truthy (⟦c⟧⇩e s)" using classify_refuted by blast
qed

text ‹
  State-carrying sibling of \<^const>‹classify_checks›: the same traversal and
  classification, with the node's own abstract state attached to each entry.
  \<^const>‹classify_checks› stays the soundness-critical primitive every domain
  cites directly; the projection lemma below shows this report is exactly that
  one with a fourth field added, so ‹classify_checks_proved_sound› and
  ‹classify_checks_refuted_sound› reach it through the projection without
  restatement.
›

definition classify_checks_with_state ::
    "cfg ⇒ (pp ⇒ 's) ⇒ (exp ⇒ 's ⇒ check_result) ⇒ (pp × exp × check_result × 's) list" where
  "classify_checks_with_state g env classify =
     map (λ(u, c, r). (u, c, r, env u)) (classify_checks g env classify)"

lemma classify_checks_with_state_proj [simp]:
  "map (λ(u, c, r, s). (u, c, r)) (classify_checks_with_state g env classify)
     = classify_checks g env classify"
  unfolding classify_checks_with_state_def by (simp add: comp_def case_prod_beta)

end