Skip to content

chore(quest): audit what m4 has left to prove, one quest per gap - #448

Merged
kixelated merged 6 commits into
mainfrom
quest/m4/verified/audit
Nov 7, 2026
Merged

chore(quest): audit what m4 has left to prove, one quest per gap#448
kixelated merged 6 commits into
mainfrom
quest/m4/verified/audit

Conversation

@kixelated

@kixelated kixelated commented Nov 7, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Finishes quest/m4/verified/audit.md: every operation, backend, and CPU tier still without a ✓ once the m3 verified epic's open quests land, the code each runs, what is already proven, and the cheapest route to a proof of that same code. It plans one leaf quest per gap under the m4 epic, most-used first, and summarizes the result in the epic's Plan.

Impact

Quest files only. No public API or wire change.

Approach

  • Started from benchmarks/verified.toml, ALGORITHMS.md's tables and Sources, proofs/README.md, and moq-dev/rind#318. Re-checked dispatch in rind/src/{low,mid,high} where ALGORITHMS.md was not specific enough (AES header protection, x86_64 P-256's k·G and d·Q, RSA's product choice by width, cipher::ChaCha20's kernels).
  • Surveyed upstream at each project's head (2026-11-06). rind's pins are already heads: s2n-bignum b4f17ee7, aws-lc-verification 79730247, and HACL* f5572590.
  • Counted the m3 epic's open quests as done: hash glue, x86_64 SHA-NI SHA-256, AES-GCM append tag, AES-GCM of 2^32 bytes and more, and ECDSA on the SHA-256 spec.

Report

What has the ✓ after m3

  • X25519 and ChaCha20 header protection on x86_64 and aarch64.
  • P-256 ECDH and ECDSA on aarch64.
  • AES-GCM on x86_64 with AVX and MOVBE but without VAES.
  • SHA-256 and HMAC, HKDF, and PBKDF2 over it on x86_64 with SHA-NI.
  • 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 gap. Parsing and randomness stay outside the ✓, as verified.toml defines it.

Upstream since m3

