Theory MCP_Carrier

theory MCP_Carrier
  imports
    "Voblint_CLI.Analysis_Config"
    "Voblint_CLI.Dispatch_Carrier"
    "Voblint_Analysis_Sign.Sign_Analyses"
    "Voblint_Analysis_Interval.Interval_Analyses"
    "Voblint_Analysis_Parity.Parity_Analyses"
    "Voblint_Analysis_Int.Int_Fixpoint_Analyses"
    "Voblint_Analysis_Int.Int_Once_Analyses"
    "Voblint_Analysis_Int.Int_Never_Analyses"
    "Voblint_Analysis_Congruence.Congruence_Analyses"
    "Voblint_Analysis_Relational.Rel_Order_Local"
    "Voblint_CLI.MCP_Field"
begin

section ‹The combined state of the registered analyses›

text ‹
  Every registered analysis owns one field of the combined state. This theory names
  the analyses, lays out the fields, and states for each analysis how its field runs,
  what it describes, how it reads back and answers queries, and where it starts.
  Nothing here is proved beyond citing each analysis's own registration; the
  combination and its soundness are in ‹MCP_Analyses›.

  A new analysis adds a constructor to each datatype below, a field to the product
  types, and one equation to each function that splits on the analysis.
›

datatype analysis_domain =
    Sign_Analysis
  | Interval_Analysis
  | Parity_Analysis
  | Int_Analysis "refine_mode"
  | Congruence_Analysis
  | Order_Analysis

lemma analysis_domain_cases:
  obtains "a = Sign_Analysis"
  | "a = Interval_Analysis"
  | "a = Parity_Analysis"
  | "a = (Int_Analysis Refine_Fixpoint)"
  | "a = (Int_Analysis Refine_Once)"
  | "a = (Int_Analysis Refine_Never)"
  | "a = Congruence_Analysis"
  | "a = Order_Analysis"
  by (cases a) (metis refine_mode.exhaust)+

subsection ‹One value type wide enough for every analysis›

text ‹
  A run result crosses the dispatcher without its caller knowing which analysis
  produced it, so every published value in it has one type: a tagged union with one
  constructor per registered analysis. Each is rendered by its own analysis and listed
  by an injective key, so no printer decides which contexts are listed.
›

datatype abstract_value =
    SignValue "sign"
  | IntervalValue "ivl"
  | ParityValue "parity"
  | IntDomValue "int_dom"
  | IntDomOnceValue "int_dom"
  | IntDomNeverValue "int_dom"
  | CongruenceValue "congruence"
  | OrderValue "(vname × vname) list option"

fun string_of_abstract_value :: "abstract_value ⇒ String.literal" where
  "string_of_abstract_value (SignValue v) =
     to_string v"
| "string_of_abstract_value (IntervalValue v) =
     to_string v"
| "string_of_abstract_value (ParityValue v) =
     to_string v"
| "string_of_abstract_value (IntDomValue v) =
     to_string v"
| "string_of_abstract_value (IntDomOnceValue v) =
     to_string v"
| "string_of_abstract_value (IntDomNeverValue v) =
     to_string v"
| "string_of_abstract_value (CongruenceValue v) =
     to_string v"
| "string_of_abstract_value (OrderValue v) =
     order_view_string v"

fun abstract_value_key :: "abstract_value ⇒ order_key" where
  "abstract_value_key (SignValue v) =
     Key_List [Key_Int 0, sign_key v]"
| "abstract_value_key (IntervalValue v) =
     Key_List [Key_Int 1, ivl_key v]"
| "abstract_value_key (ParityValue v) =
     Key_List [Key_Int 2, parity_key v]"
| "abstract_value_key (IntDomValue v) =
     Key_List [Key_Int 3, int_dom_key v]"
| "abstract_value_key (IntDomOnceValue v) =
     Key_List [Key_Int 4, int_dom_key v]"
| "abstract_value_key (IntDomNeverValue v) =
     Key_List [Key_Int 5, int_dom_key v]"
