Theory Interval_Sound

theory Interval_Sound
  imports
    Interval_Exec
begin

section ‹What the initial abstract state describes›

text ‹
  Interval's specification and its soundness are not restated here:
  ‹ivl_tf.spec_exec› is sound against ‹λd g. γ (ρ⇘𝒢⇙ d)› by
  ‹ivl_tf.sound_exec› and ‹ivl_tf.entry_cover_exec›, which every non-relational
  bundle gets from \<^locale>‹sound_nonrelational_ops›.
›

text ‹
  The initial-state contract, owned here rather than reproved at each of the four
  assembly instances: every concrete store a run may start in is described by
  \<^const>‹cinit_ivl_st›. A declared global starts at zero, which the singleton
  interval describes exactly; a local starts unconstrained, which the unbounded
  interval describes trivially. The solver discipline does not enter into it, which
  is why one lemma serves all four.
›

lemma interval_cinit_gamma:
  "cinit_stores 𝒢 ⊆ default_st_gamma 𝒢 cinit_ivl_st"
  by (auto simp: cinit_stores_def gamma_state_def default_st_gamma_initial)

end