Theory Parity_Analyses

theory Parity_Analyses
  imports
    Parity_Sound
    "Voblint_Nonrelational.Nonrel_Registration"
begin

section ‹Registering Parity at every context and update rule›

text ‹
  Parity runs through the shared D/G pipeline at the unit context. The CLI runs it as
  a field of the combined state of ‹MCP_Analyses›, whose component and
  soundness the unit registration supplies. Each registration leaves the rule that
  merges a value side-effected into a global as a parameter ‹r›. The
  equation system, the solve, the result table and every soundness endpoint come from
  the interpreted locale; this theory only names the domain's own implementation and
  facts.
›

subsection ‹At the unit context›

global_interpretation parity_rule:
    nonrel_unit_rule parity_ops cinit_parity_st r
  for r
  by (intro nonrel_unit_ruleI nonrel_registrationI
      parity_tf.sound_nonrelational_ops_axioms parity_cinit_gamma)

end