spectec/doc/example/NanoWasm.spectec

;;
;; NanoWasm
;;

;; Abstract Syntax

syntax localidx = nat
syntax globalidx = nat

syntax mut = MUT
syntax valtype = I32 | I64 | F32 | F64
syntax functype = valtype* -> valtype*
syntax globaltype = mut? valtype

syntax const = nat

syntax instr =
    | NOP
    | DROP
    | SELECT
    | CONST valtype const   hint(show %.CONST %)
    | LOCAL.GET localidx
    | LOCAL.SET localidx
    | GLOBAL.GET globalidx
    | GLOBAL.SET globalidx


;; Validation

syntax context = { GLOBALS globaltype*, LOCALS valtype* }

var C : context


relation Instr_ok: context |- instr : functype

rule Instr_ok/nop:
    C |- NOP : eps -> eps

rule Instr_ok/drop:
    C |- DROP : t -> eps

rule Instr_ok/select:
    C |- SELECT : t t I32 -> t

rule Instr_ok/const:
    C |- CONST t c : eps -> t

rule Instr_ok/local.get:
    C |- LOCAL.GET x : eps -> t
    -- if C.LOCALS[x] = t

rule Instr_ok/local.set:
    C |- LOCAL.SET x : t -> eps
    -- if C.LOCALS[x] = t

rule Instr_ok/global.get:
    C |- GLOBAL.GET x : eps -> t
    -- if C.GLOBALS[x] = MUT? t

rule Instr_ok/global.set:
    C |- GLOBAL.GET x : t -> eps
    -- if C.GLOBALS[x] = MUT t


;; Execution

syntax addr = nat
syntax moduleinst = { GLOBALS addr* }

syntax val = CONST valtype const

syntax store = { GLOBALS val* }
syntax frame = { LOCALS val*, MODULE moduleinst }
syntax state = store; frame
syntax config = state; instr*

var f : frame
var s : store
var z : state

def $local(state, localidx) : val
def $local((s; f), x) = f.LOCALS[x]

def $global(state, globalidx) : val
def $global((s; f), x) = s.GLOBALS[f.MODULE.GLOBALS[x]]

def $update_local(state, localidx, val) : state
def $update_local((s; f), x, v) = s; f[.LOCALS[x] = v]

def $update_global(state, globalidx, val) : state
def $update_global((s; f), x, v) = s[.GLOBALS[f.MODULE.GLOBALS[x]] = v]; f


relation Step: config ~> config
relation Step_pure: instr* ~> instr*

relation Step hint(tabular)
relation Step_pure hint(tabular)

rule Step/pure:
    z; instr*  ~>  z; instr'*
    -- Step_pure: instr* ~> instr'*

rule Step_pure/nop:
    NOP  ~>  eps

rule Step_pure/drop:
    val DROP  ~>  eps

rule Step_pure/select-true:
    val_1 val_2 (CONST I32 c) SELECT  ~>  val_1  -- if c =/= 0

rule Step_pure/select-false:
    val_1 val_2 (CONST I32 c) SELECT  ~>  val_2  -- otherwise

rule Step/local.get:
    z; (LOCAL.GET x)  ~>  z; val
    -- if val = $local(z, x)

rule Step/local.set:
    z; val (LOCAL.SET x)  ~>  z'; eps
    -- if z' = $update_local(z, x, val)

rule Step/global.get:
    z; (GLOBAL.GET x)  ~>  z; val
    -- if val = $global(z, x)

rule Step/global.set:
    z; val (GLOBAL.SET x)  ~>  z'; eps
    -- if z' = $update_global(z, x, val)


;; Binary Format

def $float(nat, nat*) : const

grammar Bbyte : nat = 0x00 | ... | 0xFF

grammar Bu(N : nat) : nat =
  | n:Bbyte              => n                       -- if $(n < 2^7 /\ n < 2^N)
  | n:Bbyte m:Bu($(N-7)) => $(2^7 * m + (n - 2^7))  -- if $(n >= 2^7 /\ N > 7)

grammar Bu32 : const = Bu(32)
grammar Bu64 : const = Bu(64)

grammar Bf(N : nat) : nat =
  | b*:Bbyte^(N/8) => $float(N, b*)

grammar Bf32 : const = Bf(32)
grammar Bf64 : const = Bf(64)


grammar Bvaltype : valtype =
    | 0x7F => I32
    | 0x7E => I64
    | 0x7D => F32
    | 0x7C => F64

grammar Bmut : mut? =
    | 0x00 => eps
    | 0x01 => MUT

grammar Bglobaltype : globaltype =
    | t:Bvaltype mut:Bmut => mut t

grammar Bresulttype : valtype* =
    | n:Bu32 (t:Bvaltype)^n => t^n

grammar Bfunctype : functype =
    | 0x60 t_1*:Bresulttype t_2*:Bresulttype => t_1* -> t_2*


grammar Bglobalidx : globalidx = x:Bu32 => x
grammar Blocalidx : localidx = x:Bu32 => x

grammar Binstr : instr =
  | 0x01 => NOP
  | 0x1A => DROP
  | 0x1B => SELECT
  | 0x20 x:Blocalidx => LOCAL.GET x
  | 0x21 x:Blocalidx => LOCAL.SET x
  | 0x23 x:Bglobalidx => GLOBAL.GET x
  | 0x24 x:Bglobalidx => GLOBAL.SET x
  | 0x41 n:Bu32 => CONST I32 n
  | 0x42 n:Bu64 => CONST I64 n
  | 0x43 p:Bf32 => CONST F32 p
  | 0x44 p:Bf64 => CONST F64 p