[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.
• Match admin/prove's symbol index without LLVM's .llvm.<hash> suffix, so a codegen-unit reshuffle cannot make an imported routine look absent to the bytes check.

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.

• Merged main at 9a47bbc into d49afe5 after the merge queue dropped the PR on conflicts. agreement.rs keeps the merge-base design from moq-dev/rind#529: PrivateKey stores its public key, and Agree::load returns (key, public). The curve markers and Self::Key are layered on top. The hand models (Dispatch.lean, TypesExternal.lean, FunsExternal.lean, X25519.lean, P256.lean) take main's versions with this PR's renames to <marker>.Insts.RindHighAgreementAgreePrivateKey and Keyed K Key. Dispatch.lean's quote follows the merged Rust. The Dart cross-target fix sits on main's _testTarget loop. .cargo/mutants.toml keeps main's quest path, and its AES line pins are re-derived on the merged sources (same as before). Aeneas output (Types.lean, Funs.lean) is generated by admin/prove and not committed.

• Merged main again at b44efb6, which includes moq-dev/rind#571. The merge was clean.

• Main's new admin/prove bytes step (moq-dev/rind#551) then failed with a stale ALGORITHMS.md inventory: five imported routines looked absent (x86_64 edwards25519_decode, mlkem_tomont, mlkem_mulcache_compute; aarch64 bignum_modsub, p256_scalarmulbase_alt). They are all #[inline(never)] and present. Their symbols carry LLVM's .llvm.<hash> suffix, which LLVM gives a local function another codegen unit calls, and rind_index matched demangled names exactly. This PR's code changes moved items between codegen units. Main alone passes admin/prove bytes locally at b44efb6. rind_index now drops that suffix from the demangled column, which rind_symbol and the absent check both read; the mangled symbol stays for the assembly and objdump lookups. After the fix, the absent set matches main's (only bignum_modadd on both targets), and all five routines are byte-checked.

• On 955c156: quest gate nix develop --command just ci, cargo build --release --locked, and the full quest gate nix develop .#prove --command admin/prove pass, the last with all 2,476 Lean jobs, the bytes check, and HOL Light.

• quest check --base origin/main with the dev shell's quest passes, 149 documents. quest 0.2.0's newer check flags epic Required entries across main's quest tree; this PR touches no quest files.

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.
• moq-dev/rind#551 matched demangled symbols without dropping LLVM's .llvm.<hash> suffix, so a change that reshuffles codegen units marks imported routines absent.

Review

Rewritten by quest review after each round.

• Reviewer: Codex, gpt-6.1-terra, medium effort
• Session: 01a1c64d-9b43-7a00-94ab-bbc63368456b, round 2
• Head: 955c156
• Base: origin/main at bff85b3
• Score: 9/10, The review found no actionable defects in the new change; builds and tests were not run as instructed.
• Findings: none

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
Implementer: Claude Code, claude-opus-5-5, medium effort (iterate, M)
Implementer: Claude Code, claude-opus-5-5, medium effort (iterate, M)

(Written by GPT-6.1 Sol with xhigh)
(Merge update written by Claude Opus 5.5 with medium)
(Second merge and prove-bytes fix written by Claude Opus 5.5 with medium)

[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 59 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: 9eb35ee7-9f73-4cdd-b406-3adc714a6fed

Commits

Reviewing files that changed from the base of the PR and between b44efb6 and 955c156.

Files selected for processing: 26

• .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/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)