section ‹WebAssembly Core AST›

theory Wasm_Ast
  imports
    Main
    "Native_Word.Uint8"
    "Word_Lib.Reversed_Bit_Lists"
begin

type_synonym ― ‹immediate›
  i = nat
type_synonym ― ‹static offset›
  off = nat
type_synonym ― ‹alignment exponent›
  a = nat

― ‹primitive types›
typedecl i32
typedecl i64
typedecl f32
typedecl f64

― ‹memory›
type_synonym byte = uint8

typedef bytes = "UNIV :: (byte list) set" ..
setup_lifting type_definition_bytes
declare Quotient_bytes[transfer_rule]

lift_definition bytes_takefill :: "byte ⇒ nat ⇒ bytes ⇒ bytes" is "(λa n as. takefill (Abs_uint8 a) n as)" .
lift_definition bytes_replicate :: "nat ⇒ byte ⇒ bytes" is "(λn b. replicate n (Abs_uint8 b))" .
definition msbyte :: "bytes ⇒ byte" where
  "msbyte bs = last (Rep_bytes bs)"

typedef mem = "UNIV :: (byte list) set" ..
setup_lifting type_definition_mem
declare Quotient_mem[transfer_rule]

lift_definition read_bytes :: "mem ⇒ nat ⇒ nat ⇒ bytes" is "(λm n l. take l (drop n m))" .
lift_definition write_bytes :: "mem ⇒ nat ⇒ bytes ⇒ mem" is "(λm n bs. (take n m) @ bs @ (drop (n + length bs) m))" .
lift_definition mem_append :: "mem ⇒ bytes ⇒ mem" is append .

― ‹host›
typedecl host
typedecl host_state

datatype ― ‹value types›
  t = T_i32 | T_i64 | T_f32 | T_f64

datatype ― ‹packed types›
  tp = Tp_i8 | Tp_i16 | Tp_i32

datatype ― ‹mutability›
  mut = T_immut | T_mut

record tg = ― ‹global types›
  tg_mut :: mut
  tg_t :: t

datatype ― ‹function types›
  tf = Tf "t list" "t list" ("_ '_> _" 60)

(* TYPING *)
record t_context =
  types_t :: "tf list"
  func_t :: "tf list"
  global :: "tg list"
  table :: "nat option"
  memory :: "nat option"
  local :: "t list"
  label :: "(t list) list"
  return :: "(t list) option"

record s_context =
  s_inst :: "t_context list"
  s_funcs :: "tf list"
  s_tab  :: "nat list"
  s_mem  :: "nat list"
  s_globs :: "tg list"

datatype
  sx = S | U

datatype
  unop_i = Clz | Ctz | Popcnt

datatype
  unop_f = Neg | Abs | Ceil | Floor | Trunc | Nearest | Sqrt

datatype
  binop_i = Add | Sub | Mul | Div sx | Rem sx | And | Or | Xor | Shl | Shr sx | Rotl | Rotr

datatype
  binop_f = Addf | Subf | Mulf | Divf | Min | Max | Copysign
  
datatype
  testop = Eqz
  
datatype
  relop_i = Eq | Ne | Lt sx | Gt sx | Le sx | Ge sx
  
datatype
  relop_f = Eqf | Nef | Ltf | Gtf | Lef | Gef
  
datatype
  cvtop = Convert | Reinterpret

datatype ― ‹values›
  v =
    ConstInt32 i32
    | ConstInt64 i64
    | ConstFloat32 f32
    | ConstFloat64 f64

datatype ― ‹basic instructions›
  b_e =
    Unreachable
    | Nop
    | Drop
    | Select
    | Block tf "b_e list"
    | Loop tf "b_e list"
    | If tf "b_e list" "b_e list"
    | Br i
    | Br_if i
    | Br_table "i list" i
    | Return
    | Call i
    | Call_indirect i
    | Get_local i
    | Set_local i
    | Tee_local i
    | Get_global i
    | Set_global i
    | Load t "(tp × sx) option" a off
    | Store t "tp option" a off
    | Current_memory
    | Grow_memory
    | EConst v ("C _" 60)
    | Unop_i t unop_i
    | Unop_f t unop_f
    | Binop_i t binop_i
    | Binop_f t binop_f
    | Testop t testop
    | Relop_i t relop_i
    | Relop_f t relop_f
    | Cvtop t cvtop t "sx option"

datatype cl = ― ‹function closures›
  Func_native i tf "t list" "b_e list"
| Func_host tf host

record inst = ― ‹instances›
  types :: "tf list"
  funcs :: "i list"
  tab :: "i option"
  mem :: "i option"
  globs :: "i list"

type_synonym tabinst = "(cl option) list"

record global =
  g_mut :: mut
  g_val :: v

record s = ― ‹store›
  inst :: "inst list"
  funcs :: "cl list"
  tab :: "tabinst list"
  mem :: "mem list"
  globs :: "global list"

datatype e = ― ‹administrative instruction›
  Basic b_e ("$_" 60)
  | Trap
  | Callcl cl
  | Label nat "e list" "e list"
  | Local nat i "v list" "e list"

datatype Lholed =
    ― ‹L0 = v* [<hole>] e*›
    LBase "e list" "e list"
    ― ‹L(i+1) = v* (label n {e* } Li) e*›
  | LRec "e list" nat "e list" Lholed "e list"
end

section ‹Syntactic Typeclasses›

theory Wasm_Type_Abs imports Main begin

class wasm_base = zero

class wasm_int = wasm_base +
  (* unops*)
  fixes int_clz :: "'a ⇒ 'a"
  fixes int_ctz :: "'a ⇒ 'a"
  fixes int_popcnt :: "'a ⇒ 'a"
  (* binops *)
  fixes int_add :: "'a ⇒ 'a ⇒ 'a"
  fixes int_sub :: "'a ⇒ 'a ⇒ 'a"
  fixes int_mul :: "'a ⇒ 'a ⇒ 'a"
  fixes int_div_u :: "'a ⇒ 'a ⇒ 'a option"
  fixes int_div_s :: "'a ⇒ 'a ⇒ 'a option"
  fixes int_rem_u :: "'a ⇒ 'a ⇒ 'a option"
  fixes int_rem_s :: "'a ⇒ 'a ⇒ 'a option"
  fixes int_and :: "'a ⇒ 'a ⇒ 'a"
  fixes int_or :: "'a ⇒ 'a ⇒ 'a"
  fixes int_xor :: "'a ⇒ 'a ⇒ 'a"
  fixes int_shl :: "'a ⇒ 'a ⇒ 'a"
  fixes int_shr_u :: "'a ⇒ 'a ⇒ 'a"
  fixes int_shr_s :: "'a ⇒ 'a ⇒ 'a"
  fixes int_rotl :: "'a ⇒ 'a ⇒ 'a"
  fixes int_rotr :: "'a ⇒ 'a ⇒ 'a"
  (* testops *)
  fixes int_eqz :: "'a ⇒ bool"
  (* relops *)
  fixes int_eq :: "'a ⇒ 'a ⇒ bool"
  fixes int_lt_u :: "'a ⇒ 'a ⇒ bool"
  fixes int_lt_s :: "'a ⇒ 'a ⇒ bool"
  fixes int_gt_u :: "'a ⇒ 'a ⇒ bool"
  fixes int_gt_s :: "'a ⇒ 'a ⇒ bool"
  fixes int_le_u :: "'a ⇒ 'a ⇒ bool"
  fixes int_le_s :: "'a ⇒ 'a ⇒ bool"
  fixes int_ge_u :: "'a ⇒ 'a ⇒ bool"
  fixes int_ge_s :: "'a ⇒ 'a ⇒ bool"
  (* value conversions *)
  fixes int_of_nat :: "nat ⇒ 'a"
  fixes nat_of_int :: "'a ⇒ nat"
begin
  abbreviation (input)
  int_ne where
    "int_ne x y ≡ ¬ (int_eq x y)"
end

