Theory Contextual_Check_Report

theory Contextual_Check_Report
  imports Check_Report Solved_Table Analysis_Query
begin

section ‹Contextual check verdicts over a solved result table›

text ‹
  \<^const>‹classify_checks› reads exactly one abstract state per checked node.
  A context-sensitive result has one state per ‹(node, context)› pair
  instead, and some of those pairs represent no concrete execution at all: a
  branch that is dead inside one activation, or an activation a node is never
  reached under. Classifying such a point against its stored state answers
  vacuously: a classifier's soundness obligation only constrains the stores
  its state represents, so on a state representing none, either definite
  answer satisfies that obligation vacuously --- a verdict read there is
  evidence of nothing, and reporting it as \<^const>‹Check_Proved› would
  fabricate a proof about executions that do not exist.

  ‹contextual_verdict› keeps that case outside \<^typ>‹check_result› rather
  than folding it into one of its three values. ‹Dead› means ``no concrete
  execution is represented here''; it is neither \<^const>‹Check_Unknown›, which
  says only that the abstraction decided the condition neither way on a state
  representing some stores --- it asserts no reachability, since those stores
  may over-approximate a point no execution reaches --- nor
  \<^const>‹Check_Proved›.
›

text ‹
  ‹contextual_verdict› is literally \<^typ>‹check_result lifted›
  (\<^theory>‹Voblint_Domain.Reachability_Lift›): ‹Dead› is \<^const>‹Bot›, ‹Decided›
  is \<^const>‹Lifted›, and its order/bottom/join are \<^typ>‹'a lifted›'s own
  generic instance at
  \<^typ>‹check_result› (itself \<^class>‹semilattice_sup›, from
  \<^theory>‹Voblint_Framework.Check_Result›) constructor for constructor: ‹Dead ≤ _›
  always, a ‹Decided› never sits below ‹Dead›, and two ‹Decided› verdicts
  compare and join through \<^typ>‹check_result›'s own flat order. Reusing it
  here keeps one lattice construction for "structurally absent vs. present
  with a payload" instead of two.
›

type_synonym contextual_verdict = "check_result lifted"

abbreviation Dead :: contextual_verdict where
  "Dead ≡ Bot"

abbreviation Decided :: "check_result ⇒ contextual_verdict" where
  "Decided r ≡ Lifted r"


subsection ‹Classifying one contextual point›

text ‹
  The reachability decision is not remade here: it was already made when the
  raw solved local unknown crossed the result boundary, one layer before the
  lifted readback relabels it structurally. A witness-bottom
  \<^const>‹Lifted› payload is collapsed to \<^const>‹Bot› by
  \<^const>‹canonicalize_lift›, so by the time a value is read back --- as
  every public result adapter's raw value is --- \<^const>‹Bot› already
  denotes no store. A \<^const>‹Lifted› state
  may still denote none, since the emptiness test is sound and incomplete, and
  classifying it is then vacuous but harmless. ‹classify_point› only refuses to
  classify against a state that represents nothing: a covered-but-dead
  activation, whose raw stored state a solver run could otherwise leave as
  a witness-bottom \<^const>‹Lifted›, reaches ‹classify_point› as
  \<^const>‹Bot› rather than fabricating a vacuous
  \<^const>‹Check_Proved› off an empty state.
›

fun classify_point ::
  "(exp ⇒ 'a ⇒ check_result) ⇒ exp ⇒ 'a lifted ⇒ contextual_verdict"
where
  "classify_point classify c Bot = Dead"
| "classify_point classify c (Lifted st) = Decided (classify c st)"

subsection ‹Classifying by query›

text ‹
  A check ‹c› is decided by one question, the value of its truth as an
  integer, which every analysis in a product answers and whose combined answer
  is the meet. Goblint's ‹assert› analysis asks ‹EvalInt (c != 0)› through
  ‹Queries.eval_bool›; a comparison or logical operator already evaluates to
  ‹0› or ‹1›, so for those Voblint asks about ‹c› itself and an analysis sees
  the comparison rather than its test against zero. An exact ‹1› proves the
  check and an exact ‹0› refutes it. ‹QBot› holds at no store, so a sound
  combined answer is ‹QBot› only where the state represents no store, and
  ‹classify_answer› reads it as ‹Dead›. Anything else decides
  nothing.
