Inferara fork of Bytecode Alliance project
Inference non-deterministic instructions
This repository extends the WebAssembly Binary Format with non-deterministic instructions. These instructions are used to specify algorithms in more general way to be able to compile the source code targeting proof assistants like Rocq or Lean.
More information about Inference can be found in the official Inference language spec and on the Inferara website.
Block instructions
| Instruction | WAT syntax | Binary representation | Description |
|---|---|---|---|
| Forall | (forall ) |
0xfc 0x3a |
TBD |
| Exists | (exists ) |
0xfc 0x3b |
TBD |
| Assume | (assume ) |
0xfc 0x3c |
TBD |
| Unique | (unique ) |
0xfc 0x3d |
TBD |
Variable instructions
| Instruction | WAT syntax | Binary representation | Description |
|---|---|---|---|
| i32.uzumaki | (i32.uzumaki) |
0xfc 0x31 |
TBD |
| i64.uzumaki | (i64.uzumaki) |
0xfc 0x32 |
TBD |
Origin
This project is a fork of the wasmparser.
License
This project inherits the license from the original project, which is Apache-2.0_WITH_LLVM-exception.