Theory Entry_State_Routed_Context

theory Entry_State_Routed_Context
  imports "Voblint_Framework.Routed_Context" "Voblint_Compile.Compile_Wellformed"
begin

section ‹Routing when the entry operation is a pure list of alternatives›

text ‹
  A call can be answered with several possible entry states rather than one. This
  theory covers the case where computing that list is a ∗‹pure› step: it reads no
  solver unknown and publishes nothing to a global, so the entry run has an empty
  dependency set and a bottom publication.

  ‹alts ci d› is that list --- the alternatives the specification answers for call
  ‹ci› at caller state ‹d› --- and ‹enter_pure› is the assumption that the
  specification's own ‹enter⇧♯› is exactly that list handed to its continuation.
  What the locale restricts is therefore the entry operation, not the route; hence
  the name.

  ‹route› itself stays unconstrained: it may read the call site, the caller's context and
  the entered state, or ignore any of them.  Entry-state routing is its main application
  and the reason the parameter is there --- \<^const>‹formals_route_lifted_gen› projects the
  formals out of an abstract state, an executable instance projects them out of its own
  quotient state, and one policy spelled two ways is what a parameter is for --- but
  nothing here forces a route to look at the entered value at all.  Unlike
  ‹Call_String_Routed_Context›'s ‹call_string_routed_context›, no single seed-key datatype
  is shared across instances: each is keyed by its own carrier's value list, so ‹buffer_key› and
  ‹seed› stay genuine locale parameters too.

  Everything the routed locale asks about ‹adm› reduces to two facts about ‹alts›: its
  alternatives cover every concrete call at a covered call site (‹enter_cover›), and the
  solver visited the callee entry at every context a live alternative routes to
  (‹call_fwd›).  A one-alternative specification instantiates ‹alts ci d = [(d, en ci d)]›;
  one that splits a call into several alternatives, possibly overlapping, instantiates it
  with the longer list and nothing else changes.

  Two of the routed obligations are facts about \<^const>‹compile_prog› alone and are
  discharged here once: ‹finC› (‹compile_prog_finite›) and ‹calls_unique›
  (‹compile_prog_calls_source_unique›).  ‹seed_ne_buffer_key›, ‹call_fwd› and ‹comb_fwd›
  remain per-instance assumptions: the first is datatype distinctness of the instance's
  seed key, the other two say the solved variable set covers a routed callee entry or return
  continuation, a property of the program together with what the solver explored.
›