›

fun bool_valued :: "exp ⇒ bool" where
  "bool_valued (Not _) = True"
| "bool_valued (And _ _) = True"
| "bool_valued (Or _ _) = True"
| "bool_valued (Less _ _) = True"
| "bool_valued (LessEq _ _) = True"
| "bool_valued (Greater _ _) = True"
| "bool_valued (GreaterEq _ _) = True"
| "bool_valued (Eq _ _) = True"
| "bool_valued (NotEq _ _) = True"
| "bool_valued _ = False"

lemma aval_bool_valued:
  "bool_valued e ⟹ ⟦e⟧⇩e s = (if truthy (⟦e⟧⇩e s) then 1 else 0)"
  by (cases e) auto

definition check_truth_exp :: "exp ⇒ exp" where
  "check_truth_exp c = (if bool_valued c then c else NotEq c (N 0))"

lemma bool_valued_check_truth_exp [simp]: "bool_valued (check_truth_exp c)"
  by (simp add: check_truth_exp_def)

lemma aval_check_truth_exp:
  "⟦check_truth_exp c⟧⇩e s = (if truthy (⟦c⟧⇩e s) then 1 else 0)"
  by (auto simp: check_truth_exp_def dest: aval_bool_valued[of c s])

abbreviation check_query_of :: "exp ⇒ query" where
  "check_query_of c ≡ EvalInt (check_truth_exp c)"

fun classify_answer :: "answer ⇒ contextual_verdict" where
  "classify_answer QBot = Dead"
| "classify_answer a =
     (if answer_const a = Some 1 then Decided Check_Proved
      else if answer_const a = Some 0 then Decided Check_Refuted
      else Decided Check_Unknown)"

lemma classify_answer_proved:
  assumes "classify_answer a = Decided Check_Proved"
    and "eval_holds (check_query_of c) a s"
  shows "truthy (⟦c⟧⇩e s)"
proof -
  have "answer_const a = Some 1"
    using assms(1) by (cases a rule: classify_answer.cases)
      (auto split: option.splits if_splits simp del: answer_const.simps)
  from eval_holds_constD[OF assms(2) this] show ?thesis
    by (simp add: aval_check_truth_exp split: if_splits)
qed

lemma classify_answer_refuted:
  assumes "classify_answer a = Decided Check_Refuted"
    and "eval_holds (check_query_of c) a s"
  shows "¬ truthy (⟦c⟧⇩e s)"
proof -
  have "answer_const a = Some 0"
    using assms(1) by (cases a rule: classify_answer.cases)
      (auto split: option.splits if_splits simp del: answer_const.simps)
  from eval_holds_constD[OF assms(2) this] show ?thesis
    by (simp add: aval_check_truth_exp split: if_splits)
qed

lemma classify_answer_dead:
  assumes "classify_answer a = Dead"
  shows "¬ eval_holds (EvalInt e) a s"
  using assms by (cases a) (auto split: if_splits)

subsection ‹Aggregating the contexts observed at one check›

text ‹
  Folding \<^const>‹sup› from ‹Dead› over a finite set of observations. The
  fold's unit is the empty-set answer, so a check with no covered context
  needs no separate guard. The ‹[code]› equation is the usual
  ‹comp_fun_idem› transfer to a list fold: over an unordered set the value is
  well defined only because \<^const>‹sup› is commutative, associative, and
  idempotent.
›

definition aggregate_verdicts :: "contextual_verdict set ⇒ contextual_verdict" where
  "aggregate_verdicts vs = Finite_Set.fold sup Dead vs"

lemma aggregate_verdicts_code [code]:
  "aggregate_verdicts (set vs) = List.fold sup vs Dead"
proof -
  interpret ci: comp_fun_idem "sup :: contextual_verdict ⇒ _"
    by (rule comp_fun_idem_sup)
  show ?thesis unfolding aggregate_verdicts_def by (rule ci.fold_set_fold)
qed

