def len

bend-collections@1.0.0.0 · src/crypto/curve25519/x25519.bend:88

import Base

88# the ladder's bit count, 8 len(k) - 1: 255 for a 32-byte scalar (RFC 7748
89# `bits`). Taken from the scalar, it keeps the proof checker from unfolding
90# the 255 steps for an unknown scalar.
91def len(xs: List<&2, U32>) -> Nat:
92  match xs:
93    case Nil{}:
94      0n
95    case Con{x, xt}:
96      1n+len(xt)