def bl_140

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/natfuel.bend:193

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/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

193# 140 steps suffice for bit_length below 2^j, j <= 140
194def bl_140(+j: Nat, +n: Nat, +hj: {Nat.is_le(j, 140n) == True{} : Bool}, +hn: {Nat.is_lt(n, C.pow2(j)) == True{} : Bool}) -> {M.bit_length_go(140n, n, 0n) == M.bit_length(n) : Nat}:
195  bl_fuel(140n, n, n, 0n, bends_bound(j, 140n, n, hn, hj), bends_self(n, n, N.le_refl(n)))