Theory Wasm_Soundness

section ‹Soundness Theorems›

theory Wasm_Soundness imports Main Wasm_Properties begin

theorem preservation:
  assumes "⊢_i s;vs;es : ts"
          "⦇s;vs;es⦈ ↝_i ⦇s';vs';es'⦈"
  shows "⊢_i s';vs';es' : ts"
proof -
  obtain 𝒮 where "store_typing s 𝒮" "𝒮∙None ⊩_i vs;es : ts"
    using assms(1) config_typing.simps
    by blast
  hence "store_typing s' 𝒮" "𝒮∙None ⊩_i vs';es' : ts"
    using assms(2) store_preserved types_preserved_e
    by simp_all
  thus ?thesis
    using config_typing.intros
    by blast
qed

theorem progress:
  assumes "⊢_i s;vs;es : ts"
  shows "const_list es ∨ es = [Trap] ∨ (∃a s' vs' es'. ⦇s;vs;es⦈ ↝_i ⦇s';vs';es'⦈)"
proof -
  obtain 𝒮 where "store_typing s 𝒮" "𝒮∙None ⊩_i vs;es : ts"
    using assms config_typing.simps
    by blast
  thus ?thesis
    using progress_e3
    by blast
qed

end