Theory Analysis_Run_Sound

theory Analysis_Run_Sound
  imports Analysis_Run
begin

section ‹What a configuration's table owes its report›

text ‹
  Every configuration hands the table its registration solved to
  \<^const>‹report_of›, which takes the check column from one call of
  \<^const>‹classify_checks_verdicts› and the diagnostics from one call of
  \<^const>‹arithmetic_diagnostics› over that table. So one argument serves every
  configuration.

  The argument asks two things of the table, bundled as ‹covered_table›. A
  store the program reaches at a point lies in the entry the table filed there under
  ∗‹some› context (‹table_covers›), and a point has finitely many contexts.
  Of the classifier it asks soundness in both directions (‹sound_classifier›),
  which does not depend on the table and is proved once for the combined state.
  Given both, the report built from the table is sound; the theory
  ‹Analysis_Report› states how. The context-free
  configuration's table is the instance at the end of this theory; the contextual
  ones follow in the theory after it.
›

subsection ‹Every check column is a contextual verdict report›

lemma finite_intra_prog_cfg [simp]: "finite (intra (prog_cfg p))"
  unfolding prog_cfg_def by (simp add: compile_prog_finite)

text ‹
  Forgetting the labels, the check column is the contextual verdict report itself.
›

lemma result_checks_of_verdicts:
  "map (λchk. (check_point chk, check_exp chk, check_verdict chk)) (result_checks_of g r classify)
     = classify_checks_verdicts g r classify"
  unfolding result_checks_of_def classify_checks_verdicts_def classify_checks_ctx_def
    point_verdict_def
  by (simp add: comp_def case_prod_beta image_image)

text ‹
  Where a result has checks: one per compiled \<^const>‹EA_Check› edge, at that edge's
  source node and with its label and condition, in the order the graph lists its edges.
›

definition check_sites :: "cfg ⇒ (pp × check_label × exp) list" where
  "check_sites g =
     map (λ(u, a, v). (u, ea_check_label a, ea_check_cond a))
       (filter (λ(u, a, v). is_EA_Check a) (cfg_intra_list g))"

lemma result_checks_of_sites:
  "map (λchk. (check_point chk, check_label chk, check_exp chk)) (result_checks_of g r classify)
     = check_sites g"
  unfolding result_checks_of_def check_sites_def
  by (simp add: comp_def case_prod_beta)

lemma check_sites_memI [intro]:
  assumes "finite (intra g)" and "(v, EA_Check l cnd, w) ∈ intra g"
  shows "(v, l, cnd) ∈ set (check_sites g)"
  using assms unfolding check_sites_def by force

subsection ‹A store that reaches a point sits in one of that point's contexts›

text ‹
  The table claim at a point is existential in the context: a store is described
  by the entry filed under ∗‹some› context the point was solved at --- one its
  own call history is admitted at --- and in general not by every such entry,
  since another activation's entry need not describe this store at all.
›

definition table_covers ::
    "('v ⇒ store set) ⇒ ('c, 'v) solved_table ⇒ pp ⇒ store ⇒ bool" where
  "table_covers gm r v s ⟷ (∃ctx st. lookup_table r v ctx = Lifted st ∧ s ∈ gm st)"

lemma table_coversI [intro]:
  "lookup_table r v ctx = Lifted st ⟹ s ∈ gm st ⟹ table_covers gm r v s"
  unfolding table_covers_def by blast

text ‹
  The published contextual soundness bounds one activation bucket by the table
  entry filed under that bucket's context. A caller holding a store knows only
  that the store reaches the point at all, so it needs the buckets to exhaust
  the point --- the union direction, which is where a context policy pays for
  being total. Both readings are settled in
  \<^theory>‹Voblint_CFG.Activation_Trace_Collect›: a functional policy has the union outright,
  a relational one --- such as the entry-state policy --- earns it from the
  existence of a context for every valid activation trace. \<^const>‹Bot› cannot be the entry
  found, since it concretizes to no store at all.
›

lemma lookup_table_covers_of_activation:
  fixes r :: "('c, 'v) solved_table"
  assumes union: "𝒞⇘𝒢,g,S⇙ v ⊆ (⋃c. 𝒜⇘𝒢,adm,rc,g,S⇙ v c)"
      and sound: "⋀ctx. 𝒜⇘𝒢,adm,rc,g,S⇙ v ctx
                    ⊆ gamma_lift gm (lookup_table r v ctx)"
      and mem: "s ∈ 𝒞⇘𝒢,g,S⇙ v"
  obtains ctx st where "s ∈ 𝒜⇘𝒢,adm,rc,g,S⇙ v ctx"
    and "lookup_table r v ctx = Lifted st" and "s ∈ gm st"
