October 2026 main drop: mirror from GitHub

f5deffb verified 19 days ago

10.5 kB

/-!
# Wasm.Isa

A model of the WebAssembly subset the backend emits, following the WebAssembly core
specification:

* typed operand stack (`i32` / `i64`), mutable globals, linear memory, a function table;
* `i64.load`/`i64.store` on **bytes** (little-endian), taking an `i32` address plus a static offset
  computed in unbounded arithmetic; an access with any byte outside the memory traps. There is no
  aliasing assumption: overlapping accesses are modelled exactly;
* `i64.div_s` traps on division by zero and on `INT64_MIN / -1`; `i64.div_u` traps on division by
  zero; shifts and rotates take the count modulo 64 (the spec's definition);
* `if` (without `else`) and `loop`/`br` with the spec's label discipline, including unwinding the
  operand stack to the label height on a branch; `call_indirect` through the function table (a
  callee runs on a fresh operand stack and returns the single value it leaves).

Two host calls are terminal pseudo-instructions: `exitTrap c` (`i32.const c; call $proc_exit`) and
`exitHalt` (`global.get sp; call $halt`, which dumps the machine state and exits 0).

Semantics is a big-step relation, so loops need no fuel. That the model matches a real
WebAssembly engine is an assumption, tested by differential execution (`wasmw`).
-/

namespace WordDialect
namespace Wasm

abbrev W := BitVec 64
abbrev W32 := BitVec 32

inductive Val where
  | i32 (v : W32)
  | i64 (v : W)
  deriving DecidableEq

/-- Little-endian read of `n` bytes starting at `a` (each byte taken modulo 256). -/
def rdBytes (b : Nat → Nat) (a : Nat) : Nat → Nat
  | 0 => 0
  | n + 1 => rdBytes b a n + (b (a + n) % 256) * 256 ^ n

structure WMem where
  bytes : Nat → Nat
  size : Nat

def WMem.read64 (m : WMem) (a : Nat) : Option W :=
  if a + 8 ≤ m.size then some (BitVec.ofNat 64 (rdBytes m.bytes a 8)) else none

def WMem.write64 (m : WMem) (a : Nat) (v : W) : Option WMem :=
  if a + 8 ≤ m.size then
    some { m with bytes := fun p => if a ≤ p ∧ p < a + 8 then (v.toNat / 256 ^ (p - a)) % 256 else m.bytes p }
  else none

structure WState where
  stack : List Val
  globals : Nat → Val
  mem : WMem

inductive WI where
  | i32const (v : W32)
  | i64const (v : W)
  | globalGet (i : Nat)
  | globalSet (i : Nat)
  | i64load (off : Nat)
  | i64store (off : Nat)
  | i64add | i64sub | i64mul | i64and | i64or | i64xor
  | i64shl | i64shru | i64rotl | i64rotr | i64divu | i64divs
  | i64eq | i64ne | i64ltu | i64leu | i64gtu | i64geu | i64lts | i64les | i64gts | i64ges
  | i64eqz
  | i32add | i32sub | i32shl | i32gtu | i32eq
  | i32wrap
  | i64extu
  | select
  | loop (body : List WI)
  | ite (thn : List WI)
  | br (l : Nat)
  | callIndirect
  | exitTrap (code : Nat)
  | exitHalt

/-- Control constructs, calls and terminal pseudo-instructions (handled by `RunI`, not `stepI`). -/
def WI.isCtl : WI → Bool
  | .loop _ | .ite _ | .br _ | .callIndirect | .exitTrap _ | .exitHalt => true
  | _ => false

def bool32 (b : Bool) : W32 := if b then 1#32 else 0#32

def bin64 (f : W → W → W) (s : WState) : Option WState :=
  match s.stack with
  | .i64 b :: .i64 a :: r => some { s with stack := .i64 (f a b) :: r }
  | _ => none

def cmp64 (f : W → W → Bool) (s : WState) : Option WState :=
  match s.stack with
  | .i64 b :: .i64 a :: r => some { s with stack := .i32 (bool32 (f a b)) :: r }
  | _ => none

def bin32 (f : W32 → W32 → W32) (s : WState) : Option WState :=
  match s.stack with
  | .i32 b :: .i32 a :: r => some { s with stack := .i32 (f a b) :: r }
  | _ => none

/-- One non-control instruction; `none` is a trap. -/
def stepI : WI → WState → Option WState
  | .i32const v, s => some { s with stack := .i32 v :: s.stack }
  | .i64const v, s => some { s with stack := .i64 v :: s.stack }
  | .globalGet i, s => some { s with stack := s.globals i :: s.stack }
  | .globalSet i, s =>
    match s.stack with
    | v :: r => some { s with stack := r, globals := fun j => if j = i then v else s.globals j }
    | _ => none
  | .i64load off, s =>
    match s.stack with
    | .i32 a :: r =>
      match s.mem.read64 (a.toNat + off) with
      | some v => some { s with stack := .i64 v :: r }
      | none => none
    | _ => none
  | .i64store off, s =>
    match s.stack with
    | .i64 v :: .i32 a :: r =>
      match s.mem.write64 (a.toNat + off) v with
      | some m => some { s with stack := r, mem := m }
      | none => none
    | _ => none
  | .i64add, s => bin64 (· + ·) s
  | .i64sub, s => bin64 (· - ·) s
  | .i64mul, s => bin64 (· * ·) s
  | .i64and, s => bin64 (· &&& ·) s
  | .i64or, s => bin64 (· ||| ·) s
  | .i64xor, s => bin64 (· ^^^ ·) s
  | .i64shl, s => bin64 (fun a b => a <<< (b.toNat % 64)) s
  | .i64shru, s => bin64 (fun a b => a >>> (b.toNat % 64)) s
  | .i64rotl, s => bin64 (fun a b => a.rotateLeft (b.toNat % 64)) s
  | .i64rotr, s => bin64 (fun a b => a.rotateRight (b.toNat % 64)) s
  | .i64divu, s =>
    match s.stack with
    | .i64 b :: .i64 a :: r =>
      if b = 0#64 then none
      else some { s with stack := .i64 (BitVec.ofNat 64 (a.toNat / b.toNat)) :: r }
    | _ => none
  | .i64divs, s =>
    match s.stack with
    | .i64 b :: .i64 a :: r =>
      if b = 0#64 ∨ (a = BitVec.intMin 64 ∧ b = BitVec.allOnes 64) then none
      else some { s with stack := .i64 (BitVec.ofInt 64 (Int.tdiv a.toInt b.toInt)) :: r }
    | _ => none
  | .i64eq, s => cmp64 (fun a b => a == b) s
  | .i64ne, s => cmp64 (fun a b => a != b) s
  | .i64ltu, s => cmp64 (fun a b => a.ult b) s
  | .i64leu, s => cmp64 (fun a b => a.ule b) s
  | .i64gtu, s => cmp64 (fun a b => b.ult a) s
  | .i64geu, s => cmp64 (fun a b => b.ule a) s
  | .i64lts, s => cmp64 (fun a b => a.slt b) s
  | .i64les, s => cmp64 (fun a b => a.sle b) s
  | .i64gts, s => cmp64 (fun a b => b.slt a) s
  | .i64ges, s => cmp64 (fun a b => b.sle a) s
  | .i64eqz, s =>
    match s.stack with
    | .i64 a :: r => some { s with stack := .i32 (bool32 (a == 0#64)) :: r }
    | _ => none
  | .i32add, s => bin32 (· + ·) s
  | .i32sub, s => bin32 (· - ·) s
  | .i32shl, s => bin32 (fun a b => a <<< (b.toNat % 32)) s
  | .i32gtu, s =>
    match s.stack with
    | .i32 b :: .i32 a :: r => some { s with stack := .i32 (bool32 (b.ult a)) :: r }
    | _ => none
  | .i32eq, s =>
    match s.stack with
    | .i32 b :: .i32 a :: r => some { s with stack := .i32 (bool32 (a == b)) :: r }
    | _ => none
  | .i32wrap, s =>
    match s.stack with
    | .i64 a :: r => some { s with stack := .i32 (BitVec.ofNat 32 a.toNat) :: r }
    | _ => none
  | .i64extu, s =>
    match s.stack with
    | .i32 a :: r => some { s with stack := .i64 (BitVec.ofNat 64 a.toNat) :: r }
    | _ => none
  | .select, s =>
    match s.stack with
    | .i32 c :: v2 :: v1 :: r => some { s with stack := (if c ≠ 0#32 then v1 else v2) :: r }
    | _ => none
  | _, _ => none

/-- Outcomes of running a list of instructions. -/
inductive Res where
  | normal (s : WState)
  | br (n : Nat) (s : WState)
  | exit (code : Nat)
  | halted (s : WState)
  | fault

/-- Leaving a labelled construct entered with operand stack `entry`: a branch to label 0 is
consumed (for `if`; `loop` re-enters) and the operand stack is unwound to its height at entry;
other branches propagate outward. -/
inductive BlockOut (entry : List Val) : Res → Res → Prop where
  | norm {s} : BlockOut entry (.normal s) (.normal s)
  | br0 {s} : BlockOut entry (.br 0 s) (.normal { s with stack := entry })
  | brS {n s} : BlockOut entry (.br (n + 1) s) (.br n s)
  | exit {c} : BlockOut entry (.exit c) (.exit c)
  | halted {s} : BlockOut entry (.halted s) (.halted s)
  | fault : BlockOut entry .fault .fault

/-- Results that abandon the rest of an instruction sequence. -/
def Res.abrupt : Res → Prop
  | .normal _ => False
  | _ => True

/-- A function table: entry `i` is the body of function `i`. -/
abbrev Funcs := List (List WI)

mutual
inductive RunI (fs : Funcs) : WI → WState → Res → Prop where
  | simple {i s s'} : i.isCtl = false → stepI i s = some s' → RunI fs i s (.normal s')
  | simpleFault {i s} : i.isCtl = false → stepI i s = none → RunI fs i s .fault
  | loopNormal {body s s'} : Run fs body s (.normal s') → RunI fs (.loop body) s (.normal s')
  | loopBr0 {body s s' r} :
      Run fs body s (.br 0 s') → RunI fs (.loop body) { s' with stack := s.stack } r →
      RunI fs (.loop body) s r
  | loopBrS {body s n s'} : Run fs body s (.br (n + 1) s') → RunI fs (.loop body) s (.br n s')
  | loopExit {body s c} : Run fs body s (.exit c) → RunI fs (.loop body) s (.exit c)
  | loopHalted {body s s'} : Run fs body s (.halted s') → RunI fs (.loop body) s (.halted s')
  | loopFault {body s} : Run fs body s .fault → RunI fs (.loop body) s .fault
  | iteThen {thn s r c res res'} :
      s.stack = .i32 c :: r → c ≠ 0#32 → Run fs thn { s with stack := r } res →
      BlockOut r res res' → RunI fs (.ite thn) s res'
  | iteElse {thn s r c} :
      s.stack = .i32 c :: r → c = 0#32 → RunI fs (.ite thn) s (.normal { s with stack := r })
  | iteFault {thn s} : (∀ c r, s.stack ≠ .i32 c :: r) → RunI fs (.ite thn) s .fault
  | br {l s} : RunI fs (.br l) s (.br l s)
  | callNormal {s r i body s' v} :
      s.stack = .i32 i :: r → fs[i.toNat]? = some body →
      Run fs body { s with stack := [] } (.normal s') → s'.stack = [.i32 v] →
      RunI fs .callIndirect s (.normal { s' with stack := .i32 v :: r })
  | callBad {s r i body s'} :
      s.stack = .i32 i :: r → fs[i.toNat]? = some body →
      Run fs body { s with stack := [] } (.normal s') → (∀ v, s'.stack ≠ [.i32 v]) →
      RunI fs .callIndirect s .fault
  | callAbrupt {s r i body res} :
      s.stack = .i32 i :: r → fs[i.toNat]? = some body →
      Run fs body { s with stack := [] } res → res.abrupt →
      RunI fs .callIndirect s (match res with | .br _ _ => .fault | other => other)
  | callMissing {s r i} :
      s.stack = .i32 i :: r → fs[i.toNat]? = none → RunI fs .callIndirect s .fault
  | callBadStack {s} : (∀ i r, s.stack ≠ .i32 i :: r) → RunI fs .callIndirect s .fault
  | exitTrap {c s} : RunI fs (.exitTrap c) s (.exit c)
  | exitHalt {s} : RunI fs .exitHalt s (.halted s)

inductive Run (fs : Funcs) : List WI → WState → Res → Prop where
  | nil {s} : Run fs [] s (.normal s)
  | consNormal {i is s s' r} : RunI fs i s (.normal s') → Run fs is s' r → Run fs (i :: is) s r
  | consAbrupt {i is s r} : RunI fs i s r → r.abrupt → Run fs (i :: is) s r
end

end Wasm
end WordDialect

	/-!
	# Wasm.Isa

	A model of the WebAssembly subset the backend emits, following the WebAssembly core
	specification:

	* typed operand stack (`i32` / `i64`), mutable globals, linear memory, a function table;
	* `i64.load`/`i64.store` on bytes (little-endian), taking an `i32` address plus a static offset
	computed in unbounded arithmetic; an access with any byte outside the memory traps. There is no
	aliasing assumption: overlapping accesses are modelled exactly;
	* `i64.div_s` traps on division by zero and on `INT64_MIN / -1`; `i64.div_u` traps on division by
	zero; shifts and rotates take the count modulo 64 (the spec's definition);
	* `if` (without `else`) and `loop`/`br` with the spec's label discipline, including unwinding the
	operand stack to the label height on a branch; `call_indirect` through the function table (a
	callee runs on a fresh operand stack and returns the single value it leaves).

	Two host calls are terminal pseudo-instructions: `exitTrap c` (`i32.const c; call $proc_exit`) and
	`exitHalt` (`global.get sp; call $halt`, which dumps the machine state and exits 0).

	Semantics is a big-step relation, so loops need no fuel. That the model matches a real
	WebAssembly engine is an assumption, tested by differential execution (`wasmw`).
	-/

	namespace WordDialect
	namespace Wasm

	abbrev W := BitVec 64
	abbrev W32 := BitVec 32

	inductive Val where
	\| i32 (v : W32)
	\| i64 (v : W)
	deriving DecidableEq

	/-- Little-endian read of `n` bytes starting at `a` (each byte taken modulo 256). -/
	def rdBytes (b : Nat → Nat) (a : Nat) : Nat → Nat
	\| 0 => 0
	\| n + 1 => rdBytes b a n + (b (a + n) % 256) * 256 ^ n

	structure WMem where
	bytes : Nat → Nat
	size : Nat

	def WMem.read64 (m : WMem) (a : Nat) : Option W :=
	if a + 8 ≤ m.size then some (BitVec.ofNat 64 (rdBytes m.bytes a 8)) else none

	def WMem.write64 (m : WMem) (a : Nat) (v : W) : Option WMem :=
	if a + 8 ≤ m.size then
	some { m with bytes := fun p => if a ≤ p ∧ p < a + 8 then (v.toNat / 256 ^ (p - a)) % 256 else m.bytes p }
	else none

	structure WState where
	stack : List Val
	globals : Nat → Val
	mem : WMem

	inductive WI where
	\| i32const (v : W32)
	\| i64const (v : W)
	\| globalGet (i : Nat)
	\| globalSet (i : Nat)
	\| i64load (off : Nat)
	\| i64store (off : Nat)
	\| i64add \| i64sub \| i64mul \| i64and \| i64or \| i64xor
	\| i64shl \| i64shru \| i64rotl \| i64rotr \| i64divu \| i64divs
	\| i64eq \| i64ne \| i64ltu \| i64leu \| i64gtu \| i64geu \| i64lts \| i64les \| i64gts \| i64ges
	\| i64eqz
	\| i32add \| i32sub \| i32shl \| i32gtu \| i32eq
	\| i32wrap
	\| i64extu
	\| select
	\| loop (body : List WI)
	\| ite (thn : List WI)
	\| br (l : Nat)
	\| callIndirect
	\| exitTrap (code : Nat)
	\| exitHalt

	/-- Control constructs, calls and terminal pseudo-instructions (handled by `RunI`, not `stepI`). -/
	def WI.isCtl : WI → Bool
	\| .loop _ \| .ite _ \| .br _ \| .callIndirect \| .exitTrap _ \| .exitHalt => true
	\| _ => false

	def bool32 (b : Bool) : W32 := if b then 1#32 else 0#32

	def bin64 (f : W → W → W) (s : WState) : Option WState :=
	match s.stack with
	\| .i64 b :: .i64 a :: r => some { s with stack := .i64 (f a b) :: r }
	\| _ => none

	def cmp64 (f : W → W → Bool) (s : WState) : Option WState :=
	match s.stack with
	\| .i64 b :: .i64 a :: r => some { s with stack := .i32 (bool32 (f a b)) :: r }
	\| _ => none

	def bin32 (f : W32 → W32 → W32) (s : WState) : Option WState :=
	match s.stack with
	\| .i32 b :: .i32 a :: r => some { s with stack := .i32 (f a b) :: r }
	\| _ => none

	/-- One non-control instruction; `none` is a trap. -/
	def stepI : WI → WState → Option WState
	\| .i32const v, s => some { s with stack := .i32 v :: s.stack }
	\| .i64const v, s => some { s with stack := .i64 v :: s.stack }
	\| .globalGet i, s => some { s with stack := s.globals i :: s.stack }
	\| .globalSet i, s =>
	match s.stack with
	\| v :: r => some { s with stack := r, globals := fun j => if j = i then v else s.globals j }
	\| _ => none
	\| .i64load off, s =>
	match s.stack with
	\| .i32 a :: r =>
	match s.mem.read64 (a.toNat + off) with
	\| some v => some { s with stack := .i64 v :: r }
	\| none => none
	\| _ => none
	\| .i64store off, s =>
	match s.stack with
	\| .i64 v :: .i32 a :: r =>
	match s.mem.write64 (a.toNat + off) v with
	\| some m => some { s with stack := r, mem := m }
	\| none => none
	\| _ => none
	\| .i64add, s => bin64 (· + ·) s
	\| .i64sub, s => bin64 (· - ·) s
	\| .i64mul, s => bin64 (· * ·) s
	\| .i64and, s => bin64 (· &&& ·) s
	\| .i64or, s => bin64 (· \|\|\| ·) s
	\| .i64xor, s => bin64 (· ^^^ ·) s
	\| .i64shl, s => bin64 (fun a b => a <<< (b.toNat % 64)) s
	\| .i64shru, s => bin64 (fun a b => a >>> (b.toNat % 64)) s
	\| .i64rotl, s => bin64 (fun a b => a.rotateLeft (b.toNat % 64)) s
	\| .i64rotr, s => bin64 (fun a b => a.rotateRight (b.toNat % 64)) s
	\| .i64divu, s =>
	match s.stack with
	\| .i64 b :: .i64 a :: r =>
	if b = 0#64 then none
	else some { s with stack := .i64 (BitVec.ofNat 64 (a.toNat / b.toNat)) :: r }
	\| _ => none
	\| .i64divs, s =>
	match s.stack with
	\| .i64 b :: .i64 a :: r =>
	if b = 0#64 ∨ (a = BitVec.intMin 64 ∧ b = BitVec.allOnes 64) then none
	else some { s with stack := .i64 (BitVec.ofInt 64 (Int.tdiv a.toInt b.toInt)) :: r }
	\| _ => none
	\| .i64eq, s => cmp64 (fun a b => a == b) s
	\| .i64ne, s => cmp64 (fun a b => a != b) s
	\| .i64ltu, s => cmp64 (fun a b => a.ult b) s
	\| .i64leu, s => cmp64 (fun a b => a.ule b) s
	\| .i64gtu, s => cmp64 (fun a b => b.ult a) s
	\| .i64geu, s => cmp64 (fun a b => b.ule a) s
	\| .i64lts, s => cmp64 (fun a b => a.slt b) s
	\| .i64les, s => cmp64 (fun a b => a.sle b) s
	\| .i64gts, s => cmp64 (fun a b => b.slt a) s
	\| .i64ges, s => cmp64 (fun a b => b.sle a) s
	\| .i64eqz, s =>
	match s.stack with
	\| .i64 a :: r => some { s with stack := .i32 (bool32 (a == 0#64)) :: r }
	\| _ => none
	\| .i32add, s => bin32 (· + ·) s
	\| .i32sub, s => bin32 (· - ·) s
	\| .i32shl, s => bin32 (fun a b => a <<< (b.toNat % 32)) s
	\| .i32gtu, s =>
	match s.stack with
	\| .i32 b :: .i32 a :: r => some { s with stack := .i32 (bool32 (b.ult a)) :: r }
	\| _ => none
	\| .i32eq, s =>
	match s.stack with
	\| .i32 b :: .i32 a :: r => some { s with stack := .i32 (bool32 (a == b)) :: r }
	\| _ => none
	\| .i32wrap, s =>
	match s.stack with
	\| .i64 a :: r => some { s with stack := .i32 (BitVec.ofNat 32 a.toNat) :: r }
	\| _ => none
	\| .i64extu, s =>
	match s.stack with
	\| .i32 a :: r => some { s with stack := .i64 (BitVec.ofNat 64 a.toNat) :: r }
	\| _ => none
	\| .select, s =>
	match s.stack with
	\| .i32 c :: v2 :: v1 :: r => some { s with stack := (if c ≠ 0#32 then v1 else v2) :: r }
	\| _ => none
	\| _, _ => none

	/-- Outcomes of running a list of instructions. -/
	inductive Res where
	\| normal (s : WState)
	\| br (n : Nat) (s : WState)
	\| exit (code : Nat)
	\| halted (s : WState)
	\| fault

	/-- Leaving a labelled construct entered with operand stack `entry`: a branch to label 0 is
	consumed (for `if`; `loop` re-enters) and the operand stack is unwound to its height at entry;
	other branches propagate outward. -/
	inductive BlockOut (entry : List Val) : Res → Res → Prop where
	\| norm {s} : BlockOut entry (.normal s) (.normal s)
	\| br0 {s} : BlockOut entry (.br 0 s) (.normal { s with stack := entry })
	\| brS {n s} : BlockOut entry (.br (n + 1) s) (.br n s)
	\| exit {c} : BlockOut entry (.exit c) (.exit c)
	\| halted {s} : BlockOut entry (.halted s) (.halted s)
	\| fault : BlockOut entry .fault .fault

	/-- Results that abandon the rest of an instruction sequence. -/
	def Res.abrupt : Res → Prop
	\| .normal _ => False
	\| _ => True

	/-- A function table: entry `i` is the body of function `i`. -/
	abbrev Funcs := List (List WI)

	mutual
	inductive RunI (fs : Funcs) : WI → WState → Res → Prop where
	\| simple {i s s'} : i.isCtl = false → stepI i s = some s' → RunI fs i s (.normal s')
	\| simpleFault {i s} : i.isCtl = false → stepI i s = none → RunI fs i s .fault
	\| loopNormal {body s s'} : Run fs body s (.normal s') → RunI fs (.loop body) s (.normal s')
	\| loopBr0 {body s s' r} :
	Run fs body s (.br 0 s') → RunI fs (.loop body) { s' with stack := s.stack } r →
	RunI fs (.loop body) s r
	\| loopBrS {body s n s'} : Run fs body s (.br (n + 1) s') → RunI fs (.loop body) s (.br n s')
	\| loopExit {body s c} : Run fs body s (.exit c) → RunI fs (.loop body) s (.exit c)
	\| loopHalted {body s s'} : Run fs body s (.halted s') → RunI fs (.loop body) s (.halted s')
	\| loopFault {body s} : Run fs body s .fault → RunI fs (.loop body) s .fault
	\| iteThen {thn s r c res res'} :
	s.stack = .i32 c :: r → c ≠ 0#32 → Run fs thn { s with stack := r } res →
	BlockOut r res res' → RunI fs (.ite thn) s res'
	\| iteElse {thn s r c} :
	s.stack = .i32 c :: r → c = 0#32 → RunI fs (.ite thn) s (.normal { s with stack := r })
	\| iteFault {thn s} : (∀ c r, s.stack ≠ .i32 c :: r) → RunI fs (.ite thn) s .fault
	\| br {l s} : RunI fs (.br l) s (.br l s)
	\| callNormal {s r i body s' v} :
	s.stack = .i32 i :: r → fs[i.toNat]? = some body →
	Run fs body { s with stack := [] } (.normal s') → s'.stack = [.i32 v] →
	RunI fs .callIndirect s (.normal { s' with stack := .i32 v :: r })
	\| callBad {s r i body s'} :
	s.stack = .i32 i :: r → fs[i.toNat]? = some body →
	Run fs body { s with stack := [] } (.normal s') → (∀ v, s'.stack ≠ [.i32 v]) →
	RunI fs .callIndirect s .fault
	\| callAbrupt {s r i body res} :
	s.stack = .i32 i :: r → fs[i.toNat]? = some body →
	Run fs body { s with stack := [] } res → res.abrupt →
	RunI fs .callIndirect s (match res with \| .br _ _ => .fault \| other => other)
	\| callMissing {s r i} :
	s.stack = .i32 i :: r → fs[i.toNat]? = none → RunI fs .callIndirect s .fault
	\| callBadStack {s} : (∀ i r, s.stack ≠ .i32 i :: r) → RunI fs .callIndirect s .fault
	\| exitTrap {c s} : RunI fs (.exitTrap c) s (.exit c)
	\| exitHalt {s} : RunI fs .exitHalt s (.halted s)

	inductive Run (fs : Funcs) : List WI → WState → Res → Prop where
	\| nil {s} : Run fs [] s (.normal s)
	\| consNormal {i is s s' r} : RunI fs i s (.normal s') → Run fs is s' r → Run fs (i :: is) s r
	\| consAbrupt {i is s r} : RunI fs i s r → r.abrupt → Run fs (i :: is) s r
	end

	end Wasm
	end WordDialect