[kixelated]

An audit of every outstanding quest against the code, the open PRs, and upstream, run on 2026-11-09 with seven parallel readers, and the plan that came out of it.

The audit found no exploitable bug, no panic reachable from public input, and no hot-path speed gap on mainline x86_64 or aarch64. What it found is in landing order, milestone placement, the proof plan's cost, and corners nothing tests. This PR changes quests and one AGENTS.md rule; it changes no code.

Decisions

Each was put to the maintainer on 2026-11-09. ✅ marks the choice.

• Scope of new quests: ✅ correctness tooling, speed measurement, and portable speed (rejected: no portable speed work; correctness only).
• Where active assurance lives: ✅ m2 (rejected: redefine m3 to hold it; move only the security check).
• Proof plan staging: ✅ calibrate first, and move the cold tiers to a new m5 (rejected: calibrate only; leave the 2026-11-07 plan).
• Speed rule: ✅ run the fastest source, take a verified one only where it measures as fast at every size, and plan a proof of what runs (rejected: verified code within about 10% on cold tiers only; within 10% everywhere, as AGENTS.md said). His two newest decisions already said "never slower", so the 10% buffer was the stale rule of three.
• ML-KEM-1024 and ML-DSA: ✅ into m3/parity, beside the rustls parity quest that needs them (rejected: into m2; pushing rustls parity back to m4).
• Assurance: ✅ ACVP to m2 and cryptofuzz deleted (rejected: retarget cryptofuzz at MozillaSecurity's fork; leave both in m4). guidovranken/cryptofuzz returns 404 and OSS-Fuzz disabled its cryptofuzz project.
• wasm: ✅ supported and tested (rejected: build only; refuse it with a compile error). Another session the same day planned a compile gate with runtime tests a non-goal (moq-dev/rind#545); asked which holds, he chose ✅ both, the gate now and tests after it (rejected: compile-only). Long-term: ✅ pure Rust now, with WebCrypto left open to revisit if a browser consumer appears (rejected: record it as a permanent non-goal).
• Releases: ✅ one rind 0.4 carrying all three breaking changes, and a MoQ-side PR ready before the adapter fixes publish (rejected: the 0.4 quest alone; leaving both to release-plz). Two of the three then merged while rind's hand-set 0.3.3 was unpublished, so the release PR proposed shipping them as a patch. He first chose to revert the one on main; once the second merged, he chose ✅ to set rind to 0.4.0 by hand and hold the release for the CPU-check removal (rejected: set 0.4.0 and ship now, with that removal as 0.5; revert both and release 0.3.3). moq-dev/rind#548 sets the versions.
• New tooling quests: ✅ all four groups (assembly boundary, wiping, portable and adapters, caught before merge), in m2.
• Cold-tier speed work: ✅ m3 (rejected: m2 beside the targets; m4).
• Bindings and wiping: ✅ fix the docs only (rejected: both bindings enable rind/wipe; fix the docs and plan wiping for later). Few binding users would care about wiping, since the bytes a key is loaded from stay unwiped in managed memory; the defect is the false sentence.
• x86_64 SHA-256 proof: ✅ start on awslabs/s2n-bignum#450 at a pinned commit, and consider vendoring s2n-bignum (rejected: keep waiting for it to merge). The wait-only quest is deleted.
• Keccak's portable proof: ✅ m4, beside the SHA-3 sponge it composes with (rejected: m5 with the cold tiers; staying in m3).
• AES-GCM's other IV and tag lengths: ✅ m4's by-8 kernel quest owns them, and m3's Vale-tier quest keeps the 12-byte, full-tag glue (rejected: m3 proves them all; whichever starts first).
• P-256's order: ✅ the elementary counting route (rejected: prove Hasse's bound, which Mathlib lacks; describe both). Checked on paper, not in Lean.
• Hand models in the trust base: ✅ one quest retires them all (rejected: one quest per Aeneas limitation; leave it to the re-audit). It grew from L to XL.
• Connecting s2n-bignum's GCM spec and Vale's: ✅ prove them equal in Lean (rejected: amend the composition rule to allow a spec-equivalence axiom; leave it to the quest).
• m0 and m1: ✅ m0's definition gains a published adapter that diverges from its upstream, and quic-path joins m3's outside waits (rejected: reword m0 only; leave both).
• verify_digest and the key's hash: ✅ leave it as documented (rejected: refuse a mismatched digest in 0.4, as aws-lc-rs does). Recorded in the API epic's rejected list.
• Recurring quests: ✅ the bench refresh runs before each minor release, and the armv7 debug constant-time check becomes a weekly CI job (rejected: both per release; leave both at "end of m2", which m2's outside waits may never reach).

What changed

AGENTS.md: the speed rule, as decided above. ALGORITHMS.md drops two sentences that restated the 10% buffer, and MIGRATING.md and .cargo/mutants.toml follow moved quests.

Moved

• To m2: the confidence epic's unclaimed children, rustls-provider-panics, ACVP, asm-bytes, hash-glue, hkdf-okm, the aarch64 SHA-256 proof (now the calibration every other new HOL Light proof requires), the bench report refresh, and the armv7 debug check.
• To m3/parity: ml-kem and ml-dsa. To m3: quic-path. To m4: keccak-portable.
• To a new m5: the armv7 proof epic, MD5, SHA-1, and the tiers without AES or SHA hardware.
• quest mv refuses a claimed quest, so fuzz-every-primitive, fuzz-tiers, ct-tiers, mutants-armv7, and hol-light finish from m3. quest/m3/confidence/README.md is a stub for the first four, to delete when the last merges.

Deleted: cryptofuzz, s2n-bignum-sha2-spec, the assurance epic, whose one remaining child, OSS-Fuzz, sits in m4 directly, and the m1 MoQ epic, which finished when MoQ switched in moq-dev/moq#8250 and whose last child moved to m3. Its settled decisions stay in git history.

New quests

• m2/confidence: guard-pages, asm-abi, release-preconditions, edge-limbs, zeroing-every-byte, wipe-heap-scratch, miri-portable, portable-fuzz-mutants, adapters-hostile-input, adapter-api-diff, nightlies-on-prs.
• m2/verified: simd-models.
• m2/bench: gate, tiers, aead-sizes.
• m2/api: release-0.4. m2/adoption: bindings-wipe, targets/wasm-tests.
• m3/cold-speed: portable-limbs, portable-aes-gcm, armv7-sha.
• m4: verified/aes-gcm-aarch64-192 and verified/portable (cells the epic's own Goal covers and no quest did), and protocols/hpke-pq (the post-quantum KEMs in HPKE had no owner).

Corrected

• ## Waiting sections for seven quests whose outside condition was invisible to quest waiting, each rechecked today.
• Missing Required links: asm-bytes and sha256-block on hol-light, binsec on asm-bytes, mutants-adapters on the m0 adapters epic, fips-scope on ACVP, and several in the armv7 and post-quantum quests.
• BINSEC's scope now includes the s2n-bignum routines with no constant-time theorem.
• aes-gcm-aarch64-in-place waits on awslabs/s2n-bignum#490, which does that work upstream.
• rustls-p384-mlkem1024 and rind-openmls no longer contradict the adapters' exact-API rule.
• Stale text in hpke, openssl-provider, cfrg-hybrids, ml-kem, armv7/model, the m1 MoQ epic, the m0 adapters epic, and the verified epics' summaries.

For the open PRs

Findings this PR could not apply, because each belongs to a PR another session holds. Several merged while it was open:

• #521 and #515 merged with ! and no hand-set adapter version, as predicted; #548 sets them. #516 and #519 still need theirs.
• #529's wipe question was settled in another session by #547: every key type wipes its whole value. zeroing-every-byte here is the test side of that rule.
• #524, #525, and #527 each built their own qemu harness; just qemu has since merged and they should move onto it.
• #497's fixture calls aws_lc_rs::cpu::check(), which #522 removed.
• #516 keeps ring's wasm32_unknown_unknown_js feature a no-op because wasm did not build; now that it does, the feature must select getrandom's JavaScript backend.
• #533 merged, so the HOL Light tree exists. Its prove job is capped at 60 minutes, which dozens of proofs will not fit; the calibration quest reports the real time.
• #513 repairs seven nightly regressions on main, one a real wipe bug in ARM AES keys, and no quest tracks it.

Still open

Nothing from the audit. The proof quests' sizes are re-sized from the calibration's report, which is that quest's deliverable.

Public API and wire

None. No code changes.

Models

Size: L
Implementer: Claude Code, claude-fable-5-2, high effort

🤖 Generated with Claude Code

(Written by Claude Fable 5 with high effort)

Review

Rewritten by quest review after each round.

• Reviewer: Codex, gpt-6.1-sol, high effort
• Session: 01a1c2e5-f191-7f01-aee9-90d8c77ac496, round 4
• Head: b2af58d
• Base: origin/main at 77e4572
• Score: 10/10, The incremental branch changes update release coordination and remove references to completed work, with no actionable regressions found; no builds or tests were run.
• Findings: none

[pullfrog]

ℹ️ No critical issues — one stale guidance item and one unpropagated rule sentence.

Reviewed changes

Read the full 131-file diff end-to-end and verified it against the tree and upstream: every quest link resolves (0 missing across quest/**), the milestone READMEs match the files on disk (m2 confidence 19 children, m2 verified 5, m2 bench 4, m3 confidence stub 4, m5 verified 7), the deleted quests (cryptofuzz, s2n-bignum-sha2-spec, the assurance epic, the m4 armv7 model/curve25519 split) leave no dangling references, and the repo-internal evidence the new quests cite (hkdf.rs's four From<Okm> impls, zeroing.rs's 16-byte skip and Linux/macOS cfg, rind-dart's three false wipe sentences, SIZES/AVX_VALE_SEAL_FROM/VAES_AVX2_VALE_OPEN_BELOW, SLOWER/TIER_ROWS/TIERS in admin/bench-report, Simd.lean/Vale.lean opaque defs, rustc's wide-arithmetic wasm32 feature, CONTRIBUTING.md's release rules) all check out at the cited lines. Two reviewfrog claim-verification passes over the upstream evidence — GitHub PR states, s2n-bignum at the b4f17ee pin, crates.io, IANA, datatracker, NIST, OpenSSL docs, Firefox 155 — returned SUPPORTED on every load-bearing claim, including the cryptofuzz deletion, s2n-bignum #490/#415/#450/#492, the missing _SAFE theorems at the pin, rustls 0.23.46's provider surface, and the dalek proof fork move.

• Speed rule reversed in AGENTS.md: a formally verified source is taken only where it measures as fast at every size, otherwise the fastest runs and its proof is planned; ALGORITHMS.md drops its two 10%-allowance restatements, and each quest planned under the old rule records the reversal with its rejected alternatives.
• Assurance moved to m2: new confidence, verified, and bench epics in m2 (19, 5, and 4 children); quest mv leaves four claimed confidence quests finishing from a stub m3 README; m4's assurance epic is deleted (ACVP to m2, cryptofuzz dropped with its upstream gone), leaving OSS-Fuzz directly in m4.
• Proof plan staged: the aarch64 SHA-256 proof becomes the calibration quest every later HOL Light quest requires; the cold tiers (armv7, MD5, SHA-1, no-AES/no-SHA tiers) move to a new m5; aes-gcm-aarch64-in-place now waits on upstream s2n-bignum#490.
• ML-KEM-1024 and ML-DSA moved to m3/parity beside the rustls parity quest that needs them, with MIGRATING.md, .cargo/mutants.toml, and the pq epic following.
• New quests staged: wasm support in m2/adoption/targets, the bindings' wipe-doc fix, the rind 0.4 release-ordering quest, the nightly bench gate/tier/size quests, the tooling quests (guard pages, asm-abi, edge limbs, zeroing-every-byte, wipe-heap-scratch, miri-portable, portable-fuzz-mutants, nightlies-on-prs, adapter-api-diff), simd-models, hpke-pq, m4's portable and aes-gcm-aarch64-192.
• Waiting sections re-gated for seven quests and missing Required links added across the armv7 and post-quantum quests.

ℹ️ The reversed speed rule still stands in benchmarks/armv7-sha256.md

This PR drops ALGORITHMS.md's restatement of the 10% allowance but leaves its twin sentence in benchmarks/armv7-sha256.md (lines 4–5): "exceeding the about 10% advantage required to choose unverified code over verified code." That justification no longer exists in AGENTS.md, so the doc now states a retired rule as current — and quest/m3/cold-speed/armv7-sha.md names this doc as the record its pick lands in. The pick itself survives the new rule (HACL* measured 28–30% slower), so only the sentence is stale.

Technical details

# Stale 10%-rule sentence in benchmarks/armv7-sha256.md

## Affected sites
- benchmarks/armv7-sha256.md:4-5 — "Its latency is 28.5% lower at 64 B and 30.2% lower at 1350 B than HACL*'s, exceeding the about 10% advantage required to choose unverified code over verified code."

## Required outcome
- The doc no longer states the retired "about 10% advantage required" rule as a standing requirement.

## Suggested approach
- Mirror the ALGORITHMS.md hunk from this PR: keep the measured numbers, drop the "exceeding the about 10% advantage required…" clause.

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

[pullfrog]

This bullet's third item is already done: this PR's own edit to the epic's README removed the wasm exclusion from its Goal and replaced the non-goals line, so "this epic's README, whose Goal and non-goals still exclude wasm" no longer names anything left to correct. Drop that item and keep the two that still hold — quest/m1/moq/README.md and MIGRATE.md:56 still say wasm does not build.