Theory DG_Ownership_Split_Spec

theory DG_Ownership_Split_Spec
  imports DG_Local_State_Spec State_Restriction "Voblint_Solver.Strategy_Program_Fold"
begin

section ‹Lifting a whole-state analysis onto the global channel›

text ‹
  Every other specification in this session is local-only: it answers from the
  local value and never touches ‹man_global› or ‹man_sideg›. This
  theory takes such a specification and returns one that does the opposite, and is
  the reason those capabilities exist.

  The lifted specification uses one carrier for ‹D› and ‹G›, splitting each
  state by variable ownership: \<^const>‹combine_env›'s predicate is the source
  language's own declaration of which names are global, so the global names live on
  the shared channel and the rest on the program point's own unknown. The split is
  not a representation choice: a return recombines two concrete stores by that same
  ownership rule, keeping the caller's locals and taking the globals from the
  callee.

  Each lifted transfer therefore reads the shared fact, rejoins it with the local
  half to recover the whole state, runs the argument's transfer on a manager
  holding that whole state, and splits the result back -- publishing the global
  half with ‹man_sideg› and answering with the local half. Its compiled tree
  reads the source, queries the global key, publishes a ‹Side›, and answers,
  which is what makes it the only specification here whose equations carry a
  genuine ‹QueryG› and ‹Side›.

  Because it consumes and produces a specification, it is a lifter in Goblint's
  sense -- a ‹Spec2Spec› functor, like the privatizations that give a Base
  analysis its shared-state discipline -- not a second way of writing an analysis.
  The argument keeps its own transfers; only what a transfer's local value means,
  and what happens to its result, change.

  The construction is generic in the carrier -- the same three operations exist on
  function-valued states and on the solver's association lists -- but not in the
  ownership rule, which is always \<^const>‹combine_env› and the two
  restrictions to the global and the local half at that carrier.
›


subsection ‹The ownership-splitting wrapper›

text ‹
  The pattern is stated once, over any carrier that can merge a local and a global
  half and project each back out. Which carrier is a separate question from what
  the wrapper does: the same three operations exist on function-valued states and
  on the solver's association lists, so the executable mirror is this definition at
  other arguments rather than a second development.

  It wraps a transfer rather than a pure function. What the wrapped transfer sees
  is a manager whose local value is the merged whole state; its own capabilities
  are the outer ones, which a whole-state transfer never calls. That is what makes
  the wrapper a specification-to-specification lifter -- Goblint's
  ‹Spec2Spec› -- instead of a second way of writing a transfer.
›

definition ownership_split_transfer_gen ::
  "('d ⇒ 'd ⇒ 'd) ⇒ ('d ⇒ 'd) ⇒ ('d ⇒ 'd)
   ⇒ ('x,'k,unit,'d::bounded_semilattice_sup_bot,'d) man_transfer
   ⇒ ('x,'k,unit,'d,'d) man_transfer"
where
  "ownership_split_transfer_gen cmb rg rl T m =
     do {
       g ← man_global m ();
       res ← T (m⦇man_local := cmb (man_local m) g⦈);
       _ ← man_sideg m () (rg res);
       sp_return (rl res)
     }"

text ‹
  A return combine is the same pattern with two values to merge: the caller
  continuation becomes the wrapped transfer's local value, and the callee exit is
  merged against the same shared fact before it is handed over. Merging both sides
  means the wrapped transfer sees two whole states and needs to know nothing about
  the split -- in particular the callee's globals come from the shared channel,
  not from its own locally-restricted copy.
›

definition ownership_split_combine_transfer_gen ::
  "('d ⇒ 'd ⇒ 'd) ⇒ ('d ⇒ 'd) ⇒ ('d ⇒ 'd)
   ⇒ ('x,'k,unit,'d::bounded_semilattice_sup_bot,'d) man_combine_transfer
   ⇒ ('x,'k,unit,'d,'d) man_combine_transfer"
where
  "ownership_split_combine_transfer_gen cmb rg rl T m de =
     do {
       g ← man_global m ();
       res ← T (m⦇man_local := cmb (man_local m) g⦈) (cmb de g);
       _ ← man_sideg m () (rg res);
       sp_return (rl res)
     }"

text ‹
  Entry is the one boundary the pattern cannot be reused at verbatim: a call
  answers a list of alternatives rather than one successor value. The shared
  fact is read once and the wrapped entry runs once against the merged caller
  state, so every alternative comes out of the same whole state --- an actual
  may mention a global, so the alternatives cannot be computed from the local
  half alone. Each alternative then has both of its halves split, and the answer
  is the list of split pairs.

  What reaches the shared channel is the join, over every alternative, of both
  halves' global projections. A continuation is as much a product of the merged
  state as its callee entry is, and the split discards its global half;
  publishing only one of the two would need a proof that the other carries no
  global information the environment does not already hold.