| "abstract_value_key (CongruenceValue v) =
     Key_List [Key_Int 6, congruence_key v]"
| "abstract_value_key (OrderValue v) =
     Key_List [Key_Int 7, order_view_key v]"

lemma abstract_value_key_inject [simp]:
  "abstract_value_key a = abstract_value_key b ⟷ a = b"
  by (cases a; cases b) simp_all

subsection ‹Fields›

text ‹
  The combined state nests binary products, so field ‹n› sits one
  ‹pright› deeper than field ‹n - 1›. The last field is the
  right component of the innermost product.
›

definition slot1 where
  "slot1 r = pleft r"

definition slot2 where
  "slot2 r = slot1 (pright r)"

definition slot3 where
  "slot3 r = slot2 (pright r)"

definition slot4 where
  "slot4 r = slot3 (pright r)"

definition slot5 where
  "slot5 r = slot4 (pright r)"

definition slot6 where
  "slot6 r = slot5 (pright r)"

definition slot7 where
  "slot7 r = slot6 (pright r)"

definition slot8 where
  "slot8 r = pright (pright (pright (pright (pright (pright (pright r))))))"

definition set_slot1 where
  "set_slot1 r v = Product v (pright r)"

definition set_slot2 where
  "set_slot2 r v = Product (pleft r) (set_slot1 (pright r) v)"

definition set_slot3 where
  "set_slot3 r v = Product (pleft r) (set_slot2 (pright r) v)"

definition set_slot4 where
  "set_slot4 r v = Product (pleft r) (set_slot3 (pright r) v)"

definition set_slot5 where
  "set_slot5 r v = Product (pleft r) (set_slot4 (pright r) v)"

definition set_slot6 where
  "set_slot6 r v = Product (pleft r) (set_slot5 (pright r) v)"

definition set_slot7 where
  "set_slot7 r v = Product (pleft r) (set_slot6 (pright r) v)"

definition set_slot8 where
  "set_slot8 r v = Product (slot1 r) (Product (slot2 r) (Product (slot3 r) (Product (slot4 r)
    (Product (slot5 r) (Product (slot6 r) (Product (slot7 r) v))))))"

lemmas slot_defs [simp] = slot1_def slot2_def slot3_def slot4_def slot5_def slot6_def
  slot7_def slot8_def set_slot1_def set_slot2_def set_slot3_def set_slot4_def
  set_slot5_def set_slot6_def set_slot7_def set_slot8_def

type_synonym mcp_fields =
  "(sign default_st lifted, (ivl default_st lifted, (parity default_st lifted, (int_dom
    default_st lifted, (int_dom default_st lifted, (int_dom default_st lifted, (congruence
    default_st lifted, relc) analysis_product) analysis_product) analysis_product)
    analysis_product) analysis_product) analysis_product) analysis_product"

text ‹
  The combined state wraps its fields in a type of its own. Exported code then
  names each class instance of the state once; over a bare nested product it would
  rebuild the product's instance in full at every use.
›

datatype mcp_st = MCP_St (mcp_fields: mcp_fields)

instantiation mcp_st :: ord
begin

definition less_eq_mcp_st :: "mcp_st ⇒ mcp_st ⇒ bool" where
  "less_eq_mcp_st r q ⟷ mcp_fields r ≤ mcp_fields q"

definition less_mcp_st :: "mcp_st ⇒ mcp_st ⇒ bool" where
  "less_mcp_st r q ⟷ mcp_fields r < mcp_fields q"

instance ..

end

instance mcp_st :: order
  by standard
    (auto simp: less_eq_mcp_st_def less_mcp_st_def less_le_not_le mcp_st.expand
      intro: order_trans antisym)

instantiation mcp_st :: semilattice_sup
begin

definition sup_mcp_st :: "mcp_st ⇒ mcp_st ⇒ mcp_st" where
  "sup_mcp_st r q = MCP_St (mcp_fields r ⊔ mcp_fields q)"