Project New since m3 What it changes
s2n-bignum aarch64 AES-GCM proven CORRECT and SAFE against SP 800-38D (#470, #440, #445, #482, #485). Every theorem still requires nonoverlapping input and output. The kernels' contract is a full GCM spec; in place is still unproven.
s2n-bignum The aarch64 model decodes sha512h, sha512h2, sha512su0, and sha512su1, and the SHA-3, AES, and PMULL instructions. The x86_64 model decodes broad AVX2 and VEX.256 VPCLMULQDQ, but no VAES, EVEX, IFMA, or SHA-NI. aarch64 SHA-512 can be proven in HOL Light with no model work. x86_64 VAES, AVX-512, and IFMA need model work.
s2n-bignum FIPS 180-4 specs and SHA routines are still open: #415 (SHA-256 spec, draft), #420 (SHA-512 spec and a scalar routine, open), #450 (SHA-NI, draft, quiet since 2026-09-08). Every SHA-2 quest builds on these specs at a pinned commit.
s2n-bignum ML-DSA routines ported from mldsa-native (#423, #426, #429). AVX-512 Keccak is open (#468). For the post-quantum epic once ML-DSA lands.
aws-lc-verification Nothing merged since 2026-03. No work on the aarch64 SHA-512 store. That gap needs a new proof.
HACL* and Vale Only fixes to false admitted lemmas in P-256, Ed25519, and secp256k1 (hacl-star#1080, #1081). No new VAES, SHA-2, or vector ChaCha20-Poly1305 routine.
mldsa-native, mlkem-native HOL Light coverage of the full ML-DSA poly set on both architectures. mlkem-native has no aarch64 compress. ML-DSA is ready for the post-quantum epic.
ChaCha20, Poly1305 No proof of aws-lc's stitched routines or of any aarch64 ChaCha20 or Poly1305. Vale's x86_64 Poly1305 and libjade's AVX2 ChaCha20 and Poly1305 (The Last Mile) are proven but unchanged since m3, and run separate passes. Measure them first; otherwise two new specs plus proofs (XL).
curve25519-dalek Lean proofs through Aeneas of 191 of 194 functions, serial 64-bit backend only. Reusable lemmas for armv7's 32-bit backend; nothing for AVX2.
Aeneas and Charon Charon now translates function pointers and Fn* vtables. Aeneas still rejects &dyn method calls (aeneas#1500). Input for Aeneas translates function pointers.
SymCrypt Its Aeneas-verified SHA-3 and ML-KEM live on a branch (README-VERIFIEDCRYPTO.md: about 15k lines of Lean for SHA-3 and 38k for ML-KEM, with an intrinsics model). rind's sponge and construction proofs can reuse its FIPS 202 and 203 specs.

Gaps, routes, and quests

Ranked by how often the operation and tier run, as the epic's Required list is. "HOL" means a HOL Light proof in s2n-bignum's model, and "Aeneas" means Aeneas to Lean in proofs/. Sizes follow the quest guide's agent-effort scale.

# Operation, tier Code it runs Already proven Cheapest route Size Quest
0 (enabler) - - proofs/hol-light/ in rind, checked by admin/prove over a pinned or vendored s2n-bignum M hol-light
1 QUIC AES header protection and cipher::Aes, x86_64 AES-NI and aarch64 crypto Graviola's AES-NI and NEON aese intrinsics, rind's key schedules x86_64 AES-128/256 expansion and block (AesKey.lean, AesNi.lean) Aeneas: reuse them, add AES-192 and decryption; model aese/aesmc on aarch64 M aes-header-protection
2 AES-GCM: x86_64 without AVX, plus the Vale tier's short seals, AES-192, odd IVs, and truncated tags Graviola's by-8 and AVX-512 by-16 intrinsics Key setup, partial blocks, and AEAD glue on the Vale tier Aeneas over Simd.lean's intrinsic models L aes-gcm-x86-intrinsics
3 AES-GCM, x86_64 with VAES (Zen 3+, Ice Lake+) BoringSSL aes_gcm_*_vaes_avx2/_avx512 and gcm_init_vpclmulqdq_*, the #2 kernels, Vale for short opens Vale's kernel only HOL: add VEX.256 VAES (then EVEX) to the model and prove BoringSSL's kernels on common/gcm.ml; Aeneas for the glue and kernel choice XL aes-gcm-x86-vaes
4 AES-GCM in place, aarch64 s2n-bignum kernels with in == out Kernels, out of place HOL: generalize the theorems to aliasing; retire inplace.py M aes-gcm-aarch64-in-place
5 AES-GCM, aarch64 crypto rind's NEON key setup, PMULL table, J0, AAD, partial blocks, tag, and its ≤15/31-block one-pass Rust Kernels Aeneas, with NEON intrinsics modelled L aes-gcm-aarch64
6 SHA-256 and its MACs/KDFs, aarch64 crypto aws-lc sha256_block_data_order_hw (123 instructions) Instruction semantics only HOL on #415's spec (estimated 3-5 person-weeks) L sha256-aarch64-hw
7 SHA-384/512, Ed25519, HMAC-SHA384, aarch64 with the SHA-512 instructions aws-lc sha512_block_data_order_hw NSym, up to the store HOL on #420's spec; the model already has the instructions L sha512-aarch64-hw
8 SHA-384/512, Ed25519, x86_64 with AVX2 (all Zen, Intel from Haswell) OpenSSL sha512_block_data_order_avx2 (1.15-1.47x the proven AVX and scalar routines) Nothing (SAW covers the AVX path only) HOL on #420's spec L sha512-x86-avx2
9 SHA-256, x86_64 AVX2 without SHA-NI (Haswell through Cascade Lake) OpenSSL sha256_block_data_order_avx2 Nothing HOL on #415's spec L sha256-x86-avx2
10 SHA3-256/384/512, ML-KEM's hashes and XOFs Graviola's sponge (mid/sha3.rs, about 670 lines) Every Keccak-f routine Aeneas against FIPS 202, reusing SymCrypt's spec L sha3-sponge
11 ML-KEM-768 (rind-rustls's default key exchange), aarch64 and x86_64 AVX2 FIPS 203 construction, FO transform, CBD, SampleNTT driver, Rust encodings (about 1,100 lines) Every polynomial routine (s2n-bignum, mlkem-native) Aeneas against FIPS 203, reusing SymCrypt's spec and lemmas; prove the zetas tables XL mlkem-construction
12 ML-KEM-768, x86_64 with AVX-512 VBMI2 Graviola 8-way Keccak and rejection sampler (about 320 lines of intrinsics) Nothing Aeneas over AVX-512 intrinsic models L mlkem-avx512-sampler
13 P-256 ECDH and ECDSA, x86_64 aws-lc ecp_nistz256_{,avx2_}select_w7, point_add_affine{,x}, rind's Booth-7 driver over a 152 KB table; p256_montjscalarmul and rind's to-affine s2n-bignum routines; all the shared Rust on aarch64 Measure the proven p256_scalarmul for d·Q; HOL for aws-lc's k·G routines; Aeneas for the driver and the x86_64 table L p256-x86
14 RSA PKCS#1 and PSS verification Public square-and-multiply, Knuth D montifier, EMSA checks, MGF1 RSA-2048's products on x86_64 with ADX (s2n-bignum Karatsuba) Aeneas against RFC 8017; ✓ on x86_64 ADX for RSA-2048 L rsa-verify
15 RSA, aarch64 aws-lc bn_mul_mont (1.15-2x s2n-bignum's) Nothing HOL, scalar instructions only L rsa-aarch64-mont
16 ChaCha20-Poly1305, XChaCha20, cipher::ChaCha20, x86_64 with SSE4.1 aws-lc stitched AVX2/SSE4.1 assembly, rind's AVX2 ChaCha20 kernels, aws-lc SSSE3 4x HACL* rounds; libjade (AVX2) and Vale (scalar Poly1305) prove other x86_64 code Measure libjade and Vale; otherwise HOL: new RFC 8439 ChaCha20 and Poly1305 specs and the routines; Aeneas for glue and intrinsics XL chacha20-poly1305-x86
17 Same, aarch64 aws-lc NEON assembly, Graviola NEON ChaCha20 HACL* rounds HOL on #16's specs; Aeneas XL chacha20-poly1305-aarch64
18 Trust base: P256Order, Ed25519 group membership (assumptions inside existing ✓s) HOL Light's theorems, not Lean's Lean: Hasse's bound (or Mathlib's), group closure M curve-groups
19 RSA signing, OAEP, key generation CRT, 5-bit window, gathers, verify-after-sign, EMSA and OAEP encoding, key checks, generate Products and gather on x86_64 ADX Aeneas; key generation's spec is its output's relations XL rsa-sign
20 RSA signing, x86_64 with AVX-512 IFMA aws-lc dual RSAZ rsaz_amm52x*_x2_ifma256, extract_multiplier_* Nothing HOL: add EVEX and IFMA to the model; Aeneas for the driver XL rsa-x86-ifma
21 SHA-384/512, x86_64 with the SHA512 instructions OpenSSL sha512_block_data_order_sha512ext Nothing HOL: add vsha512* to the model L sha512-x86-ext
22 P-384 ECDH and ECDSA, x86_64 and aarch64 rind's comb, select intrinsics, double multiplication, to-affine Every s2n-bignum routine Aeneas, reusing P-256's structure; table proof; measure bignum_copy_row_from_table for the select L p384
23 RSA-3072/4096 and no-ADX RSA, x86_64 aws-lc bn_mul{,x}4x_mont, bn_sqr8x_mont, bn_mul_mont_nohw, bn_power{,x}5, RSAZ AVX2 Nothing HOL XL rsa-x86-mont
24 Ed25519 verification, x86_64 AVX2 without ADX rind's port of dalek's AVX2 backend (about 1,300 lines) Nothing (dalek's Lean proofs are serial 64-bit) Aeneas over AVX2 intrinsic models L ed25519-avx2-verify
25 AES-CTR, CBC, key wrap, AES hardware aws-lc aes_hw_ctr32_encrypt_blocks and aes_hw_cbc_encrypt on x86_64; rind's NEON CTR and CBC on aarch64; mid/aes_kw.rs Block cipher after #1 HOL for the two x86_64 routines; Aeneas for the rest L aes-modes
26 P-521 ECDH and ECDSA, x86_64 and aarch64 The same over P-521's direct field s2n-bignum routines Aeneas after #22 L p521
27 ML-KEM-768, x86_64 without AVX2 rind's port of mlkem-native's portable C Keccak-f; mlkem-native's CBMC covers only its C's bounds Aeneas against the #11 spec M mlkem-portable
28 SHA-2, x86_64 without AVX2 aws-lc SHA-256 avx/ssse3/nohw, SHA-512 nohw Intel AVX SHA-512 HOL; measure #420's scalar SHA-512 routine L sha2-x86-no-avx2
29 aarch64 without crypto: AES, AES-GCM, SHA-256, SHA-1 aws-lc vpaes-armv8, ghash-neon-armv8, SHA nohws, rind's composition SHA-512 nohw HOL (tbl and 8-bit pmull are modelled); Aeneas L aarch64-no-crypto
30 x86_64 without AES-NI: AES, AES-GCM aws-lc vpaes-x86_64 and ghash-ssse3; Rust ports of aes_nohw.c and gcm_nohw.c Nothing HOL for the assembly; Aeneas with finite checks for the ports XL x86-no-aesni
31 ChaCha20-Poly1305, x86_64 without SSE4.1 HACL* rounds, aws-lc SSSE3 4x, Graviola scalar Poly1305, separate-pass glue HACL* rounds Aeneas; libcrux is 7-14% slower L chacha20-poly1305-portable
32 SHA-1, every x86_64 and aarch64 tier rind's SHA-NI, AVX2, and aarch64 intrinsics; aws-lc's avx/ssse3/nohw Padding and HMAC glue Aeneas for the intrinsics; HOL for aws-lc's L sha1
33 MD5 rind's portable Rust Nothing Aeneas against RFC 1321 M md5
34 armv7: everything but its Rust aws-lc, OpenSSL, and BoringSSL 32-bit assembly; curve25519-dalek u32; fiat-crypto with rind's umaal Rust; libcrux AES fiat-crypto's field ops (Coq), HACL* rounds and Poly1305 An epic: armv7 joins admin/prove (L), NIST curves (XL), an AArch32 model (XL), the assembly (XL), Curve25519 (XL) epic armv7

Every route proves the code rind runs today. Each switch named above (#13's p256_scalarmul, #22's table select, #28's scalar SHA-512) happens only if the proven code measures as fast. Each quest records where the faster code it keeps was measured.

Decisions

Answered by the maintainer on 2026-11-07. Three differ from what this PR first recommended; each is recorded in the quest files.

  1. Where rind's own HOL Light proofs live: in proofs/hol-light/ in rind, run by admin/prove beside the Lean proofs, over a pinned or vendored s2n-bignum. No moq-dev/s2n-bignum fork. The hol-light quest's plan is rewritten for this.
  2. Unmerged upstream specs: the SHA-2 quests may pin awslabs/s2n-bignum#415's and #420's commits, moving to the merged versions when they land; benchmarks/verified.toml's ✓ notes the pin. This one matches the recommendation.
  3. Upstream posts: no standing approval. Every quest that offers work to awslabs/s2n-bignum, or anywhere outside the moq-dev and kixelated orgs, stops and asks the maintainer before posting, and says so in its plan.
  4. New algorithms: a recurring re-audit instead of per-quest routes. Re-audit what's left to prove, end of m3 lives in m4 and requires m3. The PR that finishes it creates the next run at quest/m5/verified/re-audit.md, and each run covers the post-quantum and protocol algorithms that have landed by then.

Choices made without asking

  • One quest per gap, not per cell. Cells that share code and a route are one quest, such as x86_64 SHA-2 on every tier without AVX2, or aarch64 without the crypto extension. armv7 is a sub-epic because every one of its assembly gaps waits on a model that no tool has.
  • The trust-base assumptions inside existing ✓s (P256Order, Ed25519's group membership) are planned as a gap, since the epic shrinks the trust base too.
  • The existing children keep their ranks (asm-bytes and aeneas-fn-pointers stay first). The re-audit and the HOL Light home follow, then the gaps, ranked by use.

Validation

  • quest check: 124 documents ok.
  • nix develop --command just check: passes at 44e7274 (bench tests, quest, shell, and nix checks; no Rust changed).

Follow-ups

None beyond the planned quests.

Models

Size: M
Implementer: Claude Code, claude-opus-5-5, high effort

Review

Rewritten by quest review after each round.

  • Reviewer: Codex, gpt-6.1-sol, high effort
  • Session: 01a1b495-2deb-7bb1-ab4c-0ef2207e2feb, round 2
  • Head: f8af947
  • Base: origin/main at 64a8655
  • Score: 10/10, The documentation-only change resolves the earlier finding with no remaining actionable defects; local links and diff checks pass, and builds and tests were not run.
  • Findings: none
  • The last round's findings, at a64c8ca:
    • Fixed: low, quest/m4/verified/README.md:14: Scope the absence-of-proofs claim to rind's actual kernels; README.md:14 scopes the claim to rind's kernels, chacha20-poly1305-x86.md:10 names the existing proofs and line 11 requires benchmarking them, and chacha20-poly1305-aarch64.md:10 distinguishes their architecture.

Round 2's head was then merged with origin/main (conflict-free). 44e7274 records the maintainer's four decisions and adds the recurring re-audit they asked for. The maintainer asked for no re-review unless the plan changed beyond those edits, and it does not.

(Written by Claude Opus 5.5 with high)

🤖 Generated with Claude Code

kixelated and others added 2 commits November 6, 2026 21:42
@kixelated
chore(quest): claim quest/m4/verified/audit.md
fc624b6 
Quest-Claim: a159dbab1846b9a1
@kixelated @claude
chore(quest): audit what m4 has left to prove, and plan a quest per gap
a64c8ca 
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@kixelated kixelated changed the title Audit what's left to prove chore(quest): audit what m4 has left to prove, one quest per gap Nov 7, 2026
kixelated and others added 2 commits November 6, 2026 22:00
@kixelated
kixelated marked this pull request as ready for review November 7, 2026 06:01
@pullfrog

pullfrog Bot commented Nov 7, 2026 •
edited
Loading

Copy link
Copy Markdown

Your OpenCode Go account is out of credit. Top it up, then re-trigger Pullfrog.

OpenCode Go's response 
provider error: Insufficient account funds

Top up OpenCode Go →

Pullfrog  ｜ Rerun failed job ➔ ｜ View workflow run ｜ via Pullfrog ｜ Using glm-5.3

@coderabbitai

coderabbitai Bot commented Nov 7, 2026 •
edited
Loading

Copy link
Copy Markdown

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 31 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: 2ce1bc2c-ef88-40fd-bfa7-65c6d0783107
Commits

Reviewing files that changed from the base of the PR and between 73f0fa8 and 44e7274.

Files selected for processing: 44

  • quest/m4/verified/README.md
  • quest/m4/verified/aarch64-no-crypto.md
  • quest/m4/verified/aeneas-fn-pointers.md
  • quest/m4/verified/aes-gcm-aarch64-in-place.md
  • quest/m4/verified/aes-gcm-aarch64.md
  • quest/m4/verified/aes-gcm-x86-intrinsics.md
  • quest/m4/verified/aes-gcm-x86-vaes.md
  • quest/m4/verified/aes-header-protection.md
  • quest/m4/verified/aes-modes.md
  • quest/m4/verified/armv7/README.md
  • quest/m4/verified/armv7/assembly.md
  • quest/m4/verified/armv7/curve25519.md
  • quest/m4/verified/armv7/model.md
  • quest/m4/verified/armv7/nist-curves.md
  • quest/m4/verified/armv7/prove.md
  • quest/m4/verified/audit.md
  • quest/m4/verified/chacha20-poly1305-aarch64.md
  • quest/m4/verified/chacha20-poly1305-portable.md
  • quest/m4/verified/chacha20-poly1305-x86.md
  • quest/m4/verified/curve-groups.md
  • quest/m4/verified/ed25519-avx2-verify.md
  • quest/m4/verified/hol-light.md
  • quest/m4/verified/md5.md
  • quest/m4/verified/mlkem-avx512-sampler.md
  • quest/m4/verified/mlkem-construction.md
  • quest/m4/verified/mlkem-portable.md
  • quest/m4/verified/p256-x86.md
  • quest/m4/verified/p384.md
  • quest/m4/verified/p521.md
  • quest/m4/verified/re-audit.md
  • quest/m4/verified/rsa-aarch64-mont.md
  • quest/m4/verified/rsa-sign.md
  • quest/m4/verified/rsa-verify.md
  • quest/m4/verified/rsa-x86-ifma.md
  • quest/m4/verified/rsa-x86-mont.md
  • quest/m4/verified/sha1.md
  • quest/m4/verified/sha2-x86-no-avx2.md
  • quest/m4/verified/sha256-aarch64-hw.md
  • quest/m4/verified/sha256-x86-avx2.md
  • quest/m4/verified/sha3-sponge.md
  • quest/m4/verified/sha512-aarch64-hw.md
  • quest/m4/verified/sha512-x86-avx2.md
  • quest/m4/verified/sha512-x86-ext.md
  • quest/m4/verified/x86-no-aesni.md
  • 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

kixelated and others added 2 commits November 6, 2026 22:21
@kixelated
Merge remote-tracking branch 'origin/main' into quest/m4/verified/audit
46ed425
@kixelated @claude
chore(quest): record the maintainer's verified-epic decisions, and pl…
44e7274 
…an a recurring re-audit

HOL Light proofs live in proofs/hol-light, SHA-2 quests pin unmerged
upstream specs, every upstream post asks the maintainer, and a re-audit
recurs at the end of each milestone.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@kixelated

kixelated commented Nov 7, 2026

Copy link
Copy Markdown
Collaborator Author

Recorded the maintainer's 2026-11-07 answers in 44e7274:

  1. HOL Light home: proofs/hol-light/ in rind, run by admin/prove over a pinned or vendored s2n-bignum. No fork. hol-light.md is rewritten for it.
  2. Unmerged specs: the SHA-2 quests pin x86_64 sha256 block compression implementation without SIMD and without sha-specific instructions + functional proof + safety proof + Windows awslabs/s2n-bignum#415's and fix(adapters)!: return each adapter's own MissingFeature, not rind's #420's commits, moving to the merged versions when they land; the ✓ notes the pin.
  3. Upstream posts: no standing approval. Each quest that would post to awslabs/s2n-bignum, Mathlib, Aeneas, or anywhere outside moq-dev and kixelated says to stop and ask first.
  4. New algorithms: a recurring re-audit, quest/m4/verified/re-audit.md, at the end of m3. Each run creates the next one in the following milestone.

(Written by Claude Opus 5.5 with high)

@kixelated
kixelated added this pull request to the merge queue Nov 7, 2026
Merged via the queue into main with commit 89d10b9 Nov 7, 2026
7 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@kixelated