chore(quest): plan the follow-ups of the 2026-11-07 merges

quest/m2/adoption/README.md

@@ -74,6 +74,8 @@ don't ask again (✅ is the chosen option):
 - [pyca-compatible pyrind](/quest/m2/adoption/pyrind-cryptography.md) - pyca's `hazmat` names on pyrind
 - [Talk to pyca about rind](/quest/m2/adoption/pyca.md) - a discussion with pyca/cryptography's maintainers
 - [rind for Dart and Flutter](/quest/m2/adoption/rind-dart.md) - the `rind` package on pub.dev
+- [rind for Dart installs without a Rust toolchain](/quest/m2/adoption/rind-dart-prebuilt.md) - prebuilt, hash-pinned libraries fetched by the build hook
+- [rind for Dart is tested on Android and iOS](/quest/m2/adoption/rind-dart-mobile-tests.md) - the Dart tests on an emulator and simulator
 - [rind as a Dart `cryptography` backend](/quest/m2/adoption/rind-dart-cryptography.md) - the `cryptography` package's interface on rind
 - [Apache Iggy encrypts streams with rind](/quest/m2/adoption/iggy.md) - its AES-256-GCM message encryption on rind
 - [librespot builds rustls without ring](/quest/m2/adoption/librespot.md) - users pick their rustls provider

quest/m2/adoption/rind-dart-mobile-tests.md

