Tidy all the AES-GCM proofs - #490

common/ghash.ml and common/polyval.ml prove that the GHASH polynomial
and the POLYVAL polynomial Q(x) are irreducible over GF(2), by the
Rabin test with 128-step squaring chains.  Nothing depends on these
theorems, but every AES-GCM proof loads both files, so each of the
eight proofs repeated the two proofs and loaded Library/rabin_test.ml,
fieldtheory.ml and matroids.ml for them.

Move the two irreducibility proofs, with the squaring chains, the
quotient oracle and the lemmas only they use, verbatim into a new
common/gf128_irreducible.ml, and check it once from a new
arm/proofs/aes_gcm_spec_checks.ml, which arm/Makefile builds and runs
with the proofs (build_proofs and run_proofs).  ghash.ml now needs
only Library/ringtheory.ml.  BEZOUT_BOOL_POLY stays in ghash.ml, and
its copy BEZOUT_BOOL_POLY_Q in polyval.ml, used by the cancellation
lemmas, is replaced by it; the unused MOD_POLYVAL_0 goes.  Also fix
the references to karatsuba_pmul_proof.ml, renamed karatsuba_pmul.ml.

Natively this takes ghash.ml from 52 s to 2 s and polyval.ml from
64 s to 9 s, and drops the 32 s of rabin_test.ml, so each AES-GCM
proof loads about 2.3 minutes faster.  The spec check takes 286 s.

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

The eight AES-GCM entries of include/s2n-bignum.h came in four
shapes.  Give them one: the length behaviour (the 4-way kernels
process floor(len_bits/128) blocks and return len_bits/8, which the
old "returns bytes processed" misstated for other lengths; the _alt
kernels touch no memory and return 0 unless len_bits is a nonzero
multiple of 128, and otherwise need in + len_bits/8 < 2^63), the part
of the gcm_init_v8 table they read, the no-overlap requirement that
every proof has (in-place operation was documented as not covered
only for the two enc_alt kernels), and the NIST message limit note,
which applies to all eight.  The Inputs/outputs lines keep their
buffer sizes, so subroutine_signatures.ml is unchanged; the c89
header is regenerated.

Add an "AES code" section to README.md, like the ML-KEM one, for
the ways arm/aes-xts and arm/aes_gcm differ from the usual
s2n-bignum conventions, and update the PR checklist's note on ARM
NOIBT variants, which the AES-GCM kernels now have.

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

The AES-GCM tests had grown kernel by kernel: 30 registrations with
their own wrappers, two KAT and two Wycheproof drivers that differed
only in key size, six inline copies of the key setup, four reference
kernels that differed only in cipher and direction, and coverage that
depended on the kernel: only aes128_gcm_enc_alt had a counter
rollover test, the 4-way kernels had no test of lengths that are not
whole blocks, and nothing checked for writes past the output.

Describe each kernel by its name, entry point, key size, direction and
length contract, and give all eight the same battery,
test_aes_gcm_kernel:
  - random inputs against the reference, after the zero length and
    every block count from 1 to 32, as before;
  - the length contract: floor(len_bits/128) blocks and a return of
    len_bits/8 for the 4-way kernels, now tested for six residues and
    0..20 blocks; the guard (with the PROT_NONE cases) for the _alt
    kernels;
  - wraparound of the 32-bit counter, generalized from the
    aes128_gcm_enc_alt rollover test;
  - the AWS-LC and Wycheproof vectors, through one driver.
Every differential case also checks the 64 bytes after the output.
Each kernel is now one registration under its own name; the AES-XTS
tests are grouped together, and aes_gcm_htable, which is pure C, also
runs on x86.  tests/ref_aes_gcm.c gets one kernel reference,
ref_aes_gcm_kernel, uses the S-box, round constants and xtime of
ref_aes_xts.c instead of copies, and loses ref_gctr and
ref_aes128_gcm_encrypt, which nothing used.  tests/Makefile lists all
of test.c's includes as prerequisites of test, and the skip message
for unsupported ARM features no longer names only sha3.

Under qemu-aarch64 -cpu max the full suite passes (397 tests; the 30
AES-GCM registrations became 9).  The new checks were seen to fail on
deliberately wrong kernel descriptions (direction or length contract).

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

