Overview

Proof obligations as structure fields

In CryptWalker, every kind of primitive (NIKE, KEM, signature scheme and so on) is a Lean structure. The structure holds the primitive's types and operations, and also propositions about those operations. To give an instance, you have to supply proofs of those propositions, so every instance satisfies them by construction.

For example, the NIKE structure has a commutes field stating that deriving a shared secret from either side gives the same result, g^x^y = g^y^x. An X25519 instance that compiles is an X25519 whose key agreement provably agrees.

Two X25519 implementations

The repository contains two implementations of X25519:

• A constant-time Montgomery ladder following RFC 7748, ported from Rust by hand. Proving commutativity for the ladder directly is hard.

• An implementation on top of Mathlib's Weierstrass-curve API. Mathlib already proves the group laws, so commutes follows almost immediately.

Test vectors

Proofs cover the properties the types state. Byte-level agreement with other implementations is checked with known-answer vectors:

• NIST ACVP vectors for ML-KEM-768.

• RFC vectors for Ed25519, Argon2, HKDF and AES-GCM-SIV.

• Vectors generated by the Go libraries hpqc and Katzenpost.

These vectors are copied into testdata/, and make verify-vectors checks them against their upstream sources.

Some of the code is written by LLM agents. Vectors are the gate that every such contribution has to pass.