class wasm_float = wasm_base +
  (* unops *)
  fixes float_neg     :: "'a ⇒ 'a"
  fixes float_abs     :: "'a ⇒ 'a"
  fixes float_ceil    :: "'a ⇒ 'a"
  fixes float_floor   :: "'a ⇒ 'a"
  fixes float_trunc   :: "'a ⇒ 'a"
  fixes float_nearest :: "'a ⇒ 'a"
  fixes float_sqrt    :: "'a ⇒ 'a"
  (* binops *)
  fixes float_add :: "'a ⇒ 'a ⇒ 'a"
  fixes float_sub :: "'a ⇒ 'a ⇒ 'a"
  fixes float_mul :: "'a ⇒ 'a ⇒ 'a"
  fixes float_div :: "'a ⇒ 'a ⇒ 'a"
  fixes float_min :: "'a ⇒ 'a ⇒ 'a"
  fixes float_max :: "'a ⇒ 'a ⇒ 'a"
  fixes float_copysign :: "'a ⇒ 'a ⇒ 'a"
  (* relops *)
  fixes float_eq :: "'a ⇒ 'a ⇒ bool"
  fixes float_lt :: "'a ⇒ 'a ⇒ bool"
  fixes float_gt :: "'a ⇒ 'a ⇒ bool"
  fixes float_le :: "'a ⇒ 'a ⇒ bool"
  fixes float_ge :: "'a ⇒ 'a ⇒ bool"
begin
  abbreviation (input)
  float_ne where
    "float_ne x y ≡ ¬ (float_eq x y)"
end
end

section ‹WebAssembly Base Definitions›

theory Wasm_Base_Defs imports Wasm_Ast Wasm_Type_Abs begin

instantiation i32 :: wasm_int begin instance .. end
instantiation i64 :: wasm_int begin instance .. end
instantiation f32 :: wasm_float begin instance .. end
instantiation f64 :: wasm_float begin instance .. end

consts
  (* inter-type conversions *)
  (* float to i32 *)
  ui32_trunc_f32 :: "f32 ⇒ i32 option"
  si32_trunc_f32 :: "f32 ⇒ i32 option"
  ui32_trunc_f64 :: "f64 ⇒ i32 option"
  si32_trunc_f64 :: "f64 ⇒ i32 option"
  (* float to i64 *)
  ui64_trunc_f32 :: "f32 ⇒ i64 option"
  si64_trunc_f32 :: "f32 ⇒ i64 option"
  ui64_trunc_f64 :: "f64 ⇒ i64 option"
  si64_trunc_f64 :: "f64 ⇒ i64 option"
  (* int to f32 *)
  f32_convert_ui32 :: "i32 ⇒ f32"
  f32_convert_si32 :: "i32 ⇒ f32"
  f32_convert_ui64 :: "i64 ⇒ f32"
  f32_convert_si64 :: "i64 ⇒ f32"
  (* int to f64 *)
  f64_convert_ui32 :: "i32 ⇒ f64"
  f64_convert_si32 :: "i32 ⇒ f64"
  f64_convert_ui64 :: "i64 ⇒ f64"
  f64_convert_si64 :: "i64 ⇒ f64"
  (* intra-{int/float} conversions *)
  wasm_wrap :: "i64 ⇒ i32"
  wasm_extend_u :: "i32 ⇒ i64"
  wasm_extend_s :: "i32 ⇒ i64"
  wasm_demote :: "f64 ⇒ f32"
  wasm_promote :: "f32 ⇒ f64"
  (* boolean encoding *)
  serialise_i32 :: "i32 ⇒ bytes"
  serialise_i64 :: "i64 ⇒ bytes"
  serialise_f32 :: "f32 ⇒ bytes"
  serialise_f64 :: "f64 ⇒ bytes"
  wasm_bool :: "bool ⇒ i32"
  int32_minus_one :: i32

  (* memory *)
definition mem_size :: "mem ⇒ nat" where
  "mem_size m = length (Rep_mem m)"

definition mem_grow :: "mem ⇒ nat ⇒ mem" where
  "mem_grow m n = mem_append m (bytes_replicate (n * 64000) 0)"

definition load :: "mem ⇒ nat ⇒ off ⇒ nat ⇒ bytes option" where
  "load m n off l = (if (mem_size m ≥ (n+off+l))
                       then Some (read_bytes m (n+off) l)
                       else None)"

definition sign_extend :: "sx ⇒ nat ⇒ bytes ⇒ bytes" where
  "sign_extend sx l bytes = (let msb = msb (msbyte bytes) in
                          let byte = (case sx of U ⇒ 0 | S ⇒ if msb then -1 else 0) in
                          bytes_takefill byte l bytes)"

definition load_packed :: "sx ⇒ mem ⇒ nat ⇒ off ⇒ nat ⇒ nat ⇒ bytes option" where
  "load_packed sx m n off lp l = map_option (sign_extend sx l) (load m n off lp)"

definition store :: "mem ⇒ nat ⇒ off ⇒ bytes ⇒ nat ⇒ mem option" where
  "store m n off bs l = (if (mem_size m ≥ (n+off+l))
                          then Some (write_bytes m (n+off) (bytes_takefill 0 l bs))
                          else None)"

definition store_packed :: "mem ⇒ nat ⇒ off ⇒ bytes ⇒ nat ⇒ mem option" where
  "store_packed = store"

consts
  wasm_deserialise :: "bytes ⇒ t ⇒ v"
  (* host *)
  host_apply :: "s ⇒ tf ⇒ host ⇒ v list ⇒ host_state ⇒ (s × v list) option"

definition typeof :: " v ⇒ t" where
  "typeof v = (case v of
                 ConstInt32 _ ⇒ T_i32
               | ConstInt64 _ ⇒ T_i64
               | ConstFloat32 _ ⇒ T_f32
               | ConstFloat64 _ ⇒ T_f64)"

definition option_projl :: "('a × 'b) option ⇒ 'a option" where
  "option_projl x = map_option fst x"

definition option_projr :: "('a × 'b) option ⇒ 'b option" where
  "option_projr x = map_option snd x"

definition t_length :: "t ⇒ nat" where
 "t_length t = (case t of
                  T_i32 ⇒ 4
                | T_i64 ⇒ 8
                | T_f32 ⇒ 4
                | T_f64 ⇒ 8)"

definition tp_length :: "tp ⇒ nat" where
 "tp_length tp = (case tp of
                 Tp_i8 ⇒ 1
               | Tp_i16 ⇒ 2
               | Tp_i32 ⇒ 4)"

definition is_int_t :: "t ⇒ bool" where
 "is_int_t t = (case t of
                  T_i32 ⇒ True
                | T_i64 ⇒ True
                | T_f32 ⇒ False
                | T_f64 ⇒ False)"

definition is_float_t :: "t ⇒ bool" where
 "is_float_t t = (case t of
                    T_i32 ⇒ False
                  | T_i64 ⇒ False
                  | T_f32 ⇒ True
                  | T_f64 ⇒ True)"

definition is_mut :: "tg ⇒ bool" where
  "is_mut tg = (tg_mut tg = T_mut)"

definition app_unop_i :: "unop_i ⇒ 'i::wasm_int ⇒ 'i::wasm_int" where
  "app_unop_i iop c =
     (case iop of
     Ctz ⇒ int_ctz c
   | Clz ⇒ int_clz c
   | Popcnt ⇒ int_popcnt c)"

definition app_unop_f :: "unop_f ⇒ 'f::wasm_float ⇒ 'f::wasm_float" where
  "app_unop_f fop c =
                 (case fop of
                    Neg ⇒ float_neg c
                  | Abs ⇒ float_abs c
                  | Ceil ⇒ float_ceil c
                  | Floor ⇒ float_floor c
                  | Trunc ⇒ float_trunc c
                  | Nearest ⇒ float_nearest c
                  | Sqrt ⇒ float_sqrt c)"

