def fold

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/poly1305.bend:27

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

27# x = lo + 2^130 hi is congruent to lo + 5 hi mod p (2^130 = p + 5); the fold
28# strictly decreases x while hi > 0, so x folds bring x below 2^130.
29def fold(+x: Nat) -> Nat:
30  Nat.add(C.low(130n, x), Nat.mul(C.high(130n, x), 5n))