[kixelated]

Problem

Scheduled build, lint, ctgrind, mutation, and timing jobs failed on main. Most failures were test setup or instrumentation; ARM's AES enum also left its unused storage unwiped under wipe.

Approach

• Wipe the complete ARM AES encryption and decryption key enums on drop, matching the other backends. Give every AES key enum an explicit byte tag so zeroing preserves a valid first variant during field drop.
• Keep agreement policy on high-layer curve markers to avoid cargo-modules' receiver attribution bug. The layering checker, stored keys, and function-pointer dispatch stay the same.
• Retarget proof extraction and dispatch models to the curve markers and associated key types, preserving source quote guards, opacity boundaries, and theorem hypotheses.
• Handle an empty Dart cross-target list and apply the pinned nightly formatting.
• Declassify decoded OAEP plaintext only before the test assertion, and keep the Python extension out of forced Rust library tests in ctgrind.
• Exclude deliberately planted scanner fixtures from mutation testing; the variable-time scanner still tests them.
• Give dudect a minimal shell so unused Marvin downloads cannot prevent its tests from running.

Impact

• No public API or wire-format changes.
• Under wipe, ARM AES wrappers clear their entire storage, including the inactive enum tail. Without wipe, wiping remains disabled.
• HMAC, timing statistics, and the leak threshold are unchanged.

Validation

• quest gate nix develop --command just ci: passes, including 718 tests, 12 rind wipe tests, 6 adapter wipe tests, doc tests, builds and Clippy, and the 26-test Dart suite.
• Reproduced the ARMv7 zeroing failure at byte 244; all 12 zeroing tests pass on both QEMU crypto-extension and no-NEON paths, including a rerun with the final explicit enum tags.
• Reproduced the OAEP ctgrind error and Python cross-link failure. Both OAEP tests and all 71 adapter tests now report zero ctgrind errors.
• Reproduced Dart's line-66 pattern failure with the original empty-variable test. The fixed full suite passes all 26 tests with an empty variable; hook tests with an unset variable and the analyzer pass.
• The exact pinned nightly-2025-02-14 formatter passes for the drift files, agreement refactor, and all four AES backends.
• The original mutation configuration lists the planted fixtures; the fixed configuration excludes them. A two-backend listing audit restores exactly four displaced AES exclusions and confirms neighboring arithmetic and key-drop mutants remain enabled.
• Quiet Core 2-path HMAC-SHA256 signing passed over 20.86M measurements, t = -0.83; the planted leak was detected. The original runner's t = -13.50 was not reproduced, and this host has a different microarchitecture.
• Both exact archive URLs that returned HTTP 504 now return HTTP 200; the complete Marvin shell realizes successfully.
• Reproduced 16 spurious mid-to-high edges; the unchanged admin/structure now reports zero source and graph errors. All 13 agreement tests and the ECDH wipe test pass.
• Full quest gate nix develop .#prove --command admin/prove: passes all 2,475 build jobs, including both architecture models and the axiom audits. This fixes the PR-only failure from stale agreement dispatch quotes and extraction roots; source guards, opacity boundaries, and theorem hypotheses remain intact.
• On head 07a514e, the GitHub prove job fails before admin/prove starts: the pinned Aeneas archive download returns HTTP 504. The exact URL also returns 504 locally. Main uses the same unchanged URL and hash, and GitHub release metadata confirms the pinned digest. This external download failure is separate from the fixed source/model regression; no retry, dependency, or proof-coverage workaround was added.
• Synthetic fixtures confirm allowed layering passes and a root type alias from mid to high is rejected. A root-reexported high trait implemented in mid with no high types in its associated signatures remains invisible to the existing checker; this change does not rely on that form.

Alternatives

Keep the layering checker intact instead of filtering function dependencies, and keep the timing signal intact instead of changing the detector after an unreproduced observation.

Follow-ups

None proposed. The original HMAC timing observation remains disclosed above; a passing local measurement does not establish absence of leakage on the original runner.

Caused by

• moq-dev/rind#458 introduced the ARM AES wrapper without a whole-enum wipe.
• moq-dev/rind#315 put high-layer agreement trait methods on mid-layer key types, which cargo-modules attributes to the receiver's layer.
• moq-dev/rind#462 split an empty Dart cross-target variable into one invalid target.
• moq-dev/rind#482 added the OAEP plaintext assertion without declassifying its test value.
• moq-dev/rind#459 added the Python extension to a workspace whose ctgrind runner forces Rust library tests.
• moq-dev/rind#455 added scanner fixtures without excluding them from mutation testing.
• moq-dev/rind#483 made dudect fetch Marvin-only dependencies. The HTTP 504 outage itself was external.
• Formatting drift accumulated across changes; no single PR caused it.

Review

Independent read-only local review through T3 delegate_task.

• Reviewer: Claude Code, claude-opus-5-5, medium effort
• Session: T3 delegated task 4d7506b0-f068-4d54-8a39-5749b2e98372, round 1
• Head: a462587
• Base: origin/main at b295b31
• Score: 9/10, no actionable findings; the final branch and proof follow-through were independently reviewed.
• Findings: none.

The fresh review verified the model's marker/key parameters, each curve's dispatch, one-to-one extraction and opacity renames, source quote guards, and unchanged theorem statements and hypotheses. No axioms or proof shortcuts were added. The review's only readiness caveat was completion of the fresh local checks; their results are recorded under Validation.

Review exemption for head 07a514e: applied the online reviewer's four exact line-pin corrections unchanged in .cargo/mutants.toml. The listing audit removes only the four named already-triaged mutants; neighboring mutants remain enabled. No new round is needed for an unchanged reviewer-suggested patch.

