Wavelet is an experimental compiler from a Rust-based DSL to asynchronous dataflow circuits, with its core passes formally verified in the Lean theorem prover.

Currently supported backends include the handshake dialect from LLVM CIRCT and tagless/ordered CGRAs such as RipTide.

Build and Usage

Please first install the following dependencies:

• Elan (Lean version manager)
• Cargo
• cvc5-1.3.3

Then simply run

cargo build

which will produce the CLI binary at target/debug/wavelet.

Example source programs can be found in integration-tests/tests/*/test.rs. To compile a simple example to the handshake MLIR dialect, run:

target/debug/wavelet compile integration-tests/tests/simple/test.rs \
    | target/debug/wavelet handshake

Developing and Verifying Proofs

All of the Lean formalization can be found in wavelet-core/lean, and by default, the cargo build command above does not check any proofs. To actually verify all proofs:

cd wavelet-core/lean
lake exec cache get
lake build Thm