instance
  by standard (simp_all add: less_eq_mcp_st_def sup_mcp_st_def)

end

instantiation mcp_st :: order_bot
begin

definition bot_mcp_st :: mcp_st where
  "bot_mcp_st = MCP_St ⊥"

instance
  by standard (simp add: less_eq_mcp_st_def bot_mcp_st_def)

end

instance mcp_st :: bounded_semilattice_sup_bot ..

instantiation mcp_st :: warrowing
begin

definition widen_mcp_st :: "mcp_st ⇒ mcp_st ⇒ mcp_st" where
  "widen_mcp_st r q = MCP_St (mcp_fields r ∇ mcp_fields q)"

definition narrow_mcp_st :: "mcp_st ⇒ mcp_st ⇒ mcp_st" where
  "narrow_mcp_st r q = MCP_St (mcp_fields r Δ mcp_fields q)"

instance
  by standard
    (simp_all add: less_eq_mcp_st_def widen_mcp_st_def narrow_mcp_st_def
      narrowing_class.narrow_ge narrowing_class.narrow_le
      widening_class.widen_ge1 widening_class.widen_ge2)

end

lemma MCP_St_le_MCP_St [simp]: "MCP_St a ≤ MCP_St b ⟷ a ≤ b"
  by (simp add: less_eq_mcp_st_def)

lemma mcp_fields_bot [simp]: "mcp_fields ⊥ = ⊥"
  by (simp add: bot_mcp_st_def)

lemma mcp_fields_sup [simp]: "mcp_fields (r ⊔ q) = mcp_fields r ⊔ mcp_fields q"
  by (simp add: sup_mcp_st_def)

type_synonym mcp_val =
  "(sign abs_state lifted, (ivl abs_state lifted, (parity abs_state lifted, (int_dom
    abs_state lifted, (int_dom abs_state lifted, (int_dom abs_state lifted, (congruence
    abs_state lifted, relc) analysis_product) analysis_product) analysis_product)
    analysis_product) analysis_product) analysis_product) analysis_product"

type_synonym mcp_ctx =
  "(sign list, (ivl list, (parity list, (int_dom list, (int_dom list, (int_dom list,
    (congruence list, unit list) analysis_product) analysis_product) analysis_product)
    analysis_product) analysis_product) analysis_product) analysis_product"

subsection ‹Each analysis on its own field›

text ‹
  What the analyzer runs of one analysis: how its field steps, whether it is live or
  empty, how its published value answers a query and is displayed, and the values it
  keys a callee by. ‹registration_of› is the one function that splits on
  the analysis at runtime. The concretizations are proof-only and are not part of it:
  a record the exported code builds holds executable values only, so the emptiness
  test on published values is proof-only as well.
›

record analysis_registration =
  field_spec :: "(vname ⇒ bool) ⇒ imp_prog ⇒ mcp_st lifted local_spec"
  field_live :: "mcp_st ⇒ bool"
  field_empty :: "vname list ⇒ mcp_st ⇒ bool"
  value_answer :: "mcp_val ⇒ query ⇒ answer"
  value_display :: "mcp_val ⇒ vname list ⇒ abstract_value field_state"
  context_values :: "mcp_ctx ⇒ abstract_value list"

text ‹A field of the state is a field of its product, read and written through the wrapper.›

definition st_get :: "(mcp_fields ⇒ 'c) ⇒ mcp_st ⇒ 'c" where
  "st_get f r = f (mcp_fields r)"

definition st_put :: "(mcp_fields ⇒ 'c ⇒ mcp_fields) ⇒ mcp_st ⇒ 'c ⇒ mcp_st" where
  "st_put u r v = MCP_St (u (mcp_fields r) v)"

lemmas st_lens_defs [simp] = st_get_def st_put_def

