def limbs16

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/secp256k1/field.bend:77

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

77# exactly 16 limbs, each below 2^16
78def limbs16(+one: Nat, n: Nat, xs: List<&2, Nat>) -> Bool:
79  match n xs:
80    case 0n Nil{}:
81      True{}
82    case 0n x <> t:
83      False{}
84    case 1n+k Nil{}:
85      False{}
86    case 1n+k x <> t:
87      Bool.and(Nat.is_lt(x, C.shift(16n, one)), limbs16(one, k, t))