Theory DG_Keyed_Split_Spec

theory DG_Keyed_Split_Spec
  imports DG_Local_State_Spec "Voblint_Solver.Strategy_Tree_Side_Buffering"
    "Voblint_Solver.Strategy_Program_Fold"
begin

section ‹One solver unknown per global name›

text ‹
  The ownership-split lifter of ‹DG_Ownership_Split_Spec› keeps every program
  global in one shared value. Reading a global therefore depends on all of them,
  and writing one wakes every reader of any other. Goblint keys its globals by
  name instead, and this theory does the same for a whole-state component.

  A global name ‹x› lives at its own unknown. Its value there is a global half
  that describes ‹x› alone, cut out of a whole state by ‹rg x›. A transfer
  reads only the names its edge mentions and publishes only the names its edge
  can write. Every other global it hands the wrapped transfer as ‹free›, a global
  half that claims nothing about the unread names, so the wrapped transfer stays
  sound on it. Its result says nothing useful about the unread names either, and
  it is not published: the next point reads them from their own unknowns again.

  That last step is sound because the edge leaves the unpublished globals of a
  concrete store unchanged. Which names an edge may change is a fact of the
  concrete semantics (‹edge_writes›), established in ‹CFG_Transfer›. Which names it reads only
  affects precision: a name left out is read as ‹free›.
›

subsection ‹Reading and publishing named globals›

text ‹
  Reading a list of names folds their global halves into an accumulator, each
  value cut to the name it was read at. Publishing a list of names sends each
  its own cut of one whole state. The value-level counterparts are
  ‹view_of› and ‹pub_sides›.
›

