2 releases
| new 0.0.2 | Jan 11, 2025 |
|---|---|
| 0.0.1 | Jan 9, 2025 |
#138 in WebAssembly
81 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 0x0A |
TBD |
| Exists | (exists ) |
0xFC 0x0B |
TBD |
| Assume | (assume ) |
0xFC 0x0C |
TBD |
| Unique | (unique ) |
0xFC 0x0D |
TBD |
Variable instructions
| Instruction | WAT syntax | Binary representation | Description |
|---|---|---|---|
| i32.uzumaki | (i32.uzumaki) |
0xFC 0x1A |
TBD |
| i64.uzumaki | (i64.uzumaki) |
0xFC 0x1B |
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
~46K SLoC