[david415]

this reply written by agent mycroft@luna:

Builds on #51 (AES-128-GCM), now merged.

What changed

• AES (Cipher/AES.lean): subBytes now runs the Boyar–Peralta depth-16 S-box circuit (128 gates, 34 of them AND), bitsliced across the state with one byte per lane of a UInt64 bit plane. mixColumns doubles with mask arithmetic, xtime x = (x <<< 1) ^^^ (0x1b &&& (0 - (x >>> 7))). The key schedule's SubWord goes through the same subBytes. The table versions stay as the specification: sbox, subBytesSpec, mixColumnsSpec, expandKeySpec, expandKey128Spec, encryptBlockSpec. AEZ's imports of subBytes, shiftRows and mixColumns are unchanged.
• GHASH (Cipher/GHash.lean): the hash state and key are now two UInt64 words. Algorithm 1 is still bit-serial, but masks replace its branches, and blocks are loaded and stored without going through Nat. The old Nat code is mul / ghashSpec.
• POLYVAL (Cipher/Polyval.lean): the same treatment, with the double-width product in four words, the carry-less multiply by masks, and the 128 halvings in divX128 masked. The old code is polyvalSpec.
• Tag comparison (Util/ConstantTime.lean): ctEq ORs together the XOR of every byte pair over the full length and tests the result once at the end. decrypt in AES-GCM, AES-GCM-SIV and ChaCha20-Poly1305 now uses it. Their decrypt_encrypt / decrypt_sound laws still hold.
• Docstrings no longer say "not constant time". They now say the code is written without secret-dependent branches or secret-indexed memory accesses, and that Lean compiles through C with neither compiler proven to preserve that.

Proofs

Nothing uses sorry or native_decide, and there are no new axioms. scripts/check-axioms.sh passes on AES, GHash, Polyval, ConstantTime, AESGCM, AESGCMSIV and ChaChaPoly: every theorem depends only on propext, Classical.choice and Quot.sound.

• AES.sboxBits_eq: the circuit on the bits of a byte equals sboxByte, checked for all 256 inputs by decide +kernel.
• AES.sboxCircuit_lane: the UInt64 circuit computes the Bool circuit in every lane.
• AES.subBytes_eq_spec : subBytes = subBytesSpec and AES.mixColumns_eq_spec : mixColumns = mixColumnsSpec. These rest on xtime_eq / xtime_xor_eq, which equate xtime with mul · 2 and mul · 3 for all 256 inputs.
• AES.encryptBlock_eq_spec, AES.expandKey_eq_spec and AES.expandKey128_eq_spec: the cipher and both key schedules equal the table-based versions.
• GHash.mulCT_spec, GHash.load_toNat, GHash.store_eq and GHash.ghash_eq_spec : ghash h b = ghashSpec h b.
• Polyval.dotCT_spec, Polyval.load_toNat, Polyval.store_eq and Polyval.polyval_eq_spec : polyval h b = polyvalSpec h b.
• ConstantTime.ctEq_iff : ctEq a b = true ↔ a = b and ctEq_eq_decide : ctEq a b = decide (a = b).

Cipher.test also runs the new code against the specs at runtime: AES-128 and AES-256 on 200 random keys and blocks, and GHASH and POLYVAL on 200 random keys and lengths.

Tests

lake build succeeds (3575 jobs). Test output:

Cryptlib.Primitives.Cipher.test         FIPS-197 C.1 and C.3 ok; AES, GHASH, POLYVAL agree with specs; POLYVAL RFC 8452 example ok; all AES-256-GCM-SIV vectors passed
Cryptlib.Primitives.Cipher.aead_vectors_test
  ChaCha20-Poly1305: 316/316 Wycheproof vectors passed
  AES-256-GCM: 66/66 Wycheproof vectors passed
  AES-128-GCM: 67/67 Wycheproof vectors passed
Cryptlib.Primitives.WideBlockCipher.test   all 12 AEZ vectors passed (both encrypt and decrypt)
Cryptlib.Protocols.BACAP.test              all BACAP vectors passed
Cryptlib.Protocols.Sphinx.crypto_test      all Sphinx primitive-layer vectors passed
Cryptlib.Protocols.Sphinx.nike_vectors_test  all 10 NIKE-Sphinx vectors passed
Cryptlib.Protocols.Sphinx.kem_vectors_test   all 10 KEM-Sphinx vectors passed

Benchmarks

These come from bench/ (LeanBench, --min-time-ms 3000) on a shared 4-core machine at load average about 5, so the table gives minimum times. The spec rows run the old code in the same binary.

operation	before	after
AES-128 block	13.4 µs (table)	12.7 µs
AES-256 block	18.9 µs	17.7 µs
GHASH, 1232 B	1.93 ms (Nat)	37.6 µs
POLYVAL, 1232 B	2.25 ms (Nat)	73 µs
AES-128-GCM seal, 1200 B	3.56 ms	1.05 ms
AES-256-GCM-SIV seal, 4 KiB	12.9 ms	5.5 ms

The circuit S-box costs no more than the table did. AES time goes mostly to the array plumbing between rounds, which this PR leaves alone, and AES now accounts for nearly all of a GCM seal.