fun read_view ::
  "('x,'k,vname,'d::semilattice_sup,'d) man ⇒ (vname ⇒ 'd ⇒ 'd) ⇒ vname list ⇒ 'd
   ⇒ ('x,'k,('d,'d) dg_state,'d) strategy_program"
where
  "read_view m rg [] acc = sp_return acc"
| "read_view m rg (x # xs) acc = man_global m x ⤜ (λg. read_view m rg xs (rg x g ⊔ acc))"

fun publish_at ::
  "('x,'k,vname,'d,'d) man ⇒ (vname ⇒ 'd ⇒ 'd) ⇒ vname list ⇒ 'd
   ⇒ ('x,'k,('d,'d) dg_state,unit) strategy_program"
where
  "publish_at m rg [] r = sp_return ()"
| "publish_at m rg (x # xs) r = man_sideg m x (rg x r) ⤜ (λ_. publish_at m rg xs r)"

definition view_of :: "(vname ⇒ 'd ⇒ 'd) ⇒ vname list ⇒ (vname ⇒ 'd) ⇒ 'd
    ⇒ 'd::semilattice_sup" where
  "view_of rg xs e acc = fold (λx acc. rg x (e x) ⊔ acc) xs acc"

text ‹The global half a whole environment describes, over a list of names.›

definition full_view :: "(vname ⇒ 'd ⇒ 'd) ⇒ vname list ⇒ (vname ⇒ 'd)
    ⇒ 'd::bounded_semilattice_sup_bot" where
  "full_view rg xs e = view_of rg xs e bot"

definition pub_sides :: "(vname ⇒ 'k) ⇒ (vname ⇒ 'd ⇒ 'd) ⇒ vname list ⇒ 'd
    ⇒ 'x + 'k ⇒ ('d::bounded_semilattice_sup_bot, 'd) dg_state" where
  "pub_sides key rg xs r = foldr (λx acc. acc ⊔ bot(Inr (key x) := DG bot (rg x r))) xs bot"

lemma view_of_ge_acc: "acc ≤ view_of rg xs e acc"
  unfolding view_of_def
  by (induction xs arbitrary: acc) (auto intro: order_trans[OF sup_ge2])

lemma view_of_ge_mem: "x ∈ set xs ⟹ rg x (e x) ≤ view_of rg xs e acc"
  unfolding view_of_def
proof (induction xs arbitrary: acc)
  case Nil then show ?case by simp
next
  case (Cons y ys)
  show ?case
  proof (cases "x = y")
    case True
    then show ?thesis
      using view_of_ge_acc[of "rg y (e y) ⊔ acc" rg ys e]
      by (simp add: view_of_def)
  next
    case False
    with Cons show ?thesis by simp
  qed
qed

lemma view_of_le:
  assumes "acc ≤ v" and "⋀x. x ∈ set xs ⟹ rg x (e x) ≤ v"
  shows "view_of rg xs e acc ≤ v"
  using assms unfolding view_of_def by (induction xs arbitrary: acc) auto

lemma full_view_mono:
  assumes rg_mono: "⋀x v v'. v ≤ v' ⟹ rg x v ≤ rg x v'"
    and le: "⋀x. e x ≤ e' x"
  shows "full_view rg xs e ≤ full_view rg xs e'"
  unfolding full_view_def
proof (rule view_of_le)
  fix x assume "x ∈ set xs"
  then show "rg x (e x) ≤ view_of rg xs e' bot"
    using rg_mono[OF le[of x], of x] view_of_ge_mem[of x xs rg e' bot] by (blast intro: order_trans)
qed simp

lemma pub_sides_ge:
  "x ∈ set xs ⟹ DG bot (rg x r) ≤ pub_sides key rg xs r (Inr (key x))"
  unfolding pub_sides_def
  by (induction xs) (auto simp: sup_fun_def intro: le_supI1 le_supI2)

subsubsection ‹What a solver observes of them›

text ‹Reading names is observed as a dependency on each of their unknowns and
  nothing else; publishing names is observed as one side effect per name.›

lemma traverse_read_view [simp]:
  "traverse_rhs (read_view (mk_dg_man d key) rg xs acc K) τ
     = traverse_rhs (K (view_of rg xs (genv key τ) acc)) τ"
  by (induction xs arbitrary: acc) (simp_all add: view_of_def sp_bind_def sp_return_def)

lemma sides_read_view [simp]:
  "sides_of_rhs (read_view (mk_dg_man d key) rg xs acc K) τ
     = sides_of_rhs (K (view_of rg xs (genv key τ) acc)) τ"
  by (induction xs arbitrary: acc) (simp_all add: view_of_def sp_bind_def sp_return_def)

lemma dep_aux_read_view [simp]:
  "dep_aux τ (read_view (mk_dg_man d key) rg xs acc K)
     = (Inr ∘ key) ` set xs ∪ dep_aux τ (K (view_of rg xs (genv key τ) acc))"
  by (induction xs arbitrary: acc) (auto simp: view_of_def sp_bind_def sp_return_def)

lemma traverse_publish_at [simp]:
  "traverse_rhs (publish_at (mk_dg_man d key) rg xs r K) τ = traverse_rhs (K ()) τ"
  by (induction xs) (simp_all add: sp_bind_def sp_return_def)

lemma sides_publish_at [simp]:
  "sides_of_rhs (publish_at (mk_dg_man d key) rg xs r K) τ
     = sides_of_rhs (K ()) τ ⊔ pub_sides key rg xs r"
  by (induction xs) (simp_all add: pub_sides_def sp_bind_def sp_return_def ac_simps)

lemma dep_aux_publish_at [simp]:
  "dep_aux τ (publish_at (mk_dg_man d key) rg xs r K) = dep_aux τ (K ())"
  by (induction xs) (simp_all add: sp_bind_def sp_return_def)

lemma side_path_read_view [simp]:
  "side_path τ (read_view (mk_dg_man d key) rg xs acc K)
     = side_path τ (K (view_of rg xs (genv key τ) acc))"
  by (induction xs arbitrary: acc)
     (simp_all add: view_of_def dg_read_global_def sp_read_global_def sp_bind_def sp_return_def)

lemma side_path_publish_at [simp]:
  "side_path τ (publish_at (mk_dg_man d key) rg xs r K)
     = map key xs @ side_path τ (K ())"
  by (induction xs) (simp_all add: dg_sideg_def sp_publish_def sp_bind_def sp_return_def)

lemma sp_wf_read_view [intro]:
  "(⋀x. sp_wf (man_global m x)) ⟹ sp_wf (read_view m rg xs acc)"
  by (induction xs arbitrary: acc) (auto intro!: sp_wf_bind)

lemma sp_wf_publish_at [intro]:
  "(⋀x v. sp_wf (man_sideg m x v)) ⟹ sp_wf (publish_at m rg xs r)"
  by (induction xs) (auto intro!: sp_wf_bind)

subsection ‹The keyed transfers›

text ‹
  Each transfer reads its names, recombines them with the point's local half,
  runs the wrapped whole-state operation, publishes the names it may change and
  answers with the local half of the result. ‹cmb› and ‹rl› are the binary
  recombination and local projection the ownership split already uses.
›

definition keyed_transfer ::
  "('d ⇒ 'd ⇒ 'd) ⇒ ('d ⇒ 'd) ⇒ (vname ⇒ 'd ⇒ 'd) ⇒ (vname list ⇒ 'd)
   ⇒ vname list ⇒ vname list ⇒ ('d ⇒ 'd)
   ⇒ ('x,'k,vname,'d::bounded_semilattice_sup_bot,'d) man_transfer"
where
  "keyed_transfer cmb rl rg free R W f m =
     read_view m rg R (free R) ⤜ (λg.
     publish_at m rg W (f (cmb (man_local m) g)) ⤜ (λ_.
     sp_return (rl (f (cmb (man_local m) g)))))"

lemma dep_keyed_transfer:
  "dep_program τ (transfer_program (keyed_transfer cmb rl rg free R W f) src key)
     = insert src ((Inr ∘ key) ` set R)"
  by (simp add: dep_transfer_program keyed_transfer_def
      sp_compile_with_def sp_bind_def sp_return_def)

lemma side_path_keyed_transfer:
  "side_path τ (sp_compile
      (transfer_program (keyed_transfer cmb rl rg free R W f) src key)) = map key W"
  by (cases src)
     (simp_all add: transfer_program_def transfer_program_at_def keyed_transfer_def
        sp_compile_def sp_compile_with_def sp_map_def sp_bind_def sp_return_def
        dg_read_at_def sp_read_local_def sp_read_global_def)