locale pure_entry_routed_context =
  dg_context_activation S "λd e. γ⇩D⇩G d (e ())" 𝒢 "compile_prog Pi ps" buffer_key
    "λ_. buffer_key" route
    "routed_call_program S (λ_. buffer_key) seed (static_resolve (compile_prog Pi ps)) is_bot"
    "routed_entry_seed_programs seed"
    bot0 d⇩0 g⇩0 sigma vars x0 sg γ⇩M
  for S :: "(pp × 'c, 'k, unit, 'D::bounded_semilattice_sup_bot,
              'G::bounded_semilattice_sup_bot) dg_spec"
    and γ⇩D⇩G :: "'D ⇒ 'G ⇒ store set"
    and 𝒢 :: "vname ⇒ bool"
    and Pi :: proc_table and ps :: "pname list"
    and buffer_key :: 'k
    and route :: "pp ⇒ 'c ⇒ 'D ⇒ call_action ⇒ 'c"
    and bot0 d⇩0 g⇩0 sigma vars x0 sg
    and seed :: "pp ⇒ 'c ⇒ 'k"
    and is_bot :: "'D ⇒ bool"
    and γ⇩M :: "'M ⇒ store set"
    and alts :: "call_info ⇒ 'D ⇒ 'D enter_result list" +
  assumes seed_ne_buffer_key[simp]: "⋀p ctx. seed p ctx ≠ buffer_key"
    and is_bot_bot: "is_bot bot"
    and is_bot_sound: "⋀d gv. is_bot d ⟹ γ⇩D⇩G d gv = {}"
    and enter_pure: "⋀ci. enter⇧♯ S ci = local_enter_transfer (alts ci)"
    and enter_cover:
    "⋀u ctx dst pars args p cont s.
       (u, ctx) ∈ vars
       ⟹ (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (compile_prog Pi ps)
       ⟹ s ∈ γ⇩D⇩G (dg_local (sigma (Inl (u, ctx)))) (dg_global (sigma (Inr buffer_key)))
       ⟹ entry_pairs_cover (λd. γ⇩D⇩G d (dg_global (sigma (Inr buffer_key)))) s
             (call_enter 𝒢 (CallEdge dst pars args) s)
             (alts (call_info_of (CallEdge dst pars args) p) (dg_local (sigma (Inl (u, ctx)))))"
    and call_fwd:
    "⋀u ctx dst pars args p cont cont' entry.
       (u, ctx) ∈ vars
       ⟹ (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (compile_prog Pi ps)
       ⟹ (cont', entry) ∈ set (alts (call_info_of (CallEdge dst pars args) p)
                                  (dg_local (sigma (Inl (u, ctx)))))
       ⟹ ¬ is_bot entry
       ⟹ (FunctionEntry p, route u ctx entry (CallEdge dst pars args)) ∈ vars"
    and comb_fwd:
    "⋀cl c1 dst pars args p cont.
       (cl, c1) ∈ vars
       ⟹ (cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (compile_prog Pi ps)
       ⟹ (cont, c1) ∈ vars"
begin

text ‹The context relation this instance keys its collecting semantics by.›
abbreviation entry_context_rel :: "'c context_policy" where
  "entry_context_rel ≡ routed_entry_context_rel alts (λd e. γ⇩D⇩G d (e ())) sigma (λ_. buffer_key) route"

sublocale routed: routed_context S "λd e. γ⇩D⇩G d (e ())" 𝒢 "compile_prog Pi ps" buffer_key
  "λ_. buffer_key"
  route bot0 d⇩0 g⇩0 sigma vars x0 sg seed
  "static_resolve (compile_prog Pi ps)" is_bot γ⇩M entry_context_rel
proof unfold_locales
  show "finite (calls (compile_prog Pi ps))" by (simp add: compile_prog_finite)
next
  show "calls_source_unique (compile_prog Pi ps)"
    unfolding calls_source_unique_def using compile_prog_calls_source_unique by blast
next
  show "⋀p ctx. seed p ctx ≠ buffer_key" by (rule seed_ne_buffer_key)
next
  show "is_bot bot" by (rule is_bot_bot)
next
  show "⋀d gv. is_bot d ⟹ γ⇩D⇩G d gv = {}" by (rule is_bot_sound)
next
  fix u ctx dst pars args p cont s
  assume "(u, ctx) ∈ vars"
    and "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (compile_prog Pi ps)"
    and "s ∈ gamma_at u ctx"
  then show "p ∈ set (static_resolve (compile_prog Pi ps) cont u
                        (CallEdge dst pars args) (dg_local (sigma (Inl (u, ctx)))))"
    by (simp add: compile_prog_finite)
next
  fix u ctx dst pars args p cont s ctx'
  assume covV: "(u, ctx) ∈ vars"
    and ce: "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (compile_prog Pi ps)"
    and "s ∈ gamma_at u ctx"
    and Rc: "ctx' ∈ entry_context_rel u ctx (call_info_of (CallEdge dst pars args) p) s
               (call_enter 𝒢 (CallEdge dst pars args) s)"
  let ?ci = "call_info_of (CallEdge dst pars args) p"
  let ?d = "dg_local (sigma (Inl (u, ctx)))"
  from Rc obtain cont' entry
    where mem: "(cont', entry) ∈ set (alts ?ci ?d)"
      and ccov: "s ∈ γ⇩D⇩G cont' (dg_global (sigma (Inr buffer_key)))"
      and ecov: "call_enter 𝒢 (CallEdge dst pars args) s
                   ∈ γ⇩D⇩G entry (dg_global (sigma (Inr buffer_key)))"
      and req0: "ctx' = route u ctx entry (CallEdge (ci_dst ?ci) (ci_formals ?ci) (ci_args ?ci))"
    using Rc by (auto elim: routed_entry_context_relE)
  have req: "route u ctx entry (CallEdge dst pars args) = ctx'" using req0 by simp
  have not_bot: "¬ is_bot entry"
    using ecov is_bot_sound by fastforce
  have Rr: "enter_runs (enter⇧♯ S ?ci) (mk_dg_man ?d (λ_. buffer_key)) sigma (alts ?ci ?d) bot"
    unfolding enter_pure by (rule enter_runs_local_enter_transfer_mk_dg_man)
  have D: "enter_deps (enter⇧♯ S ?ci) (mk_dg_man ?d (λ_. buffer_key)) sigma (alts ?ci ?d) {}"
    unfolding enter_pure by (rule enter_deps_local_enter_transfer_mk_dg_man)
  show "∃pairs pub deps cont' entry.
             enter_runs (enter⇧♯ S ?ci) (mk_dg_man ?d (λ_. buffer_key)) sigma pairs pub
           ∧ enter_deps (enter⇧♯ S ?ci) (mk_dg_man ?d (λ_. buffer_key)) sigma pairs deps
           ∧ (cont', entry) ∈ set pairs
           ∧ s ∈ γ⇩D⇩G cont' (genv (λ_. buffer_key) sigma ())
           ∧ call_enter 𝒢 (CallEdge dst pars args) s
               ∈ γ⇩D⇩G entry (genv (λ_. buffer_key) sigma ())
           ∧ route u ctx entry (CallEdge dst pars args) = ctx'
           ∧ (FunctionEntry p, ctx') ∈ vars"
    using Rr D mem ccov ecov req call_fwd[OF covV ce mem not_bot] by auto
next
  fix u ctx dst pars args p cont s
  assume covV: "(u, ctx) ∈ vars"
    and ce: "(u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (compile_prog Pi ps)"
    and sin: "s ∈ gamma_at u ctx"
  show "entry_context_rel u ctx (call_info_of (CallEdge dst pars args) p) s
                 (call_enter 𝒢 (CallEdge dst pars args) s) ≠ {}"
  proof (rule routed_entry_context_rel_total)
    show "entry_pairs_cover (λd. γ⇩D⇩G d (genv (λ_. buffer_key) sigma ())) s
            (call_enter 𝒢 (CallEdge dst pars args) s)
            (alts (call_info_of (CallEdge dst pars args) p) (dg_local (sigma (Inl (u, ctx)))))"
      using enter_cover[OF covV ce sin[simplified]] by simp
  qed
next
  fix cl c1 dst pars args p cont
  assume "(cl, c1) ∈ vars"
    and "(cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (compile_prog Pi ps)"
  then show "(cont, c1) ∈ vars" by (rule comb_fwd)
next
  show "⋀p ctx v. seed p ctx ≠ buffer_key" by simp
qed

end

end