def sb01

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/sel.bend:25

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/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as BV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsrel.bend as BR

25def sb01(i: Nat, +off: Nat, +k: Nat) -> {BV.all01(BR.sb(i, off, k)) == True{} : Bool}:
26  match i:
27    case 0n:
28      {==}
29    case 1n+ +j:
30      Lg.and_intro(Nat.is_lt(CV.bit(Nat.add(off, j), k), 2n), BV.all01(BR.sb(j, off, k)), bit01(C.high(Nat.add(off, j), k)), sb01(j, off, k))