lemma aggregate_verdicts_empty [simp]: "aggregate_verdicts {} = Dead"
  unfolding aggregate_verdicts_def by simp

lemma aggregate_verdicts_insert [simp]:
  "finite vs ⟹ aggregate_verdicts (insert v vs) = v ⊔ aggregate_verdicts vs"
proof -
  assume "finite vs"
  interpret ci: comp_fun_idem "sup :: contextual_verdict ⇒ _"
    by (rule comp_fun_idem_sup)
  show ?thesis
    unfolding aggregate_verdicts_def using ‹finite vs› by simp
qed

lemma sup_contextual_verdict_eq_Dead_iff [simp]:
  "(x ⊔ y = Dead) ⟷ x = Dead ∧ y = Dead"
  by (cases x; cases y) simp_all

text ‹The finiteness premise is not bookkeeping: \<^const>‹Finite_Set.fold› returns
  its identity on an infinite carrier, so an infinite set of observations
  aggregates to ‹Dead› whatever its members are, and only the left-to-right
  direction would survive without it.›

lemma aggregate_verdicts_eq_Dead_iff:
  assumes "finite vs"
  shows "aggregate_verdicts vs = Dead ⟷ (∀v ∈ vs. v = Dead)"
  using assms by (induction vs rule: finite_induct) simp_all

text ‹The opposite direction, for a report that has only one observation per
  check and therefore no dead case to distinguish: every entry is
  ‹Decided›. Deadness is not asserted either way --- such a report simply does
  not carry the channel that would express it.›

definition decided_report ::
  "check_report_entry list ⇒ (pp × exp × contextual_verdict) list" where
  "decided_report = map (λ(u, cnd, r). (u, cnd, Decided r))"

lemma length_decided_report [simp]: "length (decided_report rs) = length rs"
  unfolding decided_report_def by simp

subsection ‹Whole-program contextual check report›

text ‹
  The context-sensitive sibling of \<^const>‹classify_checks›: the same
  \<^const>‹EA_Check› traversal in the same \<^const>‹cfg_intra_list› order, but
  reading a \<^typ>‹('ctx, 'a) solved_table› instead of a single
  \<^typ>‹pp ⇒ 's› environment, and retaining one verdict per context covered
  at the checked node rather than collapsing them at construction time.
  ‹classify_checks_ctx_positions› below is the load-bearing consequence: the
  node and condition columns coincide with \<^const>‹classify_checks›'s, so a
  positional consumer pairing this report with the source's own check list
  stays aligned.

  The per-check observations are a set, not a list. \<^typ>‹'ctx› carries no
  ordering constraint --- \<^const>‹table_contexts› is a set for precisely that
  reason, and real context types such as interval vectors have no total
  order --- so no canonical list exists to produce. Nothing downstream needs
  one: \<^const>‹aggregate_verdicts› is order-independent by construction.
›

