def uvalue

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

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

70# a constant from its little-endian bytes (U32 values), each scaled by the
71# symbolic one: uvalue(one, bs) is value(bs) for one == 1
72def uvalue(+one: Nat, xs: List<&2, U32>) -> Nat:
73  match xs:
74    case Nil{}:
75      0n
76    case Con{x, xt}:
77      Nat.add(Nat.mul(one, U32.to_nat(x)), C.shift(8n, uvalue(one, xt)))