def sa

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

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

296# Algorithm 1 of SP 800-38D: Z ^= a_i ? V : 0, V = V * x.
297def sa(+n: Nat, +low: Word(n), a: List<&2, Bool>, z: Word(n), +v: Word(n)) -> Word(n):
298  match a:
299    case Nil{}:
300      z
301    case c <> r:
302      sa(n, low, r, Word.xor(n, z, P.wscale(n, c, v)), P.times_x(n, low, v))