Soundness proof and mechanisation: https://github.com/WasmCert/WasmCert-Isabelle
Lemmas:
- e_type_consts
- store_extension_refl
- inst_typing_store_extension_inv
- frame_typing_store_extension_inv
- types_preserved_e2
- preservation
- progress_e
- progress_e1
- progress
- type checker correctness
- run_step_return_imp_lfilled
- run_step_break_imp_lfilled
- run_step_sound
CT-Wasm: https://github.com/PLSysSec/ct-wasm-proofs
Lemmas:
- config_indistinguishable_imp_config_typing
- config_indistinguishable_imp_reduce
- config_indistinguishable_imp_reduce2
- config_untrusted_constant_time
Relaxed memory: https://github.com/conrad-watt/repairing-and-mechanising-the-javascript-relaxed-memory-model
Lemmas: