def le_val

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:20

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

20# the little-endian value of bytes
21def le_val(bs: List<&2, U32>) -> Nat:
22  match bs:
23    case Nil{}: 0n
24    case b <> t: Nat.add(B.byte(b), C.shift(8n, le_val(t)))