definition app_binop_i :: "binop_i ⇒ 'i::wasm_int ⇒ 'i::wasm_int ⇒ ('i::wasm_int) option" where
  "app_binop_i iop c1 c2 = (case iop of
                              Add ⇒ Some (int_add c1 c2)
                            | Sub ⇒ Some (int_sub c1 c2)
                            | Mul ⇒ Some (int_mul c1 c2)
                            | Div U ⇒ int_div_u c1 c2
                            | Div S ⇒ int_div_s c1 c2
                            | Rem U ⇒ int_rem_u c1 c2
                            | Rem S ⇒ int_rem_s c1 c2
                            | And ⇒ Some (int_and c1 c2)
                            | Or ⇒ Some (int_or c1 c2)
                            | Xor ⇒ Some (int_xor c1 c2)
                            | Shl ⇒ Some (int_shl c1 c2)
                            | Shr U ⇒ Some (int_shr_u c1 c2)
                            | Shr S ⇒ Some (int_shr_s c1 c2)
                            | Rotl ⇒ Some (int_rotl c1 c2)
                            | Rotr ⇒ Some (int_rotr c1 c2))"

definition app_binop_f :: "binop_f ⇒ 'f::wasm_float ⇒ 'f::wasm_float ⇒ ('f::wasm_float) option" where
  "app_binop_f fop c1 c2 = (case fop of
                              Addf ⇒ Some (float_add c1 c2)
                            | Subf ⇒ Some (float_sub c1 c2)
                            | Mulf ⇒ Some (float_mul c1 c2)
                            | Divf ⇒ Some (float_div c1 c2)
                            | Min ⇒ Some (float_min c1 c2)
                            | Max ⇒ Some (float_max c1 c2)
                            | Copysign ⇒ Some (float_copysign c1 c2))"

definition app_testop_i :: "testop ⇒ 'i::wasm_int ⇒ bool" where
  "app_testop_i testop c = (case testop of Eqz ⇒ int_eqz c)"

definition app_relop_i :: "relop_i ⇒ 'i::wasm_int ⇒ 'i::wasm_int ⇒ bool" where
  "app_relop_i rop c1 c2 = (case rop of
                              Eq ⇒ int_eq c1 c2
                            | Ne ⇒ int_ne c1 c2
                            | Lt U ⇒ int_lt_u c1 c2
                            | Lt S ⇒ int_lt_s c1 c2
                            | Gt U ⇒ int_gt_u c1 c2
                            | Gt S ⇒ int_gt_s c1 c2
                            | Le U ⇒ int_le_u c1 c2
                            | Le S ⇒ int_le_s c1 c2
                            | Ge U ⇒ int_ge_u c1 c2
                            | Ge S ⇒ int_ge_s c1 c2)"

definition app_relop_f :: "relop_f ⇒ 'f::wasm_float ⇒ 'f::wasm_float ⇒ bool" where
  "app_relop_f rop c1 c2 = (case rop of
                              Eqf ⇒ float_eq c1 c2
                            | Nef ⇒ float_ne c1 c2
                            | Ltf ⇒ float_lt c1 c2
                            | Gtf ⇒ float_gt c1 c2
                            | Lef ⇒ float_le c1 c2
                            | Gef ⇒ float_ge c1 c2)" 

definition types_agree :: "t ⇒ v ⇒ bool" where
  "types_agree t v = (typeof v = t)"

definition cl_type :: "cl ⇒ tf" where
  "cl_type cl = (case cl of Func_native _ tf _ _ ⇒ tf | Func_host tf _ ⇒ tf)"

definition rglob_is_mut :: "global ⇒ bool" where
  "rglob_is_mut g = (g_mut g = T_mut)"

definition stypes :: "s ⇒ nat ⇒ nat ⇒ tf" where
  "stypes s i j = ((types ((inst s)!i))!j)"
  
definition sfunc_ind :: "s ⇒ nat ⇒ nat ⇒ nat" where
  "sfunc_ind s i j = ((inst.funcs ((inst s)!i))!j)"

definition sfunc :: "s ⇒ nat ⇒ nat ⇒ cl" where
  "sfunc s i j = (funcs s)!(sfunc_ind s i j)"

definition sglob_ind :: "s ⇒ nat ⇒ nat ⇒ nat" where
  "sglob_ind s i j = ((inst.globs ((inst s)!i))!j)"
  
definition sglob :: "s ⇒ nat ⇒ nat ⇒ global" where
  "sglob s i j = (globs s)!(sglob_ind s i j)"

definition sglob_val :: "s ⇒ nat ⇒ nat ⇒ v" where
  "sglob_val s i j = g_val (sglob s i j)"

definition smem_ind :: "s ⇒ nat ⇒ nat option" where
  "smem_ind s i = (inst.mem ((inst s)!i))"

definition stab_s :: "s ⇒ nat ⇒ nat ⇒ cl option" where
  "stab_s s i j = (let stabinst = ((tab s)!i) in  (if (length (stabinst) > j) then (stabinst!j) else None))"

definition stab :: "s ⇒ nat ⇒ nat ⇒ cl option" where
  "stab s i j = (case (inst.tab ((inst s)!i)) of Some k => stab_s s k j | None => None)"

definition supdate_glob_s :: "s ⇒ nat ⇒ v ⇒ s" where
  "supdate_glob_s s k v = s⦇globs := (globs s)[k:=((globs s)!k)⦇g_val := v⦈]⦈"

definition supdate_glob :: "s ⇒ nat ⇒ nat ⇒ v ⇒ s" where
  "supdate_glob s i j v = (let k = sglob_ind s i j in supdate_glob_s s k v)"

definition is_const :: "e ⇒ bool" where
  "is_const e = (case e of Basic (C _) ⇒ True | _ ⇒ False)"
    
definition const_list :: "e list ⇒ bool" where
  "const_list xs = list_all is_const xs"

inductive store_extension :: "s ⇒ s ⇒ bool" where
"⟦insts = insts'; fs = fs'; tclss = tclss'; list_all2 (λbs bs'. mem_size bs ≤ mem_size bs') bss bss'; gs = gs'⟧ ⟹
  store_extension ⦇s.inst = insts, s.funcs = fs, s.tab = tclss, s.mem = bss, s.globs = gs⦈
                    ⦇s.inst = insts', s.funcs = fs', s.tab = tclss', s.mem = bss', s.globs = gs'⦈"

abbreviation to_e_list :: "b_e list ⇒ e list" ("$* _" 60) where
  "to_e_list b_es ≡ map Basic b_es"

abbreviation v_to_e_list :: "v list ⇒ e list" ("$$* _" 60) where
  "v_to_e_list ves ≡ map (λv. $C v) ves"

  (* Lfilled depth thing-to-fill fill-with result *)
inductive Lfilled :: "nat ⇒ Lholed ⇒ e list ⇒ e list ⇒ bool" where
  (* "Lfill (LBase vs es') es = vs @ es @ es'" *)
  L0:"⟦const_list vs; lholed = (LBase vs es')⟧ ⟹ Lfilled 0 lholed es (vs @ es @ es')"
  (* "Lfill (LRec vs ts es' l es'') es = vs @ [Label ts es' (Lfill l es)] @ es''" *)
| LN:"⟦const_list vs; lholed = (LRec vs n es' l es''); Lfilled k l es lfilledk⟧ ⟹ Lfilled (k+1) lholed es (vs @ [Label n es' lfilledk] @ es'')"

  (* Lfilled depth thing-to-fill fill-with result *)
inductive Lfilled_exact :: "nat ⇒ Lholed ⇒ e list ⇒ e list ⇒ bool" where
  (* "Lfill (LBase vs es') es = vs @ es @ es'" *)
  L0:"⟦lholed = (LBase [] [])⟧ ⟹ Lfilled_exact 0 lholed es es"
  (* "Lfill (LRec vs ts es' l es'') es = vs @ [Label ts es' (Lfill l es)] @ es''" *)
