Checking Orchard's Poseidon Against the Test Vectors

ironwood is a Lean 4 formalization of Zcash's Orchard circuits. Its security theorems are stated against Lean definitions of the primitives, such as the Poseidon hash and the curve generators. A proof about the wrong function proves nothing, so a basic question is whether those definitions compute what Zcash actually computes.

zcash-test-vectors is the reference: inputs and outputs produced by the Python implementation the other Zcash implementations test against. PR #229 (open, awaiting review), part of #204, connects the two with Lean theorems.

What is proved

zcash-test-vectorsTheorem
poseidon.py round constants (64×3) and MDS matrix (3×3)ironwood's constants equal the generator's
orchard_poseidon, 11 vectorsthe Poseidon permutation reproduces every one
orchard_poseidon_hash, 11 vectorsthe constant-length hash reproduces every one
orchard_generators, 9 pointseach generator is the point its encoding denotes

The theorems are about the definitions the circuit and security theorems already use, not copies made for testing.

How

A script reads the vectors from a pinned commit of zcash-test-vectors and writes them into Lean data modules. It parses poseidon.py for the constants rather than running it. A manifest records each file's hash, and CI checks the hashes on every run.

The theorems are then proved by evaluation in Lean's kernel. Evaluating Poseidon directly over the field type was too slow, so the evaluation runs on a natural-number mirror, and a separate theorem proves the mirror equals the real permutation for every input. Two more theorems close the obvious gaps: one shows all the vectors are present, so no check passes vacuously, and one shows every value is a canonical field element, so nothing is lost converting them.

Generators are compared through their compressed encodings. Encoding is injective on the curve, so each theorem says the model's point is the only curve point with the vector's encoding.

ironwood's CI re-proves every vector on every change. Changing one hex digit in a data module, or deleting a vector, makes a theorem fail to build.

What it doesn't cover

Test vectors check a definition on finitely many inputs. They catch a wrong constant or a transposed matrix, which is the kind of mistake that is easy to make when porting by hand, but they don't prove the definition right everywhere.

The rest of Orchard is not covered yet: the rest of the nullifier derivation, Sinsemilla, the group-hash function itself (only its nine outputs are checked here), the Merkle tree, value commitments beyond their two bases, and the key components.

Source