fun registration_of :: "analysis_domain ⇒ analysis_registration" where
  "registration_of Sign_Analysis =
     ⦇ field_spec = (λ𝒢 p. lens_of (lift_get (st_get slot1)) (lift_put (st_put set_slot1))
       (ask_assign (exec_local_spec 𝒢 (default_st_is_bot_for (declared_global_vars p))
       (generic_tf_st_for sign_ops 𝒢) (generic_enter_st_for sign_ops 𝒢)))), field_live =
       (λr. st_get slot1 r ≠ ⊥), field_empty = (λgs r. (case st_get slot1 r of Bot ⇒ True
       | Lifted st ⇒ default_st_is_bot_for gs st)), value_answer = (λv q. (case slot1 v of
       Bot ⇒ ⊤ | Lifted st ⇒ sign_eval_answer st q)), value_display = (λv vars. Field_Store
       (map (λx. (x, SignValue (case slot1 v of Bot ⇒ ⊥ | Lifted st ⇒ st x))) vars)),
       context_values = (λctx. map SignValue (slot1 ctx)) ⦈"
| "registration_of Interval_Analysis =
     ⦇ field_spec = (λ𝒢 p. lens_of (lift_get (st_get slot2)) (lift_put (st_put set_slot2))
       (ask_assign (exec_local_spec 𝒢 (default_st_is_bot_for (declared_global_vars p))
       (generic_tf_st_for ivl_ops 𝒢) (generic_enter_st_for ivl_ops 𝒢)))), field_live =
       (λr. st_get slot2 r ≠ ⊥), field_empty = (λgs r. (case st_get slot2 r of Bot ⇒ True
       | Lifted st ⇒ default_st_is_bot_for gs st)), value_answer = (λv q. (case slot2 v of
       Bot ⇒ ⊤ | Lifted st ⇒ interval_eval_answer st q)), value_display = (λv vars.
       Field_Store (map (λx. (x, IntervalValue (case slot2 v of Bot ⇒ ⊥ | Lifted st ⇒
       st x))) vars)), context_values = (λctx. map IntervalValue (slot2 ctx)) ⦈"
| "registration_of Parity_Analysis =
     ⦇ field_spec = (λ𝒢 p. lens_of (lift_get (st_get slot3)) (lift_put (st_put set_slot3))
       (ask_assign (exec_local_spec 𝒢 (default_st_is_bot_for (declared_global_vars p))
       (generic_tf_st_for parity_ops 𝒢) (generic_enter_st_for parity_ops 𝒢)))), field_live
       = (λr. st_get slot3 r ≠ ⊥), field_empty = (λgs r. (case st_get slot3 r of Bot ⇒
       True | Lifted st ⇒ default_st_is_bot_for gs st)), value_answer = (λv q. (case
       slot3 v of Bot ⇒ ⊤ | Lifted st ⇒ parity_eval_answer st q)), value_display = (λv
       vars. Field_Store (map (λx. (x, ParityValue (case slot3 v of Bot ⇒ ⊥ | Lifted st
       ⇒ st x))) vars)), context_values = (λctx. map ParityValue (slot3 ctx)) ⦈"
| "registration_of (Int_Analysis Refine_Fixpoint) =
     ⦇ field_spec = (λ𝒢 p. lens_of (lift_get (st_get slot4)) (lift_put (st_put set_slot4))
       (ask_assign (exec_local_spec 𝒢 (default_st_is_bot_for (declared_global_vars p))
       (generic_tf_st_for (int_dom_ops Refine_Fixpoint) 𝒢) (generic_enter_st_for
       (int_dom_ops Refine_Fixpoint) 𝒢)))), field_live = (λr. st_get slot4 r ≠ ⊥),
       field_empty = (λgs r. (case st_get slot4 r of Bot ⇒ True | Lifted st ⇒
       default_st_is_bot_for gs st)), value_answer = (λv q. (case slot4 v of Bot ⇒ ⊤ |
       Lifted st ⇒ int_eval_answer Refine_Fixpoint st q)), value_display = (λv vars.
       Field_Store (map (λx. (x, IntDomValue (case slot4 v of Bot ⇒ ⊥ | Lifted st ⇒
       st x))) vars)), context_values = (λctx. map IntDomValue (slot4 ctx)) ⦈"
