Theory DG_Spec

theory DG_Spec
  imports DG_Manager "Voblint_CFG.CFG_Def"
begin

section ‹What an analysis supplies: manager-native transfers›

text ‹
  An analysis supplies one manager-native transfer per edge action and the
  pieces of the call/return protocol. A transfer takes a ‹man› and returns
  a ‹strategy_program›: global reads are ‹man_global› calls, global
  publications are ‹man_sideg› calls, and a transfer that makes neither
  compiles to a tree with no ‹QueryG› and no ‹Side› at all. This replaces the
  state-threading shape ‹'dl ⇒ 'dg ⇒ 'dg × 'dl›, which forced every transfer to
  republish the global it read even where the global channel is provably inert.

  What a program answers with depends on the field. An edge transfer and a
  combine stage answer the successor local value, so their compiled tree is an
  equation's right-hand side outright. Entry answers a list of alternatives
  instead, which no equation carries: the routed call program consumes that list,
  running one activation and return combine per alternative and joining what
  they contribute.

  There is one interface here, not a hierarchy of them. A specification is
  ∗‹local-only› when every field is a pure function of the values it is handed
  --- ‹local_transfer› for the edge fields, ‹local_enter_transfer› for entry ---
  and ∗‹effectful› when some field reads or publishes through
  ‹man_global›/‹man_sideg›. Those words describe what a given specification's
  compiled trees do, and are read off those trees -- they are not a
  classification the framework branches on.
›


text ‹
  An ‹analysis_event› is an analyzer-visible occurrence distinct from an ordinary
  control-flow transfer: a domain may observe it, but it must not by itself refine
  execution. The channel mirrors Goblint's separation of its ordinary ‹Spec›
  transfer methods (‹assign›/‹branch›/‹skip›/...) from ‹Spec.event›. The
  check itself does not: Goblint handles ‹__goblint_check› in ‹special›, as
  the library description ‹Assert {check = true; refine = false}›, and its
  ‹Events.Assert› is emitted only by the ‹abortUnless› analysis and refines
  the state in Base (goblint/analyzer ‹5320a6b7›: ‹libraryFunctions.ml›,
  ‹assert.ml›, ‹base.ml›). Voblint's sole current event is a check's
  condition, which never refines; the
  vocabulary is deliberately left open rather than pre-populated, so that a future
  VIMP source construct with no current counterpart (e.g. a diagnostic-only
  annotation) adds a constructor here instead of a new specification field. A
  construct that narrows feasible execution, such as ‹assume›, is not a
  candidate: it belongs on ‹dgs_branch› or on a new refining field, not here.

  It is declared here, beside the ‹dgs_event› field it types, because the
  specification record and the edge-action dispatcher that feeds it are the only
  things that ever case on it.
›

datatype analysis_event =
  Check_Event check_label exp

