Theory Voblint_Analysis_Congruence.Congruence_Sound

theory Congruence_Sound
  imports
    Congruence_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_congruence_st›
  describes exactly that: the singleton residue class \<^term>‹congruence_of_int 0›
  covers a declared global precisely, and \<^const>‹top› covers an unconstrained
  local trivially. It is the one place the zero-initialization of globals is
  turned into a residue class.

  Congruence'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 Congruence's own commute lemmas in
  \<^theory>‹Voblint_Analysis_Congruence.Congruence_Exec› --- so a per-domain copy
  would only rename what the locale already proves.
›

lemma congruence_cinit_gamma:
  "cinit_stores 𝒢 ⊆ default_st_gamma 𝒢 cinit_congruence_st"
  by (auto simp: cinit_stores_def gamma_state_def default_st_gamma_initial)

end