diff --git a/quest/m2/adoption/README.md b/quest/m2/adoption/README.md index f820c87a4..27b6e87ea 100644 --- a/quest/m2/adoption/README.md +++ b/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 diff --git a/quest/m2/adoption/rind-dart-mobile-tests.md b/quest/m2/adoption/rind-dart-mobile-tests.md new file mode 100644 index 000000000..668d318f4 --- /dev/null +++ b/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. diff --git a/quest/m2/adoption/rind-dart-prebuilt.md b/quest/m2/adoption/rind-dart-prebuilt.md new file mode 100644 index 000000000..9032872aa --- /dev/null +++ b/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). diff --git a/quest/m2/speed/README.md b/quest/m2/speed/README.md index 87638beb9..c6ebd5968 100644 --- a/quest/m2/speed/README.md +++ b/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 diff --git a/quest/m2/speed/armv7-sha256-hacl.md b/quest/m2/speed/armv7-sha256-hacl.md new file mode 100644 index 000000000..3a2b5efa2 --- /dev/null +++ b/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. diff --git a/quest/m3/confidence/README.md b/quest/m3/confidence/README.md index 99bf3dee1..8610bb4e5 100644 --- a/quest/m3/confidence/README.md +++ 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` diff --git a/quest/m3/confidence/testing-vectors-rows.md b/quest/m3/confidence/testing-vectors-rows.md new file mode 100644 index 000000000..43f68f4ea --- /dev/null +++ b/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. diff --git a/quest/m3/verified/README.md b/quest/m3/verified/README.md index 1b6c3cf49..5ffeb1047 100644 --- a/quest/m3/verified/README.md +++ b/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` 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 diff --git a/quest/m3/verified/aes-gcm-key-vale.md b/quest/m3/verified/aes-gcm-key-vale.md new file mode 100644 index 000000000..a17a57af7 --- /dev/null +++ b/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. diff --git a/quest/m3/verified/hash-glue.md b/quest/m3/verified/hash-glue.md index 36c3de540..5ae3281ed 100644 --- a/quest/m3/verified/hash-glue.md +++ b/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//S2nBignum.lean` does. Then prove `ct_equal` from them in Lean, discharge `CtEqual`, and pin the axioms in `Rind//Axioms.lean`. -- HKDF's `From` 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 diff --git a/quest/m3/verified/hkdf-okm.md b/quest/m3/verified/hkdf-okm.md new file mode 100644 index 000000000..108604ea7 --- /dev/null +++ b/quest/m3/verified/hkdf-okm.md @@ -0,0 +1,12 @@ +# [XS] HKDF's key conversions are proven + +## Goal + +HKDF's `From` 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//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. diff --git a/quest/m4/verified/hol-light.md b/quest/m3/verified/hol-light.md similarity index 76% rename from quest/m4/verified/hol-light.md rename to quest/m3/verified/hol-light.md index ade94c4f8..c58029f03 100644 --- a/quest/m4/verified/hol-light.md +++ b/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. diff --git a/quest/m3/verified/keccak-portable.md b/quest/m3/verified/keccak-portable.md new file mode 100644 index 000000000..e1b7ca558 --- /dev/null +++ b/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. diff --git a/quest/m4/verified/README.md b/quest/m4/verified/README.md index 9abf34189..c8ea446ab 100644 --- a/quest/m4/verified/README.md +++ b/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 diff --git a/quest/m4/verified/aarch64-no-crypto.md b/quest/m4/verified/aarch64-no-crypto.md index c89d9b66f..6f4f0233e 100644 --- a/quest/m4/verified/aarch64-no-crypto.md +++ b/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 diff --git a/quest/m4/verified/aes-gcm-aarch64-in-place.md b/quest/m4/verified/aes-gcm-aarch64-in-place.md index f8d82563e..6b44bab4a 100644 --- a/quest/m4/verified/aes-gcm-aarch64-in-place.md +++ b/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 diff --git a/quest/m4/verified/aes-gcm-x86-vaes.md b/quest/m4/verified/aes-gcm-x86-vaes.md index d1bfd435a..d645b76be 100644 --- a/quest/m4/verified/aes-gcm-x86-vaes.md +++ b/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 diff --git a/quest/m4/verified/aes-modes.md b/quest/m4/verified/aes-modes.md index 78b662b78..469a6c2a7 100644 --- a/quest/m4/verified/aes-modes.md +++ b/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 diff --git a/quest/m4/verified/chacha20-poly1305-x86.md b/quest/m4/verified/chacha20-poly1305-x86.md index 7e0e7ae6a..22a0e640a 100644 --- a/quest/m4/verified/chacha20-poly1305-x86.md +++ b/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 diff --git a/quest/m4/verified/p256-x86.md b/quest/m4/verified/p256-x86.md index a6ffed40f..c06d8066d 100644 --- a/quest/m4/verified/p256-x86.md +++ b/quest/m4/verified/p256-x86.md @@ -16,4 +16,4 @@ P-256 key agreement, ECDSA signing, and ECDSA verification, which every TLS cert ## 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 diff --git a/quest/m4/verified/rsa-aarch64-mont.md b/quest/m4/verified/rsa-aarch64-mont.md index 60beb9ea0..8a02a89e8 100644 --- a/quest/m4/verified/rsa-aarch64-mont.md +++ b/quest/m4/verified/rsa-aarch64-mont.md @@ -13,4 +13,4 @@ aws-lc's aarch64 `bn_mul_mont`, which rind runs for every RSA modulus there, is ## 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 diff --git a/quest/m4/verified/rsa-x86-ifma.md b/quest/m4/verified/rsa-x86-ifma.md index ebbadf2c1..0cd6994e7 100644 --- a/quest/m4/verified/rsa-x86-ifma.md +++ b/quest/m4/verified/rsa-x86-ifma.md @@ -13,5 +13,5 @@ On x86_64 CPUs with AVX-512 IFMA (Ice Lake and later, Zen 4 and later), where bo ## 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 - [RSA signing, decryption, and key generation are proven](/quest/m4/verified/rsa-sign.md) - the CRT glue this exponentiation slots into diff --git a/quest/m4/verified/rsa-x86-mont.md b/quest/m4/verified/rsa-x86-mont.md index 25b0f9105..c7f184bdb 100644 --- a/quest/m4/verified/rsa-x86-mont.md +++ b/quest/m4/verified/rsa-x86-mont.md @@ -13,4 +13,4 @@ Every RSA Montgomery product x86_64 runs outside s2n-bignum's Karatsuba routines ## 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 diff --git a/quest/m4/verified/sha1.md b/quest/m4/verified/sha1.md index a2ec0e1ef..ee9c0bc34 100644 --- a/quest/m4/verified/sha1.md +++ b/quest/m4/verified/sha1.md @@ -18,4 +18,4 @@ Each enters as the `ShaBlocks` hypothesis's SHA-1 half does today, which this re ## 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 diff --git a/quest/m4/verified/sha256-aarch64-hw.md b/quest/m4/verified/sha256-aarch64-hw.md index 835528993..1bf5150e6 100644 --- a/quest/m4/verified/sha256-aarch64-hw.md +++ b/quest/m4/verified/sha256-aarch64-hw.md @@ -14,4 +14,4 @@ SHA-256, and HMAC, HKDF, and PBKDF2 over it, earn the ✓ on aarch64 with the cr ## 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 diff --git a/quest/m4/verified/sha256-x86-avx2.md b/quest/m4/verified/sha256-x86-avx2.md index 660799283..0fb41f419 100644 --- a/quest/m4/verified/sha256-x86-avx2.md +++ b/quest/m4/verified/sha256-x86-avx2.md @@ -14,4 +14,4 @@ SHA-256, and HMAC, HKDF, and PBKDF2 over it, earn the ✓ on x86_64 CPUs with AV ## 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 diff --git a/quest/m4/verified/sha512-aarch64-hw.md b/quest/m4/verified/sha512-aarch64-hw.md index 2c6294c18..a652386bc 100644 --- a/quest/m4/verified/sha512-aarch64-hw.md +++ b/quest/m4/verified/sha512-aarch64-hw.md @@ -14,4 +14,4 @@ SHA-384, SHA-512, and SHA-512/256, and with them Ed25519 and HMAC and HKDF over ## 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 diff --git a/quest/m4/verified/sha512-x86-avx2.md b/quest/m4/verified/sha512-x86-avx2.md index 6ae05c357..9a0dcaf00 100644 --- a/quest/m4/verified/sha512-x86-avx2.md +++ b/quest/m4/verified/sha512-x86-avx2.md @@ -14,4 +14,4 @@ SHA-384, SHA-512, and SHA-512/256, and with them Ed25519 and HMAC and HKDF over ## 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 diff --git a/quest/m4/verified/x86-no-aesni.md b/quest/m4/verified/x86-no-aesni.md index 8d65e5adf..832daa6a4 100644 --- a/quest/m4/verified/x86-no-aesni.md +++ b/quest/m4/verified/x86-no-aesni.md @@ -13,5 +13,5 @@ AES-GCM, AES header protection, and the AES modes earn the ✓ on x86_64 CPUs wi ## 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 AES-GCM glue and specs this tier reuses