[kixelated]

Summary

agreement::PrivateKey computes its public key once, when it is generated or loaded, and keeps it. The PKCS#8 and SEC1 loaders reuse that same computation for their consistency check, and to_pkcs8() reuses it instead of another base-point multiplication.

• PrivateKey::public_key() now returns &PublicKey (a borrow, no computation).
• New PrivateKey::algorithm() and PublicKey::algorithm(); Algorithm is PartialEq/Eq.
• PrivateKey's Debug prints PrivateKey { algorithm: EcdhP256, .. } (the open follow-up from moq-dev/rind#383).
• PublicKey holds its algorithm, so to_spki() no longer infers the curve from the length.
• rind-rustls's Active drops its cached pub_key and borrows the key's own. rind-aws-lc-rs drops the algorithm fields from PrivateKey, PublicKey, and ParsedPublicKey, and maps back from rind's algorithm instead.
• PrivateKey's drop wipes only the private key. tests/zeroing.rs skips the cached public key's bytes for this type.
• Proofs: admin/prove leaves agreement::Algorithm opaque, since PublicKey now reaches its function pointers, and proofs/Rind/X86_64/Dispatch.lean models it as which of the four statics it is, dispatching generate and load on it. P-256's random draw moves behind a per-target P256Dispatch.lean: modelled on aarch64 as before, the translation's opaque new_random on x86_64. The X25519 and P-256 generate and from_scalar theorems now also state the public key each key keeps (x25519Key, p256Key), and public_key returns it. No theorem is weaker than main's, and no axiom or sorry is added; the s2n-bignum base-point contracts move from *_public_key to *_generate and *_from_scalar in Axioms.lean, since that is now where the public key is computed.

Decisions

• Settled by the maintainer on 2026-11-09, the failing prove check: ✅ fix the proofs in this PR, resized to M (rejected: land with prove failing and plan a follow-up; store AlgorithmId in PublicKey instead). Reason: main's proofs pass and this PR is what breaks them.
• Settled by the maintainer on 2026-11-09, wiping on PrivateKey's drop: ✅ wipe only self.private, and tests/zeroing.rs skips the cached public-key region for this type (rejected: wipe the whole key as Ed25519KeyPair does; wipe private only here and also change Ed25519KeyPair). This follows AGENTS.md's "wipe nothing else".

Public API

Breaking: agreement::PrivateKey::public_key() returns &PublicKey instead of PublicKey. This is what lets rind-rustls hand rustls a borrowed &[u8] without its own copy. To migrate, add .clone() where an owned key outlives its PrivateKey; key.public_key().as_ref() is unchanged. Additive: algorithm() on both key types, Eq on Algorithm. The adapters' public APIs are unchanged. No wire impact.

Choices for review

• The quest's ECDSA bullet (EcdsaKeyPair::public_key() re-parsing its cached point) is dropped. The point is already cached; the re-parse is only the coordinate range and on-curve check, far below a microsecond next to a verification (~30 us). Skipping it would need an unchecked constructor on every curve's VerifyingKey. That costs more than it saves.
• x25519_public_key and p256_public_key now take a key that satisfies x25519Key or p256Key, as generate and from_scalar prove every key they return does, instead of any curve key: public_key only reads the stored key, so its correctness is proven where the key is built. p256_public_key no longer needs a scalar-range hypothesis.
• proofs/Rind/X86_64/P256Dispatch.lean exists only so Dispatch.lean, which admin/prove copies to aarch64, can name P-256's random draw on both targets.
• The quest said the change was additive. Returning a borrow is breaking, but removing the rustls cache requires a borrow.

Benchmarks (Apple M-series, cargo bench -p rind-bench --bench x25519 --bench p256)

	rind	aws-lc-rs
p256-ecdh (generate, public key, agree)	26.6 us	29.8 us
p256-keygen	5.44 us	7.01 us

A generated key still costs one base-point multiplication; each later public_key() or to_pkcs8() is now free. The rustls handshake already cached, so its cost does not change.

Follow-ups

• Ed25519KeyPair (rind/src/high/signature.rs:1558) also wipes its public key, against the same rule. Recommendation: plan an XS quest to wipe only its secret parts and give tests/zeroing.rs the same skip.

Checks

just check and nix develop .#prove --command admin/prove pass.

Models

Size: M
Implementer: Claude, claude-opus-5-5, unknown effort
Implementer: Claude Code, claude-opus-5-5, low effort (iterate, S)
Implementer: Claude Code, claude-opus-5-5, medium effort (iterate, M)

(Written by Claude Opus 5.5)

Review

Rewritten by quest review after each round.

• Reviewer: Codex, gpt-6.1-sol, medium effort
• Session: 01a1c2df-aa52-7651-a3f1-3460ae164bef, round 1
• Head: 3ffabe7
• Base: origin/main at 78353e6
• Score: 9/10, Code inspection found no actionable regressions and the change appears ready to land, though builds and tests were not run as instructed.
• Findings: none

[kixelated]

Fixed in d051e59: PrivateKey's drop now wipes only self.private, as the maintainer decided, and tests/zeroing.rs skips the public-key region for this type. This settles the finding at rind/src/high/agreement.rs:212.

(Written by Claude Opus 5.5 with low effort)

