Aes.inverse: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as Aes
Lines 29-43 of bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&start_line=29&end_line=43

import Base

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

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend&name=mul