Theory DG_Manager

theory DG_Manager
  imports DG_State "Voblint_Solver.Strategy_Tree_Program" Analysis_Query
begin

section ‹A manager capability interface for the D/G packed carrier›

text ‹
  ‹man› is a capability fragment of Goblint's own manager record: ‹man_local›
  is the current local value, ‹man_global›/‹man_sideg› are ∗‹capabilities› a
  transfer runs to read or publish shared state, without naming which solver
  key that state lives at, and ‹man_ask› is the query channel, Goblint's
  ‹man.ask›. Goblint's manager carries more -- an event emitter, the current
  node and edge, spawn and split -- and none of that is modelled here, because
  no transfer in this development asks for it. Every ‹Spec› transfer takes a
  manager, including ones whose global component is trivial -- Goblint's
  default ‹Spec› sets ‹G = Lattice.Unit›, ‹V = EmptyV›, and its transfers still
  take the manager and mostly return ‹man.local›.

  ‹man_ask› answers a query about the stores the transfer's predecessor state
  describes. Like ‹man_global› it is a program, so a query handler may read
  shared state and the dependency shows up in the compiled equations. A
  handler may also ask in turn; the specification layer (‹DG_Spec›) bounds the
  recursion and answers ‹⊤› on a cycle, as Goblint's ‹MCP› does.

  Five type parameters run through this theory and every one built on it:

    ▪ ‹'x› --- a local solver unknown, the name of a program point under a
      context.
    ▪ ‹'k› --- a solver global key, the whole side-effect address space.
    ▪ ‹'v› --- an analysis-visible global name, Goblint's ‹V›. It embeds into
      ‹'k›, and is exactly the part of that space an analysis may address.
    ▪ ‹'dl› --- the local domain, Goblint's ‹D›.
    ▪ ‹'dg› --- the analysis-global domain, Goblint's ‹G›.

  Both capabilities take a global name rather than a key: an analysis says
  ‹man_global m v›, naming which of its globals it means, and never builds a
  solver key. Which key that name lives at is the manager's business ---
  ‹mk_dg_man› takes the embedding ‹'v ⇒ 'k› and closes it into both fields.
  An analysis with a single global instantiates ‹'v = unit› and writes
  ‹man_global m ()›. The separation matters because ‹'k› also carries the
  routed activation slots, which belong to the generator and to no analysis.

  A Base-style specification ignores the global channel entirely: it calls
  neither capability, so its compiled equations carry no ‹QueryG› and no
  ‹Side›. An effectful specification reaches the current routed global slot
  through ‹man_global›/‹man_sideg›. Which of the two a given analysis is
  therefore shows up in its compiled trees, not in this interface.

  ‹dg_read_global› and ‹dg_sideg› are what interpret those capabilities
  against the packed ‹('dl,'dg) dg_state› carrier; ‹mk_dg_man› is where the
  embedding ‹unknown_of› is closed into them, so it is the only place a name becomes a
  key. Either way a transfer written against ‹man›'s fields sees neither the
  packed carrier nor a key.
›

subsection ‹The manager record›

