Theory DG_Spec_Sound

theory DG_Spec_Sound
  imports DG_Spec "Voblint_CFG.CFG_Transfer"
begin

section ‹What a manager-native specification owes a concretization›

text ‹
  Soundness of a manager-native ‹dg_spec› relates its returned local value
  to an environment of analysis-visible globals. The manager maps each global
  name to a solver key; ‹genv› reads the global component at those keys.

  A transfer starts in the input environment and establishes its result in
  that environment joined pointwise with its publications. Unchanged globals
  therefore retain their meaning without being republished. A specification
  may read and publish several names, all interpreted by the same environment.
  Concretizations that ignore globals discharge the global obligations
  vacuously. The unit-name compatibility lemma retains the older sufficient
  condition that publications alone describe the resulting global state.
›

text ‹
  What a call's alternatives must establish. The coverage contract is the part
  that does not mention a strategy program: ‹enter_runs› and ‹enter_deps› below do describe
  an entry program and the continuations it is handed, but what an alternative
  ∗‹means› is settled here, before any of that.
  ‹pairs› covers a concrete caller when ∗‹some› alternative accounts for it: the
  caller store lies in the continuation half and the store the callee starts
  from lies in the entry half, in the same pair. The quantifier is existential
  because alternatives are a disjunction --- a call that splits into two of them
  has each covering the concrete runs it was computed for, and demanding that
  every alternative cover every caller would defeat the splitting the list
  exists to express.

  Keeping it separate from any particular program is what lets an entry
  obligation be discharged once and reused: a proof about how alternatives are
  folded never has to restate what an alternative means.
›

definition entry_pairs_cover ::
  "('D ⇒ 's set) ⇒ 's ⇒ 's ⇒ 'D enter_result list ⇒ bool"
where
  "entry_pairs_cover gammaD caller entered pairs ⟷
     (∃cont entry. (cont, entry) ∈ set pairs
        ∧ caller ∈ gammaD cont ∧ entered ∈ gammaD entry)"

lemma entry_pairs_coverI [intro]:
  assumes "(cont, entry) ∈ set pairs"
    and "caller ∈ gammaD cont" and "entered ∈ gammaD entry"
  shows "entry_pairs_cover gammaD caller entered pairs"
  using assms unfolding entry_pairs_cover_def by blast

lemma entry_pairs_coverE [elim]:
  assumes "entry_pairs_cover gammaD caller entered pairs"
  obtains cont entry
    where "(cont, entry) ∈ set pairs"
      and "caller ∈ gammaD cont" and "entered ∈ gammaD entry"
  using assms unfolding entry_pairs_cover_def by blast

lemma entry_pairs_cover_Nil [simp]:
  "¬ entry_pairs_cover gammaD caller entered []"
  by (simp add: entry_pairs_cover_def)

text ‹
  An entry transfer is a program, so its alternatives cannot be read back out of
  it: the tree it builds answers into the solver's carrier, and a list of pairs
  does not live there. What ∗‹can› be said is how it behaves under a fixed
  solution. ‹enter_runs T m sigma pairs pub› says that under ‹sigma› the program
  hands its continuation exactly ‹pairs› and publishes exactly ‹pub› on the way,
  whatever the continuation then does --- the reads resolve against ‹sigma›, so
  both are determined before any continuation is chosen.

  This is what lets a proof name an alternative. Rather than extracting the list
  after the fact, a caller fixes the ‹pairs› the continuation receives and
  reasons under that, which is the ordinary way to reason about a
  continuation-passing program. ‹pub› is carried separately because the prefix's
  own publications are part of what the call establishes: an entry that reads a
  global and republishes it has those contributions in ‹pub›, not in anything
  the continuation returns.
›