The AES-XTS tests built AES-256 key schedules with rounds = 13,
described as "the assembly convention: Nr - 1".  But both AES-XTS
proofs require the word at offset 240 of each key schedule to be 14
(set_key_schedule in arm/proofs/utils/aes_xts_common.ml), which is
also what AWS-LC's AES_set_encrypt_key stores and what the benchmark
uses.  The tests passed only because the kernels' tweak loop, which
counts rounds - 2 down in steps of two, runs as often for 13 as for
14.  Use 14 in tests/ref_aes_xts.c and the two XTS known-answer
headers, so that the tests run the kernels inside their proved
preconditions.  All the AES-XTS tests pass.

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

The AES-GCM benchmark entries came in three different orders (x86
stubs, definitions and registrations), with eight helpers that
differed only in the kernel and the round count and four styles of
comment.  The helpers also refilled the round keys and the counter
block on every timed call, inside repeat(), which is a noticeable part
of a 16-byte call.

Give the kernels the header's (alphabetical) order everywhere,
describe them in one comment, and set up the key and counter once per
benchmark, outside the timed loop; the kernels update the counter and
the tag in place, which does not affect their timing.  The sizes and
repetition factors are unchanged.  Also list ../tests/arch.h, which
benchmark.c includes, as a prerequisite in benchmarks/Makefile.

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

Give the eight kernel headers one template: the title, an Inputs/
outputs line, the prototype aligned under its first argument, then the
contract in a fixed order (what is computed and over which data GHASH
runs; the length behaviour; which bytes of key and htable are read;
the _alt pointer bound; the no-overlap requirement, which the 4-way
proofs have too; the "alternative to" paragraph, now also in both
enc_alt headers; the NIST limit note, now in all eight), the ABI line,
and the origin with a "Proofs:" line.

In the bodies, fix the comments that were wrong: the Karatsuba key
named on the lane moves (h6k for h5k and h4k for h3k in both enc_alt
kernels, h6k for h2k twice in aes256_gcm_dec_alt), the entries of the
enc_alt rem4 drain, which is also reached for the last four of 5 to 7
blocks, and the setup rationale, which described an earlier control
flow.  The exact-8 drain comments of aes256_gcm_dec_alt now describe
the cascade by its live entry points.  Remove the development notes
and tombstones ([R2] tags, "removed", "(addresses unchanged)",
"route B", "AES re-roll", the BEGIN/END generator markers) and three
commented-out instructions, and fix the typos "udpate" and "supress";
the SLOTHY output of the 4-way kernels is left as it is.  Rename the
dec_alt small-message labels from their development names
(L*_dec_w5r_small, _h1, _stub_N, _gN, _done to L*_dec_small, _ge3,
_seed_N, _blk_N, _done), and give the enc_alt kernels the same 16-byte
.align before the symbol as the others (it was .balign 4).

The padded and -DNO_IBT .text and the unwind tables of all eight
objects are byte-identical to before, so the proofs are unaffected,
and subroutine_signatures.ml regenerates unchanged.

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

Nothing in the repository uses these items of common/:
  - polyval_ghash.ml: htable_mem, a 192-byte table predicate with the
    Karatsuba middle terms in the opposite lane order from gcm_init_v8's
    table, and the only thing tying the file to the ARM state; the
    htable_powers predicate and GHASH_BATCHED_FROM_HTABLE built on it;
    GHASH_ACC_STEP_CONG and POLYVAL_DECOMP;
  - ghash_nist_bridge.ml: nine lemmas left from an earlier route to
    GUERON_PROP1 (the exponent bijection and ring-sum reindexing, the
    word decompositions of the two polynomials, WORD_ZX_SAME, which is
    WORD_ZX_TRIVIAL, and GHASH_POLYVAL_RECIPROCAL);
  - polyval.ml: BOOL_POLY_ADD_SELF and W_EXPAND.
GHASH_POLY_IN_CARRIER restated ghash.ml's GHASH_BOOL_POLY, and
karatsuba_pmul.ml rebound polyval.ml's POLY_VAR_POW_OF_WORD_256; use
the originals.

Also terminate GUERON_PROP1 with ";;" (it parsed only because the next
phrase starts with "let"), drop its stale TODO, rewrite the bridge's
header, which listed definitions and theorems that now live in
ghash_nist_defs.ml, make the comments ASCII, add the SPDX header to
the five GHASH/POLYVAL files that lacked it, and update stale comments
in fips197.ml (the FIPS 197 / aese-aesmc equivalence is proved in
aes_gcm_common.ml; NIST_TC15_KEY_SCHEDULE is used by a proof, not by
a gcm.ml KAT) and tests/ref_aes_gcm.c.

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

