Flapjack

Compiler with a correctness proof in Lean 4

Flapjack

An experimental Lean port of the Pancake compiler.

Flapjack is an experimental port of the Pancake compiler from HOL4 to Lean. It compiles programs written in the Pancake language to RISC-V assembly. The compiler comes with a machine-checked proof intended to show that the output behaves like the source.

Flapjack started with support of zkSecurity and Ethereum Foundation.

Get in touch View on GitHub ↗ See the intention of the correctness theorem
  1. Pancake AST (HOL style) your source, after parsing and conversion
  2. Crep
  3. Loop
  4. Word
  5. Stac
  6. Lab
  7. RISC-V after initialization

Layers shown above are covered by a correctness theorem. Initial steps (the parser that generates the Pancake AST, and a converter that changes the Pancake AST into HOL style) are not covered by any correctness proofs.

What it is

A small language with a compiler with a correctness theorem

From HOL4 to Lean

The Pancake compiler, ported

The Pancake compiler was originally verified in HOL4. Flapjack is bringing the compiler and proofs about it to Lean.

Agent-friendly

Easy for AI agents to write

Pancake is a small, low-level language with simple rules. That makes it a good target for code written by AI agents.

Target: RISC-V

Many features of Pancake to RISC-V

A path covering many features of Pancake source is implemented. All stages except initial steps (the Pancake parser and AST conversion) are associated with a correctness theorem. The software is open source under the BSD-3-Clause License.

Intention of the correctness theorem

The RISC-V code does what the Pancake program does

If the source terminates without failing
with result r and an I/O trace, the RISC-V code terminates too, with the same result r and the same I/O trace.
If the source diverges
and runs forever, the RISC-V code diverges too with the same I/O trace.

You reason about the Pancake program, and the theorem carries that reasoning down to the machine code.

Small print. For the correctness theorem to work fully, the stack size of the Pancake program needs to be statically determined, and must be small enough. Otherwise, the theorem leaves the possibility that the RISC-V code runs out of resources while the source doesn't. Some other limitations are documented in SOUNDNESS.md; that list is not exhaustive. The exact Lean statement needs to be examined. The exact statement is rather big and is in Lean, including all definitions directly or indirectly referred to, as interpreted by parser and elaborator of Lean. Flapjack's RISC-V model is different from the authoritative Sail RISC-V model. Nobody has examined the Lean statement as far as we know. Lean statements accepted by Lean as theorems might not be true. Flapjack is distributed "as is" under the BSD-3 Clause License.

Status

What's on the plate

Pancake → RISC-V: implemented Pancake → RISC-V: with a correctness theorem BSD-3-Clause, on GitHub ↗ ARM and x86: ask us

Get in touch

Who to talk to

zkVM guest programs

Contact zkSecurity

If you want to use Flapjack to build guest programs for zkVMs, you can talk to zkSecurity.

Visit zksecurity.xyz ↗

Other uses · ARM · x86

Contact Flamingo Ponderado

For any other use, or if you need another target such as ARM or x86, send an email.

hello@flamingoponderado.com
Open in your mail app