| LN:"⟦const_list vs; lholed = (LRec vs n es' l es''); Lfilled_exact k l es lfilledk⟧ ⟹ Lfilled_exact (k+1) lholed es (vs @ [Label n es' lfilledk] @ es'')"

definition load_store_t_bounds :: "a ⇒ tp option ⇒ t ⇒ bool" where
  "load_store_t_bounds a tp t = (case tp of
                                   None ⇒ 2^a ≤ t_length t
                                 | Some tp ⇒ 2^a ≤ tp_length tp ∧ tp_length tp < t_length t ∧  is_int_t t)"

definition cvt_i32 :: "sx option ⇒ v ⇒ i32 option" where
  "cvt_i32 sx v = (case v of
                   ConstInt32 c ⇒ None
                 | ConstInt64 c ⇒ Some (wasm_wrap c)
                 | ConstFloat32 c ⇒ (case sx of
                                        Some U ⇒ ui32_trunc_f32 c
                                      | Some S ⇒ si32_trunc_f32 c
                                      | None ⇒ None)
                 | ConstFloat64 c ⇒ (case sx of
                                        Some U ⇒ ui32_trunc_f64 c
                                      | Some S ⇒ si32_trunc_f64 c
                                      | None ⇒ None))"

definition cvt_i64 :: "sx option ⇒ v ⇒ i64 option" where
  "cvt_i64 sx v = (case v of
                   ConstInt32 c ⇒ (case sx of
                                        Some U ⇒ Some (wasm_extend_u c)
                                      | Some S ⇒ Some (wasm_extend_s c)
                                      | None ⇒ None)
                 | ConstInt64 c ⇒ None
                 | ConstFloat32 c ⇒ (case sx of
                                        Some U ⇒ ui64_trunc_f32 c
                                      | Some S ⇒ si64_trunc_f32 c
                                      | None ⇒ None)
                 | ConstFloat64 c ⇒ (case sx of
                                        Some U ⇒ ui64_trunc_f64 c
                                      | Some S ⇒ si64_trunc_f64 c
                                      | None ⇒ None))"

definition cvt_f32 :: "sx option ⇒ v ⇒ f32 option" where
  "cvt_f32 sx v = (case v of
                   ConstInt32 c ⇒ (case sx of
                                      Some U ⇒ Some (f32_convert_ui32 c)
                                    | Some S ⇒ Some (f32_convert_si32 c)
                                    | _ ⇒ None)
                 | ConstInt64 c ⇒ (case sx of
                                      Some U ⇒ Some (f32_convert_ui64 c)
                                    | Some S ⇒ Some (f32_convert_si64 c)
                                    | _ ⇒ None)
                 | ConstFloat32 c ⇒ None
                 | ConstFloat64 c ⇒ Some (wasm_demote c))"

definition cvt_f64 :: "sx option ⇒ v ⇒ f64 option" where
  "cvt_f64 sx v = (case v of
                   ConstInt32 c ⇒ (case sx of
                                      Some U ⇒ Some (f64_convert_ui32 c)
                                    | Some S ⇒ Some (f64_convert_si32 c)
                                    | _ ⇒ None)
                 | ConstInt64 c ⇒ (case sx of
                                      Some U ⇒ Some (f64_convert_ui64 c)
                                    | Some S ⇒ Some (f64_convert_si64 c)
                                    | _ ⇒ None)
                 | ConstFloat32 c ⇒ Some (wasm_promote c)
                 | ConstFloat64 c ⇒ None)"

definition cvt :: "t ⇒ sx option ⇒ v ⇒ v option" where
  "cvt t sx v = (case t of
                 T_i32 ⇒ (case (cvt_i32 sx v) of Some c ⇒ Some (ConstInt32 c) | None ⇒ None)
               | T_i64 ⇒ (case (cvt_i64 sx v) of Some c ⇒ Some (ConstInt64 c) | None ⇒ None) 
               | T_f32 ⇒ (case (cvt_f32 sx v) of Some c ⇒ Some (ConstFloat32 c) | None ⇒ None)
               | T_f64 ⇒ (case (cvt_f64 sx v) of Some c ⇒ Some (ConstFloat64 c) | None ⇒ None))"

definition bits :: "v ⇒ bytes" where
  "bits v = (case v of
               ConstInt32 c ⇒ (serialise_i32 c)
             | ConstInt64 c ⇒ (serialise_i64 c)
             | ConstFloat32 c ⇒ (serialise_f32 c)
             | ConstFloat64 c ⇒ (serialise_f64 c))"

definition bitzero :: "t ⇒ v" where
  "bitzero t = (case t of
                T_i32 ⇒ ConstInt32 0
              | T_i64 ⇒ ConstInt64 0
              | T_f32 ⇒ ConstFloat32 0
              | T_f64 ⇒ ConstFloat64 0)"

definition n_zeros :: "t list ⇒ v list" where
  "n_zeros ts = (map (λt. bitzero t) ts)"

lemma is_int_t_exists:
  assumes "is_int_t t"
  shows "t = T_i32 ∨ t = T_i64"
  using assms
  by (cases t) (auto simp add: is_int_t_def)

lemma is_float_t_exists:
  assumes "is_float_t t"
  shows "t = T_f32 ∨ t = T_f64"
  using assms
  by (cases t) (auto simp add: is_float_t_def)


lemma int_float_disjoint: "is_int_t t = -(is_float_t t)"
  by simp (metis is_float_t_def is_int_t_def t.exhaust t.simps(13-16))

lemma stab_unfold:
  assumes "stab s i j = Some cl"
  shows "∃k. inst.tab ((inst s)!i) = Some k ∧ length ((tab s)!k) > j ∧((tab s)!k)!j = Some cl"
proof -
  obtain k where have_k:"(inst.tab ((inst s)!i)) = Some k"
    using assms
    unfolding stab_def
    by fastforce
  hence s_o:"stab s i j = stab_s s k j"
    using assms
    unfolding stab_def
    by simp
  then obtain stabinst where stabinst_def:"stabinst = ((tab s)!k)"
    by blast
  hence "stab_s s k j = (stabinst!j) ∧ (length stabinst > j)"
    using assms s_o
    unfolding stab_s_def
    by (cases "(length stabinst > j)", auto)
  thus ?thesis
    using have_k stabinst_def assms s_o
    by auto
qed

lemma inj_basic: "inj Basic"
  by (meson e.inject(1) injI)

lemma inj_basic_econst: "inj (λv. $C v)"
  by (meson b_e.inject(16) e.inject(1) injI)

lemma to_e_list_1:"[$ a] = $* [a]"
  by simp

lemma to_e_list_2:"[$ a, $ b] = $* [a, b]"
  by simp

lemma to_e_list_3:"[$ a, $ b, $ c] = $* [a, b, c]"
  by simp

lemma v_exists_b_e:"∃ves. ($$*vs) = ($*ves)"
proof (induction vs)
  case (Cons a vs)
  thus ?case
  by (metis list.simps(9))
qed auto

lemma Lfilled_exact_imp_Lfilled:
  assumes "Lfilled_exact n lholed es LI"
  shows "Lfilled n lholed es LI"
  using assms
proof (induction rule: Lfilled_exact.induct)
  case (L0 lholed es)
  thus ?case
    using const_list_def Lfilled.intros(1)
    by fastforce
