proofs/math/random/below.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend as Below

14 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../spec/math/random/rand.bend as SR
import ../../../spec/math/random/source.bend as SRC
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/arith.bend as LA
import ../typed/width.bend as WI
import ../typed/w64m128.bend as M128
import ../typed/w64add.bend as WA
import ./lemire.bend as LE
import ../../lib/lemmas/proofs/nat_algebra.bend as NA

Definitions

def and_le source · line 20 · raw

@+w:Nat -> @+a:Nat -> @+b:Nat -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/rand.and_bits(w, a, b), b) == True{} : Bool}

x & m <= m

def high_lt_c source · line 35 · raw

@+x:Nat -> @+n:Nat -> @+y:Nat -> @+hy:{Nat.is_lt(y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(64n, n)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(64n, y), n) == c : Bool} -> {c == True{} : Bool}

x < 2^64 and n > 0: floor(x n / 2^64) < n

def lt_plus source · line 47 · raw

@+a:Nat -> @+n:Nat -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> {Nat.is_lt(a, Nat.add(n, a)) == True{} : Bool}

a < n + a for n > 0

def prod_lt source · line 51 · raw

@+x:Nat -> @+n:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(64n, x) == True{} : Bool} -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> {Nat.is_lt(Nat.mul(x, n), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(64n, n)) == True{} : Bool}

x < 2^64: x n < 2^64 n

def high_lt source · line 61 · raw

@+x:Nat -> @+n:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(64n, x) == True{} : Bool} -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(64n, Nat.mul(x, n)), n) == True{} : Bool}

x < 2^64 and n > 0: floor(x n / 2^64) < n

def pfst source · line 64 · raw

@-S:Data -> @p:Pair(Nat, S) -> Nat

def some_or source · line 68 · raw

@m:Maybe<&2, Nat> -> @+d:Nat -> Nat

def is_some source · line 75 · raw

@m:Maybe<&2, Nat> -> Bool

def none_some source · line 82 · raw

@+y:Nat -> @e:{None{} == Some{y} : Maybe<&2, Nat>} -> Empty

def some_inj source · line 86 · raw

@+x:Nat -> @+y:Nat -> @e:{Some{x} == Some{y} : Maybe<&2, Nat>} -> {x == y : Nat}

def acc_lt source · line 89 · raw

@+h:Nat -> @+k:Nat -> @+n:Nat -> @+hh:{Nat.is_lt(h, n) == True{} : Bool} -> @+ok:Bool -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/rand.accept(h, ok) == Some{k} : Maybe<&2, Nat>} -> {Nat.is_lt(k, n) == True{} : Bool}

def draw_pos_lt source · line 97 · raw

@+x:Nat -> @+m:Nat -> @+k:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(64n, x) == True{} : Bool} -> @+c:Bool -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/rand.draw_pos(64n, x, 1n+m, m, c) == Some{k} : Maybe<&2, Nat>} -> {Nat.is_lt(k, 1n+m) == True{} : Bool}

def draw_lt source · line 106 · raw

@+x:Nat -> @+n:Nat -> @+k:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(64n, x) == True{} : Bool} -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+e:{0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/rand.draw(64n, x, n) == Some{k} : Maybe<&2, Nat>} -> {Nat.is_lt(k, n) == True{} : Bool}

THEOREM: an accepted draw is below n

Templates

template go_lt source · line 114 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64, S)) -> @+f:Nat -> @+n:Nat -> @m:Maybe<&2, Nat> -> @+x:Nat -> @+s1:S -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(64n, x) == True{} : Bool} -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> @+hm:{0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/rand.draw(64n, x, n) == m : Maybe<&2, Nat>} -> {Nat.is_lt(pfst(S, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/rand.below_go(S, next, f, n, m, x, s1)), n) == True{} : Bool}

the bounded draw after a draw of x is below n > 0

template below_lt source · line 126 · raw

@-S:Data -> @-next:(@_:S -> Pair(0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.U64, S)) -> @+f:Nat -> @+n:Nat -> @+s:S -> @+hn:{Nat.is_lt(0n, n) == True{} : Bool} -> {Nat.is_lt(pfst(S, 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/rand.below(S, next, f, n, s)), n) == True{} : Bool}

THEOREM: the bounded draw from any source is below n > 0