law big130

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/step.bend:35

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

35# 2^130 x = x p + 5 x
36law big130:
37  for +one: Nat
38  for +h1: {one == 1n : Nat}
39  for +x: Nat
40  {C.shift(130n, x) == Nat.add(Nat.mul(x, pm(one)), Nat.mul(x, 5n)) : Nat}