def inverse

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/aes/aes.bend:29

import Base

29# Section 4.4 / 5.1.1: the multiplicative inverse of a nonzero a in GF(2^8),
30# {00} mapped to itself. The multiplicative group of GF(2^8) has 255
31# elements, so a^255 = {01} and a^-1 = a^254 for a != {00} (and
32# {00}^254 = {00}): computed by squaring, a^254 = a^2 a^4 a^8 ... a^128.
33# (tools/check_aes.py checks this against the defining property a * b = {01}
34# for all 256 bytes.)
35def inverse(+a: U32) -> U32:
36  +a2 = mul(a, a)
37  +a4 = mul(a2, a2)
38  +a8 = mul(a4, a4)
39  +a16 = mul(a8, a8)
40  +a32 = mul(a16, a16)
41  +a64 = mul(a32, a32)
42  +a128 = mul(a64, a64)
43  mul(a2, mul(a4, mul(a8, mul(a16, mul(a32, mul(a64, a128))))))