[kixelated]

Works on quest/m4/verified/aes-gcm-x86-intrinsics.md and rewrites it to what remains.

Summary

This proves rind's own by-8 AES-CTR and PCLMULQDQ GHASH on x86_64. The specs are Vale's gcm_encrypt_LE and gcm_decrypt_LE, transliterated without their 2^32-byte bound. The proof goes through Aeneas and a hand model of the kernels, and covers the AEAD API on two tiers:

• SSE tier (AES-NI and PCLMULQDQ, no AVX): this tier now earns the ✓.
• Vale's tier: rind already hands by8 the inputs Vale's routines don't take: seals under 129 bytes, and AAD or messages of 2^32 bytes or more. Every length rind takes is now proven. The ✓ already shown for 32-byte seals now rests on a proof.

New files:

• proofs/Rind/X86_64/AesGcmModel.lean: the hand model of ClmulTable's GHASH, by8, its counter, and the tag. It quotes the Rust, and admin/prove checks the quote.
• Simd.lean: models of the SSE intrinsics by8 calls. admin/simd-vectors.rs checks them against the CPU.
• GhashClmul.lean:
  • ClmulTable::new's eight key powers.
  • ClmulTable::add is Horner's rule on the zero-padded blocks, and equal to Vale's ghash_LE.
• AesGcmBy8.lean: by8 is Vale's GCTR from inc32 j0 1, plus GHASH over the padded AAD and ciphertext. The proof covers the counter's byte swaps and PADDD, the AES rounds, and the 128-byte loop's sum of descending powers.
• AesGcmClmul.lean:
  • tagged with a 96-bit nonce is gcm_encrypt_LE / gcm_decrypt_LE: the counter block is compute_iv_BE's, the length block is gcm_hash's, and the tag is GCTR on the hash.
  • AesGcm::new, encrypt, and decrypt on any table by8 takes, wherever vale declines.
• AesGcmAead.lean: the AEAD-level theorems (aes_gcm_new, aes_gcm_seal*, aes_gcm_open*), moved from AesGcm.lean and generalized:
  • they hold on either tier, under RunsAesGcm := RunsValeAesGcm ∨ RunsClmulAesGcm;
  • the bounds are rind's real ones: AAD under 2^61 bytes, messages up to 2^36 - 32;
  • hlong : 129 ≤ len is gone.

GcmKey.lean and HkdfAead.lean follow the same changes.

Trust base:

• No new axiom, sorry, bv_decide, or native_decide.
• The open theorems now also rest on CtEqual.lean's ct_compare_16_spec and ct_compare_bytes_spec, since by-8's tag check runs ct_equal. Axioms.lean records this.
• Opens take assert_held = ok () like HMAC's verify.

Docs:

• benchmarks/verified.toml:
  • adds the SSE tier's entry (aes, pclmulqdq, ssse3, sse4.1, !avx);
  • rewords Vale's tier entry and links both to AesGcmAead.lean.
• BENCHMARKS.md and the SVGs are re-rendered. Only tooltips change, since no report host lacks AVX.
• proofs/README.md and ALGORITHMS.md say what by-8's proof covers.

Public API: none changed.

Builds on neither moq-dev/rind#631 nor moq-dev/rind#627. This uses Rind/Vale.lean's AES spec, the one Vale's tier already proves against, so the by-8 and Vale theorems share one spec.

Merged main, which landed ChaCha20-Poly1305's proofs: ChaCha20Poly1305.lean now imports AesGcmAead, where this PR moved VecAsMut and VecExtend, and HkdfAead.lean's AES-GCM conversion holds under RunsAesGcm beside main's ChaCha20-Poly1305 one.

Checks: admin/prove lean (all 2495 jobs), just check, admin/bench-report render --check, and quest check --base origin/main pass.

Models

• Size: L
• Implementer: Claude Code, claude-opus-5-5, unknown effort
• Implementer: Claude Code, claude-opus-5-5, medium effort (iterate, M)

Decisions

• Scope: ✅ merge this as a self-contained step, with the quest rewritten to what remains (rejected: keep extending this PR). Maintainer, 2026-11-12, via /quest-complete. It earns the SSE tier's ✓ and makes Vale's tier's ✓ honest for short seals; the quest's Plan keeps the rest: encrypt_any / decrypt_any for other IV lengths and truncated tags, AES-192, the AVX-512 by-16 kernels, and total specs of check_gcm_lengths' refusals.

Follow-ups

• None beyond the rewritten quest.

(Written by Claude Opus 5.5 with medium)

🤖 Generated with Claude Code

Review

Rewritten by quest review after each round.

• Reviewer: Codex, gpt-6.1-sol, high effort
• Session: 01a1ce3a-a848-7831-a3c3-54b270e41083, round 1
• Head: 5b4a5d4
• Base: origin/main at c3a0151
• Score: 9/10, Code review found no actionable defects and supports landing, but builds, tests, and proof checks were not run as instructed.
• Findings: none

[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 8 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: 1877d90b-00c9-4e4a-9a5a-fd02349f00fd

Commits

Reviewing files that changed from the base of the PR and between d6a9c71 and 5b4a5d4.

Files ignored due to path filters: 8

• benchmarks/nixos2-dark.svg is excluded by !**/*.svg
• benchmarks/nixos2.svg is excluded by !**/*.svg
• benchmarks/overview-dark.svg is excluded by !**/*.svg
• benchmarks/overview.svg is excluded by !**/*.svg
• benchmarks/ovh-iad-dark.svg is excluded by !**/*.svg
• benchmarks/ovh-iad.svg is excluded by !**/*.svg
• benchmarks/ovh-sea-dark.svg is excluded by !**/*.svg
• benchmarks/ovh-sea.svg is excluded by !**/*.svg

Files selected for processing: 21

• ALGORITHMS.md
• BENCHMARKS.md
• admin/prove
• admin/simd-vectors.rs
• benchmarks/verified.toml
• proofs/README.md
• proofs/Rind/Gf128.lean
• proofs/Rind/Vale.lean
• proofs/Rind/X86_64/AesGcm.lean
• proofs/Rind/X86_64/AesGcmAead.lean
• proofs/Rind/X86_64/AesGcmBy8.lean
• proofs/Rind/X86_64/AesGcmClmul.lean
• proofs/Rind/X86_64/AesGcmModel.lean
• proofs/Rind/X86_64/Axioms.lean
• proofs/Rind/X86_64/ChaCha20Poly1305.lean
• proofs/Rind/X86_64/FunsExternal.lean
• proofs/Rind/X86_64/GcmKey.lean
• proofs/Rind/X86_64/GhashClmul.lean
• proofs/Rind/X86_64/HkdfAead.lean
• proofs/Rind/X86_64/Simd.lean
• quest/m4/verified/aes-gcm-x86-intrinsics.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

• X
• Mastodon
• Reddit
• LinkedIn