definition classify_checks_ctx ::
    "cfg ⇒ ('ctx, 'a) solved_table ⇒ (exp ⇒ 'a ⇒ check_result)
       ⇒ (pp × exp × ('ctx × contextual_verdict) set) list" where
  "classify_checks_ctx g r classify =
     map (λ(u, a, v). (u, ea_check_cond a,
            (λctx. (ctx, classify_point classify (ea_check_cond a) (lookup_table r u ctx)))
              ` table_contexts r u))
       (filter (λ(u, a, v). is_EA_Check a) (cfg_intra_list g))"

definition classify_checks_verdicts ::
    "cfg ⇒ ('ctx, 'a) solved_table ⇒ (exp ⇒ 'a ⇒ check_result)
       ⇒ (pp × exp × contextual_verdict) list" where
  "classify_checks_verdicts g r classify =
     map (λ(u, c, vs). (u, c, aggregate_verdicts (snd ` vs))) (classify_checks_ctx g r classify)"

lemma classify_checks_verdicts_proj [simp]:
  "map (λ(u, c, vs). (u, c, aggregate_verdicts (snd ` vs))) (classify_checks_ctx g r classify)
     = classify_checks_verdicts g r classify"
  unfolding classify_checks_verdicts_def by (rule refl)

lemma classify_checks_ctx_positions:
  "map (λ(u, c, vs). (u, c)) (classify_checks_ctx g r classify)
     = map (λ(u, c, res). (u, c)) (classify_checks g env classify')"
  unfolding classify_checks_ctx_def classify_checks_def
  by (simp add: comp_def case_prod_beta)

text ‹Membership unfolds to an \<^const>‹EA_Check› edge at the entry's own source
  node, with that node's whole context fan-out attached --- the same shape
  ‹classify_checks_mem_iff› gives the context-insensitive report.›

lemma classify_checks_ctx_mem_iff:
  assumes "finite (intra g)"
  shows "(v, c, vs) ∈ set (classify_checks_ctx g r classify)
     ⟷ (∃l tgt. (v, EA_Check l c, tgt) ∈ intra g)
         ∧ vs = (λctx. (ctx, classify_point classify c (lookup_table r v ctx))) ` table_contexts r v"
  unfolding classify_checks_ctx_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)

subsection ‹Contextual proved/refuted soundness›

text ‹
  The ‹Decided Check_Proved›/‹Decided Check_Refuted› analogues of
  ‹classify_checks_proved_sound›/‹classify_checks_refuted_sound›: an
  aggregated verdict of \<^term>‹Decided Check_Proved› forces every observation
  folded into it to be \<^const>‹Dead› or \<^term>‹Decided Check_Proved› --- never
  a disagreeing \<^term>‹Decided Check_Refuted› or \<^term>‹Decided Check_Unknown›,
  since either would collapse the join to \<^term>‹Decided Check_Unknown›
  instead. ‹Dead› observations contribute nothing and are filtered out at the
  call site, not here.
›

text ‹
  The order-theoretic route: every member of a finite set sits below the
  set's own fold-join (‹aggregate_verdicts_member_le›), a decided,
  non-‹Check_Unknown› aggregate already forces the set finite
  (‹aggregate_verdicts_decided_finite›, since an infinite carrier folds to the
  identity ‹Dead›), and sitting below such a verdict has only two shapes
  (‹contextual_verdict_le_Decided_iff›). Composing the three gives
  ‹aggregate_verdicts_decided_dest› directly, with no case-bash over the fold
  step: disagreement, from either side, could only have collapsed the join to
  \<^term>‹Decided Check_Unknown› instead.
›

lemma aggregate_verdicts_member_le:
  assumes "finite vs" and "v ∈ vs"
  shows "v ≤ aggregate_verdicts vs"
  using assms
  by (induction vs rule: finite_induct) (auto intro: order_trans sup_ge2)

lemma contextual_verdict_le_Decided_iff [simp]:
  assumes "r ≠ Check_Unknown"
  shows "v ≤ Decided r ⟷ v = Dead ∨ v = Decided r"
  using assms by (cases v; cases r) (simp_all add: less_eq_check_result_def)

lemma aggregate_verdicts_decided_finite:
  "aggregate_verdicts vs = Decided r ⟹ finite vs"
  by (rule ccontr) (simp add: aggregate_verdicts_def)

lemma aggregate_verdicts_decided_dest:
  assumes agg: "aggregate_verdicts vs = Decided r" and known: "r ≠ Check_Unknown"
  shows "∀v ∈ vs. v = Dead ∨ v = Decided r"
proof
  fix v
  assume "v ∈ vs"
  have "v ≤ aggregate_verdicts vs"
    using aggregate_verdicts_member_le[OF aggregate_verdicts_decided_finite[OF agg] ‹v ∈ vs›] .
  with agg known show "v = Dead ∨ v = Decided r" by simp
qed


subsection ‹One condition at one point, over its contexts›

text ‹
  The verdict a table gives a condition at a point: the classifier's verdict at
  every context the point was solved at, aggregated. A check and an arithmetic
  obligation are both read this way.
›

definition point_verdict ::
    "('ctx, 'a) solved_table ⇒ (exp ⇒ 'a ⇒ check_result) ⇒ pp ⇒ exp
       ⇒ contextual_verdict" where
  "point_verdict r classify v e =
     aggregate_verdicts
       ((λctx. classify_point classify e (lookup_table r v ctx)) ` table_contexts r v)"

text ‹
  A decided, non-‹Check_Unknown› point verdict is the classifier's own reading at
  every \<^const>‹Lifted› context of the point.
›

lemma point_verdict_decided:
  assumes agg: "point_verdict r classify v e = Decided res" and known: "res ≠ Check_Unknown"
    and look: "lookup_table r v ctx = Lifted st"
  shows "classify e st = res"
proof -
  have "classify_point classify e (lookup_table r v ctx)
          ∈ (λc. classify_point classify e (lookup_table r v c)) ` table_contexts r v"
    using lookup_table_LiftedD[OF look] by blast
  with aggregate_verdicts_decided_dest[OF agg[unfolded point_verdict_def] known] look
  show ?thesis by auto
qed

text ‹A point with a \<^const>‹Lifted› entry among finitely many contexts is not
  ‹Dead›.›

lemma point_verdict_not_dead:
  assumes fin: "finite (table_contexts r v)" and look: "lookup_table r v ctx = Lifted st"
  shows "point_verdict r classify v e ≠ Dead"
proof
  assume "point_verdict r classify v e = Dead"
  with fin have "∀x ∈ (λc. classify_point classify e (lookup_table r v c)) ` table_contexts r v.
                   x = Dead"
    unfolding point_verdict_def by (simp add: aggregate_verdicts_eq_Dead_iff)
  then have "classify_point classify e (lookup_table r v ctx) = Dead"
    using lookup_table_LiftedD[OF look] by blast
  with look show False by simp
qed

text ‹
  The context-indexed report analogue of ‹classify_checks_proved_sound›/
  ‹classify_checks_refuted_sound›, stated once for any decided,
  non-‹Check_Unknown› aggregate: it forces the classifier's own reading at
  every \<^const>‹Lifted› context to agree. The image set being folded is
  shown finite from the aggregate equation itself (‹Finite_Set.fold_infinite›:
  an infinite carrier folds to the identity ‹Dead›, which a decided,
  non-‹Check_Unknown› result already rules out), so no separate finiteness
  assumption on the covered contexts is needed.
›

lemma classify_checks_verdicts_mem_iff:
  assumes "finite (intra g)"
  shows "(v, c, vr) ∈ set (classify_checks_verdicts g ar classify)
     ⟷ (∃l tgt. (v, EA_Check l c, tgt) ∈ intra g)
         ∧ vr = aggregate_verdicts
                  ((λctx. classify_point classify c (lookup_table ar v ctx)) ` table_contexts ar v)"
proof -
  have img: "snd ` (λctx. (ctx, classify_point classify c (lookup_table ar v ctx)))
                 ` table_contexts ar v
           = (λctx. classify_point classify c (lookup_table ar v ctx)) ` table_contexts ar v"
    by (simp add: image_comp comp_def)
  have "(v, c, vr) ∈ set (classify_checks_verdicts g ar classify)
      ⟷ (∃vs. (v, c, vs) ∈ set (classify_checks_ctx g ar classify)
                 ∧ vr = aggregate_verdicts (snd ` vs))"
    unfolding classify_checks_verdicts_def set_map by (force simp: image_iff)
  also have "... ⟷ (∃l tgt. (v, EA_Check l c, tgt) ∈ intra g)
         ∧ vr = aggregate_verdicts
                  ((λctx. classify_point classify c (lookup_table ar v ctx)) ` table_contexts ar v)"
    unfolding classify_checks_ctx_mem_iff[OF assms] using img by auto
  finally show ?thesis .
qed

theorem classify_checks_ctx_decided_sound:
  assumes fin: "finite (intra g)"
    and mem: "(v, c, Decided r) ∈ set (classify_checks_verdicts g ar classify)"
    and reach: "lookup_table ar v ctx = Lifted st"
    and known: "r ≠ Check_Unknown"
  shows "classify c st = r"
proof -
  have "point_verdict ar classify v c = Decided r"
    using classify_checks_verdicts_mem_iff[OF fin, of v c "Decided r" ar classify] mem
    by (simp add: point_verdict_def)
  then show ?thesis by (rule point_verdict_decided[OF _ known reach])
qed

end