No bridge axioms this time — Pallas field arithmetic, proven properly
This repository exists because of a failure, and the README says so in the second paragraph. An earlier attempt at verifying zcash/pasta_curves axiomatized the correctness of add, sub, neg, mul, square, montgomery_reduce, and invert — that is, it assumed precisely the statements the whole exercise was supposed to establish, then proved things above them. That's a hollow certificate: the #print axioms output is technically honest and the assurance is technically zero. Rather than patch it, I restarted the target with a hard rule: no bridge axioms. The correctness of the limb arithmetic is proven or the layer isn't claimed.
Pallas is half of the Pasta cycle that Zcash's Halo 2 runs on — the curve pair engineered so each one's scalar field is the other's base field, which is what makes recursive proof composition work without field emulation. Different beast from the ed25519 family in almost every dimension that matters to a prover: short Weierstrass instead of twisted Edwards, Montgomery-form 4×64-limb arithmetic instead of radix-2⁵¹, and a modulus chosen for its 2-adicity rather than its proximity to a power of two. Verifying it exercised completely different muscles than the dalek campaign — Montgomery reduction is a genuinely different correctness argument than a ×19 fold.
Same method, though: the Rust of src/fields/fp.rs and src/curves.rs transpiled via Charon/Aeneas, theorems stated about the extraction, build gated on verification/check.sh. The foundation layer is where the distinctive work sits. PPallas is a machine-checked Lucas/Pratt primality certificate for the 255-bit Pallas modulus — convincing a paranoid kernel that 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001 is actually prime, because "everyone knows it's prime" is an axiom wearing a trench coat, and this repo's whole premise is that we've stopped doing that. Above it, the Montgomery foundations: the R constants, the reduction invariant, and the denotation bridge from limbs to 𝔽ₚ.
The pyramid tops out at the group law over short Weierstrass and scalar multiplication, with the construction status dated and explicit about which layers are green. Where the ed25519 family verifies the signature algorithm the world already runs, this one verifies the arithmetic substrate of the proving systems the next decade seems intent on running. Between the two, the method has now survived contact with two curve shapes, two limb disciplines, and five codebases — and the failure that started this repo is the best argument I have for why the axiom audit belongs in the build, not in the README.