proof -
  from mem union obtain ctx where a: "s ∈ 𝒜⇘𝒢,adm,rc,g,S⇙ v ctx" by blast
  with sound have g: "s ∈ gamma_lift gm (lookup_table r v ctx)" by blast
  show ?thesis
  proof (cases "lookup_table r v ctx")
    case Bot
    with g show ?thesis by simp
  next
    case (Lifted st)
    with g a show ?thesis by (intro that [of ctx st]) simp_all
  qed
qed

subsection ‹The table contract and the classifier contract›

text ‹
  What a configuration's table has to satisfy for its report to be sound. Each
  configuration below and in the theory after this one is an instance of
  ‹covered_table›, and owes nothing but two facts: the table exhausts the
  reachable stores, over finitely many contexts per point. The classifier owes
  soundness in both directions (‹sound_classifier›); ‹sound_table› is the two
  together.
›

definition arithmetic_safe_at :: "cfg ⇒ pp ⇒ store ⇒ bool" where
  "arithmetic_safe_at g v s ⟷
     (∀es. (v, es) ∈ set (arithmetic_expression_sites g) ⟶
       (∀e ∈ set es. ∀divisor ∈ expression_divisors e. ⟦divisor⟧⇩e s ≠ 0))"

text ‹
  A solved table ‹r› covers program ‹p›: every store the collecting semantics
  reaches at ‹v› lies in ‹gm› of the state ‹r› holds at ‹v› in
  some context, and each point has finitely many contexts.
›
locale covered_table =
  fixes p :: imp_prog
    and r :: "('c, 'v) solved_table"
    and gm :: "'v ⇒ store set"
  assumes finite_contexts: "⋀v. finite (table_contexts r v)"
      and covers: "⋀v s. s ∈ 𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v
                      ⟹ table_covers gm r v s"

text ‹
  ‹classify› is sound for ‹gm›: ‹Check_Proved› means the condition holds at
  every store in ‹gm d›, ‹Check_Refuted› that it fails at every one.
›
locale sound_classifier =
  fixes classify :: "exp ⇒ 'v ⇒ check_result"
    and gm :: "'v ⇒ store set"
  assumes proved: "⋀cnd d t. classify cnd d = Check_Proved ⟹ t ∈ gm d
                      ⟹ truthy (⟦cnd⟧⇩e t)"
      and refuted: "⋀cnd d t. classify cnd d = Check_Refuted ⟹ t ∈ gm d
                      ⟹ ¬ truthy (⟦cnd⟧⇩e t)"

lemma mcp_sound_classifier: "sound_classifier (mcp_classify as) (mcp_gamma_v as)"
  by unfold_locales (fact mcp_classify_proved, fact mcp_classify_refuted)

text ‹
  A covered table read through a sound classifier. Inside it, verdicts and
  diagnostics computed from ‹r› hold at every collected store.
›
locale sound_table = covered_table p r gm + sound_classifier classify gm
  for p :: imp_prog and r :: "('c, 'v) solved_table"
    and classify :: "exp ⇒ 'v ⇒ check_result" and gm :: "'v ⇒ store set"
begin

text ‹
  A point the arithmetic diagnostics do not name is safe at every store the
  collecting semantics admits there: no divisor evaluated at it is zero.
›

lemma arithmetic_safe:
  assumes absent: "∀d ∈ set (arithmetic_diagnostics (prog_cfg p) r classify).
      diagnostic_point d ≠ v"
    and mem: "s ∈ 𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v"
  shows "arithmetic_safe_at (prog_cfg p) v s"
proof -
  from covers[OF mem] obtain ctx st where
    look: "lookup_table r v ctx = Lifted st" and gst: "s ∈ gm st"
    unfolding table_covers_def by blast
  have safe: "⋀es e divisor. (v, es) ∈ set (arithmetic_expression_sites (prog_cfg p)) ⟹
      e ∈ set es ⟹ divisor ∈ expression_divisors e ⟹ ⟦divisor⟧⇩e s ≠ 0"
  proof -
    fix es e divisor
    assume site: "(v, es) ∈ set (arithmetic_expression_sites (prog_cfg p))"
      and expr: "e ∈ set es" and div: "divisor ∈ expression_divisors e"
    obtain obligations obligation where
      obs: "(v, obligations) ∈ set (arithmetic_sites (prog_cfg p))"
      and ob: "obligation ∈ set obligations"
      and divisor: "arithmetic_divisor obligation = divisor"
      by (rule arithmetic_sites_divisor[OF site expr div])
    have verdict: "point_verdict r classify v (arithmetic_condition obligation)
                     = Lifted Check_Proved"
      using arithmetic_diagnostics_absent[OF obs ob absent]
        point_verdict_not_dead[OF finite_contexts look, of classify]
      by blast
    have classified: "classify (arithmetic_condition obligation) st = Check_Proved"
      by (rule point_verdict_decided[OF verdict _ look]) simp
    from proved[OF classified gst] show "⟦divisor⟧⇩e s ≠ 0"
      by (auto simp: arithmetic_condition_def divisor split: if_splits)
  qed
  show ?thesis unfolding arithmetic_safe_at_def using safe by blast
