Theory Sign_Sound

theory Sign_Sound
  imports
    Sign_Exec
begin

section ‹What the initial abstract state describes›

text ‹
  Sign's specification and its soundness are not restated here:
  ‹sign_tf.spec_exec› is sound against ‹λd g. γ (ρ⇘𝒢⇙ d)› by
  ‹sign_tf.sound_exec› and ‹sign_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 assembly
  instance: every concrete store a run may start in is described by
  \<^const>‹cinit_sign_st›. It holds because a declared global starts at zero, which
  \<^const>‹SZero› describes exactly, and a local starts unconstrained, which
  \<^const>‹STop› describes trivially --- so it is a fact about Sign's initial state
  and its concretization, and about nothing else.
›

lemma sign_cinit_gamma:
  "cinit_stores 𝒢 ⊆ default_st_gamma 𝒢 cinit_sign_st"
  by (auto simp: cinit_stores_def gamma_state_def default_st_gamma_initial)

end