Theory Voblint_Result.DG_Analysis

theory DG_Analysis
  imports
    DG_Result_Construction
    Analysis_Surface
    "Voblint_Framework.Routed_Analysis_Sound"
    "Voblint_Exec.Routed_Exec_Refinement"
    Source_Activation_Sound
    "Voblint_Routing.Compiled_Routed_Equations"
    "Voblint_Routing.Entry_State_Routed_Context"
    "Voblint_Solver.TD_Solver_Bridge"
    "Voblint_Framework.DG_Keyed_Split_Spec"
begin

section ‹One context-sensitive analysis, assembled from its choices›

text ‹
  A concrete analysis picks a domain implementation, an initial state, a way of
  telling activations apart, a solver and a classifier; everything between those
  choices and the published table is the same work at every domain and at every
  context policy. This theory does that work once.

  The construction half is ‹dg_pipeline›, which carries no correctness
  assumptions, so its defining equations are unconditional and can be declared to
  the code generator. The correctness half is ‹dg_analysis›, which adds
  the domain and solver contracts and derives, for one program, the routed
  soundness statement every policy shares.

  Vocabulary. A ∗‹routed› equation system publishes a callee's entry state at a
  global seed key instead of reading the callee entry directly; a ∗‹context› is
  the value the routing function attaches to a program point so that one point
  can be solved at several unknowns; ∗‹covered› keys are the unknowns the solver
  actually visited, which is not the same as the unknowns holding a bottom state.

  What this covers, and what it does not. It is the assembly for executable
  non-relational analyses whose local unknown carries a whole reachability-lifted
  store and whose entry operation answers with a pure list of alternatives. The
  context type, the global-key type, the seed constructor, the routing function
  and the root context are all parameters; the carrier and the entry shape are
  not.
›

subsection ‹The formals route, once for every domain›

text ‹
  Keying a callee on the abstract values its formals hold on entry, at the
  executable carrier. \<^const>‹formals_route_lifted_gen› is the same decision one
  layer up, on the state a solved table hands out; the equation below is what
  lets a routed instance discharge its routing-agreement obligation without a
  domain-specific lemma. The routed generator enters the callee frame before it
  routes, so the route itself only projects the formals out of the state it is
  handed.
›

