1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/math/w64.bend as SW
4	import ../../../spec/math/random/rand.bend as SR
5	import ../../../spec/math/random/source.bend as SRC
6	import ../../../src/math/u64.bend as WU
7	import ../../lib/nat.bend as N
8	import ../../lib/logic.bend as L
9	import ../../lib/arith.bend as LA
10	import ../typed/width.bend as WI
11	import ../typed/w64m128.bend as M128
12	import ../typed/w64add.bend as WA
13	import ./lemire.bend as LE
14	import ../../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
20	def 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
35	def 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
47	def 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
51	def 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
61	def 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	
64	def pfst(-S: Data, p: Nat & S) -> Nat:
65	  (k, s) = p
66	  k
67	
68	def some_or(m: Maybe<&2, Nat>, +d: Nat) -> Nat:
69	  match m:
70	    case None{}:
71	      d
72	    case Some{x}:
73	      x
74	
75	def is_some(m: Maybe<&2, Nat>) -> Bool:
76	  match m:
77	    case None{}:
78	      False{}
79	    case Some{x}:
80	      True{}
81	
82	def 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	
86	def 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	
89	def 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	
97	def 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
106	def 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
114	def 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
126	def 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, {==})