›

definition ownership_split_enter_sides ::
  "('d ⇒ 'd) ⇒ ('d::bounded_semilattice_sup_bot) enter_result list ⇒ 'd"
where
  "ownership_split_enter_sides rg pairs =
     (⨆(cont, entry)←pairs. rg cont ⊔ rg entry)"

lemma ownership_split_enter_sides_Nil [simp]:
  "ownership_split_enter_sides rg [] = bot"
  by (simp add: ownership_split_enter_sides_def)

lemma ownership_split_enter_sides_Cons [simp]:
  "ownership_split_enter_sides rg ((cont, entry) # pairs)
     = rg cont ⊔ rg entry ⊔ ownership_split_enter_sides rg pairs"
  by (simp add: ownership_split_enter_sides_def)

text ‹
  What the joint publication bounds, and what it is bounded by. The two member
  rules are what a soundness proof reaches for once it has selected a covering
  alternative: that pair's two halves are each below what the call published, so
  a concretization taken against the published global still contains them. They
  stay untagged --- their conclusions are bare inequalities in ‹rg› and would
  broaden proof search wherever a ‹≤› goal appears.
›

lemma ownership_split_enter_sides_le_iff:
  "ownership_split_enter_sides rg pairs ≤ g
     ⟷ (∀(cont, entry) ∈ set pairs. rg cont ≤ g ∧ rg entry ≤ g)"
  by (induction pairs) auto

definition ownership_split_enter_transfer_gen ::
  "('d ⇒ 'd ⇒ 'd) ⇒ ('d ⇒ 'd) ⇒ ('d ⇒ 'd)
   ⇒ ('x,'k,unit,'d::bounded_semilattice_sup_bot,'d) man_enter_transfer
   ⇒ ('x,'k,unit,'d,'d) man_enter_transfer"
where
  "ownership_split_enter_transfer_gen cmb rg rl T m =
     do {
       g ← man_global m ();
       pairs ← T (m⦇man_local := cmb (man_local m) g⦈);
       _ ← man_sideg m () (ownership_split_enter_sides rg pairs);
       sp_return (map (λ(cont, entry). (rl cont, rl entry)) pairs)
     }"

subsection ‹What the compiled tree reads and publishes›

text ‹
  Soundness judges a transfer by these two observations, so they are proved once
  here, on the pattern at a whole-state transfer, rather than per carrier: the
  answer is the local projection of the merged whole state, and the contribution at
  the routed key is its global projection.
›

lemma dg_local_traverse_ownership_split_transfer_gen [simp]:
  "dg_local (traverse_program
             (transfer_program (ownership_split_transfer_gen cmb rg rl (local_transfer f))
                src (λ_. gk)) τ)
     = rl (f (cmb (dg_local (τ src)) (dg_global (τ (Inr gk)))))"
  by (simp add: traverse_transfer_program ownership_split_transfer_gen_def
      local_transfer_def sp_compile_with_def sp_bind_def sp_return_def)

lemma dg_global_sides_ownership_split_transfer_gen [simp]:
  "dg_global (sides_of_program
            (transfer_program (ownership_split_transfer_gen cmb rg rl (local_transfer f))
               src (λ_. gk)) τ (Inr gk))
     = rg (f (cmb (dg_local (τ src)) (dg_global (τ (Inr gk)))))"
  by (simp add: sides_transfer_program ownership_split_transfer_gen_def
      local_transfer_def sp_compile_with_def sp_bind_def sp_return_def)

lemma dg_local_traverse_ownership_split_combine_transfer_gen [simp]:
  "dg_local (traverse_program
             (combine_transfer_program
                (ownership_split_combine_transfer_gen cmb rg rl (local_combine_transfer h))
                src_cc src_ex (λ_. gk)) τ)
     = rl (h (cmb (dg_local (τ src_cc)) (dg_global (τ (Inr gk))))
             (cmb (dg_local (τ src_ex)) (dg_global (τ (Inr gk)))))"
  by (simp add: traverse_combine_transfer_program ownership_split_combine_transfer_gen_def
      local_combine_transfer_def sp_compile_with_def sp_bind_def sp_return_def)

lemma dg_global_sides_ownership_split_combine_transfer_gen [simp]:
  "dg_global (sides_of_program
            (combine_transfer_program
               (ownership_split_combine_transfer_gen cmb rg rl (local_combine_transfer h))
               src_cc src_ex (λ_. gk)) τ (Inr gk))
     = rg (h (cmb (dg_local (τ src_cc)) (dg_global (τ (Inr gk))))
             (cmb (dg_local (τ src_ex)) (dg_global (τ (Inr gk)))))"
  by (simp add: sides_combine_transfer_program ownership_split_combine_transfer_gen_def
      local_combine_transfer_def sp_compile_with_def sp_bind_def sp_return_def)

