Theory Routed_Call_Programs

theory Routed_Call_Programs
  imports DG_Spec_Sound DG_Indexed_Generator
    "Voblint_Domain.Nonrelational_State"
begin

section ‹The equations one call action generates›

text ‹
  What a routed call is, as solver input, before anything is claimed about its
  soundness. Each callee a call action resolves to becomes one strategy program:
  it runs the specification's entry transfer on the caller's local value,
  chooses the callee's context from the entry half of the alternative that
  produced, publishes that entered state at a global proxy key --- an
  ∗‹activation seed›, the only channel by which the entered state reaches
  the callee's entry unknown --- reads the callee's exit back at that same
  context, and runs the specification's combine against the alternative's
  continuation half. The publication only joins into the seed and destabilizes
  its readers; the exit read is the query that makes the solver evaluate the
  callee at that context.
  The other half of the protocol is the callee's own entry equation reading its
  seed slot back: that is ‹routed_entry_seed_programs›.

  This theory is construction and observation only: which unknowns a program
  reads, which keys it publishes to, and lower bounds on what it contributes
  at each. Whether those contributions are sound is ‹Routed_Context›'s
  question, which fixes the shape built here as ‹cmb› and ‹extra› and
  discharges CALL and COMB against it once.
›


subsection ‹The routed key space›

datatype ('v,'c) global_unknown =
  Analysis_Buffer
| Analysis_Global 'v
| Activation_Seed (seed_pp: pp) (seed_ctx: 'c)

text ‹
  The solver's global unknowns have three owners. The generator uses
  \<^const>‹Analysis_Buffer› for a node's buffered global answer. \<^const>‹Analysis_Global› wraps a name of
  the analysis's own type ‹'v› --- Goblint's ‹V› --- and is the only kind an
  analysis can reach, through \<^const>‹man_global›/\<^const>‹man_sideg›.
  \<^const>‹Activation_Seed› holds the entry state published at a callee's
  activation, keyed by the callee entry point and the routed context.

  The remaining constructors separate analysis effects from activation routing. ‹Analysis_Global› embeds this
  development's analogue of Goblint's ‹Spec.V› into the solver's global-key
  space --- the namespace itself is ‹'v›, and this constructor is the address
  around it. Goblint's own Base analysis supplies a non-trivial one
  (privatization globals, thread-return globals) rather than a single global
  cell. ‹Activation_Seed› is not Goblint's --- their
  framework records reachable contexts on a separate global whose value is a
  set of contexts, keyed by function. It is a solver adapter, not the
  translation of any Goblint constraint constructor: the vendored solver
  publishes to global keys only, so the one way to hand a callee's entry
  unknown a value is to publish at a global proxy that the entry equation reads
  back. Publication does not demand the callee; the caller's read of the
  callee's exit does. It is named to say so, so that no later reader takes it
  for a Goblint correspondence.

  The types keep the two apart. A transfer names a global as a ‹'v› and never
  builds a key, because \<^const>‹mk_dg_man› holds the embedding; only the routing
  and generator layers apply \<^const>‹Activation_Seed›. Every routed context
  instantiates ‹'c› (call strings at \<^typ>‹cfg_node list›, entry states at a
  value list, context-insensitive at \<^typ>‹unit› --- which is exactly Goblint's
  own ‹C = Printable.Unit›), and an analysis with one global takes ‹'v = unit›.
›

lemma activation_seed_ne_analysis_global [simp]:
  "Activation_Seed u c ≠ Analysis_Global v"
  "Analysis_Global v ≠ Activation_Seed u c"
  by simp_all

subsection ‹The canonical routed entry-seed publication and return combine›

