Galette

Compiler with a correctness proof in Rocq

Galette

An experimental Rocq port of the Pancake compiler.

Galette is an experimental port of the Pancake compiler from HOL4 to Rocq. It compiles programs written in a fragment of the Pancake language (some features, such as floating point, are not supported yet) to RISC-V assembly. Every ported definition is tagged with the HOL4 declaration it translates, so the Rocq statements look like the HOL4 ones. The extracted compiler reproduces the output of the original cake --pancake --target=riscv byte for byte on Flapjack's parity corpus. The compiler comes with a machine-checked proof intended to show that the output behaves like the source.

Galette is a sibling of Flapjack, the Lean port of the same compiler.

Get in touch View on GitHub ↗ See the intention of the correctness theorem
  1. Pancake parser and static checker
  2. Crep
  3. Loop
  4. Word
  5. Stack
  6. Lab
  7. RISC-V assembler, encoder, exporter

Every layer above is ported from HOL4. The passes from Pancake to RISC-V are covered by the ported correctness theorem; the parser is not.

What it is

The Pancake compiler, in Rocq

From HOL4 to Rocq

The Pancake compiler, ported

The Pancake compiler was originally verified in HOL4. Galette brings the compiler and the proofs about it to Rocq. HOL4 is the reference, and Flapjack's Lean port is a second opinion.

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.

Same-looking definitions

One HOL4 declaration, one translation

Every ported declaration is tagged with the HOL4 declaration it translates, and each HOL4 declaration has at most one translation. A script checks the tags. All of them have been compared line by line with HOL4; the 225 known differences are documented.

Same bytes

Byte-identical RISC-V output

The extracted compiler matches the original cake output byte for byte on all 166 fixtures of Flapjack's parity corpus, and on two builds of a stateless Ethereum guest program (about 5 MB of assembly each). The software is open source under the BSD-3-Clause License.

Intention of the correctness theorem

The machine code does what the Pancake program does

If the source terminates without failing
with result r and an I/O trace, the machine code terminates too, with the same result r and the same I/O trace.
If the source diverges
and runs forever, the machine 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. The theorem is a Rocq port of HOL4's pan_to_target_compile_semantics, and its statement is meant to match the HOL4 one clause by clause. As in HOL4, for the 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 machine code runs out of resources while the source doesn't. The exact Rocq statement is rather big, including all definitions directly or indirectly referred to, and needs to be examined. Its only axioms are the classical logic, choice and extensionality axioms declared in Base.v. The RISC-V model is a port of HOL4's L3 model, not the authoritative Sail model. See PROGRESS.md. Nobody has examined the Rocq statement as far as we know. Rocq statements accepted by Rocq as theorems might not be true. Galette is distributed "as is" under the BSD-3 Clause License.

Status

What's on the plate

Pancake fragment → RISC-V: implemented Floating point and some other Pancake features: not supported Byte-identical with cake on the parity corpus Pancake fragment → RISC-V: with a correctness theorem BSD-3-Clause, on GitHub ↗ Other targets: ask us

Get in touch

Who to talk to

Any use · other targets

Contact Flamingo Ponderado

If you want to use Galette, or if you need another target, send an email.

hello@flamingoponderado.com
Open in your mail app