4 releases
| new 0.0.4 | Jan 27, 2025 |
|---|---|
| 0.0.3 | Jan 27, 2025 |
| 0.0.2 | Jan 11, 2025 |
| 0.0.1 | Jan 9, 2025 |
#228 in WebAssembly
439 downloads per month
745KB
17K
SLoC
inf-wast
Inferara fork of Bytecode Alliance project
A Rust parser for the WebAssembly Text Format (WAT). Extended with Inference non-deterministic instructions.
Inference non-deterministic instructions
This repository extends the WebAssembly Text Format (WAT) 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 wast.
License
This project inherits the license from the original project, which is Apache-2.0_WITH_LLVM-exception.
Dependencies
~3MB
~47K SLoC