def valid_bytes

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

import Base

128# 32 values, each below 256
129def valid_bytes(n: Nat, xs: List<&2, U32>) -> Bool:
130  match n:
131    case 0n:
132      match xs:
133        case Nil{}:
134          True{}
135        case Con{x, xt}:
136          False{}
137    case 1n+m:
138      match xs:
139        case Nil{}:
140          False{}
141        case Con{x, xt}:
142          Bool.and(U32.is_lt(x, 256), valid_bytes(m, xt))