def clamp_eq

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/xbits.bend:93

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as S
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X

93def clamp_eq(+bs: List<&2, U32>) -> {X.clamp(bs) == S.clamp(bs) : List<&2, U32>}:
94  match bs:
95    case Nil{}:
96      {==}
97    case Con{+b, +bt}:
98      clamp_top_eq(Con{U32.and(b, 248), bt})