Theory MCP_Spec

theory MCP_Spec
  imports "Voblint_Framework.DG_Spec_Sound" "Voblint_Domain.Reachability_Lift"
begin

section ‹Many cooperating analyses over one state›

text ‹
  Goblint's ‹MCP› runs every activated analysis on its own part of one
  combined state (‹mCP.ml› at ‹0dc12d355›). Voblint keeps the combined state
  as one type ‹'s›, a record with a field per registered analysis, and a
  component as operations on the whole record that touch only its own field.
  The activation list chooses which components run; the fields of inactive
  analyses are never read.

  Every operation of a component receives the query channel of the manager
  Goblint hands it, ‹man.ask›, as a function \<^typ>‹channel› from queries to
  answers: its query handler (‹S.query man q›), its edge transfers, its entry
  (‹S.enter man›) and both stages of its return. The return stages also receive
  the callee's channel, which Goblint's normal-call transfer in ‹constraints.ml›
  passes as ‹f_ask›.
  A handler may therefore ask further queries while it answers, and the channel
  that answers them is the one ‹ask_rec› below closes over the combined
  state, as Goblint's ‹MCP.query'› does.

  The channel is a pure function of the state it describes. A component
  therefore neither reads nor publishes globals: the combined state covers
  analyses whose operations are local, and effectful analyses run as
  specifications of their own (\<^const>‹dgs_query› is the effectful handler).

  A component holds only what runs. What its states describe, a set of stores,
  is not executable and is supplied beside it wherever soundness is stated,
  as \<^class>‹numeric_domain› keeps ‹gamma› out of \<^class>‹executable_domain›.
›

record 's local_spec =
  ls_query :: "channel ⇒ 's ⇒ channel"
  ls_skip :: "channel ⇒ 's ⇒ 's"
  ls_assign :: "channel ⇒ vname ⇒ exp ⇒ 's ⇒ 's"
  ls_special :: "channel ⇒ special_call ⇒ vname ⇒ 's ⇒ 's"
  ls_branch :: "channel ⇒ exp ⇒ bool ⇒ 's ⇒ 's"
  ls_body :: "channel ⇒ pname ⇒ 's ⇒ 's"
  ls_return :: "channel ⇒ exp option ⇒ pname ⇒ 's ⇒ 's"
  ls_event :: "channel ⇒ analysis_event ⇒ 's ⇒ 's"
  ls_enter :: "channel ⇒ call_info ⇒ 's × 's ⇒ ('s × 's) list"
  ls_combine_env :: "channel ⇒ channel ⇒ call_info ⇒ 's ⇒ 's ⇒ 's"
  ls_combine_assign :: "channel ⇒ call_info ⇒ 's ⇒ 's ⇒ 's"

text ‹
  The edge transfers are separate fields, one per kind of edge, as Goblint's
  ‹Spec› has ‹skip›, ‹assign›, ‹special›, ‹branch›, ‹body›, ‹return› and
  ‹event›. A component that overrides one of them updates that field alone. The
  step on an arbitrary edge is derived from them.
›

definition ls_step :: "'s local_spec ⇒ channel ⇒ edge_action ⇒ 's ⇒ 's" where
  "ls_step c ch = local_spec_step (ls_skip c ch) (ls_assign c ch) (ls_special c ch)
     (ls_branch c ch) (ls_body c ch) (ls_return c ch) (ls_event c ch)"

lemma ls_step_simps [simp]:
  "ls_step c ch EA_Nop = ls_skip c ch"
  "ls_step c ch (EA_Assign x e) = ls_assign c ch x e"
  "ls_step c ch (EA_Special sc x) = ls_special c ch sc x"
  "ls_step c ch (EA_Assume b) = ls_branch c ch b True"
  "ls_step c ch (EA_AssumeNot b) = ls_branch c ch b False"
  "ls_step c ch (EA_Body p) = ls_body c ch p"
  "ls_step c ch (EA_Ret r p) = ls_return c ch r p"
  "ls_step c ch (EA_Check l cnd) = ls_event c ch (Check_Event l cnd)"
  by (simp_all add: ls_step_def)

lemma ls_step_event_action [simp]: "ls_step c ch (event_action e) = ls_event c ch e"
  by (cases e) simp

lemma ls_step_update_other [simp]:
  "ls_step (c⦇ls_query := h⦈) = ls_step c"
  "ls_step (c⦇ls_enter := e⦈) = ls_step c"
  "ls_step (c⦇ls_combine_env := ce⦈) = ls_step c"
  "ls_step (c⦇ls_combine_assign := ca⦈) = ls_step c"
  by (simp_all add: ls_step_def fun_eq_iff)

text ‹
  A component whose edge transfers are one function of the edge, such as a
  lens onto a field or a fold over several components, is built from that
  function: each field is the function at its kind of edge.
›