definition keyed_combine_transfer ::
  "('d ⇒ 'd ⇒ 'd) ⇒ ('d ⇒ 'd) ⇒ (vname ⇒ 'd ⇒ 'd) ⇒ (vname list ⇒ 'd)
   ⇒ vname list ⇒ ('d ⇒ 'd ⇒ 'd)
   ⇒ ('x,'k,vname,'d::bounded_semilattice_sup_bot,'d) man_combine_transfer"
where
  "keyed_combine_transfer cmb rl rg free W h m de =
     publish_at m rg W (h (cmb (man_local m) (free [])) (cmb de (free []))) ⤜ (λ_.
     sp_return (rl (h (cmb (man_local m) (free [])) (cmb de (free [])))))"

definition keyed_enter_transfer ::
  "('d ⇒ 'd ⇒ 'd) ⇒ ('d ⇒ 'd) ⇒ (vname ⇒ 'd ⇒ 'd) ⇒ (vname list ⇒ 'd)
   ⇒ vname list ⇒ vname list ⇒ ('d ⇒ 'd enter_result list)
   ⇒ ('x,'k,vname,'d::bounded_semilattice_sup_bot,'d) man_enter_transfer"
where
  "keyed_enter_transfer cmb rl rg free R W en m =
     read_view m rg R (free R) ⤜ (λg.
     publish_at m rg W (⨆(c, e)←en (cmb (man_local m) g). e) ⤜ (λ_.
     sp_return (map (λ(c, e). (rl c, rl e)) (en (cmb (man_local m) g)))))"

text ‹A call answers the alternatives its entry computes from the recombined state
  and publishes each name in ‹W› cut from the join of the entered states.›

lemma enter_runs_keyed_enter_transfer:
  "enter_runs (keyed_enter_transfer cmb rl rg free R W en) (mk_dg_man d key) σ
     (map (λ(c, e). (rl c, rl e)) (en (cmb d (view_of rg R (genv key σ) (free R)))))
     (pub_sides key rg W
        (⨆(c, e)←en (cmb d (view_of rg R (genv key σ) (free R))). e))"
  unfolding enter_runs_def keyed_enter_transfer_def
  by (simp add: sp_bind_def sp_return_def ac_simps)

lemma enter_deps_keyed_enter_transfer:
  "enter_deps (keyed_enter_transfer cmb rl rg free R W en) (mk_dg_man d key) σ
     (map (λ(c, e). (rl c, rl e)) (en (cmb d (view_of rg R (genv key σ) (free R)))))
     ((Inr ∘ key) ` set R)"
  unfolding enter_deps_def keyed_enter_transfer_def
  by (simp add: sp_bind_def sp_return_def)

text ‹Only the manager's local value and its two global capabilities are read, so
  the query channel installed around a transfer does not change it.›

lemma read_view_outer_man [simp]:
  "read_view (outer_man Q m) rg xs acc = read_view m rg xs acc"
  by (induction xs arbitrary: acc) simp_all

lemma publish_at_outer_man [simp]:
  "publish_at (outer_man Q m) rg xs r = publish_at m rg xs r"
  by (induction xs) simp_all

lemma keyed_transfer_outer_man [simp]:
  "keyed_transfer cmb rl rg free R W f (outer_man Q m) = keyed_transfer cmb rl rg free R W f m"
  by (simp add: keyed_transfer_def)

subsection ‹The lifter›

text ‹
  Every edge runs the component's closed step through ‹keyed_transfer›, reading
  the globals its expressions mention and publishing the globals it may assign.
  A return reads nothing and may assign its destination. The return pipeline is
  wrapped once, as in the ownership split.

  A call reads the globals its actuals mention and passes every other global as
  ‹free›. The context a call enters is computed from that state, and the analyzer
  recomputes it outside the solver from the same view of the solved environment.
›

definition keyed_split_spec ::
  "(vname ⇒ bool) ⇒ ('d ⇒ 'd ⇒ 'd) ⇒ ('d ⇒ 'd) ⇒ (vname ⇒ 'd ⇒ 'd)
   ⇒ (vname list ⇒ 'd) ⇒ 'd local_spec
   ⇒ ('x,'k,vname,'d::bounded_semilattice_sup_bot,'d) dg_spec"
where
  "keyed_split_spec 𝒢 cmb rl rg free c =
     (let step = (λa. keyed_transfer cmb rl rg free (edge_global_reads 𝒢 a)
                        (edge_global_writes 𝒢 a) ⟦a⟧⇧♯⇘c⇙)
      in local_dg_spec_template⦇
         dgs_skip := step EA_Nop,
         dgs_assign := (λx e. step (EA_Assign x e)),
         dgs_special := (λsc x. step (EA_Special sc x)),
         dgs_branch := (λb pol. step (if pol then EA_Assume b else EA_AssumeNot b)),
         dgs_body := (λp. step (EA_Body p)),
         dgs_return := (λe p. step (EA_Ret e p)),
         dgs_enter := (λci. keyed_enter_transfer cmb rl rg free
            (call_global_reads 𝒢 (ci_args ci)) (global_names_in 𝒢 (ci_formals ci))
            (λd. ls_enter c (ls_channel c d) ci (d, d))),
         dgs_event := (λev. step (event_action ev)),
         dgs_combine_assign := (λci. keyed_combine_transfer cmb rl rg free
            (global_names_in 𝒢 (case_option [] (λx. [x]) (ci_dst ci)))
            (λdc de. ls_combine c (ls_channel c dc) (ls_channel c de) ci dc de)) ⦈)"


lemma dg_spec_step_keyed_split_spec [simp]:
  "dg_spec_step (keyed_split_spec 𝒢 cmb rl rg free c) a
     = keyed_transfer cmb rl rg free (edge_global_reads 𝒢 a) (edge_global_writes 𝒢 a)
         ⟦a⟧⇧♯⇘c⇙"
  unfolding keyed_split_spec_def Let_def by (cases a) simp_all

lemma dgs_enter_keyed_split_spec [simp]:
  "enter⇧♯ (keyed_split_spec 𝒢 cmb rl rg free c) ci
     = keyed_enter_transfer cmb rl rg free (call_global_reads 𝒢 (ci_args ci))
         (global_names_in 𝒢 (ci_formals ci)) (λd. ls_enter c (ls_channel c d) ci (d, d))"
  unfolding keyed_split_spec_def Let_def by simp

lemma dgs_query_keyed_split_spec [simp]:
  "dgs_query (keyed_split_spec 𝒢 cmb rl rg free c) m q = sp_return ⊤"
  unfolding keyed_split_spec_def Let_def by simp

lemma dg_spec_combine_transfer_keyed_split_spec [simp]:
  "dg_spec_combine_transfer (keyed_split_spec 𝒢 cmb rl rg free c) ci
     = keyed_combine_transfer cmb rl rg free (global_names_in 𝒢 (case_option [] (λx. [x]) (ci_dst ci)))
         (λdc de. ls_combine c (ls_channel c dc) (ls_channel c de) ci dc de)"
  unfolding dg_spec_combine_transfer_def keyed_split_spec_def Let_def
  by (simp add: local_combine_transfer_def fun_eq_iff)

lemma dg_spec_wf_keyed_split_spec [intro, simp]:
  "dg_spec_wf (keyed_split_spec 𝒢 cmb rl rg free c)"
  unfolding dg_spec_wf_def
  by (auto simp: keyed_transfer_def keyed_enter_transfer_def keyed_combine_transfer_def
      intro!: sp_wf_bind)


subsection ‹Soundness of the keyed lifter›

text ‹
  A point's state is its local half recombined with the global half its
  environment describes over the program's global names ‹xs›. The carrier owes
  monotone operations, and that a name outside a read set is cut to something
  below ‹free› of that set. What it owes about concretization is one
  frame law, ‹mix›: a store described by a result, whose globals outside
  ‹W› agree with a store described against an environment, is described by the
  result's local half recombined with the result's own cut at the names in
  ‹W› and the environment at every other name.
›

theorem keyed_split_contract:
  fixes cmb :: "'d::bounded_semilattice_sup_bot ⇒ 'd ⇒ 'd"
  assumes sound: "sound_local_spec 𝒢 gm c"
    and cmb_mono: "⋀d d' g g'. d ≤ d' ⟹ g ≤ g' ⟹ cmb d g ≤ cmb d' g'"
    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: "⋀l0 e r s s' W. s ∈ gm (cmb l0 (full_view rg xs e)) ⟹ s' ∈ gm r
        ⟹ (∀x. 𝒢 x ⟶ x ∉ set W ⟶ s' x = s x)
        ⟹ s' ∈ gm (cmb (rl r) (full_view rg xs (λx. if x ∈ set W then rg x r else e x)))"
  shows "analysis_contract (keyed_split_spec 𝒢 cmb rl rg free c)
           (λd e. gm (cmb d (full_view rg xs e))) 𝒢"
proof -
  have gm_mono_all: "∀x y. x ≤ y ⟶ gm x ⊆ gm y"
    using sound unfolding sound_local_spec_def by (rule conjunct1)
  then have gm_mono: "⋀x y. x ≤ y ⟹ gm x ⊆ gm y" by blast
  have env_mono: "⋀d d' e e'. d ≤ d' ⟹ (⋀x. e x ≤ e' x)
      ⟹ gm (cmb d (full_view rg xs e)) ⊆ gm (cmb d' (full_view rg xs e'))"
    by (rule gm_mono, rule cmb_mono, assumption, rule full_view_mono[OF rg_mono]) simp
  have view_ge: "full_view rg xs e ≤ view_of rg R e (free R)" for e R
    unfolding full_view_def
  proof (rule view_of_le)
    fix x assume "x ∈ set xs"
    show "rg x (e x) ≤ view_of rg R e (free R)"
    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 out: "(λx. if x ∈ set W then rg x r else e x) x ≤ (e ⊔ genv key P) x"
    if pub: "⋀x. x ∈ set W ⟹ rg x r ≤ dg_global (P (Inr (key x)))"
    for e W r x key and P :: "'z + 'w ⇒ ('d, 'd) dg_state"
    using pub[of x] by (auto intro: le_supI2)
  have pub: "rg x r ≤ dg_global ((bot ⊔ pub_sides key rg W r) (Inr (key x)))"
    if "x ∈ set W" for x W r key
    using pub_sides_ge[OF that, of rg r key] by (simp add: less_eq_dg_state_def)
  show ?thesis
  proof (unfold_locales, goal_cases wf mono step comb)
    case wf show ?case by (rule dg_spec_wf_keyed_split_spec)
  next
    case (mono d d' e e')
    then show ?case by (intro env_mono) (simp_all add: le_fun_def)
  next
    case (step a τ src key)
    let ?d = "dg_local (τ src)" and ?e = "genv key τ"
    let ?R = "edge_global_reads 𝒢 a" and ?W = "edge_global_writes 𝒢 a"
    let ?g = "view_of rg ?R ?e (free ?R)"
    let ?r = "⟦a⟧⇧♯⇘c⇙ (cmb ?d ?g)"
    have loc: "edge_out (keyed_split_spec 𝒢 cmb rl rg free c) a src key τ = rl ?r"
      by (simp add: dg_spec_edge_program_def traverse_transfer_program keyed_transfer_def
          sp_compile_with_def sp_bind_def sp_return_def)
    have sides: "sides_of_program
        (dg_spec_edge_program (keyed_split_spec 𝒢 cmb rl rg free c) a src key) τ
        = bot ⊔ pub_sides key rg ?W ?r"
      by (simp add: dg_spec_edge_program_def sides_transfer_program keyed_transfer_def
          sp_compile_with_def sp_bind_def sp_return_def bot_fun_def[symmetric])
    show ?case
    proof
      fix s' assume "s' ∈ edge_collect a (gm (cmb ?d (full_view rg xs ?e)))"
      then obtain s where s: "s ∈ gm (cmb ?d (full_view rg xs ?e))" and st: "s' ∈ edge_step a s"
        by (auto simp: edge_collect_def)
      have "s ∈ gm (cmb ?d ?g)"
        using s gm_mono[OF cmb_mono[OF order_refl view_ge]] by blast
      then have "s' ∈ edge_collect a (gm (cmb ?d ?g))" using st by (auto simp: edge_collect_def)
      then have r: "s' ∈ gm ?r" using closed_step_sound[OF sound] by blast
      have fr: "∀x. 𝒢 x ⟶ x ∉ set ?W ⟶ s' x = s x"
        using edge_step_frame[OF st] by auto
      have "s' ∈ gm (cmb (rl ?r) (full_view rg xs (λx. if x ∈ set ?W then rg x ?r else ?e x)))"
        by (rule mix[OF s r fr])
      also have "… ⊆ gm (cmb (rl ?r) (full_view rg xs (?e ⊔ genv key (bot ⊔ pub_sides key rg ?W ?r))))"
        by (rule env_mono[OF order_refl], rule out, erule pub)
      finally show "s' ∈ gm (cmb (edge_out (keyed_split_spec 𝒢 cmb rl rg free c) a src key τ)
          (full_view rg xs
            (genv key τ ⊔ edge_pub (keyed_split_spec 𝒢 cmb rl rg free c) a src key τ)))"
        unfolding loc sides .
    qed
  next
    case (comb s dc key τ t de ci)
    let ?e = "genv key τ" and ?W = "global_names_in 𝒢 (case_option [] (λx. [x]) (ci_dst ci))"
    let ?h = "λdc de. ls_combine c (ls_channel c dc) (ls_channel c de) ci dc de"
    let ?r = "?h (cmb dc (free [])) (cmb de (free []))"
    have free_ge: "full_view rg xs ?e ≤ free []"
      unfolding full_view_def by (rule view_of_le) (simp_all add: rg_free)
    have sc: "s ∈ gm (cmb dc (free []))"
      using comb(1) gm_mono[OF cmb_mono[OF order_refl free_ge]] by blast
    have tc: "t ∈ gm (cmb de (free []))"
      using comb(2) gm_mono[OF cmb_mono[OF order_refl free_ge]] by blast
    have r: "combine_collect 𝒢 (ci_dst ci) s t ∈ gm ?r"
      by (rule closed_combine_sound[OF sound sc tc])
    have fr: "∀x. 𝒢 x ⟶ x ∉ set ?W ⟶ combine_collect 𝒢 (ci_dst ci) s t x = t x"
      by (auto intro: combine_collect_frame)
    have "combine_collect 𝒢 (ci_dst ci) s t
        ∈ gm (cmb (rl ?r) (full_view rg xs (λx. if x ∈ set ?W then rg x ?r else ?e x)))"
      by (rule mix[OF comb(2) r fr])
    also have "… ⊆ gm (cmb (rl ?r) (full_view rg xs (?e ⊔ genv key (bot ⊔ pub_sides key rg ?W ?r))))"
      by (rule env_mono[OF order_refl], rule out, erule pub)
    finally show ?case
      by (simp add: keyed_combine_transfer_def sp_compile_with_def sp_bind_def sp_return_def
          bot_fun_def[symmetric])
  qed
qed

end