Only comments change: the comment-free token streams of all six files
are identical to before, so the proofs are unaffected.

Each 4-way proof gets one header box: the kernel and its contract, the
proof structure with the -DNO_IBT offsets of the core theorem and its
legs, the vocabulary files, and the IBT lift.  Development history is
removed: timing and memory anecdotes, superseded-tactic notes, phase
labels, tombstones, comments orphaned when their lemmas moved to
aes_gcm_common.ml, and in aes256_gcm_enc.ml the boxes duplicated when
per-leg files were concatenated.  Comments that were wrong about the
code are fixed: core-theorem end PCs (pc + 0x448 for 0x710 and
pc + 0x3cc for 0xb7c), control-flow maps, register roles (X16 and Q30
in copied maps), step ranges, conjunct counts, leftovers of the fixed
counter value 2, names that do not exist, and two statements found in
review (the AES instructions work in lane order, not big-endian; the
per-block store is a two-eor macro, not an eor3).  The aes_gcm_common.ml
header now says that all eight AES-GCM proofs load it.  Comment lines
are wrapped within 79 columns and boxes are aligned.

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

Only comments change: the comment-free token streams of both files are
identical to before, so the proofs are unaffected.

The two proofs get the same comments, adapted to the key size: one
header box (contract, legs and their PCs, vocabulary, IBT lift); the
PERF/REPLAY-PERFORMANCE blocks cut to their design reasons; session,
gate and status labels, tombstones, plans and size anecdotes removed.
Comments that were wrong about the code are fixed against the -DNO_IBT
disassembly and the tactics next to them: the SETUP step numbers (8
behind), stale store PCs and tail-fold states, the TAIL_REM8 notes,
the tbl index register (Q12, not Q25), the tail's eor3 operand (v29),
the loop back edge (b.lt), Q19 (plain nist_ghash, no byteswap128),
fixed-counter leftovers, the block counts of SETUP0 ({5,6,7,8}), the
three paths of the subroutine theorem, AES-256 leftovers in the
AES-128 file, and names that do not exist.  Orphaned and duplicated
notes are moved to or merged with the items they describe, and
"8x/x4" becomes "8-way/4-way".

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

Only comments change: the comment-free token streams of both files are
identical to before, so the proofs are unaffected.

Each file gets one header box (contract, IBT lift, proof structure
with its -DNO_IBT offsets, vocabulary, file order) in place of the
"Binary:" line and the KEY PIPELINE FACT box.  Development history is
removed: arc markers, "objdump-confirmed" and "hyps=0" status words,
plan text and tactic scripts left in comments, tombstones, and every
timing, memory or size figure; the design reasons stay, without the
numbers.  Comments that were wrong about the code are fixed against
the code and the -DNO_IBT disassembly (state and step numbers,
offsets, counts, names that do not exist), including the AES-256
leftovers in the AES-128 port, and nothing describes the unreachable
L*_dec_blocks_more_than_7 block as executed any more.  The small-input
labels are cited by their new names.  The 486 items that are
token-identical between the two files now carry the same comments in
both, so that they can later move to a shared file unchanged.

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

common/fips197.ml ran 16 known-answer tests and built three 256-entry
lookup tables at every load, so every AES-GCM proof paid for them,
while common/gcm.ml, loaded by nothing, ran four inc32 tests and kept
its GCTR, GHASH and GCM tests commented out; those printed their
results rather than checking them, so gcm_ae and gcm_ad had never been
evaluated against a published vector.

Move the FIPS 197 tests verbatim into a new common/fips197_kats.ml and
add checks of the two key expansion functions against FIPS 197
Appendices A.1 and A.3 (nothing had used them).  Build the lookup
tables on first use, so the 4-way proofs, which never evaluate AES on
constants, do not build them.  Keep only definitions and conversions in
common/gcm.ml, adding GCM_AE_CONV and GCM_AD_CONV, and put its tests
in a new common/gcm_kats.ml as proved statements: inc32, GCTR through
the conversion without lookup tables, the expansion of the Test Case 3
key, gcm_ae for the McGrew-Viega Test Cases 1-3 and 13-15 (all those
with a 96-bit IV and whole blocks), and gcm_ad for Test Case 3, which
returns the plaintext with the right tag and NONE with its last bit
flipped.  arm/proofs/aes_gcm_spec_checks.ml loads both files, and
arm/Makefile now lists the common/ files that the AES-GCM proofs and
the spec checks depend on.

