Theory Routed_Exec_Refinement

theory Routed_Exec_Refinement
  imports
    DG_Local_State_Exec_Refinement
begin

section ‹Routed execution, once for every domain and context policy›

text ‹
  \<^locale>‹dg_domain_exec› already reduces a domain's obligation to the routed
  spine to three primitive commute facts. What it deliberately does not carry is the
  ∗‹routing› layer: the equation system a routed analysis actually solves, and the
  executable-to-abstract transport of its post-solution. Each domain, at each context
  policy, re-derived that layer, and because \<^const>‹routed_call_program› mentions no domain
  constant, those derivations differ only in the domain carrier, the routing function
  and a name prefix.

  This locale is that layer, stated once. It adds the seed-key pair the routed
  generator needs --- kept as parameters rather than a fixed datatype, so a domain
  keeps its own key type and this locale stays independent of how that type is
  eventually shared --- together with the executable and abstract routing functions
  and their agreement, and derives the commute and transport facts every routed
  instance needs. A context-insensitive instance passes \<^const>‹route_unit› on both
  sides, where agreement is free; a call-string instance passes its own routing
  function on each side and discharges the agreement from that function's own laws.

  Deliberately absent: the equation-system, solved-table and result ⬚‹definition›s
  themselves. They must stay concrete per-domain constants because they carry ‹[code]›
  equations, and \<^locale>‹dg_domain_exec›'s own ‹empty_pred_exact› is not
  dischargeable without fixing a concrete global set, so no locale carrying it can be
  interpreted globally. The domain keeps its definitions; what it stops re-proving is
  everything below.

  Also deliberately absent: the solver. The generated equation system is
  solver-independent, and ‹TD_side_upd_rule› already supplies
  ‹partial_post_solution› for every update rule on the menu, so a solver choice
  is an argument at the use site, never a parameter of the domain capability.
›


subsection ‹The buffered generator at any component›

text ‹
  The buffered generator a domain actually solves, reconciled with the unbuffered one
  the framework is stated over, for every component run as a specification. Both
  reshaping hooks are the identity: the buffered generator only asks a hook to hoist
  what it publishes at the buffered key ‹buffer_key›, and a component publishes nothing
  there, since its edge transfers, its entry and its return all read and write the
  local unknown only. Its queries do not change that: its channel is a pure function
  of the local value, so an asking transfer is still a local one.
›

