[kixelated]

Follow-up to moq-dev/rind#384, which proved P-256's generator has order n. The aarch64 P-256 ECDSA proof now assumes HOL Light's P256_GROUP_ELEMENT_ORDER only for verification with a parsed public key; key generation, loading, signing, and verifying with a key pair's own point no longer need it. benchmarks/verified.toml still said the whole ✓ assumed it, so this narrows the note and re-renders BENCHMARKS.md.

just check passes.

🤖 Generated with Claude Code

(Written by Claude Opus 5.5)

[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 58 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: 6a9cfc78-8ca8-4da8-9e06-2904db00c773

Commits

Reviewing files that changed from the base of the PR and between 8747f62 and 6226d94.

Files selected for processing: 2

• BENCHMARKS.md
• benchmarks/verified.toml

• 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: 6226d94

No actionable findings in this documentation-only change.

The narrower assumption matches the proof at this commit:

• proofs/Rind/Aarch64/P256Signature.lean:388-488 states generation, key loading, and signing without a P256Order parameter.
• p256_ecdsa_key_pair_verify (lines 516-535) supplies g_mult_order d hd0 hd, whose proof in proofs/Rind/P256Multiples.lean:357-364 derives the key pair's point order from the proven generator order.
• p256_ecdsa_public_key_new (lines 540-563) still takes ho : P256Order and uses it for verification with the parsed point.
• The changed proof text in benchmarks/verified.toml:108 matches the rendered aarch64 ECDSA row in BENCHMARKS.md:564; the partial-correctness caveat for the unbounded nonce loop remains.

Direction: no revision requested on the reviewed diff.

Limits: GitHub-only static review. I did not run quest context, just check, the benchmark renderer, or Lean proofs; the PR's reported just check result was not independently reproduced. At the reviewed head, the queue checks are skipped, CodeRabbit is rate-limited, and Pullfrog failed with the reported provider-credit error, so these checks do not establish a fresh test/proof pass.