definition enter_runs ::
  "('x,'k,'v,'D::bounded_semilattice_sup_bot,'G::bounded_semilattice_sup_bot) man_enter_transfer
   ⇒ ('x,'k,'v,'D,'G) man ⇒ ('x + 'k ⇒ ('D,'G) dg_state)
   ⇒ 'D enter_result list ⇒ ('x + 'k ⇒ ('D,'G) dg_state) ⇒ bool"
where
  "enter_runs T m sigma pairs pub ⟷
     (∀K. traverse_rhs (T m K) sigma = traverse_rhs (K pairs) sigma
          ∧ sides_of_rhs (T m K) sigma = pub ⊔ sides_of_rhs (K pairs) sigma)"

lemma enter_runsD_traverse:
  assumes "enter_runs T m sigma pairs pub"
  shows "traverse_rhs (T m K) sigma = traverse_rhs (K pairs) sigma"
  using assms unfolding enter_runs_def by blast

lemma enter_runsD_sides:
  assumes "enter_runs T m sigma pairs pub"
  shows "sides_of_rhs (T m K) sigma = pub ⊔ sides_of_rhs (K pairs) sigma"
  using assms unfolding enter_runs_def by blast

text ‹A pure entry hands over its alternatives directly and publishes nothing.›

lemma enter_runs_local_enter_transfer [intro]:
  "enter_runs (local_enter_transfer f) m sigma (f (man_local m)) bot"
  by (simp add: enter_runs_def local_enter_transfer_def sp_return_def
      sup_fun_def bot_fun_def)

text ‹The same at a built manager, where \<^const>‹man_local› has already been
  read off. A caller whose alternatives are written out as a list --- which is
  how every routed instance states its entry obligation --- matches this one by
  ordinary unification, where the rule above would first have to reduce
  ‹man_local (mk_dg_man d key)› under a higher-order variable.›

lemma enter_runs_local_enter_transfer_mk_dg_man [intro]:
  "enter_runs (local_enter_transfer f) (mk_dg_man d unknown_of) sigma (f d) bot"
  using enter_runs_local_enter_transfer[of f "mk_dg_man d unknown_of" sigma] by simp

text ‹The converse direction, which a consumer needs when it has an arbitrary run
  in hand rather than the one above: a pure entry's publication is pinned, so no
  case analysis on the run is possible.›

lemma enter_runs_local_pub_bot:
  assumes "enter_runs (local_enter_transfer f) m sigma pairs pub"
  shows "pub = bot"
proof -
  have "sides_of_rhs (local_enter_transfer f m (λ_. Answer bot)) sigma
          = pub ⊔ sides_of_rhs (Answer bot) sigma"
    using assms by (rule enter_runsD_sides)
  then show ?thesis
    by (simp add: local_enter_transfer_def sp_return_def fun_eq_iff sup_fun_def bot_fun_def)
qed

text ‹
  Values and publications are not everything the generator needs to know about
  an entry program: what it ∗‹reads› matters too, and reading is invisible in
  both. An entry that consults a global depends on that unknown even when it
  publishes ‹bot› there, and the solver's admissibility arguments are stated
  over dependencies, not over answers.

  ‹enter_deps› is deliberately a separate relation over the ∗‹same› ‹pairs›: a
  proof that obtained its alternatives from \<^const>‹enter_runs› and its
  dependencies from an independently quantified list would be talking about two
  different executions. Packaging the two together, with
  \<^const>‹entry_pairs_cover›, is what keeps one call's story single.
›

definition enter_deps ::
  "('x,'k,'v,'D::bounded_semilattice_sup_bot,'G::bounded_semilattice_sup_bot) man_enter_transfer
   ⇒ ('x,'k,'v,'D,'G) man ⇒ ('x + 'k ⇒ ('D,'G) dg_state)
   ⇒ 'D enter_result list ⇒ ('x + 'k) set ⇒ bool"
where
  "enter_deps T m sigma pairs deps ⟷
     (∀K. dep_aux sigma (T m K) = deps ∪ dep_aux sigma (K pairs))"

lemma enter_depsD:
  assumes "enter_deps T m sigma pairs deps"
  shows "dep_aux sigma (T m K) = deps ∪ dep_aux sigma (K pairs)"
  using assms unfolding enter_deps_def by blast

text ‹A pure entry reads nothing of its own.›

lemma enter_deps_local_enter_transfer [intro]:
  "enter_deps (local_enter_transfer f) m sigma (f (man_local m)) {}"
  by (simp add: enter_deps_def local_enter_transfer_def sp_return_def)

lemma enter_deps_local_enter_transfer_mk_dg_man [intro]:
  "enter_deps (local_enter_transfer f) (mk_dg_man d unknown_of) sigma (f d) {}"
  using enter_deps_local_enter_transfer[of f "mk_dg_man d unknown_of" sigma] by simp

text ‹
  The analysis contract carries everything that is independent of how a call is compiled:
  the ordinary edge transfers and the return combine. Entry is not here. A
  \<^const>‹dgs_enter› answers a list, which is not an equation's answer, so what
  makes it sound is a property of the program the routed generator builds from
  it, stated through \<^const>‹entry_pairs_cover› against the routed alternative
  the solved system actually selects --- a property this locale alone cannot
  state, since it never mentions how a call compiles.

  So ‹analysis_contract› is the entry-independent part and not a complete soundness
  statement: interpreting it alone leaves a call's entry entirely unconstrained.
  ‹routed_context› (‹Routed_Context›, downstream in this session) is
  the complete statement, extending this contract with that entry obligation for
  the routed equation shape, and is what an analysis should be asked to
  establish.
›

subsection ‹Proof-level compiled combine form›

text ‹
  A return combine compiled the way an edge transfer is: read the caller
  continuation and the callee exit from two unknowns, and run the composed
  combine against them. No generator builds this. The routed call program already
  holds the alternative's own continuation, so it runs
  \<^const>‹dg_spec_combine_transfer› against that value directly and never reads
  a caller unknown a second time.

  It lives here, ahead of the locale that consumes it, because ∗‹stating›
  the return obligation at a pair of addresses is all it is for: a proof that
  quantifies over the pair needs a program to quantify over. Reading it in
  \<^theory>‹Voblint_Framework.DG_Spec›, among the formers a generator really
  does build, invited exactly the wrong conclusion.

  Both levels earn their place, which is why there are two of them.
  ‹combine_transfer_program› is used at an arbitrary
  \<^type>‹man_combine_transfer› --- by the ownership-split observation
  equations in ‹DG_Ownership_Split_Spec›, and by the relational domain's --- while
  ‹dg_spec_combine_program› is used at a selected specification, by
  ‹combine_sound_program› below, which restates the return obligation at
  two ∗‹solver addresses›. That is what the value form cannot express: a
  caller bounding the program from a post-solution reads it at two unknowns,
  so the obligation has to name the addresses, not the values they hold. ‹combine_program_at› is the one internal step, kept for symmetry
  with the edge driver rather than for a second consumer.
›

definition combine_program_at ::
  "('x,'k,'v,'dl,'dg) man_combine_transfer
   ⇒ 'x + 'k ⇒ 'x + 'k ⇒ ('v ⇒ 'k)
   ⇒ ('x,'k,('dl::bot,'dg) dg_state,'dl) strategy_program"
where
  "combine_program_at transfer src_cc src_ex unknown_of =
     do {
       dc ← dg_read_at src_cc;
       de ← dg_read_at src_ex;
       transfer (mk_dg_man dc unknown_of) de
     }"

definition combine_transfer_program ::
  "('x,'k,'v,'dl::bot,'dg::bot) man_combine_transfer ⇒ 'x + 'k ⇒ 'x + 'k ⇒ ('v ⇒ 'k)
   ⇒ ('x,'k,('dl,'dg) dg_state,('dl,'dg) dg_state) strategy_program"
where
  "combine_transfer_program T src_cc src_ex unknown_of =
     sp_map (λd. DG d ⊥) (combine_program_at T src_cc src_ex unknown_of)"

definition dg_spec_combine_program ::
  "('x,'k,'v,'dl::bot,'dg::bot) dg_spec ⇒ call_info ⇒ 'x + 'k ⇒ 'x + 'k ⇒ ('v ⇒ 'k)
   ⇒ ('x,'k,('dl,'dg) dg_state,('dl,'dg) dg_state) strategy_program"
where
  "dg_spec_combine_program S ci src_cc src_ex unknown_of =
     combine_transfer_program (dg_spec_combine_transfer S ci) src_cc src_ex unknown_of"

text ‹
  What compilation costs an observation here: the two source reads, and then
  the composed combine run at the values they produced. The counterpart of
  \<^theory>‹Voblint_Framework.DG_Spec›'s edge bridges, and untagged for the same
  reason.
›

lemma traverse_combine_transfer_program:
  "traverse_program (combine_transfer_program T src_cc src_ex unknown_of) τ
     = traverse_rhs (sp_compile_with (λd. DG d ⊥)
         (T (mk_dg_man (dg_local (τ src_cc)) unknown_of) (dg_local (τ src_ex)))) τ"
  by (simp add: combine_transfer_program_def combine_program_at_def sp_compile_with_def
      sp_bind_def)

lemma sides_combine_transfer_program:
  "sides_of_program (combine_transfer_program T src_cc src_ex unknown_of) τ
     = sides_of_rhs (sp_compile_with (λd. DG d ⊥)
         (T (mk_dg_man (dg_local (τ src_cc)) unknown_of) (dg_local (τ src_ex)))) τ"
  by (simp add: combine_transfer_program_def combine_program_at_def sp_compile_with_def
      sp_bind_def)

lemma dep_combine_transfer_program:
  "dep_program τ (combine_transfer_program T src_cc src_ex unknown_of)
     = insert src_cc (insert src_ex
         (dep_aux τ (sp_compile_with (λd. DG d ⊥)
            (T (mk_dg_man (dg_local (τ src_cc)) unknown_of) (dg_local (τ src_ex))))))"
  by (simp add: combine_transfer_program_def combine_program_at_def sp_compile_with_def
      sp_bind_def)

text ‹What the compiled form observes when both stages are local --- the combine
  counterparts of the edge-tree facts in \<^theory>‹Voblint_Framework.DG_Spec›.›

lemma traverse_local_combine_program [simp]:
  "traverse_program (combine_transfer_program (local_combine_transfer h) src_cc src_ex gk) τ
     = DG (h (dg_local (τ src_cc)) (dg_local (τ src_ex))) bot"
  by (simp add: traverse_combine_transfer_program local_combine_transfer_def
      sp_compile_with_def sp_return_def)

lemma sides_local_combine_program [simp]:
  "sides_of_program (combine_transfer_program (local_combine_transfer h) src_cc src_ex gk) τ k
     = bot"
  by (simp add: sides_combine_transfer_program local_combine_transfer_def
      sp_compile_with_def sp_return_def)

lemma dep_local_combine_program [simp]:
  "dep_program τ (combine_transfer_program (local_combine_transfer h) src_cc src_ex gk)
     = {src_cc, src_ex}"
  by (simp add: dep_combine_transfer_program local_combine_transfer_def
      sp_compile_with_def sp_return_def)

subsection ‹What a manager-native specification owes›

text ‹
  A specification names its global facts by ‹'v›, and a key map places each name at
  a solver unknown. The global environment a valuation holds under a key map is what
  it holds at those unknowns; the same reading of a program's side-effects is the
  environment the program publishes.
›

definition genv :: "('v ⇒ 'k) ⇒ ('x + 'k ⇒ ('dl, 'dg) dg_state) ⇒ 'v ⇒ 'dg" where
  "genv key τ v = dg_global (τ (Inr (key v)))"

text ‹Applied to a name, the environment is the lookup it stands for.›

declare genv_def [simp]

text ‹Every name at one key reads one value: the environment of a single slot.›

lemma genv_const [simp]: "genv (λ_. k) τ = (λ_. dg_global (τ (Inr k)))"
  by (simp add: fun_eq_iff)

text ‹What an edge's compiled program answers under ‹τ›: its local result and the
  global environment its side-effects publish. The combine counterparts run the
  composed combine at a continuation ‹dc› and a callee exit ‹de›.›

abbreviation edge_out where
  "edge_out S a src key τ ≡ dg_local (traverse_program (dg_spec_edge_program S a src key) τ)"

abbreviation edge_pub where
  "edge_pub S a src key τ ≡ genv key (sides_of_program (dg_spec_edge_program S a src key) τ)"

abbreviation combine_out where
  "combine_out S ci key dc de τ ≡
     dg_local (traverse_rhs (sp_compile_with (λd. DG d ⊥)
       (dg_spec_combine_transfer S ci (mk_dg_man dc key) de)) τ)"

abbreviation combine_pub where
  "combine_pub S ci key dc de τ ≡
     genv key (sides_of_rhs (sp_compile_with (λd. DG d ⊥)
       (dg_spec_combine_transfer S ci (mk_dg_man dc key) de)) τ)"

text ‹The contract a specification signs: its concretization is monotone, an edge's program
  over-approximates the concrete edge step, and its combine over-approximates the concrete
  return. Both obligations read the globals from the environment the valuation holds, and
  describe the result against that environment joined with what the program publishes:
  a global the step does not write is still what was read, so a step owes no
  publication for it.›
locale analysis_contract =
  fixes S :: "('x,'k,'v,'D::bounded_semilattice_sup_bot,
                'G::bounded_semilattice_sup_bot) dg_spec"
    and γ⇩D⇩G :: "'D ⇒ ('v ⇒ 'G) ⇒ store set"
    and 𝒢 :: "vname ⇒ bool"
  assumes spec_wf: "dg_spec_wf S"
    and gammaDG_mono:
      "⟦d ≤ d'; e ≤ e'⟧ ⟹ γ⇩D⇩G d e ⊆ γ⇩D⇩G d' e'"
    and step_sound:
      "edge_collect a (γ⇩D⇩G (dg_local (τ src)) (genv key τ))
         ⊆ γ⇩D⇩G (edge_out S a src key τ) (genv key τ ⊔ edge_pub S a src key τ)"
    and combine_sound:
      "⟦s ∈ γ⇩D⇩G q (genv key τ); t ∈ γ⇩D⇩G r (genv key τ)⟧ ⟹
        combine_collect 𝒢 (ci_dst ci) s t
          ∈ γ⇩D⇩G (combine_out S ci key q r τ) (genv key τ ⊔ combine_pub S ci key q r τ)"

text ‹
  The obligation is stated at ∗‹values› rather than at two unknown reads,
  because the routed call boundary applies combine at the continuation the
  entry produced, which is not in general what any unknown holds. Where the
  continuation ∗‹is› the caller's own solved value --- the monovariant call
  shape --- the tree form below is the instance at that value, so nothing is
  lost for a generator that reads both sides from unknowns.
›

lemma (in analysis_contract) combine_sound_program:
  assumes sc: "s ∈ γ⇩D⇩G (dg_local (τ src_cc)) (genv key τ)"
    and se: "t ∈ γ⇩D⇩G (dg_local (τ src_ex)) (genv key τ)"
  shows "combine_collect 𝒢 (ci_dst ci) s t
          ∈ γ⇩D⇩G (dg_local (traverse_program (dg_spec_combine_program S ci src_cc src_ex key) τ))
              (genv key τ ⊔ genv key (sides_of_program (dg_spec_combine_program S ci src_cc src_ex key) τ))"
  using combine_sound[where q = "dg_local (τ src_cc)" and r = "dg_local (τ src_ex)"
      and τ = τ and key = key and ci = ci, OF sc se]
  by (simp add: dg_spec_combine_program_def traverse_combine_transfer_program
      sides_combine_transfer_program)

text ‹
  A specification with a single global fact owes the contract at the environment that
  holds it. The stricter obligations below, which describe the result against what the
  program publishes alone, imply it, because the published value lies below its join
  with the one read.
›

lemma analysis_contract_unitI:
  fixes S :: "('x,'k,unit,'D::bounded_semilattice_sup_bot,
                'G::bounded_semilattice_sup_bot) dg_spec"
    and gm :: "'D ⇒ 'G ⇒ store set"
  assumes wf: "dg_spec_wf S"
    and mono: "⋀d d' g g'. ⟦d ≤ d'; g ≤ g'⟧ ⟹ gm d g ⊆ gm d' g'"
    and step: "⋀a τ src gk.
      edge_collect a (gm (dg_local (τ src)) (dg_global (τ (Inr gk))))
        ⊆ gm (edge_out S a src (λ_. gk) τ)
            (dg_global (sides_of_program (dg_spec_edge_program S a src (λ_. gk)) τ (Inr gk)))"
    and comb: "⋀s τ dc gk t de ci.
      ⟦s ∈ gm dc (dg_global (τ (Inr gk))); t ∈ gm de (dg_global (τ (Inr gk)))⟧ ⟹
        combine_collect 𝒢 (ci_dst ci) s t
          ∈ gm (combine_out S ci (λ_. gk) dc de τ)
              (dg_global (sides_of_rhs (sp_compile_with (λd. DG d ⊥)
                 (dg_spec_combine_transfer S ci (mk_dg_man dc (λ_. gk)) de)) τ (Inr gk)))"
  shows "analysis_contract S (λd e. gm d (e ())) 𝒢"
proof
  show "dg_spec_wf S" by (rule wf)
next
  fix d d' :: 'D and e e' :: "unit ⇒ 'G"
  assume "d ≤ d'" "e ≤ e'"
  then show "gm d (e ()) ⊆ gm d' (e' ())" by (simp add: mono le_funD)
next
  fix a τ src and key :: "unit ⇒ 'k"
  have key: "key = (λ_. key ())" by (rule ext) simp
  have "edge_collect a (gm (dg_local (τ src)) (genv key τ ()))
          ⊆ gm (edge_out S a src key τ) (edge_pub S a src key τ ())"
    using step[of a τ src "key ()"] by (subst (1 2 3) key) (simp add: genv_def)
  also have "… ⊆ gm (edge_out S a src key τ) ((genv key τ ⊔ edge_pub S a src key τ) ())"
    by (rule mono) simp_all
  finally show "edge_collect a (gm (dg_local (τ src)) (genv key τ ()))
          ⊆ gm (edge_out S a src key τ) ((genv key τ ⊔ edge_pub S a src key τ) ())" .
next
  fix s dc t de ci and key :: "unit ⇒ 'k" and τ :: "'x + 'k ⇒ ('D, 'G) dg_state"
  assume s: "s ∈ gm dc (genv key τ ())" and t: "t ∈ gm de (genv key τ ())"
  have key: "key = (λ_. key ())" by (rule ext) simp
  have "combine_collect 𝒢 (ci_dst ci) s t
          ∈ gm (combine_out S ci key dc de τ) (combine_pub S ci key dc de τ ())"
    using comb[of s dc τ "key ()" t de ci] s t by (subst (1 2 3) key) (simp add: genv_def)
  then show "combine_collect 𝒢 (ci_dst ci) s t
          ∈ gm (combine_out S ci key dc de τ) ((genv key τ ⊔ combine_pub S ci key dc de τ) ())"
    by (rule subsetD[OF mono, rotated 2]) simp_all
qed

end