Theory DG_Live_Unknowns

theory DG_Live_Unknowns
  imports DG_Analysis "Voblint_Compile.Live_Nodes"
begin

section ‹Which solved keys a terminating solve is closed on›

text ‹
  The key set a terminating solve returns is not one the soundness argument can use as it
  stands: it may hold keys the solver queried under an earlier value and no longer reads,
  and keys of procedures whose result it never solved.  ‹live_unknowns› keeps a solved key
  when its node belongs to a procedure (\<^theory>‹Voblint_Compile.Live_Nodes›) whose result
  is solved at the same context.  From what each generated equation reads under the final
  valuation, ‹live_unknowns_cover› shows that set closed under every intra edge, every call
  continuation and every call that enters a live state, with no premise beyond termination
  and a well-formed program.  The endpoints below restate the routed soundness over these
  keys and carry it to the published table.
›

subsection ‹What a routed equation reads›

lemma dep_aux_routed_node_rhs:
  assumes wf: "⋀w. ∀q ∈ set (routed_contribution_programs pred_sel site_sel route
                     it cmb extra g cx w). sp_wf q"
  shows "dep_aux τ (routed_node_rhs pred_sel site_sel buffer_key_at route it cmb extra g bot0 d⇩0 g⇩0
           (v, cx))
     = (⋃q∈set (routed_contribution_programs pred_sel site_sel route it cmb extra g cx v).
          dep_program τ q)"
  by (cases "v = cfg_entry g")
     (simp_all add: routed_node_rhs_def Let_def dep_program_side_rhs_fold_dg_char[OF wf])

lemma dep_L_routed_node_rhs_intra:
  assumes fin: "finite (intra g)" and e: "(u, a, v) ∈ intra g"
    and wf: "⋀w. ∀q ∈ set (routed_contribution_programs
                     intra_predecessor_addr_list call_site_list route
                     (λcx src a. dg_spec_edge_program S a src slot) cmb extra g cx w). sp_wf q"
  shows "(u, cx) ∈ dep⇩L (routed_node_rhs intra_predecessor_addr_list call_site_list buffer_key_at route
            (λcx src a. dg_spec_edge_program S a src slot) cmb extra g bot0 d⇩0 g⇩0) τ (v, cx)"
proof -
  have "dg_spec_edge_program S a (Inl (u, cx)) slot
          ∈ set (routed_contribution_programs intra_predecessor_addr_list call_site_list route
                   (λcx src a. dg_spec_edge_program S a src slot) cmb extra g cx v)"
    using e fin
    by (force simp: routed_contribution_programs_def intra_predecessor_addr_list_def
        intra_predecessors_def)
  then show ?thesis
    unfolding dep⇩L_def dep_def
    using dep_dg_spec_edge_program_source[of "Inl (u, cx)" τ S a slot]
    by (auto simp: dep_aux_routed_node_rhs[OF wf])
qed

lemma dep_program_routed_call_program:
  assumes wfS: "dg_spec_wf S"
  shows "dep_program τ (routed_call_program S global_of seed resolve is_bot route ctx ca cc v)
     = insert (Inl (cc, ctx))
         (⋃q∈set (resolve v cc ca (dg_local (τ (Inl (cc, ctx))))).
            dep_program τ (routed_callee_call_program S global_of seed route is_bot ctx ca cc
                        (dg_local (τ (Inl (cc, ctx)))) q))"
  by (simp add: routed_call_program_def sp_compile_bind sp_wf_observes
      dep_program_side_rhs_fold_dg_char[OF sp_wf_routed_callee_call_programs[OF wfS]])

lemma routed_call_program_mem:
  assumes fin: "finite (calls g)" and e: "(u, ca, FunctionEntry q, k) ∈ calls g"
  shows "routed_call_program S global_of seed resolve is_bot route cx ca u k
           ∈ set (routed_contribution_programs pred_sel call_site_list route it
                    (routed_call_program S global_of seed resolve is_bot) extra g cx k)"
proof -
  have "(u, ca) ∈ set (call_site_list g k)" using e fin by auto
  then show ?thesis by (rule routed_contribution_programs_combineI)
qed

lemma dep_L_routed_node_rhs_call_site:
  assumes fin: "finite (calls g)" and e: "(u, ca, FunctionEntry q, k) ∈ calls g"
    and wfS: "dg_spec_wf S"
    and wf: "⋀w. ∀q ∈ set (routed_contribution_programs pred_sel call_site_list route it
                     (routed_call_program S global_of seed resolve is_bot) extra g cx w). sp_wf q"
  shows "(u, cx) ∈ dep⇩L (routed_node_rhs pred_sel call_site_list buffer_key_at route it
            (routed_call_program S global_of seed resolve is_bot) extra g bot0 d⇩0 g⇩0) τ (k, cx)"
proof -
  have "Inl (u, cx)
          ∈ dep_program τ (routed_call_program S global_of seed resolve is_bot route cx ca u k)"
    by (simp add: dep_program_routed_call_program[OF wfS])
  then show ?thesis
    unfolding dep⇩L_def dep_def
    using routed_call_program_mem
            [OF fin e, of S global_of seed resolve is_bot route cx pred_sel it extra]
    by (auto simp: dep_aux_routed_node_rhs[OF wf])
qed