Natively common/fips197.ml now loads in 1.6 s instead of 30.6 s; the
spec checks take 598 s in all.

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

The AES-GCM contracts are stated with the kernel vocabulary of
arm/proofs/utils/aes_gcm_spec.ml (ctr_block, nist_input_block,
nist_cipher_block), which was not connected to the NIST SP 800-38D
definitions of common/gcm.ml.  Now that loading common/gcm.ml costs
nothing beyond its definitions, make aes_gcm_spec.ml load it and prove
there that inc32 advances ctr_block by one (INC32_CTR_BLOCK,
ITER_INC32_CTR_BLOCK, moved from the two 8-way decrypt proofs, which
proved them identically) and that the output blocks in NIST byte order
are GCTR, from the counter block ctr_block nonce c, of the input blocks
(GCTR_CTR_BLOCK, GCTR_NIST_BLOCKS).  With c = 2 that is GCTR from
inc32(J0), as GCM-AE and GCM-AD use it.

The two 8-way decrypt proofs also drop their local copy of the inc32
definition, kept to avoid loading the rest of common/gcm.ml.

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

The four 8-way kernels start with the same guard (cbz x1; tst x1, awslabs#127;
b.ne to a frameless "mov w0, #0; ret"), but only the two encrypt proofs
proved the no-access guarantee for a rejected length, each with its
own 60-line simulation, events tactic and mask lemma, followed by a
load-time check of the theorems' shape that prove already guarantees.

Put WB_MASK7_EQ_MOD, the branch facts ALT_GUARD_FACTS, EVENTS_NOMEM_TAC
and a tactic ALT_GUARD_REJECT_TAC into aes_gcm_common.ml, prove both
encrypt kernels' NOIBT_REJECT_NOACCESS theorems with it, and add the
same pair, AES{128,256}_GCM_DEC_ALT_{NOIBT_,}REJECT_NOACCESS, to the
two decrypt proofs: when len_bits is zero or not a multiple of 128 the
kernel returns 0 without any memory access, assuming nothing about
the data, key, table, counter, stack or separation.  The padded forms
follow by ARM_ADD_IBT_RULE.  The statements of the encrypt theorems are
unchanged; the shape checks go.

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

aes128_gcm_dec_alt.ml was ported from aes256_gcm_dec_alt.ml, and 377
of its top-level items are still token-identical to the AES-256 ones
and depend only on each other: the GHASH/Karatsuba bridge and its
N-block layer, the SIMD-fold simulation helpers, the counter core, the
int128 byte-list lemmas, the decrypt specification and the key-size
independent tactics and goal builders.  Move them, in the AES-256
order and with their comments, into a new
arm/proofs/utils/aes_gcm_dec_alt_common.ml that both proofs load.
No other item binds the names they bind, and the comment-free token
streams of the two proofs' items, together with the shared file's,
are exactly the old ones.

The shared file loads the AES-XTS byte-list utilities and the
lane-order AES specification that these items use; the proofs now
start with base.ml, the shared file and subroutine_signatures.ml
instead of loading their dependencies part way through.  arm/Makefile
lists the new dependencies.  About 4500 lines go.

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

Both 8-way decrypt kernels kept the generator's
L*_dec_blocks_more_than_7, 12 instructions that nothing reaches since
exactly 8 remaining blocks go to the dedicated drain
L*_dec_exact8_drain and every other remainder enters the cascade at
L*_dec_blocks_more_than_6 or later.  Delete it from aes256_gcm_dec_alt.S
(padded .text 5960 -> 5912 bytes) and aes128_gcm_dec_alt.S (5012 ->
4964), and update the origin notes.  Both objects have no unreachable
instruction left, one FDE covering the function with consistent rules,
and the -DNO_IBT .text is still the padded one without its first 4
bytes.

In the proofs every code address after the block moves by -0x30: the
listings (12 words fewer, 11 branch words that cross the block), the
code numerals that are such addresses or the code length (47 in the
AES-256 proof: the core exit 4556 -> 4508, the event PCs of the return
paths and the hardcoded length 5956 -> 5908; 31 in the AES-128 proof,
3756 -> 3708 and 5008 -> 4960) and the addresses in comments.  The
dead code was never executed, so no step count or state changes.

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

