~/jendhub

def canon

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

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

42# y < 2^130: y itself when y < p, else y - p = (y + 5) - 2^130.
43def canon(+y: Nat) -> Nat:
44  match y:
45    case 0n: 0n
46    case 1n+z: pick(C.fits(130n, Nat.add(1n+z, 5n)), 1n+z, C.low(130n, Nat.add(1n+z, 5n)))

Uses (5)

Used by (1)