def kbit_le

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

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/spec/crypto/curve25519/field.bend as FS
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/proofs/math/typed/width.bend as WI
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

77def kbit_le(+bs: List<&2, U32>, +t: Nat, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {Nat.is_le(S.kbit(FS.value(bs), t), 1n) == True{} : Bool}:
78  WI.bit_le1(C.high(t, FS.value(bs)))