text ‹A whole-state transfer never asks, so the query channel the generator
  installs around the wrapper leaves it unchanged.›

lemma ownership_split_transfer_gen_local_outer_man [simp]:
  "ownership_split_transfer_gen cmb rg rl (local_transfer f) (outer_man Q m)
     = ownership_split_transfer_gen cmb rg rl (local_transfer f) m"
  by (simp add: ownership_split_transfer_gen_def local_transfer_def)
text ‹
  What the lifter reads, in the same terms. The shared slot is read before the
  wrapped transfer runs, so it is a dependency of the call whatever the wrapped
  transfer does --- and it stays one even when nothing is published there,
  which is exactly why dependencies are tracked apart from
  \<^const>‹enter_runs›'s publications. The trailing ‹man_sideg› writes rather
  than reads, so it contributes no dependency of its own.
›

lemma enter_deps_ownership_split_enter_transfer_gen [intro]:
  fixes sigma :: "'x + 'k ⇒ ('d::bounded_semilattice_sup_bot,'d) dg_state"
  assumes T: "enter_deps T (mk_dg_man (cmb d (dg_global (sigma (Inr (unknown_of ()))))) unknown_of)
                sigma pairs deps"
  shows "enter_deps (ownership_split_enter_transfer_gen cmb rg rl T) (mk_dg_man d unknown_of) sigma
           (map (λ(cont, entry). (rl cont, rl entry)) pairs)
           ({Inr (unknown_of ())} ∪ deps)"
  unfolding enter_deps_def
proof (intro allI)
  fix K
  show "dep_aux sigma (ownership_split_enter_transfer_gen cmb rg rl T (mk_dg_man d unknown_of) K)
          = ({Inr (unknown_of ())} ∪ deps)
            ∪ dep_aux sigma (K (map (λ(cont, entry). (rl cont, rl entry)) pairs))"
    by (simp add: ownership_split_enter_transfer_gen_def sp_bind_def sp_return_def
        enter_depsD[OF T] Un_assoc)
qed
text ‹
  How the lifter behaves under a solution, in the same terms as the transfer it
  wraps. The manager has to be a concrete \<^const>‹mk_dg_man›: for an arbitrary
  one ‹man_sideg m ()› is opaque and the slot it publishes at cannot be named,
  so there would be nothing to state.

  The wrapped transfer is run at the reconstructed caller state, so its
  alternatives are the ones computed against the whole state rather than the
  local half --- that is the step a caller-local-only entry could not perform.
  Its own publications survive in ‹pub›, and the lifter adds exactly one
  contribution of its own, at the routed slot.
›

lemma enter_runs_ownership_split_enter_transfer_gen [intro]:
  fixes sigma :: "'x + 'k ⇒ ('d::bounded_semilattice_sup_bot,'d) dg_state"
  assumes T: "enter_runs T (mk_dg_man (cmb d (dg_global (sigma (Inr (unknown_of ()))))) unknown_of)
                sigma pairs pub"
  shows "enter_runs (ownership_split_enter_transfer_gen cmb rg rl T) (mk_dg_man d unknown_of) sigma
           (map (λ(cont, entry). (rl cont, rl entry)) pairs)
           (pub ⊔ (bot(Inr (unknown_of ()) := DG bot (ownership_split_enter_sides rg pairs))))"
  unfolding enter_runs_def
proof (intro allI conjI)
  fix K
  show "traverse_rhs (ownership_split_enter_transfer_gen cmb rg rl T (mk_dg_man d unknown_of) K) sigma
          = traverse_rhs (K (map (λ(cont, entry). (rl cont, rl entry)) pairs)) sigma"
    by (simp add: ownership_split_enter_transfer_gen_def sp_bind_def sp_return_def
        enter_runsD_traverse[OF T])
next
  fix K
  show "sides_of_rhs (ownership_split_enter_transfer_gen cmb rg rl T (mk_dg_man d unknown_of) K) sigma
          = (pub ⊔ (bot(Inr (unknown_of ()) := DG bot (ownership_split_enter_sides rg pairs))))
            ⊔ sides_of_rhs (K (map (λ(cont, entry). (rl cont, rl entry)) pairs)) sigma"
    by (simp add: ownership_split_enter_transfer_gen_def sp_bind_def sp_return_def
        enter_runsD_sides[OF T] sup_fun_def fun_upd_def)
       (auto simp: fun_eq_iff ac_simps split: if_splits)
qed

subsection ‹The specification-to-specification lifter›

