1 unstable release
| new 0.0.5 | Jan 30, 2025 |
|---|
#475 in WebAssembly
1.5MB
27K
SLoC
inf-wasmparser
Inferara fork of Bytecode Alliance project
A Rust parser for the WebAssembly Binary Format. Extended with Inference non-deterministic instructions.
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.
Dependencies
~175–710KB
~14K SLoC