Models

Size: M
Implementer: Codex, gpt-6.1-sol, xhigh effort
Implementer: Codex, gpt-6.1-sol, xhigh effort
Implementer: Codex, gpt-6.1-sol, xhigh effort
Implementer: Codex, gpt-6.1-sol, xhigh effort

(Written by GPT-6.1 Sol with xhigh)

[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 5 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: 115eaab7-da0b-4d54-8dde-9fe2fb2b8697

Commits

Reviewing files that changed from the base of the PR and between ae45ece and 07a514e.

Files selected for processing: 27

• .cargo/mutants.toml
• .github/workflows/timing.yml
• CONTRIBUTING.md
• admin/ctgrind
• admin/prove
• flake.nix
• proofs/Rind/Aarch64/FunsExternal.lean
• proofs/Rind/Aarch64/P256.lean
• proofs/Rind/Aarch64/P256Dispatch.lean
• proofs/Rind/Aarch64/TypesExternal.lean
• proofs/Rind/X86_64/Dispatch.lean
• proofs/Rind/X86_64/FunsExternal.lean
• proofs/Rind/X86_64/TypesExternal.lean
• proofs/Rind/X86_64/X25519.lean
• rind-aws-lc-rs/src/cipher.rs
• rind-aws-lc-rs/src/rsa.rs
• rind-aws-lc-rs/src/signature.rs
• rind-aws-lc-rs/tests/keys.rs
• rind-dart/test/hook_test.dart
• rind/src/high/agreement.rs
• rind/src/high/pkcs1.rs
• rind/src/low/aarch64/aes.rs
• rind/src/low/arm/aes.rs
• rind/src/low/cpu.rs
• rind/src/low/portable/aes.rs
• rind/src/low/portable/poly1305.rs
• rind/src/low/x86_64/aes.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]

Important

Two must-address findings inline: the prove check is red on this PR — the agreement refactor outdates the Rust quoted in proofs/Rind/X86_64/Dispatch.lean and proofs/Rind/Aarch64/P256Dispatch.lean — and four pinned exclude_re lines in .cargo/mutants.toml went stale where the new #[repr(u8)] lines shifted aarch64/aes.rs and x86_64/aes.rs.

Reviewed changes

• ARM AES key wiping: low/arm/aes.rs's AesKey/AesDecKey now wipe the whole enum on drop (zeroise_value + Zeroable), matching the other backends, and every backend's AES key enums — including the portable one nested in ARM's variant 0 — gain #[repr(u8)] so all-bits-zero stays a valid value while drop glue runs on the wiped tag.
• Agreement dispatch refactor: Agree moves off the mid-layer key types onto high-layer markers (X25519Curve, curve::P256/P384/P521) with an associated Key type, so cargo-modules stops attributing high-layer edges to mid-layer receivers. Dispatch, stored-key layout, and wiping are unchanged; the agreement and pkcs1 unit tests and the 12-test zeroing suite pass locally, and the armv7 and aarch64 backends cross-compile clean.
• Nightly repairs: a minimal .#dudect devShell splits dudect from .#timing's Marvin fetches; admin/ctgrind excludes rind-python, whose forced --lib test binary would need libpython; the Dart hook test treats a set-but-empty RIND_DART_CROSS_TARGETS as no targets; the OAEP test declassifies the decoded plaintext only at the assertion; and vartime_planted.rs — compiled only under admin/ct-vartime's --cfg rind_vartime_planted — is excluded from cargo-mutants.
• Formatting: pinned-nightly rustfmt import reordering in rind-aws-lc-rs and low/portable/poly1305.rs, and a doc wrap in low/cpu.rs.

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

[moq-bot]

quest land watch: the merge queue removed this pull request at 07a514e because it conflicts with main (merge_conflict).

The land fixer works on it in the background, and the watcher re-enqueues it at the back of the queue once it is fixed or judged flaky, or hands it back here with what it needs.

(written by quest land watch)

[moq-bot]

codex, gpt-6.1-sol, medium effort land fixer note:

Failure log lines 7–9:

CONFLICT (content): Merge conflict in rind-aws-lc-rs/src/rsa.rs
Auto-merging rind-aws-lc-rs/tests/keys.rs
Automatic merge failed; fix conflicts and then commit the result.

Merged base into pr-513 in a0019950fff316ab0d1cb5aa39b64264b3c88c3a. The resolution preserves the PR’s import ordering and base’s conditional ring-io import. Only that conflict required manual resolution; protected paths retain the automatic merge result, and Cargo.lock matches base.

Formatting and the Rust clippy phase of just ci base passed. The remaining CI and release build were stopped after proof validation proved unavailable: admin/prove reports charon: command not found. The pinned proof shell requires an uncached flake input; its local-only evaluation failed under restricted URI access. Full validation remains required before landing. The PR’s own prove job in the supplied log failed downloading Aeneas with HTTP 504 responses.

(written by codex, gpt-6.1-sol, medium effort)

[moq-bot]

codex, gpt-6.1-sol, medium effort land fixer: Merge conflict re·solved in a0019950fff316ab0d1cb5aa39b64264b3c88c3a, but full checks could not run: admin/prove reports "admin/prove: line 180: charon: command not found".. Recommendation: Review the prepared merge commit and run just ci base, cargo build --release --locked, and nix develop .#prove --command admin/prove with the pinned tools available.

CONFLICT (content): Merge conflict in rind-aws-lc-rs/src/rsa.rs
Auto-merging rind-aws-lc-rs/tests/keys.rs
Automatic merge failed; fix conflicts and then commit the result.

(written by codex, gpt-6.1-sol, medium effort)