| "registration_of (Int_Analysis Refine_Once) =
     ⦇ field_spec = (λ𝒢 p. lens_of (lift_get (st_get slot5)) (lift_put (st_put set_slot5))
       (ask_assign (exec_local_spec 𝒢 (default_st_is_bot_for (declared_global_vars p))
       (generic_tf_st_for (int_dom_ops Refine_Once) 𝒢) (generic_enter_st_for (int_dom_ops
       Refine_Once) 𝒢)))), field_live = (λr. st_get slot5 r ≠ ⊥), field_empty = (λgs r.
       (case st_get slot5 r of Bot ⇒ True | Lifted st ⇒ default_st_is_bot_for gs st)),
       value_answer = (λv q. (case slot5 v of Bot ⇒ ⊤ | Lifted st ⇒ int_eval_answer
       Refine_Once st q)), value_display = (λv vars. Field_Store (map (λx. (x,
       IntDomOnceValue (case slot5 v of Bot ⇒ ⊥ | Lifted st ⇒ st x))) vars)),
       context_values = (λctx. map IntDomOnceValue (slot5 ctx)) ⦈"
| "registration_of (Int_Analysis Refine_Never) =
     ⦇ field_spec = (λ𝒢 p. lens_of (lift_get (st_get slot6)) (lift_put (st_put set_slot6))
       (ask_assign (exec_local_spec 𝒢 (default_st_is_bot_for (declared_global_vars p))
       (generic_tf_st_for (int_dom_ops Refine_Never) 𝒢) (generic_enter_st_for (int_dom_ops
       Refine_Never) 𝒢)))), field_live = (λr. st_get slot6 r ≠ ⊥), field_empty = (λgs r.
       (case st_get slot6 r of Bot ⇒ True | Lifted st ⇒ default_st_is_bot_for gs st)),
       value_answer = (λv q. (case slot6 v of Bot ⇒ ⊤ | Lifted st ⇒ int_eval_answer
       Refine_Never st q)), value_display = (λv vars. Field_Store (map (λx. (x,
       IntDomNeverValue (case slot6 v of Bot ⇒ ⊥ | Lifted st ⇒ st x))) vars)),
       context_values = (λctx. map IntDomNeverValue (slot6 ctx)) ⦈"
| "registration_of Congruence_Analysis =
     ⦇ field_spec = (λ𝒢 p. lens_of (lift_get (st_get slot7)) (lift_put (st_put set_slot7))
       (ask_assign (exec_local_spec 𝒢 (default_st_is_bot_for (declared_global_vars p))
       (generic_tf_st_for congruence_ops 𝒢) (generic_enter_st_for congruence_ops 𝒢)))),
       field_live = (λr. st_get slot7 r ≠ ⊥), field_empty = (λgs r. (case st_get slot7 r
       of Bot ⇒ True | Lifted st ⇒ default_st_is_bot_for gs st)), value_answer = (λv q.
       (case slot7 v of Bot ⇒ ⊤ | Lifted st ⇒ congruence_eval_answer st q)), value_display
       = (λv vars. Field_Store (map (λx. (x, CongruenceValue (case slot7 v of Bot ⇒ ⊥ |
       Lifted st ⇒ st x))) vars)), context_values = (λctx. map CongruenceValue (slot7 ctx)) ⦈"
| "registration_of Order_Analysis =
     ⦇ field_spec = (λ𝒢 p. lens_of (lift_get (st_get slot8)) (lift_put (st_put set_slot8))
       (order_spec (program_vars p))), field_live = (λr. st_get slot8 r ≠ ⊥), field_empty =
       (λgs r. st_get slot8 r = RelBot), value_answer = (λv q. relc_qry (slot8 v) q),
       value_display = (λv vars. Field_Whole (OrderValue (order_pairs (slot8 v)))),
       context_values = (λctx. []) ⦈"

