def red_scale_false

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

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

257def red_scale_false(+n: Nat, +low: Word(n), +b: List<&2, Bool>) -> {P.reduce(n, low, P.scale(False{}, b)) == Word.zero(n) : Word(n)}:
258  match b:
259    case Nil{}:
260      {==}
261    case x <> xs:
262      %Equal.sym(Word(n), P.reduce(n, low, P.scale(False{}, xs)), Word.zero(n), red_scale_false(n, low, xs)) : {Word.xor(n, P.constant(n, False{}), P.times_x(n, low, _)) == Word.zero(n) : Word(n)}
263      %Equal.sym(Word(n), P.times_x(n, low, Word.zero(n)), Word.zero(n), tx_zero(n, low)) : {Word.xor(n, P.constant(n, False{}), _) == Word.zero(n) : Word(n)}
264      constant_false_xor(n)