def bpv

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac.bend as Mac

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

304def bpv(+one: Nat) -> Nat:
305  Nat.sub(C.shift(130n, one), 6n)

Uses (3)