fun part_gamma :: "(vname ⇒ bool) ⇒ analysis_domain ⇒ mcp_st lifted ⇒ store set" where
  "part_gamma 𝒢 Sign_Analysis =
     (λx. gamma_lift (default_st_gamma 𝒢) (lift_get (st_get slot1) x))"
| "part_gamma 𝒢 Interval_Analysis =
     (λx. gamma_lift (default_st_gamma 𝒢) (lift_get (st_get slot2) x))"
| "part_gamma 𝒢 Parity_Analysis =
     (λx. gamma_lift (default_st_gamma 𝒢) (lift_get (st_get slot3) x))"
| "part_gamma 𝒢 (Int_Analysis Refine_Fixpoint) =
     (λx. gamma_lift (default_st_gamma 𝒢) (lift_get (st_get slot4) x))"
| "part_gamma 𝒢 (Int_Analysis Refine_Once) =
     (λx. gamma_lift (default_st_gamma 𝒢) (lift_get (st_get slot5) x))"
| "part_gamma 𝒢 (Int_Analysis Refine_Never) =
     (λx. gamma_lift (default_st_gamma 𝒢) (lift_get (st_get slot6) x))"
| "part_gamma 𝒢 Congruence_Analysis =
     (λx. gamma_lift (default_st_gamma 𝒢) (lift_get (st_get slot7) x))"
| "part_gamma 𝒢 Order_Analysis =
     (λx. γ (lift_get (st_get slot8) x))"

fun val_empty :: "analysis_domain ⇒ mcp_val ⇒ bool" where
  "val_empty Sign_Analysis v =
     (case slot1 v of Bot ⇒ True | Lifted st ⇒ is_empty_state st)"
| "val_empty Interval_Analysis v =
     (case slot2 v of Bot ⇒ True | Lifted st ⇒ is_empty_state st)"
| "val_empty Parity_Analysis v =
     (case slot3 v of Bot ⇒ True | Lifted st ⇒ is_empty_state st)"
| "val_empty (Int_Analysis Refine_Fixpoint) v =
     (case slot4 v of Bot ⇒ True | Lifted st ⇒ is_empty_state st)"
| "val_empty (Int_Analysis Refine_Once) v =
     (case slot5 v of Bot ⇒ True | Lifted st ⇒ is_empty_state st)"
| "val_empty (Int_Analysis Refine_Never) v =
     (case slot6 v of Bot ⇒ True | Lifted st ⇒ is_empty_state st)"
| "val_empty Congruence_Analysis v =
     (case slot7 v of Bot ⇒ True | Lifted st ⇒ is_empty_state st)"
| "val_empty Order_Analysis v =
     ((slot8 v) = RelBot)"

fun val_gamma :: "analysis_domain ⇒ mcp_val ⇒ store set" where
  "val_gamma Sign_Analysis v =
     γ⇩⊥ (slot1 v)"
| "val_gamma Interval_Analysis v =
     γ⇩⊥ (slot2 v)"
| "val_gamma Parity_Analysis v =
     γ⇩⊥ (slot3 v)"
| "val_gamma (Int_Analysis Refine_Fixpoint) v =
     γ⇩⊥ (slot4 v)"
| "val_gamma (Int_Analysis Refine_Once) v =
     γ⇩⊥ (slot5 v)"
| "val_gamma (Int_Analysis Refine_Never) v =
     γ⇩⊥ (slot6 v)"
| "val_gamma Congruence_Analysis v =
     γ⇩⊥ (slot7 v)"
| "val_gamma Order_Analysis v =
     γ (slot8 v)"

subsection ‹What each field publishes›

text ‹
  A published value reads each non-relational field's stored state as a total function
  on variables and keeps the order field as it is.
›