record ('x,'k,'v,'dl,'dg) man =
  man_local :: 'dl
  man_global :: "'v ⇒ ('x,'k,('dl,'dg) dg_state,'dg) strategy_program"
  man_sideg :: "'v ⇒ 'dg ⇒ ('x,'k,('dl,'dg) dg_state,unit) strategy_program"
  man_ask :: "query ⇒ ('x,'k,('dl,'dg) dg_state,answer) strategy_program"

subsection ‹Packed-carrier primitives›

text ‹
  A solver unknown holds a whole \<^type>‹dg_state›, so reading one yields both
  halves and only one of them is ever wanted. ‹dg_read_at› reads any unknown
  and keeps \<^const>‹dg_local›; ‹dg_read_global› reads a global key and keeps
  \<^const>‹dg_global›; ‹dg_sideg› publishes a global contribution, padding the local
  half it does not write with ‹bot›.

  These three are where the packed carrier is taken apart and put back
  together. The framework's own transfer constructors use only these and
  ‹man›'s fields, and an analysis author is expected to do the same; the
  transfer type does not enforce it, since a transfer may build any
  ‹strategy_program› it likes. The tree formers that assemble a right-hand side
  do construct \<^const>‹DG› values directly.
›

definition dg_read_at :: "'x + 'k ⇒ ('x,'k,('dl,'dg) dg_state,'dl) strategy_program" where
  "dg_read_at src = sp_read_at src ⤜ (sp_return o dg_local)"

definition dg_read_global :: "'k ⇒ ('x,'k,('dl,'dg) dg_state,'dg) strategy_program" where
  "dg_read_global gk = sp_read_global gk ⤜ (sp_return o dg_global)"

definition dg_sideg :: "'k ⇒ 'dg ⇒ ('x,'k,('dl::bot,'dg) dg_state,unit) strategy_program" where
  "dg_sideg gk gd = sp_publish gk (DG bot gd)"

subsection ‹What the primitives do, observed›

text ‹
  Each primitive contributes one step to a compiled tree, and the three
  observations a solver makes of that tree --- its answer, its publications,
  its dependencies --- see exactly that step and then continue into the
  continuation. Proving it once here is what keeps later proofs off the
  encoding: without these, every fact about a compiled transfer has to case on
  the address and unfold \<^const>‹sp_bind›, \<^const>‹sp_return› and the read
  primitives to reach its own subject.

  They are ‹simp› rules in the direction that eliminates a primitive and
  exposes the value it read, and they terminate because the program strictly
  shrinks at each step.
›

lemma traverse_dg_read_at [simp]:
  "traverse_rhs (dg_read_at src K) τ = traverse_rhs (K (dg_local (τ src))) τ"
  by (cases src) (simp_all add: dg_read_at_def sp_bind_def sp_read_local_def
      sp_read_global_def sp_return_def)

lemma sides_dg_read_at [simp]:
  "sides_of_rhs (dg_read_at src K) τ = sides_of_rhs (K (dg_local (τ src))) τ"
  by (cases src) (simp_all add: dg_read_at_def sp_bind_def sp_read_local_def
      sp_read_global_def sp_return_def)

lemma dep_aux_dg_read_at [simp]:
  "dep_aux τ (dg_read_at src K) = insert src (dep_aux τ (K (dg_local (τ src))))"
  by (cases src) (simp_all add: dg_read_at_def sp_bind_def sp_read_local_def
      sp_read_global_def sp_return_def)

lemma traverse_dg_read_global [simp]:
  "traverse_rhs (dg_read_global gk K) τ = traverse_rhs (K (dg_global (τ (Inr gk)))) τ"
  by (simp add: dg_read_global_def sp_bind_def sp_read_global_def sp_return_def)

lemma sides_dg_read_global [simp]:
  "sides_of_rhs (dg_read_global gk K) τ = sides_of_rhs (K (dg_global (τ (Inr gk)))) τ"
  by (simp add: dg_read_global_def sp_bind_def sp_read_global_def sp_return_def)

lemma dep_aux_dg_read_global [simp]:
  "dep_aux τ (dg_read_global gk K)
     = insert (Inr gk) (dep_aux τ (K (dg_global (τ (Inr gk)))))"
  by (simp add: dg_read_global_def sp_bind_def sp_read_global_def sp_return_def)

lemma traverse_dg_sideg [simp]:
  "traverse_rhs (dg_sideg gk gd K) τ = traverse_rhs (K ()) τ"
  by (simp add: dg_sideg_def sp_publish_def)

lemma dep_aux_dg_sideg [simp]:
  "dep_aux τ (dg_sideg gk gd K) = dep_aux τ (K ())"
  by (simp add: dg_sideg_def sp_publish_def)

text ‹Publication is the one primitive an observation does not simply pass
  through: it raises the contribution at its own key and leaves every other
  key to the continuation.›

lemma sides_dg_sideg [simp]:
  "sides_of_rhs (dg_sideg gk gd K) τ = sides_of_rhs (K ()) τ ⊔ bot(Inr gk := DG bot gd)"
  by (simp add: dg_sideg_def sp_publish_def Let_def fun_eq_iff sup_fun_def)

text ‹Each primitive runs its continuation once, so a transfer assembled from
  them does too and the fold's well-formedness side conditions discharge by
  ‹simp› wherever a concrete transfer is in hand.›

lemma sp_wf_dg_read_at [intro, simp]: "sp_wf (dg_read_at src)"
  unfolding dg_read_at_def by (intro sp_wf_bind) (simp_all add: comp_def)

lemma sp_wf_dg_read_global [intro, simp]: "sp_wf (dg_read_global gk)"
  unfolding dg_read_global_def by (intro sp_wf_bind) (simp_all add: comp_def)

lemma sp_wf_dg_sideg [intro, simp]: "sp_wf (dg_sideg gk gd)"
  by (simp add: dg_sideg_def)

subsection ‹Constructing a manager›

text ‹
  ‹mk_dg_man› closes the name-to-key embedding into both effectful fields, so
  a transfer built against ‹man› never sees a key itself. A manager-native
  transfer should reach shared state through the record fields rather than
  call ‹dg_read_global›/‹dg_sideg› or name a key directly, so that a future
  manager (instrumented, differently routed, or backed by distinct global
  unknowns) is a second interpretation of the same fields rather than a change
  to any transfer.

  A built manager answers every query with ‹⊤›, the claim that holds of
  every store. Whoever runs a specification installs a real query channel on
  top: the equation generator installs the specification's own query
  (‹dg_spec_edge_program›), and a product of specifications installs the
  meet of its components' answers.
›

definition mk_dg_man :: "'dl::bot ⇒ ('v ⇒ 'k) ⇒ ('x,'k,'v,'dl,'dg) man" where
  "mk_dg_man d unknown_of = ⦇
     man_local = d,
     man_global = (λv. dg_read_global (unknown_of v)),
     man_sideg = (λv. dg_sideg (unknown_of v)),
     man_ask = (λ_. sp_return ⊤) ⦈"

text ‹
  What a built manager answers, and the one way it is rebuilt: a second transfer
  stage runs from the point the first reached, and since only the local value
  changes, that update is again a manager built at the new value. These are the
  rules the proofs need; \<^const>‹mk_dg_man› itself stays folded, so a manager
  travels through a goal as one term instead of a three-field record literal.
  Keeping \<^const>‹mk_dg_man› folded also preserves matching: an assumption
  about a built manager would stop matching if the goal decayed into a record
  literal.

  The two capability rules are stated unapplied. Applying one is the same rule
  plus a beta step, so the unapplied form subsumes the applied one and also
  rewrites the occurrences that carry no argument --- a manager passed whole to
  an entry transfer, for instance.
›

lemma mk_dg_man_simps [simp]:
  "man_local (mk_dg_man d unknown_of) = d"
  "man_global (mk_dg_man d unknown_of) = (λv. dg_read_global (unknown_of v))"
  "man_sideg (mk_dg_man d unknown_of) = (λv. dg_sideg (unknown_of v))"
  "man_ask (mk_dg_man d unknown_of) = (λ_. sp_return ⊤)"
  by (simp_all add: mk_dg_man_def)

lemma mk_dg_man_local_update [simp]:
  "mk_dg_man d unknown_of⦇man_local := e⦈ = mk_dg_man e unknown_of"
  "mk_dg_man d unknown_of⦇man_ask := A, man_local := e⦈ = mk_dg_man e unknown_of⦇man_ask := A⦈"
  by (simp_all add: mk_dg_man_def)

type_synonym ('x,'k,'v,'dl,'dg) man_transfer =
  "('x,'k,'v,'dl,'dg) man ⇒ ('x,'k,('dl,'dg) dg_state,'dl) strategy_program"

text ‹
  A query handler takes the same manager and answers the query in the answer
  lattice, Goblint's ‹Spec.query man q›.
›

type_synonym ('x,'k,'v,'dl,'dg) man_query =
  "('x,'k,'v,'dl,'dg) man ⇒ query ⇒ ('x,'k,('dl,'dg) dg_state,answer) strategy_program"

text ‹
  A combine-shaped transfer takes the same manager plus the callee-exit
  value as an ordinary trailing argument, the way Goblint's
  ‹combine_env›/‹combine_assign› take the same ‹man› plus a ‹D.t›.
›

type_synonym ('x,'k,'v,'dl,'dg) man_combine_transfer =
  "('x,'k,'v,'dl,'dg) man ⇒ 'dl ⇒ ('x,'k,('dl,'dg) dg_state,'dl) strategy_program"

text ‹
  A call answers a list of alternatives, and each alternative is a pair: the
  value the caller resumes with once the callee returns, and the value the
  callee starts from. This is Goblint's ‹Spec.enter›, whose result is a list of
  such pairs. The two halves must be produced by one run of the transfer,
  because an alternative's continuation is only meaningful against the callee
  entry it was computed with; a program answering the pairs keeps them together
  and leaves the caller free to consume them however the equation shape needs.

  The result is not a ‹'dl›, so an entry transfer is not a
  \<^type>‹man_transfer›: it cannot be the answer of an equation on its own, and
  whatever consumes it must reduce the list to one local value first.
›

type_synonym 'dl enter_result = "'dl × 'dl"

type_synonym ('x,'k,'v,'dl,'dg) man_enter_transfer =
  "('x,'k,'v,'dl,'dg) man
   ⇒ ('x,'k,('dl,'dg) dg_state,'dl enter_result list) strategy_program"

text ‹
  A second transfer stage runs from the point the first reached by updating
  \<^const>‹man_local› in place --- ‹m⦇man_local := d⦈› --- leaving both
  capabilities as they were. Nothing is extracted out of the program and
  re-wrapped, and the record's own update equations are all the later proofs
  need about it.
›

end