def digits

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/curve25519/field.bend:60

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

60# a constant from its little-endian base-256 digits, each scaled by the
61# symbolic one (so the checker never unfolds it): digits(one, [65n, 219n, 1n])
62# is 121665 for one == 1
63def digits(+one: Nat, ds: List<&2, Nat>) -> Nat:
64  match ds:
65    case Nil{}:
66      0n
67    case Con{d, dt}:
68      Nat.add(Nat.mul(one, d), C.shift(8n, digits(one, dt)))