lemma dep_L_routed_node_rhs_callee_result:
  assumes fin: "finite (calls g)" and e: "(u, ca, FunctionEntry q, k) ∈ calls g"
    and deps: "enter_deps (enter⇧♯ S (call_info_of ca q))
                 (mk_dg_man (dg_local (τ (Inl (u, cx)))) global_of) τ pairs D"
    and mem: "(c, ent) ∈ set pairs"
    and res: "q ∈ set (resolve k u ca (dg_local (τ (Inl (u, cx)))))"
    and nb: "¬ is_bot ent"
    and wfS: "dg_spec_wf S"
    and wf: "⋀w. ∀q ∈ set (routed_contribution_programs pred_sel call_site_list route it
                     (routed_call_program S global_of seed resolve is_bot) extra g cx w). sp_wf q"
  shows "(FunctionResult q, route u cx ent ca)
           ∈ dep⇩L (routed_node_rhs pred_sel call_site_list buffer_key_at route it
                (routed_call_program S global_of seed resolve is_bot) extra g bot0 d⇩0 g⇩0) τ (k, cx)"
proof -
  let ?d = "dg_local (τ (Inl (u, cx)))"
  have callee: "dep_program τ (routed_callee_call_program S global_of seed route is_bot cx ca u ?d q)
      = D ∪ dep_program τ (side_rhs_fold_dg bot
          (map (routed_call_alternative_program S global_of seed route is_bot cx ca u q) pairs))"
    unfolding routed_callee_call_program_def sp_compile_bind
    by (rule enter_depsD[OF deps, simplified])
  have "Inl (FunctionResult q, route u cx ent ca)
          ∈ dep_program τ (routed_callee_call_program S global_of seed route is_bot cx ca u ?d q)"
  proof -
    have "Inl (FunctionResult q, route u cx ent ca)
            ∈ dep_program τ (routed_call_alternative_program S global_of seed route is_bot cx ca u q
                           (c, ent))"
      using nb by (simp add: routed_call_alternative_program_def Let_def)
    then show ?thesis
      unfolding callee
        dep_program_side_rhs_fold_dg_char[OF sp_wf_routed_call_alternative_programs[OF wfS]]
      using mem by auto
  qed
  then have "Inl (FunctionResult q, route u cx ent ca)
               ∈ dep_program τ (routed_call_program S global_of seed resolve is_bot route cx ca u k)"
    using res by (auto simp: dep_program_routed_call_program[OF wfS])
  then show ?thesis
    unfolding dep⇩L_def dep_def
    using routed_call_program_mem
            [OF fin e, of S global_of seed resolve is_bot route cx pred_sel it extra]
    by (auto simp: dep_aux_routed_node_rhs[OF wf])
qed

subsection ‹Keys of a solve whose activation returned›

text ‹
  The solved key set is closed under the equations' reads (‹sol_vars_dep_closed›).
  Walking those reads backwards, ‹live_unknowns_cover› shows ‹live_unknowns› closed
  under intra edges, call continuations and the entries of callees a call actually enters.
›

context dg_analysis
begin

lemma analysis_contribs_wf [simp]:
  "∀q ∈ set (routed_contribution_programs intra_predecessor_addr_list call_site_list
       (route (declared_global p))
       (λctx' src a. dg_spec_edge_program (analysis_spec (declared_global p) p) a src
          global_of)
       (routed_call_program (analysis_spec (declared_global p) p) global_of seed rsv
          (λd. d = Bot))
       (routed_entry_seed_programs seed) cfg cx w). sp_wf q"
  by (rule routed_contribution_programs_wf) auto