qed

end

text ‹
  The shape every registration publishes its soundness in, with its context policy
  ‹adm› and root context ‹rc›: every valid activation trace carries a context, and
  each activation bucket is bounded by the entry filed under its context. The
  buckets then exhaust the point, which is all a ‹covered_table› needs.
›

locale activation_table =
  fixes p :: imp_prog
    and r :: "('c, 'v) solved_table"
    and gm :: "'v ⇒ store set"
    and adm :: "'c context_policy"
    and rc :: 'c
  assumes has_context:
      "⋀t. t ∈ 𝒯⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙
         ⟹ ∃c. activation_context_rel (declared_global p) adm rc (prog_cfg p) t c"
    and bucket_bound:
      "⋀u ctx. 𝒜⇘declared_global p,adm,rc,prog_cfg p,cinit_stores (declared_global p)⇙ u ctx
         ⊆ gamma_lift gm (lookup_table r u ctx)"
    and finite_table: "finite_solved_table r"
begin

lemma covered: "covered_table p r gm"
proof (rule covered_table.intro)
  show "finite (table_contexts r v)" for v by (rule finite_table_contexts [OF finite_table])
  have union: "𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ u
                 ⊆ (⋃c. 𝒜⇘declared_global p,adm,rc,prog_cfg p,
                             cinit_stores (declared_global p)⇙ u c)" for u
    by (rule equalityD1 [OF node_collect_eq_Union_activation_of_has_context [OF has_context]])
  show "table_covers gm r v s"
    if "s ∈ 𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v"
    for v s
    by (meson lookup_table_covers_of_activation [OF union bucket_bound that] table_coversI)
qed

end

subsection ‹The context-free configuration›

text ‹
  The unit registration keys every activation at the one context ‹()›, a
  function of the call site and the caller's context, so the buckets exhaust a point
  outright and each is bounded by its entry.
›

lemma mcp_rule_table:
  assumes wf: "wf_program_compile_input p"
    and cov: "mcp_rule.terminates as r (declared_global p) p"
  shows "activation_table p (mcp_rule.result as r (declared_global p) p)
           (mcp_gamma_v (activation as)) (context_policy_of_fun (λu c t. ())) ()"
proof (rule activation_table.intro, goal_cases)
  case (1 t)
  show ?case
    by (rule exI, subst activation_context_rel_of_fun_iff [OF 1]) (rule refl)
next
  case (2 u ctx)
  show ?case
    using mcp_rule.fun_route_activation_collect_sound_of_terminates [OF _ wf cov]
    unfolding mcp_rule.gamma_reader_eq_lookup by (simp add: route_unit_def)
next
  case 3
  show ?case
    using mcp_rule.vars_finite_of_terminates [OF cov]
    by (simp add: finite_solved_table_def dg_pipeline.result_def
        dg_pipeline.sol_vars_def)
qed

text ‹The same with program globals on the shared channel.›

lemma mcp_split_rule_table:
  assumes wf: "wf_program_compile_input p"
    and cov: "mcp_split_rule.terminates as r (declared_global p) p"
  shows "activation_table p (mcp_split_rule.result as r (declared_global p) p)
           (mcp_gamma_v (activation as)) (context_policy_of_fun (λu c t. ())) ()"
proof (rule activation_table.intro, goal_cases)
  case (1 t)
  show ?case
    by (rule exI, subst activation_context_rel_of_fun_iff [OF 1]) (rule refl)
next
  case (2 u ctx)
  show ?case
    using mcp_split_rule.fun_route_activation_collect_sound_of_terminates [OF _ wf cov]
    unfolding mcp_split_rule.gamma_reader_eq_lookup by (simp add: route_unit_def)
next
  case 3
  show ?case
    using mcp_split_rule.vars_finite_of_terminates [OF cov]
    by (simp add: finite_solved_table_def dg_pipeline.result_def
        dg_pipeline.sol_vars_def)
qed

end