theorem pp_dg_spec_of:
  assumes S: "S = dg_spec_of c"
    and ne: "⋀p ctx. seed p ctx ≠ buffer_key"
    and pp: "part_post_solution
     (routed_node_rhs_buffered intra_predecessor_addr_list call_site_list (λ_. buffer_key) route_st
        (λctx' src a. dg_spec_edge_program S a src (λ_. buffer_key))
        (routed_call_program S (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot))
        (routed_entry_seed_programs seed)
        g bot0 d⇩0 g⇩0)
     x0 sigma_st vars"
  shows "part_post_solution
     (routed_node_rhs intra_predecessor_addr_list call_site_list (λ_. buffer_key) route_st
        (λctx' src a. dg_spec_edge_program S a src (λ_. buffer_key))
        (routed_call_program S (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot))
        (routed_entry_seed_programs seed)
        g bot0 d⇩0 g⇩0)
     x0 sigma_st vars"
proof -
  have wf: "dg_spec_wf S" by (simp add: S)
  have intra_free: "sides_of_program (dg_spec_edge_program S a src (λ_. buffer_key)) τ z = bot"
    for a src τ z
    by (simp add: S dg_spec_edge_program_def)
  have cmb_free: "sides_of_program
      (routed_call_program S (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot) route' ctx' ca cc ex)
      τ (Inr buffer_key) = bot" for route' ctx' ca cc ex τ
    by (rule routed_call_program_side_free_at_buffer_key[OF wf])
       (auto simp: S local_transfer_def local_combine_transfer_def ne
         dest!: enter_runs_local_pub_bot)
  show ?thesis
  proof (rule part_post_solution_routed_node_rhs_buffered
      [where cmb_c =
        "routed_call_program S (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot)"
         and it_c = "λctx' src a. dg_spec_edge_program S a src (λ_. buffer_key)"])
    show "⋀c' w. ∀p ∈ set (routed_contribution_programs intra_predecessor_addr_list
             call_site_list route_st (λctx' src a. dg_spec_edge_program S a src (λ_. buffer_key))
             (routed_call_program S (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot))
             (routed_entry_seed_programs seed) g c' w). sp_wf p"
      by (rule routed_contribution_programs_wf)
         (auto intro: sp_wf_dg_spec_edge_program[OF wf] sp_wf_routed_call_program[OF wf])
    then show "⋀c' w. ∀p ∈ set (routed_contribution_programs intra_predecessor_addr_list
             call_site_list route_st (λctx' src a. dg_spec_edge_program S a src (λ_. buffer_key))
             (routed_call_program S (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot))
             (routed_entry_seed_programs seed) g c' w). sp_wf p" .
    show "⋀c' src a τ. dg_local (sides_of_program (dg_spec_edge_program S a src (λ_. buffer_key)) τ
             (Inr ((λ_. buffer_key) c'))) = bot"
      by (simp add: intra_free bot_dg_state_def)
    show "⋀c' src a τ. dg_global (traverse_program (dg_spec_edge_program S a src (λ_. buffer_key)) τ)
           = dg_global (sides_of_program (dg_spec_edge_program S a src (λ_. buffer_key)) τ
               (Inr ((λ_. buffer_key) c')))"
      by (simp add: S dg_spec_edge_program_def bot_dg_state_def)
    show "⋀c' src a τ. sides_of_program (dg_spec_edge_program S a src (λ_. buffer_key)) τ
             (Inr ((λ_. buffer_key) c')) = bot"
      by (rule intra_free)
    show "⋀c' ca cc ex τ. dg_local (sides_of_program
             (routed_call_program S (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot) route_st c' ca cc ex)
             τ (Inr ((λ_. buffer_key) c'))) = bot"
      by (simp add: cmb_free bot_dg_state_def)
    show "⋀c' ca cc ex τ. dg_global (traverse_program
             (routed_call_program S (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot) route_st c' ca cc ex) τ)
           = dg_global (sides_of_program
               (routed_call_program S (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot) route_st c' ca cc ex)
               τ (Inr ((λ_. buffer_key) c')))"
      by (simp add: routed_call_program_global_free[OF wf] cmb_free bot_dg_state_def)
    show "⋀c' ca cc ex τ. sides_of_program
             (routed_call_program S (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot) route_st c' ca cc ex)
             τ (Inr ((λ_. buffer_key) c')) = bot"
      by (rule cmb_free)
    show "⋀c' w τ z x. x ∈ set (routed_entry_seed_programs seed route_st c' w)
           ⟹ sides_of_program x τ z = bot"
      by (rule routed_entry_seed_programs_free)
    show "⋀c' w τ x. x ∈ set (routed_entry_seed_programs seed route_st c' w)
           ⟹ dg_global (traverse_program x τ) = bot"
      by (rule routed_entry_seed_programs_local_only)
  qed (simp_all add: pp)
qed

text ‹
  ‹routed_domain_exec› adds call routing to ‹dg_domain_exec›: seed keys
  never collide with the analysis global, and routing and callee resolution on
  the executable state agree with their abstract versions after readback.
›

locale routed_domain_exec =
  dg_domain_exec 𝒢 empty_pred tf_st enter_st sk asn sp br bd rt en ev
  for 𝒢 :: "vname ⇒ bool"
    and empty_pred :: "'a::numeric_domain default_st ⇒ bool"
    and tf_st :: "edge_action ⇒ 'a default_st ⇒ 'a default_st"
    and enter_st :: "call_info ⇒ 'a default_st ⇒ 'a default_st"
    and sk :: "'a abs_state ⇒ 'a abs_state"
    and asn :: "vname ⇒ exp ⇒ 'a abs_state ⇒ 'a abs_state"
    and sp :: "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 :: "call_info ⇒ 'a abs_state ⇒ 'a abs_state"
    and ev :: "analysis_event ⇒ 'a abs_state ⇒ 'a abs_state" +
  fixes buffer_key :: 'k
    and seed :: "pp ⇒ 'c ⇒ 'k"
    and route_st :: "pp ⇒ 'c ⇒ 'a default_st lifted ⇒ call_action ⇒ 'c"
    and route_abs :: "pp ⇒ 'c ⇒ 'a abs_state lifted ⇒ call_action ⇒ 'c"
    and resolve_st :: "cfg ⇒ pp ⇒ pp ⇒ call_action ⇒ 'a default_st lifted ⇒ pname list"
    and resolve_abs :: "cfg ⇒ pp ⇒ pp ⇒ call_action ⇒ 'a abs_state lifted ⇒ pname list"
  assumes seed_ne_buffer_key [simp]: "⋀p ctx. seed p ctx ≠ buffer_key"
      and route_agree: "⋀u c' d ca. route_st u c' d ca
                          = route_abs u c' (readback 𝒢 d) ca"
      and resolve_agree: "⋀g w cc ca d. resolve_st g w cc ca d
                          = resolve_abs g w cc ca (readback 𝒢 d)"
begin

text ‹The routed combine tree commutes with the executable-to-abstract reader. ‹spec_st›
  and ‹spec_abs› come from \<^locale>‹dg_domain_exec›; nothing here mentions a domain
  constant beyond them, so one proof serves every instance. The caller continuation needs
  no hypothesis: \<^const>‹dg_spec_combine_transfer› already runs it inside the combine
  sub-tree.›

lemma dg_prog_st_commute_routed_call_program:
  "dg_reader_commute_gen.dg_prog_st_commute
     (map_lift (default_st_to_fun 𝒢)) (map_lift (default_st_to_fun 𝒢)) env
     (routed_call_program spec_st (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot) route_st ctx ca cc ex)
     (routed_call_program spec_abs (λ_. buffer_key) seed (resolve_abs g) (λd. d = Bot)
        route_abs ctx ca cc ex)"
  by (rule dg_reader_commute_gen.dg_prog_st_commute_routed_call_program
        [where Floc = "map_lift (default_st_to_fun 𝒢)"
           and Fglob = "map_lift (default_st_to_fun 𝒢)"])
     (rule dg_reader_commute_gen_lifted_for seed_ne_buffer_key
           dg_spec_wf_exec_dg_spec
           dg_spec_wf_lifted_state_dg_spec
           Henter_lifted_for Hcomb_lifted_for
           route_agree map_lift_eq_Bot_iff resolve_agree)+

text ‹The routed extra-goal list commutes elementwise, for the same reason.›

text ‹
  The buffered generator a domain actually solves, reconciled with the unbuffered one
  the framework is stated over --- at the executable spec, before publication.

  Both reshaping hooks are the identity here. The buffered generator only ever asks a
  hook to hoist what it publishes at the buffered key ‹buffer_key›; this spec is local-only,
  so its intra tree and its routed combine publish nothing there, and each tree is
  already its own contribution analogue. That is a property of the trees --- read off
  ‹routed_call_program_side_free_at_buffer_key› and the local-only compile-down facts --- not of any
  analysis family: a spec whose transfers do publish at ‹buffer_key› would have to supply
  reshaped hooks instead, with the same generic bridge unchanged. The routed seed
  survives untouched, because a seed key is never ‹buffer_key› and the bridge requires
  off-key sides to be preserved, not removed.

  An instance that interprets the spine at ‹spec_st› hands this post-solution to
  \<^locale>‹dg_context_activation› directly.
›

abbreviation intra_st :: "'c ⇒ pp × 'c + 'k ⇒ edge_action
   ⇒ (pp × 'c, 'k, ('a default_st lifted, 'a default_st lifted) dg_state,
        ('a default_st lifted, 'a default_st lifted) dg_state) strategy_program"
where
  "intra_st ctx' src a ≡ dg_spec_edge_program spec_st a src (λ_. buffer_key)"

abbreviation cmb_st :: "cfg ⇒ (pp ⇒ 'c ⇒ 'a default_st lifted ⇒ call_action ⇒ 'c)
   ⇒ 'c ⇒ call_action ⇒ pp ⇒ pp
   ⇒ (pp × 'c, 'k, ('a default_st lifted, 'a default_st lifted) dg_state,
        ('a default_st lifted, 'a default_st lifted) dg_state) strategy_program"
where
  "cmb_st g ≡ routed_call_program spec_st (λ_. buffer_key) seed (resolve_st g) (λd. d = Bot)"

theorem pp_st:
  assumes pp: "part_post_solution
     (routed_node_rhs_buffered intra_predecessor_addr_list call_site_list (λ_. buffer_key) route_st
        intra_st (cmb_st g)
        (routed_entry_seed_programs seed)
        g bot0 d⇩0 g⇩0)
     x0 sigma_st vars"
  shows "part_post_solution
     (routed_node_rhs intra_predecessor_addr_list call_site_list (λ_. buffer_key) route_st
        intra_st (cmb_st g)
        (routed_entry_seed_programs seed)
        g bot0 d⇩0 g⇩0)
     x0 sigma_st vars"
  by (rule pp_dg_spec_of[where S = spec_st])
     (rule exec_dg_spec_def, rule seed_ne_buffer_key, rule pp)

end

end