text ‹
  Every edge transfer of the argument specification is wrapped, entry through its
  own list-shaped wrapper, and the whole return pipeline is wrapped once rather
  than stage by stage: wrapping each stage separately would split and re-merge
  between them, and the second merge would read the shared fact again instead of
  the first stage's own result. So \<^const>‹dgs_combine_env› stays at its identity
  default and \<^const>‹dgs_combine_assign› carries the wrapped
  \<^const>‹dg_spec_combine_transfer› of the argument.
›

definition ownership_split_lift_gen ::
  "('d ⇒ 'd ⇒ 'd) ⇒ ('d ⇒ 'd) ⇒ ('d ⇒ 'd)
   ⇒ ('x,'k,unit,'d::bounded_semilattice_sup_bot,'d) dg_spec
   ⇒ ('x,'k,unit,'d,'d) dg_spec"
where
  "ownership_split_lift_gen cmb rg rl S = local_dg_spec_template⦇
     dgs_skip := ownership_split_transfer_gen cmb rg rl (skip⇧♯ S),
     dgs_assign := (λx e. ownership_split_transfer_gen cmb rg rl (assign⇧♯ S x e)),
     dgs_special := (λsc x. ownership_split_transfer_gen cmb rg rl (special⇧♯ S sc x)),
     dgs_branch := (λb pol. ownership_split_transfer_gen cmb rg rl (branch⇧♯ S b pol)),
     dgs_body := (λp. ownership_split_transfer_gen cmb rg rl (body⇧♯ S p)),
     dgs_return := (λe p. ownership_split_transfer_gen cmb rg rl (return⇧♯ S e p)),
     dgs_enter := (λci. ownership_split_enter_transfer_gen cmb rg rl (enter⇧♯ S ci)),
     dgs_event := (λevt. ownership_split_transfer_gen cmb rg rl (event⇧♯ S evt)),
     dgs_combine_assign :=
       (λci. ownership_split_combine_transfer_gen cmb rg rl (dg_spec_combine_transfer S ci)) ⦈"

text ‹Both eliminate a constructed wrapper specification and expose the
  corresponding transfer wrapper, in a terminating direction, so they fire
  wherever a lifted specification meets the edge or combine dispatch.›

lemma dg_spec_step_ownership_split_lift_gen [simp]:
  "dg_spec_step (ownership_split_lift_gen cmb rg rl S) a
     = ownership_split_transfer_gen cmb rg rl (dg_spec_step S a)"
  unfolding ownership_split_lift_gen_def by (cases a) simp_all

lemma dgs_enter_ownership_split_lift_gen [simp]:
  "enter⇧♯ (ownership_split_lift_gen cmb rg rl S) ci
     = ownership_split_enter_transfer_gen cmb rg rl (enter⇧♯ S ci)"
  unfolding ownership_split_lift_gen_def by simp

lemma dgs_query_ownership_split_lift_gen [simp]:
  "dgs_query (ownership_split_lift_gen cmb rg rl S) m q = sp_return ⊤"
  unfolding ownership_split_lift_gen_def by simp

lemma dg_spec_combine_transfer_ownership_split_lift_gen [simp]:
  "dg_spec_combine_transfer (ownership_split_lift_gen cmb rg rl S) ci
     = ownership_split_combine_transfer_gen cmb rg rl (dg_spec_combine_transfer S ci)"
  unfolding dg_spec_combine_transfer_def ownership_split_lift_gen_def
  by (simp add: local_transfer_def local_combine_transfer_def)

text ‹The lifter preserves well-formedness: it reads the shared slot, runs the
  wrapped transfer at a manager built the same way, publishes once and answers.
  Every step of that is a closure lemma.›

lemma sp_wf_dgs_combine_assign_ownership_split_lift_gen [intro]:
  assumes "dg_spec_wf S"
  shows
    "sp_wf (combine_assign⇧♯ (ownership_split_lift_gen cmb rg rl S) ci (mk_dg_man d unknown_of) ex)"
  unfolding ownership_split_lift_gen_def
  by (auto simp: ownership_split_combine_transfer_gen_def
      intro!: sp_wf_bind dg_spec_wf_combine[OF assms])

lemma dg_spec_wf_ownership_split_lift_gen [intro]:
  assumes "dg_spec_wf S"
  shows "dg_spec_wf (ownership_split_lift_gen cmb rg rl S)"
  unfolding dg_spec_wf_def
  by (auto simp: ownership_split_transfer_gen_def ownership_split_enter_transfer_gen_def
      ownership_split_combine_transfer_gen_def
      intro!: sp_wf_bind dg_spec_wf_step_ask[OF assms] dg_spec_wf_enter[OF assms]
        dg_spec_wf_combine[OF assms])

end