def bytes

bend-collections-laws-crypto@1.0.0.0 · src/crypto/poly1305/limbs.bend:114

import Base

114# n bytes of the value of ds + u (mod 2^(8n)).
115def bytes(n: Nat, +ds: List<&2, U32>, u: U32) -> List<&2, U32>:
116  match n:
117    case 0n: Nil{}
118    case 1n+k:
119      +s = U32.add(u, hd0(ds))
120      U32.and(s, 255) <> bytes(k, tl(ds), U32.shrn(s, 8n))