lemma sol_vars_dep_closed:
  assumes solves: "terminates (declared_global p) p"
    and x: "x ∈ sol_vars (declared_global p) p"
    and y: "y ∈ dep⇩L
       (routed_node_rhs intra_predecessor_addr_list call_site_list (λ_. buffer_key)
          (route (declared_global p))
          (λctx' src a. dg_spec_edge_program (analysis_spec (declared_global p) p) a src global_of)
          (routed_call_program (analysis_spec (declared_global p) 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 (declared_global p) (Lifted init_st)))
       (sol_env (declared_global p) p) x"
  shows "y ∈ sol_vars (declared_global p) p"
  using pp_routed[OF solves] x y by blast

lemma prog_cfg_finite: "finite (intra (prog_cfg p))" "finite (calls (prog_cfg p))"
  unfolding prog_cfg_def by (simp_all add: compile_prog_finite)

lemma sol_vars_back_intra:
  assumes solves: "terminates (declared_global p) p"
    and v: "(v, cx) ∈ sol_vars (declared_global p) p" and e: "(u, a, v) ∈ intra (prog_cfg p)"
  shows "(u, cx) ∈ sol_vars (declared_global p) p"
  by (rule sol_vars_dep_closed
        [OF solves v dep_L_routed_node_rhs_intra[OF prog_cfg_finite(1) e analysis_contribs_wf]])

lemma sol_vars_back_call_site:
  assumes solves: "terminates (declared_global p) p"
    and k: "(k, cx) ∈ sol_vars (declared_global p) p"
    and e: "(u, ca, FunctionEntry q, k) ∈ calls (prog_cfg p)"
  shows "(u, cx) ∈ sol_vars (declared_global p) p"
  by (rule sol_vars_dep_closed
        [OF solves k dep_L_routed_node_rhs_call_site
           [OF prog_cfg_finite(2) e dg_spec_wf_analysis_spec analysis_contribs_wf]])

lemma sol_vars_callee_result:
  assumes solves: "terminates (declared_global p) p"
    and k: "(k, cx) ∈ sol_vars (declared_global p) p"
    and e: "(u, ca, FunctionEntry q, k) ∈ calls (prog_cfg p)"
    and nb: "entry_of (declared_global p) p (call_info_of ca q)
               (dg_local (sol_env (declared_global p) p (Inl (u, cx))))
               (sol_global (declared_global p) p) ≠ Bot"
  shows "(FunctionResult q, ctx_succ (declared_global p) p u cx ca q)
           ∈ sol_vars (declared_global p) p"
proof -
  let ?d = "dg_local (sol_env (declared_global p) p (Inl (u, cx)))"
  let ?alt =
    "entry_alt (declared_global p) p (call_info_of ca q) ?d (sol_global (declared_global p) p)"
  have res: "q ∈ set (static_resolve (prog_cfg p) k u ca ?d)"
    using e prog_cfg_finite(2) by simp
  obtain D where deps: "enter_deps (enter⇧♯ (analysis_spec (declared_global p) p) (call_info_of ca q))
      (mk_dg_man ?d global_of) (sol_env (declared_global p) p) [?alt] D"
    using place_enter_deps unfolding sol_global_def by blast
  have mem: "(fst ?alt, snd ?alt) ∈ set [?alt]" by simp
  show ?thesis
    unfolding ctx_succ_def entry_of_def
    by (rule sol_vars_dep_closed[OF solves k],
        rule dep_L_routed_node_rhs_callee_result[where resolve = "static_resolve (prog_cfg p)"
            and τ = "sol_env (declared_global p) p" and cx = cx,
          OF prog_cfg_finite(2) e deps mem res])
       (use nb in ‹simp add: entry_of_def›, rule dg_spec_wf_analysis_spec, rule
         analysis_contribs_wf)
qed

lemma sol_vars_back_reach:
  assumes solves: "terminates (declared_global p) p"
    and w: "(w, cx) ∈ sol_vars (declared_global p) p"
    and r: "local_reaches (prog_cfg p) y w"
  shows "(y, cx) ∈ sol_vars (declared_global p) p"
  using r[unfolded local_reaches_def]
proof (induction rule: converse_rtrancl_induct)
  case base show ?case by (rule w)
next
  case (step y z)
  from step.hyps(1) show ?case
    unfolding local_succ_rel_def
    using sol_vars_back_intra[OF solves step.IH] sol_vars_back_call_site[OF solves step.IH]
    by blast
qed
definition live_unknowns :: "imp_prog ⇒ (pp × 'c) set" where
  "live_unknowns p =
     {(u, cx) ∈ sol_vars (declared_global p) p.
        ∃q. prog_node (prog_table p) (prog_procs p) q u
          ∧ (FunctionResult q, cx) ∈ sol_vars (declared_global p) p}"

lemma live_unknowns_sub: "live_unknowns p ⊆ sol_vars (declared_global p) p"
  unfolding live_unknowns_def by blast

lemma live_unknowns_of_result:
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
    and live: "prog_node (prog_table p) (prog_procs p) q y"
    and r: "(FunctionResult q, cx) ∈ sol_vars (declared_global p) p"
  shows "(y, cx) ∈ live_unknowns p"
proof -
  have "local_reaches (prog_cfg p) y (FunctionResult q)"
    unfolding prog_cfg_def by (rule prog_node_reaches[OF live])
  then have "(y, cx) ∈ sol_vars (declared_global p) p" by (rule sol_vars_back_reach[OF solves r])
  then show ?thesis unfolding live_unknowns_def using live r by blast
qed

theorem live_unknowns_cover:
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
  shows "ctx_vars_cover_live (prog_cfg p) (λ_ _. True) (live_succ (declared_global p) p)
           root_ctx (live_unknowns p)"
proof (rule ctx_vars_cover_liveI)
  have root: "(FunctionResult prog_main_name, root_ctx) ∈ sol_vars (declared_global p) p"
    using pp_routed[OF solves] by (simp add: root_query_def prog_cfg_def)
  show "(cfg_entry (prog_cfg p), root_ctx) ∈ live_unknowns p"
    using live_unknowns_of_result[OF wf solves prog_node_main_entry[OF wf] root]
    by (simp add: prog_cfg_def)
next
  fix u a v ctx
  assume u: "(u, ctx) ∈ live_unknowns p" and e: "(u, a, v) ∈ intra (prog_cfg p)"
  from u obtain q where lq: "prog_node (prog_table p) (prog_procs p) q u"
    and r: "(FunctionResult q, ctx) ∈ sol_vars (declared_global p) p"
    unfolding live_unknowns_def by blast
  have "prog_node (prog_table p) (prog_procs p) q v"
    using prog_node_intra[OF wf lq] e by (simp add: prog_cfg_def)
  then show "(v, ctx) ∈ live_unknowns p" by (rule live_unknowns_of_result[OF wf solves _ r])
next
  fix u ctx dst fs as q k
  assume u: "(u, ctx) ∈ live_unknowns p"
    and e: "(u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls (prog_cfg p)"
  from u obtain r where lr: "prog_node (prog_table p) (prog_procs p) r u"
    and res: "(FunctionResult r, ctx) ∈ sol_vars (declared_global p) p"
    unfolding live_unknowns_def by blast
  have "prog_node (prog_table p) (prog_procs p) r k"
    using prog_node_calls[OF wf lr] e by (simp add: prog_cfg_def)
  then show "(k, ctx) ∈ live_unknowns p" by (rule live_unknowns_of_result[OF wf solves _ res])
next
  fix u ctx dst fs as q k ctx'
  assume u: "(u, ctx) ∈ live_unknowns p"
    and e: "(u, CallEdge dst fs as, FunctionEntry q, k) ∈ calls (prog_cfg p)"
    and s: "live_succ (declared_global p) p u ctx (CallEdge dst fs as) q = Some ctx'"
  from u obtain r where lr: "prog_node (prog_table p) (prog_procs p) r u"
    and res: "(FunctionResult r, ctx) ∈ sol_vars (declared_global p) p"
    unfolding live_unknowns_def by blast
  have "prog_node (prog_table p) (prog_procs p) r k"
    using prog_node_calls[OF wf lr] e by (simp add: prog_cfg_def)
  then have k: "(k, ctx) ∈ sol_vars (declared_global p) p"
    using live_unknowns_of_result[OF wf solves _ res] live_unknowns_sub by blast
  from s have nb: "entry_of (declared_global p) p (call_info_of (CallEdge dst fs as) q)
               (dg_local (sol_env (declared_global p) p (Inl (u, ctx))))
               (sol_global (declared_global p) p) ≠ Bot"
    and c': "ctx' = ctx_succ (declared_global p) p u ctx (CallEdge dst fs as) q"
    by (auto simp: live_succ_def split: if_splits)
  have rq: "(FunctionResult q, ctx') ∈ sol_vars (declared_global p) p"
    unfolding c' by (rule sol_vars_callee_result[OF solves k e nb])
  have "prog_node (prog_table p) (prog_procs p) q (FunctionEntry q)"
    using prog_node_callee_entry[OF wf] e by (simp add: prog_cfg_def)
  then show "(FunctionEntry q, ctx') ∈ live_unknowns p"
    by (rule live_unknowns_of_result[OF wf solves _ rq])
qed

lemma root_live_key:
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
  shows "root_query p ∈ live_unknowns p"
proof -
  have r: "(FunctionResult prog_main_name, root_ctx) ∈ sol_vars (declared_global p) p"
    using pp_routed[OF solves] by (simp add: root_query_def prog_cfg_def)
  show ?thesis
    using live_unknowns_of_result[OF wf solves prog_node_result[OF prog_node_main_entry[OF wf]] r]
    by (simp add: root_query_def prog_cfg_def)
qed
subsection ‹The entry-state endpoint over the live keys›

text ‹
  The routed soundness statement restated over ‹live_unknowns›, whose coverage
  needs no premise beyond termination, and carried to the published table and
  the source-level endpoints under the functional context policy.
›

context
  fixes p :: imp_prog
begin

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

text ‹
  Establishes ‹routed_analysis› over the live keys, for any relation admitting call contexts.
  Beyond termination and well-formedness a policy owes only its own two facts: an
  admitted context is the one this pipeline routes the entered state to, and every
  concrete call at a live key is admitted somewhere. ‹live_unknowns_cover› supplies
  callee-entry membership.
›

lemma routed_analysis_from_live_unknowns:
  fixes adm :: "'c context_policy"
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
    and cover_R: "⋀u ctx dst pars args q cont s ctx'. (u, ctx) ∈ live_unknowns 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 (declared_global p) (CallEdge dst pars args) s)
        ⟹ route (declared_global p) u ctx
              (entered p (call_info_of (CallEdge dst pars args) q)
                 (dg_local (sol_env (declared_global p) p (Inl (u, ctx)))))
              (CallEdge dst pars args) = ctx'"
    and total_R: "⋀u ctx dst pars args q cont s. (u, ctx) ∈ live_unknowns p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ s ∈ pgam p (dg_local (sol_env (declared_global p) p (Inl (u, ctx)))) (gsol p)
        ⟹ adm u ctx (call_info_of (CallEdge dst pars args) q) s
                      (call_enter (declared_global p) (CallEdge dst pars args) s) ≠ {}"
  shows "routed_analysis (analysis_spec (declared_global p) p) (λd e. pgam p d e)
     (declared_global p) (prog_cfg p) buffer_key global_of
     (route (declared_global p)) Bot (Lifted init_st)
     (place_rg (declared_global p) (Lifted init_st))
     (sol_env (declared_global p) p) (live_unknowns p) (root_query p) seed (λd. d = Bot) adm
     (λd e. map_lift (rd (declared_global p)) (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_subset[OF post_bounded_of_part_post_solution[OF pp_routed[OF solves]]
          root_live_key[OF wf solves] live_unknowns_sub])
next
  case (SgCov v c) then show ?case by simp
next
  case (SgUncov v c) then show ?case by simp
next
  case (Fwd u a v c)
  show ?case
    by (rule ctx_vars_cover_live_edgeD[OF live_unknowns_cover[OF wf solves] Fwd(1) _ Fwd(3)]) simp
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 (declared_global p) p (Inl (u, ctx)))"
  let ?g = "genv global_of (sol_env (declared_global p) p)"
  let ?ent = "entered p ?ci ?caller"
  have sin: "s ∈ pgam p ?caller (gsol p)"
    using EnterCover(3) by (simp add: sol_global_def)
  have cov: "entry_pairs_cover (λd. pgam p d (gsol p)) s
      (call_enter (declared_global p) (CallEdge dst pars args) s)
      [entry_alt (declared_global p) p ?ci ?caller (gsol p)]"
  proof (rule entry_cover[OF solves _ EnterCover(2) sin])
    show "(cont, ctx) ∈ sol_vars (declared_global p) p"
      using ctx_vars_cover_live_combineD[OF live_unknowns_cover[OF wf solves] EnterCover(1,2)]
        live_unknowns_sub by blast
  qed
  obtain c e where ce: "entry_alt (declared_global p) p ?ci ?caller (gsol p) = (c, e)"
    by (cases "entry_alt (declared_global p) p ?ci ?caller (gsol p)")
  have nbE: "?ent ≠ Bot"
  proof
    assume "?ent = Bot"
    with cov ce show False by (simp add: entry_pairs_cover_def entry_of_def place_cmb_bot)
  qed
  have req: "route (declared_global p) u ctx ?ent (CallEdge dst pars args) = ctx'"
    by (rule cover_R[OF EnterCover(1,2,4)])
  have covE: "(FunctionEntry q, ctx') ∈ live_unknowns p"
    by (rule ctx_vars_cover_live_enterD[OF live_unknowns_cover[OF wf solves] EnterCover(1,2)])
       (use nbE req in ‹simp add: live_succ_def ctx_succ_def›)
  obtain pub where runs: "enter_runs (enter⇧♯ (analysis_spec (declared_global p) p) ?ci)
      (mk_dg_man ?caller global_of) (sol_env (declared_global p) p)
      [entry_alt (declared_global p) p ?ci ?caller ?g] pub"
    using place_enter_runs by blast
  obtain deps where deps: "enter_deps (enter⇧♯ (analysis_spec (declared_global p) p) ?ci)
      (mk_dg_man ?caller global_of) (sol_env (declared_global p) p)
      [entry_alt (declared_global p) p ?ci ?caller ?g] deps"
    using place_enter_deps by blast
  have ce': "entry_alt (declared_global p) p ?ci ?caller ?g = (c, e)"
    using ce by (simp add: sol_global_def)
  have sc: "s ∈ pgam p c ?g"
    and ec: "call_enter (declared_global p) (CallEdge dst pars args) s ∈ pgam p e ?g"
    using cov ce by (simp_all add: entry_pairs_cover_def sol_global_def)
  have re: "route (declared_global p) 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)
  show ?case
    by (rule ctx_vars_cover_live_combineD[OF live_unknowns_cover[OF wf solves] CombFwd(1,2)])
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 finite_subset[OF live_unknowns_sub vars_finite_of_terminates[OF solves]])
qed

text ‹
  The reader over the live keys agrees with the published one on them and describes
  nothing elsewhere, so a bound proved for it is a bound on the published table.
›

lemma gamma_live_reader_le:
  "pgam p (solved_local_reader (live_unknowns p) (sol_env (declared_global p) p) (Inl (v, ctx)))
       (gsol p)
     ⊆ pgam p (reader (declared_global p) p (Inl (v, ctx))) (gsol p)"
proof (cases "(v, ctx) ∈ live_unknowns p")
  case True
  then have "(v, ctx) ∈ sol_vars (declared_global p) p" by (rule subsetD[OF live_unknowns_sub])
  with True show ?thesis by (simp add: reader_def)
next
  case False then show ?thesis by (simp add: place_cmb_bot)
qed

theorem activation_collect_sound_live_unknowns:
  fixes adm :: "'c context_policy"
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
    and cover_R: "⋀u ctx dst pars args q cont s ctx'. (u, ctx) ∈ live_unknowns 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 (declared_global p) (CallEdge dst pars args) s)
        ⟹ route (declared_global p) u ctx
              (entered p (call_info_of (CallEdge dst pars args) q)
                 (dg_local (sol_env (declared_global p) p (Inl (u, ctx)))))
              (CallEdge dst pars args) = ctx'"
    and total_R: "⋀u ctx dst pars args q cont s. (u, ctx) ∈ live_unknowns p
        ⟹ (u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)
        ⟹ s ∈ pgam p (dg_local (sol_env (declared_global p) p (Inl (u, ctx)))) (gsol p)
        ⟹ adm u ctx (call_info_of (CallEdge dst pars args) q) s
                      (call_enter (declared_global p) (CallEdge dst pars args) s) ≠ {}"
  shows "𝒜⇘declared_global p,adm,root_ctx,prog_cfg p,cinit_stores (declared_global p)⇙ v ctx
           ⊆ pgam p (reader (declared_global p) p (Inl (v, ctx))) (gsol p)"
proof -
  interpret live: routed_analysis "analysis_spec (declared_global p) p" "λd e. pgam p d e"
      "declared_global p" "prog_cfg p" buffer_key global_of
      "route (declared_global p)" Bot
        "Lifted init_st" "place_rg (declared_global p) (Lifted init_st)"
      "sol_env (declared_global p) p" "live_unknowns p" "root_query p" seed "λd. d = Bot" adm
      "λd e. map_lift (rd (declared_global p)) (place_cmb p d e)"
      γ⇩V empty⇩V classify
    by (rule routed_analysis_from_live_unknowns[where adm = adm, OF wf solves cover_R total_R])
  have entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ live_unknowns p"
    by (rule ctx_vars_cover_live_entryD[OF live_unknowns_cover[OF wf solves]])
  have init_env_le:
    "init_env (declared_global p) p ≤ genv global_of (sol_env (declared_global p) p)"
    using init_env_le_sol[OF solves subsetD[OF live_unknowns_sub entry_cov]
      live.pp_entry_init_global_bound[OF entry_cov]]
    by (simp add: sol_global_def)
  have "𝒜⇘declared_global p,adm,root_ctx,prog_cfg p,cinit_stores (declared_global p)⇙ v ctx
        ⊆ pgam p (solved_local_reader (live_unknowns p) (sol_env (declared_global p) p) (Inl (v, ctx)))
             (gsol p)"
    using live.activation_collect_dg_sound
        [OF entry_cov _ init_env_le, of "cinit_stores (declared_global p)" v ctx] cinit_le_init
    by (simp add: sol_global_def)
  then show ?thesis using gamma_live_reader_le by blast
qed

text ‹
  A policy whose route ignores the entered state --- a call string, or the unit
  context --- admits exactly the context it computes, so both of its facts are
  immediate.
›

theorem fun_route_activation_collect_sound_of_terminates:
  fixes ctx_fun :: "cfg_node ⇒ 'c ⇒ store ⇒ 'c"
  assumes route_const: "⋀u ctx d ca s. route (declared_global p) u ctx d ca = ctx_fun u ctx s"
    and wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
  shows "𝒜⇘declared_global p,context_policy_of_fun ctx_fun,root_ctx,
           prog_cfg p,cinit_stores (declared_global p)⇙ v ctx
           ⊆ pgam p (reader (declared_global p) p (Inl (v, ctx))) (gsol p)"
proof (rule activation_collect_sound_live_unknowns[OF wf solves])
  fix u ctx dst pars args q cont and s :: store and ctx'
  assume "(u, ctx) ∈ live_unknowns p"
    and "(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 (declared_global p) (CallEdge dst pars args) s)"
  show "route (declared_global p) u ctx
          (entered p (call_info_of (CallEdge dst pars args) q)
             (dg_local (sol_env (declared_global p) p (Inl (u, ctx)))))
          (CallEdge dst pars args) = ctx'"
    using Rc
    by (simp add:
      route_const[of _ _ _ _ "call_enter (declared_global p) (CallEdge dst pars args) s"])
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 (declared_global p) (CallEdge dst pars args) s) ≠ {}"
    by simp
