[kixelated]

Problem

The aarch64 P-256 theorems assumed that a multiple of G by a scalar in [1, n) is a finite point. ECDH's public key took it as a hypothesis, and ECDSA's key generation, signing, and verification took P256Order: every finite point has order n, which needs a count of the curve's points that Mathlib lacks.

Closes the quest P-256's generator is proven to have order n.

Approach

• n prime was already proven, by moq-dev/rind#346's Pratt certificate (N256Prime.lean).
• n·G = 0 (n256_nsmul_G in P256Multiples.lean): decide +kernel computes (n - 1)·G by doubling and adding (mulCheck), and gets -G. It checks every sum with moq-dev/rind#343's inverse-free addOk, so the extended-Euclid inverse that produces the coordinates (invEuclid) is untrusted. No native_decide, and no new axiom: Axioms.lean's pins are unchanged.
• From those two facts, Mathlib's addOrderOf_eq_prime gives G's order n (g_mult). Every multiple d·G with d in [1, n) also has order n (g_mult_order).
• P256Order is now per point. P256OrderOf P is the property for one point, P256Laws no longer carries an order, and p256Laws proves it with no hypothesis. The verify chain takes P256OrderOf Q for its key's point.
• Hypotheses dropped:
  • ECDH: p256_public_key takes the scalar's range [1, n) instead of a finite multiple. Every key has a scalar in that range, as p256_generate and p256_from_private_key state.
  • ECDSA: p256_ecdsa_generate, p256_ecdsa_from_private_key_and_public_key, and p256_ecdsa_sign lose P256Order. So does p256_ecdsa_key_pair_verify, since its Q = d·G.
• Kept: p256_ecdsa_public_key_new (a parsed peer point) keeps P256Order, and p256_agree keeps its fault case. Its docstring says why: a peer's point needs the group's order n, a point count beyond Mathlib (Hasse's bound at least).

Cost

P256Multiples.lean takes 15.9 s alone, against 8.1 s on main, so about 8 s more. Its peak memory is 4.0 GB, against 3.1 GB. The first version used Fermat inverses and took 16 s more; extended Euclid halved that. The file sits on the aarch64 P-256 path, which runs in parallel with the x86_64 modules.

Impact

• No public API or wire change. Only proofs/ and the quest tree change.
• Lean statement changes: p256_public_key's conclusion is now p256PublicKey d b.val, which moved to P256.lean. P256Laws.of_order is now p256Laws.

Alternatives

• An embedded certificate of about 383 points: about 60 KB of Lean source with no speed win, since the kernel's checks are the same.
• Batch-inverting a Jacobian chain with Montgomery's trick, which would be faster but needs more untrusted code. 8 s did not seem worth it.
• Building on the aarch64 generator table: fewer steps, but it would tie a curve fact to one backend's translation.

Follow-ups

• benchmarks/verified.toml (and so BENCHMARKS.md) still says the aarch64 ECDSA ✓ assumes P256_GROUP_ELEMENT_ORDER. That is still true, but now only for verification with a parsed public key. I left it alone, to keep this PR to proofs/ while moq-dev/rind#383 is open.

Validation

• admin/prove passes on the merged head b1842ae (CARGO_BUILD_JOBS=3, Lean capped at 6 GB).
• just check and just ci pass.

Review

Codex (gpt-6.1-sol, medium effort), round 1 on head b1842ae: no findings.

(Written by Claude Opus 5.5)

🤖 Generated with Claude Code

[pullfrog]

Your OpenCode Go account is out of credit. Top it up, then re-trigger Pullfrog.

OpenCode Go's response

provider error: Upstream request failed: Insufficient account funds

Top up OpenCode Go →

  ^{｜ Rerun failed job ➔ ｜ View workflow run ｜ via Pullfrog ｜ Using glm-5.3}

[coderabbitai]

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 20 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: CHILL
• Plan: Advanced
• Run ID: 6b7f96d7-1ae3-4d12-9e43-8bfd7ab8df19

Commits

Reviewing files that changed from the base of the PR and between e69a6a1 and b1842ae.

Files selected for processing: 7

• proofs/README.md
• proofs/Rind/Aarch64/P256.lean
• proofs/Rind/Aarch64/P256Ecdsa.lean
• proofs/Rind/Aarch64/P256Signature.lean
• proofs/Rind/P256Multiples.lean
• quest/m3/verified/README.md
• quest/m3/verified/p256-generator-order.md

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn

[kixelated]

Automated review by review (OpenAI)

Reviewed head: b1842ae

Findings: No actionable correctness issues found in the seven-file diff and supporting proof definitions.

Direction: The separation of unconditional group laws from per-point nonzero-multiple requirements is sound. mulCheck_spec checks the generated coordinates through addOk, so the Euclidean inverse implementation does not expand the trust base. The generator-order result is threaded through key generation, signing, and key-pair verification while retaining the parsed-public-key assumption and ECDH fault case.

Verification limits: GitHub-only source review; I did not run Lean, admin/prove, just check, just ci, or performance measurements. The existing axiom guards cover the affected public theorems and remain unchanged. The GitHub prove job is still running, so its result remains outstanding.