def red_shift

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

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

283def red_shift(+n: Nat, +low: Word(n), +p: List<&2, Bool>) -> {P.reduce(n, low, False{} <> p) == P.times_x(n, low, P.reduce(n, low, p)) : Word(n)}:
284  constant_false_l(n, P.times_x(n, low, P.reduce(n, low, p)))