def dbound
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as Stepimport Base
57# the fold's limb bound: 321 * 2^21 < 2^30
58def dbound(+one: Nat) -> Nat:
59 Nat.add(s21(one), Nat.mul(s21(one), 320n))
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as Stepimport Base
57# the fold's limb bound: 321 * 2^21 < 2^30
58def dbound(+one: Nat) -> Nat:
59 Nat.add(s21(one), Nat.mul(s21(one), 320n))