[atiernan]

PR2 of P-384 ECDSA verification (3.5h): the field arithmetic for clazel-p384, built on fiat-crypto =0.3.0 behind six axioms. It is stacked on #22, and the crate stays at tier 0.

Commits

• dcd344b spec: the field contracts (field/spec.rs, field/contract.rs), committed before any code.

• 26c4e5e: src/axioms.rs, holding p_mul, p_add, p_sub, n_mul, n_add and n_sub, one per fiat call. Also the fiat-crypto dependency, its DEPENDENCIES.md row (shipped) and the VERIFICATION.md TCB entry.

• 8b1d2d1: field/fe.rs and field/lemmas.rs, proven against the contracts over the axioms:

  • an Fe type whose invariant keeps each value below its modulus;
  • our own big-endian octet conversion with its range check;
  • Montgomery conversion as mul by R² and by 1;
  • square-and-multiply pow;
  • inv, proven equal to the spec's checked inv.

  Plus tests/field.rs, which uses known answers computed in Python.

• A merge of clazel-p384: ECDSA P-384 verification spec (3.5h, PR1), tier 0 #22, bringing in the spec's mutations.json, plus the TCB wording below.

Axioms

Each axiom's requires is fiat's printed precondition, 0 ≤ eval arg < m. Each ensures is fiat's printed postcondition, quoted verbatim in its doc comment.

Independent review. A fresh session reviewed axioms.rs at SHA-256 e9ee88f170b0f0565a44a016c66b9b94fe7371ca50acd1efe61ea6289dbfa4e3. Verdict: all six are sound.

• The calls: each calls the right function, with the arguments in the right order and p and n never mixed.
• The contracts: each requires and ensures matches fiat exactly. Both inverse literals and both R² literals were checked against the moduli.
• No panics: none is possible, including with overflow checks on. Every fiat operation was checked.
• Call sites: the Fe invariant discharges every one.

The review found one gap in the TCB text. It now also names:

• the printed pre/postcondition comments, which the axioms copy;
• rustc's i128, u64 and i8 arithmetic;
• that the published crate is the synthesizer's output.

It also no longer says the unwritten ECDSA code is proven.

Checks done

• Verus: 84 verified, 0 errors, from a clean cache.
• Mutations: cargo xtask mutate clazel-p384 gives 26 of 26 killed with certificates.
• Tests and lints: cargo test passes 7 tests, and clippy and fmt are clean.
• cargo xtask check: passes, with 18 documented axioms (12 in clazel-crypto, 6 here).

Not yet

• No point code and no verify.
• No mutations of the field code.
• No conformance suite or independent transcription.

CI has not run yet.

🤖 Generated with Claude Code