@@ -0,0 +1,11 @@
+# [S] rind for Dart is tested on Android and iOS
+
+## Goal
+
+The `rind` Dart package's tests run on an Android emulator (including a 32-bit armv7 image) and the iOS simulator in CI, through a Flutter integration-test app, so mobile pointer handling and the build hook's mobile paths are executed, not only compiled.
+
+## Plan
+
+Planned with the maintainer on 2026-11-07, a follow-up of [moq-dev/rind#462](https://github.com/moq-dev/rind/pull/462): its nightly job cross-builds and checks every architecture but runs the tests only on desktop hosts, so armv7's 32-bit pointers are never exercised.
+
+- Reuse the iOS-simulator and Android jobs rind's own CI already runs ([moq-dev/rind#432](https://github.com/moq-dev/rind/pull/432)) where they fit.

quest/m2/adoption/rind-dart-prebuilt.md

@@ -0,0 +1,12 @@
+# [M] rind for Dart installs without a Rust toolchain
+
+## Goal
+
+The `rind` Dart package's build hook downloads a prebuilt native library for the target, pinned by hash in the package, so Flutter and Dart app builders need no Rust toolchain. Building from source stays available as an explicit opt-in user-define, never a silent fallback when a download fails.
+
+## Plan
+
+Planned with the maintainer on 2026-11-07, a follow-up of [moq-dev/rind#462](https://github.com/moq-dev/rind/pull/462), which builds from source; needing Rust and its mobile targets is the largest barrier for app builders.
+
+- Release CI builds each target's library, records its hash in the package, and attaches it to the release; the hook refuses a library whose hash doesn't match.
+- Targets: those the package already cross-builds (Android, iOS, macOS, Linux, Windows).

quest/m2/speed/README.md

@@ -58,3 +58,4 @@ dual RSAZ only when the runner has IFMA.
 
 - [The Ed25519 verify benchmark times every library the same way](/quest/m2/speed/ed25519-verify-bench.md) - rind's row parses the key inside the loop
 - [HKDF-SHA256 expand is back to its earlier speed on x86_64](/quest/m2/speed/hkdf-expand-regression.md) - desktop measured 47 to 66 ns between two runs; confirm on a runner, then bisect
+- [armv7 without the crypto extension runs the fastest SHA-256](/quest/m2/speed/armv7-sha256-hacl.md) - Graviola's or HACL*'s, measured

quest/m2/speed/armv7-sha256-hacl.md

@@ -0,0 +1,11 @@
+# [XS] armv7 without the crypto extension runs the fastest SHA-256
+
+## Goal
+
+On armv7 without the ARMv8 crypto extension, rind's SHA-256 runs whichever of Graviola's routine and HACL*'s is fastest, by the verified-source rule: HACL*'s unless Graviola's is more than about 10% faster. `ALGORITHMS.md` and the bench rows show the pick.
+
+## Plan
+
+Planned with the maintainer on 2026-11-07, a follow-up of [moq-dev/rind#458](https://github.com/moq-dev/rind/pull/458): the portable backend took HACL*'s SHA-256 in place of Graviola's, but armv7 without the crypto extension kept Graviola's unmeasured.
+
+- Time both on armv7 in 32-bit mode on the arm64 runner (as the speed epic's hardware rule says), at 64 B and 1350 B.

quest/m3/confidence/README.md

@@ -27,3 +27,4 @@ All three constant-time tools state they can't see variable-time instructions. O
 - [Mutation testing on AVX-512](/quest/m3/confidence/mutants-avx512.md) - the AVX-512 paths no campaign host runs, under Intel SDE
 - [Mutation testing on armv7](/quest/m3/confidence/mutants-armv7.md) - the code only 32-bit ARM compiles, under qemu-arm
 - [Mutation testing of DIT](/quest/m3/confidence/mutants-dit.md) - DIT detection and setting, on cores that have it
+- [TESTING.md lists the CCTV and imported vector sets](/quest/m3/confidence/testing-vectors-rows.md) - rows for `thirdparty/cctv` and `thirdparty/vectors`

quest/m3/confidence/testing-vectors-rows.md

@@ -0,0 +1,9 @@
+# [XS] TESTING.md lists the CCTV and imported vector sets
+
+## Goal
+
+`TESTING.md` maps `thirdparty/cctv` and `thirdparty/vectors` (aws-lc's and BoringSSL's files) to the primitives and tiers they cover, as it does every other suite.
+
+## Plan
+
+Follow-up of [moq-dev/rind#481](https://github.com/moq-dev/rind/pull/481), which added those suites but left `TESTING.md` alone while [moq-dev/rind#454](https://github.com/moq-dev/rind/pull/454), which writes `TESTING.md`, was open; both are queued, #454 first. It joins the confidence epic, the epic of the PR that suggested it.

quest/m3/verified/README.md

@@ -41,7 +41,11 @@ Decided with the maintainer on 2026-11-03, after the benchmark report (`BENCHMAR
 
 ## Required
 
+- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m3/verified/hol-light.md) - where the proofs this epic writes for unproven assembly live, checked by `admin/prove`
 - [The hash and KDF glue's constant-time compares are proven](/quest/m3/verified/hash-glue.md) - the compares behind `hmac::verify` and `pbkdf2::Secret::verify`, in HOL Light
+- [HKDF's key conversions are proven](/quest/m3/verified/hkdf-okm.md) - the `From<Okm>` keys QUIC's packet protection starts from
 - [x86_64 SHA-NI SHA-256 block function is proven](/quest/m3/verified/sha256-block.md) - today's routine proven on s2n-bignum's SHA-256 spec, or a proven one as fast
 - [AES-GCM of 2^32 bytes and more is proven on the Vale tier](/quest/m3/verified/aes-gcm-vale-long.md) - drops the ✓'s size caveat
+- [AES-GCM's custom-IV key is proven on the Vale tier](/quest/m3/verified/aes-gcm-key-vale.md) - `aead::gcm::Key`, for 12-byte IVs and any others
 - [ECDSA's theorems rest on the SHA-256 spec](/quest/m3/verified/sha256-spec-unify.md) - one SHA-256 spec, so ECDSA composes with the hash proof
+- [The portable backend's Keccak-f is proven or replaced](/quest/m3/verified/keccak-portable.md) - SHA-3 and ML-KEM on every architecture without rind assembly

quest/m3/verified/aes-gcm-key-vale.md

@@ -0,0 +1,12 @@
+# [S] AES-GCM's custom-IV key is proven on the Vale tier
+
+## Goal
+
+`aead::gcm::Key`'s seal and open are proven on the Vale tier for 12-byte IVs and full 16-byte tags, where they call the proven `aead::Key`. Its other IV lengths and truncated tags, which run `encrypt_any` and `decrypt_any` (`rind/src/mid/aes_gcm.rs`), are proven too or recorded as a gap with its reason in the proof coverage.
+
+## Plan
+
+Planned with the maintainer on 2026-11-07, a follow-up of [moq-dev/rind#477](https://github.com/moq-dev/rind/pull/477), which proved `seal_in_place_append_tag` on the Vale tier.
+
+- The 12-byte, full-tag case is mostly glue over `aead::Key`'s theorems.
+- `encrypt_any`/`decrypt_any` derive the counter block from GHASH over the IV and may truncate the tag; prove them if the Vale-tier model reaches, otherwise record the gap so the ✓ names its scope.

quest/m3/verified/hash-glue.md

@@ -12,12 +12,11 @@ Planned with the maintainer on 2026-11-03 from the audit.
 
 - Prove `ct_compare_bytes` and `ct_compare_16` in HOL Light on each target: the result is zero exactly when the inputs are equal, and the routine runs in constant time.
 - Restate those proofs as axioms about the Rust wrappers, as `Rind/<Arch>/S2nBignum.lean` does. Then prove `ct_equal` from them in Lean, discharge `CtEqual`, and pin the axioms in `Rind/<Arch>/Axioms.lean`.
-- HKDF's `From<Okm>` impls for `aead::Key`, `aead::quic::HeaderProtectionKey`, and `hmac::Key` (`rind/src/high/hkdf.rs`) are unproven: prove each fills its key from `kdf.hkdf_fill`'s bytes. They need no HOL Light and can land first.
-- `Rind/X86_64/Sha512.lean` keeps its own SHA-512 padding and buffering lemmas (`sha512_pad_spec`, `sha512_split_tail_spec`, `sha512_complete_blocks_spec`). `Blockwise.lean`'s generic ones could replace them in the same PR, or the work can be dropped.
+- `Rind/X86_64/Sha512.lean` keeps its own SHA-512 padding and buffering lemmas (`sha512_pad_spec`, `sha512_split_tail_spec`, `sha512_complete_blocks_spec`). Replacing them with `Blockwise.lean`'s generic ones was dropped on [moq-dev/rind#476](https://github.com/moq-dev/rind/pull/476): the proofs hold, and only duplication would go.
 
 ## Required
 
-- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m4/verified/hol-light.md) - where the HOL Light proofs live and CI checks them
+- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m3/verified/hol-light.md) - where the HOL Light proofs live and CI checks them
 
 ## Related
 

quest/m3/verified/hkdf-okm.md

@@ -0,0 +1,12 @@
+# [XS] HKDF's key conversions are proven
+
+## Goal
+
+HKDF's `From<Okm>` impls for `aead::Key`, `aead::quic::HeaderProtectionKey`, and `hmac::Key` (`rind/src/high/hkdf.rs`) are proven in `proofs/` to fill each key from `kdf.hkdf_fill`'s bytes, composing with the HKDF theorems in `Rind/<Arch>/Hkdf.lean`, on x86_64 and aarch64.
+
+## Plan
+
+Split out of [the hash-glue quest](/quest/m3/verified/hash-glue.md) with the maintainer on 2026-11-07, after [moq-dev/rind#476](https://github.com/moq-dev/rind/pull/476): these conversions need no HOL Light, so they shouldn't wait behind [hol-light.md](/quest/m3/verified/hol-light.md) as the compares do.
+
+- Each impl is a thin wrapper over `fill`; prove it with the same Aeneas translation and `admin/prove` flow #476 used.
+- The resulting keys feed QUIC's packet protection, so state the theorem in terms the AEAD and header-protection proofs can consume.

quest/m4/verified/hol-light.md → quest/m3/verified/hol-light.md

@@ -2,10 +2,12 @@
 
 ## Goal
 
-The HOL Light proofs this epic writes for routines s2n-bignum lacks (aws-lc's, OpenSSL's, and BoringSSL's assembly, generalizations of s2n-bignum's own theorems, and additions to its instruction models) live in `proofs/hol-light/` in rind. `admin/prove` checks them beside the Lean proofs, against the object code rind imports, so `proofs/`'s axioms cite them as they cite s2n-bignum's.
+The HOL Light proofs rind writes for routines s2n-bignum lacks (aws-lc's, OpenSSL's, and BoringSSL's assembly, generalizations of s2n-bignum's own theorems, and additions to its instruction models) live in `proofs/hol-light/` in rind. `admin/prove` checks them beside the Lean proofs, against the object code rind imports, so `proofs/`'s axioms cite them as they cite s2n-bignum's.
 
 ## Plan
 
+Moved from m4 into m3 with the maintainer on 2026-11-07: [the hash-glue quest](/quest/m3/verified/hash-glue.md)'s constant-time compares are its first consumer, so the tree starts there.
+
 Decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448): an in-repo tree run by `admin/prove`, not a `moq-dev/s2n-bignum` fork.
 
 - s2n-bignum's model, tactics, and specs come in pinned, as a Nix input or submodule at a recorded commit, or vendored if pinning cannot build. Either way the pin is one recorded revision that the proofs and `benchmarks/verified.toml` name.

quest/m3/verified/keccak-portable.md

@@ -0,0 +1,12 @@
+# [M] The portable backend's Keccak-f is proven or replaced
+
+## Goal
+
+The portable backend's Keccak-f permutation (`rind/src/low/portable/keccak.rs`, hand-ported) is either proven against a Keccak-f[1600] spec, or replaced by a verified implementation (such as libcrux/HACL*'s) that is no more than about 10% slower, so no portable path runs an unverified Keccak-f under SHA-3 and ML-KEM.
+
+## Plan
+
+Planned with the maintainer on 2026-11-07, a follow-up of [moq-dev/rind#458](https://github.com/moq-dev/rind/pull/458), which added the portable backend and left this the only unverified Keccak-f on a portable path.
+
+- Measure the candidates on the portable backend first (forced on x86_64 and on an aarch64 runner); AGENTS.md's rule applies: prefer the verified source unless another is more than about 10% faster.
+- If the hand port stays, prove it with Aeneas against the same spec [the SHA-3 sponge quest](/quest/m4/verified/sha3-sponge.md) uses, so the two compose.

quest/m4/verified/README.md

@@ -8,11 +8,11 @@ Every operation rind exports, on every backend and CPU tier, earns `benchmarks/v
 
 Decided with the maintainer on 2026-11-07, planning m4's long-term work with no token budget. This reopens the m3 audit's "accepted unless a route changes it" list: VAES AES-GCM, SIMD ChaCha20-Poly1305, SHA-256 and SHA-1 on every tier, RSA end to end, ML-KEM's construction, P-384 and P-521 glue, x86_64 P-256, armv7's curves, the AES and GHASH fallbacks, and the rest.
 
-- Prove the fast code rind runs; never swap in slower verified code to earn a ✓. Where no proof of a routine exists, write one in HOL Light, in [`proofs/hol-light/`](/quest/m4/verified/hol-light.md), or in Lean. Offering it upstream is optional, with no standing approval: each quest stops and asks the maintainer before posting to awslabs/s2n-bignum or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)).
+- Prove the fast code rind runs; never swap in slower verified code to earn a ✓. Where no proof of a routine exists, write one in HOL Light, in [`proofs/hol-light/`](/quest/m3/verified/hol-light.md), or in Lean. Offering it upstream is optional, with no standing approval: each quest stops and asks the maintainer before posting to awslabs/s2n-bignum or anywhere outside the moq-dev and kixelated orgs (decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448)).
 - The m3 epic's settled choices hold: Aeneas to Lean for rind's Rust, and its composition rule.
 - Audit ([moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448), 2026-11-06), counting [the m3 epic](/quest/m3/verified/README.md)'s open quests as done: the ✓ then holds for X25519 and ChaCha20 header protection on x86_64 and aarch64, P-256 on aarch64, AES-GCM on x86_64's Vale tier, SHA-256 and its MACs and KDFs on x86_64 with SHA-NI, and SHA-384/512 and Ed25519 on Intel x86_64 with AVX but not AVX2 and on aarch64 without the SHA-512 instructions. Every other cell is a child below, ranked by how often the operation and tier run.
   - Upstream since m3: s2n-bignum proves aarch64 AES-GCM against SP 800-38D, out of place only, and models the aarch64 SHA-512 instructions; its FIPS 180-4 specs and x86_64 SHA-NI proof ([awslabs/s2n-bignum#415](https://github.com/awslabs/s2n-bignum/pull/415), [#420](https://github.com/awslabs/s2n-bignum/pull/420), [#450](https://github.com/awslabs/s2n-bignum/pull/450)) are still open. No proof covers the ChaCha20-Poly1305 or VAES AES-GCM assembly rind runs, or any aarch64 ChaCha20 or Poly1305; aws-lc-verification and HACL\* have added nothing rind runs.
-  - Most children write HOL Light for assembly no one has proven. Decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448): those proofs live in [`proofs/hol-light/`](/quest/m4/verified/hol-light.md), run by `admin/prove` beside the Lean proofs over a pinned or vendored s2n-bignum, not in a fork. The SHA-2 children may pin [awslabs/s2n-bignum#415](https://github.com/awslabs/s2n-bignum/pull/415)'s and [#420](https://github.com/awslabs/s2n-bignum/pull/420)'s unmerged specs by commit, moving to the merged versions when they land, with the ✓ noting the pin.
+  - Most children write HOL Light for assembly no one has proven. Decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448): those proofs live in [`proofs/hol-light/`](/quest/m3/verified/hol-light.md), run by `admin/prove` beside the Lean proofs over a pinned or vendored s2n-bignum, not in a fork. The SHA-2 children may pin [awslabs/s2n-bignum#415](https://github.com/awslabs/s2n-bignum/pull/415)'s and [#420](https://github.com/awslabs/s2n-bignum/pull/420)'s unmerged specs by commit, moving to the merged versions when they land, with the ✓ noting the pin.
   - Parsing and randomness stay outside the ✓, as `benchmarks/verified.toml` defines it.
   - No algorithm from [post-quantum](/quest/m4/pq/README.md) or [protocols](/quest/m4/protocols/README.md) has landed. Decided with the maintainer on 2026-11-07 on [moq-dev/rind#448](https://github.com/moq-dev/rind/pull/448): [a recurring re-audit](/quest/m4/verified/re-audit.md) at the end of each milestone covers them as they land, rather than each algorithm's quest stating its own route.
 
@@ -21,7 +21,6 @@ Decided with the maintainer on 2026-11-07, planning m4's long-term work with no
 - [rind's assembly is byte-identical to the proven object code](/quest/m4/verified/asm-bytes.md) - the transliteration leaves the trust base
 - [Aeneas translates function pointers](/quest/m4/verified/aeneas-fn-pointers.md) - the hand models of rind's dispatch retire
 - [Re-audit what's left to prove, end of m3](/quest/m4/verified/re-audit.md) - recurring: what still lacks a ✓, new algorithms included, planned as children
-- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m4/verified/hol-light.md) - where the proofs this epic writes for unproven assembly live, checked by `admin/prove`
 - [AES and QUIC AES header protection are proven with AES hardware](/quest/m4/verified/aes-header-protection.md) - every QUIC packet's mask on x86_64 and aarch64
 - [x86_64's by-8 and by-16 AES-GCM intrinsics are proven](/quest/m4/verified/aes-gcm-x86-intrinsics.md) - AES-GCM without AVX, and the Vale tier's short seals, AES-192, odd IVs, and truncated tags
 - [AES-GCM on x86_64 with VAES is proven](/quest/m4/verified/aes-gcm-x86-vaes.md) - BoringSSL's VAES kernels, the common x86_64 tier

quest/m4/verified/aarch64-no-crypto.md

@@ -13,5 +13,5 @@ Every operation earns the ✓ on aarch64 cores without the crypto extension (the
 
 ## Required
 
-- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m4/verified/hol-light.md) - where the HOL Light proofs live and CI checks them
+- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m3/verified/hol-light.md) - where the HOL Light proofs live and CI checks them
 - [AES-GCM on aarch64 is proven](/quest/m4/verified/aes-gcm-aarch64.md) - the AEAD glue this tier shares

quest/m4/verified/aes-gcm-aarch64-in-place.md

@@ -14,4 +14,4 @@ s2n-bignum's aarch64 AES-GCM kernels, which rind runs with the same input and ou
 
 ## Required
 
-- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m4/verified/hol-light.md) - where the HOL Light proofs live and CI checks them
+- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m3/verified/hol-light.md) - where the HOL Light proofs live and CI checks them

quest/m4/verified/aes-gcm-x86-vaes.md

@@ -15,5 +15,5 @@ AES-GCM earns the ✓ on x86_64 CPUs with VAES and VPCLMULQDQ (Ice Lake and late
 
 ## Required
 
-- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m4/verified/hol-light.md) - where the HOL Light proofs live and CI checks them
+- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m3/verified/hol-light.md) - where the HOL Light proofs live and CI checks them
 - [x86_64's by-8 and by-16 AES-GCM intrinsics are proven](/quest/m4/verified/aes-gcm-x86-intrinsics.md) - the short messages this tier hands to them

quest/m4/verified/aes-modes.md

@@ -12,5 +12,5 @@
 
 ## Required
 
-- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m4/verified/hol-light.md) - where the HOL Light proofs live and CI checks them
+- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m3/verified/hol-light.md) - where the HOL Light proofs live and CI checks them
 - [AES and QUIC AES header protection are proven with AES hardware](/quest/m4/verified/aes-header-protection.md) - the block cipher and its intrinsic models

quest/m4/verified/chacha20-poly1305-x86.md

@@ -15,4 +15,4 @@ ChaCha20-Poly1305 and XChaCha20-Poly1305, TLS's and QUIC's other AEAD, and `ciph
 
 ## Required
 
-- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m4/verified/hol-light.md) - where the HOL Light proofs live and CI checks them
+- [rind's own HOL Light proofs live in proofs/hol-light](/quest/m3/verified/hol-light.md) - where the HOL Light proofs live and CI checks them