[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 9 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: 97f0ae74-2d49-47d0-8f6d-8d12a2e23264

Commits

Reviewing files that changed from the base of the PR and between ccdda85 and 3ffabe7.

Files selected for processing: 23

• admin/prove
• proofs/README.md
• proofs/Rind/Aarch64/Axioms.lean
• proofs/Rind/Aarch64/FunsExternal.lean
• proofs/Rind/Aarch64/P256.lean
• proofs/Rind/Aarch64/P256Dispatch.lean
• proofs/Rind/Aarch64/TypesExternal.lean
• proofs/Rind/X86_64/Axioms.lean
• proofs/Rind/X86_64/Dispatch.lean
• proofs/Rind/X86_64/FunsExternal.lean
• proofs/Rind/X86_64/P256Dispatch.lean
• proofs/Rind/X86_64/TypesExternal.lean
• proofs/Rind/X86_64/X25519.lean
• quest/m2/api/agreement-key-state.md
• rind-aws-lc-rs/src/agreement.rs
• rind-python/src/agreement.rs
• rind-ring/src/agreement.rs
• rind-rustls/src/kx_group.rs
• rind-timing/src/cases.rs
• rind/src/high/agreement.rs
• rind/tests/cpu.rs
• rind/tests/debug.rs
• rind/tests/zeroing.rs

• 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

[pullfrog]

ℹ️ No critical issues — one wording/coverage nit in the proofs.

Reviewed changes

Reviewed the full 23-file diff end-to-end (Rust API, adapters, tests, and the Lean proof remodel), and verified locally: the admin/prove quote guard, cargo test -p rind --lib agreement, --test zeroing/--test debug with --features wipe, rind-aws-lc-rs (including --features wipe), rind-rustls --all-targets, clippy/fmt on the touched crates, and cargo check on the untouched consumers (rind-bench, rind-dart, rind-dimpl); the prove workflow is green on 3ffabe7.

• agreement::PrivateKey keeps its public key and algorithm, computed once at generate/load: public_key() returns &PublicKey, algorithm() is added to both key types, Algorithm is Eq, and to_pkcs8() plus the PKCS#8/SEC1 consistency checks reuse the stored public instead of a fresh base-point multiply.
• agreement::PublicKey holds its algorithm, so to_spki() dispatches on it instead of inferring the curve from key length.
• Adapters drop their caches: rind-rustls's Active borrows the key's own public key, and rind-aws-lc-rs drops its algorithm fields, mapping back from rind's algorithm via Algorithm::from_rind.
• Wipe scope: PrivateKey::drop wipes only self.private, and tests/zeroing.rs skips the cached public-key region — the maintainer-settled decision, matching AGENTS.md's "wipe nothing else".
• Proofs: agreement::Algorithm is modeled as a tag dispatching generate/load, P-256's random draw moves behind per-target P256Dispatch.lean, x25519Key/p256Key state the public key each key holds, and the s2n-bignum base-point contracts move to *_generate/*_from_scalar where the computation now lives.

  ^{｜ Fix all ➔ ｜ Fix 👍s ➔ ｜ View workflow run ｜ Using glm-5.3 ｜ 𝕏}

[pullfrog]

The docstring's "every key" (and p256_public_key's in proofs/Rind/Aarch64/P256.lean:1152) overstates the coverage: only keys from generate and from_scalar are shown to hold their public key. On main, x25519_public_key took any Keyed and recomputed, so even a key returned by the opaque from_pkcs8 loader had its public_key() provably correct; on this branch nothing establishes x25519Key for such a key, since its stored public now comes from inside the opaque boundary. Consider rewording here (and qualifying the PR body's "no theorem is weaker than main's"), or keeping the public-key computation in translated code for the loader path.

Technical details

# Proof coverage of loader-derived keys' public key

## Affected sites
- `proofs/Rind/X86_64/X25519.lean:396` — docstring claims `x25519_generate`/`x25519_from_scalar` show "every key" holds its public key; only keys from those two entry points are covered.
- `proofs/Rind/Aarch64/P256.lean:1152-1154` — same wording on `p256_public_key`.

## Why coverage narrowed
On `main`, `x25519_public_key` took any `high.agreement.Keyed mid.x25519.PrivateKey` with no hypothesis, and `PrivateKey::public_key` recomputed via the translated `encode_public` — so the composed statement "whatever key the opaque `x25519_from_pkcs8` returns, `public_key()` is `rfcx25519(scalar, 9)`" was provable. On this branch `x25519_public_key` requires `x25519Key d key`, and nothing establishes that predicate for `from_pkcs8`-derived keys: the opaque `x25519_from_pkcs8` now also produces the stored `high.agreement.PublicKey` with no spec. (`p256_public_key` on `main` already required scalar-range hypotheses, so its loader-path coverage was hypothesis-gated before as well.)

## Required outcome
- Either the docstrings and PR body state the narrowed coverage accurately ("every key those loaders return"), or the loader path keeps the public-key computation in translated code so `x25519Key` stays derivable for it.

## Suggested approach (optional)
`x25519_from_pkcs8` could stay opaque but return only the key plus the v2 DER's carried public key (`Option<&[u8]>`), with `Agree::load` — which is translated on x86_64 — computing `key.encode_public(algorithm)` and the consistency check outside the opaque boundary, restoring the unconditional `public_key` guarantee for that path.