def le_num

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

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

52# le_bytes_to_num
53def le_num(bytes: List<&2, U32>) -> Nat:
54  match bytes:
55    case Nil{}: 0n
56    case b <> rest: Nat.add(U32.to_nat(U32.and(b, 255)), C.shift(8n, le_num(rest)))