record ('x,'k,'v,'dl,'dg) dg_spec =
  dgs_skip           :: "('x,'k,'v,'dl,'dg) man_transfer" ("skip⇧♯")
  dgs_assign         :: "vname ⇒ exp ⇒ ('x,'k,'v,'dl,'dg) man_transfer" ("assign⇧♯")
  dgs_special        :: "special_call ⇒ vname ⇒ ('x,'k,'v,'dl,'dg) man_transfer" ("special⇧♯")
  dgs_branch         :: "exp ⇒ bool ⇒ ('x,'k,'v,'dl,'dg) man_transfer" ("branch⇧♯")
  dgs_body           :: "pname ⇒ ('x,'k,'v,'dl,'dg) man_transfer" ("body⇧♯")
  dgs_return         :: "exp option ⇒ pname ⇒ ('x,'k,'v,'dl,'dg) man_transfer" ("return⇧♯")
  dgs_enter          :: "call_info ⇒ ('x,'k,'v,'dl,'dg) man_enter_transfer" ("enter⇧♯")
  dgs_event          :: "analysis_event ⇒ ('x,'k,'v,'dl,'dg) man_transfer" ("event⇧♯")
  dgs_combine_env    :: "call_info ⇒ ('x,'k,'v,'dl,'dg) man_combine_transfer" ("combine'_env⇧♯")
  dgs_combine_assign :: "call_info ⇒ ('x,'k,'v,'dl,'dg) man_combine_transfer" ("combine'_assign⇧♯")
  dgs_query          :: "('x,'k,'v,'dl,'dg) man_query"

text ‹
  ‹dgs_query› is Goblint's ‹Spec.query›: it answers a query from the manager
  it is given, and may read globals or ask further queries through it. What an
  answer claims is fixed by \<^const>‹eval_holds›; answering ‹⊤› claims
  nothing.
›

text ‹
  Every field carries the Goblint ‹Spec› method name it answers to, marked
  ‹⇧♯›. A specification therefore reads in the analyzer's vocabulary,
  and the marker keeps the abstract operation apart from the concrete one it
  over-approximates: \<^const>‹combine_env› merges two stores, whereas
  ‹combine_env⇧♯› is the field a domain fills to describe that merge.
  The whole-state combine wears the same marker as ‹combine⇧♯›, so it
  means one thing on both sides of the transfer boundary.

  Two of the names contain an underscore, which a mixfix template would
  otherwise read as an argument slot, so they escape it as ‹'_›. The
  selector names stay available for record construction and update, neither of
  which takes notation.
›

text ‹
  Procedure-return combine is split the same way Goblint's ‹Spec› splits
  it: an environment merge followed by a return-value assign, both taking
  the same manager plus the callee exit. The composed form sequences them
  monadically -- ‹combine_assign› runs from the point ‹combine_env›
  reached, against the same manager with \<^const>‹man_local› updated to that
  point, so any effects ‹combine_env› emitted stay in the program and nothing
  is extracted into a pure pair in between.
›

definition dg_spec_combine_transfer ::
  "('x,'k,'v,'dl,'dg) dg_spec ⇒ call_info ⇒ ('x,'k,'v,'dl,'dg) man_combine_transfer"
where
  "dg_spec_combine_transfer S ci m exit =
     do {
       d_env ← combine_env⇧♯ S ci m exit;
       combine_assign⇧♯ S ci (m⦇man_local := d_env⦈) exit
     }"

text ‹
  ‹EA_Check› routes through \<^const>‹dgs_event› rather than \<^const>‹dgs_skip›:
  a check is an analysis event (on the channel that mirrors Goblint's
  ‹Spec.event›; Goblint's own check goes through ‹special›, see
  ‹analysis_event› above), and conflating it with skip would make a future domain's
  non-identity skip silently change what a check edge does. A concrete
  ‹dg_spec› therefore supplies its own notion of a
  check event directly, the same way it already supplies
  \<^const>‹dgs_body›/\<^const>‹dgs_return›.
›

fun dg_spec_step ::
  "('x,'k,'v,'dl,'dg,'z) dg_spec_scheme ⇒ edge_action ⇒ ('x,'k,'v,'dl,'dg) man_transfer"
where
  "dg_spec_step S EA_Nop            = skip⇧♯ S"
| "dg_spec_step S (EA_Assign x e)   = assign⇧♯ S x e"
| "dg_spec_step S (EA_Special sc x) = special⇧♯ S sc x"
| "dg_spec_step S (EA_Assume b)     = branch⇧♯ S b True"
| "dg_spec_step S (EA_AssumeNot b)  = branch⇧♯ S b False"
| "dg_spec_step S (EA_Body p)       = body⇧♯ S p"
| "dg_spec_step S (EA_Ret e p)      = return⇧♯ S e p"
| "dg_spec_step S (EA_Check l cnd)  = event⇧♯ S (Check_Event l cnd)"

subsection ‹Compiling a specification to right-hand sides›

text ‹
  An edge equation reads the source unknown, builds the manager around it with
  the routed key closed in, and runs the specification's transfer. Every
  generator's edge right-hand side is a ‹dg_spec_edge_program›.
›

text ‹
  The driver underneath: read the source unknown, close the key into a fresh
  manager around what came back, and run the transfer once. The transfer itself
  never sees the key, only whatever the manager's fields already close over.
›

definition transfer_program_at ::
  "('x,'k,'v,'dl,'dg) man_transfer ⇒ 'x + 'k ⇒ ('v ⇒ 'k)
   ⇒ ('x,'k,('dl::bot,'dg) dg_state,'dl) strategy_program"
where
  "transfer_program_at transfer src unknown_of =
     do {
       d ← dg_read_at src;
       transfer (mk_dg_man d unknown_of)
     }"

definition transfer_program ::
  "('x,'k,'v,'dl::bot,'dg::bot) man_transfer ⇒ 'x + 'k ⇒ ('v ⇒ 'k)
   ⇒ ('x,'k,('dl,'dg) dg_state,('dl,'dg) dg_state) strategy_program"
where
  "transfer_program T src unknown_of = sp_map (λd. DG d bot) (transfer_program_at T src unknown_of)"

text ‹
  Before the specification's edge transfer runs, its query channel is set to
  the specification's own answers about the state the edge starts from, as
  Goblint's ‹MCP› builds ‹outer_man› around the predecessor. Every transfer on
  the edge sees the same channel, and nothing it computes changes it.

  A handler may ask in turn, through a manager whose channel is the same
  construction one level down. As in Goblint's ‹MCP.query'›, a query already
  being asked answers ‹⊤› instead of recursing, the result lattice's top on
  a cycle. The depth bound has no counterpart in Goblint: queries range over
  an infinite type, so cycle detection alone does not make the recursion
  total. Exhausting it aborts the generated program, so a bound that is too
  small shows up as a failed run and never as a silent loss of precision.
  Logically \<^const>‹Code.abort› is its fallback, here ‹⊤›, which holds of
  every store, so the bound plays no part in soundness.

  The channel depends on the specification only through its handler, so a
  specification derived by overriding other fields keeps the same channel.
›

definition query_depth :: nat where
  "query_depth = 1024"

fun ask_with ::
  "('x,'k,'v,'dl,'dg) man_query ⇒ nat ⇒ query set ⇒ ('x,'k,'v,'dl,'dg) man
   ⇒ query ⇒ ('x,'k,('dl,'dg) dg_state,answer) strategy_program"
where
  "ask_with Q 0 asked m q =
     Code.abort (STR ''query recursion exceeded query_depth'') (λ_. sp_return ⊤)"
| "ask_with Q (Suc n) asked m q =
     (if q ∈ asked then sp_return ⊤
      else Q (m⦇man_ask := ask_with Q n (insert q asked) m⦈) q)"

definition outer_man ::
  "('x,'k,'v,'dl,'dg) man_query ⇒ ('x,'k,'v,'dl,'dg) man ⇒ ('x,'k,'v,'dl,'dg) man"
where
  "outer_man Q m = m⦇man_ask := ask_with Q query_depth {} m⦈"

lemma outer_man_simps [simp]:
  "man_local (outer_man Q m) = man_local m"
  "man_global (outer_man Q m) = man_global m"
  "man_sideg (outer_man Q m) = man_sideg m"
  "man_ask (outer_man Q m) = ask_with Q query_depth {} m"
  by (simp_all add: outer_man_def)

definition dg_spec_edge_program ::
  "('x,'k,'v,'dl::bot,'dg::bot) dg_spec ⇒ edge_action ⇒ 'x + 'k ⇒ ('v ⇒ 'k)
   ⇒ ('x,'k,('dl,'dg) dg_state,('dl,'dg) dg_state) strategy_program"
where
  "dg_spec_edge_program S a src unknown_of =
     transfer_program (λm. dg_spec_step S a (outer_man (dgs_query S) m)) src unknown_of"

text ‹
  What compilation costs an observation: exactly the source read, and then the
  transfer run at the value that read produced. Everything a proof about a
  compiled edge needs from the encoding is here, so nothing downstream has to
  case on the address or unfold the program monad again.

  Left untagged. Rewriting a compiled tree back into a manager application
  grows the term, and the direction is only wanted where a proof is about to
  reason about the transfer itself; the primitive laws in
  \<^theory>‹Voblint_Framework.DG_Manager› are the ones that should fire
  everywhere.
›

lemma traverse_transfer_program:
  "traverse_program (transfer_program T src unknown_of) τ
     = traverse_rhs (sp_compile_with (λd. DG d bot) (T (mk_dg_man (dg_local (τ src)) unknown_of))) τ"
  by (simp add: transfer_program_def transfer_program_at_def sp_compile_with_def sp_bind_def)

lemma sides_transfer_program:
  "sides_of_program (transfer_program T src unknown_of) τ
     = sides_of_rhs (sp_compile_with (λd. DG d bot) (T (mk_dg_man (dg_local (τ src)) unknown_of))) τ"
  by (simp add: transfer_program_def transfer_program_at_def sp_compile_with_def sp_bind_def)

lemma dep_transfer_program:
  "dep_program τ (transfer_program T src unknown_of)
     = insert src
         (dep_aux τ (sp_compile_with (λd. DG d bot) (T (mk_dg_man (dg_local (τ src)) unknown_of))))"
  by (simp add: transfer_program_def transfer_program_at_def sp_compile_with_def sp_bind_def)

subsection ‹Specifications whose transfers run their continuation once›

text ‹
  A \<^type>‹man_transfer› is a function from a continuation to a tree, so a
  specification could in principle write one that drops or duplicates it.
  \<^const>‹sp_wf› rules that out, and the generator's fold needs it: what a
  contribution publishes is only well posed for a transfer that runs its
  continuation once.

  ‹dg_spec_wf› asks it of the four ways a specification is run --- an edge
  step, a query, the entry alternatives, and the two-stage combine --- and only
  at the managers that actually occur, the ones \<^const>‹mk_dg_man› builds. An
  edge step and a query handler run under a query channel installed around that
  manager, so they are asked for every channel that is itself well formed; a
  wrapper that reruns a step at a rebuilt manager needs exactly that
  generality. That restriction is not a
  weakening: a transfer never meets any other manager, and an arbitrary one has
  opaque capability fields about which nothing could be said. A specification
  written with the manager's own primitives satisfies all four by ‹simp›,
  since every primitive and every combinator carries a closure lemma.
›

definition dg_spec_wf :: "('x,'k,'v,'dl::bot,'dg) dg_spec ⇒ bool" where
  "dg_spec_wf S ⟷
     (∀a d unknown_of ch. (∀q. sp_wf (ch q))
          ⟶ sp_wf (dg_spec_step S a ((mk_dg_man d unknown_of)⦇man_ask := ch⦈)))
     ∧ (∀d unknown_of ch q. (∀q'. sp_wf (ch q'))
          ⟶ sp_wf (dgs_query S ((mk_dg_man d unknown_of)⦇man_ask := ch⦈) q))
     ∧ (∀ci d unknown_of. sp_wf (enter⇧♯ S ci (mk_dg_man d unknown_of)))
     ∧ (∀ci d unknown_of ex. sp_wf (dg_spec_combine_transfer S ci (mk_dg_man d unknown_of) ex))"

lemma dg_spec_wf_step_ask:
  "dg_spec_wf S ⟹ (⋀q. sp_wf (ch q))
   ⟹ sp_wf (dg_spec_step S a ((mk_dg_man d unknown_of)⦇man_ask := ch⦈))"
  by (simp add: dg_spec_wf_def)

lemma dg_spec_wf_query:
  "dg_spec_wf S ⟹ (⋀q. sp_wf (ch q))
   ⟹ sp_wf (dgs_query S ((mk_dg_man d unknown_of)⦇man_ask := ch⦈) q)"
  by (simp add: dg_spec_wf_def)

lemma sp_wf_ask_with:
  assumes "dg_spec_wf S"
  shows "sp_wf (ask_with (dgs_query S) n asked (mk_dg_man d unknown_of) q)"
proof (induction n arbitrary: asked q)
  case (Suc n)
  then show ?case
    using assms by (simp add: dg_spec_wf_def)
qed simp

lemma dg_spec_wf_step:
  "dg_spec_wf S ⟹ sp_wf (dg_spec_step S a (outer_man (dgs_query S) (mk_dg_man d unknown_of)))"
  unfolding outer_man_def by (intro dg_spec_wf_step_ask sp_wf_ask_with)

lemma dg_spec_wf_enter:
  "dg_spec_wf S ⟹ sp_wf (enter⇧♯ S ci (mk_dg_man d unknown_of))"
  by (simp add: dg_spec_wf_def)

lemma dg_spec_wf_combine:
  "dg_spec_wf S ⟹ sp_wf (dg_spec_combine_transfer S ci (mk_dg_man d unknown_of) ex)"
  by (simp add: dg_spec_wf_def)

lemma sp_wf_transfer_program [intro]:
  assumes "⋀d. sp_wf (T (mk_dg_man d unknown_of))"
  shows "sp_wf (transfer_program T src unknown_of)"
  unfolding transfer_program_def transfer_program_at_def
  by (intro sp_wf_map sp_wf_bind sp_wf_dg_read_at assms)

lemma sp_wf_dg_spec_edge_program [intro]:
  "dg_spec_wf S ⟹ sp_wf (dg_spec_edge_program S a src unknown_of)"
  unfolding dg_spec_edge_program_def
  by (intro sp_wf_transfer_program) (rule dg_spec_wf_step)

subsection ‹Writing a transfer›

text ‹
  An analysis author writes manager-native transfers and nothing else. The
  framework turns them into solver right-hand sides; \<^const>‹QueryL›,
  \<^const>‹QueryG› and \<^const>‹Side› belong to that step, and a specification
  field that names one has reached past the interface into the solver's. That
  is a discipline, not something the types rule out: a transfer returns a
  \<^type>‹strategy_program› and could build any of them by hand. Three recipes
  cover every field of a \<^type>‹dg_spec› without doing so:

    ▪ A transfer that only transforms the local value is ‹local_transfer f›,
      and its compiled tree is one read and an answer: no ‹QueryG›, no
      ‹Side›.
    ▪ A transfer that reads or publishes shared state runs the capabilities
      in sequence and answers the new local value ---
      ‹do {g <- man_global m v; _ <- man_sideg m v g'; sp_return d'}› --- which
      is the same shape as the Goblint method that reads ‹man.global›, calls
      ‹man.sideg›, and returns a ‹D.t›.
    ▪ An entry transfer answers the list of alternatives instead of one
      value: ‹sp_return [(continuation, entry), ...]›, possibly after the same
      capability calls. It never folds that list; the routed call program does.
›

subsection ‹Local-only transfers›

text ‹
  The local-only shape: a pure transformation of the local value, touching
  no global at all. Its compiled edge tree is one source read followed
  directly by the answer -- no ‹QueryG›, no ‹Side› -- so its side
  contribution is ‹bot› at every key and its dependency set is exactly the
  source unknown. The global channel simply does not appear in these
  compile-down facts, which is what makes a local-only specification's
  soundness argument collapse to plain inclusions on pure functions.
›

definition local_transfer :: "('dl ⇒ 'dl) ⇒ ('x,'k,'v,'dl,'dg) man_transfer" where
  "local_transfer f m = sp_return (f (man_local m))"

lemma local_transfer_outer_man [simp]:
  "local_transfer f (outer_man Q m) = local_transfer f m"
  by (simp add: local_transfer_def)

subsection ‹Answers and the local query handler›

text ‹
  A transfer that consults the query channel receives the answers as an
  ordinary function argument, so a proof about the transfer quantifies over
  them. A question nobody answers is answered ‹⊤›, which claims nothing.
›

type_synonym channel = "query ⇒ answer"

text ‹
  The local query handler: answers are a pure function of the local value.
  Such a handler never asks in turn, so the recursive channel the generator
  installs around it reduces to the handler itself.
›

definition local_query :: "('dl ⇒ channel) ⇒ ('x,'k,'v,'dl,'dg) man_query" where
  "local_query h m q = sp_return (h (man_local m) q)"

lemma local_query_update [simp]:
  "local_query h (m⦇man_ask := ch⦈) = local_query h m"
  by (simp add: local_query_def fun_eq_iff)

lemma local_transfer_update [simp]:
  "local_transfer f (m⦇man_ask := ch⦈) = local_transfer f m"
  by (simp add: local_transfer_def)

lemma ask_with_local_query:
  "ask_with (local_query h) n asked m q
     = sp_return (if n = 0 ∨ q ∈ asked then ⊤ else h (man_local m) q)"
  by (cases n) (simp_all add: local_query_def)

lemma outer_man_local_query [simp]:
  "outer_man (local_query h) m = m⦇man_ask := local_query h m⦈"
  unfolding outer_man_def
  by (simp add: ask_with_local_query query_depth_def local_query_def fun_eq_iff)


text ‹
  The entry counterpart: the alternatives are a pure function of the caller
  value, so the program reads no unknown and publishes nothing. ‹f› answers the
  whole list, which is what lets a local-only specification still offer several
  alternatives.
›

definition local_enter_transfer ::
  "('dl ⇒ 'dl enter_result list) ⇒ ('x,'k,'v,'dl,'dg) man_enter_transfer"
where
  "local_enter_transfer f m = sp_return (f (man_local m))"

lemma sp_compile_transfer_program_local_transfer:
  "sp_compile (transfer_program (local_transfer f) (Inl x) unknown_of)
     = QueryL x (λa. Answer (DG (f (dg_local a)) bot))"
  "sp_compile (transfer_program (local_transfer f) (Inr g) unknown_of)
     = QueryG g (λa. Answer (DG (f (dg_local a)) bot))"
  by (simp_all add: transfer_program_def transfer_program_at_def local_transfer_def
      dg_read_at_def sp_bind_assoc sp_compile_def sp_compile_with_def
      sp_bind_def sp_return_def sp_read_local_def sp_read_global_def)

lemma traverse_local_transfer_program [simp]:
  "traverse_program (transfer_program (local_transfer f) src unknown_of) τ = DG (f (dg_local (τ src))) bot"
  by (cases src) (simp_all add: sp_compile_transfer_program_local_transfer)

lemma sides_local_transfer_program [simp]:
  "sides_of_program (transfer_program (local_transfer f) src unknown_of) τ k = bot"
  by (cases src) (simp_all add: sp_compile_transfer_program_local_transfer)

lemma dep_local_transfer_program [simp]:
  "dep_program τ (transfer_program (local_transfer f) src unknown_of) = {src}"
  by (cases src) (simp_all add: sp_compile_transfer_program_local_transfer)

subsection ‹Local-only combine›

text ‹
  The combine counterpart: a pure function of the caller-continuation and
  callee exit states, no global contact. When both stages --- ‹combine_env⇧♯›
  and ‹combine_assign⇧♯› --- are local, the whole return pipeline collapses
  monadically to one pure composition -- the sequencing updates
  \<^const>‹man_local› and extracts nothing -- and the
  compiled combine tree is two reads and an answer, with no contribution
  and dependencies exactly the two sources.
›

definition local_combine_transfer ::
  "('dl ⇒ 'dl ⇒ 'dl) ⇒ ('x,'k,'v,'dl,'dg) man_combine_transfer"
where
  "local_combine_transfer f m exit = sp_return (f (man_local m) exit)"

lemma dg_spec_combine_transfer_local:
  assumes "combine_env⇧♯ S ci = local_combine_transfer ce"
    and "combine_assign⇧♯ S ci = local_combine_transfer ca"
  shows "dg_spec_combine_transfer S ci m exit
           = sp_return (ca (ce (man_local m) exit) exit)"
  by (simp add: dg_spec_combine_transfer_def assms local_combine_transfer_def)

subsection ‹The reads every compiled transfer makes›

text ‹
  A compiled edge tree begins by reading its source unknown, and a compiled
  combine tree by reading the call site and the callee exit, before the
  transfer runs at all. Those reads are therefore dependencies of ∗‹any›
  specification's tree, effectful or not -- unlike the global key, which
  appears only when the transfer actually queries it. Coverage arguments
  need exactly these, so they are stated once here rather than as an exact
  dependency set that would hold only for one kind of specification.
›

lemma dep_transfer_program_source:
  "src ∈ dep_program τ (transfer_program T src gk)"
  by (simp add: dep_transfer_program)

lemma dep_dg_spec_edge_program_source:
  "src ∈ dep_program τ (dg_spec_edge_program S a src gk)"
  unfolding dg_spec_edge_program_def by (rule dep_transfer_program_source)

subsection ‹A default specification, and overriding its fields›

text ‹
  ‹local_dg_spec_template› is the identity local-only specification: every
  transfer hands back the local value it was given, and a return combine
  keeps the caller's. An analysis starts from it and overrides the fields
  it implements --
  ‹local_dg_spec_template⦇dgs_assign := ..., dgs_branch := ...⦈› -- the way a
  Goblint ‹Spec› includes ‹DefaultSpec› and defines only the transfers it
  needs.

  It is named a template, not a default, because it is not Goblint's default
  behavior and nothing here treats it as one: it is the record every field of
  which is still to be chosen.

  This is a construction scaffold, not a soundness result. Leaving a field
  at the identity is a claim about that analysis: that ignoring the edge is
  sound for it. It is false in general -- an assignment analysis that leaves
  ‹dgs_assign› at the identity does not track assignments -- and nothing here
  checks it. Whether a specification, defaulted fields included, means
  anything is settled by ‹analysis_contract› together with the entry
  obligation that locale deliberately leaves open --- never by how the record
  was assembled.

  It is also not a transcription of Goblint's ‹IdentitySpec›, and the return
  combine is where the two differ: both stages here keep the value they are
  handed, so the composed default keeps the ∗‹caller› continuation, whereas
  Goblint's ‹combine_env› answers the callee exit and its ‹combine_assign›
  answers ‹man.local›, so the composed default there ends at the callee's
  value. Both are neutral for their own purpose; this one is neutral for
  ∗‹record update›. A wrapper that overrides only the final stage, such as
  ‹ownership_split_dg_spec_st_for› in ‹Ownership_Split_Exec›, relies on
  that: were the default to substitute the callee exit first, the wrapper would run against a
  continuation the caller never had. Changing the default is therefore an
  audit of every partial override, not a one-line edit.
›


definition local_dg_spec_template :: "('x,'k,'v,'D,'G) dg_spec" where
  "local_dg_spec_template = ⦇
     dgs_skip = local_transfer id,
     dgs_assign = (λx e. local_transfer id),
     dgs_special = (λsc x. local_transfer id),
     dgs_branch = (λb pol. local_transfer id),
     dgs_body = (λp. local_transfer id),
     dgs_return = (λe p. local_transfer id),
     dgs_enter = (λci. local_enter_transfer (λd. [(d, d)])),
     dgs_event = (λev. local_transfer id),
     dgs_combine_env = (λci. local_combine_transfer (λd de. d)),
     dgs_combine_assign = (λci. local_combine_transfer (λd de. d)),
     dgs_query = (λm q. sp_return ⊤) ⦈"

text ‹The argument-free template must generalize in generated ML. Expanding the
  local transfer makes its skip field a function value, avoiding the value restriction
  on the application ‹local_transfer id› while keeping the template itself named.›

lemmas [code] = local_dg_spec_template_def[unfolded local_transfer_def]

lemma local_dg_spec_template_simps [simp]:
  "skip⇧♯ local_dg_spec_template = local_transfer id"
  "assign⇧♯ local_dg_spec_template x e = local_transfer id"
  "special⇧♯ local_dg_spec_template sc x = local_transfer id"
  "branch⇧♯ local_dg_spec_template b pol = local_transfer id"
  "body⇧♯ local_dg_spec_template p = local_transfer id"
  "return⇧♯ local_dg_spec_template eo p = local_transfer id"
  "enter⇧♯ local_dg_spec_template ci = local_enter_transfer (λd. [(d, d)])"
  "event⇧♯ local_dg_spec_template ev = local_transfer id"
  "combine_env⇧♯ local_dg_spec_template ci = local_combine_transfer (λd de. d)"
  "combine_assign⇧♯ local_dg_spec_template ci = local_combine_transfer (λd de. d)"
  "dgs_query local_dg_spec_template m q = sp_return ⊤"
  by (simp_all add: local_dg_spec_template_def)

subsection ‹The pure edge dispatch›

text ‹
  ‹local_spec_step› is the pure counterpart of \<^const>‹dg_spec_step›'s
  dispatch: it selects the operation the edge names. A component's step on an
  arbitrary edge is this dispatch over its per-edge fields.
›

fun local_spec_step ::
  "('D ⇒ 'D) ⇒ (vname ⇒ exp ⇒ 'D ⇒ 'D) ⇒ (special_call ⇒ vname ⇒ 'D ⇒ 'D)
   ⇒ (exp ⇒ bool ⇒ 'D ⇒ 'D) ⇒ (pname ⇒ 'D ⇒ 'D)
   ⇒ (exp option ⇒ pname ⇒ 'D ⇒ 'D)
   ⇒ (analysis_event ⇒ 'D ⇒ 'D) ⇒ edge_action ⇒ 'D ⇒ 'D"
where
  "local_spec_step sk asn sp br bd rt ev EA_Nop = sk"
| "local_spec_step sk asn sp br bd rt ev (EA_Assign x e) = asn x e"
| "local_spec_step sk asn sp br bd rt ev (EA_Special sc x) = sp sc x"
| "local_spec_step sk asn sp br bd rt ev (EA_Assume b) = br b True"
| "local_spec_step sk asn sp br bd rt ev (EA_AssumeNot b) = br b False"
| "local_spec_step sk asn sp br bd rt ev (EA_Body p) = bd p"
| "local_spec_step sk asn sp br bd rt ev (EA_Ret e p) = rt e p"
| "local_spec_step sk asn sp br bd rt ev (EA_Check l cnd) = ev (Check_Event l cnd)"

fun event_action :: "analysis_event ⇒ edge_action" where
  "event_action (Check_Event l cnd) = EA_Check l cnd"

end