8 releases
| new 0.0.8 | Apr 15, 2025 |
|---|---|
| 0.0.7 | Apr 14, 2025 |
| 0.0.5 | Jan 30, 2025 |
#242 in WebAssembly
141 downloads per month
740KB
16K
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 |
In this block all possible program execution paths are considered |
| Exists | (exists ) |
0xFC 0x3b |
In this block the existance of a certain program execution path is considered |
| Assume | (assume ) |
0xFC 0x3c |
In this block the assumption about the program state in defined |
| Unique | (unique ) |
0xFC 0x3d |
In this block it is assumed the existance of only one certain program execution path |
Variable instructions
| Instruction | WAT syntax | Binary representation | Description |
|---|---|---|---|
| i32.uzumaki | (i32.uzumaki) |
0xFC 0x31 |
i32 value type attribute guiding inference compiler to generate a proof that reason about all possible values the variable can hold |
| i64.uzumaki | (i64.uzumaki) |
0xFC 0x32 |
i64 value type attribute guiding inference compiler to generate a proof that reason about all possible values the variable can hold |
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
~49K SLoC