aes128_gcm_enc_alt is aes256_gcm_enc_alt with 10 rounds and 11 round
keys instead of 14 and 15, and the two proofs were one proof in two
copies: after renaming, their items differed only in the cipher and
code constants, the round count, ten program counters and nine step
counts.  Write it once, in arm/proofs/utils/aes_gcm_enc_alt_proof.ml,
on a layer of the items that depend on neither, which goes to
arm/proofs/utils/aes_gcm_enc_alt_common.ml.

Each kernel proof keeps its machine code, binds enc_alt_kernel (of the
record type aes_gcm_enc_alt_kernel of the common layer) to its
parameters, loads the shared proof with loadt and writes out its
exported theorems, proving them by ACCEPT_TAC of the shared ones.  The
quotations of the shared proof that depend on the kernel are wrapped
in kterm, which instantiates their free variables (cipher, tmc, nr,
nrk, keybytes, the program counters and the states at the small-path
tail entries) with the kernel's values; the step counts that differ
are OCaml integers.  The exported statements are unchanged.

In the shared proof, the safety theorems of the four small paths and
of the tail arms 1..7 now come from one generator each
(prove_fast_safe, prove_tail_rem_safe), the arms 2..7 of the TAIL_REM
case split from one tactic (TAIL_REM_ARM_TAC), and the setup's steps
between its two guards from SETUP_LOADS_TAC.  The two proofs go from
22981 lines to 12922 in four files.

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

The two 8-way decrypt proofs proved at every load the GHASH key table
htable_mem_8 at four keys (the all-zero AES-128 and AES-256 keys, the
FIPS-197 Appendix B key and the key of GCM test case 15), equal to the
tables gcm_init_v8 writes, and that the byte-reversed H gives another
table.  Nothing depends on these known answers, which check the
specification, so they move to arm/proofs/aes_gcm_spec_checks.ml,
which "make proofs" runs once.

The *_ZERO_KEY_CORRECT theorems of the four 8-way kernels were made in
two ways: the decrypt proofs rewrote with those known answers, the
encrypt proofs evaluated the table with HTABLE_MEM_8_KEY_CONV and
checked its first entry.  All four are now ALT_ZERO_KEY_RULE of
aes_gcm_common.ml, which does the latter.

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

AES128_GCM_DEC_ALT_CORRECT and AES256_GCM_DEC_ALT_CORRECT restated
the core spine in the shared vocabulary, but nothing uses them: the
exported theorems come from the subroutine spine.  Delete them, which
also saves their proof time, and the unused GCM_CTR_INC_ITER_ITER,
AES128_ENCRYPT_TOWER and AES-128 wbn_backlegs, and the two section
boxes that introduced the material now in aes_gcm_dec_alt_common.ml.

That shared layer kept the AES-256 proof's comments; make them hold
for both key sizes, and say that the addresses, labels and step
numbers they quote are the AES-256 kernel's.

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

The 8-way decrypt proofs called the length, tag and key-table arguments
bit_len, xi_p and htbl_p, where the other AES-GCM proofs, the
REJECT_NOACCESS theorems and the C prototypes use len_bits, tag_p and
htable_p.  Rename them throughout, and likewise the bound variable of
gcm_wb_blocks and GCM_WB_BLOCKS_VALID and the bit_len of the internal
legs of the 8-way encrypt proof.  The exported statements change only
in these bound variable names.

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

  - LENGTH_INT128_TO_BYTES was LENGTH_OF_INT128_TO_BYTES of
    aes_xts_common.ml, which the 8-way decrypt proofs load;
  - IVAL_WSUB_SMALL (8-way decrypt) and IVAL_WORD_SUB_SMALL (8-way
    encrypt), and IVAL_PTR_ADD (AES-256 8-way decrypt) and IV_ADD
    (8-way encrypt), are now IVAL_WORD_SUB_SMALL and IVAL_PTR_ADD of
    aes_gcm_common.ml;
  - the AES-128 decrypt proof's INPUT_PREFIX_TO_BYTE128_LANES was the
    AES-256 one's INPUT_BYTES_TO_BYTE128_LANES; it is now in
    aes_gcm_dec_alt_common.ml;
  - WRF8_IS_BYTEREVERSE was GSYM BREV_RF8_128;
  - in aes256_gcm_dec.ml ZX_WT was ZX_COUNTER_UD and WORD_ZX_ID32 an
    instance of WORD_ZX_TRIVIAL, and a local NIST_GHASH_NIL hid the
    one of ghash_nist_defs.ml (it is now NIST_GHASH_LIST_OF_SEQ_0);
  - BIT_WORD_1_256 of ghash_nist_bridge.ml was BIT_WORD_1;
  - three 4-way proofs proved SUBSUMED_APPLY again inline.

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