qed

text ‹
  The same fact read off the published surface, and what it yields at a program
  point, at a check and at a source run. A store reaching a point lies in one of
  the point's contexts, so the point is bounded by the union of the states published
  there. At the unit policy the union has the one member ‹()›.
›

theorem fun_route_state_at_sound:
  fixes ctx_fun :: "cfg_node ⇒ 'c ⇒ store ⇒ 'c"
  assumes route_const: "⋀u ctx d ca s. route (declared_global p) u ctx d ca = ctx_fun u ctx s"
    and wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
  shows "𝒜⇘declared_global p,context_policy_of_fun ctx_fun,root_ctx,
           prog_cfg p,cinit_stores (declared_global p)⇙ v ctx
           ⊆ γ⇩V (state_at (declared_global p) p ctx v)"
proof -
  have "𝒜⇘declared_global p,context_policy_of_fun ctx_fun,root_ctx,
          prog_cfg p,cinit_stores (declared_global p)⇙ v ctx
        ⊆ gamma_lift γ⇩V (lookup_table (result (declared_global p) p) v ctx)"
    using fun_route_activation_collect_sound_of_terminates[OF route_const wf solves]
    unfolding gamma_reader_eq_lookup .
  then show ?thesis
    by (auto simp: state_at_unfold bot_state_empty split: lifted.splits)
