law Sbox.value

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

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

41# The constant-time S-box circuit is FIPS 197's S-box (the inverse in
42# GF(2^8), {00} to {00}, then the affine map), on every input.
43law Sbox.value:
44  for +x: U32
45  {B.sbox(x) == S.sbox(x) : U32}