KEY11_SPLIT and KEY15_SPLIT, RK_ETA_11 and RK_ETA_15, and the two
KEY_READS_FROM_WORDLIST were copies differing in the number of round
keys.  Prove each from a generator, prove_key_split in
aes_gcm_common.ml and prove_rk_eta and prove_key_reads in
aes_gcm_dec_alt_common.ml, which build the same statements as before.

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

Some boxed comment lines of the AES-GCM proofs were a column or two
short of the box (some since they were written, some after renames of
the names they quote), and four were too long.  Re-pad them, and
re-wrap the paragraphs that no longer fit.  Comments only.

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

The machine-code listing of aes128_gcm_enc_alt.ml was patched by hand
from the AES-256 one: its words are right (define_assert_from_elf
checks them), but the 37 that differ carried objdump-style comments,
with tabs, instead of print_literal_from_elf's decoded forms.  Take the
comments from print_literal_from_elf, as for the other listings.
Comments only.

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

The exported CORRECT and SAFE theorems of the four 4-way kernels
(aes128_gcm_enc, aes128_gcm_dec, aes256_gcm_enc and aes256_gcm_dec)
required the output buffer to be disjoint from the input.  They now
allow it to be the input buffer itself: the input buffer leaves the
right-hand list of the ALLPAIRS hypothesis and gets clauses of its own,

  ALL (nonoverlapping (in_p,n)) [tag; ivec; stack frame] /\
  (in_p = out_p \/ nonoverlapping (in_p,n) (out_p,n)),

so each old theorem follows from the new one.

The proofs keep the input blocks in foralls over the blocks from some
lo on that no store of the leg reaches: the blocks not yet stored, and
for the pipelined decrypt loops the blocks above the last one stored.
The nonoverlapping automation handles the disjunction, so the
simulations carry these facts over the output stores.  New tactics in
aes_gcm_common.ml: INTRO_HYPS_TAC introduces the hypotheses without
splitting the disjunction, INPUT_LEG_TAC narrows the input fact at the
start of a leg and INPUT_POSTS_TAC closes the narrowed input facts of a
postcondition.  The file headers say that the output may be the input.

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

The same generalization for aes128_gcm_enc_alt and aes256_gcm_enc_alt,
whose shared proof (aes_gcm_enc_alt_proof.ml) gets the narrowed input
foralls of the 4-way proofs.  The main loop now assumes the pointer
bound val in_p + 16 * nb < 2 EXP 63, a hypothesis of the exported
theorems, which the nonoverlapping automation needs to separate the
input still to be read from the stores of the loop.  The internal
safety legs drop the input buffer from their nonoverlapping
hypotheses, which they never needed.

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

The same generalization for aes128_gcm_dec_alt and aes256_gcm_dec_alt.
These proofs read the input as a byte list, and the legs that store
output blocks now carry only the read of the input still to be read,

  read (memory :> bytes (in_p + 128(i+1),16 nblk - 128(i+1))) s =
  num_of_bytelist (SUB_LIST (128(i+1),16 nblk - 128(i+1)) ibytes),

in the main-loop invariant, the front prefix and the seam before the
tail, where it is the whole input of the shifted tail.  The front frame
no longer re-asserts the input buffer, which it does not preserve when
in_p = out_p.  New lemmas and tactics in aes_gcm_dec_alt_common.ml:
READ_BYTES_SLICE, INPUT_SUFFIX_SLICE, INPUT_SUFFIX_LANE, INPLACE_SHIFT,
WBN_SUFFIX8_TAC and WBN_NEXT_SUFFIX_TAC; WBN_RAWCT_READ, WBN_Q9_SPEC
and WBN_INPUT_SUFFIX_GEN (for WBN_INPUT_SLICE_GEN), which each proof
had its own copy of, are shared there.  The internal core safety
theorems drop the input buffer from their nonoverlapping hypotheses.
Also moves a comment of aes_gcm_dec_alt_common.ml back to its lemma.

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

The battery of the eight AES-GCM kernels gets test_aes_gcm_inplace,
the cases of test_aes_gcm_random with the kernel working in place on a
copy of the input in its output buffer, compared with the out-of-place
reference as before.

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

