def fits_one

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bytes.bend:232

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/lib/nat.bend as N
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/ineq.bend as I

232# x < 2^k (2^k with a symbolic one): x fits k bits
233def fits_one(k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(k, one)) == True{} : Bool}) -> {C.fits(k, x) == True{} : Bool}:
234  match k:
235    case 0n:
236      +hx1 = I.lt_subst_r(x, one, 1n, h1, hx)
237      +e0 = N.le_antisym(x, 0n, N.lt_succ_le(x, 0n, hx1), N.zero_le(x))
238      %Equal.sym(Nat, x, 0n, e0) : {Nat.is_eq(_, 0n) == True{} : Bool}
239      {==}
240    case 1n+ +j:
241      +hh = Equal.trans(Bool, Nat.is_lt(C.half(x), C.shift(j, one)), Nat.is_lt(x, Nat.double(C.shift(j, one))), True{}, WW.lt_half(x, C.shift(j, one)), hx)
242      fits_one(j, one, h1, C.half(x), hh)