definition exec_formals_route ::
    "(vname ⇒ bool) ⇒ pp ⇒ 'a list
       ⇒ ('a::bot) default_st lifted ⇒ call_action ⇒ 'a list" where
  "exec_formals_route 𝒢 u ctx d ca =
     (case ca of CallEdge dst pars args ⇒
        formals_context pars
          (ρ⇘𝒢⇙ (case d of Bot ⇒ bot | Lifted d0 ⇒ d0)))"

text ‹
  The same routing decision taken from a solved ∗‹result› instead of from the
  solver's carrier. A rendering that draws one node per activation has to know
  which callee context a call edge enters, and the table it draws from holds
  \<^typ>‹'a abs_state› rather than \<^typ>‹'a default_st› --- so the projection
  \<^const>‹exec_formals_route› performs is unavailable to it, and the entered
  state has to be recomputed from the caller's. ‹enter› is the domain's own
  entry transfer and is the only domain-specific value involved; emptiness is
  \<^const>‹is_empty›, the \<^class>‹executable_domain› operation every domain carries.

  The witness search runs over the formals rather than over the whole state,
  and it has to: \<^const>‹is_empty_state› quantifies over every \<^typ>‹vname›, so
  its code equation would demand an \<^class>‹enum› instance for
  \<^typ>‹String.literal› and this constant would not generate code at all.
  Restricting to the formals is also exact rather than merely cheaper ---
  procedure entry resets every non-global variable to top and leaves every
  global at the caller's own value, so no name outside the formals can witness
  emptiness that the caller did not already have.

  \<^const>‹None› means the call routes nowhere, because the entered state
  represents no concrete store. It is not a sentinel context: an empty formal
  list is a legitimate context in its own right --- a zero-formal callee's own
  entry is genuinely keyed at ‹[]› --- so no \<^typ>‹'a list› value could carry
  that meaning without colliding with a real one.
›

definition callee_ctx_of ::
    "((vname ⇒ bool) ⇒ vname list ⇒ exp list ⇒ 'a abs_state ⇒ 'a abs_state)
       ⇒ (vname ⇒ bool) ⇒ call_action ⇒ ('a::executable_domain) abs_state
       ⇒ 'a list option" where
  "callee_ctx_of enter 𝒢 ca st =
     (case ca of CallEdge dst pars args ⇒
        (let entered = enter 𝒢 pars args st
         in if list_ex (λx. is_empty (entered x)) pars then None
            else Some (formals_context pars entered)))"

lemma exec_formals_route_commute:
  "formals_route_lifted_gen u ctx (ρ⇘𝒢⇙ d) ca
     = exec_formals_route 𝒢 u ctx d ca"
  by (cases d; cases ca)
     (simp_all add: formals_route_lifted_gen_def formals_route_lifted_def
        exec_formals_route_def default_st_to_fun_def)

subsection ‹The construction›

text ‹
  The pipeline runs one component, ‹comp 𝒢 p›: a single analysis, or the
  combination of several. ‹init_st› is the unlifted entry state; the pipeline
  lifts it, because a reachability-lifted carrier is what the routed generator
  solves over. ‹empty p› is the carrier's executable emptiness test and ‹rd 𝒢›
  reads a carrier state back as the value the result table publishes. Nothing
  here fixes what the carrier or the published value is.
  ‹bot_state› is a parameter rather than the \<^class>‹order_bot› operation for the
  same code-generation reason \<^locale>‹analysis_surface› states: a sort constraint
  here would demand an executable \<^const>‹bot› at a function type.
›

text ‹
  Everything one solve publishes, read back as values: the result table, the
  solved value of each global name, the seed a call published at a procedure entry under a
  context, what one edge's local step makes of a point's solved state, and where a
  call leads when it contributes at all.
›

record ('c, 'n, 'v) solved_run =
  run_table :: "('c, 'v) solved_table"
  run_shared :: "'n ⇒ 'v lifted"
  run_seed :: "pname ⇒ 'c ⇒ 'v lifted"
  run_step :: "pp ⇒ 'c ⇒ edge_action ⇒ 'v lifted"
  run_succ :: "cfg_node ⇒ 'c ⇒ call_action ⇒ pname ⇒ 'c option"

text ‹
  ‹dg_pipeline› only fixes parameters: the component ‹comp›, the carrier
  operations ‹emp›, ‹rd› and ‹init_st›, the key a node buffers its own
  global part at and the key ‹global_of n› each global name lives at, the
  context policy ‹seed›/‹route›/
  ‹root_ctx›, the solver ‹solve› with its domain, the check classifier, and the
  placement of program state between the two halves of a solver unknown.
  The soundness assumptions live in the locales built on it.

  The placement is six operations. ‹place_spec› builds the D/G specification
  the equations run, from the component. ‹place_cmb› recombines a local value
  with the solved global environment into the state a point describes, and
  ‹place_rl› and ‹place_rg› project a state onto the part each half keeps.
  ‹place_inits› lists the initial value of each global name, which the program
  entry publishes at that name's key ‹global_of n›. ‹place_enter› is the caller
  state a call enters from: it may describe more than ‹place_cmb›, so a call reads
  only the globals it needs. An analysis that keeps all of its state in the local
  half builds the specification with \<^const>‹dg_spec_of›, recombines by ignoring
  the environment, keeps every state locally, publishes \<^const>‹Bot›, lists no
  initial values and enters from the caller's state as it is.
›

locale dg_pipeline =
  fixes comp :: "(vname ⇒ bool) ⇒ imp_prog ⇒ 's::semilattice_sup lifted local_spec"
    and emp :: "imp_prog ⇒ 's ⇒ bool"
    and rd :: "(vname ⇒ bool) ⇒ 's ⇒ 'v"
    and init_st :: 's
    and buffer_key :: 'k
    and global_of :: "'n ⇒ 'k"
    and seed :: "pp ⇒ 'c ⇒ 'k"
    and route :: "(vname ⇒ bool) ⇒ pp ⇒ 'c ⇒ 's lifted ⇒ call_action ⇒ 'c"
    and root_ctx :: 'c
    and solve :: "(pp × 'c, 'k, ('s lifted, 's lifted) dg_state) eqsT
                  ⇒ pp × 'c
                  ⇒ (pp × 'c) set × (pp × 'c + 'k ⇒ ('s lifted, 's lifted) dg_state)"
    and solve_dom :: "(pp × 'c, 'k, ('s lifted, 's lifted) dg_state) eqsT ⇒ pp × 'c ⇒ bool"
    and bot_state :: 'v
    and classify :: "exp ⇒ 'v ⇒ check_result"
    and place_spec :: "imp_prog ⇒ 's lifted local_spec
                        ⇒ (pp × 'c, 'k, 'n, 's lifted, 's lifted) dg_spec"
    and place_cmb :: "imp_prog ⇒ 's lifted ⇒ ('n ⇒ 's lifted) ⇒ 's lifted"
    and place_rl :: "(vname ⇒ bool) ⇒ 's lifted ⇒ 's lifted"
    and place_rg :: "(vname ⇒ bool) ⇒ 's lifted ⇒ 's lifted"
    and place_inits :: "(vname ⇒ bool) ⇒ imp_prog ⇒ ('n × 's lifted) list"
    and place_enter :: "imp_prog ⇒ call_info ⇒ 's lifted ⇒ ('n ⇒ 's lifted) ⇒ 's lifted"
begin

definition analysis_spec :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ (pp × 'c, 'k, 'n, 's lifted, 's lifted) dg_spec" where
  "analysis_spec 𝒢 p = place_spec p (comp 𝒢 p)"

text ‹
  The state the component enters a callee with, from a whole caller state. The
  pipeline supports components whose entry answers one alternative, the caller's
  state paired with this one.
›

definition comp_entry :: "(vname ⇒ bool) ⇒ imp_prog ⇒ call_info ⇒ 's lifted
    ⇒ 's lifted" where
  "comp_entry 𝒢 p ci w = snd (hd (ls_enter (comp 𝒢 p) (ls_channel (comp 𝒢 p) w) ci (w, w)))"

text ‹
  The alternative a call enters its callee with, as the solver stores it: the
  component enters from the caller state ‹place_enter› recombines, and each
  half of the answer keeps its local part.
›

definition entry_alt :: "(vname ⇒ bool) ⇒ imp_prog ⇒ call_info ⇒ 's lifted
    ⇒ ('n ⇒ 's lifted) ⇒ 's lifted × 's lifted" where
  "entry_alt 𝒢 p ci d g =
     (let w = place_enter p ci d g in (place_rl 𝒢 w, place_rl 𝒢 (comp_entry 𝒢 p ci w)))"

text ‹The state a call enters its callee with.›

definition entry_of :: "(vname ⇒ bool) ⇒ imp_prog ⇒ call_info ⇒ 's lifted
    ⇒ ('n ⇒ 's lifted) ⇒ 's lifted"
  where "entry_of 𝒢 p ci d g = snd (entry_alt 𝒢 p ci d g)"

text ‹
  The unknown the solver is asked for. It is the program exit at the root
  context: a demand-driven solver is started at the answer a caller wants and
  explores backwards from it, so the root query is the exit and the entry point
  is reached as one of its dependencies.
›

definition root_query :: "imp_prog ⇒ pp × 'c" where
  "root_query p = (cfg_exit (prog_cfg p), root_ctx)"

text ‹
  ‹root_query›'s own type mentions no domain, so a code equation for it carries a
  sort hypothesis the code generator cannot see and silently rejects. The two
  constants that use it inline it instead: their types do mention the domain, so
  their equations are accepted, and ‹root_query› never has to be executable.
›

text ‹
  The initial value of each global name is a side effect like any other: the
  program entry publishes it, once, at the name's key, as a run's initialization
  happens before its first statement. A placement that keeps its initial global
  part at the node's own key passes no such values.
›

definition init_publications :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ pp × 'c ⇒ ('k × ('s lifted, 's lifted) dg_state) list" where
  "init_publications 𝒢 p x =
     (if x = (cfg_entry (prog_cfg p), root_ctx)
      then map (λ(n, d). (global_of n, DG Bot d)) (place_inits 𝒢 p) else [])"

text ‹
  The generated code evaluates this test at every equation evaluation, so the code
  equation names the entry node directly instead of compiling the program each time.
›

lemma init_publications_code:
  "init_publications 𝒢 p x =
     (if x = (FunctionEntry prog_main_name, root_ctx)
      then map (λ(n, d). (global_of n, DG Bot d)) (place_inits 𝒢 p) else [])"
  by (simp add: init_publications_def prog_cfg_def)

text ‹
  The initial global environment a run starts from: what the entry node buffers at
  its own key, read at every name living there, together with the root's initial
  publications.
›

definition init_env :: "(vname ⇒ bool) ⇒ imp_prog ⇒ 'n ⇒ 's lifted" where
  "init_env 𝒢 p n =
     (if global_of n = buffer_key then place_rg 𝒢 (Lifted init_st) else Bot)
       ⊔ (⨆(m, d)←filter (λ(m, d). m = n) (place_inits 𝒢 p). d)"

definition equations :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ (pp × 'c, 'k,
         ('s lifted, 's lifted) dg_state) eqsT" where
  "equations 𝒢 p =
     with_init (init_publications 𝒢 p)
       (compiled_routed_eqs_for buffer_key global_of seed (route 𝒢)
          (analysis_spec 𝒢 p) (prog_cfg p) (Lifted init_st) (place_rg 𝒢 (Lifted init_st)))"

definition solution :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ (pp × 'c) set
         × (pp × 'c + 'k
              ⇒ ('s lifted, 's lifted) dg_state)" where
  "solution 𝒢 p = solve (equations 𝒢 p) (root_query p)"

definition terminates :: "(vname ⇒ bool) ⇒ imp_prog ⇒ bool" where
  "terminates 𝒢 p = solve_dom (equations 𝒢 p) (root_query p)"

lemma solution_code: "solution 𝒢 p = solve (equations 𝒢 p) (cfg_exit (prog_cfg p), root_ctx)"
  by (simp add: solution_def root_query_def)

lemma terminates_code:
  "terminates 𝒢 p = solve_dom (equations 𝒢 p) (cfg_exit (prog_cfg p), root_ctx)"
  by (simp add: terminates_def root_query_def)

definition sol_vars :: "(vname ⇒ bool) ⇒ imp_prog ⇒ (pp × 'c) set" where
  "sol_vars 𝒢 p = fst (solution 𝒢 p)"

definition sol_env :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ pp × 'c + 'k ⇒ ('s lifted, 's lifted) dg_state" where
  "sol_env 𝒢 p = snd (solution 𝒢 p)"

definition reader :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ pp × 'c + 'k ⇒ 's lifted" where
  "reader 𝒢 p = solved_local_reader (sol_vars 𝒢 p) (sol_env 𝒢 p)"

definition result :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ ('c, 'v) solved_table" where
  "result 𝒢 p = dg_result_for (rd 𝒢) (emp p) (place_cmb p) global_of (solution 𝒢 p)"

text ‹The solved global environment every recombination reads.›

definition sol_global :: "(vname ⇒ bool) ⇒ imp_prog ⇒ 'n ⇒ 's lifted" where
  "sol_global 𝒢 p = genv global_of (sol_env 𝒢 p)"

text ‹
  Where a call leads, as a function of the call site and the caller's context
  alone: this route applied to the state this solve published at that site. It
  names no concretization, so it belongs here rather than beside the soundness
  endpoints -- which is what lets a registration that cannot export a binder
  publish it by spelling this out, exactly as it publishes \<^const>‹result›.
›

definition ctx_succ :: "(vname ⇒ bool) ⇒ imp_prog ⇒ cfg_node ⇒ 'c
    ⇒ call_action ⇒ pname ⇒ 'c" where
  "ctx_succ 𝒢 p u ctx ca q =
     route 𝒢 u ctx (entry_of 𝒢 p (call_info_of ca q) (dg_local (sol_env 𝒢 p (Inl (u, ctx))))
                      (sol_global 𝒢 p)) ca"


text ‹
  Where a call leads when it contributes at all: ‹None› when the entered state is
  bottom, which is exactly when the routed call program drops the alternative, and
  otherwise the context \<^const>‹ctx_succ› names.
›

definition live_succ :: "(vname ⇒ bool) ⇒ imp_prog ⇒ cfg_node ⇒ 'c
    ⇒ call_action ⇒ pname ⇒ 'c option" where
  "live_succ 𝒢 p u ctx ca q =
     (if entry_of 𝒢 p (call_info_of ca q) (dg_local (sol_env 𝒢 p (Inl (u, ctx))))
           (sol_global 𝒢 p) = Bot
      then None else Some (ctx_succ 𝒢 p u ctx ca q))"


text ‹
  The values one solution publishes. The seeds are read exactly as a table entry is,
  so an unwritten key reads as \<^const>‹Bot›. The shared global is read
  without that canonicalization: its local half is bottom by construction, which
  would make every value it holds read as \<^const>‹Bot›.

  A step is what one edge's local step makes of a point's solved state: the term
  that edge contributes to its target's equation, re-evaluated on the solution. A
  target with several incoming edges stores only their join, so this is the one
  place the contribution of a single edge can be read. It is the component's own
  step, run with the answers its handler gives on the recombined state, as the
  edge transfer runs it, and published with the state it describes.

  The successor is \<^const>‹live_succ› read off the same solution, so a caller
  listing where every call leads does not solve the system again for each call.

  The solution is an argument, so a caller holding the executable solver's answer
  reads it without solving again; ‹run› below reads the specification's solve.
›

definition solved_run_of :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ (pp × 'c) set × (pp × 'c + 'k ⇒ ('s lifted, 's lifted) dg_state)
    ⇒ ('c, 'n, 'v) solved_run" where
  "solved_run_of 𝒢 p sol =
     (let c = comp 𝒢 p;
          g = genv global_of (snd sol);
          read = (λd. map_lift (rd 𝒢) (canonicalize_lift (emp p) d))
      in ⦇ run_table = dg_result_for (rd 𝒢) (emp p) (place_cmb p) global_of sol,
           run_shared = (λn. map_lift (rd 𝒢) (g n)),
           run_seed = (λf ctx. read (place_cmb p
                         (dg_local (snd sol (Inr (seed (FunctionEntry f) ctx)))) g)),
           run_step = (λv ctx a. read (let d = place_cmb p (dg_local (snd sol (Inl (v, ctx)))) g
                                       in ⟦a⟧⇧♯⇘c⇙ d)),
           run_succ = (λu ctx ca q.
             let d = entry_of 𝒢 p (call_info_of ca q) (dg_local (snd sol (Inl (u, ctx)))) g
             in if d = Bot then None else Some (route 𝒢 u ctx d ca)) ⦈)"

definition run :: "(vname ⇒ bool) ⇒ imp_prog ⇒ ('c, 'n, 'v) solved_run" where
  "run 𝒢 p = solved_run_of 𝒢 p (solution 𝒢 p)"

lemma run_table_run [simp]: "run_table (run 𝒢 p) = result 𝒢 p"
  by (simp add: run_def solved_run_of_def result_def Let_def)

lemma run_succ_run: "run_succ (run 𝒢 p) = live_succ 𝒢 p"
  by (simp add: run_def solved_run_of_def live_succ_def ctx_succ_def sol_env_def sol_global_def
      Let_def fun_eq_iff)

text ‹
  The contextual publication surface: one verdict per context at a check, and
  the aggregate a caller prints. Both are \<^const>‹classify_checks_ctx› and
  \<^const>‹classify_checks_verdicts› unchanged -- they are generic in the context
  type already -- so nothing here is policy-specific beyond supplying this
  pipeline's own result table.
›

definition check_projection :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ (pp × exp × ('c × contextual_verdict) set) list" where
  "check_projection 𝒢 p = classify_checks_ctx (prog_cfg p) (result 𝒢 p) classify"

definition verdict_report :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ (pp × exp × contextual_verdict) list" where
  "verdict_report 𝒢 p = classify_checks_verdicts (prog_cfg p) (result 𝒢 p) classify"

text ‹
  The same table read at one context: the state published there, and the check
  report off those states. These are \<^locale>‹analysis_surface›'s readings of this
  pipeline's result, so every policy publishes the same surface; a
  context-insensitive run reads it at ‹()›.
›

definition state_at :: "(vname ⇒ bool) ⇒ imp_prog ⇒ 'c ⇒ pp ⇒ 'v" where
  "state_at 𝒢 = analysis_surface.state_at (result 𝒢) bot_state"

definition report :: "(vname ⇒ bool) ⇒ imp_prog ⇒ 'c ⇒ check_report_entry list" where
  "report 𝒢 = analysis_surface.report (result 𝒢) bot_state classify"

definition report_with_state :: "(vname ⇒ bool) ⇒ imp_prog
    ⇒ 'c ⇒ (pp × exp × check_result × bool × 'v) list" where
  "report_with_state 𝒢 = analysis_surface.report_with_state (result 𝒢) bot_state classify"

lemma state_at_unfold:
  "state_at 𝒢 p ctx v
     = (case lookup_table (result 𝒢 p) v ctx of Bot ⇒ bot_state | Lifted st ⇒ st)"
  by (simp add: state_at_def analysis_surface.state_at_def)
end

text ‹Register the exported locale equations for direct calls to the generic pipeline.
  Attributes inside the locale apply through interpretation; code generation here also
  needs equations for the constants with their locale parameters left abstract.›

declare
  dg_pipeline.analysis_spec_def [code]
  dg_pipeline.comp_entry_def [code]
  dg_pipeline.entry_alt_def [code]
  dg_pipeline.entry_of_def [code]
  dg_pipeline.sol_global_def [code]
  dg_pipeline.init_publications_code [code]
  dg_pipeline.equations_def [code]
  dg_pipeline.solution_code [code]
  dg_pipeline.terminates_code [code]
  dg_pipeline.sol_vars_def [code]
  dg_pipeline.sol_env_def [code]
  dg_pipeline.reader_def [code]
  dg_pipeline.result_def [code]
  dg_pipeline.ctx_succ_def [code]
  dg_pipeline.live_succ_def [code]
  dg_pipeline.solved_run_of_def [code]
  dg_pipeline.run_def [code]
  dg_pipeline.check_projection_def [code]
  dg_pipeline.verdict_report_def [code]
  dg_pipeline.state_at_def [code]
  dg_pipeline.report_def [code]
  dg_pipeline.report_with_state_def [code]

subsection ‹The contracts›

text ‹
  What an instance owes, and nothing more: its component is sound for the
  concretization its publication map induces, its entry answers one alternative, its two
  emptiness tests are exact, its seed keys are distinct from the analysis-wide
  global, its solver is a \<^locale>‹certified_solver› (a post-solution over
  finitely many keys once it terminates), its classifier is correct, and its entry
  state describes every initial store. The equation system, the solve, the covered keys, the reader,
  the result table and the report are all fixed by \<^locale>‹dg_pipeline›
  above and appear here only in conclusions. Each obligation is stated at the
  program's own declared globals, the one set the soundness statement uses.
›

locale dg_analysis =
  dg_pipeline comp emp rd init_st buffer_key global_of seed route root_ctx solve solve_dom
    bot_state classify place_spec place_cmb place_rl place_rg place_inits place_enter
  + certified_solver solve solve_dom solve_c
  for comp :: "(vname ⇒ bool) ⇒ imp_prog ⇒ 's::semilattice_sup lifted local_spec"
    and emp :: "imp_prog ⇒ 's ⇒ bool"
    and rd :: "(vname ⇒ bool) ⇒ 's ⇒ 'v"
    and init_st :: 's
    and buffer_key :: 'k
    and global_of :: "'n ⇒ 'k"
    and seed :: "pp ⇒ 'c ⇒ 'k"
    and route :: "(vname ⇒ bool) ⇒ pp ⇒ 'c ⇒ 's lifted ⇒ call_action ⇒ 'c"
    and root_ctx :: 'c
    and solve solve_dom
    and bot_state :: 'v
    and classify :: "exp ⇒ 'v ⇒ check_result"
    and γ⇩V :: "'v ⇒ store set"
    and empty⇩V :: "'v ⇒ bool"
    and solve_c :: "(pp × 'c, 'k, ('s lifted, 's lifted) dg_state) eqsT
                    ⇒ pp × 'c
                    ⇒ ((pp × 'c) set
                          × (pp × 'c + 'k ⇒ ('s lifted, 's lifted) dg_state)) option"
    and place_spec :: "imp_prog ⇒ 's lifted local_spec
                        ⇒ (pp × 'c, 'k, 'n, 's lifted, 's lifted) dg_spec"
    and place_cmb :: "imp_prog ⇒ 's lifted ⇒ ('n ⇒ 's lifted) ⇒ 's lifted"
    and place_rl :: "(vname ⇒ bool) ⇒ 's lifted ⇒ 's lifted"
    and place_rg :: "(vname ⇒ bool) ⇒ 's lifted ⇒ 's lifted"
    and place_inits :: "(vname ⇒ bool) ⇒ imp_prog ⇒ ('n × 's lifted) list"
    and place_enter :: "imp_prog ⇒ call_info ⇒ 's lifted ⇒ ('n ⇒ 's lifted) ⇒ 's lifted" +
  assumes comp_sound:
      "⋀p. sound_local_spec (declared_global p)
               (λd. gamma_lift γ⇩V (map_lift (rd (declared_global p)) d))
               (comp (declared_global p) p)"
    and enter_single:
      "⋀p ci d. ls_enter (comp (declared_global p) p) (ls_channel (comp (declared_global p) p) d)
                    ci (d, d)
                  = [(d, comp_entry (declared_global p) p ci d)]"
    and place_contract:
      "⋀p. analysis_contract (analysis_spec (declared_global p) p)
               (λd e. gamma_lift γ⇩V
                        (map_lift (rd (declared_global p)) (place_cmb p d e)))
               (declared_global p)"
    and place_enter_runs:
      "⋀p ci d σ. ∃pub. enter_runs (enter⇧♯ (analysis_spec (declared_global p) p) ci)
          (mk_dg_man d global_of) σ
          [entry_alt (declared_global p) p ci d (genv global_of σ)] pub"
    and place_enter_deps:
      "⋀p ci d σ. ∃deps. enter_deps (enter⇧♯ (analysis_spec (declared_global p) p) ci)
          (mk_dg_man d global_of) σ
          [entry_alt (declared_global p) p ci d (genv global_of σ)] deps"
    and place_entry_sound:
      "⋀p ci d σ pub s.
         enter_runs (enter⇧♯ (analysis_spec (declared_global p) p) ci)
           (mk_dg_man d global_of) σ
           [entry_alt (declared_global p) p ci d (genv global_of σ)] pub
         ⟹ genv global_of pub ≤ genv global_of σ
         ⟹ s ∈ gamma_lift γ⇩V (map_lift (rd (declared_global p))
              (place_cmb p d (genv global_of σ)))
         ⟹ s ∈ gamma_lift γ⇩V (map_lift (rd (declared_global p))
                   (place_cmb p
                      (fst (entry_alt (declared_global p) p ci d (genv global_of σ)))
                      (genv global_of σ)))
           ∧ call_enter (declared_global p) (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s
               ∈ gamma_lift γ⇩V (map_lift (rd (declared_global p))
                   (place_cmb p
                      (snd (entry_alt (declared_global p) p ci d (genv global_of σ)))
                      (genv global_of σ)))"
    and place_cmb_bot: "⋀p e. place_cmb p Bot e = Bot"
    and place_init:
      "⋀p. gamma_lift γ⇩V (map_lift (rd (declared_global p)) (Lifted init_st))
         ⊆ gamma_lift γ⇩V (map_lift (rd (declared_global p))
              (place_cmb p (Lifted init_st) (init_env (declared_global p) p)))"
    and empty_rd: "⋀p s. emp p s ⟷ empty⇩V (rd (declared_global p) s)"
    and empty⇩V_sound: "sound_emptiness empty⇩V γ⇩V"
    and seed_ne_buffer_key: "⋀v ctx. seed v ctx ≠ buffer_key"
    and seed_ne_global_of: "⋀v ctx n. seed v ctx ≠ global_of n"
    and classify_proved:
      "⋀c d s. classify c d = Check_Proved ⟹ s ∈ γ⇩V d ⟹ truthy (⟦c⟧⇩e s)"
    and classify_refuted:
      "⋀c d s. classify c d = Check_Refuted ⟹ s ∈ γ⇩V d
         ⟹ ¬ truthy (⟦c⟧⇩e s)"
    and bot_state_empty: "γ⇩V bot_state = {}"
    and init_sound:
      "⋀p. cinit_stores (declared_global p) ⊆ γ⇩V (rd (declared_global p) init_st)"
begin

text ‹The generic contract asks the published emptiness test only to be sound: a
  product of analyses may describe nothing without any one of them saying so. A
  particular instance may still be exact.›

lemmas empty⇩V_soundD = sound_emptinessD [OF empty⇩V_sound]

text ‹
  Termination is a per-program side condition, and this is how a caller decides
  it: run the solver's own executable termination check on this program's
  equations. The premise stays ‹solve_dom› everywhere else, so nothing in the
  soundness argument depends on the check having been run.
›

lemma terminates_of_solve_c:
  assumes "solve_c (equations 𝒢 p) (root_query p) ≠ None"
  shows "terminates 𝒢 p"
  unfolding terminates_def by (rule dom_of_solve_c[OF assms])

text ‹
  An answer of the executable solver is the solve itself, so a run built from that
  answer is \<^const>‹run›, and its program needs no separate termination premise.
›

lemma solve_c_run:
  assumes "solve_c (equations 𝒢 p) (root_query p) = Some sol"
  shows "terminates 𝒢 p" and "solved_run_of 𝒢 p sol = run 𝒢 p"
  using assms terminates_of_solve_c solve_of_solve_c[OF assms]
  by (simp_all add: run_def solution_def)

lemma vars_finite_of_terminates:
  assumes "terminates 𝒢 p"
  shows "finite (sol_vars 𝒢 p)"
  using solve_fin[OF assms[unfolded terminates_def]]
  by (simp add: sol_vars_def solution_def)

text ‹
  The contexts a concrete call is admitted at under an entry-state policy: every
  context the entered state routes to. This is a top-level constant rather than
  something read out of a per-program interpretation, because an analysis
  publishes it -- a caller stating a context-indexed collecting fact has to name
  the relation those contexts are indexed by, and an example checking a routing
  decision has to name it too.

  With one alternative per call it is one context per abstract caller state; it
  is still a relation and not a function because several concrete callers sharing
  one abstract state reach the same context.
›

definition admitted_contexts :: "(vname ⇒ bool) ⇒ imp_prog ⇒ 'c context_policy" where
  "admitted_contexts 𝒢 p =
     routed_entry_context_rel
       (λci d. [entry_alt 𝒢 p ci d (sol_global 𝒢 p)])
       (λd e. gamma_lift γ⇩V (map_lift (rd 𝒢) (place_cmb p d e)))
       (sol_env 𝒢 p) global_of (route 𝒢)"

subsection ‹What the assembly derives, for one program›

text ‹
  Fixing one program ‹p›, this part equates the published table with the solved
  reader, puts the solver's answer in the routed spine's shape, and states routed
  soundness for any relation of admitted contexts.
›

context
  fixes p :: imp_prog
begin

abbreviation (input) pgs :: "vname ⇒ bool" where "pgs ≡ declared_global p"
  ― ‹input-only, so interpreted facts print ‹declared_global p››

text ‹What a carrier state describes, published and concretized, and what a point's
  two halves describe once recombined against the solved global.›

abbreviation cgam :: "'s lifted ⇒ store set" where
  "cgam d ≡ gamma_lift γ⇩V (map_lift (rd pgs) d)"

abbreviation (input) pgam :: "'s lifted ⇒ ('n ⇒ 's lifted) ⇒ store set" where
  "pgam d e ≡ cgam (place_cmb p d e)"

abbreviation (input) gsol :: "'n ⇒ 's lifted" where
  "gsol ≡ sol_global pgs p"

abbreviation entered :: "call_info ⇒ 's lifted ⇒ 's lifted" where
  "entered ci d ≡ entry_of pgs p ci d gsol"

lemma empty_rd_exact: "emp p s = empty⇩V (rd pgs s)"
  by (simp add: empty_rd)

lemma dg_spec_wf_analysis_spec [intro, simp]: "dg_spec_wf (analysis_spec pgs p)"
  by (rule analysis_contract.spec_wf[OF place_contract])

lemma pgam_Bot [simp]: "pgam Bot g = {}"
  by (simp add: place_cmb_bot)

text ‹
  The published table and the solved reader describe the same stores at every
  key. A caller states soundness against \<^const>‹lookup_table› of the result
  table, while the routed endpoints are stated against the reader; this is the
  equation between them, and it needs no coverage premise. At a covered key it
  is publication commuting with the normalization; at an uncovered one it is
  \<^const>‹Bot› against \<^const>‹Bot›, and both describe nothing.
›

lemma gamma_reader_eq_lookup:
  "pgam (reader pgs p (Inl (v, ctx))) gsol
     = gamma_lift γ⇩V (lookup_table (result pgs p) v ctx)"
proof -
  have gc: "gamma_lift γ⇩V (canonicalize_lift empty⇩V x) = gamma_lift γ⇩V x" for x
    by (rule gamma_lift_canonicalize_lift) (rule empty⇩V_soundD)
  show ?thesis
  proof (cases "(v, ctx) ∈ sol_vars pgs p")
    case True
    then show ?thesis
      by (simp add: reader_def result_def sol_vars_def sol_env_def sol_global_def gc
          map_lift_canonicalize_lift[of "emp p" "empty⇩V" "rd pgs", OF empty_rd_exact])
  next
    case False
    then show ?thesis by (simp add: reader_def result_def sol_vars_def bot_lifted_eq)
  qed
qed

subsubsection ‹The solver's answer, in the shape the routed spine consumes›

text ‹
  An analysis solves the buffered generator -- a node with several intra
  predecessors or several returning calls publishes its analysis-wide
  contribution once per evaluation rather than once per contribution -- while the
  framework states its soundness over the unbuffered one. ‹pp_routed› is that
  reconciliation at this pipeline's own equations, which the placement owes.
›

lemma pp_buffered:
  assumes solves: "terminates pgs p"
  shows "part_post_solution (equations pgs p) (root_query p)
           (sol_env pgs p) (sol_vars pgs p)"
  using solve_pp[OF solves[unfolded terminates_def]]
  by (simp add: sol_env_def sol_vars_def solution_def)

theorem pp_routed:
  assumes solves: "terminates pgs p"
  shows "part_post_solution
     (routed_node_rhs intra_predecessor_addr_list call_site_list (λ_. buffer_key) (route pgs)
        (λctx' src a. dg_spec_edge_program (analysis_spec pgs p) a src global_of)
        (routed_call_program (analysis_spec pgs p) global_of seed
           (static_resolve (prog_cfg p)) (λd. d = Bot))
        (routed_entry_seed_programs seed)
        (prog_cfg p) Bot (Lifted init_st) (place_rg pgs (Lifted init_st)))
     (root_query p) (sol_env pgs p) (sol_vars pgs p)"
  using part_post_solution_with_init[OF pp_buffered[OF solves, unfolded equations_def]]
  unfolding compiled_routed_eqs_for_def bot_lifted_eq
  by (rule pp_routed_of_buffered[OF dg_spec_wf_analysis_spec seed_ne_buffer_key])

text ‹
  The run starts below the solved environment once the solve covers the program
  entry: the entry node publishes the placement's initial global part at its own
  key, and each listed initial value at its name's key.
›

lemma init_publication_le_sol:
  assumes solves: "terminates pgs p"
    and entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ sol_vars pgs p"
    and mem: "(n, d) ∈ set (place_inits pgs p)"
  shows "d ≤ gsol n"
proof -
  have pp: "part_post_solution (equations pgs p) (root_query p) (sol_env pgs p) (sol_vars pgs p)"
    by (rule pp_buffered[OF solves])
  have "DG Bot d ≤ sol_env pgs p (Inr (global_of n))"
    by (rule post_bounded_with_init_at[OF post_bounded_of_part_post_solution[OF pp,
          unfolded equations_def] entry_cov])
       (use mem in ‹auto simp: init_publications_def›)
  then show ?thesis by (simp add: sol_global_def less_eq_dg_state_def)
qed

lemma foldr_init_le:
  "∀(m, d) ∈ set xs. d ≤ f m
     ⟹ (⨆(m, d)←filter (λ(m, d). m = n) xs. d) ≤ (f n :: 's lifted)"
  by (induction xs) auto

lemma init_env_le_sol:
  assumes solves: "terminates pgs p"
    and entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ sol_vars pgs p"
    and own: "place_rg pgs (Lifted init_st) ≤ dg_global (sol_env pgs p (Inr buffer_key))"
  shows "init_env pgs p ≤ gsol"
proof (rule le_funI)
  fix n
  have "(⨆(m, d)←filter (λ(m, d). m = n) (place_inits pgs p). d) ≤ gsol n"
    by (rule foldr_init_le) (use init_publication_le_sol[OF solves entry_cov] in blast)
  moreover have "(if global_of n = buffer_key then place_rg pgs (Lifted init_st) else Bot)
                   ≤ gsol n"
    using own by (auto simp: sol_global_def)
  ultimately show "init_env pgs p n ≤ gsol n"
    unfolding init_env_def by simp
qed

subsubsection ‹The one entry alternative this carrier answers with›

text ‹
  The specification's entry answers with a single alternative, the recombined
  caller state and the callee frame entered from it, each split back by the
  placement. ‹entry_cover› is the only fact about it any context policy needs,
  namely that a concrete call from a described caller lands in the described
  callee.
›

text ‹
  What a call publishes on entry is below the solved global, once the node the
  call returns to is solved: that node's equation runs the call, and a
  post-solution bounds what every solved equation publishes.
›

lemma enter_pub_le_sol:
  assumes solves: "terminates pgs p"
    and cont: "(k, ctx) ∈ sol_vars pgs p"
    and ce: "(u, ca, FunctionEntry q, k) ∈ calls (prog_cfg p)"
    and R: "enter_runs (enter⇧♯ (analysis_spec pgs p) (call_info_of ca q))
              (mk_dg_man (dg_local (sol_env pgs p (Inl (u, ctx)))) global_of)
              (sol_env pgs p) pairs pub"
  shows "genv global_of pub ≤ gsol"
proof (rule le_funI)
  fix n
  let ?K = "Inr (global_of n)"
  let ?σ = "sol_env pgs p"
  let ?callee = "routed_callee_call_program (analysis_spec pgs p) global_of seed (route pgs)
                   (λd. d = Bot) ctx ca u (dg_local (?σ (Inl (u, ctx)))) q"
  let ?call = "routed_call_program (analysis_spec pgs p) global_of seed
                 (static_resolve (prog_cfg p)) (λd. d = Bot) (route pgs) ctx ca u k"
  let ?contribs = "routed_contribution_programs intra_predecessor_addr_list call_site_list (route pgs)
        (λctx' src a. dg_spec_edge_program (analysis_spec pgs p) a src global_of)
        (routed_call_program (analysis_spec pgs p) global_of seed
           (static_resolve (prog_cfg p)) (λd. d = Bot))
        (routed_entry_seed_programs seed) (prog_cfg p) ctx k"
  let ?rhs = "routed_node_rhs intra_predecessor_addr_list call_site_list (λ_. buffer_key) (route pgs)
        (λctx' src a. dg_spec_edge_program (analysis_spec pgs p) a src global_of)
        (routed_call_program (analysis_spec pgs p) global_of seed
           (static_resolve (prog_cfg p)) (λd. d = Bot))
        (routed_entry_seed_programs seed)
        (prog_cfg p) Bot (Lifted init_st) (place_rg pgs (Lifted init_st))"
  have fin: "finite (calls (prog_cfg p))"
    unfolding prog_cfg_def by (simp add: compile_prog_finite)
  have wf: "∀t ∈ set ?contribs. sp_wf t"
    by (rule routed_contribution_programs_wf) auto
  have "pub ?K ≤ sides_of_program ?callee ?σ ?K"
    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 "… ≤ sides_of_program ?call ?σ ?K"
    by (rule routed_call_program_sides_ge_at[OF dg_spec_wf_analysis_spec])
       (use ce fin in simp)
  also have "… ≤ sides_of_program (side_rhs_fold_dg
      (if k = cfg_entry (prog_cfg p) then Bot ⊔ Lifted init_st else Bot) ?contribs)
      ?σ ?K"
  proof (rule sides_le_side_rhs_fold_dg[OF wf])
    have "(u, ca) ∈ set (call_site_list (prog_cfg p) k)" using ce fin by auto
    then show "?call ∈ set ?contribs" by (rule routed_contribution_programs_combineI)
  qed
  also have "… ≤ sides_of_rhs (?rhs (k, ctx)) ?σ ?K"
    unfolding routed_node_rhs_def Let_def
    by (cases "k = cfg_entry (prog_cfg p)") (auto simp: Let_def)
  also have "… ≤ ?σ ?K"
    using pp_routed[OF solves] cont by (blast dest: le_funD)
  finally show "genv global_of pub n ≤ gsol n"
    unfolding sol_global_def by (simp add: less_eq_dg_state_def)
qed

lemma entry_cover:
  assumes solves: "terminates pgs p"
    and cont: "(k, ctx) ∈ sol_vars pgs p"
    and ce: "(u, CallEdge dst pars args, FunctionEntry q, k) ∈ calls (prog_cfg p)"
    and sin: "s ∈ pgam (dg_local (sol_env pgs p (Inl (u, ctx)))) gsol"
  shows "entry_pairs_cover (λd. pgam d gsol) s (call_enter pgs (CallEdge dst pars args) s)
           [entry_alt pgs p (call_info_of (CallEdge dst pars args) q)
              (dg_local (sol_env pgs p (Inl (u, ctx)))) gsol]"
proof -
  let ?ci = "call_info_of (CallEdge dst pars args) q"
  let ?d = "dg_local (sol_env pgs p (Inl (u, ctx)))"
  let ?alt = "entry_alt pgs p ?ci ?d gsol"
  obtain pub where R: "enter_runs (enter⇧♯ (analysis_spec pgs p) ?ci)
      (mk_dg_man ?d global_of) (sol_env pgs p)
      [entry_alt pgs p ?ci ?d (genv global_of (sol_env pgs p))] pub"
    using place_enter_runs by blast
  have le: "genv global_of pub ≤ genv global_of (sol_env pgs p)"
    using enter_pub_le_sol[OF solves cont ce R] by (simp add: sol_global_def)
  have "s ∈ pgam (fst ?alt) gsol ∧ call_enter pgs (CallEdge dst pars args) s ∈ pgam (snd ?alt) gsol"
    using place_entry_sound[OF R le sin[unfolded sol_global_def]]
    unfolding sol_global_def by (simp del: declared_global_iff)
  then show ?thesis
    by (intro entry_pairs_coverI[of "fst ?alt" "snd ?alt"]) simp_all
qed

subsubsection ‹The routed soundness statement, at any admitted-context relation›

text ‹
  Which contexts a concrete call is admitted at is the one thing a context policy
  still chooses, so ‹adm› is a parameter here rather than a derived object. What
  the policy owes about it is exactly two facts: a context ‹adm› admits is the one
  this pipeline's route computes on the entered state, at a covered unknown
  (‹cover_R›); and ‹adm› admits at least one context for every concrete call at a
  covered call site (‹total_R›). Everything else below is fixed by the pipeline.
›

text ‹
  The specification is sound for the recombined concretization; the placement
  owes this, so the routed statement below never re-derives it.
›

interpretation dg_base: analysis_contract "analysis_spec pgs p" "λd e. pgam d e" pgs
  by (rule place_contract)

lemma routed_analysis_sound_of_live:
  fixes adm :: "'c context_policy"
  assumes solves: "terminates pgs p"
    and fwd_ok: "⋀u a v ctx. (u, ctx) ∈ sol_vars pgs p
        ⟹ dg_local (sol_env pgs p (Inl (u, ctx))) ≠ Bot
        ⟹ (u, a, v) ∈ intra (prog_cfg p) ⟹ (v, ctx) ∈ sol_vars pgs p"
    and comb_fwd_ok: "⋀cl c1 dst pars args q cont. (cl, c1) ∈ sol_vars pgs p
        ⟹ (cl, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ (cont, c1) ∈ sol_vars pgs p"
    and cover_R: "⋀u ctx dst pars args q cont s ctx'.
        (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ ctx' ∈ adm u ctx (call_info_of (CallEdge dst pars args) q) s
              (call_enter pgs (CallEdge dst pars args) s)
        ⟹ entered (call_info_of (CallEdge dst pars args) q)
              (dg_local (sol_env pgs p (Inl (u, ctx)))) ≠ Bot
        ⟹ route pgs u ctx
                (entered (call_info_of (CallEdge dst pars args) q)
                   (dg_local (sol_env pgs p (Inl (u, ctx)))))
                (CallEdge dst pars args) = ctx'
            ∧ (FunctionEntry q, ctx') ∈ sol_vars pgs p"
    and total_R: "⋀u ctx dst pars args q cont s.
        (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ s ∈ pgam (dg_local (sol_env pgs p (Inl (u, ctx)))) gsol
        ⟹ adm u ctx (call_info_of (CallEdge dst pars args) q) s
                      (call_enter pgs (CallEdge dst pars args) s) ≠ {}"
  shows "routed_analysis (analysis_spec pgs p) (λd e. pgam d e) pgs (prog_cfg p)
     buffer_key global_of
     (route pgs) Bot (Lifted init_st) (place_rg pgs (Lifted init_st)) (sol_env pgs p)
     (sol_vars pgs p) (root_query p)
     seed (λd. d = Bot) adm (λd e. map_lift (rd pgs) (place_cmb p d e)) γ⇩V empty⇩V
     classify"
proof (unfold_locales, goal_cases CmbWf ExtraWf FinE PP SgCov SgUncov Fwd FinC CallsUnique
    SeedUnknown SeedNeGlobal IsBotBot IsBotSound ResolveSound EnterCover EnterTotal CombFwd GammaRd
    EmptyExact ClProved ClRefuted VarsFin)
  case CmbWf show ?case by (rule sp_wf_routed_call_program[OF dg_spec_wf_analysis_spec])
next
  case ExtraWf then show ?case by (rule sp_wf_routed_entry_seed_programs)
next
  case FinE show ?case unfolding prog_cfg_def by (simp add: compile_prog_finite)
next
  case PP show ?case by (rule post_bounded_of_part_post_solution[OF pp_routed[OF solves]])
next
  case (SgCov v c) then show ?case by simp
next
  case (SgUncov v c) then show ?case by (simp add: bot_lifted_eq)
next
  case (Fwd u a v c)
  have "dg_local (sol_env pgs p (Inl (u, c))) ≠ Bot"
    using Fwd(2) by auto
  with Fwd(1,3) show ?case by (blast intro: fwd_ok)
next
  case FinC show ?case unfolding prog_cfg_def by (simp add: compile_prog_finite)
next
  case CallsUnique show ?case
    unfolding calls_source_unique_def prog_cfg_def
    using compile_prog_calls_source_unique by blast
next
  case (SeedUnknown q ctx) show ?case by (rule seed_ne_buffer_key)
next
  case (SeedNeGlobal q ctx v) show ?case by (rule seed_ne_global_of)
next
  case IsBotBot show ?case by simp
next
  case (IsBotSound d g') then show ?case by simp
next
  case (ResolveSound u ctx dst pars args q cont s)
  then show ?case unfolding prog_cfg_def by (simp add: compile_prog_finite)
next
  case (EnterCover u ctx dst pars args q cont s ctx')
  let ?ci = "call_info_of (CallEdge dst pars args) q"
  let ?caller = "dg_local (sol_env pgs p (Inl (u, ctx)))"
  let ?g = "genv global_of (sol_env pgs p)"
  have sin: "s ∈ pgam ?caller gsol"
    using EnterCover(3) by (simp add: sol_global_def)
  have cov: "entry_pairs_cover (λd. pgam d gsol) s
      (call_enter pgs (CallEdge dst pars args) s) [entry_alt pgs p ?ci ?caller gsol]"
    by (rule entry_cover[OF solves comb_fwd_ok[OF EnterCover(1,2)] EnterCover(2) sin])
  obtain c e where ce: "entry_alt pgs p ?ci ?caller gsol = (c, e)"
    by (cases "entry_alt pgs p ?ci ?caller gsol")
  have nbE: "entered ?ci ?caller ≠ Bot"
  proof
    assume "entered ?ci ?caller = Bot"
    with cov ce show False by (simp add: entry_pairs_cover_def entry_of_def place_cmb_bot)
  qed
  have req: "route pgs u ctx (entered ?ci ?caller) (CallEdge dst pars args) = ctx'"
    and covE: "(FunctionEntry q, ctx') ∈ sol_vars pgs p"
    using cover_R[OF EnterCover(1,2,4) nbE] by blast+
  obtain pub where runs: "enter_runs (enter⇧♯ (analysis_spec pgs p) ?ci)
      (mk_dg_man ?caller global_of) (sol_env pgs p)
      [entry_alt pgs p ?ci ?caller ?g] pub"
    using place_enter_runs by blast
  obtain deps where deps: "enter_deps (enter⇧♯ (analysis_spec pgs p) ?ci)
      (mk_dg_man ?caller global_of) (sol_env pgs p)
      [entry_alt pgs p ?ci ?caller ?g] deps"
    using place_enter_deps by blast
  have ce': "entry_alt pgs p ?ci ?caller ?g = (c, e)"
    using ce by (simp add: sol_global_def)
  have sc: "s ∈ pgam c ?g" and ec: "call_enter pgs (CallEdge dst pars args) s ∈ pgam e ?g"
    using cov ce by (simp_all add: entry_pairs_cover_def sol_global_def)
  have re: "route pgs u ctx e (CallEdge dst pars args) = ctx'"
    using req ce by (simp add: entry_of_def)
  show ?case
    using runs deps sc ec re covE unfolding ce' by fastforce
next
  case (EnterTotal u ctx dst pars args q cont s)
  then show ?case by (intro total_R) (simp_all add: sol_global_def)
next
  case (CombFwd cl c1 dst pars args q cont)
  then show ?case by (rule comb_fwd_ok)
next
  case (GammaRd d g') show ?case by simp
next
  case (EmptyExact v) then show ?case by (rule empty⇩V_soundD)
next
  case (ClProved c d s) then show ?case by (rule classify_proved)
next
  case (ClRefuted c d s) then show ?case by (rule classify_refuted)
next
  case VarsFin show ?case by (rule vars_finite_of_terminates[OF solves])
qed

lemma routed_analysis_sound_of:
  fixes adm :: "'c context_policy"
  assumes solves: "terminates pgs p"
    and fwd_ok: "⋀u a v ctx. (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, a, v) ∈ intra (prog_cfg p) ⟹ (v, ctx) ∈ sol_vars pgs p"
    and comb_fwd_ok: "⋀cl c1 dst pars args q cont. (cl, c1) ∈ sol_vars pgs p
        ⟹ (cl, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ (cont, c1) ∈ sol_vars pgs p"
    and cover_R: "⋀u ctx dst pars args q cont s ctx'.
        (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ ctx' ∈ adm u ctx (call_info_of (CallEdge dst pars args) q) s
              (call_enter pgs (CallEdge dst pars args) s)
        ⟹ route pgs u ctx
                (entered (call_info_of (CallEdge dst pars args) q)
                   (dg_local (sol_env pgs p (Inl (u, ctx)))))
                (CallEdge dst pars args) = ctx'
            ∧ (FunctionEntry q, ctx') ∈ sol_vars pgs p"
    and total_R: "⋀u ctx dst pars args q cont s.
        (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ s ∈ pgam (dg_local (sol_env pgs p (Inl (u, ctx)))) gsol
        ⟹ adm u ctx (call_info_of (CallEdge dst pars args) q) s
                      (call_enter pgs (CallEdge dst pars args) s) ≠ {}"
  shows "routed_analysis (analysis_spec pgs p) (λd e. pgam d e) pgs (prog_cfg p)
     buffer_key global_of
     (route pgs) Bot (Lifted init_st) (place_rg pgs (Lifted init_st)) (sol_env pgs p)
     (sol_vars pgs p) (root_query p)
     seed (λd. d = Bot) adm (λd e. map_lift (rd pgs) (place_cmb p d e)) γ⇩V empty⇩V
     classify"
  by (rule routed_analysis_sound_of_live [where adm = adm, OF solves _ comb_fwd_ok _ total_R])
     (blast intro: fwd_ok dest: cover_R)+

subsubsection ‹The published endpoint, under termination and coverage›

text ‹
  Under termination and closure of the solved keys, ‹activation_collect_sound_of›
  bounds every admitted activation by the solved table's entry at its context.
›

lemma cinit_le_init: "cinit_stores pgs ⊆ pgam (Lifted init_st) (init_env pgs p)"
  using init_sound[of p] place_init[of p] by auto

text ‹
  Every activation the activation-trace semantics admits at a context is described by the
  solved table's entry for that context. The coverage premises are the shape a
  solver's own reachable set supplies: an edge out of an unknown the solve
  visited lands on one it also visited.
›

lemma activation_collect_sound_of:
  fixes adm :: "'c context_policy"
  assumes solves: "terminates pgs p"
    and entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ sol_vars pgs p"
    and fwd_ok: "⋀u a v ctx. (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, a, v) ∈ intra (prog_cfg p) ⟹ (v, ctx) ∈ sol_vars pgs p"
    and comb_fwd_ok: "⋀cl c1 dst pars args q cont. (cl, c1) ∈ sol_vars pgs p
        ⟹ (cl, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ (cont, c1) ∈ sol_vars pgs p"
    and cover_R: "⋀u ctx dst pars args q cont s ctx'.
        (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ ctx' ∈ adm u ctx (call_info_of (CallEdge dst pars args) q) s
              (call_enter pgs (CallEdge dst pars args) s)
        ⟹ route pgs u ctx
                (entered (call_info_of (CallEdge dst pars args) q)
                   (dg_local (sol_env pgs p (Inl (u, ctx)))))
                (CallEdge dst pars args) = ctx'
            ∧ (FunctionEntry q, ctx') ∈ sol_vars pgs p"
    and total_R: "⋀u ctx dst pars args q cont s.
        (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ s ∈ pgam (dg_local (sol_env pgs p (Inl (u, ctx)))) gsol
        ⟹ adm u ctx (call_info_of (CallEdge dst pars args) q) s
                      (call_enter pgs (CallEdge dst pars args) s) ≠ {}"
  shows "𝒜⇘pgs,adm,root_ctx,prog_cfg p,cinit_stores pgs⇙ v ctx
           ⊆ pgam (reader pgs p (Inl (v, ctx))) gsol"
proof -
  interpret adapter: routed_analysis "analysis_spec pgs p" "λd e. pgam d e" pgs
      "prog_cfg p" buffer_key global_of "route pgs" Bot "Lifted init_st"
      "place_rg pgs (Lifted init_st)" "sol_env pgs p" "sol_vars pgs p" "root_query p" seed
      "λd. d = Bot" adm "λd e. map_lift (rd pgs) (place_cmb p d e)" γ⇩V empty⇩V classify
    by (rule routed_analysis_sound_of
          [where adm = adm, OF solves fwd_ok comb_fwd_ok cover_R total_R])
  have init_env_le: "init_env pgs p ≤ genv global_of (sol_env pgs p)"
    using init_env_le_sol[OF solves entry_cov adapter.pp_entry_init_global_bound[OF entry_cov]]
    by (simp add: sol_global_def)
  show ?thesis
    using adapter.activation_collect_dg_sound[OF entry_cov _ init_env_le, of "cinit_stores pgs" v
      ctx]
      cinit_le_init
    by (simp add: reader_def sol_global_def)
qed

subsubsection ‹The two context policies this assembly supports›

text ‹
  ‹entry_context_rel› is the relation an entry-state policy induces: a concrete
  call is admitted at every context some covering alternative of the entry answer
  routes to. With one alternative per call that is a single context per abstract
  caller state, but several concrete callers sharing an abstract state may still
  reach one context, which is exactly why a relation and not a function.
›

lemma admitted_contexts_alt:
  "admitted_contexts pgs p =
     routed_entry_context_rel (λci d. [entry_alt pgs p ci d gsol]) (λd e. pgam d e)
       (sol_env pgs p) global_of (route pgs)"
  by (simp add: admitted_contexts_def)

abbreviation entry_context_rel :: "'c context_policy" where
  "entry_context_rel ≡ admitted_contexts pgs p"

text ‹
  How a caller shows that this call is admitted at the context it computed: the
  concrete caller store is described by the recombined caller, and the entered
  store by the callee frame entered from it, each recombined against the solved
  global. The single alternative means a witness never has to name the
  alternatives list.
›

lemma admitted_contextsI:
  assumes caller: "s ∈ pgam (fst (entry_alt pgs p ci (dg_local (sol_env pgs p (Inl (u, ctx)))) gsol))
                     gsol"
    and entered_in: "s' ∈ pgam (entered ci (dg_local (sol_env pgs p (Inl (u, ctx))))) gsol"
  shows "route pgs u ctx (entered ci (dg_local (sol_env pgs p (Inl (u, ctx)))))
             (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci))
           ∈ entry_context_rel u ctx ci s s'"
  unfolding admitted_contexts_alt
  by (rule routed_entry_context_relI
        [where cont = "fst (entry_alt pgs p ci (dg_local (sol_env pgs p (Inl (u, ctx)))) gsol)"])
     (use caller entered_in in ‹simp_all add: entry_of_def sol_global_def›)

text ‹
  The same fact with the call action spelled as the caller has it. A witness
  names a literal \<^const>‹CallEdge›, while the rule above reconstructs one from
  the \<^type>‹call_info›'s three projections, and ⬚‹rule› does not reduce the
  projections. Every concrete instance wants this shape.
›

lemma admitted_contextsI_call:
  assumes caller: "s ∈ pgam (fst (entry_alt pgs p (call_info_of (CallEdge dst pars args) q)
                       (dg_local (sol_env pgs p (Inl (u, ctx)))) gsol)) gsol"
    and entered_in: "s' ∈ pgam (entered (call_info_of (CallEdge dst pars args) q)
                           (dg_local (sol_env pgs p (Inl (u, ctx))))) gsol"
  shows "route pgs u ctx
             (entered (call_info_of (CallEdge dst pars args) q)
                (dg_local (sol_env pgs p (Inl (u, ctx)))))
             (CallEdge dst pars args)
           ∈ entry_context_rel u ctx (call_info_of (CallEdge dst pars args) q) s s'"
  using admitted_contextsI[OF caller entered_in] by simp

lemma entry_state_routed_analysis_sound:
  assumes solves: "terminates pgs p"
    and fwd_ok: "⋀u a v ctx. (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, a, v) ∈ intra (prog_cfg p) ⟹ (v, ctx) ∈ sol_vars pgs p"
    and call_fwd_ok: "⋀u ctx dst pars args q cont. (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ (FunctionEntry q,
               route pgs u ctx
                 (entered (call_info_of (CallEdge dst pars args) q)
                    (dg_local (sol_env pgs p (Inl (u, ctx)))))
                 (CallEdge dst pars args))
              ∈ sol_vars pgs p"
    and comb_fwd_ok: "⋀cl c1 dst pars args q cont. (cl, c1) ∈ sol_vars pgs p
        ⟹ (cl, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ (cont, c1) ∈ sol_vars pgs p"
  shows "routed_analysis (analysis_spec pgs p) (λd e. pgam d e) pgs (prog_cfg p)
     buffer_key global_of
     (route pgs) Bot (Lifted init_st) (place_rg pgs (Lifted init_st)) (sol_env pgs p)
     (sol_vars pgs p) (root_query p)
     seed (λd. d = Bot) entry_context_rel
     (λd e. map_lift (rd pgs) (place_cmb p d e)) γ⇩V empty⇩V classify"
proof (rule routed_analysis_sound_of
    [where adm = entry_context_rel, OF solves fwd_ok comb_fwd_ok])
  fix u ctx dst pars args q cont and s :: store and ctx'
  assume covV: "(u, ctx) ∈ sol_vars pgs p"
    and ce: "(u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)"
    and Rc: "ctx' ∈ entry_context_rel u ctx (call_info_of (CallEdge dst pars args) q) s
               (call_enter pgs (CallEdge dst pars args) s)"
  let ?ci = "call_info_of (CallEdge dst pars args) q"
  let ?caller = "dg_local (sol_env pgs p (Inl (u, ctx)))"
  from Rc[unfolded admitted_contexts_alt] obtain cont' entry
    where mem: "(cont', entry) ∈ set [entry_alt pgs p ?ci ?caller gsol]"
      and req0: "ctx' = route pgs u ctx entry
                   (CallEdge (ci_dst ?ci) (ci_formals ?ci) (ci_args ?ci))"
    by (rule routed_entry_context_relE)
  have "entry = entered ?ci ?caller" using mem by (simp add: entry_of_def) (metis snd_conv)
  with req0 have req: "route pgs u ctx (entered ?ci ?caller) (CallEdge dst pars args) = ctx'"
    by simp
  show "route pgs u ctx (entered ?ci ?caller) (CallEdge dst pars args) = ctx'
          ∧ (FunctionEntry q, ctx') ∈ sol_vars pgs p"
    using req call_fwd_ok[OF covV ce] by simp
next
  fix u ctx dst pars args q cont and s :: store
  assume covV: "(u, ctx) ∈ sol_vars pgs p"
    and ce: "(u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)"
    and sin: "s ∈ pgam (dg_local (sol_env pgs p (Inl (u, ctx)))) gsol"
  show "entry_context_rel u ctx (call_info_of (CallEdge dst pars args) q) s
                 (call_enter pgs (CallEdge dst pars args) s) ≠ {}"
    unfolding admitted_contexts_alt
    by (rule routed_entry_context_rel_total)
       (use entry_cover[OF solves comb_fwd_ok[OF covV ce] ce sin]
         in ‹simp add: sol_global_def del: declared_global_iff›)
qed

text ‹
  The two endpoints an entry-state caller consumes: the per-context collecting
  bound, and the existence of a context for every valid activation trace, which a
  source-level caller needs to name a context witness at all. Both are the
  routed spine's own theorems at the interpretation just established.
›

context
  assumes solves: "terminates pgs p"
    and fwd_ok: "⋀u a v ctx. (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, a, v) ∈ intra (prog_cfg p) ⟹ (v, ctx) ∈ sol_vars pgs p"
    and call_fwd_ok: "⋀u ctx dst pars args q cont. (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ (FunctionEntry q,
               route pgs u ctx
                 (entered (call_info_of (CallEdge dst pars args) q)
                    (dg_local (sol_env pgs p (Inl (u, ctx)))))
                 (CallEdge dst pars args))
              ∈ sol_vars pgs p"
    and comb_fwd_ok: "⋀cl c1 dst pars args q cont. (cl, c1) ∈ sol_vars pgs p
        ⟹ (cl, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ (cont, c1) ∈ sol_vars pgs p"
begin

interpretation entry: routed_analysis "analysis_spec pgs p" "λd e. pgam d e" pgs
    "prog_cfg p" buffer_key global_of "route pgs" Bot "Lifted init_st"
    "place_rg pgs (Lifted init_st)" "sol_env pgs p" "sol_vars pgs p" "root_query p" seed
    "λd. d = Bot" entry_context_rel "λd e. map_lift (rd pgs) (place_cmb p d e)"
    γ⇩V empty⇩V classify
  by (rule entry_state_routed_analysis_sound [OF solves fwd_ok call_fwd_ok comb_fwd_ok])

lemma entry_init_env_le:
  assumes entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ sol_vars pgs p"
  shows "init_env pgs p ≤ genv global_of (sol_env pgs p)"
  using init_env_le_sol[OF solves entry_cov entry.pp_entry_init_global_bound[OF entry_cov]]
  by (simp add: sol_global_def)

corollary entry_state_activation_collect_sound:
  assumes entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ sol_vars pgs p"
  shows "𝒜⇘pgs,entry_context_rel,root_ctx,prog_cfg p,cinit_stores pgs⇙ v ctx
           ⊆ pgam (reader pgs p (Inl (v, ctx))) gsol"
  using entry.activation_collect_dg_sound
      [OF entry_cov _ entry_init_env_le[OF entry_cov], of "cinit_stores pgs" v ctx]
    cinit_le_init
  by (simp add: reader_def sol_global_def)

theorem entry_state_has_context:
  assumes entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ sol_vars pgs p"
    and trace: "t ∈ 𝒯⇘pgs,prog_cfg p,cinit_stores pgs⇙"
  shows "∃c. activation_context_rel pgs entry_context_rel root_ctx (prog_cfg p) t c"
  using entry.routed_valid_activation_trace_has_context
      [OF entry_cov _ entry_init_env_le[OF entry_cov] trace] cinit_le_init
  by simp

text ‹
  The two together: covering the entry is enough for the activation buckets to
  exhaust the context-insensitive collection, so a caller holding only a
  \<^const>‹node_collect› membership -- which is what a source run delivers -- can
  pass to the bucket its own call history produced.  Without this the per-context
  bounds above say nothing about a run whose context is not known in advance.
›

theorem entry_state_node_collect_eq_Union:
  assumes entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ sol_vars pgs p"
  shows "𝒞⇘pgs,prog_cfg p,cinit_stores pgs⇙ v
           = (⋃ctx. 𝒜⇘pgs,entry_context_rel,root_ctx,prog_cfg p,cinit_stores pgs⇙ v ctx)"
  by (rule node_collect_eq_Union_activation_of_has_context)
     (rule entry_state_has_context [OF entry_cov])

end

text ‹
  A route that never reads the state it is handed is a function of the call site
  and the caller's context alone, so the contexts it admits are the graph of a
  context function on concrete stores -- the shape the call-string and
  context-insensitive policies both publish. ‹route_const› is the whole of what
  such a policy owes; ‹ctx_fun› is its trace-semantic counterpart.
›

corollary fun_route_activation_collect_sound:
  fixes ctx_fun :: "cfg_node ⇒ 'c ⇒ store ⇒ 'c"
  assumes route_const: "⋀u ctx d ca s. route pgs u ctx d ca = ctx_fun u ctx s"
    and solves: "terminates pgs p"
    and fwd_ok: "⋀u a v ctx. (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, a, v) ∈ intra (prog_cfg p) ⟹ (v, ctx) ∈ sol_vars pgs p"
    and call_fwd_ok: "⋀u ctx dst pars args q cont d. (u, ctx) ∈ sol_vars pgs p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ (FunctionEntry q, route pgs u ctx d (CallEdge dst pars args))
              ∈ sol_vars pgs p"
    and comb_fwd_ok: "⋀cl c1 dst pars args q cont. (cl, c1) ∈ sol_vars pgs p
        ⟹ (cl, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ (cont, c1) ∈ sol_vars pgs p"
    and entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ sol_vars pgs p"
  shows "𝒜⇘pgs,context_policy_of_fun ctx_fun,root_ctx,prog_cfg p,cinit_stores pgs⇙ v ctx
           ⊆ pgam (reader pgs p (Inl (v, ctx))) gsol"
proof (rule activation_collect_sound_of[OF solves entry_cov fwd_ok comb_fwd_ok])
  fix u ctx dst pars args q cont and s :: store and ctx'
  assume covV: "(u, ctx) ∈ sol_vars pgs p"
    and ce: "(u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)"
    and Rc: "ctx' ∈ context_policy_of_fun ctx_fun u ctx
               (call_info_of (CallEdge dst pars args) q) s
               (call_enter pgs (CallEdge dst pars args) s)"
  have req: "route pgs u ctx d (CallEdge dst pars args) = ctx'" for d
    using Rc
    by (simp add: route_const[of _ _ _ _ "call_enter pgs (CallEdge dst pars args) s"])
  show "route pgs u ctx
          (entered (call_info_of (CallEdge dst pars args) q)
             (dg_local (sol_env pgs p (Inl (u, ctx)))))
          (CallEdge dst pars args) = ctx'
        ∧ (FunctionEntry q, ctx') ∈ sol_vars pgs p"
    using req call_fwd_ok[OF covV ce] by simp
next
  fix u ctx dst pars args q cont and s :: store
  show "context_policy_of_fun ctx_fun u ctx
                 (call_info_of (CallEdge dst pars args) q) s
                 (call_enter pgs (CallEdge dst pars args) s) ≠ {}"
    by simp
qed

text ‹
  The functional route's counterpart of the entry-state union. It needs nothing
  at all: \<^const>‹activation_context_of› is total, so every valid activation trace carries a context without
  any coverage having been established.
›

theorem fun_route_node_collect_eq_Union:
  "𝒞⇘pgs,prog_cfg p,cinit_stores pgs⇙ v
     = (⋃ctx. 𝒜⇘pgs,context_policy_of_fun ctx_fun,root_ctx,prog_cfg p,cinit_stores pgs⇙ v ctx)"
  by (rule node_collect_eq_Union_activation_of_fun)

end

end

subsection ‹Every variable in the local half›

text ‹
  The placement every analysis uses unless it shares program globals: the
  specification is the component's own \<^const>‹dg_spec_of›, a point's state is
  its local unknown alone, and nothing is published at the analysis-wide global.
  Its placement obligations follow from the component's soundness and its
  single-alternative entry, so an instance owes exactly what it owed before the
  placement was a parameter.
›

theorem dg_analysis_whole_stateI:
  fixes comp :: "(vname ⇒ bool) ⇒ imp_prog ⇒ 's::semilattice_sup lifted local_spec"
    and seed :: "pp ⇒ 'c ⇒ 'k"
  assumes solver: "certified_solver solve solve_dom solve_c"
    and comp_sound:
      "⋀p. sound_local_spec (declared_global p)
               (λd. gamma_lift γ⇩V (map_lift (rd (declared_global p)) d))
               (comp (declared_global p) p)"
    and enter_single:
      "⋀p ci d. ls_enter (comp (declared_global p) p) (ls_channel (comp (declared_global p) p) d)
                    ci (d, d)
                  = [(d, dg_pipeline.comp_entry comp (declared_global p) p ci d)]"
    and empty_rd: "⋀p s. emp p s ⟷ empty⇩V (rd (declared_global p) s)"
    and empty⇩V_sound: "sound_emptiness empty⇩V γ⇩V"
    and seed_ne: "⋀v ctx. seed v ctx ≠ buffer_key"
    and classify_proved:
      "⋀c d s. classify c d = Check_Proved ⟹ s ∈ γ⇩V d ⟹ truthy (⟦c⟧⇩e s)"
    and classify_refuted:
      "⋀c d s. classify c d = Check_Refuted ⟹ s ∈ γ⇩V d
         ⟹ ¬ truthy (⟦c⟧⇩e s)"
    and bot_state_empty: "γ⇩V bot_state = {}"
    and init_sound:
      "⋀p. cinit_stores (declared_global p) ⊆ γ⇩V (rd (declared_global p) init_st)"
    and seed_ne_global: "⋀v ctx n. seed v ctx ≠ global_of n"
  shows "dg_analysis comp emp rd init_st buffer_key global_of seed
           solve solve_dom bot_state classify γ⇩V empty⇩V solve_c
           (λ𝒢 c. dg_spec_of c) (λ𝒢 d e. d) (λ𝒢 d. d) (λ𝒢 d. Bot) (λ𝒢 p. [])
           (λp ci d e. d)"
proof (rule dg_analysis.intro[OF solver dg_analysis_axioms.intro], goal_cases CompSound
    EnterSingle Contract Runs Deps EntrySound CmbBot Init EmptyRd EmptyV SeedNe SeedNeGlobal
    ClProved ClRefuted BotState InitSound)
  case (CompSound p) show ?case by (rule comp_sound)
next
  case (EnterSingle p ci d) show ?case by (rule enter_single)
next
  case (Contract p) show ?case
    unfolding dg_pipeline.analysis_spec_def by (rule dg_spec_of_contract[OF comp_sound])
next
  case (Runs p ci d σ) show ?case
    by (rule exI, simp add: dg_pipeline.analysis_spec_def dg_spec_of_def enter_single
        dg_pipeline.entry_alt_def, rule enter_runs_local_enter_transfer_mk_dg_man)
next
  case (Deps p ci d σ) show ?case
    by (rule exI, simp add: dg_pipeline.analysis_spec_def dg_spec_of_def enter_single
        dg_pipeline.entry_alt_def, rule enter_deps_local_enter_transfer_mk_dg_man)
next
  case (EntrySound p ci d σ pub s)
  let ?c = "comp (declared_global p) p"
  obtain q where "q ∈ set (ls_enter ?c (ls_channel ?c d) ci (d, d))"
      "s ∈ gamma_lift γ⇩V (map_lift (rd (declared_global p)) (fst q))"
      "call_enter (declared_global p) (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s
         ∈ gamma_lift γ⇩V (map_lift (rd (declared_global p)) (snd q))"
    using comp_sound[of p] EntrySound(3) ls_channel_sound[OF comp_sound[of p]]
    unfolding sound_local_spec_def by (metis fst_conv)
  then show ?case
    by (simp add: enter_single dg_pipeline.entry_alt_def)
next
  case (CmbBot p g) show ?case by simp
next
  case (Init p) show ?case by simp
next
  case (EmptyRd p s) show ?case by (rule empty_rd)
next
  case EmptyV show ?case by (rule empty⇩V_sound)
next
  case (SeedNe v ctx) show ?case by (rule seed_ne)
next
  case (SeedNeGlobal v ctx n) show ?case by (rule seed_ne_global)
next
  case (ClProved c d s) then show ?case by (rule classify_proved)
next
  case (ClRefuted c d s) then show ?case by (rule classify_refuted)
next
  case BotState show ?case by (rule bot_state_empty)
next
  case (InitSound p) show ?case by (rule init_sound)
qed

subsection ‹Program globals keyed by name›

text ‹
  The placement that keeps each program global at its own unknown
  ‹global_of x›. The specification is the component wrapped by the keyed lifter,
  and a point's state is its local half recombined with the solved environment
  over the program's declared globals. The root publishes each declared
  global's initial value at its key, and the node-owned buffer stays empty.

  Beyond the component's own soundness, the carrier owes monotone operations,
  that a name outside a read set is cut below ‹free› of that set, and two facts
  about concretization: the frame law ‹mix› of @{thm [source] keyed_split_contract},
  and that a state is described by its local half recombined with its own cuts.
›

theorem dg_analysis_keyedI:
  fixes comp :: "(vname ⇒ bool) ⇒ imp_prog ⇒ 's::semilattice_sup lifted local_spec"
    and seed :: "pp ⇒ 'c ⇒ 'k"
    and global_of :: "vname ⇒ 'k"
    and cmb :: "'s lifted ⇒ 's lifted ⇒ 's lifted"
    and rg :: "vname ⇒ 's lifted ⇒ 's lifted"
  assumes solver: "certified_solver solve solve_dom solve_c"
    and comp_sound:
      "⋀p. sound_local_spec (declared_global p)
               (λd. gamma_lift γ⇩V (map_lift (rd (declared_global p)) d))
               (comp (declared_global p) p)"
    and enter_single:
      "⋀p ci d. ls_enter (comp (declared_global p) p) (ls_channel (comp (declared_global p) p) d)
                    ci (d, d)
                  = [(d, dg_pipeline.comp_entry comp (declared_global p) p ci d)]"
    and cmb_mono: "⋀d d' g g'. d ≤ d' ⟹ g ≤ g' ⟹ cmb d g ≤ cmb d' g'"
    and cmb_rl: "⋀x g. cmb (rl x) g = cmb x g"
    and rl_cmb: "⋀d g. rl (cmb d g) = rl d"
    and cmb_bot: "⋀g. cmb Bot g = Bot"
    and rg_mono: "⋀x v v'. v ≤ v' ⟹ rg x v ≤ rg x v'"
    and rg_free: "⋀x R v. x ∉ set R ⟹ rg x v ≤ free R"
    and mix: "⋀p l0 e r s s' W.
        s ∈ gamma_lift γ⇩V (map_lift (rd (declared_global p))
               (cmb l0 (full_view rg (declared_global_vars p) e)))
        ⟹ s' ∈ gamma_lift γ⇩V (map_lift (rd (declared_global p)) r)
        ⟹ (∀x. declared_global p x ⟶ x ∉ set W ⟶ s' x = s x)
        ⟹ s' ∈ gamma_lift γ⇩V (map_lift (rd (declared_global p))
               (cmb (rl r) (full_view rg (declared_global_vars p)
                  (λx. if x ∈ set W then rg x r else e x))))"
    and init_view: "⋀p. gamma_lift γ⇩V (map_lift (rd (declared_global p)) (Lifted init_st))
        ⊆ gamma_lift γ⇩V (map_lift (rd (declared_global p))
             (cmb (Lifted init_st) (full_view rg (declared_global_vars p)
                (λx. rg x (Lifted init_st)))))"
    and empty_rd: "⋀p s. emp p s ⟷ empty⇩V (rd (declared_global p) s)"
    and empty⇩V_sound: "sound_emptiness empty⇩V γ⇩V"
    and seed_ne: "⋀v ctx. seed v ctx ≠ buffer_key"
    and seed_ne_global: "⋀v ctx n. seed v ctx ≠ global_of n"
    and classify_proved:
      "⋀c d s. classify c d = Check_Proved ⟹ s ∈ γ⇩V d ⟹ truthy (⟦c⟧⇩e s)"
    and classify_refuted:
      "⋀c d s. classify c d = Check_Refuted ⟹ s ∈ γ⇩V d
         ⟹ ¬ truthy (⟦c⟧⇩e s)"
    and bot_state_empty: "γ⇩V bot_state = {}"
    and init_sound:
      "⋀p. cinit_stores (declared_global p) ⊆ γ⇩V (rd (declared_global p) init_st)"
  shows "dg_analysis comp emp rd init_st buffer_key global_of seed
           solve solve_dom bot_state classify γ⇩V empty⇩V solve_c
           (λp c. keyed_split_spec (declared_global p) cmb rl rg free c)
           (λp d e. cmb d (full_view rg (declared_global_vars p) e)) (λ𝒢. rl) (λ𝒢 d. Bot)
           (λ𝒢 p. map (λx. (x, rg x (Lifted init_st))) (declared_global_vars p))
           (λp ci d e. cmb d (view_of rg (call_global_reads (declared_global p) (ci_args ci)) e
              (free (call_global_reads (declared_global p) (ci_args ci)))))"
proof -
  let ?gm = "λp d. gamma_lift γ⇩V (map_lift (rd (declared_global p)) d)"
  have gm_mono: "⋀p x y. x ≤ y ⟹ ?gm p x ⊆ ?gm p y"
    using comp_sound unfolding sound_local_spec_def by metis
  show ?thesis
  proof (rule dg_analysis.intro[OF solver dg_analysis_axioms.intro], goal_cases CompSound
      EnterSingle Contract Runs Deps EntrySound CmbBot Init EmptyRd EmptyV SeedNe SeedNeGlobal
      ClProved ClRefuted BotState InitSound)
    case (CompSound p) show ?case by (rule comp_sound)
  next
    case (EnterSingle p ci d) show ?case by (rule enter_single)
  next
    case (Contract p) show ?case
      unfolding dg_pipeline.analysis_spec_def
      using comp_sound[where p = p] cmb_mono rg_mono rg_free mix[where p = p]
      by (rule keyed_split_contract)
  next
    case (Runs p ci d σ) show ?case
      using enter_runs_keyed_enter_transfer[of cmb rl rg free
          "call_global_reads (declared_global p) (ci_args ci)"
          "global_names_in (declared_global p) (ci_formals ci)"
          "λd. ls_enter (comp (declared_global p) p) (ls_channel (comp (declared_global p) p) d)
             ci (d, d)" d global_of σ]
      by (auto simp: dg_pipeline.analysis_spec_def dg_pipeline.entry_alt_def enter_single Let_def)
  next
    case (Deps p ci d σ) show ?case
      using enter_deps_keyed_enter_transfer[of cmb rl rg free
          "call_global_reads (declared_global p) (ci_args ci)"
          "global_names_in (declared_global p) (ci_formals ci)"
          "λd. ls_enter (comp (declared_global p) p) (ls_channel (comp (declared_global p) p) d)
             ci (d, d)" d global_of σ]
      by (auto simp: dg_pipeline.analysis_spec_def dg_pipeline.entry_alt_def enter_single Let_def)
  next
    case (EntrySound p ci d σ pub s)
    let ?𝒢 = "declared_global p" and ?xs = "declared_global_vars p"
    let ?c = "comp ?𝒢 p"
    let ?e = "genv global_of σ"
    let ?R = "call_global_reads ?𝒢 (ci_args ci)"
    let ?v = "view_of rg ?R ?e (free ?R)"
    let ?w = "cmb d ?v"
    let ?E = "dg_pipeline.comp_entry comp ?𝒢 p ci ?w"
    let ?W = "global_names_in ?𝒢 (ci_formals ci)"
    let ?ce = "call_enter ?𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci))"
    have alt: "dg_pipeline.entry_alt comp (λ𝒢. rl)
        (λp ci d e. cmb d (view_of rg (call_global_reads (declared_global p) (ci_args ci)) e
           (free (call_global_reads (declared_global p) (ci_args ci)))))
        ?𝒢 p ci d ?e = (rl ?w, rl ?E)"
      by (simp add: dg_pipeline.entry_alt_def Let_def)
    have R0: "enter_runs (enter⇧♯ (dg_pipeline.analysis_spec comp
          (λp. keyed_split_spec (declared_global p) cmb rl rg free) ?𝒢 p) ci)
        (mk_dg_man d global_of) σ [(rl ?w, rl ?E)] (pub_sides global_of rg ?W (?E ⊔ bot))"
      using enter_runs_keyed_enter_transfer[of cmb rl rg free ?R ?W
          "λd. ls_enter ?c (ls_channel ?c d) ci (d, d)" d global_of σ]
      by (simp add: dg_pipeline.analysis_spec_def enter_single)
    have pub: "pub = pub_sides global_of rg ?W (?E ⊔ bot)"
      using enter_runsD_sides[OF EntrySound(1)[unfolded alt], of "λ_. Answer bot"]
        enter_runsD_sides[OF R0, of "λ_. Answer bot"]
      by (simp add: bot_fun_def[symmetric])
    have E_Bot: "?E ⊔ Bot = ?E" by (cases ?E) simp_all
    have le: "rg x ?E ≤ ?e x" if "x ∈ set ?W" for x
    proof -
      have "DG bot (rg x ?E) ≤ pub (Inr (global_of x))"
        using pub_sides_ge[OF that, of rg "?E ⊔ bot" global_of] by (simp add: pub E_Bot)
      then have "rg x ?E ≤ genv global_of pub x" by (simp add: less_eq_dg_state_def)
      also have "… ≤ ?e x" using EntrySound(2) by (simp add: le_fun_def)
      finally show ?thesis .
    qed
    have view_ge: "full_view rg ?xs ?e ≤ ?v"
      unfolding full_view_def
    proof (rule view_of_le)
      fix x assume "x ∈ set ?xs"
      show "rg x (?e x) ≤ ?v"
      proof (cases "x ∈ set ?R")
        case True then show ?thesis by (rule view_of_ge_mem)
      next
        case False
        then show ?thesis using rg_free view_of_ge_acc by (blast intro: order_trans)
      qed
    qed simp
    have s0: "s ∈ ?gm p (cmb d (full_view rg ?xs ?e))" using EntrySound(3) by simp
    have sw: "s ∈ ?gm p ?w"
      using s0 gm_mono[OF cmb_mono[OF order_refl view_ge]] by blast
    have sE: "?ce s ∈ ?gm p ?E"
    proof -
      obtain q where "q ∈ set (ls_enter ?c (ls_channel ?c ?w) ci (?w, ?w))" "?ce s ∈ ?gm p (snd q)"
        using comp_sound[where p = p] sw ls_channel_sound[OF comp_sound[where p = p] sw]
        unfolding sound_local_spec_def by (metis fst_conv)
      then show ?thesis by (simp add: enter_single)
    qed
    have fr: "∀x. ?𝒢 x ⟶ x ∉ set ?W ⟶ ?ce s x = s x"
      by (auto intro: call_enter_frame)
    have "?ce s ∈ ?gm p (cmb (rl ?E) (full_view rg ?xs (λx. if x ∈ set ?W then rg x ?E else ?e x)))"
      by (rule mix[OF s0 sE fr])
    moreover have "cmb (rl ?E) (full_view rg ?xs (λx. if x ∈ set ?W then rg x ?E else ?e x))
        ≤ cmb (rl ?E) (full_view rg ?xs ?e)"
    proof (intro cmb_mono order_refl full_view_mono[OF rg_mono])
      fix x
      show "(if x ∈ set ?W then rg x ?E else ?e x) ≤ ?e x"
        using le[of x] by (cases "x ∈ set ?W") simp_all
    qed
    ultimately have "?ce s ∈ ?gm p (cmb (rl ?E) (full_view rg ?xs ?e))"
      using gm_mono by blast
    moreover have "s ∈ ?gm p (cmb (rl ?w) (full_view rg ?xs ?e))"
      using s0 by (simp add: rl_cmb cmb_rl)
    ultimately show ?case by (simp add: alt)
  next
    case (CmbBot p g) show ?case by (simp add: cmb_bot)
  next
    case (Init p)
    let ?xs = "declared_global_vars p"
    let ?ie = "dg_pipeline.init_env init_st buffer_key global_of (λ𝒢 d. Bot)
      (λ𝒢 p. map (λx. (x, rg x (Lifted init_st))) (declared_global_vars p)) (declared_global p) p"
    have ie: "rg x (Lifted init_st) ≤ ?ie x" if x: "x ∈ set ?xs" for x
    proof -
      have "rg x (Lifted init_st)
          ≤ (⨆(m, d)←filter (λ(m, d). m = x) (map (λy. (y, rg y (Lifted init_st))) ys). d)"
        if "x ∈ set ys" for ys
        using that by (induction ys) (auto intro: le_supI1 le_supI2)
      then show ?thesis using x by (simp add: dg_pipeline.init_env_def le_supI2)
    qed
    have "full_view rg ?xs (λx. rg x (Lifted init_st)) ≤ full_view rg ?xs ?ie"
      unfolding full_view_def
    proof (rule view_of_le)
      fix x assume x: "x ∈ set ?xs"
      show "rg x (rg x (Lifted init_st)) ≤ view_of rg ?xs ?ie bot"
        using rg_mono[OF ie[OF x], of x] view_of_ge_mem[OF x, of rg ?ie bot] by (rule order_trans)
    qed simp
    then show ?case
      using init_view[where p = p] gm_mono[OF cmb_mono[OF order_refl], where p = p] by blast
  next
    case (EmptyRd p s) show ?case by (rule empty_rd)
  next
    case EmptyV show ?case by (rule empty⇩V_sound)
  next
    case (SeedNe v ctx) show ?case by (rule seed_ne)
  next
    case (SeedNeGlobal v ctx n) show ?case by (rule seed_ne_global)
  next
    case (ClProved c d s) then show ?case by (rule classify_proved)
  next
    case (ClRefuted c d s) then show ?case by (rule classify_refuted)
  next
    case BotState show ?case by (rule bot_state_empty)
  next
    case (InitSound p) show ?case by (rule init_sound)
  qed
qed

subsection ‹An executable analysis as the pipeline's component›

text ‹
  What an executable non-relational analysis owes, stated over its own
  transfers: the abstract transfer it implements is sound, its executable
  mirror represents that transfer, and its routing, solver, classifier and
  entry state satisfy the pipeline's contracts on the represented abstract store.
  Its component is \<^const>‹exec_local_spec›, so the generic pipeline runs
  exactly its local specification, and every theorem above holds of it.

  ‹route_abs› is the same routing decision taken on the abstract carrier, kept
  for the analyses that state it; the pipeline's soundness does not use it.
›

locale dg_analysis_exec = certified_solver solve solve_dom solve_c
  for tf_st :: "(vname ⇒ bool) ⇒ edge_action
                  ⇒ 'a::numeric_domain default_st ⇒ 'a default_st"
    and enter_st :: "(vname ⇒ bool) ⇒ call_info ⇒ 'a default_st ⇒ 'a default_st"
    and init_st :: "'a default_st"
    and buffer_key :: 'k
    and global_of :: "unit ⇒ 'k"
    and seed :: "pp ⇒ 'c ⇒ 'k"
    and route :: "(vname ⇒ bool) ⇒ pp ⇒ 'c ⇒ 'a default_st lifted ⇒ call_action ⇒ 'c"
    and root_ctx :: 'c
    and solve :: "(pp × 'c, 'k, ('a default_st lifted, 'a default_st lifted) dg_state) eqsT
                  ⇒ pp × 'c
                  ⇒ (pp × 'c) set
                       × (pp × 'c + 'k ⇒ ('a default_st lifted, 'a default_st lifted) dg_state)"
    and solve_dom :: "(pp × 'c, 'k, ('a default_st lifted, 'a default_st lifted) dg_state) eqsT
                      ⇒ pp × 'c ⇒ bool"
    and bot_state :: "'a abs_state"
    and classify :: "exp ⇒ 'a abs_state ⇒ check_result"
    and sk :: "'a abs_state ⇒ 'a abs_state"
    and asn :: "vname ⇒ exp ⇒ 'a abs_state ⇒ 'a abs_state"
    and spc :: "special_call ⇒ vname ⇒ 'a abs_state ⇒ 'a abs_state"
    and br :: "exp ⇒ bool ⇒ 'a abs_state ⇒ 'a abs_state"
    and bd :: "pname ⇒ 'a abs_state ⇒ 'a abs_state"
    and rt :: "exp option ⇒ pname ⇒ 'a abs_state ⇒ 'a abs_state"
    and en :: "(vname ⇒ bool) ⇒ call_info ⇒ 'a abs_state ⇒ 'a abs_state"
    and ev :: "analysis_event ⇒ 'a abs_state ⇒ 'a abs_state"
    and route_abs :: "(vname ⇒ bool) ⇒ pp ⇒ 'c ⇒ 'a abs_state lifted ⇒ call_action ⇒ 'c"
    and solve_c :: "(pp × 'c, 'k,
                       ('a default_st lifted, 'a default_st lifted) dg_state) eqsT
                    ⇒ pp × 'c
                    ⇒ ((pp × 'c) set
                          × (pp × 'c + 'k
                               ⇒ ('a default_st lifted, 'a default_st lifted) dg_state)) option" +
  assumes tf_sound: "⋀𝒢. sound_nonrelational_transfer 𝒢 sk asn spc br bd rt (en 𝒢) ev"
    and tf_commute:
      "⋀𝒢 a s. live_default_st 𝒢 s
         ⟹ ρ⇘𝒢⇙ (tf_st 𝒢 a s)
               = local_spec_step sk asn spc br bd rt ev a (ρ⇘𝒢⇙ s)"
    and enter_commute:
      "⋀𝒢 ci s. ρ⇘𝒢⇙ (enter_st 𝒢 ci s)
                    = en 𝒢 ci (ρ⇘𝒢⇙ s)"
    and route_agree:
      "⋀𝒢 u ctx d ca. route 𝒢 u ctx d ca
         = route_abs 𝒢 u ctx (ρ⇘𝒢⇙ d) ca"
    and exec_seed_ne_buffer_key: "⋀v ctx. seed v ctx ≠ buffer_key"
    and exec_classify_proved:
      "⋀c d s. classify c d = Check_Proved ⟹ s ∈ γ d ⟹ truthy (⟦c⟧⇩e s)"
    and exec_classify_refuted:
      "⋀c d s. classify c d = Check_Refuted ⟹ s ∈ γ d
         ⟹ ¬ truthy (⟦c⟧⇩e s)"
    and bot_state_eq: "bot_state = bot"
    and exec_init_sound: "⋀𝒢. cinit_stores 𝒢 ⊆ default_st_gamma 𝒢 init_st"
    and exec_own_key: "⋀n. global_of n = buffer_key"

sublocale dg_analysis_exec ⊆ dg_analysis
    "λ𝒢 p. exec_local_spec 𝒢 (default_st_is_bot_for (declared_global_vars p))
             (tf_st 𝒢) (enter_st 𝒢)"
    "λp. default_st_is_bot_for (declared_global_vars p)"
    default_st_to_fun init_st buffer_key global_of seed route root_ctx
      solve solve_dom bot_state classify
    gamma_state is_empty_state solve_c "λ𝒢 c. dg_spec_of c" "λ𝒢 d e. d" "λ𝒢 d. d"
      "λ𝒢 d. Bot" "λ𝒢 p. []" "λp ci d e. d"
proof (rule dg_analysis_whole_stateI[OF certified_solver_axioms],
    goal_cases CompSound EnterSingle EmptyExact EmptyVExact SeedNe ClProved ClRefuted BotState
    Init SeedNeGlobal)
  case (CompSound p)
  interpret dom: dg_domain_exec "declared_global p"
      "default_st_is_bot_for (declared_global_vars p)" "tf_st (declared_global p)"
      "enter_st (declared_global p)" sk asn spc br bd rt "en (declared_global p)" ev
    by unfold_locales
       (rule tf_commute, assumption,
        rule enter_commute,
        rule default_st_is_bot_for_iff[OF declared_global_iff])
  show ?case
    by (rule dom.exec_local_spec_sound[OF tf_sound, unfolded gamma_lift_default_st_gamma_to_fun])
next
  case (EnterSingle p ci d)
  then show ?case by (simp add: dg_pipeline.comp_entry_def)
next
  case (EmptyExact p s)
  then show ?case by (rule default_st_is_bot_for_iff[OF declared_global_iff])
next
  case EmptyVExact show ?case
    by (rule sound_emptinessI) (erule is_empty_state_gamma_state_empty)
next
  case (SeedNe v ctx) then show ?case by (rule exec_seed_ne_buffer_key)
next
  case (ClProved c d s) then show ?case by (rule exec_classify_proved)
next
  case (ClRefuted c d s) then show ?case by (rule exec_classify_refuted)
next
  case BotState then show ?case
    by (simp add: bot_state_eq is_empty_state_iff_gamma_state_empty[symmetric])
next
  case (Init p) then show ?case
    using exec_init_sound[of "declared_global p"] by (simp add: default_st_gamma_def)
next
  case (SeedNeGlobal v ctx n) show ?case
    unfolding exec_own_key by (rule exec_seed_ne_buffer_key)
qed

text ‹
  The component's soundness at the carrier's own concretization, which is
  what a caller composing components on the carrier needs.
›

lemma (in dg_analysis_exec) exec_comp_sound:
  "sound_local_spec (declared_global p) (gamma_lift (default_st_gamma (declared_global p)))
     (exec_local_spec (declared_global p) (default_st_is_bot_for (declared_global_vars p))
        (tf_st (declared_global p)) (enter_st (declared_global p)))"
  unfolding gamma_lift_default_st_gamma_to_fun by (rule comp_sound)

text ‹
  The state a call enters its callee with, at the executable component: the entry
  transfer, lifted over reachability.
›

lemma (in dg_analysis_exec) comp_entry_exec:
  "dg_pipeline.comp_entry
     (λ𝒢 p. exec_local_spec 𝒢 (default_st_is_bot_for (declared_global_vars p))
        (tf_st 𝒢) (enter_st 𝒢))
     𝒢 p ci d
   = transfer_lift (default_st_is_bot_for (declared_global_vars p)) (enter_st 𝒢 ci) d"
  by (simp add: dg_pipeline.comp_entry_def)

text ‹
  The same against the solved global, the shape \<^const>‹dg_pipeline.ctx_succ›
  reads, so a caller can fold an executable entry back into it.
›

lemma (in dg_analysis_exec) entry_of_exec:
  "entry_of 𝒢 p ci d (sol_global 𝒢 p)
   = transfer_lift (default_st_is_bot_for (declared_global_vars p)) (enter_st 𝒢 ci) d"
  by (simp add: dg_pipeline.entry_of_def dg_pipeline.entry_alt_def comp_entry_exec)

end