next
  case (LN vs lholed n es' l es'' k es lfilledk)
  thus ?case
    using Lfilled.intros(2)
    by fastforce
qed

lemma Lfilled_exact_app_imp_exists_Lfilled:
  assumes "const_list ves"
          "Lfilled_exact n lholed (ves@es) LI"
  shows "∃lholed'. Lfilled n lholed' es LI"
  using assms(2,1)
proof (induction "(ves@es)" LI rule: Lfilled_exact.induct)
  case (L0 lholed)
  show ?case
    using Lfilled.intros(1)[OF L0(2), of _ "[]"]
    by fastforce
next
  case (LN vs lholed n es' l es'' k lfilledk)
  thus ?case
    using Lfilled.intros(2)
    by fastforce
qed

lemma Lfilled_imp_exists_Lfilled_exact:
  assumes "Lfilled n lholed es LI"
  shows "∃lholed' ves es_c. const_list ves ∧ Lfilled_exact n lholed' (ves@es@es_c) LI"
  using assms Lfilled_exact.intros
  by (induction rule: Lfilled.induct) fastforce+

lemma n_zeros_typeof:
  "n_zeros ts = vs ⟹ (ts = map typeof vs)"
proof (induction ts arbitrary: vs)
  case Nil
  thus ?case
    unfolding n_zeros_def
    by simp
next
  case (Cons t ts)
  obtain vs' where "n_zeros ts = vs'"
    using n_zeros_def
    by blast
  moreover
  have "typeof (bitzero t) = t"
    unfolding typeof_def bitzero_def
    by (cases t, simp_all)
  ultimately
  show ?case
    using Cons
    unfolding n_zeros_def
    by auto
qed

end

theory Wasm imports Wasm_Base_Defs begin

(* TYPING RELATION *)
inductive b_e_typing :: "[t_context, b_e list, tf] ⇒ bool" ("_ ⊢ _ : _" 60) where
  ― ‹‹num ops››
  const:"𝒞 ⊢ [C v]         : ([]    _> [(typeof v)])"
| unop_i:"is_int_t t   ⟹ 𝒞 ⊢ [Unop_i t _]  : ([t]   _> [t])"
| unop_f:"is_float_t t ⟹ 𝒞 ⊢ [Unop_f t _]  : ([t]   _> [t])"
| binop_i:"is_int_t t   ⟹ 𝒞 ⊢ [Binop_i t iop] : ([t,t] _> [t])"
| binop_f:"is_float_t t ⟹ 𝒞 ⊢ [Binop_f t _] : ([t,t] _> [t])"
| testop:"is_int_t t   ⟹ 𝒞 ⊢ [Testop t _]  : ([t]   _> [T_i32])"
| relop_i:"is_int_t t   ⟹ 𝒞 ⊢ [Relop_i t _] : ([t,t] _> [T_i32])"
| relop_f:"is_float_t t ⟹ 𝒞 ⊢ [Relop_f t _] : ([t,t] _> [T_i32])"
  ― ‹‹convert››
| convert:"⟦(t1 ≠ t2); (sx = None) = ((is_float_t t1 ∧ is_float_t t2) ∨ (is_int_t t1 ∧ is_int_t t2 ∧ (t_length t1 < t_length t2)))⟧ ⟹ 𝒞 ⊢ [Cvtop t1 Convert t2 sx] : ([t2] _> [t1])"
  ― ‹‹reinterpret››
| reinterpret:"⟦(t1 ≠ t2); t_length t1 = t_length t2⟧ ⟹ 𝒞 ⊢ [Cvtop t1 Reinterpret t2 None] : ([t2] _> [t1])"
  ― ‹‹unreachable, nop, drop, select››
| unreachable:"𝒞 ⊢ [Unreachable] : (ts _> ts')"
| nop:"𝒞 ⊢ [Nop] : ([] _> [])"
| drop:"𝒞 ⊢ [Drop] : ([t] _> [])"
| select:"𝒞 ⊢ [Select] : ([t,t,T_i32] _> [t])"
  ― ‹‹block››
| block:"⟦tf = (tn _> tm); 𝒞⦇label := ([tm] @ (label 𝒞))⦈ ⊢ es : (tn _> tm)⟧ ⟹ 𝒞 ⊢ [Block tf es] : (tn _> tm)"
  ― ‹‹loop››
| loop:"⟦tf = (tn _> tm); 𝒞⦇label := ([tn] @ (label 𝒞))⦈ ⊢ es : (tn _> tm)⟧ ⟹ 𝒞 ⊢ [Loop tf es] : (tn _> tm)"
  ― ‹‹if then else››
| if_wasm:"⟦tf = (tn _> tm); 𝒞⦇label := ([tm] @ (label 𝒞))⦈ ⊢ es1 : (tn _> tm); 𝒞⦇label := ([tm] @ (label 𝒞))⦈ ⊢ es2 : (tn _> tm)⟧ ⟹ 𝒞 ⊢ [If tf es1 es2] : (tn @ [T_i32] _> tm)"
  ― ‹‹br››
| br:"⟦i < length(label 𝒞); (label 𝒞)!i = ts⟧ ⟹ 𝒞 ⊢ [Br i] : (t1s @ ts _> t2s)"
  ― ‹‹br_if››
| br_if:"⟦i < length(label 𝒞); (label 𝒞)!i = ts⟧ ⟹ 𝒞 ⊢ [Br_if i] : (ts @ [T_i32] _> ts)"
  ― ‹‹br_table››
| br_table:"⟦list_all (λi. i < length(label 𝒞) ∧ (label 𝒞)!i = ts) (is@[i])⟧ ⟹ 𝒞 ⊢ [Br_table is i] : (t1s @ ts @ [T_i32] _> t2s)"
  ― ‹‹return››
| return:"⟦(return 𝒞) = Some ts⟧ ⟹ 𝒞 ⊢ [Return] : (t1s @ ts _> t2s)"
  ― ‹‹call››
| call:"⟦i < length(func_t 𝒞); (func_t 𝒞)!i = tf⟧ ⟹ 𝒞 ⊢ [Call i] : tf"
  ― ‹‹call_indirect››
| call_indirect:"⟦i < length(types_t 𝒞); (types_t 𝒞)!i = (t1s _> t2s); (table 𝒞) ≠ None⟧ ⟹ 𝒞 ⊢ [Call_indirect i] : (t1s @ [T_i32] _> t2s)"
  ― ‹‹get_local››
| get_local:"⟦i < length(local 𝒞); (local 𝒞)!i = t⟧ ⟹ 𝒞 ⊢ [Get_local i] : ([] _> [t])"
  ― ‹‹set_local››
| set_local:"⟦i < length(local 𝒞); (local 𝒞)!i = t⟧ ⟹ 𝒞 ⊢ [Set_local i] : ([t] _> [])"
  ― ‹‹tee_local››
| tee_local:"⟦i < length(local 𝒞); (local 𝒞)!i = t⟧ ⟹ 𝒞 ⊢ [Tee_local i] : ([t] _> [t])"
  ― ‹‹get_global››
| get_global:"⟦i < length(global 𝒞); tg_t ((global 𝒞)!i) = t⟧ ⟹ 𝒞 ⊢ [Get_global i] : ([] _> [t])"
  ― ‹‹set_global››
| set_global:"⟦i < length(global 𝒞); tg_t ((global 𝒞)!i) = t; is_mut ((global 𝒞)!i)⟧ ⟹ 𝒞 ⊢ [Set_global i] : ([t] _> [])"
  ― ‹‹load››
| load:"⟦(memory 𝒞) = Some n; load_store_t_bounds a (option_projl tp_sx) t⟧ ⟹ 𝒞 ⊢ [Load t tp_sx a off] : ([T_i32] _> [t])"
  ― ‹‹store››
| store:"⟦(memory 𝒞) = Some n; load_store_t_bounds a tp t⟧ ⟹ 𝒞 ⊢ [Store t tp a off] : ([T_i32,t] _> [])"
  ― ‹‹current_memory››
| current_memory:"(memory 𝒞) = Some n ⟹ 𝒞 ⊢ [Current_memory] : ([] _> [T_i32])"
  ― ‹‹Grow_memory››
| grow_memory:"(memory 𝒞) = Some n ⟹ 𝒞 ⊢ [Grow_memory] : ([T_i32] _> [T_i32])"
  ― ‹‹empty program››
| empty:"𝒞 ⊢ [] : ([] _> [])"
  ― ‹‹composition››
| composition:"⟦𝒞 ⊢ es : (t1s _> t2s); 𝒞 ⊢ [e] : (t2s _> t3s)⟧ ⟹ 𝒞 ⊢ es @ [e] : (t1s _> t3s)"
  ― ‹‹weakening››
| weakening:"𝒞 ⊢ es : (t1s _> t2s) ⟹ 𝒞 ⊢ es : (ts @ t1s _> ts @ t2s)"

inductive cl_typing :: "[s_context, cl, tf] ⇒ bool" where
   "⟦i < length (s_inst 𝒮); ((s_inst 𝒮)!i) = 𝒞; tf = (t1s _> t2s); 𝒞⦇local := (local 𝒞) @ t1s @ ts, label := ([t2s] @ (label 𝒞)), return := Some t2s⦈ ⊢ es : ([] _> t2s)⟧ ⟹ cl_typing 𝒮 (Func_native i tf ts es) (t1s _> t2s)"
|  "cl_typing 𝒮 (Func_host tf h) tf"

(* lifting the b_e_typing relation to the administrative operators *)
inductive e_typing :: "[s_context, t_context, e list, tf] ⇒ bool" ("_∙_ ⊢ _ : _" 60)
and       s_typing :: "[s_context, (t list) option, nat, v list, e list, t list] ⇒ bool" ("_∙_ ⊩'_ _ _;_ : _" 60) where
(* section: e_typing *)
  (* lifting *)
  "𝒞 ⊢ b_es : tf ⟹ 𝒮∙𝒞 ⊢ $*b_es : tf"
  (* composition *)
| "⟦𝒮∙𝒞 ⊢ es : (t1s _> t2s); 𝒮∙𝒞 ⊢ [e] : (t2s _> t3s)⟧ ⟹ 𝒮∙𝒞 ⊢ es @ [e] : (t1s _> t3s)"
  (* weakening *)
| "𝒮∙𝒞 ⊢ es : (t1s _> t2s) ⟹𝒮∙𝒞 ⊢ es : (ts @ t1s _> ts @ t2s)"
  (* trap *)
| "𝒮∙𝒞 ⊢ [Trap] : tf"
  (* local *)
| "⟦𝒮∙Some ts ⊩_i vs;es : ts; length ts = n⟧ ⟹ 𝒮∙𝒞 ⊢ [Local n i vs es] : ([] _> ts)"
  (* callcl *)
| "⟦cl_typing 𝒮 cl tf⟧ ⟹ 𝒮∙𝒞  ⊢ [Callcl cl] : tf"
  (* label *)
| "⟦𝒮∙𝒞 ⊢ e0s : (ts _> t2s); 𝒮∙𝒞⦇label := ([ts] @ (label 𝒞))⦈ ⊢ es : ([] _> t2s); length ts = n⟧ ⟹ 𝒮∙𝒞 ⊢ [Label n e0s es] : ([] _> t2s)"
(* section: s_typing *)
| "⟦i < (length (s_inst 𝒮)); tvs = map typeof vs; 𝒞 =((s_inst 𝒮)!i)⦇local := (local ((s_inst 𝒮)!i) @ tvs), return := rs⦈; 𝒮∙𝒞 ⊢ es : ([] _> ts); (rs = Some ts) ∨ rs = None⟧ ⟹ 𝒮∙rs ⊩_i vs;es : ts"

definition "globi_agree gs n g = (n < length gs ∧ gs!n = g)"

definition "memi_agree sm j m = ((∃j' m'. j = Some j' ∧ j' < length sm ∧  m = Some m' ∧ sm!j' = m') ∨ j = None ∧ m = None)"

definition "funci_agree fs n f = (n < length fs ∧ fs!n = f)"

inductive inst_typing :: "[s_context, inst, t_context] ⇒ bool" where
  "⟦list_all2 (funci_agree (s_funcs 𝒮)) fs tfs; list_all2 (globi_agree (s_globs 𝒮)) gs tgs; (i = Some i' ∧ i' < length (s_tab 𝒮) ∧ (s_tab 𝒮)!i' = (the n)) ∨ (i = None ∧ n = None); memi_agree (s_mem 𝒮) j m⟧ ⟹ inst_typing 𝒮 ⦇types = ts, funcs = fs, tab = i, mem = j, globs = gs⦈ ⦇types_t = ts, func_t = tfs, global = tgs, table = n, memory = m, local = [], label = [], return = None⦈"

definition "glob_agree g tg = (tg_mut tg = g_mut g ∧ tg_t tg = typeof (g_val g))"

definition "tab_agree 𝒮 tcl = (case tcl of None ⇒ True | Some cl ⇒ ∃tf. cl_typing 𝒮 cl tf)"

definition "mem_agree bs m = (λ bs m. m ≤ mem_size bs) bs m"

inductive store_typing :: "[s, s_context] ⇒ bool" where
  "⟦𝒮 = ⦇s_inst = 𝒞s, s_funcs = tfs, s_tab = ns, s_mem = ms, s_globs = tgs⦈; list_all2 (inst_typing 𝒮) insts 𝒞s; list_all2 (cl_typing 𝒮) fs tfs; list_all (tab_agree 𝒮) (concat tclss); list_all2 (λ tcls n. n ≤ length tcls) tclss ns; list_all2 mem_agree bss ms; list_all2 glob_agree gs tgs⟧ ⟹ store_typing ⦇s.inst = insts, s.funcs = fs, s.tab = tclss, s.mem = bss, s.globs = gs⦈ 𝒮"

inductive config_typing :: "[nat, s, v list, e list, t list] ⇒ bool" ("⊢'_ _ _;_;_ : _" 60) where
  "⟦store_typing s 𝒮; 𝒮∙None ⊩_i vs;es : ts⟧ ⟹ ⊢_i s;vs;es : ts"

(* REDUCTION RELATION *)

inductive reduce_simple :: "[e list, e list] ⇒ bool" ("⦇_⦈ ↝ ⦇_⦈" 60) where
  ― ‹‹integer unary ops››
  unop_i32:"⦇[$C (ConstInt32 c), $(Unop_i T_i32 iop)]⦈ ↝ ⦇[$C (ConstInt32 (app_unop_i iop c))]⦈"
| unop_i64:"⦇[$C (ConstInt64 c), $(Unop_i T_i64 iop)]⦈ ↝ ⦇[$C (ConstInt64 (app_unop_i iop c))]⦈"
  ― ‹‹float unary ops››
| unop_f32:"⦇[$C (ConstFloat32 c), $(Unop_f T_f32 fop)]⦈ ↝ ⦇[$C (ConstFloat32 (app_unop_f fop c))]⦈"
| unop_f64:"⦇[$C (ConstFloat64 c), $(Unop_f T_f64 fop)]⦈ ↝ ⦇[$C (ConstFloat64 (app_unop_f fop c))]⦈"
  ― ‹‹int32 binary ops››
| binop_i32_Some:"⟦app_binop_i iop c1 c2 = (Some c)⟧ ⟹ ⦇[$C (ConstInt32 c1), $C (ConstInt32 c2), $(Binop_i T_i32 iop)]⦈ ↝ ⦇[$C (ConstInt32 c)]⦈"
| binop_i32_None:"⟦app_binop_i iop c1 c2 = None⟧ ⟹ ⦇[$C (ConstInt32 c1), $C (ConstInt32 c2), $(Binop_i T_i32 iop)]⦈ ↝ ⦇[Trap]⦈"
  ― ‹‹int64 binary ops››
| binop_i64_Some:"⟦app_binop_i iop c1 c2 = (Some c)⟧ ⟹ ⦇[$C (ConstInt64 c1), $C (ConstInt64 c2), $(Binop_i T_i64 iop)]⦈ ↝ ⦇[$C (ConstInt64 c)]⦈"
| binop_i64_None:"⟦app_binop_i iop c1 c2 = None⟧ ⟹ ⦇[$C (ConstInt64 c1), $C (ConstInt64 c2), $(Binop_i T_i64 iop)]⦈ ↝ ⦇[Trap]⦈"
  ― ‹‹float32 binary ops››
| binop_f32_Some:"⟦app_binop_f fop c1 c2 = (Some c)⟧ ⟹ ⦇[$C (ConstFloat32 c1), $C (ConstFloat32 c2), $(Binop_f T_f32 fop)]⦈ ↝ ⦇[$C (ConstFloat32 c)]⦈"
| binop_f32_None:"⟦app_binop_f fop c1 c2 = None⟧ ⟹ ⦇[$C (ConstFloat32 c1), $C (ConstFloat32 c2), $(Binop_f T_f32 fop)]⦈ ↝ ⦇[Trap]⦈"
  ― ‹‹float64 binary ops››
| binop_f64_Some:"⟦app_binop_f fop c1 c2 = (Some c)⟧ ⟹ ⦇[$C (ConstFloat64 c1), $C (ConstFloat64 c2), $(Binop_f T_f64 fop)]⦈ ↝ ⦇[$C (ConstFloat64 c)]⦈"
| binop_f64_None:"⟦app_binop_f fop c1 c2 = None⟧ ⟹ ⦇[$C (ConstFloat64 c1), $C (ConstFloat64 c2), $(Binop_f T_f64 fop)]⦈ ↝ ⦇[Trap]⦈"
  ― ‹‹testops››
| testop_i32:"⦇[$C (ConstInt32 c), $(Testop T_i32 testop)]⦈ ↝ ⦇[$C ConstInt32 (wasm_bool (app_testop_i testop c))]⦈"
| testop_i64:"⦇[$C (ConstInt64 c), $(Testop T_i64 testop)]⦈ ↝ ⦇[$C ConstInt32 (wasm_bool (app_testop_i testop c))]⦈"
  ― ‹‹int relops››
| relop_i32:"⦇[$C (ConstInt32 c1), $C (ConstInt32 c2), $(Relop_i T_i32 iop)]⦈ ↝ ⦇[$C (ConstInt32 (wasm_bool (app_relop_i iop c1 c2)))]⦈"
| relop_i64:"⦇[$C (ConstInt64 c1), $C (ConstInt64 c2), $(Relop_i T_i64 iop)]⦈ ↝ ⦇[$C (ConstInt32 (wasm_bool (app_relop_i iop c1 c2)))]⦈"
  ― ‹‹float relops››
| relop_f32:"⦇[$C (ConstFloat32 c1), $C (ConstFloat32 c2), $(Relop_f T_f32 fop)]⦈ ↝ ⦇[$C (ConstInt32 (wasm_bool (app_relop_f fop c1 c2)))]⦈"
| relop_f64:"⦇[$C (ConstFloat64 c1), $C (ConstFloat64 c2), $(Relop_f T_f64 fop)]⦈ ↝ ⦇[$C (ConstInt32 (wasm_bool (app_relop_f fop c1 c2)))]⦈"
  ― ‹‹convert››
| convert_Some:"⟦types_agree t1 v; cvt t2 sx v = (Some v')⟧ ⟹ ⦇[$(C v), $(Cvtop t2 Convert t1 sx)]⦈ ↝ ⦇[$(C v')]⦈"
| convert_None:"⟦types_agree t1 v; cvt t2 sx v = None⟧ ⟹ ⦇[$(C v), $(Cvtop t2 Convert t1 sx)]⦈ ↝ ⦇[Trap]⦈"
  ― ‹‹reinterpret››
| reinterpret:"types_agree t1 v ⟹ ⦇[$(C v), $(Cvtop t2 Reinterpret t1 None)]⦈ ↝ ⦇[$(C (wasm_deserialise (bits v) t2))]⦈"
  ― ‹‹unreachable››
| unreachable:"⦇[$ Unreachable]⦈ ↝ ⦇[Trap]⦈"
  ― ‹‹nop››
| nop:"⦇[$ Nop]⦈ ↝ ⦇[]⦈"
  ― ‹‹drop››
| drop:"⦇[$(C v), ($ Drop)]⦈ ↝ ⦇[]⦈"
  ― ‹‹select››
| select_false:"int_eq n 0 ⟹ ⦇[$(C v1), $(C v2), $C (ConstInt32 n), ($ Select)]⦈ ↝ ⦇[$(C v2)]⦈"
| select_true:"int_ne n 0 ⟹ ⦇[$(C v1), $(C v2), $C (ConstInt32 n), ($ Select)]⦈ ↝ ⦇[$(C v1)]⦈"
  ― ‹‹block››
| block:"⟦const_list vs; length vs = n; length t1s = n; length t2s = m⟧ ⟹ ⦇vs @ [$(Block (t1s _> t2s) es)]⦈ ↝ ⦇[Label m [] (vs @ ($* es))]⦈"
  ― ‹‹loop››
| loop:"⟦const_list vs; length vs = n; length t1s = n; length t2s = m⟧ ⟹ ⦇vs @ [$(Loop (t1s _> t2s) es)]⦈ ↝ ⦇[Label n [$(Loop (t1s _> t2s) es)] (vs @ ($* es))]⦈"
  ― ‹‹if››
| if_false:"int_eq n 0 ⟹ ⦇[$C (ConstInt32 n), $(If tf e1s e2s)]⦈ ↝ ⦇[$(Block tf e2s)]⦈"
| if_true:"int_ne n 0 ⟹ ⦇[$C (ConstInt32 n), $(If tf e1s e2s)]⦈ ↝ ⦇[$(Block tf e1s)]⦈"
  ― ‹‹label››
| label_const:"const_list vs ⟹ ⦇[Label n es vs]⦈ ↝ ⦇vs⦈"
| label_trap:"⦇[Label n es [Trap]]⦈ ↝ ⦇[Trap]⦈"
  ― ‹‹br››
| br:"⟦const_list vs; length vs = n; Lfilled i lholed (vs @ [$(Br i)]) LI⟧ ⟹ ⦇[Label n es LI]⦈ ↝ ⦇vs @ es⦈"
  ― ‹‹br_if››
| br_if_false:"int_eq n 0 ⟹ ⦇[$C (ConstInt32 n), $(Br_if i)]⦈ ↝ ⦇[]⦈"
| br_if_true:"int_ne n 0 ⟹ ⦇[$C (ConstInt32 n), $(Br_if i)]⦈ ↝ ⦇[$(Br i)]⦈"
  ― ‹‹br_table››
| br_table:"⟦length is > (nat_of_int c)⟧ ⟹ ⦇[$C (ConstInt32 c), $(Br_table is i)]⦈ ↝ ⦇[$(Br (is!(nat_of_int c)))]⦈"
| br_table_length:"⟦length is ≤ (nat_of_int c)⟧ ⟹ ⦇[$C (ConstInt32 c), $(Br_table is i)]⦈ ↝ ⦇[$(Br i)]⦈"
  ― ‹‹local››
| local_const:"⟦const_list es; length es = n⟧ ⟹ ⦇[Local n i vs es]⦈ ↝ ⦇es⦈"
| local_trap:"⦇[Local n i vs [Trap]]⦈ ↝ ⦇[Trap]⦈"
  ― ‹‹return››
| return:"⟦const_list vs; length vs = n; Lfilled j lholed (vs @ [$Return]) es⟧  ⟹ ⦇[Local n i vls es]⦈ ↝ ⦇vs⦈"
  ― ‹‹tee_local››
| tee_local:"is_const v ⟹ ⦇[v, $(Tee_local i)]⦈ ↝ ⦇[v, v, $(Set_local i)]⦈"
| trap:"⟦es ≠ [Trap]; Lfilled 0 lholed [Trap] es⟧ ⟹ ⦇es⦈ ↝ ⦇[Trap]⦈"

(* full reduction rule *)
inductive reduce :: "[s, v list, e list, nat, s, v list, e list] ⇒ bool" ("⦇_;_;_⦈ ↝'_ _ ⦇_;_;_⦈" 60) where
  ― ‹‹lifting basic reduction››
  basic:"⦇e⦈ ↝ ⦇e'⦈ ⟹ ⦇s;vs;e⦈ ↝_i ⦇s;vs;e'⦈"
  ― ‹‹call››
| call:"⦇s;vs;[$(Call j)]⦈ ↝_i ⦇s;vs;[Callcl (sfunc s i j)]⦈"
  ― ‹‹call_indirect››
| call_indirect_Some:"⟦stab s i (nat_of_int c) = Some cl; stypes s i j = tf; cl_type cl = tf⟧ ⟹ ⦇s;vs;[$C (ConstInt32 c), $(Call_indirect j)]⦈ ↝_i ⦇s;vs;[Callcl cl]⦈"
| call_indirect_None:"⟦(stab s i (nat_of_int c) = Some cl ∧ stypes s i j ≠ cl_type cl) ∨ stab s i (nat_of_int c) = None⟧ ⟹ ⦇s;vs;[$C (ConstInt32 c), $(Call_indirect j)]⦈ ↝_i ⦇s;vs;[Trap]⦈"
  ― ‹‹call››
| callcl_native:"⟦cl = Func_native j (t1s _> t2s) ts es; ves = ($$* vcs); length vcs = n; length ts = k; length t1s = n; length t2s = m; (n_zeros ts = zs) ⟧ ⟹ ⦇s;vs;ves @ [Callcl cl]⦈ ↝_i ⦇s;vs;[Local m j (vcs@zs) [$(Block ([] _> t2s) es)]]⦈"
| callcl_host_Some:"⟦cl = Func_host (t1s _> t2s) f; ves = ($$* vcs); length vcs = n; length t1s = n; length t2s = m; host_apply s (t1s _> t2s) f vcs hs = Some (s', vcs')⟧ ⟹ ⦇s;vs;ves @ [Callcl cl]⦈ ↝_i ⦇s';vs;($$* vcs')⦈"
| callcl_host_None:"⟦cl = Func_host (t1s _> t2s) f; ves = ($$* vcs); length vcs = n; length t1s = n; length t2s = m⟧ ⟹ ⦇s;vs;ves @ [Callcl cl]⦈ ↝_i ⦇s;vs;[Trap]⦈"
  ― ‹‹get_local››
| get_local:"⟦length vi = j⟧ ⟹ ⦇s;(vi @ [v] @ vs);[$(Get_local j)]⦈ ↝_i ⦇s;(vi @ [v] @ vs);[$(C v)]⦈"
  ― ‹‹set_local››
| set_local:"⟦length vi = j⟧ ⟹ ⦇s;(vi @ [v] @ vs);[$(C v'), $(Set_local j)]⦈ ↝_i ⦇s;(vi @ [v'] @ vs);[]⦈"
  ― ‹‹get_global››
| get_global:"⦇s;vs;[$(Get_global j)]⦈ ↝_i ⦇s;vs;[$ C(sglob_val s i j)]⦈"
  ― ‹‹set_global››
| set_global:"supdate_glob s i j v = s' ⟹ ⦇s;vs;[$(C v), $(Set_global j)]⦈ ↝_i ⦇s';vs;[]⦈"
  ― ‹‹load››
| load_Some:"⟦smem_ind s i = Some j; ((mem s)!j) = m; load m (nat_of_int k) off (t_length t) = Some bs⟧ ⟹ ⦇s;vs;[$C (ConstInt32 k), $(Load t None a off)]⦈ ↝_i ⦇s;vs;[$C (wasm_deserialise bs t)]⦈"
| load_None:"⟦smem_ind s i = Some j; ((mem s)!j) = m; load m (nat_of_int k) off (t_length t) = None⟧ ⟹ ⦇s;vs;[$C (ConstInt32 k), $(Load t None a off)]⦈ ↝_i ⦇s;vs;[Trap]⦈"
  ― ‹‹load packed››
| load_packed_Some:"⟦smem_ind s i = Some j; ((mem s)!j) = m; load_packed sx m (nat_of_int k) off (tp_length tp) (t_length t) = Some bs⟧ ⟹ ⦇s;vs;[$C (ConstInt32 k), $(Load t (Some (tp, sx)) a off)]⦈ ↝_i ⦇s;vs;[$C (wasm_deserialise bs t)]⦈"
| load_packed_None:"⟦smem_ind s i = Some j; ((mem s)!j) = m; load_packed sx m (nat_of_int k) off (tp_length tp) (t_length t) = None⟧ ⟹ ⦇s;vs;[$C (ConstInt32 k), $(Load t (Some (tp, sx)) a off)]⦈ ↝_i ⦇s;vs;[Trap]⦈"
  ― ‹‹store››
| store_Some:"⟦types_agree t v; smem_ind s i = Some j; ((mem s)!j) = m; store m (nat_of_int k) off (bits v) (t_length t) = Some mem'⟧ ⟹ ⦇s;vs;[$C (ConstInt32 k), $C v, $(Store t None a off)]⦈ ↝_i ⦇s⦇mem:= ((mem s)[j := mem'])⦈;vs;[]⦈"
| store_None:"⟦types_agree t v; smem_ind s i = Some j; ((mem s)!j) = m; store m (nat_of_int k) off (bits v) (t_length t) = None⟧ ⟹ ⦇s;vs;[$C (ConstInt32 k), $C v, $(Store t None a off)]⦈ ↝_i ⦇s;vs;[Trap]⦈"
  ― ‹‹store packed›› (* take only (tp_length tp) lower order bytes *)
| store_packed_Some:"⟦types_agree t v; smem_ind s i = Some j; ((mem s)!j) = m; store_packed m (nat_of_int k) off (bits v) (tp_length tp) = Some mem'⟧ ⟹ ⦇s;vs;[$C (ConstInt32 k), $C v, $(Store t (Some tp) a off)]⦈ ↝_i ⦇s⦇mem:= ((mem s)[j := mem'])⦈;vs;[]⦈"
| store_packed_None:"⟦types_agree t v; smem_ind s i = Some j; ((mem s)!j) = m; store_packed m (nat_of_int k) off (bits v) (tp_length tp) = None⟧ ⟹ ⦇s;vs;[$C (ConstInt32 k), $C v, $(Store t (Some tp) a off)]⦈ ↝_i ⦇s;vs;[Trap]⦈"
  ― ‹‹current_memory››
| current_memory:"⟦smem_ind s i = Some j; ((mem s)!j) = m; mem_size m = n⟧ ⟹ ⦇s;vs;[ $(Current_memory)]⦈ ↝_i ⦇s;vs;[$C (ConstInt32 (int_of_nat n))]⦈"
  ― ‹‹grow_memory››
| grow_memory:"⟦smem_ind s i = Some j; ((mem s)!j) = m; mem_size m = n; mem_grow m (nat_of_int c) = mem'⟧ ⟹ ⦇s;vs;[$C (ConstInt32 c), $(Grow_memory)]⦈ ↝_i ⦇s⦇mem:= ((mem s)[j := mem'])⦈;vs;[$C (ConstInt32 (int_of_nat n))]⦈"
  ― ‹‹grow_memory fail››
| grow_memory_fail:"⟦smem_ind s i = Some j; ((mem s)!j) = m; mem_size m = n⟧ ⟹ ⦇s;vs;[$C (ConstInt32 c),$(Grow_memory)]⦈ ↝_i ⦇s;vs;[$C (ConstInt32 int32_minus_one)]⦈"
  (* The bad ones. *)
  ― ‹‹inductive label reduction››
| label:"⟦⦇s;vs;es⦈ ↝_i ⦇s';vs';es'⦈; Lfilled k lholed es les; Lfilled k lholed es' les'⟧ ⟹ ⦇s;vs;les⦈ ↝_i ⦇s';vs';les'⦈"
  ― ‹‹inductive local reduction››
| local:"⟦⦇s;vs;es⦈ ↝_i ⦇s';vs';es'⦈⟧ ⟹ ⦇s;v0s;[Local n i vs es]⦈ ↝_j ⦇s';v0s;[Local n i vs' es']⦈"

end