def lemire_count

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/lemire.bend:326

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/math/random/rand.bend as SR
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/natural/arith.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as UA

326# THEOREM (Lemire's branch): floor(2^w / n) outputs draw k
327def lemire_count(+w: Nat, +m: Nat, +k: Nat, +hp: {Nat.is_eq(SR.and_bits(w, 1n+m, m), 0n) == False{} : Bool}, +hw: {C.fits(w, 1n+m) == True{} : Bool}, +hk: {Nat.is_lt(k, 1n+m) == True{} : Bool}) -> {SR.count(w, 1n+m, k, C.shift(w, 1n)) == Nat.div(C.shift(w, 1n), 1n+m) : Nat}:
328  +W = C.shift(w, 1n)
329  +t = SR.pow2mod(w, 1n+m)
330  +a = Nat.add(t, C.shift(w, k))
331  +b = C.shift(w, 1n+k)
332  +q = Nat.div(W, 1n+m)
333  +Ca = Nat.div(Nat.add(a, m), 1n+m)
334  +Cb = Nat.div(Nat.add(b, m), 1n+m)
335  +cnt = SR.count(w, 1n+m, k, W)
336  +ht = Equal.trans(Bool, Nat.is_lt(t, 1n+m), Nat.is_lt(Nat.mod(W, 1n+m), 1n+m), True{}, Equal.cong(Nat, Bool, z => Nat.is_lt(z, 1n+m), t, Nat.mod(W, 1n+m), pm(w, m)), AR.dm_lt(m, W))
337  +hab = hab_of(w, m, k, hw)
338  +hcb = cb_le(w, m, k, hk)
339  +bq = Equal.trans(Nat, Cb, Nat.div(Nat.add(Nat.mul(q, 1n+m), Nat.add(a, m)), 1n+m), Nat.add(q, Ca),
340    Equal.cong(Nat, Nat, z => Nat.div(z, 1n+m), Nat.add(b, m), Nat.add(Nat.mul(q, 1n+m), Nat.add(a, m)), bm_eq(w, m, k)),
341    div_add_mul(q, m, Nat.add(a, m)))
342  +hca = Equal.trans(Bool, Nat.is_le(Ca, Cb), Nat.is_le(Ca, Nat.add(q, Ca)), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(Ca, z), Cb, Nat.add(q, Ca), bq), le_plus(q, Ca))
343  +ma = min_le(W, Ca, N.le_trans(Ca, Cb, W, hca, hcb))
344  +mb = min_le(W, Cb, hcb)
345  UA.add_cancel_r(cnt, q, Ca,
346    Equal.trans(Nat, Nat.add(cnt, Ca), Nat.add(cnt, cnt_lt(1n+m, a, W)), Nat.add(q, Ca),
347      Equal.cong(Nat, Nat, z => Nat.add(cnt, z), Ca, cnt_lt(1n+m, a, W),
348        Equal.trans(Nat, Ca, Nat.min(W, Ca), cnt_lt(1n+m, a, W), Equal.sym(Nat, Nat.min(W, Ca), Ca, ma), Equal.sym(Nat, cnt_lt(1n+m, a, W), Nat.min(W, Ca), cnt_min(m, a, W)))),
349      Equal.trans(Nat, Nat.add(cnt, cnt_lt(1n+m, a, W)), cnt_lt(1n+m, b, W), Nat.add(q, Ca),
350        sum_lemire(w, m, k, W, hp, ht, hab),
351        Equal.trans(Nat, cnt_lt(1n+m, b, W), Nat.min(W, Cb), Nat.add(q, Ca),
352          cnt_min(m, b, W),
353          Equal.trans(Nat, Nat.min(W, Cb), Cb, Nat.add(q, Ca), mb, bq)))))