definition mcp_rd :: "(vname ⇒ bool) ⇒ mcp_st ⇒ mcp_val" where
  "mcp_rd 𝒢 r = Product (map_lift (default_st_to_fun 𝒢) (st_get slot1 r)) (Product
    (map_lift (default_st_to_fun 𝒢) (st_get slot2 r)) (Product (map_lift (default_st_to_fun
    𝒢) (st_get slot3 r)) (Product (map_lift (default_st_to_fun 𝒢) (st_get slot4 r))
    (Product (map_lift (default_st_to_fun 𝒢) (st_get slot5 r)) (Product (map_lift
    (default_st_to_fun 𝒢) (st_get slot6 r)) (Product (map_lift (default_st_to_fun 𝒢)
    (st_get slot7 r)) (st_get slot8 r)))))))"

definition mcp_gamma_v :: "analysis_domain list ⇒ mcp_val ⇒ store set" where
  "mcp_gamma_v as v = (⋂a ∈ set as. val_gamma a v)"

subsection ‹Where each field starts, and what it keys a callee by›

text ‹
  The entry state starts every active field at its analysis's own entry state and
  every other field at its bottom. A field no active analysis runs is never read, and
  keeping it at bottom makes the solver's joins, widenings and comparisons on it
  constant-time. Under the entry-state policy a callee is keyed by what the active
  fields key it by; a field no active analysis runs keys nothing.
›

definition mcp_init :: "analysis_domain list ⇒ mcp_st" where
  "mcp_init as = MCP_St (Product (if Sign_Analysis ∈ set as then Lifted cinit_sign_st
    else ⊥) (Product (if Interval_Analysis ∈ set as then Lifted cinit_ivl_st else ⊥)
    (Product (if Parity_Analysis ∈ set as then Lifted cinit_parity_st else ⊥) (Product
    (if (Int_Analysis Refine_Fixpoint) ∈ set as then Lifted cinit_int_dom_st else ⊥)
    (Product (if (Int_Analysis Refine_Once) ∈ set as then Lifted cinit_int_dom_st else
    ⊥) (Product (if (Int_Analysis Refine_Never) ∈ set as then Lifted cinit_int_dom_st
    else ⊥) (Product (if Congruence_Analysis ∈ set as then Lifted cinit_congruence_st
    else ⊥) (if Order_Analysis ∈ set as then (⊤ :: relc) else ⊥))))))))"

definition mcp_formals_route ::
  "analysis_domain list ⇒ (vname ⇒ bool) ⇒ pp ⇒ mcp_ctx ⇒ mcp_st lifted
     ⇒ call_action ⇒ mcp_ctx" where
  "mcp_formals_route as 𝒢 u ctx d ca = Product (if Sign_Analysis ∈ set as then
    exec_formals_route 𝒢 u [] (lift_get (st_get slot1) d) ca else []) (Product (if
    Interval_Analysis ∈ set as then exec_formals_route 𝒢 u [] (lift_get (st_get slot2) d) ca
    else []) (Product (if Parity_Analysis ∈ set as then exec_formals_route 𝒢 u [] (lift_get
    (st_get slot3) d) ca else []) (Product (if (Int_Analysis Refine_Fixpoint) ∈ set as then
    exec_formals_route 𝒢 u [] (lift_get (st_get slot4) d) ca else []) (Product (if
    (Int_Analysis Refine_Once) ∈ set as then exec_formals_route 𝒢 u [] (lift_get (st_get
    slot5) d) ca else []) (Product (if (Int_Analysis Refine_Never) ∈ set as then
    exec_formals_route 𝒢 u [] (lift_get (st_get slot6) d) ca else []) (Product (if
    Congruence_Analysis ∈ set as then exec_formals_route 𝒢 u [] (lift_get (st_get slot7) d)
    ca else []) (if Order_Analysis ∈ set as then [] else [])))))))"

definition mcp_root_ctx :: mcp_ctx where
  "mcp_root_ctx = Product [] (Product [] (Product [] (Product [] (Product [] (Product []
    (Product [] []))))))"

text ‹
  A key for a whole context, injective on every context: each field's values,
  field by field. Listing contexts by it drops none.