qed

theorem fun_route_result_node_sound:
  fixes ctx_fun :: "cfg_node ⇒ 'c ⇒ store ⇒ 'c"
  assumes route_const: "⋀u ctx d ca s. route (declared_global p) u ctx d ca = ctx_fun u ctx s"
    and wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
  shows "𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v
           ⊆ (⋃ctx. γ⇩V (state_at (declared_global p) p ctx v))"
  using fun_route_node_collect_eq_Union[where ctx_fun = ctx_fun and p = p and v = v]
    fun_route_state_at_sound[OF route_const wf solves]
  by (simp add: SUP_mono')

theorem fun_route_report_proved_sound:
  fixes ctx_fun :: "cfg_node ⇒ 'c ⇒ store ⇒ 'c"
  assumes route_const: "⋀u ctx d ca s. route (declared_global p) u ctx d ca = ctx_fun u ctx s"
    and wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
    and mem: "(v, c, Check_Proved) ∈ set (report (declared_global p) p ctx)"
  shows "∀s ∈ 𝒜⇘declared_global p,context_policy_of_fun ctx_fun,root_ctx,
                 prog_cfg p,cinit_stores (declared_global p)⇙ v ctx. truthy (⟦c⟧⇩e s)"
proof -
  have fin: "finite (intra (prog_cfg p))"
    unfolding prog_cfg_def by (simp add: compile_prog_finite)
  show ?thesis
    by (rule classify_checks_proved_sound
          [where g = "prog_cfg p" and env = "state_at (declared_global p) p ctx"
             and classify = classify and γ⇩S = γ⇩V
             and reach = "λv. 𝒜⇘declared_global p,context_policy_of_fun ctx_fun,root_ctx,
                               prog_cfg p,cinit_stores (declared_global p)⇙ v ctx",
           OF fin _ classify_proved fun_route_state_at_sound[OF route_const wf solves]])
       (use mem in ‹simp add: report_def state_at_def analysis_surface.report_def›)
qed

theorem fun_route_report_refuted_sound:
  fixes ctx_fun :: "cfg_node ⇒ 'c ⇒ store ⇒ 'c"
  assumes route_const: "⋀u ctx d ca s. route (declared_global p) u ctx d ca = ctx_fun u ctx s"
    and wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
    and mem: "(v, c, Check_Refuted) ∈ set (report (declared_global p) p ctx)"
  shows "∀s ∈ 𝒜⇘declared_global p,context_policy_of_fun ctx_fun,root_ctx,
                 prog_cfg p,cinit_stores (declared_global p)⇙ v ctx. ¬ truthy (⟦c⟧⇩e s)"
proof -
  have fin: "finite (intra (prog_cfg p))"
    unfolding prog_cfg_def by (simp add: compile_prog_finite)
  show ?thesis
    by (rule classify_checks_refuted_sound
          [where g = "prog_cfg p" and env = "state_at (declared_global p) p ctx"
             and classify = classify and γ⇩S = γ⇩V
             and reach = "λv. 𝒜⇘declared_global p,context_policy_of_fun ctx_fun,root_ctx,
                               prog_cfg p,cinit_stores (declared_global p)⇙ v ctx",
           OF fin _ classify_refuted fun_route_state_at_sound[OF route_const wf solves]])
       (use mem in ‹simp add: report_def state_at_def analysis_surface.report_def›)
qed

theorem fun_route_source_sound:
  fixes ctx_fun :: "cfg_node ⇒ 'c ⇒ store ⇒ 'c" and s0 s :: store
  assumes route_const: "⋀u ctx d ca s. route (declared_global p) u ctx d ca = ctx_fun u ctx s"
    and wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
    and s0: "s0 ∈ cinit_stores (declared_global p)"
    and run: "declared_global p, prog_table p ⊢ (main_body (prog_table p), s0, [])
                →⇩p⇧* (residual, s, frs)"
  shows "∃v stk ctx. prog_table p, prog_cfg p, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)
           ∧ s ∈ γ⇩V (state_at (declared_global p) p ctx v)"
proof -
  have cfg_eq: "prog_cfg p = compile_prog (prog_table p) (prog_procs p)"
    by (rule prog_cfg_def)
  have "∃v stk. prog_table p, prog_cfg p, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)
          ∧ s ∈ (⋃ctx. γ⇩V (state_at (declared_global p) p ctx v))"
    unfolding cfg_eq
    by (rule source_sound_from_node_collect_cap[OF wf s0 run])
       (use fun_route_result_node_sound[OF route_const wf solves] in ‹simp add: cfg_eq›)
  then show ?thesis by blast
qed

subsection ‹Entry-state routing›

text ‹
  Instantiates the live-key endpoints at ‹admitted_contexts›, the policy that routes
  a call by its entered state. Its two policy facts hold by construction, so the
  results need only termination and a well-formed program.
›

lemma entry_state_routed_analysis_from_live_unknowns:
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
  shows "routed_analysis (analysis_spec (declared_global p) p) (λd e. pgam p d e)
     (declared_global p) (prog_cfg p) buffer_key global_of
     (route (declared_global p)) Bot (Lifted init_st)
     (place_rg (declared_global p) (Lifted init_st))
     (sol_env (declared_global p) p) (live_unknowns p) (root_query p) seed (λd. d = Bot)
     (admitted_contexts (declared_global p) p)
     (λd e. map_lift (rd (declared_global p)) (place_cmb p d e))
     γ⇩V empty⇩V classify"
proof (rule routed_analysis_from_live_unknowns[OF wf solves])
  fix u ctx dst pars args q cont and s :: store and ctx'
  assume "(u, ctx) ∈ live_unknowns p"
    and "(u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)"
    and Rc: "ctx' ∈ admitted_contexts (declared_global p) p u ctx
               (call_info_of (CallEdge dst pars args) q) s
               (call_enter (declared_global p) (CallEdge dst pars args) s)"
  let ?ci = "call_info_of (CallEdge dst pars args) q"
  let ?caller = "dg_local (sol_env (declared_global p) p (Inl (u, ctx)))"
  let ?ent = "entered p ?ci ?caller"
  from Rc[unfolded admitted_contexts_alt] obtain cont' entry
    where mem: "(cont', entry) ∈ set [entry_alt (declared_global p) p ?ci ?caller (gsol p)]"
      and req0: "ctx' = route (declared_global p) u ctx entry
                   (CallEdge (ci_dst ?ci) (ci_formals ?ci) (ci_args ?ci))"
    by (rule routed_entry_context_relE)
  have "entry = ?ent" using mem by (simp add: entry_of_def) (metis snd_conv)
  then show "route (declared_global p) u ctx ?ent (CallEdge dst pars args) = ctx'"
    using req0 by simp
next
  fix u ctx dst pars args q cont and s :: store
  assume uL: "(u, ctx) ∈ live_unknowns p"
    and ce: "(u, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls (prog_cfg p)"
    and sin: "s ∈ pgam p (dg_local (sol_env (declared_global p) p (Inl (u, ctx)))) (gsol p)"
  have cont: "(cont, ctx) ∈ sol_vars (declared_global p) p"
    using ctx_vars_cover_live_combineD[OF live_unknowns_cover[OF wf solves] uL ce]
      live_unknowns_sub by blast
  show "admitted_contexts (declared_global p) p u ctx
                 (call_info_of (CallEdge dst pars args) q) s
                 (call_enter (declared_global p) (CallEdge dst pars args) s) ≠ {}"
    unfolding admitted_contexts_alt
    by (rule routed_entry_context_rel_total)
       (use entry_cover[OF solves cont ce sin]
         in ‹simp add: sol_global_def del: declared_global_iff›)
qed

theorem entry_state_activation_collect_sound_of_terminates:
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
  shows "𝒜⇘declared_global p,admitted_contexts (declared_global p) p,
           root_ctx,prog_cfg p,cinit_stores (declared_global p)⇙ v ctx
           ⊆ pgam p (reader (declared_global p) p (Inl (v, ctx))) (gsol p)"
proof -
  interpret live: routed_analysis "analysis_spec (declared_global p) p" "λd e. pgam p d e"
      "declared_global p" "prog_cfg p" buffer_key global_of
      "route (declared_global p)" Bot
        "Lifted init_st" "place_rg (declared_global p) (Lifted init_st)"
      "sol_env (declared_global p) p" "live_unknowns p" "root_query p" seed "λd. d = Bot"
      "admitted_contexts (declared_global p) p"
      "λd e. map_lift (rd (declared_global p)) (place_cmb p d e)"
      γ⇩V empty⇩V classify
    by (rule entry_state_routed_analysis_from_live_unknowns[OF wf solves])
  have entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ live_unknowns p"
    by (rule ctx_vars_cover_live_entryD[OF live_unknowns_cover[OF wf solves]])
  have init_env_le:
    "init_env (declared_global p) p ≤ genv global_of (sol_env (declared_global p) p)"
    using init_env_le_sol[OF solves subsetD[OF live_unknowns_sub entry_cov]
      live.pp_entry_init_global_bound[OF entry_cov]]
    by (simp add: sol_global_def)
  have "𝒜⇘declared_global p,admitted_contexts (declared_global p) p,
          root_ctx,prog_cfg p,cinit_stores (declared_global p)⇙ v ctx
        ⊆ pgam p (solved_local_reader (live_unknowns p) (sol_env (declared_global p) p) (Inl (v, ctx)))
             (gsol p)"
    using live.activation_collect_dg_sound
        [OF entry_cov _ init_env_le, of "cinit_stores (declared_global p)" v ctx] cinit_le_init
    by (simp add: sol_global_def)
  then show ?thesis using gamma_live_reader_le by blast
qed

corollary entry_state_lookup_sound_of_terminates:
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
  shows "𝒜⇘declared_global p,admitted_contexts (declared_global p) p,
           root_ctx,prog_cfg p,cinit_stores (declared_global p)⇙ v ctx
           ⊆ gamma_lift γ⇩V (lookup_table (result (declared_global p) p) v ctx)"
  using entry_state_activation_collect_sound_of_terminates[OF wf solves]
  unfolding gamma_reader_eq_lookup .

lemma entry_state_has_context_of_terminates:
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
    and t: "t ∈ 𝒯⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙"
  shows "∃c. activation_context_rel (declared_global p) (admitted_contexts (declared_global p) p)
               root_ctx (prog_cfg p) t c"
proof -
  interpret live: routed_analysis "analysis_spec (declared_global p) p" "λd e. pgam p d e"
      "declared_global p" "prog_cfg p" buffer_key global_of
      "route (declared_global p)" Bot
        "Lifted init_st" "place_rg (declared_global p) (Lifted init_st)"
      "sol_env (declared_global p) p" "live_unknowns p" "root_query p" seed "λd. d = Bot"
      "admitted_contexts (declared_global p) p"
      "λd e. map_lift (rd (declared_global p)) (place_cmb p d e)"
      γ⇩V empty⇩V classify
    by (rule entry_state_routed_analysis_from_live_unknowns[OF wf solves])
  have entry_cov: "(cfg_entry (prog_cfg p), root_ctx) ∈ live_unknowns p"
    by (rule ctx_vars_cover_live_entryD[OF live_unknowns_cover[OF wf solves]])
  have init_env_le:
    "init_env (declared_global p) p ≤ genv global_of (sol_env (declared_global p) p)"
    using init_env_le_sol[OF solves subsetD[OF live_unknowns_sub entry_cov]
      live.pp_entry_init_global_bound[OF entry_cov]]
    by (simp add: sol_global_def)
  show ?thesis
    using live.routed_valid_activation_trace_has_context[OF entry_cov _ init_env_le t] cinit_le_init
    by simp
qed

theorem entry_state_node_collect_eq_Union_of_terminates:
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
  shows "𝒞⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙ v
           = (⋃ctx. 𝒜⇘declared_global p,admitted_contexts (declared_global p) p,
                       root_ctx,prog_cfg p,cinit_stores (declared_global p)⇙ v ctx)"
  by (rule node_collect_eq_Union_activation_of_has_context)
     (rule entry_state_has_context_of_terminates[OF wf solves])

text ‹
  The entry-state policy in one statement: the solve is fixed first, the policy is
  read off it, and that policy is total on valid traces and covered by the solved
  states. This order of quantifiers is why reading contexts off the result is not
  circular.
›
corollary entry_state_policy_of_terminates:
  assumes wf: "wf_program_compile_input p" and solves: "terminates (declared_global p) p"
  shows "∀t ∈ 𝒯⇘declared_global p,prog_cfg p,cinit_stores (declared_global p)⇙.
           ∃c. activation_context_rel (declared_global p) (admitted_contexts (declared_global p) p)
                 root_ctx (prog_cfg p) t c"
    and "𝒜⇘declared_global p,admitted_contexts (declared_global p) p,
           root_ctx,prog_cfg p,cinit_stores (declared_global p)⇙ v ctx
           ⊆ pgam p (reader (declared_global p) p (Inl (v, ctx))) (gsol p)"
  using entry_state_has_context_of_terminates[OF wf solves]
    entry_state_activation_collect_sound_of_terminates[OF wf solves]
  by blast+

end

end

end