text ‹
  The routing combine reads the caller under its own context, the callee exit under the
  context ‹route› selects from the callee's entered value --- the alternative's own
  second component, after ‹enter⇧♯› has run --- and the exact matched
  \<^typ>‹call_action› (from \<^const>‹return_call_action_list›, never re-derived from
  the call site's outgoing edges). The spec's own enter and combine transfers run as
  compiled manager programs over the caller value, so whether the global slot ‹buffer_key›
  is read or published at all is the specification's business: a Base-style spec's
  transfers touch no global and the routed program then carries no ‹buffer_key› effect either,
  while an effectful spec's own ‹man_global›/‹man_sideg› calls ride inside the
  compiled subtrees.

  Parameter order matches ‹dg_context_activation›'s ‹cmb› calling
  convention: the generator supplies ‹route› as ‹cmb›'s own first argument
  (‹cmb route c ca cc ex› in \<^const>‹routed_node_rhs›), so
  ‹routed_call_program S global_of seed›, closing over the spec, the shared slot, and the
  seed-key injection, is the value that instantiates ‹cmb›.

  This program owns the whole call lifecycle for one call action: it reads the caller once,
  routes the callee context once (‹ctx'›), and shares that one ‹ctx'› between the
  entry-seed publication and the combine's callee-exit read. The publication hands
  the callee's entry its value, and the exit read, a \<^const>‹QueryL› of the callee's
  \<^const>‹FunctionResult› node at ‹ctx'›, is what makes the solver evaluate
  the callee; both happen in the one equation that combines the result, so
  ‹enter#› runs exactly once per call action rather than once per hook. The caller
  continuation is not reconstructed here: it is handed to
  \<^const>‹dg_spec_combine_transfer› as the manager's own local value, and that
  pipeline runs ‹combine_env⇧♯› and ‹combine_assign⇧♯› over it,
  so this layer only chooses addresses and keys. Only the half that
  cannot move stays with ‹routed_entry_seed_programs›: a callee's own entry equation is the one
  place that can read its own seed slot back. ‹route› is kept as a parameter of that
  hook purely to match ‹dg_context_activation›'s ‹extra› calling
  convention, which always supplies it.

  The seed channel is ‹'D›-typed, so ‹'D› and ‹'G› stay independent. The
  publication writes the callee's freshly entered local state --- a ‹'D›-typed value
  --- into the ‹dg_local› half of the \<^type>‹dg_state› published at the seed key. A
  \<^type>‹dg_state› already carries both fields at every key regardless of whether the
  key is reached through ‹Inl› (a ‹(pp, 'c)› local unknown) or ‹Inr› (a ‹'k›
  global unknown): ‹dg_local›/‹dg_global› are call-site conventions, not something
  \<^const>‹QueryL›/\<^const>‹QueryG› themselves enforce. Since ‹seed p ctx› is
  always distinct from ‹buffer_key› (‹seed_ne_buffer_key›) and no other equation ever
  publishes to a seed key, nothing else reads or writes that key's ‹dg_local› half.
›

text ‹
  One resolved callee: enter the frame through the spec's compiled enter transfer,
  key the entered state, publish it at the routed seed, read that activation's exit
  back and run the spec's composed combine. The caller's local state is passed in
  rather than read here, because the call site reads it once and every target it
  resolves to is entered from that same value.
›

text ‹
  What one call alternative contributes. The continuation and the callee-entry
  value arrive together, from a single run of the specification's entry, and
  this is where they are used together: the entry half chooses the context and
  is published at that context's seed, and the continuation half is the local
  value the return combine runs against. Neither is recoverable from the other,
  which is why the pair travels this far intact.

  Naming it separately is what lets the bounds below speak about ∗‹one›
  alternative: the program the generator builds is a fold over these, so every
  obligation about a selected alternative is a statement about one element of
  that fold rather than about the fold itself.
›

definition routed_call_alternative_program ::
  "(pp × 'c, 'k, 'v, 'D::bounded_semilattice_sup_bot,
     'G::bounded_semilattice_sup_bot) dg_spec ⇒ ('v ⇒ 'k)
   ⇒ (pp ⇒ 'c ⇒ 'k)
   ⇒ (pp ⇒ 'c ⇒ 'D ⇒ call_action ⇒ 'c)
   ⇒ ('D ⇒ bool)
   ⇒ 'c ⇒ call_action ⇒ pp ⇒ pname ⇒ 'D enter_result
   ⇒ (pp × 'c, 'k, ('D, 'G) dg_state, ('D, 'G) dg_state) strategy_program"
where
  "routed_call_alternative_program S global_of seed route is_bot ctx ca cc p alt =
     (case alt of (cont, entry) ⇒
        (if is_bot entry
         then sp_map (λd. DG d bot)
                (dg_spec_combine_transfer S (call_info_of ca p)
                  (mk_dg_man cont global_of) bot)
         else
           (let ctx' = route cc ctx entry ca
            in do {
                 _ ← sp_publish (seed (FunctionEntry p) ctx') (DG entry bot);
                 callee_state ← sp_read_local (FunctionResult p, ctx');
                 sp_map (λd. DG d bot)
                   (dg_spec_combine_transfer S (call_info_of ca p)
                     (mk_dg_man cont global_of)
                     (dg_local callee_state))
               })))"

text ‹
  Deliberately not a ‹simp› rule: it expands into a \<^const>‹Side› over a
  \<^const>‹QueryL› over a compiled combine, and letting that fire everywhere
  would put a whole call boundary into every goal mentioning the constant.
  The observation lemmas below cite it where they need it.
›

lemma routed_call_alternative_program_bot [simp]:
  assumes "is_bot entry"
  shows "routed_call_alternative_program S global_of seed route is_bot ctx ca cc p (cont, entry)
           = sp_map (λd. DG d bot)
               (dg_spec_combine_transfer S (call_info_of ca p)
                 (mk_dg_man cont global_of) bot)"
  using assms by (simp add: routed_call_alternative_program_def)

lemma routed_call_alternative_program_nonbot [simp]:
  assumes "¬ is_bot entry"
  shows "routed_call_alternative_program S global_of seed route is_bot ctx ca cc p (cont, entry)
     = do {
         _ ← sp_publish (seed (FunctionEntry p) (route cc ctx entry ca)) (DG entry bot);
         callee_state ← sp_read_local (FunctionResult p, route cc ctx entry ca);
         sp_map (λd. DG d bot)
           (dg_spec_combine_transfer S (call_info_of ca p)
             (mk_dg_man cont global_of)
             (dg_local callee_state))
       }"
  unfolding routed_call_alternative_program_def using assms by (simp add: Let_def)

definition routed_callee_call_program ::
  "(pp × 'c, 'k, 'v, 'D::bounded_semilattice_sup_bot,
     'G::bounded_semilattice_sup_bot) dg_spec ⇒ ('v ⇒ 'k)
   ⇒ (pp ⇒ 'c ⇒ 'k)
   ⇒ (pp ⇒ 'c ⇒ 'D ⇒ call_action ⇒ 'c)
   ⇒ ('D ⇒ bool)
   ⇒ 'c ⇒ call_action ⇒ pp ⇒ 'D ⇒ pname
   ⇒ (pp × 'c, 'k, ('D, 'G) dg_state, ('D, 'G) dg_state) strategy_program"
where
  "routed_callee_call_program S global_of seed route is_bot ctx ca cc caller p =
     do {
       pairs ← enter⇧♯ S (call_info_of ca p) (mk_dg_man caller global_of);
       side_rhs_fold_dg bot
         (map (routed_call_alternative_program S global_of seed route is_bot ctx ca cc p) pairs)
     }"

text ‹
  The call site's own contribution: read the caller state, ask
  ‹resolve› which procedures this site can enter given that state, and join what each
  resolved activation returns. The callee is the resolver's answer, not a component of
  the enumeration the equation system was built from, so a resolver reading the caller
  state selects the target at solve time. \<^const>‹static_targets› is the resolver that
  ignores the state and answers from the CFG, which reproduces the statically
  enumerated behaviour exactly.

  An empty answer contributes \<^const>‹bot›. Under \<^const>‹static_targets› that happens
  only where the CFG has no call edge, i.e. where the enumeration produced no combine
  tree either.
›

definition routed_call_program ::
  "(pp × 'c, 'k, 'v, 'D::bounded_semilattice_sup_bot,
     'G::bounded_semilattice_sup_bot) dg_spec ⇒ ('v ⇒ 'k)
   ⇒ (pp ⇒ 'c ⇒ 'k)
   ⇒ (pp ⇒ pp ⇒ call_action ⇒ 'D ⇒ pname list)
   ⇒ ('D ⇒ bool)
   ⇒ (pp ⇒ 'c ⇒ 'D ⇒ call_action ⇒ 'c)
   ⇒ 'c ⇒ call_action ⇒ pp ⇒ pp
   ⇒ (pp × 'c, 'k, ('D, 'G) dg_state, ('D, 'G) dg_state) strategy_program"
where
  "routed_call_program S global_of seed resolve is_bot route ctx ca cc v =
     do {
       caller_state ← sp_read_local (cc, ctx);
       side_rhs_fold_dg bot
         (map (routed_callee_call_program S global_of seed route is_bot ctx ca cc
                 (dg_local caller_state))
              (resolve v cc ca (dg_local caller_state)))
     }"


text ‹The seed read-back hook: at a callee entry it reads the seed out of the
  ‹dg_local› half, matching ‹routed_call_program›'s write.›
definition routed_entry_seed_programs ::
  "(pp ⇒ 'c ⇒ 'k)
   ⇒ (pp ⇒ 'c ⇒ 'D::bounded_semilattice_sup_bot ⇒ call_action ⇒ 'c)
   ⇒ 'c ⇒ pp
   ⇒ (pp × 'c, 'k, ('D, 'G::bounded_semilattice_sup_bot) dg_state,
        ('D, 'G) dg_state) strategy_program list"
where
  "routed_entry_seed_programs seed route ctx v =
     (case v of FunctionEntry _ ⇒
        [do {
           seed_state ← sp_read_global (seed v ctx);
           sp_return (DG (dg_local seed_state) bot)
         }]
       | _ ⇒ [])"

lemma routed_entry_seed_programs_free:
  "x ∈ set (routed_entry_seed_programs seed route ctx v)
     ⟹ sides_of_program x tau z = bot"
  unfolding routed_entry_seed_programs_def
  by (cases v) (auto simp: sp_compile_def bot_fun_def)

lemma routed_entry_seed_programs_local_only:
  "x ∈ set (routed_entry_seed_programs seed route ctx v)
     ⟹ dg_global (traverse_program x tau) = bot"
  unfolding routed_entry_seed_programs_def by (cases v) (auto simp: sp_compile_def)

text ‹
  Every routed hook runs its continuation once, given that the specification's
  transfers do. The generator's fold asks for exactly that, and a context policy
  discharges it by naming its specification's \<^const>‹dg_spec_wf›.
›

lemma sp_wf_routed_entry_seed_programs [intro]:
  "x ∈ set (routed_entry_seed_programs seed route ctx v) ⟹ sp_wf x"
  unfolding routed_entry_seed_programs_def by (cases v) auto

lemma sp_wf_routed_call_alternative_program [intro]:
  assumes "dg_spec_wf S"
  shows
    "sp_wf (routed_call_alternative_program S global_of seed route is_bot ctx ca cc p alt)"
  unfolding routed_call_alternative_program_def Let_def
  by (auto intro!: sp_wf_map sp_wf_bind dg_spec_wf_combine[OF assms] split: prod.splits)

lemma sp_wf_routed_callee_call_program [intro]:
  assumes "dg_spec_wf S"
  shows
    "sp_wf (routed_callee_call_program S global_of seed route is_bot ctx ca cc caller p)"
  unfolding routed_callee_call_program_def
  by (intro sp_wf_bind dg_spec_wf_enter[OF assms] sp_wf_side_rhs_fold_dg)
     (auto intro: sp_wf_routed_call_alternative_program[OF assms])

lemma sp_wf_routed_call_program [intro]:
  assumes "dg_spec_wf S"
  shows
    "sp_wf (routed_call_program S global_of seed resolve is_bot route ctx ca cc v)"
  unfolding routed_call_program_def
  by (intro sp_wf_bind sp_wf_read_local sp_wf_side_rhs_fold_dg)
     (auto intro: sp_wf_routed_callee_call_program[OF assms])

lemma sp_wf_routed_call_alternative_programs [intro]:
  "dg_spec_wf S
     ⟹ ∀q ∈ set (map (routed_call_alternative_program S global_of seed route
             is_bot ctx ca cc p) pairs). sp_wf q"
  by (auto intro: sp_wf_routed_call_alternative_program)

lemma sp_wf_routed_callee_call_programs [intro]:
  "dg_spec_wf S
     ⟹ ∀q ∈ set (map (routed_callee_call_program S global_of seed route
             is_bot ctx ca cc caller) ps). sp_wf q"
  by (auto intro: sp_wf_routed_callee_call_program)

text ‹
  How a routed per-target program relates to its parts under a solution. Each bound
  is stated for ∗‹one› alternative of the list a single run of the entry
  produced, because the program is a fold over exactly those. These are the only
  facts CALL and COMB below need about its body.
›


lemma routed_callee_call_program_sides_ge_seed:
  assumes wfS: "dg_spec_wf S"
    and R: "enter_runs (enter⇧♯ S (call_info_of (CallEdge dst pars args) p))
                (mk_dg_man caller global_of) σ pairs pub"
    and mem: "(cont, entry) ∈ set pairs"
    and nb: "¬ is_bot entry"
  shows "DG entry bot
           ≤ sides_of_program (routed_callee_call_program S global_of seed route is_bot ctx
                (CallEdge dst pars args) cc caller p) σ
                (Inr (seed (FunctionEntry p)
                   (route cc ctx entry (CallEdge dst pars args))))"
proof -
  let ?F = "routed_call_alternative_program S global_of seed route is_bot ctx
              (CallEdge dst pars args) cc p"
  let ?k = "Inr (seed (FunctionEntry p) (route cc ctx entry (CallEdge dst pars args)))"
  have "DG entry bot ≤ sides_of_program (?F (cont, entry)) σ ?k"
    unfolding routed_call_alternative_program_def using nb
    by (simp add: Let_def sp_compile_def)
  also have "… ≤ sides_of_program (side_rhs_fold_dg bot (map ?F pairs)) σ ?k"
    by (rule sides_le_side_rhs_fold_dg[OF sp_wf_routed_call_alternative_programs[OF wfS]])
       (use mem in force)
  also have "… ≤ sides_of_program (routed_callee_call_program S global_of seed route is_bot ctx
                     (CallEdge dst pars args) cc caller p) σ ?k"
    unfolding routed_callee_call_program_def
    by (simp add: sp_compile_bind sp_wf_observes enter_runsD_sides[OF R] sup_fun_def)
  finally show ?thesis .
qed

text ‹
  One rung further out: one resolved target's contribution survives the fold
  over the site's targets. Stated without a locale so a proof that must place a
  publication inside the solution --- one whose concretization reads the global
  channel --- can walk outwards from a call site it has not yet routed.
›

lemma routed_call_program_sides_ge_at:
  assumes wfS: "dg_spec_wf S"
    and mem: "p ∈ set (resolve v cc ca (dg_local (σ (Inl (cc, ctx)))))"
  shows "sides_of_program (routed_callee_call_program S global_of seed route is_bot ctx ca cc
             (dg_local (σ (Inl (cc, ctx)))) p) σ z
           ≤ sides_of_program
                (routed_call_program S global_of seed resolve is_bot route ctx ca cc v) σ z"
proof -
  have "routed_callee_call_program S global_of seed route is_bot ctx ca cc
          (dg_local (σ (Inl (cc, ctx)))) p
          ∈ set (map (routed_callee_call_program S global_of seed route is_bot ctx ca cc
                        (dg_local (σ (Inl (cc, ctx)))))
                  (resolve v cc ca (dg_local (σ (Inl (cc, ctx))))))"
    using mem by simp
  from sides_le_side_rhs_fold_dg[OF sp_wf_routed_callee_call_programs[OF wfS] this,
        where acc = bot and k = z]
  show ?thesis
    by (simp add: routed_call_program_def sp_compile_bind sp_wf_observes)
qed

lemma routed_callee_call_program_sides_ge_combine:
  assumes wfS: "dg_spec_wf S"
    and R: "enter_runs (enter⇧♯ S (call_info_of ca p))
                (mk_dg_man caller global_of) σ pairs pub"
    and mem: "(cont, entry) ∈ set pairs"
  shows "sides_of_program
           (routed_call_alternative_program S global_of seed route is_bot ctx ca cc p (cont, entry))
             σ z
           ≤ sides_of_program
                (routed_callee_call_program S global_of seed route is_bot ctx ca cc caller p) σ z"
proof -
  let ?F = "routed_call_alternative_program S global_of seed route is_bot ctx ca cc p"
  have "sides_of_program (?F (cont, entry)) σ z
          ≤ sides_of_program (side_rhs_fold_dg bot (map ?F pairs)) σ z"
    by (rule sides_le_side_rhs_fold_dg[OF sp_wf_routed_call_alternative_programs[OF wfS]])
       (use mem in force)
  also have "… ≤ sides_of_program
                    (routed_callee_call_program S global_of seed route is_bot ctx ca cc caller p) σ z"
    unfolding routed_callee_call_program_def
    by (simp add: sp_compile_bind sp_wf_observes enter_runsD_sides[OF R] sup_fun_def)
  finally show ?thesis .
qed

text ‹
  And the answer: the value a selected alternative's return combine produces is
  below what the call answers, because the call answers the join over every
  alternative. This is the bound COMB needs --- one alternative's combine is
  covered, not all of them jointly. It holds for a bottom alternative too, whose
  combine runs against \<^const>‹bot›.
›

lemma routed_callee_call_program_traverse_ge:
  assumes wfS: "dg_spec_wf S"
    and R: "enter_runs (enter⇧♯ S (call_info_of ca p))
                (mk_dg_man caller global_of) σ pairs pub"
    and mem: "(cont, entry) ∈ set pairs"
  shows "dg_local (traverse_program
             (routed_call_alternative_program S global_of seed route is_bot ctx ca cc p (cont, entry))
               σ)
           ≤ dg_local (traverse_program
                (routed_callee_call_program S global_of seed route is_bot ctx ca cc caller p) σ)"
proof -
  let ?F = "routed_call_alternative_program S global_of seed route is_bot ctx ca cc p"
  have "dg_local (traverse_program (?F (cont, entry)) σ)
          ≤ side_acc_dg bot σ (map ?F pairs)"
    by (rule dg_local_traverse_le_side_acc_dg) (use mem in force)
  also have "… = dg_local (traverse_program
                     (routed_callee_call_program S global_of seed route is_bot ctx ca cc caller p) σ)"
    unfolding routed_callee_call_program_def
    by (simp add: sp_compile_bind sp_wf_observes enter_runsD_traverse[OF R]
        traverse_side_rhs_fold_dg[OF sp_wf_routed_call_alternative_programs[OF wfS]])
  finally show ?thesis .
qed


subsection ‹When a routed combine publishes nothing at the analysis global›

text ‹
  Whether a program needs reshaping before the buffered generator can consume it is a
  property of that program, not of the analysis that produced it. The two facts below
  say when a routed combine needs none.

  ▪ Its answer always carries ‹bot› on the globals half: the per-call-site fold
    accumulates only ‹dg_local›.
  ▪ It publishes nothing at ‹buffer_key› as soon as the spec's own enter and combine
    sub-programs publish nothing there --- the only side the routed program adds is
    the seed, and a seed key is never ‹buffer_key›.

  A program with both properties is already its own contribution analogue, so the
  buffered generator's ‹cmb_c› hook can be the program itself. A spec whose transfers
  do publish at ‹buffer_key› fails the second and must supply a reshaped hook instead.
›

lemma sides_side_rhs_fold_dg_bot:
  assumes wf: "∀t ∈ set ts. sp_wf t"
    and "⋀t. t ∈ set ts ⟹ sides_of_program t σ z = bot"
  shows "sides_of_program (side_rhs_fold_dg acc ts) σ z = bot"
  using assms
  by (simp add: sides_of_program_side_rhs_fold_dg_char[OF wf] foldr_sup_bot_of_all_bot)

lemma routed_call_program_global_free:
  assumes wfS: "dg_spec_wf S"
  shows "dg_global (traverse_program
           (routed_call_program S global_of seed resolve is_bot route ctx ca cc v) σ) = bot"
  by (simp add: routed_call_program_def sp_compile_bind sp_wf_observes
      traverse_side_rhs_fold_dg[OF sp_wf_routed_callee_call_programs[OF wfS]])

text ‹
  Every hook the routed generator builds from a well-formed specification answers
  nothing on its global half: an edge answers its transfer's local value, a call
  answers the folded return values, and a seed answers its local slot. So the
  buffered generator a solver runs is the unbuffered one the framework is stated
  over, at every specification, whether or not it publishes at the analysis global.
›

lemma dg_global_traverse_dg_spec_edge_program:
  assumes "dg_spec_wf S"
  shows "dg_global (traverse_program (dg_spec_edge_program S a src unknown_of) σ) = bot"
proof -
  let ?P = "transfer_program_at (λm. dg_spec_step S a (outer_man (dgs_query S) m)) src unknown_of"
  have wf: "sp_wf ?P"
    unfolding transfer_program_at_def
    by (intro sp_wf_bind sp_wf_dg_read_at) (rule dg_spec_wf_step[OF assms])
  have "?P (λv. Answer (DG v bot))
      = sp_lift_tree (?P (λv. Answer (DG v bot))) (λd. Answer (DG (dg_local d) bot))"
    using sp_wf_graft[OF wf, where k = "λv. Answer (DG v bot)"
        and h = "λd. Answer (DG (dg_local d) bot)"]
    by simp
  then have "traverse_rhs (?P (λv. Answer (DG v bot))) σ
      = DG (dg_local (traverse_rhs (?P (λv. Answer (DG v bot))) σ)) bot"
    by (metis (no_types, lifting) traverse_rhs.simps(1) traverse_rhs_sp_lift_tree)
  then show ?thesis
    by (simp add: dg_spec_edge_program_def transfer_program_def sp_compile_def
        sp_compile_with_def) (metis dg_state.sel(2))
qed

theorem pp_routed_of_buffered:
  assumes wfS: "dg_spec_wf S"
    and ne: "⋀p ctx. seed p ctx ≠ buffer_key"
    and pp: "part_post_solution
     (routed_node_rhs_buffered intra_predecessor_addr_list call_site_list (λ_. buffer_key) route
        (λctx' src a. dg_spec_edge_program S a src global_of)
        (routed_call_program S global_of seed resolve is_bot)
        (routed_entry_seed_programs seed)
        g bot0 d⇩0 g⇩0)
     x0 sigma vars"
  shows "part_post_solution
     (routed_node_rhs intra_predecessor_addr_list call_site_list (λ_. buffer_key) route
        (λctx' src a. dg_spec_edge_program S a src global_of)
        (routed_call_program S global_of seed resolve is_bot)
        (routed_entry_seed_programs seed)
        g bot0 d⇩0 g⇩0)
     x0 sigma vars"
proof (rule part_post_solution_routed_node_rhs_buffered_answers_local[OF _ _ pp])
  show "⋀c' w. ∀p ∈ set (routed_contribution_programs intra_predecessor_addr_list
           call_site_list route (λctx' src a. dg_spec_edge_program S a src global_of)
           (routed_call_program S global_of seed resolve is_bot)
           (routed_entry_seed_programs seed) g c' w). sp_wf p"
    by (rule routed_contribution_programs_wf)
       (auto intro: sp_wf_dg_spec_edge_program[OF wfS] sp_wf_routed_call_program[OF wfS])
  show "⋀c' w p τ. p ∈ set (routed_contribution_programs intra_predecessor_addr_list
           call_site_list route (λctx' src a. dg_spec_edge_program S a src global_of)
           (routed_call_program S global_of seed resolve is_bot)
           (routed_entry_seed_programs seed) g c' w)
         ⟹ dg_global (traverse_program p τ) = bot"
    by (auto elim!: routed_contribution_programsE
        simp: routed_call_program_global_free[OF wfS] routed_entry_seed_programs_local_only
          dg_global_traverse_dg_spec_edge_program[OF wfS])
qed

text ‹
  The entry half of the condition is now stated through \<^const>‹enter_runs›: an
  entry program publishes nothing at ‹buffer_key› exactly when the ‹pub› it runs to is
  \<^const>‹bot› there. It has to be stated this way: an entry program answers a
  list of alternatives, not the solver's value type, so it has no compiled tree
  of its own to observe.
›

lemma routed_callee_call_program_side_free_at_buffer_key:
  assumes wfS: "dg_spec_wf S"
    and enter_free: "⋀ci d pairs pub.
        enter_runs (enter⇧♯ S ci) (mk_dg_man d global_of) σ pairs pub ⟹ pub (Inr buffer_key) = bot"
    and enter_runs_ex: "⋀ci d. ∃pairs pub.
        enter_runs (enter⇧♯ S ci) (mk_dg_man d global_of) σ pairs pub"
    and comb_free: "⋀ci d de z. sides_of_rhs (sp_compile_with (λx. DG x bot)
        (dg_spec_combine_transfer S ci (mk_dg_man d global_of) de)) σ z = bot"
    and ne: "⋀p ctx'. seed (FunctionEntry p) ctx' ≠ buffer_key"
  shows "sides_of_program
           (routed_callee_call_program S global_of seed route is_bot ctx ca cc caller p) σ (Inr buffer_key)
         = bot"
proof -
  obtain pairs pub
    where R: "enter_runs (enter⇧♯ S (call_info_of ca p))
                (mk_dg_man caller global_of) σ pairs pub"
    using enter_runs_ex by blast
  have alts: "⋀t. t ∈ set (map (routed_call_alternative_program S global_of seed route is_bot ctx
                                  ca cc p) pairs)
                 ⟹ sides_of_program t σ (Inr buffer_key) = bot"
    by (auto simp: routed_call_alternative_program_def Let_def sp_compile_def
        comb_free ne[THEN not_sym] split: if_splits)
  have "sides_of_program
          (routed_callee_call_program S global_of seed route is_bot ctx ca cc caller p) σ (Inr buffer_key)
        = pub (Inr buffer_key)
          ⊔ sides_of_program (side_rhs_fold_dg bot
                (map (routed_call_alternative_program S global_of seed route is_bot ctx ca cc p)
                  pairs))
              σ (Inr buffer_key)"
    unfolding routed_callee_call_program_def
    by (simp add: sp_compile_bind sp_wf_observes enter_runsD_sides[OF R] sup_fun_def)
  also have "… = bot"
  proof -
    have "sides_of_program (side_rhs_fold_dg bot
            (map (routed_call_alternative_program S global_of seed route is_bot ctx ca cc p) pairs))
            σ (Inr buffer_key) = bot"
      by (rule sides_side_rhs_fold_dg_bot[OF sp_wf_routed_call_alternative_programs[OF wfS]])
         (rule alts)
    then show ?thesis using enter_free[OF R] by simp
  qed
  finally show ?thesis .
qed

lemma routed_call_program_side_free_at_buffer_key:
  assumes wfS: "dg_spec_wf S"
    and enter_free: "⋀ci d pairs pub.
        enter_runs (enter⇧♯ S ci) (mk_dg_man d global_of) σ pairs pub ⟹ pub (Inr buffer_key) = bot"
    and enter_runs_ex: "⋀ci d. ∃pairs pub.
        enter_runs (enter⇧♯ S ci) (mk_dg_man d global_of) σ pairs pub"
    and comb_free: "⋀ci d de z. sides_of_rhs (sp_compile_with (λx. DG x bot)
        (dg_spec_combine_transfer S ci (mk_dg_man d global_of) de)) σ z = bot"
    and ne: "⋀p ctx'. seed (FunctionEntry p) ctx' ≠ buffer_key"
  shows "sides_of_program (routed_call_program S global_of seed resolve is_bot route ctx ca cc v)
           σ (Inr buffer_key) = bot"
proof -
  have at_free: "⋀caller p.
      sides_of_program (routed_callee_call_program S global_of seed route is_bot ctx ca cc caller p)
        σ (Inr buffer_key) = bot"
    by (rule routed_callee_call_program_side_free_at_buffer_key[OF wfS])
       (rule enter_free enter_runs_ex comb_free ne, assumption?)+
  have "sides_of_program (side_rhs_fold_dg bot
          (map (routed_callee_call_program S global_of seed route is_bot ctx ca cc
                  (dg_local (σ (Inl (cc, ctx)))))
             (resolve v cc ca (dg_local (σ (Inl (cc, ctx))))))) σ (Inr buffer_key) = bot"
    by (rule sides_side_rhs_fold_dg_bot[OF sp_wf_routed_callee_call_programs[OF wfS]])
       (auto simp: at_free)
  then show ?thesis by (simp add: routed_call_program_def sp_compile_bind sp_wf_observes)
qed


end