›

definition mcp_ctx_key :: "mcp_ctx ⇒ order_key" where
  "mcp_ctx_key ctx = Key_List [Key_List (map abstract_value_key (map SignValue (slot1
    ctx))), Key_List (map abstract_value_key (map IntervalValue (slot2 ctx))), Key_List
    (map abstract_value_key (map ParityValue (slot3 ctx))), Key_List (map
    abstract_value_key (map IntDomValue (slot4 ctx))), Key_List (map abstract_value_key
    (map IntDomOnceValue (slot5 ctx))), Key_List (map abstract_value_key (map
    IntDomNeverValue (slot6 ctx))), Key_List (map abstract_value_key (map CongruenceValue
    (slot7 ctx))), Key_List (map (λ_. Key_List []) (slot8 ctx))]"

lemma mcp_ctx_key_inject: "mcp_ctx_key a = mcp_ctx_key b ⟹ a = b"
  unfolding mcp_ctx_key_def slot1_def slot2_def slot3_def slot4_def slot5_def slot6_def
    slot7_def slot8_def
  by (simp add: inj_def; elim conjE; (rule analysis_product.expand; simp)+)

subsection ‹What each analysis's registration supplies›

text ‹
  Each fact below splits on the analysis and cites the matching registration.
›

lemma field_spec_sound:
  "sound_local_spec (declared_global p) (part_gamma (declared_global p) a)
     (field_spec (registration_of a) (declared_global p) p)"
  by (cases a rule: analysis_domain_cases;
      simp only: part_gamma.simps registration_of.simps analysis_registration.simps;
      rule field_component_sound[OF ask_assign_sound[OF sign_rule.exec_comp_sound]]
        field_component_sound[OF ask_assign_sound[OF interval_rule.exec_comp_sound]]
        field_component_sound[OF ask_assign_sound[OF parity_rule.exec_comp_sound]]
        field_component_sound[OF ask_assign_sound[OF int_fixpoint_rule.exec_comp_sound]]
        field_component_sound[OF ask_assign_sound[OF int_once_rule.exec_comp_sound]]
        field_component_sound[OF ask_assign_sound[OF int_never_rule.exec_comp_sound]]
        field_component_sound[OF ask_assign_sound[OF congruence_rule.exec_comp_sound]]
        field_component_sound[OF order_spec_sound];
      auto simp: less_eq_mcp_st_def less_eq_analysis_product_def)

lemma single_entry_field_spec: "single_entry (field_spec (registration_of a) 𝒢 p)"
  by (cases a rule: analysis_domain_cases) (auto intro!: single_entry_lens_of lift_put_get
    single_entry_ask_assign[OF single_entry_exec_local_spec] single_entry_order_spec)

lemma mcp_init_sound:
  "cinit_stores (declared_global p)
     ⊆ mcp_gamma_v as (mcp_rd (declared_global p) (mcp_init as))"
proof -
  have "cinit_stores (declared_global p)
          ⊆ val_gamma a (mcp_rd (declared_global p) (mcp_init as))"
    if "a ∈ set as" for a
    by (cases a rule: analysis_domain_cases)
       (use that sign_rule.init_sound interval_rule.init_sound parity_rule.init_sound
         int_fixpoint_rule.init_sound int_once_rule.init_sound int_never_rule.init_sound
         congruence_rule.init_sound in ‹simp_all add: mcp_init_def mcp_rd_def›)
  then show ?thesis by (auto simp: mcp_gamma_v_def)
qed

lemma value_answer_sound:
  "s ∈ val_gamma a v
     ⟹ eval_holds q (value_answer (registration_of a) v q) s"
  by (cases a rule: analysis_domain_cases)
     (auto split: lifted.splits intro: sign_tf.check.eval_answer_sound
       ivl_tf.check.eval_answer_sound parity_tf.check.eval_answer_sound
       int_tf.check.eval_answer_sound congruence_tf.check.eval_answer_sound
       relc_qry_sound)

end