law Inverse.unit

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/laws.bend:47

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as S

47# The specification's inverse (a^254) is the multiplicative inverse of
48# FIPS 197 section 4.4: a * a^-1 = {01} for every nonzero byte, and {00}
49# goes to {00} (5.1.1); so S.sbox is "inverse, then affine map".
50law Inverse.unit:
51  for +x: U32
52  for +h: {U32.is_eq(U32.and(255, x), 0) == False{} : Bool}
53  {S.mul(x, S.inverse(x)) == 1 : U32}