[atiernan]

PR3 of P-384 ECDSA verification (3.5h). It adds the group law, the scalar product and verify, proven against contract.rs over PR2's six axioms. It is stacked on #23, and the crate stays at tier 0.

Commits

• cb00c2d (contracts): src/point_contract.rs, committed before the code. It states ec_add, scalar_mul, decode_public_key and derive_e (mod n) against spec.rs. verify keeps PR1's verify_requires/verify_ensures unchanged.
• f2b4401 (code):
  • point.rs: the SEC 1 §2.2.1 affine group law in the spec's case order, plus key decoding and validation.
  • scalar.rs: MSB-first double-and-add. Its invariant is that, after each prefix of bits, the result equals spec::scalar_mul of that prefix. No associativity is used.
  • convert.rs: reduction of an octet prefix mod m.
  • lemmas.rs: among others, the spec's bit-string derive_e equals os2ip of the first min(|h|, 48) octets.
  • verify.rs: proven to give exactly spec::ecdsa_verify(p384(), …) on every input.
• f6a97f1 (tests): tests/verify.rs.
  • Wycheproof ecdsa_secp384r1_sha384_test.json at d17cc89f: valid tcIds 1, 2, 5, 7, 295, 296, 297 and 300 are accepted; invalid tcIds 102, 109, 151, 171, 195 and 204 are rejected.
  • Also rejected: tampered r and s; r or s equal to 0, n, n + 1 or 2^384 − 1; wrong, short, long and empty digests; off-curve, compressed, infinity, wrong-length and X = p / Y = p keys.
  • A 64-octet digest is truncated to its leftmost 48 octets.

Checked

• Verus: 133 verified, 0 errors, from a clean cache, re-run independently of the agent. No rlimit is raised.
• axioms.rs: byte-identical to the reviewed file (SHA-256 e9ee88f1…a4e3). The 18 documented axioms are unchanged.
• Unchanged: spec.rs and field/contract.rs are untouched. contract.rs changed only in a doc comment.
• Tests: cargo test passes 7 field tests and 9 verify tests, in both debug and release.
• Lints: clippy and fmt are clean.
• cargo xtask check: passes.
• cargo xtask mutate clazel-p384: 26 of 26 mutations killed with certificates.
• Speed: about 45 ms per verification in release and 0.94 s in debug, measured on macOS. That fits the design's Stage 1 estimate.

Not done

• Step 9 with x_R ≥ n is proven but never exercised: no test vector reaches it, and the chance of one doing so is about 2^-190.
• No mutations of the exec code, no Kani harnesses, no full conformance suite (that is PR5), and no independent transcription (PR6).
• Verus has been run on macOS only.

CI has not run yet.

🤖 Generated with Claude Code