include/s2n-bignum.h said that in-place operation (out == in) is not
covered.  The eight entries now give the proved contract, with out
either equal to in or disjoint from it, and the README's AES code
section says that the kernels may be called in place.

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

The correctness proofs of the tail arms TAIL_REM2..TAIL_REM7, of the
small-path tails FAST1_TAIL..FAST4_TAIL and of the small paths
FAST1..FAST4 in aes_gcm_enc_alt_proof.ml were written out once each,
and differed only in the block count, the state numbers and a few
step counts.  They now come from generators: prove_tail_rem r and
prove_fast_tail r, with tail_q19_fold r (the Q19 fold of the r-block
batched reduce, formerly TAIL_Q19_FOLD_REM2..7 and FOLD_Q19_REM2..7),
TAIL_IN_BLOCKS_TAC and TAIL_POST_TAC, and prove_fast r, with
FAST_DISPATCH_TAC r.  The statements are built from templates and are
the same terms as before.  The case split of TAIL_REM and the
mid-states of FAST1..FAST4 take the precondition of the arm or tail
from its theorem (leg_pre, mid_state and stack_mod_p).

aes_gcm_enc_alt_proof.ml goes from 7650 to 5600 lines.

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

The 32 exported theorems of the eight AES-GCM kernels quantified their
variables in three different orders, one per family.  They now follow
the C argument order, as most s2n-bignum theorems do: the arguments
in_p len_bits out_p tag_p ivec_p key_p htable_p, then the values in the
order of their pointers (inblock tag0 nonce c rk; the SAFE theorems
have none), then pc stackpointer returnaddress.  The 4-way SAFE
theorems already had this order; the other 24 statements change only
in it.  The f_events argument orders are unchanged.

ARM_ADD_RETURN_STACK_TAC pairs the quantifiers of the core theorem
with those of the goal by position, so the four 4-way core CORRECT
theorems take the same order.  The 8-way SAFE statements are generated
from the CORRECT ones by mk_safety_spec, which keeps their order.

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

In HOL Light a capitalized name reads as a theorem unless its suffix
says otherwise, and tactics end in _TAC.  120 tactics of the AES-GCM
proofs did not: closers such as CLOSE, KSCLOSE and CIPHER_CLOSE,
steppers such as NSTEP and SAFE_SIM, and many others.  They are
renamed, in the code and in the comments, by appending _TAC, moving
an inner _TAC to the end (SETUP_RECON_TAC_GEN becomes
SETUP_RECON_GEN_TAC) and capitalizing (CTRREG_dec becomes
CTRREG_DEC_TAC).  Two names would have clashed: the generic
SAFE_SIM_TAC becomes ARM_SAFE_SIM_TAC, so that its per-kernel
instances SAFE_SIM can take the name, and the generator
INPUT_SPLIT_DEC becomes INPUT_SPLIT_N_TAC.  The tacticals MUST,
MUST_PROGRESS, CLOSE_WITH, CLOSE_R2_WITH and LEAF_WITH keep their
names, like HOL Light's TRY and EVERY.

The comment-free token streams are those of the previous commit with
the names replaced (also in three failure messages), and the comments
are the same word for word; the box comments that the longer names
overflowed are re-wrapped.

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

The AES-GCM proof files had about 4400 lines longer than 80 columns.
They are wrapped, mostly by a tool that breaks lines only at spaces
outside strings and comments, so that the comment-free token stream
is unchanged, and that prefers the breaks of the surrounding code:
after THEN, after a list or conjunction separator, before ==>, after
the = of an equation, with the continuation aligned just inside the
innermost open bracket or quotation.  The long free-form comments are
re-wrapped, and two string literals given to parse_term are laid out
again (only their whitespace changes).  The machine-code listings
generated by print_literal_from_elf are left as they are.

No other line of these files is now longer than 80 columns.

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

The header comments of the eight AES-GCM kernels still said that the
output must not overlap the input and that in-place operation
(out == in) is not covered by the proof, which has been false since
the proofs were generalized to allow it.  They now state the proved
contract, as include/s2n-bignum.h already does: out, tag and ivec must
not overlap each other, key or htable, tag and ivec must not overlap
in, and out must either be in or not overlap it.  The comment change
leaves the object code unchanged.

include/s2n-bignum-c89.h is regenerated from include/s2n-bignum.h,
which had not been done since the latter was updated.

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

