proofs/math/random/below.bend

bend-collections-laws-crypto@1.0.0.0 · 127 lines · 15 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as SR
5import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as SRC
6import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as LA
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend as M128
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as WA
13import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire.bend as LE
14import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
15
16# Every draw the specification accepts, and its last candidate, is below n:
17# so is the bounded draw from any source (and, by Uint64n.value, uint64n).
18
19# x & m <= m
20def and_le(+w: Nat, +a: Nat, +b: Nat) -> {Nat.is_le(SR.and_bits(w, a, b), b) == True{} : Bool}:
21  match w:
22    case 0n:
23      N.zero_le(b)
24    case 1n+p:
25      +hb = WI.hb(b)
26      +h1 = WA.mul_le1(C.bit(a), C.bit(b), WI.bit_le1(a))
27      +h2 = N.double_le(SR.and_bits(p, C.half(a), C.half(b)), C.half(b), and_le(p, C.half(a), C.half(b)))
28      +h3 = N.le_trans(Nat.add(Nat.mul(C.bit(a), C.bit(b)), Nat.double(SR.and_bits(p, C.half(a), C.half(b)))), Nat.add(C.bit(b), Nat.double(SR.and_bits(p, C.half(a), C.half(b)))), Nat.add(C.bit(b), Nat.double(C.half(b))),
29        WI.le_add_r(Nat.mul(C.bit(a), C.bit(b)), C.bit(b), Nat.double(SR.and_bits(p, C.half(a), C.half(b))), h1),
30        N.le_add_left(Nat.double(SR.and_bits(p, C.half(a), C.half(b))), Nat.double(C.half(b)), C.bit(b), h2))
31      %Equal.sym(Nat, b, Nat.add(C.bit(b), Nat.double(C.half(b))), hb) : {Nat.is_le(Nat.add(Nat.mul(C.bit(a), C.bit(b)), Nat.double(SR.and_bits(p, C.half(a), C.half(b)))), _) == True{} : Bool}
32      h3
33
34# x < 2^64 and n > 0: floor(x n / 2^64) < n
35def high_lt_c(+x: Nat, +n: Nat, +y: Nat, +hy: {Nat.is_lt(y, C.shift(64n, n)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(C.high(64n, y), n) == c : Bool}) -> {c == True{} : Bool}:
36  match c:
37    case True{}:
38      {==}
39    case False{}:
40      +h = C.high(64n, y)
41      +ge = N.le_trans(C.shift(64n, n), C.shift(64n, h), y, WI.shift_mono(64n, n, h, N.not_lt_le(h, n, hc)),
42        %Equal.sym(Nat, y, Nat.add(C.low(64n, y), C.shift(64n, h)), WI.low_high(64n, y)) : {Nat.is_le(C.shift(64n, h), _) == True{} : Bool}
43        LE.le_plus(C.low(64n, y), C.shift(64n, h)))
44      Empty.absurd({False{} == True{} : Bool}, L.false_true(Equal.trans(Bool, False{}, Nat.is_lt(y, C.shift(64n, n)), True{}, Equal.sym(Bool, Nat.is_lt(y, C.shift(64n, n)), False{}, N.le_not_lt(y, C.shift(64n, n), ge)), hy)))
45
46# a < n + a for n > 0
47def lt_plus(+a: Nat, +n: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_lt(a, Nat.add(n, a)) == True{} : Bool}:
48  Equal.trans(Bool, Nat.is_lt(a, Nat.add(n, a)), Nat.is_lt(0n, n), True{}, WI.lt_cancel_r(0n, n, a), hn)
49
50# x < 2^64: x n < 2^64 n
51def prod_lt(+x: Nat, +n: Nat, +one: Nat, +h1: {one == 1n : Nat}, +hx: {C.fits(64n, x) == True{} : Bool}, +hn: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_lt(Nat.mul(x, n), C.shift(64n, n)) == True{} : Bool}:
52  +W = C.shift(64n, one)
53  +hw = WI.lt_one(64n, one, h1, x, hx)
54  +hle = LA.mul_le(1n+x, W, n, N.lt_succ_le_succ(x, W, hw))
55  +hlt = N.lt_le_trans(Nat.mul(x, n), Nat.mul(1n+x, n), Nat.mul(W, n), lt_plus(Nat.mul(x, n), n, hn), hle)
56  %Equal.sym(Nat, C.shift(64n, n), Nat.mul(n, W), WI.shift_mul_one(64n, one, h1, n)) : {Nat.is_lt(Nat.mul(x, n), _) == True{} : Bool}
57  %NA.mul_comm(W, n) : {Nat.is_lt(Nat.mul(x, n), _) == True{} : Bool}
58  hlt
59
60# x < 2^64 and n > 0: floor(x n / 2^64) < n
61def high_lt(+x: Nat, +n: Nat, +hx: {C.fits(64n, x) == True{} : Bool}, +hn: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_lt(C.high(64n, Nat.mul(x, n)), n) == True{} : Bool}:
62  high_lt_c(x, n, Nat.mul(x, n), prod_lt(x, n, 1n, {==}, hx, hn), Nat.is_lt(C.high(64n, Nat.mul(x, n)), n), {==})
63
64def pfst(-S: Data, p: Nat & S) -> Nat:
65  (k, s) = p
66  k
67
68def some_or(m: Maybe<&2, Nat>, +d: Nat) -> Nat:
69  match m:
70    case None{}:
71      d
72    case Some{x}:
73      x
74
75def is_some(m: Maybe<&2, Nat>) -> Bool:
76  match m:
77    case None{}:
78      False{}
79    case Some{x}:
80      True{}
81
82def none_some(+y: Nat, e: {None{} == Some{y} : Maybe<&2, Nat>}) -> Empty:
83  %Equal.sym(Maybe<&2, Nat>, None{}, Some{y}, e) : L.truth(is_some(_))
84  Unit{}
85
86def some_inj(+x: Nat, +y: Nat, e: {Some{x} == Some{y} : Maybe<&2, Nat>}) -> {x == y : Nat}:
87  Equal.cong(Maybe<&2, Nat>, Nat, m => some_or(m, x), Some{x}, Some{y}, e)
88
89def acc_lt(+h: Nat, +k: Nat, +n: Nat, +hh: {Nat.is_lt(h, n) == True{} : Bool}, +ok: Bool, +e: {SR.accept(h, ok) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_lt(k, n) == True{} : Bool}:
90  match ok:
91    case True{}:
92      %some_inj(h, k, e) : {Nat.is_lt(_, n) == True{} : Bool}
93      hh
94    case False{}:
95      Empty.absurd({Nat.is_lt(k, n) == True{} : Bool}, none_some(k, e))
96
97def draw_pos_lt(+x: Nat, +m: Nat, +k: Nat, +hx: {C.fits(64n, x) == True{} : Bool}, +c: Bool, +e: {SR.draw_pos(64n, x, 1n+m, m, c) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_lt(k, 1n+m) == True{} : Bool}:
98  match c:
99    case True{}:
100      %some_inj(SR.and_bits(64n, x, m), k, e) : {Nat.is_lt(_, 1n+m) == True{} : Bool}
101      N.le_lt_succ(SR.and_bits(64n, x, m), m, and_le(64n, x, m))
102    case False{}:
103      acc_lt(C.high(64n, Nat.mul(x, 1n+m)), k, 1n+m, high_lt(x, 1n+m, hx, {==}), Bool.not(Bool.and(Nat.is_lt(C.low(64n, Nat.mul(x, 1n+m)), 1n+m), Nat.is_lt(C.low(64n, Nat.mul(x, 1n+m)), SR.pow2mod(64n, 1n+m)))), e)
104
105# THEOREM: an accepted draw is below n
106def draw_lt(+x: Nat, +n: Nat, +k: Nat, +hx: {C.fits(64n, x) == True{} : Bool}, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +e: {SR.draw(64n, x, n) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_lt(k, n) == True{} : Bool}:
107  match n:
108    case 0n:
109      Empty.absurd({Nat.is_lt(k, 0n) == True{} : Bool}, L.false_true(hn))
110    case 1n+m:
111      draw_pos_lt(x, m, k, hx, Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n), e)
112
113# the bounded draw after a draw of x is below n > 0
114def go_lt(~S: Data, ~next: S -> WU.U64 & S, +f: Nat, +n: Nat, m: Maybe<&2, Nat>, +x: Nat, +s1: S, +hx: {C.fits(64n, x) == True{} : Bool}, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +hm: {SR.draw(64n, x, n) == m : Maybe<&2, Nat>}) -> {Nat.is_lt(pfst(S, SR.below_go(~S, ~next, f, n, m, x, s1)), n) == True{} : Bool}:
115  match f m:
116    case 0n Some{k}:
117      draw_lt(x, n, k, hx, hn, hm)
118    case 0n None{}:
119      high_lt(x, n, hx, hn)
120    case 1n+g Some{k}:
121      draw_lt(x, n, k, hx, hn, hm)
122    case 1n+g None{}:
123      go_lt(~S, ~next, g, n, SR.draw(64n, SW.value(SRC.fst64(S, next(s1))), n), SW.value(SRC.fst64(S, next(s1))), SRC.snd64(S, next(s1)), M128.fit64(SRC.fst64(S, next(s1))), hn, {==})
124
125# THEOREM: the bounded draw from any source is below n > 0
126def below_lt(~S: Data, ~next: S -> WU.U64 & S, +f: Nat, +n: Nat, +s: S, +hn: {Nat.is_lt(0n, n) == True{} : Bool}) -> {Nat.is_lt(pfst(S, SR.below(~S, ~next, f, n, s)), n) == True{} : Bool}:
127  go_lt(~S, ~next, f, n, SR.draw(64n, SW.value(SRC.fst64(S, next(s))), n), SW.value(SRC.fst64(S, next(s))), SRC.snd64(S, next(s)), M128.fit64(SRC.fst64(S, next(s))), hn, {==})