Ix: a zero-knowledge proof-carrying code platform

We have just folded space from Ix. Many machines on Ix. New machines.

The Ix platform enables the compilation of Lean 4 programs into zero-knowledge succinct non-interactive arguments of knowledge (zk-SNARKs). This allows the execution and typechecking of any Lean program to be verified by performing a sub-100-millisecond operation against an approximately 1 kilobyte certificate, regardless of the size of the original Lean program. In fact, the correctness of the entire mathlib library of formal mathematics, containing around 2 million lines of code, may be compiled in this way into a single kilobyte sized cryptographic certificate.

We call this technique zero-knowledge proof-carrying code or zkPCC, as an extension of the well-known proof-carrying code paradigm. Instead of a host system verifying formal proofs carried by an application as in proof-carrying code, in zkPCC the host or user verifies a cryptographic zero-knowledge proof generated from the typechecking of that formal proof. This greatly improves the runtime cost of this verification operation (potentially even up to O(1) depending on the specific zk-SNARK protocol used) and minimizes the complexity of locally dependent tooling (e.g. build systems for the formal proof language).

Additionally, while in proof-carrying code an application must reveal the proof artifact that demonstrates some formal property to the user, in zkPCC this proof artifact may be kept private, which opens up new possibilities for economic transactions over proofs.

:warning: This repository is a pre-alpha work in progress and should not be used for any purpose.

Use Cases

Our expectation is that Ix, and zkPCC in general, will allow applications to frictionlessly ship security guarantees to their users. Some possible use cases could be:

• Software written in compiled languages like Rust can attach to their binaries proofs of type signatures or other formal properties verified by tools such as Aeneas. Given mature certified compilation infrastructure (e.g. a future CompCert equivalent in Lean4), proofs that the compilation occurred correctly can also be attached, which would mitigate supply-chain attacks, such as those famously described by Ken Thompson in Reflections on Trusting Trust. This would also enable secure decentralized binary caching, saving on the need for duplicative local recompilation or expensive continuous integration software.
• In operating systems, hardware based process isolation costs 25%-33% overhead in terms of processor cycles. This means everytime you buy a laptop, cell phone, web server, you have to pay for a third more computing power, because we don't know how to safely run applications in protection ring 0. By reducing verification overhead and improving portability over proof-carrying code, zkPCC potentially enables more sophisticated software-based process isolation.
• Decentralized platforms like the Ethereum blockchain could publish formal specifications of their protocol and then require clients, layer-2s, zkVMs, etc. to publish zkPCC proofs that their current specific version satisfies such specifications. Such proofs could be verified on-chain, and even programmatically gate certain protocol updates (e.g. version X validates that version X+1 is a correct update).
• Individual smart contracts can publish on-chain proofs of their formal models or proofs showing that their bytecode was generated from particular sources (currently a trusted block explorer feature).
• Cryptographic projects like the risc0 zkVM could include a proof of the correctness of their Lean 4 formal model alongside (or aggregated within) every proof produced by their zkVM.

Example: Embedding Fermat's Last Theorem in Fermat's Margin Note

In or around 1637, the mathematician Pierre Fermat conjectured the following:

1. It is impossible to separate a cube into two cubes, or a fourth power into two fourth powers, or in general, any power higher than the second, into two like powers.
2. I have discovered a truly marvelous proof of this
3. which this margin is too narrow to contain.

The first part of this statement famously evaded proof for over 350 years before finally being demonstrated by Andrew Wiles in 1994. Mathematicians and historians of mathematics have also long debated the second part, whether Fermat's claim that he possessed a proof of the first part is credible, which seems unlikely given the complexity and modern mathematical infrastructure used by the Wiles proof of the first part. Rarely discussed, however, is the third part, which is in fact a statement of proof theory, specifically one which proposes an information theoretic lower bound to the size of the proof of a particular proposition.

The specific margin in question is page 85 in the 1621 edition of Diophantus' Arithmetica, which is a folio volume with dimensions 353mm tall by 225mm wide by 40mm deep. Leaving the precise dimensions of the margins as an exercise to the reader, it is trivial to show the proposition is false regardless of margin size, or the size of the proof (up to very large bounds) if one permits the proof to printed in the margin using arbitrarily small text, using microfilm, photolithography, etc. It is more interesting to assume that what Fermat meant was that the margin is too narrow to contain a proof written in Fermat's own handwriting.

Happily, we have an example of text we know would satisfy this constraint, Fermat's margin note itself! In Latin, the note reads:

Cubum autem in duos cubos, aut quadratoquadratum in duos quadratoquadratos & generaliter nullam in infinitum ultra quadratum potestatem in duos eiusdem nominis fas est dividere cuius rei demonstrationem mirabilem sane detexi. Hanc marginis exiguitas non caperet.

At 262 characters, and 8-bits per character, this is 2096 bits, or 262 bytes. This is quite small, but fortunately not quite as small as a Groth16 proof over BN254:

A Groth16 proof has two G1 points and one G2. In the BN254 pairing curve these take 64 and 128 bytes respectively uncompressed totaling 256 bytes for a proof.

So if we can show that a Groth16 proof of a proof of the first part of Fermat's Last Theorem is constructible, we will have clearly - though non-constructively- disproven the third part.

A Lean 4 formalization of Fermat's Last Theorem is in progress, and gives the statement as:

theorem PNat.pow_add_pow_ne_pow
    (x y z : ℕ+)
    (n : ℕ) (hn : n > 2) :
    x^n + y^n ≠ z^n :=
  PNat.pow_add_pow_ne_pow_of_FermatLastTheorem FLT.Wiles_Taylor_Wiles x y z n hn

Currently, as the dependencies of this theorem contain sorry holes, we cannot feed it through ix (which only works over complete program graphs). Once the formalization is complete, however, you will be able to do

> ix store FLT.lean PNat.pow_add_pow_ne_pow
e53c3d4bad8538e152a89d8bf75be178a3876252744961b9a087fe3973545c20
> ix prove --check e53c3d4bad8538e152a89d8bf75be178a3876252744961b9a087fe3973545c20
b44236ba17ad7445ae3eac48a8ba86ba00f08c069237b08451e311b688146e7e

to generate a multi-STARK proof that the theorem typechecks. With a Groth16 circuit that recursively proves verification of such proofs, i.e. a Groth16 final SNARK, the construction is complete, and we can embed a proof of Fermat's Last Theorem in Fermat's Margin Note.

Architecture

Ix consists of the following core components:

• The Ix compiler, which transforms Lean 4 programs into a format called ixon, the ix object notation, which is an alpha-invariant content-addressable serialization or wire format. The compiler also includes a decompiler to convert ixon objects back into Lean programs (by preserving the alpha-relevant metadata in a separate ixon object and re-merging the computationally relevant and irrelevant parts).
• The Aiur zkDSL which is a first-order functional programming language that generates multi-STARK circuits.
• The IxVM (not yet released), which implements reduction and typechecking of ixon (including ingress and egress from and to binary data).
• Integration with the iroh p2p network so that different ix users can easily share ixon data between themselves.

Benchmarks

Compiler performance benchmarks are tracked at https://bencher.dev/console/projects/ix/plots

Usage

Prerequisites

• Install Clang to enable Bindgen, then set LIBCLANG_PATH per https://rust-lang.github.io/rust-bindgen/requirements.html

Build

• Build and test the Ix library with lake build and lake test
• Install the ix binary with lake run install, or run with lake exe ix

Testing

Lean tests: lake test

• lake test -- <suite> runs one or multiple primary test suites. Primary suites: ffi, byte-array, ixon, claim, commit, canon, keccak, sharing, graph-unit, condense-unit
• lake test -- --ignored runs only the expensive test suites: shard-map, rust-canon-roundtrip, serial-canon-roundtrip, parallel-canon-roundtrip, graph-cross, condense-cross, compile, decompile, rust-serialize, rust-decompile, commit-io, aiur, aiur-hashes, ixvm
  • Most tests require at least 32 GB RAM
  • The compile and decompile tests require 128 GB RAM
  • aiur and aiur-hashes generate ZK proofs and use significant CPU
• lake test -- --ignored <ignored-suite> runs one or multiple expensive suites by name
• lake test -- --include-ignored runs both primary and expensive test suites
• lake test -- --include-ignored <ignored-suite> runs all primary suites plus one or multiple expensive suites
• lake test -- cli runs CLI integration tests
• lake test -- rust-compile runs the Rust cross-compilation diagnostic

Rust tests: cargo test or cargo nextest run

Proving under SP1

The Ix kernel typechecker has an SP1 guest at sp1/guest/ driven by a host at sp1/host/. The workflow is two steps: first compile a Lean program to a .ixe serialized Ixon.Env, then feed that file to the SP1 host to either execute or prove the typecheck.

Nix users only: enter the SP1 dev shell first to pick up cargo-prove and the succinct Rust toolchain:

nix develop .#sp1

Non-Nix users: install the SP1 toolchain manually per the SP1 docs.

1. Compile a .ixe from a Lean file. ix compile takes the Lean source as a positional argument and writes the serialized Ixon.Env; --out sets the output path (default: the lowercased input stem plus .ixe). For a small demo env:

lake exe ix compile Tests/MinimalDefs.lean --out minimal.ixe

For a larger, realistic env compile one of the Benchmarks/Compile targets, then scope proving to a single constant with --constant (step 2):

lake exe ix compile Benchmarks/Compile/CompileInit.lean --out init.ixe

1. Execute or prove under SP1. From sp1/host/, run the host with --ixe pointing at the file produced above:

cd sp1/host # Execute the kernel typecheck in the SP1 VM (no proof), prints failures + cycles RUST_LOG=info cargo run --release -- --execute --ixe ../../minimal.ixe # Generate and verify a compressed SP1 proof of the same typecheck (CPU) WITHOUT_VK_VERIFICATION=1 RUST_LOG=info cargo run --release -- --ixe ../../minimal.ixe # Prove a single constant out of a larger env (Anon-only): the host resolves # the name and ships only that constant's closure sub-env. Full-closure by # default; add --skip-deps for a subject-only check (deps trusted). WITHOUT_VK_VERIFICATION=1 RUST_LOG=info cargo run --release -- --ixe ../../init.ixe --constant Nat.add_comm

With no --ixe, the host runs against an empty Ixon.Env.

Verifying-key bypass (WITHOUT_VK_VERIFICATION=1). Proving currently requires this environment variable; --execute does not. The guest hashes via the patched BLAKE3's BLAKE3_COMPRESS precompile (see argumentcomputer/BLAKE3 branch sp1), whose recursion shapes aren't in the SP1 prover's bundled vk_map.bin. Without the bypass, proving aborts with vk not allowed / vk_root mismatch. The host is built with the SP1 fork's experimental feature, which honors this variable on both th