Theory Wasm_Ast
section ‹WebAssembly Core AST›
theory Wasm_Ast
imports
Main
"Native_Word.Uint8"
"Word_Lib.Reversed_Bit_Lists"
begin
type_synonym
i = nat
type_synonym
off = nat
type_synonym
a = nat
typedecl i32
typedecl i64
typedecl f32
typedecl f64
type_synonym byte = uint8
typedef bytes = "UNIV :: byte list set" ..
setup_lifting type_definition_bytes
declare Quotient_bytes[transfer_rule]
code_datatype Abs_bytes
lemma Rep_bytes_Abs_bytes_eq [code]:
"Rep_bytes (Abs_bytes bs) = bs"
by transfer rule
lift_definition bytes_takefill :: "byte ⇒ nat ⇒ bytes ⇒ bytes"
is ‹takefill :: uint8 ⇒ nat ⇒ uint8 list ⇒ uint8 list› .
declare bytes_takefill.abs_eq [code]
lift_definition bytes_replicate :: "nat ⇒ byte ⇒ bytes"
is ‹replicate :: nat ⇒ uint8 ⇒ uint8 list› .
declare bytes_replicate.abs_eq [code]
lift_definition msbyte :: "bytes ⇒ byte"
is ‹last :: uint8 list ⇒ uint8› .
declare msbyte.abs_eq [code]
typedef mem = "UNIV :: byte list set" ..
setup_lifting type_definition_mem
declare Quotient_mem[transfer_rule]
code_datatype Abs_mem
lemma Rep_mem_Abs_mem_eq [code]:
"Rep_mem (Abs_mem bs) = bs"
by transfer rule
lift_definition read_bytes :: "mem ⇒ nat ⇒ nat ⇒ bytes"
is "λm n l. take l (drop n m)" .
declare read_bytes.abs_eq [code]
lift_definition write_bytes :: "mem ⇒ nat ⇒ bytes ⇒ mem"
is "λm n bs. (take n m) @ bs @ (drop (n + length bs) m)" .
declare write_bytes.abs_eq [code]
lift_definition mem_append :: "mem ⇒ bytes ⇒ mem"
is append .
declare mem_append.abs_eq [code]
typedecl host
typedecl host_state