Theory Int_Sound

theory Int_Sound
  imports
    Int_Classify
begin

section ‹What Int supplies to the framework›

text ‹
  Two reader-commutation facts and an initial-state contract. None of the three
  mentions a context, a routing function, a seed key, or a solver. The
  commutation facts are \<^theory>‹Voblint_Analysis_Int.Int_Exec›'s
  ‹int_tf.tf_st_for_commute› and ‹int_tf.enter_st_for_commute›, proved once for
  every refinement mode.

  Int'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›, which an assembly reaches by interpreting that locale
  from the commutation facts --- so a per-domain copy would only rename what the
  locale already proves.
›

subsection ‹What the initial abstract state describes›

text ‹
  The stores a run may start in are described by the function the entry state
  represents. This mentions neither a solver nor a coverage
  assumption --- only the entry state and the global-variable predicate --- so
  it is stated here rather than inside a solved-system context.
›

lemma int_cinit_gamma:
  "cinit_stores 𝒢 ⊆ default_st_gamma 𝒢 cinit_int_dom_st"
  by (auto simp: cinit_stores_def gamma_state_def default_st_gamma_initial
      gamma_top [where 'a = int_dom, unfolded gamma_abs_int_dom_ext])

end