definition make_local_spec ::
  "(channel ⇒ 's ⇒ channel) ⇒ (channel ⇒ edge_action ⇒ 's ⇒ 's)
   ⇒ (channel ⇒ call_info ⇒ 's × 's ⇒ ('s × 's) list)
   ⇒ (channel ⇒ channel ⇒ call_info ⇒ 's ⇒ 's ⇒ 's)
   ⇒ (channel ⇒ call_info ⇒ 's ⇒ 's ⇒ 's) ⇒ 's local_spec" where
  "make_local_spec qry st en ce ca = ⦇
     ls_query = qry,
     ls_skip = (λch. st ch EA_Nop),
     ls_assign = (λch x e. st ch (EA_Assign x e)),
     ls_special = (λch sc x. st ch (EA_Special sc x)),
     ls_branch = (λch b pol. st ch (if pol then EA_Assume b else EA_AssumeNot b)),
     ls_body = (λch p. st ch (EA_Body p)),
     ls_return = (λch r p. st ch (EA_Ret r p)),
     ls_event = (λch ev. st ch (event_action ev)),
     ls_enter = en, ls_combine_env = ce, ls_combine_assign = ca ⦈"

lemma make_local_spec_sel [simp]:
  "ls_query (make_local_spec qry st en ce ca) = qry"
  "ls_step (make_local_spec qry st en ce ca) = st"
  "ls_enter (make_local_spec qry st en ce ca) = en"
  "ls_combine_env (make_local_spec qry st en ce ca) = ce"
  "ls_combine_assign (make_local_spec qry st en ce ca) = ca"
proof -
  have "ls_step (make_local_spec qry st en ce ca) ch a = st ch a" for ch a
  proof (cases a)
    case (EA_Check l cnd)
    then show ?thesis by (simp add: make_local_spec_def ls_step_def)
  qed (simp_all add: make_local_spec_def ls_step_def)
  then show "ls_step (make_local_spec qry st en ce ca) = st" by (simp add: fun_eq_iff)
qed (simp_all add: make_local_spec_def)

text ‹
  The return runs in the two stages of Goblint's ‹combine_env› and
  ‹combine_assign›, which both receive the callee's channel. Only the first
  receives the caller's: Goblint's ‹combine_assign› asks about the state
  ‹combine_env› produced, which describes no concrete store on its own here,
  since soundness and independence speak only about the composite.
›

abbreviation ls_combine ::
  "'s local_spec ⇒ channel ⇒ channel ⇒ call_info ⇒ 's ⇒ 's ⇒ 's" where
  "ls_combine c ch ch' ci x de ≡ ls_combine_assign c ch' ci (ls_combine_env c ch ch' ci x de) de"

text ‹
  A local specification is sound for a concretization ‹gamma› when each operation covers the
  concrete behaviour, whatever the other fields of the record hold. Every
  operation is proved against every channel that holds at the stores it is
  asked about, so its proof cannot depend on who answers: the caller's store for a
  step, an entry, a query and the first stage of a return, and the callee's exit
  store for the callee's channel.
›

definition sound_local_spec ::
  "(vname ⇒ bool) ⇒ ('s::order ⇒ store set) ⇒ 's local_spec ⇒ bool" where
  "sound_local_spec 𝒢 gm c ⟷
     (∀x y. x ≤ y ⟶ gm x ⊆ gm y)
     ∧ (∀ch a x. edge_collect a (gm x ∩ Collect (eval_query.channel_holds ch))
                  ⊆ gm (ls_step c ch a x))
     ∧ (∀ch s ci p. s ∈ gm (fst p) ⟶ eval_query.channel_holds ch s ⟶
          (∃q ∈ set (ls_enter c ch ci p). s ∈ gm (fst q)
             ∧ call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s
                 ∈ gm (snd q)))
     ∧ (∀ch ch' s t ci x de. s ∈ gm x ⟶ eval_query.channel_holds ch s ⟶
          t ∈ gm de ⟶ eval_query.channel_holds ch' t ⟶
          combine_collect 𝒢 (ci_dst ci) s t ∈ gm (ls_combine c ch ch' ci x de))
     ∧ (∀ch s x q. s ∈ gm x ⟶ eval_query.channel_holds ch s ⟶
          eval_holds q (ls_query c ch x q) s)"

text ‹
  The step obligation splits into one law per kind of edge, each about the
  field that handles it: the store the edge produces lies in what the field
  returns, for every store and channel that hold before. A component proves the
  laws of the fields it defines, and a field it replaces needs only its own law
  again (‹sound_local_spec_update›).
›

definition sound_skip :: "('s ⇒ store set) ⇒ (channel ⇒ 's ⇒ 's) ⇒ bool" where
  "sound_skip gm f ⟷
     (∀ch x s. s ∈ gm x ⟶ eval_query.channel_holds ch s ⟶ s ∈ gm (f ch x))"

definition sound_assign ::
  "('s ⇒ store set) ⇒ (channel ⇒ vname ⇒ exp ⇒ 's ⇒ 's) ⇒ bool" where
  "sound_assign gm f ⟷
     (∀ch x s y e. s ∈ gm x ⟶ eval_query.channel_holds ch s ⟶ s(y := ⟦e⟧⇩e s) ∈ gm (f ch y e x))"

definition sound_special ::
  "('s ⇒ store set) ⇒ (channel ⇒ special_call ⇒ vname ⇒ 's ⇒ 's) ⇒ bool" where
  "sound_special gm f ⟷
     (∀ch x s sc y t. s ∈ gm x ⟶ eval_query.channel_holds ch s ⟶ t ∈ special_step sc y s
        ⟶ t ∈ gm (f ch sc y x))"

definition sound_branch :: "('s ⇒ store set) ⇒ (channel ⇒ exp ⇒ bool ⇒ 's ⇒ 's) ⇒ bool" where
  "sound_branch gm f ⟷
     (∀ch x s b pol. s ∈ gm x ⟶ eval_query.channel_holds ch s ⟶ truthy (⟦b⟧⇩e s) = pol
        ⟶ s ∈ gm (f ch b pol x))"

definition sound_body :: "('s ⇒ store set) ⇒ (channel ⇒ pname ⇒ 's ⇒ 's) ⇒ bool" where
  "sound_body gm f ⟷
     (∀ch x s p. s ∈ gm x ⟶ eval_query.channel_holds ch s ⟶ s ∈ gm (f ch p x))"

definition sound_return ::
  "('s ⇒ store set) ⇒ (channel ⇒ exp option ⇒ pname ⇒ 's ⇒ 's) ⇒ bool" where
  "sound_return gm f ⟷
     (∀ch x s r p. s ∈ gm x ⟶ eval_query.channel_holds ch s
        ⟶ s(ret_var := (case r of None ⇒ s ret_var | Some a ⇒ ⟦a⟧⇩e s)) ∈ gm (f ch r p x))"

definition sound_event :: "('s ⇒ store set) ⇒ (channel ⇒ analysis_event ⇒ 's ⇒ 's) ⇒ bool" where
  "sound_event gm f ⟷
     (∀ch x s ev. s ∈ gm x ⟶ eval_query.channel_holds ch s ⟶ s ∈ gm (f ch ev x))"

text ‹
  The laws of the other fields. The handler's answers hold at every store its
  state describes. An entry covers the caller's store and the store the call
  enters by one of its pairs. The two return stages carry one law together,
  because only their composition describes a concrete store.
›

definition sound_query :: "('s ⇒ store set) ⇒ (channel ⇒ 's ⇒ channel) ⇒ bool" where
  "sound_query gm h ⟷
     (∀ch s x q. s ∈ gm x ⟶ eval_query.channel_holds ch s ⟶ eval_holds q (h ch x q) s)"

definition sound_enter ::
  "(vname ⇒ bool) ⇒ ('s ⇒ store set)
   ⇒ (channel ⇒ call_info ⇒ 's × 's ⇒ ('s × 's) list) ⇒ bool" where
  "sound_enter 𝒢 gm en ⟷
     (∀ch s ci p. s ∈ gm (fst p) ⟶ eval_query.channel_holds ch s ⟶
        (∃q ∈ set (en ch ci p). s ∈ gm (fst q)
           ∧ call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s ∈ gm (snd q)))"

definition sound_combine ::
  "(vname ⇒ bool) ⇒ ('s ⇒ store set)
   ⇒ (channel ⇒ channel ⇒ call_info ⇒ 's ⇒ 's ⇒ 's)
   ⇒ (channel ⇒ call_info ⇒ 's ⇒ 's ⇒ 's) ⇒ bool" where
  "sound_combine 𝒢 gm ce ca ⟷
     (∀ch ch' s t ci x de. s ∈ gm x ⟶ eval_query.channel_holds ch s ⟶
        t ∈ gm de ⟶ eval_query.channel_holds ch' t ⟶
        combine_collect 𝒢 (ci_dst ci) s t ∈ gm (ca ch' ci (ce ch ch' ci x de) de))"

theorem ls_step_sound_iff:
  "(∀ch a x. edge_collect a (gm x ∩ Collect (eval_query.channel_holds ch)) ⊆ gm (ls_step c ch a x))
   ⟷ sound_skip gm (ls_skip c) ∧ sound_assign gm (ls_assign c) ∧ sound_special gm (ls_special c)
     ∧ sound_branch gm (ls_branch c) ∧ sound_body gm (ls_body c)
     ∧ sound_return gm (ls_return c) ∧ sound_event gm (ls_event c)"
  (is "?step ⟷ ?fields")
proof
  assume step: ?step
  have at: "t ∈ gm (ls_step c ch a x)"
    if "s ∈ gm x" "eval_query.channel_holds ch s" "t ∈ edge_step a s" for ch a x s t
    using step that unfolding edge_collect_def by blast
  have pol: "s ∈ gm (ls_branch c ch b pol x)"
    if "s ∈ gm x" "eval_query.channel_holds ch s" "truthy (⟦b⟧⇩e s) = pol" for ch b pol x s
  proof (cases pol)
    case True
    then show ?thesis
      using at[OF that(1,2), where a = "EA_Assume b" and t = s] that(3) by simp
  next
    case False
    then show ?thesis
      using at[OF that(1,2), where a = "EA_AssumeNot b" and t = s] that(3) by simp
  qed
  have ev: "s ∈ gm (ls_event c ch ev x)"
    if "s ∈ gm x" "eval_query.channel_holds ch s" for ch ev x s
  proof (cases ev)
    case (Check_Event l e)
    then show ?thesis using at[OF that, where a = "EA_Check l e" and t = s] by simp
  qed
  have special: "t ∈ gm (ls_special c ch sc y x)"
    if "s ∈ gm x" "eval_query.channel_holds ch s" "t ∈ special_step sc y s" for ch x s sc y t
    using at[OF that(1,2), where a = "EA_Special sc y" and t = t] that(3)
    by (simp only: edge_step.simps ls_step_simps)
  show ?fields
    unfolding sound_skip_def sound_assign_def sound_special_def sound_branch_def sound_body_def
      sound_return_def sound_event_def
    using at[where a = EA_Nop] at[where a = "EA_Assign _ _"]
      at[where a = "EA_Body _"] at[where a = "EA_Ret _ _"] pol ev special
    by (fastforce+)
next
  assume F: ?fields
  show ?step
  proof (intro allI subsetI)
    fix ch a x t
    assume "t ∈ edge_collect a (gm x ∩ Collect (eval_query.channel_holds ch))"
    then obtain s where s: "s ∈ gm x" "eval_query.channel_holds ch s" "t ∈ edge_step a s"
      unfolding edge_collect_def by blast
    show "t ∈ gm (ls_step c ch a x)"
    proof (cases a)
      case (EA_Special sc y)
      have "t ∈ special_step sc y s" using s(3) EA_Special by (simp only: edge_step.simps)
      then show ?thesis
        using F s(1,2) EA_Special unfolding sound_special_def by (simp only: ls_step_simps)
    next
      case (EA_Assume b)
      then have "t = s" "truthy (⟦b⟧⇩e s) = True" using s(3) by (simp_all split: if_splits)
      then show ?thesis
        using F s(1,2) EA_Assume unfolding sound_branch_def by (simp only: ls_step_simps)
    next
      case (EA_AssumeNot b)
      then have "t = s" "truthy (⟦b⟧⇩e s) = False" using s(3) by (simp_all split: if_splits)
      then show ?thesis
        using F s(1,2) EA_AssumeNot unfolding sound_branch_def by (simp only: ls_step_simps)
    qed (use F s in ‹auto simp: sound_skip_def sound_assign_def sound_body_def sound_return_def
                     sound_event_def›)
  qed
qed

text ‹
  The certificate is exactly the conjunction of a monotone concretization and
  one law per field, the two return stages sharing one law. A local
  specification is therefore built, taken apart and changed field by field.
›

theorem sound_local_spec_iff:
  "sound_local_spec 𝒢 gm c ⟷
     (∀x y. x ≤ y ⟶ gm x ⊆ gm y)
     ∧ sound_query gm (ls_query c)
     ∧ sound_skip gm (ls_skip c) ∧ sound_assign gm (ls_assign c)
     ∧ sound_special gm (ls_special c) ∧ sound_branch gm (ls_branch c)
     ∧ sound_body gm (ls_body c) ∧ sound_return gm (ls_return c)
     ∧ sound_event gm (ls_event c)
     ∧ sound_enter 𝒢 gm (ls_enter c)
     ∧ sound_combine 𝒢 gm (ls_combine_env c) (ls_combine_assign c)"
  unfolding sound_local_spec_def ls_step_sound_iff sound_query_def sound_enter_def
    sound_combine_def
  by (intro iffI; elim conjE; intro conjI; assumption)

lemma sound_local_specI:
  assumes "⋀x y. x ≤ y ⟹ gm x ⊆ gm y"
    and "sound_query gm (ls_query c)"
    and "sound_skip gm (ls_skip c)" and "sound_assign gm (ls_assign c)"
    and "sound_special gm (ls_special c)" and "sound_branch gm (ls_branch c)"
    and "sound_body gm (ls_body c)" and "sound_return gm (ls_return c)"
    and "sound_event gm (ls_event c)"
    and "sound_enter 𝒢 gm (ls_enter c)"
    and "sound_combine 𝒢 gm (ls_combine_env c) (ls_combine_assign c)"
  shows "sound_local_spec 𝒢 gm c"
  using assms unfolding sound_local_spec_iff by blast

lemma sound_local_specD:
  assumes "sound_local_spec 𝒢 gm c"
  shows sound_local_spec_monoD: "x ≤ y ⟹ gm x ⊆ gm y"
    and sound_local_spec_queryD: "sound_query gm (ls_query c)"
    and sound_local_spec_skipD: "sound_skip gm (ls_skip c)"
    and sound_local_spec_assignD: "sound_assign gm (ls_assign c)"
    and sound_local_spec_specialD: "sound_special gm (ls_special c)"
    and sound_local_spec_branchD: "sound_branch gm (ls_branch c)"
    and sound_local_spec_bodyD: "sound_body gm (ls_body c)"
    and sound_local_spec_returnD: "sound_return gm (ls_return c)"
    and sound_local_spec_eventD: "sound_event gm (ls_event c)"
    and sound_local_spec_enterD: "sound_enter 𝒢 gm (ls_enter c)"
    and sound_local_spec_combineD:
      "sound_combine 𝒢 gm (ls_combine_env c) (ls_combine_assign c)"
  using assms unfolding sound_local_spec_iff by blast+

text ‹
  A sound local specification stays sound when one field is replaced by one
  satisfying that field's law. A return stage is replaced together with the law
  of the composed return it forms with the other stage.
›

lemma sound_local_spec_update:
  assumes "sound_local_spec 𝒢 gm c"
  shows sound_local_spec_update_query:
      "sound_query gm h ⟹ sound_local_spec 𝒢 gm (c⦇ls_query := h⦈)"
    and sound_local_spec_update_skip:
      "sound_skip gm sk ⟹ sound_local_spec 𝒢 gm (c⦇ls_skip := sk⦈)"
    and sound_local_spec_update_assign:
      "sound_assign gm asn ⟹ sound_local_spec 𝒢 gm (c⦇ls_assign := asn⦈)"
    and sound_local_spec_update_special:
      "sound_special gm sp ⟹ sound_local_spec 𝒢 gm (c⦇ls_special := sp⦈)"
    and sound_local_spec_update_branch:
      "sound_branch gm br ⟹ sound_local_spec 𝒢 gm (c⦇ls_branch := br⦈)"
    and sound_local_spec_update_body:
      "sound_body gm bd ⟹ sound_local_spec 𝒢 gm (c⦇ls_body := bd⦈)"
    and sound_local_spec_update_return:
      "sound_return gm rt ⟹ sound_local_spec 𝒢 gm (c⦇ls_return := rt⦈)"
    and sound_local_spec_update_event:
      "sound_event gm ev ⟹ sound_local_spec 𝒢 gm (c⦇ls_event := ev⦈)"
    and sound_local_spec_update_enter:
      "sound_enter 𝒢 gm en ⟹ sound_local_spec 𝒢 gm (c⦇ls_enter := en⦈)"
    and sound_local_spec_update_combine_env:
      "sound_combine 𝒢 gm ce (ls_combine_assign c)
       ⟹ sound_local_spec 𝒢 gm (c⦇ls_combine_env := ce⦈)"
    and sound_local_spec_update_combine_assign:
      "sound_combine 𝒢 gm (ls_combine_env c) ca
       ⟹ sound_local_spec 𝒢 gm (c⦇ls_combine_assign := ca⦈)"
  using assms unfolding sound_local_spec_iff by simp_all

subsection ‹Conservative defaults›

text ‹
  A field whose concrete counterpart leaves the store unchanged has a default
  that decides nothing: the handler answers ‹⊤›, and skip, body, event and
  branch keep the state. Each is sound for every concretization. Assign,
  special, return, entry and the second return stage change the store or the
  frame, so no default is sound for every concretization and an analysis
  supplies them. The first return stage defaults to the caller's state; it has
  no law of its own, only the composed return does.
›

definition query_unknown :: "channel ⇒ 's ⇒ channel" where
  "query_unknown ch x = ⊤"

definition skip_identity :: "channel ⇒ 's ⇒ 's" where
  "skip_identity ch x = x"

definition body_identity :: "channel ⇒ pname ⇒ 's ⇒ 's" where
  "body_identity ch p x = x"

definition event_identity :: "channel ⇒ analysis_event ⇒ 's ⇒ 's" where
  "event_identity ch ev x = x"

definition branch_identity :: "channel ⇒ exp ⇒ bool ⇒ 's ⇒ 's" where
  "branch_identity ch b pol x = x"

definition combine_env_identity :: "channel ⇒ channel ⇒ call_info ⇒ 's ⇒ 's ⇒ 's" where
  "combine_env_identity ch ch' ci x de = x"

lemma sound_query_unknown: "sound_query gm query_unknown"
  by (simp add: sound_query_def query_unknown_def)

lemma sound_skip_identity: "sound_skip gm skip_identity"
  by (simp add: sound_skip_def skip_identity_def)

lemma sound_body_identity: "sound_body gm body_identity"
  by (simp add: sound_body_def body_identity_def)

lemma sound_event_identity: "sound_event gm event_identity"
  by (simp add: sound_event_def event_identity_def)

lemma sound_branch_identity: "sound_branch gm branch_identity"
  by (simp add: sound_branch_def branch_identity_def)

lemma sound_combine_env_identity:
  "sound_combine 𝒢 gm combine_env_identity ca ⟷
     (∀ch' s t ci x de. s ∈ gm x ⟶ t ∈ gm de ⟶ eval_query.channel_holds ch' t ⟶
        combine_collect 𝒢 (ci_dst ci) s t ∈ gm (ca ch' ci x de))"
  unfolding sound_combine_def combine_env_identity_def
  using eval_query.channel_holds_top by blast

text ‹
  A local specification that supplies only the five operations without a
  default. An analysis starts from it and overrides the fields it decides more
  precisely; each override needs only its own law again
  (‹sound_local_spec_update›).
›

definition conservative_local_spec ::
  "(channel ⇒ vname ⇒ exp ⇒ 's ⇒ 's)
   ⇒ (channel ⇒ special_call ⇒ vname ⇒ 's ⇒ 's)
   ⇒ (channel ⇒ exp option ⇒ pname ⇒ 's ⇒ 's)
   ⇒ (channel ⇒ call_info ⇒ 's × 's ⇒ ('s × 's) list)
   ⇒ (channel ⇒ call_info ⇒ 's ⇒ 's ⇒ 's) ⇒ 's local_spec" where
  "conservative_local_spec asn sp rt en ca = ⦇
     ls_query = query_unknown, ls_skip = skip_identity, ls_assign = asn,
     ls_special = sp, ls_branch = branch_identity, ls_body = body_identity,
     ls_return = rt, ls_event = event_identity, ls_enter = en,
     ls_combine_env = combine_env_identity, ls_combine_assign = ca ⦈"

theorem sound_conservative_local_spec:
  assumes "⋀x y. x ≤ y ⟹ gm x ⊆ gm y"
    and "sound_assign gm asn" and "sound_special gm sp" and "sound_return gm rt"
    and "sound_enter 𝒢 gm en" and "sound_combine 𝒢 gm combine_env_identity ca"
  shows "sound_local_spec 𝒢 gm (conservative_local_spec asn sp rt en ca)"
  by (rule sound_local_specI)
     (simp_all add: conservative_local_spec_def assms sound_query_unknown sound_skip_identity
        sound_body_identity sound_event_identity sound_branch_identity)
text ‹
  A component leaves a concretization alone when none of its operations
  changes what that concretization says. For components that each own one
  field of a record this is the lens law that updating one field leaves the
  others.
›

definition mcp_frame :: "'s local_spec ⇒ ('s ⇒ store set) ⇒ bool" where
  "mcp_frame c gm ⟷
     (∀ch a x. gm (ls_step c ch a x) = gm x)
     ∧ (∀ch ci p q. q ∈ set (ls_enter c ch ci p) ⟶
          gm (fst q) = gm (fst p) ∧ gm (snd q) = gm (snd p))
     ∧ (∀ch ch' ci x de. gm (ls_combine c ch ch' ci x de) = gm x)"

text ‹
  Cooperating analyses come as pairs of a concretization and a component.
  They are independent when each leaves the others' concretizations alone.
›

type_synonym 's certified_component = "('s ⇒ store set) × 's local_spec"

fun mcp_independent :: "'s certified_component list ⇒ bool" where
  "mcp_independent [] ⟷ True"
| "mcp_independent ((g, c) # gcs) ⟷
     (∀(g', c') ∈ set gcs. mcp_frame c g' ∧ mcp_frame c' g) ∧ mcp_independent gcs"

section ‹The query channel›

text ‹
  A handler answers a query given the channel through which it may ask further
  ones. ‹ask_rec› closes that recursion over one state, as Goblint's
  ‹MCP.query'› does: a query already being asked answers ‹⊤› instead of
  recursing, and every other query is answered by the handler under a channel
  that remembers it. The depth bound plays the role it plays in
  \<^const>‹ask_with›: queries range over an infinite type, so cycle detection
  alone does not make the recursion total, and exhausting the bound aborts the
  generated program. Logically the fallback is ‹⊤›, so the bound plays no part
  in soundness. Goblint also caches answers per transfer; that changes only how
  often a handler runs.
›

fun ask_rec :: "(channel ⇒ 's ⇒ channel) ⇒ nat ⇒ query set ⇒ 's ⇒ channel" where
  "ask_rec H 0 asked x q =
     Code.abort (STR ''query recursion exceeded query_depth'') (λ_. ⊤)"
| "ask_rec H (Suc n) asked x q =
     (if q ∈ asked then ⊤ else H (ask_rec H n (insert q asked) x) x q)"

text ‹
  A handler that answers soundly under every sound channel makes the closed
  channel sound: by induction on the depth, each level's channel holds, so the
  handler's answer under it holds.
›

lemma ask_rec_sound:
  assumes "⋀ch q. eval_query.channel_holds ch s ⟹ eval_holds q (H ch x q) s"
  shows "eval_query.channel_holds (ask_rec H n asked x) s"
proof (induction n arbitrary: asked)
  case 0
  then show ?case by (simp add: eval_query.channel_holds_def)
next
  case (Suc n)
  then show ?case
    using assms by (auto simp: eval_query.channel_holds_def)
qed

definition ls_channel :: "'s local_spec ⇒ 's ⇒ channel" where
  "ls_channel c x = ask_rec (ls_query c) query_depth {} x"

lemma ls_channel_sound:
  assumes "sound_local_spec 𝒢 γ⇩c c" and "s ∈ γ⇩c x"
  shows "eval_query.channel_holds (ls_channel c x) s"
  unfolding ls_channel_def
  by (rule ask_rec_sound) (use assms in ‹simp add: sound_local_spec_def›)

lemma ls_channel_const: "ls_query c = (λch x. h x) ⟹ ls_channel c = h"
  by (simp add: ls_channel_def query_depth_def fun_eq_iff eval_nat_numeral)

section ‹The combined operations›

text ‹
  The combined operations run the active components in turn. Soundness needs
  only \<^const>‹mcp_frame›: a component keeps what the other components'
  states describe, not their representation, so the soundness proof says
  nothing about the order of the fold. A component that updates only its own
  field of a product does leave the other fields unchanged, and for those the
  order does not matter; Goblint runs every component on the predecessor's
  part of the state, which is the same computation. Every component gets the
  same channel, as every Goblint component gets the same ‹man.ask›.
›

definition mcp_step :: "'s local_spec list ⇒ channel ⇒ edge_action ⇒ 's ⇒ 's" where
  "mcp_step cs ch a x = fold (λc y. ls_step c ch a y) cs x"

definition mcp_en_from ::
  "'s local_spec list ⇒ channel ⇒ call_info ⇒ 's × 's ⇒ 's enter_result list" where
  "mcp_en_from cs ch ci p = fold (λc ps. concat (map (ls_enter c ch ci) ps)) cs [p]"

definition mcp_comb ::
  "'s local_spec list ⇒ channel ⇒ channel ⇒ call_info ⇒ 's ⇒ 's ⇒ 's" where
  "mcp_comb cs ch ch' ci x de = fold (λc y. ls_combine c ch ch' ci y de) cs x"

text ‹
  The combined handler meets every component's answer, each given the same
  channel, as ‹MCP.query'› meets the results of all analyses.
›

definition mcp_qry :: "'s local_spec list ⇒ channel ⇒ 's ⇒ channel" where
  "mcp_qry cs ch x q = fold (λc r. r ⊓ ls_query c ch x q) cs ⊤"

definition mcp_gamma :: "('s ⇒ store set) list ⇒ 's ⇒ store set" where
  "mcp_gamma Γ x = (⋂γ⇩i ∈ set Γ. γ⇩i x)"

section ‹Soundness of the combination›

text ‹
  The combined state is sound for the intersection ‹mcp_gamma› of the
  components' concretizations. Step, combine, entry and query folds each stay
  sound because a component leaves the others' concretizations unchanged.
›

lemma mcp_gamma_Cons [simp]: "mcp_gamma (g # gs) x = g x ∩ mcp_gamma gs x"
  by (simp add: mcp_gamma_def)

lemma mcp_gamma_Nil [simp]: "mcp_gamma [] x = UNIV"
  by (simp add: mcp_gamma_def)

text ‹Components a fold runs leave an independent concretization as it was.›

lemma gamma_fold_step:
  "(∀c ∈ set cs. mcp_frame c g) ⟹ g (fold (λc y. ls_step c ch a y) cs x) = g x"
  by (induction cs arbitrary: x) (simp_all add: mcp_frame_def)

lemma gamma_fold_comb:
  "(∀c ∈ set cs. mcp_frame c g) ⟹ g (fold (λc y. ls_combine c ch ch' ci y de) cs x) = g x"
  by (induction cs arbitrary: x) (simp_all add: mcp_frame_def)

lemma mcp_gamma_frame:
  "(∀g ∈ set gs. mcp_frame c g) ⟹ mcp_gamma gs (ls_step c ch a x) = mcp_gamma gs x"
  "(∀g ∈ set gs. mcp_frame c g) ⟹ mcp_gamma gs (ls_combine c ch ch' ci x de) = mcp_gamma gs x"
  by (auto simp: mcp_gamma_def mcp_frame_def intro!: INF_cong)

lemma mcp_independent_Cons_frames:
  assumes "mcp_independent ((g, c) # gcs)"
  shows "∀g' ∈ fst ` set gcs. mcp_frame c g'" "∀c' ∈ snd ` set gcs. mcp_frame c' g"
    "mcp_independent gcs"
  using assms by auto

lemma mcp_step_sound:
  assumes "∀(g, c) ∈ set gcs. sound_local_spec 𝒢 g c" and "mcp_independent gcs"
  shows "edge_collect a (mcp_gamma (map fst gcs) x ∩ Collect (eval_query.channel_holds ch))
           ⊆ mcp_gamma (map fst gcs) (mcp_step (map snd gcs) ch a x)"
  using assms
proof (induction gcs arbitrary: x)
  case Nil
  then show ?case by (simp add: mcp_step_def)
next
  case (Cons gc gcs)
  obtain g c where gc: "gc = (g, c)" by fastforce
  let ?O = "Collect (eval_query.channel_holds ch)"
  let ?x1 = "ls_step c ch a x"
  have frames: "∀g' ∈ fst ` set gcs. mcp_frame c g'" "∀c' ∈ snd ` set gcs. mcp_frame c' g"
    "mcp_independent gcs"
    using mcp_independent_Cons_frames[OF Cons.prems(2)[unfolded gc]] by simp_all
  have own: "edge_collect a (g x ∩ ?O) ⊆ g ?x1"
    using Cons.prems(1) unfolding gc by (simp add: sound_local_spec_def)
  have own_kept: "g (mcp_step (map snd gcs) ch a ?x1) = g ?x1"
    unfolding mcp_step_def by (rule gamma_fold_step) (use frames in auto)
  have rest: "edge_collect a (mcp_gamma (map fst gcs) ?x1 ∩ ?O)
      ⊆ mcp_gamma (map fst gcs) (mcp_step (map snd gcs) ch a ?x1)"
    by (rule Cons.IH) (use Cons.prems(1) frames in auto)
  have rest_eq: "mcp_gamma (map fst gcs) ?x1 = mcp_gamma (map fst gcs) x"
    by (rule mcp_gamma_frame(1)) (use frames in auto)
  have "edge_collect a (mcp_gamma (map fst (gc # gcs)) x ∩ ?O)
          ⊆ edge_collect a (g x ∩ ?O) ∩ edge_collect a (mcp_gamma (map fst gcs) ?x1 ∩ ?O)"
    unfolding gc by (intro Int_greatest edge_collect_mono) (auto simp: rest_eq)
  also have "… ⊆ mcp_gamma (map fst (gc # gcs)) (mcp_step (map snd (gc # gcs)) ch a x)"
    using own own_kept rest unfolding gc by (auto simp: mcp_step_def)
  finally show ?case .
qed

lemma mcp_comb_sound:
  assumes "∀(g, c) ∈ set gcs. sound_local_spec 𝒢 g c" and "mcp_independent gcs"
    and "s ∈ mcp_gamma (map fst gcs) x" and "eval_query.channel_holds ch s"
    and "t ∈ mcp_gamma (map fst gcs) de" and "eval_query.channel_holds ch' t"
  shows "combine_collect 𝒢 (ci_dst ci) s t
           ∈ mcp_gamma (map fst gcs) (mcp_comb (map snd gcs) ch ch' ci x de)"
  using assms
proof (induction gcs arbitrary: x)
  case Nil
  then show ?case by simp
next
  case (Cons gc gcs)
  obtain g c where gc: "gc = (g, c)" by fastforce
  let ?x1 = "ls_combine c ch ch' ci x de"
  have frames: "∀g' ∈ fst ` set gcs. mcp_frame c g'" "∀c' ∈ snd ` set gcs. mcp_frame c' g"
    "mcp_independent gcs"
    using mcp_independent_Cons_frames[OF Cons.prems(2)[unfolded gc]] by simp_all
  have own: "combine_collect 𝒢 (ci_dst ci) s t ∈ g ?x1"
    using Cons.prems(1,3-6) unfolding gc by (simp add: sound_local_spec_def)
  have own_kept: "g (mcp_comb (map snd gcs) ch ch' ci ?x1 de) = g ?x1"
    unfolding mcp_comb_def by (rule gamma_fold_comb) (use frames in auto)
  have rest_eq: "mcp_gamma (map fst gcs) ?x1 = mcp_gamma (map fst gcs) x"
    by (rule mcp_gamma_frame(2)) (use frames in auto)
  have rest: "combine_collect 𝒢 (ci_dst ci) s t
      ∈ mcp_gamma (map fst gcs) (mcp_comb (map snd gcs) ch ch' ci ?x1 de)"
    by (rule Cons.IH) (use Cons.prems frames rest_eq gc in auto)
  show ?case
    using own own_kept rest unfolding gc by (simp add: mcp_comb_def)
qed

text ‹
  Entry threads a list of pairs through the components. The invariant carries
  the concretizations of the components already run (‹ds›), whose fields are
  set in both halves, and the components still to run (‹gcs›), whose fields
  are still the caller's.
›

lemma mcp_en_fold_sound:
  assumes "∀(g, c) ∈ set gcs. sound_local_spec 𝒢 g c" and "mcp_independent gcs"
    and "∀c ∈ snd ` set gcs. ∀d ∈ set ds. mcp_frame c d"
    and "∃p ∈ set ps. s ∈ mcp_gamma (map fst gcs) (fst p) ∧ s ∈ mcp_gamma ds (fst p)
                       ∧ E ∈ mcp_gamma ds (snd p)"
    and A: "eval_query.channel_holds ch s"
    and E: "E = call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s"
  shows "∃p ∈ set (fold (λc ps. concat (map (ls_enter c ch ci) ps)) (map snd gcs) ps).
           s ∈ mcp_gamma (map fst gcs) (fst p) ∧ s ∈ mcp_gamma ds (fst p)
           ∧ E ∈ mcp_gamma (map fst gcs) (snd p) ∧ E ∈ mcp_gamma ds (snd p)"
  using assms(1-4)
proof (induction gcs arbitrary: ps ds)
  case Nil
  then show ?case by simp
next
  case (Cons gc gcs)
  obtain g c where gc: "gc = (g, c)" by fastforce
  have frames: "∀g' ∈ fst ` set gcs. mcp_frame c g'" "∀c' ∈ snd ` set gcs. mcp_frame c' g"
    "mcp_independent gcs"
    using mcp_independent_Cons_frames[OF Cons.prems(2)[unfolded gc]] by simp_all
  obtain p where p: "p ∈ set ps" "s ∈ g (fst p)" "s ∈ mcp_gamma (map fst gcs) (fst p)"
      "s ∈ mcp_gamma ds (fst p)" "E ∈ mcp_gamma ds (snd p)"
    using Cons.prems(4) unfolding gc by auto
  have "sound_local_spec 𝒢 g c" using Cons.prems(1) unfolding gc by simp
  then obtain q where q: "q ∈ set (ls_enter c ch ci p)" "s ∈ g (fst q)" "E ∈ g (snd q)"
    using p(2) A unfolding E sound_local_spec_def by meson
  have keep: "d (fst q) = d (fst p) ∧ d (snd q) = d (snd p)"
    if "d ∈ fst ` set gcs ∪ set ds" for d
  proof -
    have "mcp_frame c d" using that frames(1) Cons.prems(3) unfolding gc by auto
    then show ?thesis using q(1) unfolding mcp_frame_def by blast
  qed
  have q_in: "q ∈ set (concat (map (ls_enter c ch ci) ps))"
    using p(1) q(1) by auto
  have "∃p ∈ set (fold (λc ps. concat (map (ls_enter c ch ci) ps)) (map snd gcs)
                 (concat (map (ls_enter c ch ci) ps))).
          s ∈ mcp_gamma (map fst gcs) (fst p) ∧ s ∈ mcp_gamma (g # ds) (fst p)
          ∧ E ∈ mcp_gamma (map fst gcs) (snd p) ∧ E ∈ mcp_gamma (g # ds) (snd p)"
  proof (rule Cons.IH)
    show "∀(g, c) ∈ set gcs. sound_local_spec 𝒢 g c" using Cons.prems(1) by simp
    show "mcp_independent gcs" by (fact frames(3))
    show "∀c' ∈ snd ` set gcs. ∀d ∈ set (g # ds). mcp_frame c' d"
      using frames(2) Cons.prems(3) unfolding gc by auto
    show "∃p ∈ set (concat (map (ls_enter c ch ci) ps)).
            s ∈ mcp_gamma (map fst gcs) (fst p) ∧ s ∈ mcp_gamma (g # ds) (fst p)
            ∧ E ∈ mcp_gamma (g # ds) (snd p)"
    proof (rule bexI[OF _ q_in])
      show "s ∈ mcp_gamma (map fst gcs) (fst q) ∧ s ∈ mcp_gamma (g # ds) (fst q)
              ∧ E ∈ mcp_gamma (g # ds) (snd q)"
      proof -
        have "mcp_gamma (map fst gcs) (fst q) = mcp_gamma (map fst gcs) (fst p)"
            "mcp_gamma ds (fst q) = mcp_gamma ds (fst p)"
            "mcp_gamma ds (snd q) = mcp_gamma ds (snd p)"
          using keep by (auto simp: mcp_gamma_def intro!: INF_cong)
        then show ?thesis using p(3-5) q(2,3) by simp
      qed
    qed
  qed
  then show ?case unfolding gc by (auto simp: mcp_gamma_def)
qed

lemma mcp_qry_fold_sound:
  "s ∈ mcp_gamma (map fst gcs) x ⟹ eval_query.channel_holds ch s
   ⟹ ∀(g, c) ∈ set gcs. sound_local_spec 𝒢 g c
   ⟹ eval_holds q r s
   ⟹ eval_holds q (fold (λc r. r ⊓ ls_query c ch x q) (map snd gcs) r) s"
proof (induction gcs arbitrary: r)
  case (Cons gc gcs)
  obtain g c where gc: "gc = (g, c)" by fastforce
  have "eval_holds q (ls_query c ch x q) s"
    using Cons.prems unfolding gc by (simp add: sound_local_spec_def)
  with Cons.prems(4) have "eval_holds q (r ⊓ ls_query c ch x q) s"
    by (rule eval_query.inf_sound)
  then show ?case
    using Cons.IH[of "r ⊓ ls_query c ch x q"] Cons.prems(1-3) unfolding gc by simp
qed simp

section ‹A component as a specification›

text ‹
  A component runs as the specification whose fields are its own operations,
  each given the component's closed channel on the state it is asked about. The
  specification reads no global and publishes none. Its channel is a pure
  function of the state, so a transfer asks it whatever it needs while it runs,
  as a Goblint transfer asks ‹man.ask›. Entry starts both halves at the
  caller's record.
›

text ‹The step a component takes on an edge, with its own channel.›

definition closed_step :: "'s local_spec ⇒ edge_action ⇒ 's ⇒ 's" where
  "closed_step c a d = ls_step c (ls_channel c d) a d"

text ‹‹⟦a⟧⇧♯⇘c⇙ d› is the abstract transfer of action ‹a›, the counterpart of
  the abstract evaluation ‹⟦e⟧⇧♯ d›; the subscript names the component.›

abbreviation abs_step :: "edge_action ⇒ 's local_spec ⇒ 's ⇒ 's"
  ("⟦_⟧⇧♯⇘_⇙") where
  "⟦a⟧⇧♯⇘c⇙ ≡ closed_step c a"

definition dg_spec_of :: "'s local_spec ⇒ ('x,'k,'v,'s::bot,'G) dg_spec" where
  "dg_spec_of c = local_dg_spec_template⦇
     dgs_skip := local_transfer ⟦EA_Nop⟧⇧♯⇘c⇙,
     dgs_assign := (λx e. local_transfer ⟦EA_Assign x e⟧⇧♯⇘c⇙),
     dgs_special := (λsc x. local_transfer ⟦EA_Special sc x⟧⇧♯⇘c⇙),
     dgs_branch := (λb pol. local_transfer
                      ⟦if pol then EA_Assume b else EA_AssumeNot b⟧⇧♯⇘c⇙),
     dgs_body := (λp. local_transfer ⟦EA_Body p⟧⇧♯⇘c⇙),
     dgs_return := (λe p. local_transfer ⟦EA_Ret e p⟧⇧♯⇘c⇙),
     dgs_enter := (λci. local_enter_transfer (λd. ls_enter c (ls_channel c d) ci (d, d))),
     dgs_event := (λev. local_transfer ⟦event_action ev⟧⇧♯⇘c⇙),
     dgs_combine_env := (λci. local_combine_transfer
        (λdc de. ls_combine_env c (ls_channel c dc) (ls_channel c de) ci dc de)),
     dgs_combine_assign := (λci. local_combine_transfer
        (λdc de. ls_combine_assign c (ls_channel c de) ci dc de)),
     dgs_query := local_query (ls_channel c) ⦈"


lemma dg_spec_of_simps [simp]:
  "skip⇧♯ (dg_spec_of c) = local_transfer ⟦EA_Nop⟧⇧♯⇘c⇙"
  "assign⇧♯ (dg_spec_of c) x e = local_transfer ⟦EA_Assign x e⟧⇧♯⇘c⇙"
  "special⇧♯ (dg_spec_of c) sc x = local_transfer ⟦EA_Special sc x⟧⇧♯⇘c⇙"
  "branch⇧♯ (dg_spec_of c) b pol
     = local_transfer ⟦if pol then EA_Assume b else EA_AssumeNot b⟧⇧♯⇘c⇙"
  "body⇧♯ (dg_spec_of c) p = local_transfer ⟦EA_Body p⟧⇧♯⇘c⇙"
  "return⇧♯ (dg_spec_of c) eo p = local_transfer ⟦EA_Ret eo p⟧⇧♯⇘c⇙"
  "enter⇧♯ (dg_spec_of c) ci
     = local_enter_transfer (λd. ls_enter c (ls_channel c d) ci (d, d))"
  "event⇧♯ (dg_spec_of c) ev = local_transfer ⟦event_action ev⟧⇧♯⇘c⇙"
  "combine_env⇧♯ (dg_spec_of c) ci = local_combine_transfer
     (λdc de. ls_combine_env c (ls_channel c dc) (ls_channel c de) ci dc de)"
  "combine_assign⇧♯ (dg_spec_of c) ci = local_combine_transfer
     (λdc de. ls_combine_assign c (ls_channel c de) ci dc de)"
  "dgs_query (dg_spec_of c) = local_query (ls_channel c)"
  by (simp_all add: dg_spec_of_def)

lemma dg_spec_step_dg_spec_of [simp]:
  "dg_spec_step (dg_spec_of c) a = local_transfer ⟦a⟧⇧♯⇘c⇙"
  by (cases a) simp_all

lemma dg_spec_combine_transfer_dg_spec_of [simp]:
  "dg_spec_combine_transfer (dg_spec_of c) ci
     = local_combine_transfer (λdc de. ls_combine c (ls_channel c dc) (ls_channel c de) ci dc de)"
  by (intro ext) (simp add: dg_spec_combine_transfer_local local_combine_transfer_def)

lemma dg_spec_wf_dg_spec_of [intro, simp]: "dg_spec_wf (dg_spec_of c)"
  by (auto simp: dg_spec_wf_def local_query_def local_enter_transfer_def
      local_combine_transfer_def local_transfer_def)

text ‹
  Run as a specification, a sound component's step and return are sound
  outright: its own channel holds at every store its state describes, so the
  laws it proves against every holding channel apply to that one.
›

lemma closed_step_sound:
  assumes sound: "sound_local_spec 𝒢 gm c"
  shows "edge_collect a (gm d) ⊆ gm (⟦a⟧⇧♯⇘c⇙ d)"
proof -
  have "gm d = gm d ∩ Collect (eval_query.channel_holds (ls_channel c d))"
    using ls_channel_sound[OF sound] by blast
  moreover have "edge_collect a (gm d ∩ Collect (eval_query.channel_holds (ls_channel c d)))
      ⊆ gm (ls_step c (ls_channel c d) a d)"
    using sound unfolding sound_local_spec_def by blast
  ultimately show ?thesis by (simp add: closed_step_def)
qed

lemma closed_combine_sound:
  assumes sound: "sound_local_spec 𝒢 gm c" and "s ∈ gm dc" and "t ∈ gm de"
  shows "combine_collect 𝒢 (ci_dst ci) s t
           ∈ gm (ls_combine c (ls_channel c dc) (ls_channel c de) ci dc de)"
  using assms ls_channel_sound[OF sound assms(2)] ls_channel_sound[OF sound assms(3)]
  unfolding sound_local_spec_def by blast

theorem dg_spec_of_contract:
  assumes sound: "sound_local_spec 𝒢 gm c"
  shows "analysis_contract (dg_spec_of c) (λd g. gm d) 𝒢"
proof (unfold_locales, goal_cases wf mono step comb)
  case wf
  then show ?case by (rule dg_spec_wf_dg_spec_of)
next
  case mono
  then show ?case using sound unfolding sound_local_spec_def by metis
next
  case (step a τ src gk)
  then show ?case
    using closed_step_sound[OF sound] by (simp add: dg_spec_edge_program_def)
next
  case comb
  then show ?case
    by (simp add: local_combine_transfer_def closed_combine_sound[OF sound])
qed

section ‹Several components as one›

text ‹
  The combination of several components is itself a component. One
  component is its own combination, so a single analysis and an ‹MCP› of one
  analysis are the same specification. Several components run their returns
  one after the other, each through both of its stages: the combination's env
  stage runs every component's composite, and its assign stage keeps the state
  it is handed. Running every env stage before every assign stage would need the
  stages of different components to commute, which independence of their
  concretizations does not give. The composite needs the caller's channel, which
  only the env stage receives.
›

fun mcp_combine :: "'s local_spec list ⇒ 's local_spec" where
  "mcp_combine [c] = c"
| "mcp_combine cs =
     make_local_spec (mcp_qry cs) (mcp_step cs) (mcp_en_from cs) (mcp_comb cs) (λch' ci dc de. dc)"

definition mcp_spec :: "'s local_spec list ⇒ ('x,'k,'v,'s::bot,'G) dg_spec" where
  "mcp_spec cs = dg_spec_of (mcp_combine cs)"

theorem mcp_combine_sound:
  assumes sound: "∀(γ⇩i, c⇩i) ∈ set comps. sound_local_spec 𝒢 γ⇩i c⇩i"
    and indep: "mcp_independent comps" and ne: "comps ≠ []"
  shows "sound_local_spec 𝒢 (mcp_gamma (map fst comps)) (mcp_combine (map snd comps))"
proof (cases "∃x. comps = [x]")
  case True
  then obtain γ⇩i c⇩i where "comps = [(γ⇩i, c⇩i)]" by fastforce
  then show ?thesis using sound by (simp add: sound_local_spec_def mcp_gamma_def)
next
  case False
  have comb: "mcp_combine (map snd comps) =
     make_local_spec (mcp_qry (map snd comps)) (mcp_step (map snd comps))
       (mcp_en_from (map snd comps)) (mcp_comb (map snd comps)) (λch' ci dc de. dc)"
    using False ne by (cases "map snd comps" rule: mcp_combine.cases) (auto simp: Cons_eq_map_conv)
  have enter: "∃q ∈ set (mcp_en_from (map snd comps) ch ci p).
                 s ∈ mcp_gamma (map fst comps) (fst q)
                 ∧ call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s
                     ∈ mcp_gamma (map fst comps) (snd q)"
    if "s ∈ mcp_gamma (map fst comps) (fst p)" "eval_query.channel_holds ch s" for ch s ci p
    using mcp_en_fold_sound[OF sound indep, of "[]" "[p]" s _ ch ci] that
    by (auto simp: mcp_en_from_def)
  have mono: "∀x y. x ≤ y ⟶ mcp_gamma (map fst comps) x ⊆ mcp_gamma (map fst comps) y"
    using sound by (fastforce simp: mcp_gamma_def sound_local_spec_def)
  have qry: "∀ch s x q. s ∈ mcp_gamma (map fst comps) x ⟶ eval_query.channel_holds ch s
               ⟶ eval_holds q (mcp_qry (map snd comps) ch x q) s"
    unfolding mcp_qry_def using mcp_qry_fold_sound[OF _ _ sound] by simp
  show ?thesis
    unfolding comb sound_local_spec_def
    using mono mcp_step_sound[OF sound indep] mcp_comb_sound[OF sound indep] enter qry
    by simp
qed

theorem mcp_contract:
  assumes "∀(γ⇩i, c⇩i) ∈ set comps. sound_local_spec 𝒢 γ⇩i c⇩i" and "mcp_independent comps"
    and "comps ≠ []"
  shows "analysis_contract (mcp_spec (map snd comps)) (λd g. mcp_gamma (map fst comps) d) 𝒢"
  unfolding mcp_spec_def by (rule dg_spec_of_contract[OF mcp_combine_sound[OF assms]])

section ‹A component on one field of a larger state›

text ‹
  A component over its own carrier ‹'c› runs on one field of the combined
  state through a lens: every operation reads the field, and writes back only
  the field, as Goblint's ‹inner_man› hands a component its own part of the
  ‹MCP› state. The channel passes through unchanged: it describes the stores
  of the whole state, which are the stores the field describes as well.
›

definition lens_of :: "('s ⇒ 'c) ⇒ ('s ⇒ 'c ⇒ 's) ⇒ 'c local_spec ⇒ 's local_spec"
where
  "lens_of get put c = make_local_spec
     (λch x. ls_query c ch (get x))
     (λch a x. put x (ls_step c ch a (get x)))
     (λch ci p. map (λ(q, e). (put (fst p) q, put (snd p) e))
                (ls_enter c ch ci (get (fst p), get (snd p))))
     (λch ch' ci x de. put x (ls_combine_env c ch ch' ci (get x) (get de)))
     (λch' ci x de. put x (ls_combine_assign c ch' ci (get x) (get de)))"

lemma get_mc_comb_lens_of:
  assumes "⋀x v. get (put x v) = v"
  shows
    "get (ls_combine (lens_of get put c) ch ch' ci x de) = ls_combine c ch ch' ci (get x) (get de)"
  by (simp add: lens_of_def assms)

theorem lens_of_sound:
  assumes sound: "sound_local_spec 𝒢 g c"
    and get_put: "⋀x v. get (put x v) = v"
    and get_mono: "⋀x y. x ≤ y ⟹ get x ≤ get y"
  shows "sound_local_spec 𝒢 (λx. g (get x)) (lens_of get put c)"
proof -
  have enter: "∃q ∈ set (ls_enter (lens_of get put c) ch ci p).
                 s ∈ g (get (fst q))
                 ∧ call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s
                     ∈ g (get (snd q))"
    if s_in: "s ∈ g (get (fst p))" and A: "eval_query.channel_holds ch s" for ch s ci p
  proof -
    have "s ∈ g (fst (get (fst p), get (snd p)))" using s_in by simp
    then obtain q where "q ∈ set (ls_enter c ch ci (get (fst p), get (snd p)))" "s ∈ g (fst q)"
        "call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s ∈ g (snd q)"
      using sound A unfolding sound_local_spec_def by metis
    then show ?thesis
      by (intro bexI[of _ "(put (fst p) (fst q), put (snd p) (snd q))"])
         (auto simp: lens_of_def get_put)
  qed
  show ?thesis
    using sound get_mono enter
    unfolding sound_local_spec_def get_mc_comb_lens_of[of get put, OF get_put]
    by (simp add: lens_of_def get_put)
qed

section ‹Replacing a component's handler›

text ‹
  The handler is the only operation that neither changes a state nor is framed,
  so any other handler that answers soundly for the same states may replace it.
  This is how an analysis written without a query handler becomes a provider
  once it runs in the combined state.
›

definition with_qry :: "(channel ⇒ 's ⇒ channel) ⇒ 's local_spec ⇒ 's local_spec" where
  "with_qry h c = c⦇ls_query := h⦈"

theorem with_qry_sound:
  assumes "sound_local_spec 𝒢 gm c"
    and "⋀ch s x q. s ∈ gm x ⟹ eval_query.channel_holds ch s ⟹ eval_holds q (h ch x q) s"
  shows "sound_local_spec 𝒢 gm (with_qry h c)"
  using assms unfolding sound_local_spec_def with_qry_def by simp

lemma with_qry_frame: "mcp_frame c g ⟹ mcp_frame (with_qry h c) g"
  by (simp add: mcp_frame_def with_qry_def)

section ‹Normalizing what a component produces›

text ‹
  A normalization ‹k› that keeps a state's concretization may be applied to
  what a component produces: each step, the entered half of each entry, and
  the return after its second stage. The caller half of an entry is the
  caller's state and stays as it is. The first stage of a return is left
  alone, because the component's soundness speaks only about the composite.
  The combined state of several analyses uses this to become unreachable as
  soon as one active analysis is, as Goblint's ‹MCP› raises ‹Deadcode›.
›

definition map_local_spec :: "('s ⇒ 's) ⇒ 's local_spec ⇒ 's local_spec" where
  "map_local_spec k c = make_local_spec (ls_query c)
     (λch a x. k (ls_step c ch a x))
     (λch ci p. map (λ(q, e). (q, k e)) (ls_enter c ch ci p))
     (ls_combine_env c)
     (λch' ci x de. k (ls_combine_assign c ch' ci x de))"

theorem map_local_spec_sound:
  assumes sound: "sound_local_spec 𝒢 g c"
    and keep: "⋀x. g (k x) = g x"
  shows "sound_local_spec 𝒢 g (map_local_spec k c)"
proof -
  have enter: "∃q ∈ set (ls_enter (map_local_spec k c) ch ci p).
                 s ∈ g (fst q)
                 ∧ call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s ∈ g (snd q)"
    if s_in: "s ∈ g (fst p)" and A: "eval_query.channel_holds ch s" for ch s ci p
  proof -
    obtain q where "q ∈ set (ls_enter c ch ci p)" "s ∈ g (fst q)"
        "call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s ∈ g (snd q)"
      using sound s_in A unfolding sound_local_spec_def by metis
    then show ?thesis
      by (intro bexI[of _ "(fst q, k (snd q))"]) (auto simp: map_local_spec_def keep)
  qed
  show ?thesis
    using sound enter unfolding sound_local_spec_def
    by (simp add: map_local_spec_def keep)
qed

section ‹Components whose entry answers once›

text ‹
  An entry that answers a single alternative, paired with the caller's own
  state, is what the routed pipeline consumes. Lenses, combination and
  normalization keep that shape.
›

definition single_entry :: "'s local_spec ⇒ bool" where
  "single_entry c ⟷ (∀ch ci p. ∃e. ls_enter c ch ci p = [(fst p, e)])"

lemma single_entryD:
  "single_entry c ⟹ ls_enter c ch ci p = [(fst p, snd (hd (ls_enter c ch ci p)))]"
  unfolding single_entry_def by (metis list.sel(1) snd_conv)

lemma single_entry_lens_of:
  assumes single: "single_entry c" and put_get: "⋀x. put x (get x) = x"
  shows "single_entry (lens_of get put c)"
  unfolding single_entry_def
proof (intro allI)
  fix ch ci p
  obtain e where "ls_enter c ch ci (get (fst p), get (snd p)) = [(get (fst p), e)]"
    using single unfolding single_entry_def by (metis fst_conv)
  then show "∃e. ls_enter (lens_of get put c) ch ci p = [(fst p, e)]"
    by (simp add: lens_of_def put_get)
qed

lemma single_entry_map_local_spec:
  assumes "single_entry c"
  shows "single_entry (map_local_spec k c)"
  unfolding single_entry_def
proof (intro allI)
  fix ch ci p
  obtain e where "ls_enter c ch ci p = [(fst p, e)]"
    using assms unfolding single_entry_def by blast
  then show "∃e. ls_enter (map_local_spec k c) ch ci p = [(fst p, e)]"
    by (simp add: map_local_spec_def)
qed

lemma single_entry_with_qry: "single_entry c ⟹ single_entry (with_qry h c)"
  by (simp add: single_entry_def with_qry_def)

lemma single_entry_mcp_en_fold:
  assumes "∀c ∈ set cs. single_entry c"
  shows "∃e. fold (λc ps. concat (map (ls_enter c ch ci) ps)) cs [(d, e0)] = [(d, e)]"
  using assms
proof (induction cs arbitrary: e0)
  case (Cons c cs)
  obtain e1 where "ls_enter c ch ci (d, e0) = [(d, e1)]"
    using Cons.prems unfolding single_entry_def by (metis fst_conv list.set_intros(1))
  then show ?case using Cons.IH[of e1] Cons.prems by simp
qed simp

lemma single_entry_mcp_combine:
  assumes single: "∀c ∈ set cs. single_entry c" and ne: "cs ≠ []"
  shows "single_entry (mcp_combine cs)"
proof (cases "∃c. cs = [c]")
  case True
  then show ?thesis using single by auto
next
  case False
  then have "ls_enter (mcp_combine cs) = mcp_en_from cs"
    using ne by (cases cs rule: mcp_combine.cases) auto
  then show ?thesis
    unfolding single_entry_def mcp_en_from_def
    using single_entry_mcp_en_fold[OF single] by (metis prod.collapse)
qed

section ‹One field of a reachability-lifted record›

text ‹
  The combined state is a record of fields under one reachability lift, whose
  \<^const>‹Bot› is the state no analysis can reach. Each field has a bottom of
  its own: a reachability-lifted field's is \<^const>‹Bot›, and a carrier with an
  unreachable element of its own uses that. A field's lens reads the field's
  bottom from the unreachable state, and writing any other value into it starts
  from the record whose fields are all at bottom. Writing bottom into the
  unreachable state leaves it unreachable, so writing back what was read
  changes nothing.
›

definition lift_get :: "('r ⇒ 'c::bot) ⇒ 'r lifted ⇒ 'c" where
  "lift_get f x = (case x of Bot ⇒ ⊥ | Lifted r ⇒ f r)"

definition lift_put :: "('r ⇒ 'c::bot ⇒ 'r) ⇒ 'r::bot lifted ⇒ 'c ⇒ 'r lifted" where
  "lift_put u x v =
     (case x of
        Bot ⇒ (if v = ⊥ then Bot else Lifted (u ⊥ v))
      | Lifted r ⇒ Lifted (u r v))"

lemma lift_get_simps [simp]:
  "lift_get f Bot = ⊥" "lift_get f (Lifted r) = f r"
  by (simp_all add: lift_get_def)

lemma lift_get_put:
  assumes "⋀r v. f (u r v) = v" and "f ⊥ = ⊥"
  shows "lift_get f (lift_put u x v) = v"
  using assms by (cases x) (simp_all add: lift_put_def)

lemma lift_put_get:
  assumes "⋀r. u r (f r) = r"
  shows "lift_put u x (lift_get f x) = x"
  using assms by (cases x) (simp_all add: lift_put_def)

lemma lift_get_mono:
  fixes f :: "'r::semilattice_sup ⇒ 'c::order_bot"
  assumes "⋀r r'. r ≤ r' ⟹ f r ≤ f r'"
  shows "x ≤ y ⟹ lift_get f x ≤ lift_get f y"
  using assms by (cases x; cases y) simp_all

lemma lift_get_put_other:
  assumes "⋀r v. f2 (u1 r v) = f2 r" and "f2 ⊥ = ⊥"
  shows "lift_get f2 (lift_put u1 x v) = lift_get f2 x"
  using assms by (cases x) (simp_all add: lift_put_def)

text ‹
  Components that each own a distinct field are independent: a list of
  distinct analyses, each run on its own field, satisfies
  \<^const>‹mcp_independent› as soon as every one leaves every other field alone.
›

lemma mcp_independent_map:
  assumes "distinct as"
    and "⋀a b. a ∈ set as ⟹ b ∈ set as ⟹ a ≠ b ⟹ mcp_frame (c a) (g b)"
  shows "mcp_independent (map (λa. (g a, c a)) as)"
  using assms by (induction as) auto

end