text:
||| Validation Rules for Instructions
||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html)
module WebAssembly.Validation.Instructions

import WebAssembly.Structure
import WebAssembly.Validation.Types
import WebAssembly.Validation.Conventions

import Data.List

mutual
  ||| Instruction Sequences
  ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#instruction-sequences)
  public export
  data ValidSequence : Context -> (List Instr) -> FuncType -> Type where
    ||| Empty Instruction Sequence
    |||
    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#empty-instruction-sequence-epsilon)
    |||
    ||| > ```
    ||| > ---------------
    ||| > C ⊢ epsilon : ft
    ||| > ```
    ValidEmpty : (c : Context)
              -> (ft : FuncType)
              -> ValidSequence c [] ft

    ||| Non-Empty Instruction Sequence
    |||
    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#non-empty-instruction-sequence-xref-syntax-instructions-syntax-instr-mathit-instr-ast-xref-syntax-instructions-syntax-instr-mathit-instr-n)
    |||
    ||| ```
    ||| C ⊢ instr∗ : [t1∗] -> [t0∗ t]    C ⊢ instr : [t∗] -> [t3∗]
    ||| -----------------------------------------------------------
    ||| C ⊢ instr∗ instr : [t1∗] -> [t0∗ t3∗]
    ||| ```
    ValidCons  : (c  : Context)
              -> (is : List Instr)
              -> (i  : Instr)
              -> (t0 : ResultType)
              -> (t1 : ResultType)
              -> (t3 : ResultType)
              -> (t  : ResultType)
              -> ValidSequence c is (t1 ->> (t0 ++ t))
              -> ValidInstr c i (t ->> t3)
              -> ValidSequence c (is ++ [i]) (t1 ->> (t0 ++ t3))

  ||| Instructions
  public export
  data ValidInstr : Context -> Instr -> FuncType -> Type where

    ||| Sepc: https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-unreachable
    |||
    ||| ```
    ||| --------------------------------
    ||| C ⊢ unreachable : [t1∗] -> [t2∗]
    ||| ```
    MkValidUnreachable       : (c : Context)
                            -> (ft : FuncType)
                            -> ValidInstr c Unreachable ft

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-nop)
    |||
    ||| ```
    ||| ------------------
    ||| C ⊢ nop : [] -> []
    ||| ```
    MkValidNop               : (c : Context)
                            -> ValidInstr c Nop ([] ->> [])

    ||| Validation of `block`-instrucions
    |||
    ||| > * The block type must be valid as some function type [t∗1]→[t∗2].
    ||| > * Let C′ be the same context as C, but with the result type [t∗2] prepended to the labels vector.
    ||| > * Under context C′, the instruction sequence instr∗ must be valid with type [t∗1]→[t∗2].
    ||| > * Then the compound instruction is valid with type [t∗1]→[t∗2].
    ||| > – Source: [🔗 Core Specifation](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-block-xref-syntax-instructions-syntax-blocktype-mathit-blocktype-xref-syntax-instructions-syntax-instr-mathit-instr-ast-xref-syntax-instructions-syntax-instr-control-mathsf-end)
    |||
    ||| ```
    ||| C ⊢ blocktype: [t1∗] -> [t2∗]   C,labels[t2∗] ⊢ instr∗ : [t1∗] -> [t2∗]
    ||| -----------------------------------------------------------------------
    ||| C ⊢ block blocktype instr∗ end : [t1∗] -> [t2∗]
    ||| ```
    MkValidBlock             : (c  : Context)
                            -> (bt : BlockType)
                            -> (is : List Instr)
                            -> (t1 : ResultType)
                            -> (t2 : ResultType)
                            -> ValidBlockType c bt (t1 ->> t2)
                            -> ValidSequence (prependLabels [t2] c) is (t1 ->> t2)
                            -> ValidInstr c (Block bt is) (t1 ->> t2)

    |||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-loop-xref-syntax-instructions-syntax-blocktype-mathit-blocktype-xref-syntax-instructions-syntax-instr-mathit-instr-ast-xref-syntax-instructions-syntax-instr-control-mathsf-end)
    |||
    ||| ```
    ||| C ⊢ blocktype: [t1∗] -> [t2∗]   C,labels[t1∗] ⊢ instr∗ : [t1∗] -> [t2∗]
    ||| -----------------------------------------------------------------------
    ||| C ⊢ loop blocktype instr∗ end : [t1∗] -> [t2∗]
    ||| ```
    MkValidLoop              : (c  : Context)
                            -> (bt : BlockType)
                            -> (is : List Instr)
                            -> (t1 : ResultType)
                            -> (t2 : ResultType)
                            -> ValidBlockType c bt (t1 ->> t2)
                            -> ValidSequence (prependLabels [t1] c) is (t1 ->> t2)
                            -> ValidInstr c (Loop bt is) (t1 ->> t2)

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-if-xref-syntax-instructions-syntax-blocktype-mathit-blocktype-xref-syntax-instructions-syntax-instr-mathit-instr-1-ast-xref-syntax-instructions-syntax-instr-control-mathsf-else-xref-syntax-instructions-syntax-instr-mathit-instr-2-ast-xref-syntax-instructions-syntax-instr-control-mathsf-end)
    |||
    ||| ```
    ||| C ⊢ blocktype : [t1∗] -> [t2∗]   C,labels[t2∗] ⊢ instr1∗ : [t1∗] -> [t2∗]   C,labels[t2∗] ⊢ instr2∗ : [t1∗] -> [t2∗]
    ||| --------------------------------------------------------------------------------------------------------------------
    ||| C ⊢ if blocktype instr1∗ else instr2∗ end : [t1∗ i32] -> [t2∗]
    ||| ```
    MkValidIf                : (c  : Context)
                            -> (bt : BlockType)
                            -> (is : List Instr)
                            -> (js : List Instr)
                            -> (t1 : ResultType)
                            -> (t2 : ResultType)
                            -> ValidBlockType c bt (t1 ->> t2)
                            -> ValidSequence (prependLabels [t2] c) is (t1 ->> t2)
                            -> ValidSequence (prependLabels [t2] c) js (t1 ->> t2)
                            -> ValidInstr c (If bt is js) ((t1 ++ [TI32]) ->> t2)

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-br-l)
    |||
    ||| ```
    ||| C.labels[l] = [t∗]
    ||| ---------------------------
    ||| C ⊢ br l : [t1∗ t] -> [t2∗]
    ||| ```
    MkValidBr                : (c  : Context)
                            -> (l  : LabelIdx)
                            -> (t1 : ResultType)
                            -> (t2 : ResultType)
                            -> {auto in_bounds: InBounds l (labels c)}
                            -> ValidInstr c (Br l) ((t1 ++ (index l (labels c))) ->> t2)

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-br-if-l)
    |||
    ||| ```
    ||| C.labels[l] = [t∗]
    ||| -------------------------------
    ||| C ⊢ br_if l : [t∗ TI32] -> [t∗]
    ||| ```
    MkValidBrIf              : (c : Context)
                            -> (l : LabelIdx)
                            -> {auto in_bounds: InBounds l (labels c)}
                            -> ValidInstr c (BrIf l) (((index l (labels c)) ++ [TI32]) ->> (index l (labels c)))

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-br-table-l-ast-l-n)
    |||
    ||| ```
    ||| (C.labels[l] = [t∗])∗    C.labels[lN] = [t∗]
    ||| --------------------------------------------
    ||| C ⊢ br_table l∗ lN : [t1∗ t∗ i32] -> [t2∗]
    ||| ```
    MkValidBrTable           : (c : Context)
                            -> (ls : List LabelIdx)
                            -> (lN : LabelIdx)
                            -> (t1 : ResultType)
                            -> (t2 : ResultType)
                            -> {auto in_bounds: InBounds lN (labels c)}
                            -> ( (li : LabelIdx)
                              -> Elem li ls
                              -> {auto in_bounds_i: InBounds li (labels c)}
                              -> ((index li (labels c)) = (index lN (labels c))))
                            -> ValidInstr c (BrTable ls lN) ((t1 ++ (index lN (labels c)) ++ [TI32]) ->> t2)

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-return)
    |||
    ||| ```
    ||| C.return = [t∗]
    ||| ------------------------------
    ||| C ⊢ return : [t1∗ t∗] -> [t2∗]
    ||| ```
    MkValidReturn            : (c  : Context)
                            -> (t1 : ResultType)
                            -> (t2 : ResultType)
                            -> (t  : ResultType)
                            -> (return c = Just t)
                            -> ValidInstr c (Return) ((t1 ++ t) ->> t2)

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-call-x)
    |||
    ||| ```
    ||| C.funcs[x] = [t1*] -> [t2*]
    ||| ---------------------------
    ||| C ⊢ call x : [t1*] -> [t2*]
    ||| ```
    MkValidCall              : (c : Context)
                            -> (x : FuncIdx)
                            -> {auto in_bounds: InBounds x (funcs c)}
                            -> ValidInstr c (Call x) (index x (funcs c))

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-call-indirect-x)
    |||
    ||| ```
    ||| C.tables[0] = limits functype    C.types[x] = [t1*] -> [t2*]
    ||| ------------------------------------------------------------
    ||| C ⊢ call_indirect x : [t1* i32] -> [t2*]
    ||| ```
    MkValidCallIndirect      : (c  : Context)
                            -> (x  : TypeIdx)
                            -> (t1 : ResultType)
                            -> (t2 : ResultType)
                            -> {auto in_bounds_0: InBounds 0 (tables c)}
                            -> {auto in_bounds_x: InBounds x (types c)}
                            -> ((index x (types c)) = (t1 ->> t2))
                            -> ValidInstr c (CallIndirect x) ((t1 ++ [TI32]) ->> t2)

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-parametric-mathsf-drop)
    |||
    ||| ```
    ||| --------------------
    ||| C ⊢ drop : [t] -> []
    ||| ```
    MkValidDrop              : (c : Context)
                            -> (t : ValType)
                            -> ValidInstr c Drop ([t] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-parametric-mathsf-select)
    |||
    ||| ```
    ||| -----------------------------
    ||| C ⊢ select : [t t i32] -> [t]
    ||| ```
    MkValidSelect            : (c : Context)
                            -> (t : ValType)
                            -> ValidInstr c Select ([t, t, TI32] ->> [t])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-variable-mathsf-local-get-x)
    |||
    ||| ```
    ||| C.locals[x] = t
    ||| ---------------------------
    ||| C ⊢ local.get x : [] -> [t]
    ||| ```
    MkValidLocalGet          : (c : Context)
                            -> (x : LocalIdx)
                            -> {auto in_bounds: InBounds x (locals c)}
                            -> ValidInstr c (LocalGet x) ([] ->> [index x (locals c)])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-variable-mathsf-local-set-x)
    |||
    ||| ```
    ||| C.locals[x] = t
    ||| ---------------------------
    ||| C ⊢ local.set x : [t] -> []
    ||| ```
    MkValidLocalSet          : (c : Context)
                            -> (x : LocalIdx)
                            -> {auto in_bounds: InBounds x (locals c)}
                            -> ValidInstr c (LocalSet x) ([index x (locals c)] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-variable-mathsf-local-tee-x)
    |||
    ||| ```
    ||| C.locals[x] = t
    ||| ----------------------------
    ||| C ⊢ local.tee x : [t] -> [t]
    ||| ```
    MkValidLocalTee          : (c : Context)
                            -> (x : LocalIdx)
                            -> {auto in_bounds: InBounds x (locals c)}
                            -> ValidInstr c (LocalTee x) ([index x (locals c)] ->> [index x (locals c)])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-variable-mathsf-global-get-x)
    |||
    ||| ```
    ||| C.globals[x] = mut t
    ||| ----------------------------
    ||| C ⊢ global.get x : [] -> [t]
    ||| ```
    MkValidGlobalGet         : (c : Context)
                            -> (x : GlobalIdx)
                            -> {auto in_bounds: InBounds x (globals c)}
                            -> ValidInstr c (GlobalGet x) ([] ->> [snd (index x (globals c))])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-variable-mathsf-global-set-x)
    |||
    ||| ```
    ||| C.globals[x] = var t
    ||| ----------------------------
    ||| C ⊢ global.set x : [] -> [t]
    ||| ```
    MkValidGlobalSet         : (c : Context)
                            -> (x : GlobalIdx)
                            -> (t : ValType)
                            -> {auto in_bounds: InBounds x (globals c)}
                            -> ((index x (globals c)) = (Var, t))
                            -> ValidInstr c (GlobalSet x) ([] ->> [t])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= |t|/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI32Load           : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 4
                            -> ValidInstr c (I32Load memarg) ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= |t|/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI64Load           : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 8
                            -> ValidInstr c (I64Load memarg) ([TI32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= |t|/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidF32Load           : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 4
                            -> ValidInstr c (F32Load memarg) ([TI32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= |t|/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidF64Load           : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 8
                            -> ValidInstr c (F64Load memarg) ([TI32] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI32Load8S         : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 1
                            -> ValidInstr c (I32Load8S memarg) ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI32Load8U         : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 1
                            -> ValidInstr c (I32Load8U memarg) ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI32Load16S        : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 2
                            -> ValidInstr c (I32Load16S memarg) ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI32Load16U        : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 2
                            -> ValidInstr c (I32Load16U memarg) ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI64Load8S         : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 1
                            -> ValidInstr c (I64Load8S memarg) ([TI32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI64Load8U         : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 1
                            -> ValidInstr c (I64Load8U memarg) ([TI32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI64Load16S        : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 2
                            -> ValidInstr c (I64Load16S memarg) ([TI32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI64Load16U        : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 2
                            -> ValidInstr c (I64Load16U memarg) ([TI32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI64Load32S        : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 4
                            -> ValidInstr c (I64Load32S memarg) ([TI32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-load-n-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32] -> [t]
    ||| ```
    MkValidI64Load32U        : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 4
                            -> ValidInstr c (I64Load32U memarg) ([TI32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= |t|/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32 t] -> []
    ||| ```
    MkValidI32Store          : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 4
                            -> ValidInstr c (I32Store memarg) ([TI32, TI32] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= |t|/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32 t] -> []
    ||| ```
    MkValidI64Store          : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 8
                            -> ValidInstr c (I64Store memarg) ([TI32, TI64] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= |t|/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32 t] -> []
    ||| ```
    MkValidF32Store          : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 4
                            -> ValidInstr c (F32Store memarg) ([TI32, TF32] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= |t|/8
    ||| ------------------------------------------------
    ||| C ⊢ t.load memarg : [i32 t] -> []
    ||| ```
    MkValidF64Store          : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 8
                            -> ValidInstr c (F64Store memarg) ([TI32, TF64] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-n-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ----------------------------------------------
    ||| C ⊢ t.load memarg : [i32 t] -> []
    ||| ```
    MkValidI32Store8         : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 1
                            -> ValidInstr c (I32Store8 memarg) ([TI32, TI32] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-n-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ----------------------------------------------
    ||| C ⊢ t.load memarg : [i32 t] -> []
    ||| ```
    MkValidI32Store16        : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 2
                            -> ValidInstr c (I32Store16 memarg) ([TI32, TI32] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-n-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ----------------------------------------------
    ||| C ⊢ t.load memarg : [i32 t] -> []
    ||| ```
    MkValidI64Store8         : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 1
                            -> ValidInstr c (I64Store8 memarg) ([TI32, TI64] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-n-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ----------------------------------------------
    ||| C ⊢ t.load memarg : [i32 t] -> []
    ||| ```
    MkValidI64Store16        : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 2
                            -> ValidInstr c (I64Store16 memarg) ([TI32, TI64] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-memory-mathsf-store-n-xref-syntax-instructions-syntax-memarg-mathit-memarg)
    |||
    ||| ```
    ||| C.mems[0] = memtype    2^(memarg.align) <= N/8
    ||| ----------------------------------------------
    ||| C ⊢ t.load memarg : [i32 t] -> []
    ||| ```
    MkValidI64Store32        : (c      : Context)
                            -> (memarg : MemArg)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> LTE (power 2 (align memarg)) 4
                            -> ValidInstr c (I64Store32 memarg) ([TI32, TI64] ->> [])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#xref-syntax-instructions-syntax-instr-memory-mathsf-memory-size)
    |||
    ||| ```
    ||| C.mems[0] = memtype
    ||| -----------------------------
    ||| C ⊢ memory.size : [] -> [i32]
    ||| ```
    MkValidMemorySize        : (c : Context)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> ValidInstr c MemorySize ([] ->> [TI32])

    ||| [🔗 Spec]()
    |||
    ||| ```
    ||| C.mems[0] = memtype
    ||| --------------------------------
    ||| C ⊢ memory.grow : [i32] -> [I32]
    ||| ```
    MkValidMemoryGrow        : (c : Context)
                            -> {auto in_bounds: InBounds 0 (mems c)}
                            -> ValidInstr c MemoryGrow ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-numeric-mathsf-const-c)
    |||
    ||| ```
    ||| -------------------------
    ||| C ⊢ t.const c : [] -> [t]
    ||| ```
    MkValidI32Const          : (c   : Context)
                            -> (i32 : I32)
                            -> ValidInstr c (I32Const i32) ([] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-numeric-mathsf-const-c)
    |||
    ||| ```
    ||| -------------------------
    ||| C ⊢ t.const c : [] -> [t]
    ||| ```
    MkValidI64Const          : (c   : Context)
                            -> (i64 : I64)
                            -> ValidInstr c (I64Const i64) ([] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-numeric-mathsf-const-c)
    |||
    ||| ```
    ||| -------------------------
    ||| C ⊢ t.const c : [] -> [t]
    ||| ```
    MkValidF32Const          : (c   : Context)
                            -> (f32 : F32)
                            -> ValidInstr c (F32Const f32) ([] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-instr-numeric-mathsf-const-c)
    |||
    ||| ```
    ||| -------------------------
    ||| C ⊢ t.const c : [] -> [t]
    ||| ```
    MkValidF64Const          : (c   : Context)
                            -> (f64 : F64)
                            -> ValidInstr c (F64Const f64) ([] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-testop-mathit-testop)
    |||
    ||| ```
    ||| ---------------------------
    ||| C ⊢ t.testop : [t] -> [i32]
    ||| ```
    MkValidI32Eqz            : (c : Context)
                            -> ValidInstr c I32Eqz ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI32Eq             : (c : Context)
                            -> ValidInstr c I32Eq ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI32Ne             : (c : Context)
                            -> ValidInstr c I32Ne ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI32LtS            : (c : Context)
                            -> ValidInstr c I32LtS ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI32LtU            : (c : Context)
                            -> ValidInstr c I32LtU ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI32GtS            : (c : Context)
                            -> ValidInstr c I32GtS ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI32GtU            : (c : Context)
                            -> ValidInstr c I32GtU ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI32LeS            : (c : Context)
                            -> ValidInstr c I32LeS ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI32LeU            : (c : Context)
                            -> ValidInstr c I32LeU ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI32GeS            : (c : Context)
                            -> ValidInstr c I32GeS ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI32GeU            : (c : Context)
                            -> ValidInstr c I32GeU ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-testop-mathit-testop)
    |||
    ||| ```
    ||| ---------------------------
    ||| C ⊢ t.testop : [t] -> [i32]
    ||| ```
    MkValidI64Eqz            : (c : Context)
                            -> ValidInstr c I64Eqz ([TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI64Eq             : (c : Context)
                            -> ValidInstr c I64Eq ([TI64, TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI64Ne             : (c : Context)
                            -> ValidInstr c I64Ne ([TI64, TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI64LtS            : (c : Context)
                            -> ValidInstr c I64LtS ([TI64, TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI64LtU            : (c : Context)
                            -> ValidInstr c I64LtU ([TI64, TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI64GtS            : (c : Context)
                            -> ValidInstr c I64GtS ([TI64, TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI64GtU            : (c : Context)
                            -> ValidInstr c I64GtU ([TI64, TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI64LeS            : (c : Context)
                            -> ValidInstr c I64LeS ([TI64, TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI64LeU            : (c : Context)
                            -> ValidInstr c I64LeU ([TI64, TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI64GeS            : (c : Context)
                            -> ValidInstr c I64GeS ([TI64, TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidI64GeU            : (c : Context)
                            -> ValidInstr c I64GeU ([TI64, TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF32Eq             : (c : Context)
                            -> ValidInstr c F32Eq ([TF32, TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF32Ne             : (c : Context)
                            -> ValidInstr c F32Ne ([TF32, TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF32Lt             : (c : Context)
                            -> ValidInstr c F32Lt ([TF32, TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF32Gt             : (c : Context)
                            -> ValidInstr c F32Gt ([TF32, TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF32Le             : (c : Context)
                            -> ValidInstr c F32Le ([TF32, TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF32Ge             : (c : Context)
                            -> ValidInstr c F32Ge ([TF32, TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF64Eq             : (c : Context)
                            -> ValidInstr c F64Eq ([TF64, TF64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF64Ne             : (c : Context)
                            -> ValidInstr c F64Ne ([TF64, TF64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF64Lt             : (c : Context)
                            -> ValidInstr c F64Lt ([TF64, TF64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF64Gt             : (c : Context)
                            -> ValidInstr c F64Gt ([TF64, TF64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF64Le             : (c : Context)
                            -> ValidInstr c F64Le ([TF64, TF64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-relop-mathit-relop)
    |||
    ||| ```
    ||| ----------------------------
    ||| C ⊢ t.relop : [t t] -> [i32]
    ||| ```
    MkValidF64Ge             : (c : Context)
                            -> ValidInstr c F64Ge ([TF64, TF64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI32Clz            : (c : Context)
                            -> ValidInstr c I32Clz ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI32Ctz            : (c : Context)
                            -> ValidInstr c I32Ctz ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI32Popcnt         : (c : Context)
                            -> ValidInstr c I32Popcnt ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32Add            : (c : Context)
                            -> ValidInstr c I32Add ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32Sub            : (c : Context)
                            -> ValidInstr c I32Sub ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32Mul            : (c : Context)
                            -> ValidInstr c I32Mul ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32DivS           : (c : Context)
                            -> ValidInstr c I32DivS ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32DivU           : (c : Context)
                            -> ValidInstr c I32DivU ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32RemS           : (c : Context)
                            -> ValidInstr c I32RemS ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32RemU           : (c : Context)
                            -> ValidInstr c I32RemU ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32And            : (c : Context)
                            -> ValidInstr c I32And ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32Or             : (c : Context)
                            -> ValidInstr c I32Or ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32Xor            : (c : Context)
                            -> ValidInstr c I32Xor ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32Shl            : (c : Context)
                            -> ValidInstr c I32Shl ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32ShrS           : (c : Context)
                            -> ValidInstr c I32ShrS ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32ShrU           : (c : Context)
                            -> ValidInstr c I32ShrU ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32Rotl           : (c : Context)
                            -> ValidInstr c I32Rotl ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI32Rotr           : (c : Context)
                            -> ValidInstr c I32Rotr ([TI32, TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI64Clz            : (c : Context)
                            -> ValidInstr c I64Clz ([TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI64Ctz            : (c : Context)
                            -> ValidInstr c I64Ctz ([TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI64Popcnt         : (c : Context)
                            -> ValidInstr c I64Popcnt ([TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64Add            : (c : Context)
                            -> ValidInstr c I64Add ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64Sub            : (c : Context)
                            -> ValidInstr c I64Sub ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64Mul            : (c : Context)
                            -> ValidInstr c I64Mul ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64DivS           : (c : Context)
                            -> ValidInstr c I64DivS ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64DivU           : (c : Context)
                            -> ValidInstr c I64DivU ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64RemS           : (c : Context)
                            -> ValidInstr c I64RemS ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64RemU           : (c : Context)
                            -> ValidInstr c I64RemU ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64And            : (c : Context)
                            -> ValidInstr c I64And ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64Or             : (c : Context)
                            -> ValidInstr c I64Or ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64Xor            : (c : Context)
                            -> ValidInstr c I64Xor ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64Shl            : (c : Context)
                            -> ValidInstr c I64Shl ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64ShrS           : (c : Context)
                            -> ValidInstr c I64ShrS ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64ShrU           : (c : Context)
                            -> ValidInstr c I64ShrU ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64Rotl           : (c : Context)
                            -> ValidInstr c I64Rotl ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidI64Rotr           : (c : Context)
                            -> ValidInstr c I64Rotr ([TI64, TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF32Abs            : (c : Context)
                            -> ValidInstr c F32Abs ([TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF32Neg            : (c : Context)
                            -> ValidInstr c F32Neg ([TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF32Ceil           : (c : Context)
                            -> ValidInstr c F32Ceil ([TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF32Floor          : (c : Context)
                            -> ValidInstr c F32Floor ([TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF32Trunc          : (c : Context)
                            -> ValidInstr c F32Trunc ([TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF32Nearest        : (c : Context)
                            -> ValidInstr c F32Nearest ([TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF32Sqrt           : (c : Context)
                            -> ValidInstr c F32Sqrt ([TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF32Add            : (c : Context)
                            -> ValidInstr c F32Add ([TF32, TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF32Sub            : (c : Context)
                            -> ValidInstr c F32Sub ([TF32, TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF32Mul            : (c : Context)
                            -> ValidInstr c F32Mul ([TF32, TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF32Div            : (c : Context)
                            -> ValidInstr c F32Div ([TF32, TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF32Min            : (c : Context)
                            -> ValidInstr c F32Min ([TF32, TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF32Max            : (c : Context)
                            -> ValidInstr c F32Max ([TF32, TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF32Copysign       : (c : Context)
                            -> ValidInstr c F32Copysign ([TF32, TF32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF64Abs            : (c : Context)
                            -> ValidInstr c F64Abs ([TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF64Neg            : (c : Context)
                            -> ValidInstr c F64Neg ([TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF64Ceil           : (c : Context)
                            -> ValidInstr c F64Ceil ([TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF64Floor          : (c : Context)
                            -> ValidInstr c F64Floor ([TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF64Trunc          : (c : Context)
                            -> ValidInstr c F64Trunc ([TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF64Nearest        : (c : Context)
                            -> ValidInstr c F64Nearest ([TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidF64Sqrt           : (c : Context)
                            -> ValidInstr c F64Sqrt ([TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF64Add            : (c : Context)
                            -> ValidInstr c F64Add ([TF64, TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF64Sub            : (c : Context)
                            -> ValidInstr c F64Sub ([TF64, TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF64Mul            : (c : Context)
                            -> ValidInstr c F64Mul ([TF64, TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF64Div            : (c : Context)
                            -> ValidInstr c F64Div ([TF64, TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF64Min            : (c : Context)
                            -> ValidInstr c F64Min ([TF64, TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF64Max            : (c : Context)
                            -> ValidInstr c F64Max ([TF64, TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-binop-mathit-binop)
    |||
    ||| ```
    ||| --------------------------
    ||| C ⊢ t.binop : [t t] -> [t]
    ||| ```
    MkValidF64Copysign       : (c : Context)
                            -> ValidInstr c F64Copysign ([TF64, TF64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI32WrapI64        : (c : Context)
                            -> ValidInstr c I32WrapI64 ([TI64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI32TruncF32S      : (c : Context)
                            -> ValidInstr c I32TruncF32S ([TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI32TruncF32U      : (c : Context)
                            -> ValidInstr c I32TruncF32U ([TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI32TruncF64S      : (c : Context)
                            -> ValidInstr c I32TruncF64S ([TF64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI32TruncF64U      : (c : Context)
                            -> ValidInstr c I32TruncF64U ([TF64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64ExtendI32S     : (c : Context)
                            -> ValidInstr c I64ExtendI32S ([TI32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64ExtendI32U     : (c : Context)
                            -> ValidInstr c I64ExtendI32U ([TI32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64TruncF32S      : (c : Context)
                            -> ValidInstr c I64TruncF32S ([TF32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64TruncF32U      : (c : Context)
                            -> ValidInstr c I64TruncF32U ([TF32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64TruncF64S      : (c : Context)
                            -> ValidInstr c I64TruncF64S ([TF64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64TruncF64U      : (c : Context)
                            -> ValidInstr c I64TruncF64U ([TF64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF32ConvertI32S    : (c : Context)
                            -> ValidInstr c F32ConvertI32S ([TI32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF32ConvertI32U    : (c : Context)
                            -> ValidInstr c F32ConvertI32U ([TI32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF32ConvertI64S    : (c : Context)
                            -> ValidInstr c F32ConvertI64S ([TI64] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF32ConvertI64U    : (c : Context)
                            -> ValidInstr c F32ConvertI64U ([TI64] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF32DemoteF64      : (c : Context)
                            -> ValidInstr c F32DemoteF64 ([TF64] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF64ConvertI32S    : (c : Context)
                            -> ValidInstr c F64ConvertI32S ([TI32] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF64ConvertI32U    : (c : Context)
                            -> ValidInstr c F64ConvertI32U ([TI32] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF64ConvertI64S    : (c : Context)
                            -> ValidInstr c F64ConvertI64S ([TI64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF64ConvertI64U    : (c : Context)
                            -> ValidInstr c F64ConvertI64U ([TI64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF64PromoteF32     : (c : Context)
                            -> ValidInstr c F64PromoteF32 ([TF32] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI32ReinterpretF32 : (c : Context)
                            -> ValidInstr c I32ReinterpretF32 ([TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64ReinterpretF64 : (c : Context)
                            -> ValidInstr c I64ReinterpretF64 ([TF64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF32ReinterpretI32 : (c : Context)
                            -> ValidInstr c F32ReinterpretI32 ([TI32] ->> [TF32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidF64ReinterpretI64 : (c : Context)
                            -> ValidInstr c F64ReinterpretI64 ([TI64] ->> [TF64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI32Extend8S       : (c : Context)
                            -> ValidInstr c I32Extend8S ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI32Extend16S      : (c : Context)
                            -> ValidInstr c I32Extend16S ([TI32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI64Extend8S       : (c : Context)
                            -> ValidInstr c I64Extend8S ([TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI64Extend16S      : (c : Context)
                            -> ValidInstr c I64Extend16S ([TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-mathsf-xref-syntax-instructions-syntax-unop-mathit-unop)
    |||
    ||| ```
    ||| -----------------------
    ||| C ⊢ t.unop : [t] -> [t]
    ||| ```
    MkValidI64Extend32S      : (c : Context)
                            -> ValidInstr c I64Extend32S ([TI64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI32TruncSatF32S   : (c : Context)
                            -> ValidInstr c I32TruncSatF32S ([TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI32TruncSatF32U   : (c : Context)
                            -> ValidInstr c I32TruncSatF32U ([TF32] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI32TruncSatF64S   : (c : Context)
                            -> ValidInstr c I32TruncSatF64S ([TF64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI32TruncSatF64U   : (c : Context)
                            -> ValidInstr c I32TruncSatF64U ([TF64] ->> [TI32])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64TruncSatF32S   : (c : Context)
                            -> ValidInstr c I64TruncSatF32S ([TF32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64TruncSatF32U   : (c : Context)
                            -> ValidInstr c I64TruncSatF32U ([TF32] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64TruncSatF64S   : (c : Context)
                            -> ValidInstr c I64TruncSatF64S ([TF64] ->> [TI64])

    ||| [🔗 Spec](https://webassembly.github.io/spec/core/valid/instructions.html#t-2-mathsf-xref-syntax-instructions-syntax-cvtop-mathit-cvtop-mathsf-t-1-mathsf-xref-syntax-instructions-syntax-sx-mathit-sx)
    |||
    ||| ```
    ||| ----------------------------------
    ||| C ⊢ t2.cvtop_t1_sx? : [t1] -> [t2]
    ||| ```
    MkValidI64TruncSatF64U   : (c : Context)
                            -> ValidInstr c I64TruncSatF64U ([TF64] ->> [TI64])

||| [🔗Spec](https://webassembly.github.io/spec/core/valid/instructions.html#valid-constant)
public export
data ConstInstr : (c : Context) -> Instr -> Type where
  MkConstI32       : (c : Context) -> (i32 : I32) -> ConstInstr c (I32Const i32)
  MkConstI64       : (c : Context) -> (i64 : I64) -> ConstInstr c (I64Const i64)
  MkConstF32       : (c : Context) -> (f32 : F32) -> ConstInstr c (F32Const f32)
  MkConstF64       : (c : Context) -> (f64 : F64) -> ConstInstr c (F64Const f64)
  MkConstGlobalGet : (c : Context)
                  -> (x : GlobalIdx)
                  -> (t : ValType)
                  -> {auto in_bounds: InBounds x (globals c)}
                  -> (index x (globals c) = (Const, t))
                  -> ConstInstr c (GlobalGet x)

||| [🔗Spec](https://webassembly.github.io/spec/core/valid/instructions.html#valid-constant)
public export
data ConstExpr : (c : Context) -> List Instr -> Type where
  MkConstExprEmpty : (c : Context) -> ConstExpr c []
  MkConstExprCons  : (c     : Context)
                  -> (instr : Instr)
                  -> (expr  : Expr)
                  -> ConstInstr c instr
                  -> ConstExpr c expr
                  -> ConstExpr c (instr::expr)

max_stars_repo_name: RaoulSchaffranek/idris-webassembly

max_issues_repo_name: RaoulSchaffranek/idris-webassembly

max_forks_repo_name: RaoulSchaffranek/idris-webassembly


text:
twice : Char -> Char -> Char -> Char -> Nat -> (Nat, Nat)
twice w x y z Z = (Z, Z)
twice m n o p (S x)
    = case twice m n o p x of
           (a, b) => (S a, S b)

bothS : Int -> String -> (Nat, Nat) -> (Nat, Nat)
bothS test dummy = \(c, d) => (S c, S d)

pf : (x : Nat) -> twice 'a' 'b' 'c' 'd' (S x)
                     = bothS 99 "red balloons" (twice 'a' 'b' 'c' 'd' x)
pf k = Refl -- Refl

ext: idr


text:
module Control.Eff.Writer

import Control.Eff.Internal

%default total

public export
data WriterL : (lbl : k) -> (w : Type) -> (a : Type) -> Type where
  [search lbl]
  Tell : (vw : w) -> WriterL lbl w ()

public export
Writer : (w,a : Type) -> Type
Writer = WriterL ()

export
tellAt : (0 lbl : k) -> Has (WriterL lbl w) fs => w -> Eff fs ()
tellAt lbl vw = send $ Tell {lbl} vw

export %inline
tell : Has (Writer w) fs => w -> Eff fs ()
tell = tellAt ()

--------------------------------------------------------------------------------
--          Running Writer
--------------------------------------------------------------------------------

export
handleWriter :  {0 m : Type -> Type}
             -> (tell : w -> m ())
             -> WriterL lbl w a
             -> m a
handleWriter tell (Tell vw) = tell vw

unWriter : u -> (u -> w -> u) -> WriterL lbl w a -> (a,u)
unWriter vu f (Tell vw) = ((), f vu vw)

export
foldWriterAt :  (0 lbl : k)
             -> Has (WriterL lbl w) fs
             => u
             -> (u -> w -> u)
             -> Eff fs t
             -> Eff (fs - WriterL lbl w) (t,u)
foldWriterAt _ vu acc =
  handleRelayS vu (\x,y => pure (y,x)) $ \vu2,w,f =>
    let (vv,vu3) = unWriter vu2 acc w
     in f vu3 vv

export %inline
foldWriter :  Has (Writer w) fs
           => u
           -> (u -> w -> u)
           -> Eff fs t
           -> Eff (fs - Writer w) (t,u)
foldWriter = foldWriterAt ()

export
runWriterAt :  (0 lbl : k)
            -> Has (WriterL lbl w) fs
            => Monoid w
            => Eff fs t
            -> Eff (fs - WriterL lbl w) (t,w)
runWriterAt lbl = foldWriterAt lbl neutral (<+>)

export %inline
runWriter : Has (Writer w) fs => Monoid w =>
            Eff fs t -> Eff (fs - Writer w) (t,w)
runWriter = runWriterAt ()


text:
module MonadTransUniv

import public MonadFunctor

import Control.Monad.Error.Interface
import Control.Monad.Reader
import Control.Monad.RWS
import Control.Monad.State
import Control.Monad.Writer

namespace Reader

  public export %inline
  [Trans] MonadReader r m => MonadTrans t => MonadFunctor t => Monad (t m) => MonadReader r (t m) where
    ask   = lift ask
    local = liftMap . local

namespace State

  public export %inline
  [Trans] MonadState s m => MonadTrans t => Monad (t m) => MonadState s (t m) where
    get   = lift get
    put   = lift . put
    state = lift . state

namespace Writer

  public export %inline
  [Trans] MonadWriter r m => MonadTrans t => MonadFunctor t => Monad (t m) => MonadWriter r (t m) where
    writer = lift . writer
    tell   = lift . tell
    listen = liftMap listen
    pass   = liftMap pass

max_stars_repo_name: buzden/idris-playground

max_issues_repo_name: buzden/idris-playground

max_forks_repo_name: buzden/idris-playground


text:
module WebAssembly.Structure.Instructions.Memory

import WebAssembly.Structure.Values

import Decidable.Equality

-- Definition
-- Hint: Actual control-instructions are defined in
-- WebAssembly.Structure.Instructions.Definition

public export
record MemArg where
  constructor MkMemArg
  offset : U32
  align  : U32

-- Equality

total public export
lemma_memarg__offset_injective: ((o1 = o2) -> Void) -> (MkMemArg o1 a1 = MkMemArg o2 a2) -> Void
lemma_memarg__offset_injective o1_not_o2 Refl = o1_not_o2 Refl

total public export
lemma_memarg__align_injective: ((a1 = a2) -> Void) -> (MkMemArg o1 a1 = MkMemArg o2 a2) -> Void
lemma_memarg__align_injective a1_not_a2 Refl = a1_not_a2 Refl

-- Decidable Equality

public export
implementation DecEq MemArg where
  decEq (MkMemArg o1 a1) (MkMemArg o2 a2) = case decEq o1 o2 of
    No o1_not_o2 => No $ lemma_memarg__offset_injective o1_not_o2
    Yes Refl     => case decEq a1 a2 of
      No a1_not_a2 => No $ lemma_memarg__align_injective a1_not_a2
      Yes Refl     => Yes Refl


text:
module Data.List.Predicates.Thinning

import Data.List

%default total
%access public export

data Thinning : (xs,ys : List type) -> Type where
  Empty : Thinning Nil Nil
  Add   : (x : type) -> Thinning xs ys -> Thinning (x::xs) (x::ys)
  Skip  : Thinning xs ys -> Thinning xs (y::ys)

SubList : (xs,ys : List type) -> Type
SubList = Thinning

max_stars_repo_name: MarcelineVQ/idris-containers

max_issues_repo_name: MarcelineVQ/idris-containers

max_forks_repo_name: MarcelineVQ/idris-containers


text:
module Control.Linear.Network

-- An experimental linear type based API to sockets

import public Data.Either
import public Data.Maybe

import Control.Linear.LIO

import public Network.Socket.Data
import Network.Socket

public export
data SocketState = Ready | Bound | Listening | Open | Closed

||| Define the domain of SocketState transitions.
||| Label every such transition.
public export
data Action : SocketState -> Type where
  Bind    : Action Ready
  Listen  : Action Bound
  Accept  : Action Listening
  Send    : Action Open
  Receive : Action Open
  Close   : Action st

export
data Socket : SocketState -> Type where
     MkSocket : Socket.Data.Socket -> Socket st

||| For every label of a SocketState transition
||| and a success value of the transition,
||| define its result.
public export
Next : (action : Action st)
    -> (success : Bool)
    -> Type
Next Bind    True  = Socket Bound
Next Listen  True  = Socket Listening
Next Accept  True  = LPair (Socket Listening) (Socket Open)
Next Send    True  = Socket Open
Next Receive True  = Socket Open
Next Close   True  = Socket Closed
Next _       False = Socket Closed

export
newSocket : LinearIO io
      => (fam  : SocketFamily)
      -> (ty   : SocketType)
      -> (pnum : ProtocolNumber)
      -> (success : (1 sock : Socket Ready) -> L io ())
      -> (fail : SocketError -> L io ())
      -> L io ()
newSocket fam ty pnum success fail
    = do Right rawsock <- socket fam ty pnum
               | Left err => fail err
         success (MkSocket rawsock)

export
close : LinearIO io => (1 sock : Socket st) -> L1 io (Socket Closed)
close (MkSocket sock)
    = do Socket.close sock
         pure1 (MkSocket sock)

export
done : LinearIO io => (1 sock : Socket Closed) -> L io ()
done (MkSocket sock) = pure ()

export
bind : LinearIO io =>
       (1 sock : Socket Ready) ->
       (addr : Maybe SocketAddress) ->
       (port : Port) ->
       L1 io (Res (Maybe SocketError)
         (\res => Next Bind (isNothing res)))
bind (MkSocket sock) addr port
    = do code <- Socket.bind sock addr port
         case code of
           0 =>
             pure1 $ Nothing # MkSocket sock
           err =>
             pure1 $ Just err # MkSocket sock

export
connect : LinearIO io =>
          (sock : Socket) ->
          (addr : SocketAddress) ->
          (port : Port) ->
          L1 io (Res (Maybe SocketError)
            (\case Nothing => Socket Ready
                   Just _  => Socket Closed))
connect sock addr port
    = do code <- Socket.connect sock addr port
         case code of
           0 =>
             pure1 $ Nothing # MkSocket sock
           err =>
             pure1 $ Just err # MkSocket sock

export
listen : LinearIO io =>
         (1 sock : Socket Bound) ->
         L1 io (Res (Maybe SocketError)
           (\res => Next Listen (isNothing res)))
listen (MkSocket sock)
    = do code <- Socket.listen sock
         case code of
           0 =>
             pure1 $ Nothing # MkSocket sock
           err =>
             pure1 $ Just err # MkSocket sock

export
accept : LinearIO io =>
         (1 sock : Socket Listening) ->
         L1 io (Res (Maybe SocketError)
           (\res => Next Accept (isNothing res)))
accept (MkSocket sock)
    = do Right (sock', sockaddr) <- Socket.accept sock
             | Left err => pure1 (Just err # MkSocket sock)
         pure1 (Nothing # (MkSocket sock # MkSocket sock'))

export
send : LinearIO io =>
       (1 sock : Socket Open) ->
       (msg : String) ->
       L1 io (Res (Maybe SocketError)
         (\res => Next Send (isNothing res)))
send (MkSocket sock) msg
    = do Right c <- Socket.send sock msg
             | Left err => pure1 (Just err # MkSocket sock)
         pure1 (Nothing # MkSocket sock)

export
recv : LinearIO io =>
       (1 sock : Socket Open) ->
       (len : ByteLength) ->
       L1 io (Res (Either SocketError (String, ResultCode))
         (\res => Next Receive (isRight res)))
recv (MkSocket sock) len
    = do Right msg <- Socket.recv sock len
             | Left err => pure1 (Left err # MkSocket sock)
         pure1 (Right msg # MkSocket sock)

export
recvAll : LinearIO io =>
          (1 sock : Socket Open) ->
          L1 io (Res (Either SocketError String)
            (\res => Next Receive (isRight res)))
recvAll (MkSocket sock)
    = do Right msg <- Socket.recvAll sock
             | Left err => pure1 (Left err # MkSocket sock)
         pure1 (Right msg # MkSocket sock)


text:
module Main
import Types
import Lib

---Testcase calculateDeltas--PASS

main: IO()
main = do
  let thetas = (0, 0)
  let alpha = 0.3
  let trainingset = [(0.0,50.0), (1.0,60.0), (2.0,70.0)]
  let iterations = 1
  print $ show $ linearRegression thetas alpha trainingset iterations

--Results for the test -50.0

--Testcase adjustDeltas -- PASS
--main: IO()
--main = do
--  let deltas = [6.0, 5.2]
--  let examples = [(7.0,50.0), (2.0,3.0)]
--  print $ adjustDeltas deltas examples


text:
import Data.Vect

inputs : Vect 4 Double
inputs = [1.0, 2.0, 3.0, 2.5]

weights1 : Vect 4 Double
weights1 = [0.2, 0.8, -0.5, 1.0]
weights2 : Vect 4 Double
weights2 = [0.5, -0.91, 0.26, -0.5]
weights3 : Vect 4 Double
weights3 = [-0.26, -0.27, 0.17, 0.87]

weights : Vect 3 (Vect 4 Double)
weights = [weights1, weights2, weights3]

bias1 : Double
bias1 = 2.0
bias2 : Double
bias2 = 3.0
bias3 : Double
bias3 = 0.5

-- NOTE: this is not the idiomatic way to implement this.  This follows
-- the spirit of the Python lesson, which aims for simplicity and clarity.
output : Vect 3 Double
output = [
  (index 0 inputs)*(index 0 weights1) + (index 1 inputs)*(index 1 weights1) + (index 2 inputs)*(index 2 weights1) + (index 3 inputs)*(index 3 weights1) + bias1,
  (index 0 inputs)*(index 0 weights2) + (index 1 inputs)*(index 1 weights2) + (index 2 inputs)*(index 2 weights2) + (index 3 inputs)*(index 3 weights2) + bias2,
  (index 0 inputs)*(index 0 weights3) + (index 1 inputs)*(index 1 weights3) + (index 2 inputs)*(index 2 weights3) + (index 3 inputs)*(index 3 weights3) + bias3]

main : IO ()
main = printLn output


text:
module Data.Sexp.Parser

import Libraries.Text.Bounded
import Libraries.Text.Parser

import Data.List1
import Data.Sexp
import Data.Sexp.Lexer

Parser : Type -> Type -> Type
Parser tok a = Grammar tok True a

exact : Eq a => Show a => a -> Parser a ()
exact t = terminal ("expected " ++ (show t)) f where
  f : a -> Maybe ()
  f x = if x == t then Just () else Nothing

ignoreComment : Parser Token ()
ignoreComment = terminal "comment" f where
  f : Token -> Maybe ()
  f (Comment _) = Just ()
  f _ = Nothing

mutual
  oneSexp : Parser Token Sexp
  oneSexp = (many ignoreComment) *> (parseSAtom <|> parseSList)

  parseSList : Parser Token Sexp
  parseSList = do
    content <- ((exact LParen) `seq` \_ => many oneSexp <* (exact RParen))
    pure $ SList content

  parseSAtom : Parser Token Sexp
  parseSAtom = terminal "atom" isAtom where
    isAtom : Token -> Maybe Sexp
    isAtom (Atom a) = Just $ SAtom a
    isAtom (QuotedAtom a) = Just $ SAtom a
    isAtom _ = Nothing

sexpMain : Parser Token (List Sexp)
sexpMain = forget <$> some oneSexp

export
parseSexp : List (WithBounds Token) -> Either (String) (List Sexp)
parseSexp toks = case parse sexpMain toks of
                      Left (Error s remaining) => Left $ "parse error: \"" ++ s ++ "\"\nremaining tokens: " ++ (show "xxx")
                      Right (e, toks) => Right e

max_stars_repo_name: boxfire/rapid

max_issues_repo_name: boxfire/rapid

max_forks_repo_name: boxfire/rapid


text:
module Test

aString : String
aString = "Hello, World!"

max_stars_repo_name: teto/REPLica

max_issues_repo_name: teto/REPLica

max_forks_repo_name: teto/REPLica