src/crypto/aes/sbox.bend checks

The AES S-box and the GF(2^8) doublings MixColumns needs, computed with U32 bit operations only: no table and no branch reads a secret byte.

The S-box is the depth-16, 113-gate (+ 4 NOT) circuit of Boyar and Peralta ("A depth-16 circuit for the AES S-box", 2011; the gate list BearSSL's aes_ct uses), evaluated on one byte with one bit per U32 (values 0 or 1). Its input x0..x7 is the byte's bit 7..0 and its output s0..s7 the result's bit 7..0. proofs/crypto/aes/sbox.bend proves it equal, on every input, to FIPS 197's S-box (the inverse in GF(2^8) followed by the affine map). Every mask is the first operand of U32.and, so the bits above the low eight of an input never reach the result.

The S-box. (The one-constructor match only opens the U32, no branch: it keeps a proof about an unknown word from expanding the 117 gates.)

{02} * x in GF(2^8) (FIPS 197 section 4.2.1, xtime): shift left and, when bit 7 was set, add x^8 = {1b}; the reduction mask is 0 - bit7, not a branch.

{03} * x = {02} * x + x.