def par01

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/blist.bend:82

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/proofs/math/typed/width.bend as WW
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/u32and.bend as FB

82# the parity bit of the prefix byte
83def par01(+pre: U32) -> {Nat.is_lt(U32.to_nat(U32.and(pre, 1)), 2n) == True{} : Bool}:
84  %Equal.sym(Nat, U32.to_nat(U32.and(pre, 1)), C.low(1n, U32.to_nat(pre)), FB.andm(pre, 1n, 1, {==})) : {Nat.is_lt(_, 2n) == True{} : Bool}
85  WW.low_lt(1n, U32.to_nat(pre))