Theory Parity_Sound

theory Parity_Sound
  imports
    Parity_Exec
begin

section ‹What a run's initial abstract state describes›

text ‹
  A run starts with every declared global at zero and every local
  unconstrained. The one lemma here says \<^const>‹cinit_parity_st› describes
  exactly that: zero is even, so \<^const>‹PEven› covers a declared global
  precisely, and \<^const>‹PTop› covers an unconstrained local trivially.
  Choosing \<^const>‹PEven› rather than \<^const>‹PTop› for globals is what makes
  this a fact worth owning: it is the one place the zero-initialization of
  globals is turned into a parity.

  Parity's specification, its concretization and the soundness of the one
  against the other are not restated here. Those are constants and theorems of
  \<^locale>‹dg_domain_exec›, and an assembly reaches them by interpreting
  that locale from Parity's own commute lemmas in
  \<^theory>‹Voblint_Analysis_Parity.Parity_Exec› --- so a per-domain copy would
  only rename what the locale already proves.
›

lemma parity_cinit_gamma:
  "cinit_stores 𝒢 ⊆ default_st_gamma 𝒢 cinit_parity_st"
  by (auto simp: cinit_stores_def gamma_state_def default_st_gamma_initial)


end