The legs for nb = 9..16 (one full group, so no main loop) were written
out next to the general ones and differed from them only in k = 0:
SETUP_G1 and SETUP_G1_SAFE next to SETUP_GEN and SETUP_GEN_SAFE, and
FIXED_CORRECT_G1 next to GEN_CORRECT.  Each pair now comes from one
function (prove_setup, prove_setup_safe and prove_gen_correct), and
the statements of the g = 1 legs are derived from the general ones:
setup_g1_form takes k = 0 for ~(k = 0) and the exit at
pc + pc_prepretail for pc + pc_loop, and drops SETUP_GEN's flag
conjunct; fixed_g1_form takes k = 0 for ~(k = 0) and 0 for k in the
other hypotheses.  The statements are the same terms as before.

aes_gcm_enc_alt_proof.ml goes from 5692 to 5288 lines.

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

PREPRETAIL_TAIL_SAFE, FIXED_CORRECT_G1_SAFE, LOOP_TAIL_SAFE and
GEN_CORRECT_SAFE each compose two safety legs by double abstract
bigstep, with the same tactic written out four times.  They now use
one tactic, SAFE_SEQ2_TAC, given the two legs and their
instantiations; it builds the trace witness, the second leg's events
after the first's, from the goal's f_events arguments.  The
statements are unchanged.

aes_gcm_enc_alt_proof.ml goes from 5288 to 5145 lines.

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

Use the linux64 main-loop output of AWS-LC aesv8-gcm-armv8-unroll8.pl
from commit 6869608079c6b33fdb10e6c231bf6f2204862b89, retaining its
comments, spacing and original EOR3 .inst directives. Adapt only the
local loop label to the surrounding s2n-bignum assembly.

Before/after GCC, Clang, Mach-O and AWS-LC delocator objects are byte
identical for both BTI and NOIBT builds. Proof sources are unchanged.

Select AES-128 GHASH normalization using the existing AES round count,
removing eak_native_loop from the shared record and kernel configurations.
Keep all three explicit load positions for each kernel.

Verified identical specialized shared proof scripts and OCaml guard/fold
behavior for AES-128 and AES-256. Assembly and exported theorem statements
are unchanged. No new cold HOL replay was run for this equivalent refactor.

Replace the 20 raw .inst encodings with eor3 mnemonics while preserving AWS-LC instruction order and the generated Perl comments.

Validation: complete before/after objects are identical for BTI and NOIBT under GCC, Clang, Mach-O and the AWS-LC delocator. Proof sources and machine literals are unchanged.

Re-box the comments that the native AES-128 main loop added or changed
to the 79-column boxes of the files, describe the difference between
the two kernels in the header of the shared proof in its original
terms, and note in the MAIN_LOOP header what the native instruction
order changes in the loop proof.  Also re-pad one comment line of the
tail section.  Comment changes only.

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

Skip .hidden, .type and .size on _WIN32, as the generic
_internal_s2n_bignum.h already does for .hidden. With this, the AArch64
files assemble for Windows (COFF), except those using Apple-style @page
relocations.

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

The two AES-128-specific steps of the shared 8-way encrypt proof, the
extra Q21/Q29 guard of the main-loop stepper and the re-association
in the Q19 fold, tested enc_alt_kernel.eak_rounds = 10.  That holds
for the AES-128 kernel, but it is not the property the steps depend
on: they follow the instruction order of its main loop, the native
order of AWS-LC's AES-128 kernel.  Restore the kernel parameter
eak_native_loop for it (true for aes128_gcm_enc_alt and false for
aes256_gcm_enc_alt), which "ARM: remove redundant AES-GCM encrypt
proof flag" had replaced by the round-count test, and test the flag.
The proofs take the same steps as before.

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

The .note.gnu.property section that _internal_s2n_bignum_arm.h emits
to mark objects as BTI-compatible is an ELF note, and the header
already leaves it out on Apple.  Leave it out on Windows too, as "Make
the ARM symbol directives no-ops on Windows" does for the .hidden,
.type and .size directives.

On COFF the note has no meaning.  clang 18 turns it into a writable
32-byte data section in every object, and clang 14 rejects its
.pushsection and .popsection directives, so that with clang 14 none of
the AArch64 sources assembled for Windows.  With this change all 362
sources that include the header assemble for aarch64-pc-windows-msvc
and aarch64-w64-windows-gnu with clang 14 and clang 18, with and
without S2N_BN_HIDE_SYMBOLS and NO_IBT.  For Linux and macOS the
preprocessed sources and the objects are unchanged.

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