law bigp

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/modp.bend:19

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

19law bigp:
20  for +one: Nat
21  for +h1: {one == 1n : Nat}
22  for +bp: Nat
23  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
24  for +x: Nat
25  {C.shift(130n, x) == Nat.add(Nat.mul(x, 1n+bp), Nat.mul(x, 5n)) : Nat}