proofs/math/random/uint64n.bend

bend-collections-laws-math@1.0.0.0 · 335 lines · 41 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
4import bend-collections-laws-math@1.0.0.0/spec/math/random/rand.bend as SR
5import bend-collections-laws-math@1.0.0.0/spec/math/random/source.bend as SRC
6import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
7import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
8import bend-collections-laws-math@1.0.0.0/src/math/random/rand.bend as R
9import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
11import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as LA
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WI
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64m128.bend as M128
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64dmrem.bend as DMR
16import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as AR
17import bend-collections-laws-math@1.0.0.0/proofs/math/random/bits.bend as BI
18import bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend as LE
19import bend-collections-laws-math@1.0.0.0/spec/math/random.bend as SRM
20import bend-collections-laws-math@1.0.0.0/proofs/lib/u32alg.bend as UA
21
22# rand.bend's uint64n computes the specification's bounded draw
23# (spec/math/random/rand.bend below: the first draw Go's uint64n accepts,
24# among at most 128) for every source and bound, and so is below n.
25
26def Z() -> WU.U64:
27  WU.U64{0, 0}
28
29def one64() -> WU.U64:
30  WU.U64{1, 0}
31
32# ---- the threshold 2^64 mod n ----
33
34def q_one(+q: Nat, +one: Nat, +h1: {one == 1n : Nat}, +c: Bool, +hc: {Nat.is_eq(q, 0n) == c : Bool}, +hq0: {c == False{} : Bool}, +hq1: {C.fits(1n, q) == True{} : Bool}) -> {q == one : Nat}:
35  match q:
36    case 0n:
37      Empty.absurd({0n == one : Nat}, L.true_false(Equal.trans(Bool, True{}, c, False{}, hc, hq0)))
38    case 1n:
39      Equal.sym(Nat, one, 1n, h1)
40    case 2n+r:
41      Empty.absurd({2n+r == one : Nat}, L.false_true(hq1))
42
43def add_eq0_r(+a: Nat, +b: Nat, +h: {Nat.add(a, b) == 0n : Nat}) -> {b == 0n : Nat}:
44  match a:
45    case 0n:
46      h
47    case 1n+p:
48      Empty.absurd({b == 0n : Nat}, N.succ_zero(Nat.add(p, b), h))
49
50def q_nz_c(+q: Nat, +s: Nat, +vn: Nat, +hn: {Nat.is_eq(vn, 0n) == False{} : Bool}, +e: {Nat.add(s, vn) == C.shift(64n, q) : Nat}, +c: Bool, +hc: {Nat.is_eq(q, 0n) == c : Bool}) -> {c == False{} : Bool}:
51  match c:
52    case False{}:
53      {==}
54    case True{}:
55      +hq = N.eq_from_is_eq(q, 0n, hc)
56      +sum0 = Equal.trans(Nat, Nat.add(s, vn), C.shift(64n, q), 0n, e, Equal.trans(Nat, C.shift(64n, q), C.shift(64n, 0n), 0n, Equal.cong(Nat, Nat, z => C.shift(64n, z), q, 0n, hq), WI.shift_zero(64n)))
57      +v0 = add_eq0_r(s, vn, sum0)
58      Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_eq(vn, 0n), False{}, Equal.sym(Bool, Nat.is_eq(vn, 0n), True{}, Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), vn, 0n, v0)), hn)))
59
60def q_nz(+q: Nat, +s: Nat, +vn: Nat, +hn: {Nat.is_eq(vn, 0n) == False{} : Bool}, +e: {Nat.add(s, vn) == C.shift(64n, q) : Nat}) -> {Nat.is_eq(q, 0n) == False{} : Bool}:
61  q_nz_c(q, s, vn, hn, e, Nat.is_eq(q, 0n), {==})
62
63# a nonzero word and its negation add up to 2^64
64def neg_sum(+one: Nat, +h1: {one == 1n : Nat}, +n: WU.U64, +hn: {Nat.is_eq(SW.value(n), 0n) == False{} : Bool}) -> {Nat.add(SW.value(X.sub(Z(), n)), SW.value(n)) == C.shift(64n, one) : Nat}:
65  +s = SW.value(X.sub(Z(), n))
66  +vn = SW.value(n)
67  +q = M128.QSUB(one, Z(), n)
68  +e = M128.sub_eq(one, h1, Z(), n)
69  +hs = Equal.trans(Bool, C.fits(65n, C.shift(64n, q)), C.fits(65n, Nat.add(s, vn)), True{}, Equal.cong(Nat, Bool, z => C.fits(65n, z), C.shift(64n, q), Nat.add(s, vn), Equal.sym(Nat, Nat.add(s, vn), C.shift(64n, q), e)), M128.sum_fits(64n, s, vn, M128.fit64(X.sub(Z(), n)), M128.fit64(n)))
70  +hq1 = Equal.trans(Bool, C.fits(1n, q), C.fits(1n, C.high(64n, C.shift(64n, q))), True{}, Equal.cong(Nat, Bool, z => C.fits(1n, z), q, C.high(64n, C.shift(64n, q)), Equal.sym(Nat, C.high(64n, C.shift(64n, q)), q, WI.high_u(64n, 0n, q, {==}))), M128.fits_hi(C.shift(64n, q), hs))
71  +hq = q_nz(q, s, vn, hn, e)
72  %q_one(q, one, h1, Nat.is_eq(q, 0n), {==}, hq, hq1) : {Nat.add(s, vn) == C.shift(64n, _) : Nat}
73  e
74
75# pow2mod through a symbolic one (2^64 is never a closed term)
76def pm_one(+w: Nat, +m: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {SR.pow2mod(w, 1n+m) == Nat.mod(C.shift(w, one), 1n+m) : Nat}:
77  %Equal.sym(Nat, one, 1n, h1) : {SR.pow2mod(w, 1n+m) == Nat.mod(C.shift(w, _), 1n+m) : Nat}
78  LE.pm(w, m)
79
80def thresh_m(+one: Nat, +h1: {one == 1n : Nat}, +n: WU.U64, +m: Nat, +hv: {SW.value(n) == 1n+m : Nat}, +hz: {X.is_zero(n) == False{} : Bool}) -> {SW.value(R.thresh(n)) == SR.pow2mod(64n, 1n+m) : Nat}:
81  +s = SW.value(X.sub(Z(), n))
82  +hn = Equal.trans(Bool, Nat.is_eq(SW.value(n), 0n), X.is_zero(n), False{}, Equal.sym(Bool, X.is_zero(n), Nat.is_eq(SW.value(n), 0n), WA.is_zero_value(n)), hz)
83  +ns = Equal.trans(Nat, Nat.add(s, 1n+m), Nat.add(s, SW.value(n)), C.shift(64n, one), Equal.cong(Nat, Nat, z => Nat.add(s, z), 1n+m, SW.value(n), Equal.sym(Nat, SW.value(n), 1n+m, hv)), neg_sum(one, h1, n, hn))
84  Equal.trans(Nat, SW.value(R.thresh(n)), Nat.mod(s, SW.value(n)), SR.pow2mod(64n, 1n+m),
85    DMR.divmod_rem(X.sub(Z(), n), n, hz),
86    %Equal.sym(Nat, SW.value(n), 1n+m, hv) : {Nat.mod(s, _) == SR.pow2mod(64n, 1n+m) : Nat}
87    Equal.trans(Nat, Nat.mod(s, 1n+m), Nat.mod(Nat.add(Nat.mul(1n, 1n+m), s), 1n+m), SR.pow2mod(64n, 1n+m),
88      Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(1n, 1n+m), s), 1n+m), Nat.mod(s, 1n+m), AR.absorb(m, 1n, s)),
89      %Equal.sym(Nat, Nat.mul(1n, 1n+m), 1n+m, LA.one_mul(1n+m)) : {Nat.mod(Nat.add(_, s), 1n+m) == SR.pow2mod(64n, 1n+m) : Nat}
90      %N.add_comm(s, 1n+m) : {Nat.mod(_, 1n+m) == SR.pow2mod(64n, 1n+m) : Nat}
91      %Equal.sym(Nat, Nat.add(s, 1n+m), C.shift(64n, one), ns) : {Nat.mod(_, 1n+m) == SR.pow2mod(64n, 1n+m) : Nat}
92      Equal.sym(Nat, SR.pow2mod(64n, 1n+m), Nat.mod(C.shift(64n, one), 1n+m), pm_one(64n, m, one, h1))))
93
94# n - 1 for a nonzero n
95def pred_value(+n: WU.U64, +m: Nat, +hv: {SW.value(n) == 1n+m : Nat}) -> {SW.value(X.sub(n, one64())) == m : Nat}:
96  +hle = Equal.trans(Bool, Nat.is_le(1n, SW.value(n)), Nat.is_le(1n, 1n+m), True{}, Equal.cong(Nat, Bool, z => Nat.is_le(1n, z), SW.value(n), 1n+m, hv), N.zero_le(m))
97  Equal.trans(Nat, SW.value(X.sub(n, one64())), Nat.sub(SW.value(n), 1n), m, WA.sub_value(n, one64(), hle),
98    %Equal.sym(Nat, SW.value(n), 1n+m, hv) : {Nat.sub(_, 1n) == m : Nat}
99    N.sub_zero(m))
100
101# the power-of-two test is n & (n - 1) == 0
102def pow2_value(+n: WU.U64, +m: Nat, +hv: {SW.value(n) == 1n+m : Nat}) -> {R.is_pow2(n) == Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) : Bool}:
103  Equal.trans(Bool, R.is_pow2(n), Nat.is_eq(SW.value(R.and64(n, X.sub(n, one64()))), 0n), Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n),
104    WA.is_zero_value(R.and64(n, X.sub(n, one64()))),
105    %Equal.sym(Nat, SW.value(R.and64(n, X.sub(n, one64()))), SR.and_bits(64n, SW.value(n), SW.value(X.sub(n, one64()))), BI.and64_value(n, X.sub(n, one64()))) : {Nat.is_eq(_, 0n) == Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) : Bool}
106    %Equal.sym(Nat, SW.value(n), 1n+m, hv) : {Nat.is_eq(SR.and_bits(64n, _, SW.value(X.sub(n, one64()))), 0n) == Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) : Bool}
107    %Equal.sym(Nat, SW.value(X.sub(n, one64())), m, pred_value(n, m, hv)) : {Nat.is_eq(SR.and_bits(64n, 1n+m, _), 0n) == Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) : Bool}
108    {==})
109
110# the mask is x & (n - 1)
111def mask_value(+x: WU.U64, +n: WU.U64, +m: Nat, +hv: {SW.value(n) == 1n+m : Nat}) -> {SW.value(R.and64(x, X.sub(n, one64()))) == SR.and_bits(64n, SW.value(x), m) : Nat}:
112  %Equal.sym(Nat, SW.value(R.and64(x, X.sub(n, one64()))), SR.and_bits(64n, SW.value(x), SW.value(X.sub(n, one64()))), BI.and64_value(x, X.sub(n, one64()))) : {_ == SR.and_bits(64n, SW.value(x), m) : Nat}
113  %Equal.sym(Nat, SW.value(X.sub(n, one64())), m, pred_value(n, m, hv)) : {SR.and_bits(64n, SW.value(x), _) == SR.and_bits(64n, SW.value(x), m) : Nat}
114  {==}
115
116# the halves of the 128-bit product
117def m128_lo(+x: WU.U64, +n: WU.U64) -> {SW.value(X.pfst(X.mul128(x, n))) == C.low(64n, Nat.mul(SW.value(x), SW.value(n))) : Nat}:
118  match x n:
119    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
120      +r = SW.value(X.pfst(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh})))
121      +q = SW.value(X.psnd(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh})))
122      %M128.m128_value(al, ah, bl, bh) : {r == C.low(64n, _) : Nat}
123      Equal.sym(Nat, C.low(64n, Nat.add(r, C.shift(64n, q))), r, WI.low_u(64n, r, q, M128.fit64(X.pfst(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh})))))
124
125def m128_hi(+x: WU.U64, +n: WU.U64) -> {SW.value(X.psnd(X.mul128(x, n))) == C.high(64n, Nat.mul(SW.value(x), SW.value(n))) : Nat}:
126  match x n:
127    case WU.U64{+al, +ah} WU.U64{+bl, +bh}:
128      +r = SW.value(X.pfst(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh})))
129      +q = SW.value(X.psnd(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh})))
130      %M128.m128_value(al, ah, bl, bh) : {q == C.high(64n, _) : Nat}
131      Equal.sym(Nat, C.high(64n, Nat.add(r, C.shift(64n, q))), q, WI.high_u(64n, r, q, M128.fit64(X.pfst(X.mul128(WU.U64{al, ah}, WU.U64{bl, bh})))))
132
133# ---- the draws ----
134
135# the specification's bounded draw after a draw of x with state s
136def cont(~S: Data, ~next: S -> WU.U64 & S, f: Nat, +n: Nat, +x: Nat, +s: S) -> Nat & S:
137  SR.below_go(~S, ~next, f, n, SR.draw(64n, x, n), x, s)
138
139def below_cont(~S: Data, ~next: S -> WU.U64 & S, +f: Nat, +n: Nat, +s: S) -> {SR.below(~S, ~next, f, n, s) == cont(~S, ~next, f, n, SW.value(SRC.fst64(S, next(s))), SRC.snd64(S, next(s))) : Nat & S}:
140  {==}
141
142def fixpoint(~S: Data, ~next: S -> WU.U64 & S, +f: Nat, +n: WU.U64, +t: WU.U64, +hi: WU.U64, +lo: WU.U64, +s: S, +h: {X.lt(lo, t) == False{} : Bool}) -> {R.retry(~S, ~next, f, n, t, R.D{hi, lo, s}) == R.D{hi, lo, s} : R.Draw<S>}:
143  match f:
144    case 0n:
145      {==}
146    case 1n+g:
147      %Equal.sym(Bool, X.lt(lo, t), False{}, h) : {R.retry(~S, ~next, g, n, t, R.again(~S, ~next, n, hi, lo, s, _)) == R.D{hi, lo, s} : R.Draw<S>}
148      fixpoint(~S, ~next, g, n, t, hi, lo, s, h)
149
150# Lemire's decision of the specification: accept unless lo < 2^64 mod n
151def dec(+x: Nat, +m: Nat, +hp: {Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) == False{} : Bool}, +htn: {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(C.low(64n, Nat.mul(x, 1n+m)), SR.pow2mod(64n, 1n+m)) == c : Bool}) -> {SR.draw(64n, x, 1n+m) == SR.accept(C.high(64n, Nat.mul(x, 1n+m)), Bool.not(c)) : Maybe<&2, Nat>}:
152  %Equal.sym(Maybe<&2, Nat>, SR.draw(64n, x, 1n+m), SR.lemire(64n, 1n+m, C.high(64n, Nat.mul(x, 1n+m)), C.low(64n, Nat.mul(x, 1n+m))), LE.draw_lemire(64n, m, x, hp)) : {_ == SR.accept(C.high(64n, Nat.mul(x, 1n+m)), Bool.not(c)) : Maybe<&2, Nat>}
153  %Equal.sym(Bool, 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))), c, LE.and_lt(C.low(64n, Nat.mul(x, 1n+m)), 1n+m, SR.pow2mod(64n, 1n+m), htn, c, hc)) : {SR.accept(C.high(64n, Nat.mul(x, 1n+m)), Bool.not(_)) == SR.accept(C.high(64n, Nat.mul(x, 1n+m)), Bool.not(c)) : Maybe<&2, Nat>}
154  {==}
155
156def last_acc(~S: Data, ~next: S -> WU.U64 & S, +h: Nat, +ok: Bool, +x: Nat, +n: Nat, +s: S, +hh: {h == C.high(64n, Nat.mul(x, n)) : Nat}) -> {SR.below_go(~S, ~next, 0n, n, SR.accept(h, ok), x, s) == (h, s) : Nat & S}:
157  match ok:
158    case True{}:
159      {==}
160    case False{}:
161      %Equal.sym(Nat, h, C.high(64n, Nat.mul(x, n)), hh) : {(C.high(64n, Nat.mul(x, n)), s) == (_, s) : Nat & S}
162      {==}
163
164def pm_lt(+m: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}:
165  Equal.trans(Bool, Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m), Nat.is_lt(Nat.mod(C.shift(64n, one), 1n+m), 1n+m), True{},
166    Equal.cong(Nat, Bool, z => Nat.is_lt(z, 1n+m), SR.pow2mod(64n, 1n+m), Nat.mod(C.shift(64n, one), 1n+m), pm_one(64n, m, one, h1)),
167    AR.dm_lt(m, C.shift(64n, one)))
168
169# the implementation's rejection test is the specification's
170def lt_low(+x: WU.U64, +n: WU.U64, +m: Nat, +t: WU.U64, +hv: {SW.value(n) == 1n+m : Nat}, +ht: {SW.value(t) == SR.pow2mod(64n, 1n+m) : Nat}) -> {X.lt(X.pfst(X.mul128(x, n)), t) == Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), SR.pow2mod(64n, 1n+m)) : Bool}:
171  Equal.trans(Bool, X.lt(X.pfst(X.mul128(x, n)), t), Nat.is_lt(SW.value(X.pfst(X.mul128(x, n))), SW.value(t)), Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), SR.pow2mod(64n, 1n+m)),
172    WA.lt_value(X.pfst(X.mul128(x, n)), t),
173    %Equal.sym(Nat, SW.value(X.pfst(X.mul128(x, n))), C.low(64n, Nat.mul(SW.value(x), SW.value(n))), m128_lo(x, n)) : {Nat.is_lt(_, SW.value(t)) == Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), SR.pow2mod(64n, 1n+m)) : Bool}
174    %Equal.sym(Nat, SW.value(n), 1n+m, hv) : {Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), _)), SW.value(t)) == Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), SR.pow2mod(64n, 1n+m)) : Bool}
175    %Equal.sym(Nat, SW.value(t), SR.pow2mod(64n, 1n+m), ht) : {Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), _) == Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), SR.pow2mod(64n, 1n+m)) : Bool}
176    {==})
177
178def hi_value(+x: WU.U64, +n: WU.U64, +m: Nat, +hv: {SW.value(n) == 1n+m : Nat}) -> {SW.value(X.psnd(X.mul128(x, n))) == C.high(64n, Nat.mul(SW.value(x), 1n+m)) : Nat}:
179  %hv : {SW.value(X.psnd(X.mul128(x, n))) == C.high(64n, Nat.mul(SW.value(x), _)) : Nat}
180  m128_hi(x, n)
181
182def hd_of(+x: WU.U64, +n: WU.U64, +m: Nat, +t: WU.U64, +hv: {SW.value(n) == 1n+m : Nat}, +hp: {Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) == False{} : Bool}, +htn: {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}, +ht: {SW.value(t) == SR.pow2mod(64n, 1n+m) : Nat}, +c: Bool, +hc: {X.lt(X.pfst(X.mul128(x, n)), t) == c : Bool}) -> {SR.draw(64n, SW.value(x), 1n+m) == SR.accept(C.high(64n, Nat.mul(SW.value(x), 1n+m)), Bool.not(c)) : Maybe<&2, Nat>}:
183  dec(SW.value(x), m, hp, htn, c, Equal.trans(Bool, Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), SR.pow2mod(64n, 1n+m)), X.lt(X.pfst(X.mul128(x, n)), t), c, Equal.sym(Bool, X.lt(X.pfst(X.mul128(x, n)), t), Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), SR.pow2mod(64n, 1n+m)), lt_low(x, n, m, t, hv, ht)), hc))
184
185# one retry step, accepted
186def step_false(~S: Data, ~next: S -> WU.U64 & S, +g: Nat, +n: WU.U64, +m: Nat, +t: WU.U64, +x: WU.U64, +s1: S, +hv: {SW.value(n) == 1n+m : Nat}, +hp: {Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) == False{} : Bool}, +htn: {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}, +ht: {SW.value(t) == SR.pow2mod(64n, 1n+m) : Nat}, +hc: {X.lt(X.pfst(X.mul128(x, n)), t) == False{} : Bool}) -> {SRM.val_pair(S, R.result(S, R.retry(~S, ~next, g, n, t, R.again(~S, ~next, n, X.psnd(X.mul128(x, n)), X.pfst(X.mul128(x, n)), s1, False{})))) == cont(~S, ~next, 1n+g, 1n+m, SW.value(x), s1) : Nat & S}:
187  +hi = X.psnd(X.mul128(x, n))
188  +lo = X.pfst(X.mul128(x, n))
189  +H = C.high(64n, Nat.mul(SW.value(x), 1n+m))
190  %Equal.sym(R.Draw<S>, R.retry(~S, ~next, g, n, t, R.D{hi, lo, s1}), R.D{hi, lo, s1}, fixpoint(~S, ~next, g, n, t, hi, lo, s1, hc)) : {SRM.val_pair(S, R.result(S, _)) == cont(~S, ~next, 1n+g, 1n+m, SW.value(x), s1) : Nat & S}
191  %Equal.sym(Maybe<&2, Nat>, SR.draw(64n, SW.value(x), 1n+m), SR.accept(H, True{}), hd_of(x, n, m, t, hv, hp, htn, ht, False{}, hc)) : {(SW.value(hi), s1) == SR.below_go(~S, ~next, 1n+g, 1n+m, _, SW.value(x), s1) : Nat & S}
192  Equal.cong(Nat, Nat & S, z => (z, s1), SW.value(hi), H, hi_value(x, n, m, hv))
193
194# one retry step, rejected: the next draw
195def step_true(~S: Data, ~next: S -> WU.U64 & S, +g: Nat, +n: WU.U64, +m: Nat, +t: WU.U64, +x: WU.U64, +s1: S, +hv: {SW.value(n) == 1n+m : Nat}, +hp: {Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) == False{} : Bool}, +htn: {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}, +ht: {SW.value(t) == SR.pow2mod(64n, 1n+m) : Nat}, +hc: {X.lt(X.pfst(X.mul128(x, n)), t) == True{} : Bool}, +rec: {SRM.val_pair(S, R.result(S, R.retry(~S, ~next, g, n, t, R.draw(S, n, next(s1))))) == cont(~S, ~next, g, 1n+m, SW.value(SRC.fst64(S, next(s1))), SRC.snd64(S, next(s1))) : Nat & S}) -> {SRM.val_pair(S, R.result(S, R.retry(~S, ~next, g, n, t, R.again(~S, ~next, n, X.psnd(X.mul128(x, n)), X.pfst(X.mul128(x, n)), s1, True{})))) == cont(~S, ~next, 1n+g, 1n+m, SW.value(x), s1) : Nat & S}:
196  +H = C.high(64n, Nat.mul(SW.value(x), 1n+m))
197  %Equal.sym(Maybe<&2, Nat>, SR.draw(64n, SW.value(x), 1n+m), SR.accept(H, False{}), hd_of(x, n, m, t, hv, hp, htn, ht, True{}, hc)) : {SRM.val_pair(S, R.result(S, R.retry(~S, ~next, g, n, t, R.draw(S, n, next(s1))))) == SR.below_go(~S, ~next, 1n+g, 1n+m, _, SW.value(x), s1) : Nat & S}
198  rec
199
200def step_case(~S: Data, ~next: S -> WU.U64 & S, +g: Nat, +n: WU.U64, +m: Nat, +t: WU.U64, +x: WU.U64, +s1: S, +hv: {SW.value(n) == 1n+m : Nat}, +hp: {Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) == False{} : Bool}, +htn: {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}, +ht: {SW.value(t) == SR.pow2mod(64n, 1n+m) : Nat}, +c: Bool, +hc: {X.lt(X.pfst(X.mul128(x, n)), t) == c : Bool}, +rec: {SRM.val_pair(S, R.result(S, R.retry(~S, ~next, g, n, t, R.draw(S, n, next(s1))))) == cont(~S, ~next, g, 1n+m, SW.value(SRC.fst64(S, next(s1))), SRC.snd64(S, next(s1))) : Nat & S}) -> {SRM.val_pair(S, R.result(S, R.retry(~S, ~next, g, n, t, R.again(~S, ~next, n, X.psnd(X.mul128(x, n)), X.pfst(X.mul128(x, n)), s1, c)))) == cont(~S, ~next, 1n+g, 1n+m, SW.value(x), s1) : Nat & S}:
201  match c:
202    case False{}:
203      step_false(~S, ~next, g, n, m, t, x, s1, hv, hp, htn, ht, hc)
204    case True{}:
205      step_true(~S, ~next, g, n, m, t, x, s1, hv, hp, htn, ht, hc, rec)
206
207# THEOREM (the rejection loop): f retries from the draw p follow the
208# specification's draws
209def loop(~S: Data, ~next: S -> WU.U64 & S, +f: Nat, +n: WU.U64, +m: Nat, +t: WU.U64, p: WU.U64 & S, +hv: {SW.value(n) == 1n+m : Nat}, +hp: {Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) == False{} : Bool}, +htn: {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}, +ht: {SW.value(t) == SR.pow2mod(64n, 1n+m) : Nat}) -> {SRM.val_pair(S, R.result(S, R.retry(~S, ~next, f, n, t, R.draw(S, n, p)))) == cont(~S, ~next, f, 1n+m, SW.value(SRC.fst64(S, p)), SRC.snd64(S, p)) : Nat & S}:
210  match f p:
211    case 0n Tuple{+x, +s1}:
212      +H = C.high(64n, Nat.mul(SW.value(x), 1n+m))
213      +c0 = X.lt(X.pfst(X.mul128(x, n)), t)
214      %Equal.sym(Maybe<&2, Nat>, SR.draw(64n, SW.value(x), 1n+m), SR.accept(H, Bool.not(c0)), hd_of(x, n, m, t, hv, hp, htn, ht, c0, {==})) : {(SW.value(X.psnd(X.mul128(x, n))), s1) == SR.below_go(~S, ~next, 0n, 1n+m, _, SW.value(x), s1) : Nat & S}
215      %Equal.sym(Nat & S, SR.below_go(~S, ~next, 0n, 1n+m, SR.accept(H, Bool.not(c0)), SW.value(x), s1), (H, s1), last_acc(~S, ~next, H, Bool.not(c0), SW.value(x), 1n+m, s1, {==})) : {(SW.value(X.psnd(X.mul128(x, n))), s1) == _ : Nat & S}
216      Equal.cong(Nat, Nat & S, z => (z, s1), SW.value(X.psnd(X.mul128(x, n))), H, hi_value(x, n, m, hv))
217    case 1n+g Tuple{+x, +s1}:
218      step_case(~S, ~next, g, n, m, t, x, s1, hv, hp, htn, ht, X.lt(X.pfst(X.mul128(x, n)), t), {==}, loop(~S, ~next, g, n, m, t, next(s1), hv, hp, htn, ht))
219
220def lt_low_n(+x: WU.U64, +n: WU.U64, +m: Nat, +hv: {SW.value(n) == 1n+m : Nat}) -> {X.lt(X.pfst(X.mul128(x, n)), n) == Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), 1n+m) : Bool}:
221  Equal.trans(Bool, X.lt(X.pfst(X.mul128(x, n)), n), Nat.is_lt(SW.value(X.pfst(X.mul128(x, n))), SW.value(n)), Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), 1n+m),
222    WA.lt_value(X.pfst(X.mul128(x, n)), n),
223    %Equal.sym(Nat, SW.value(X.pfst(X.mul128(x, n))), C.low(64n, Nat.mul(SW.value(x), SW.value(n))), m128_lo(x, n)) : {Nat.is_lt(_, SW.value(n)) == Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), 1n+m) : Bool}
224    %Equal.sym(Nat, SW.value(n), 1n+m, hv) : {Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), _)), _) == Nat.is_lt(C.low(64n, Nat.mul(SW.value(x), 1n+m)), 1n+m) : Bool}
225    {==})
226
227# lo >= n: the first draw is accepted by the specification too
228def first_false(~S: Data, ~next: S -> WU.U64 & S, +n: WU.U64, +m: Nat, +x: WU.U64, +s1: S, +hv: {SW.value(n) == 1n+m : Nat}, +hp: {Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) == False{} : Bool}, +htn: {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}, +hc: {X.lt(X.pfst(X.mul128(x, n)), n) == False{} : Bool}) -> {SRM.val_pair(S, R.lemire_small(~S, ~next, n, X.psnd(X.mul128(x, n)), X.pfst(X.mul128(x, n)), s1, False{})) == cont(~S, ~next, 127n, 1n+m, SW.value(x), s1) : Nat & S}:
229  +L = C.low(64n, Nat.mul(SW.value(x), 1n+m))
230  +H = C.high(64n, Nat.mul(SW.value(x), 1n+m))
231  +pm = SR.pow2mod(64n, 1n+m)
232  +hn = Equal.trans(Bool, Nat.is_lt(L, 1n+m), X.lt(X.pfst(X.mul128(x, n)), n), False{},
233    Equal.sym(Bool, X.lt(X.pfst(X.mul128(x, n)), n), Nat.is_lt(L, 1n+m), lt_low_n(x, n, m, hv)),
234    hc)
235  +hl = N.le_not_lt(L, pm, N.le_trans(pm, 1n+m, L, N.lt_le(pm, 1n+m, htn), N.not_lt_le(L, 1n+m, hn)))
236  %Equal.sym(Maybe<&2, Nat>, SR.draw(64n, SW.value(x), 1n+m), SR.accept(H, True{}), dec(SW.value(x), m, hp, htn, False{}, hl)) : {(SW.value(X.psnd(X.mul128(x, n))), s1) == SR.below_go(~S, ~next, 127n, 1n+m, _, SW.value(x), s1) : Nat & S}
237  Equal.cong(Nat, Nat & S, z => (z, s1), SW.value(X.psnd(X.mul128(x, n))), H, hi_value(x, n, m, hv))
238
239# the first draw: accepted at once when lo >= n, else the loop
240def first_case(~S: Data, ~next: S -> WU.U64 & S, +one: Nat, +h1: {one == 1n : Nat}, +n: WU.U64, +m: Nat, +x: WU.U64, +s1: S, +hv: {SW.value(n) == 1n+m : Nat}, +hz: {X.is_zero(n) == False{} : Bool}, +hp: {Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) == False{} : Bool}, +htn: {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}, +c: Bool, +hc: {X.lt(X.pfst(X.mul128(x, n)), n) == c : Bool}) -> {SRM.val_pair(S, R.lemire_small(~S, ~next, n, X.psnd(X.mul128(x, n)), X.pfst(X.mul128(x, n)), s1, c)) == cont(~S, ~next, 127n, 1n+m, SW.value(x), s1) : Nat & S}:
241  match c:
242    case True{}:
243      loop(~S, ~next, 127n, n, m, R.thresh(n), (x, s1), hv, hp, htn, thresh_m(one, h1, n, m, hv, hz))
244    case False{}:
245      first_false(~S, ~next, n, m, x, s1, hv, hp, htn, hc)
246
247# ---- the mask branch and n == 0 ----
248
249def mask_pair(-S: Data, +n: WU.U64, +m: Nat, p: WU.U64 & S, +hv: {SW.value(n) == 1n+m : Nat}) -> {SRM.val_pair(S, R.mask(S, n, p)) == (SR.and_bits(64n, SW.value(SRC.fst64(S, p)), m), SRC.snd64(S, p)) : Nat & S}:
250  match p:
251    case Tuple{+x, +s1}:
252      Equal.cong(Nat, Nat & S, z => (z, s1), SW.value(R.and64(x, X.sub(n, one64()))), SR.and_bits(64n, SW.value(x), m), mask_value(x, n, m, hv))
253
254def all1(n: Nat) -> Word(n):
255  match n:
256    case 0n:
257      WNil{}
258    case 1n+p:
259      WCon{True{}, all1(p)}
260
261def and_true(+b: Bool) -> {Bool.and(b, True{}) == b : Bool}:
262  match b:
263    case True{}:
264      {==}
265    case False{}:
266      {==}
267
268def and_all1(+n: Nat, +w: Word(n)) -> {Word.and(n, w, all1(n)) == w : Word(n)}:
269  match n w:
270    case 0n WNil{}:
271      {==}
272    case 1n+p WCon{+x, +t}:
273      %Equal.sym(Bool, Bool.and(x, True{}), x, and_true(x)) : {WCon{_, Word.and(p, t, all1(p))} == WCon{x, t} : Word(1n+p)}
274      Equal.cong(Word(p), Word(1n+p), z => WCon{x, z}, Word.and(p, t, all1(p)), t, and_all1(p, t))
275
276def uand_all(+y: U32, +M: U32, +hM: {M == U32{all1(32n)} : U32}) -> {U32.and(y, M) == y : U32}:
277  match y:
278    case U32{+w}:
279      %Equal.sym(U32, M, U32{all1(32n)}, hM) : {U32.and(U32{w}, _) == U32{w} : U32}
280      Equal.cong(Word(32n), U32, z => U32{z}, Word.and(32n, w, all1(32n)), w, and_all1(32n, w))
281
282# n == 0 is read as 2^64: the whole word
283def zero_pair(-S: Data, p: WU.U64 & S) -> {SRM.val_pair(S, R.mask(S, Z(), p)) == (SW.value(SRC.fst64(S, p)), SRC.snd64(S, p)) : Nat & S}:
284  match p:
285    case Tuple{+x, +s1}:
286      match x:
287        case WU.U64{+l, +h}:
288          %Equal.sym(U32, U32.and(l, X.lo(X.sub(Z(), one64()))), l, uand_all(l, X.lo(X.sub(Z(), one64())), {==})) : {(Nat.add(U32.to_nat(_), C.shift(32n, U32.to_nat(U32.and(h, X.hi(X.sub(Z(), one64())))))), s1) == (SW.value(WU.U64{l, h}), s1) : Nat & S}
289          %Equal.sym(U32, U32.and(h, X.hi(X.sub(Z(), one64()))), h, uand_all(h, X.hi(X.sub(Z(), one64())), {==})) : {(Nat.add(U32.to_nat(l), C.shift(32n, U32.to_nat(_))), s1) == (SW.value(WU.U64{l, h}), s1) : Nat & S}
290          {==}
291
292# ---- uint64n ----
293
294def top_first(~S: Data, ~next: S -> WU.U64 & S, +one: Nat, +h1: {one == 1n : Nat}, +n: WU.U64, +m: Nat, p: WU.U64 & S, +hv: {SW.value(n) == 1n+m : Nat}, +hz: {X.is_zero(n) == False{} : Bool}, +hp: {Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) == False{} : Bool}) -> {SRM.val_pair(S, R.lemire_first(~S, ~next, n, R.draw(S, n, p))) == cont(~S, ~next, 127n, 1n+m, SW.value(SRC.fst64(S, p)), SRC.snd64(S, p)) : Nat & S}:
295  match p:
296    case Tuple{+x, +s1}:
297      first_case(~S, ~next, one, h1, n, m, x, s1, hv, hz, hp, pm_lt(m, one, h1), X.lt(X.pfst(X.mul128(x, n)), n), {==})
298
299def value_nz(~S: Data, ~next: S -> WU.U64 & S, +one: Nat, +h1: {one == 1n : Nat}, +s: S, +n: WU.U64, +m: Nat, +hv: {SW.value(n) == 1n+m : Nat}, +hz: {X.is_zero(n) == False{} : Bool}, +c: Bool, +hc: {Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n) == c : Bool}) -> {SRM.val_pair(S, R.uint64n_pick(~S, ~next, s, n, c)) == SR.below(~S, ~next, 127n, 1n+m, s) : Nat & S}:
300  match c:
301    case True{}:
302      +x = SW.value(SRC.fst64(S, next(s)))
303      Equal.trans(Nat & S, SRM.val_pair(S, R.mask(S, n, next(s))), (SR.and_bits(64n, x, m), SRC.snd64(S, next(s))), SR.below(~S, ~next, 127n, 1n+m, s),
304        mask_pair(S, n, m, next(s), hv),
305        %Equal.sym(Maybe<&2, Nat>, SR.draw(64n, x, 1n+m), Some{SR.and_bits(64n, x, m)}, LE.draw_mask(64n, m, x, hc)) : {(SR.and_bits(64n, x, m), SRC.snd64(S, next(s))) == SR.below_go(~S, ~next, 127n, 1n+m, _, x, SRC.snd64(S, next(s))) : Nat & S}
306        {==})
307    case False{}:
308      Equal.trans(Nat & S, SRM.val_pair(S, R.lemire_first(~S, ~next, n, R.draw(S, n, next(s)))), cont(~S, ~next, 127n, 1n+m, SW.value(SRC.fst64(S, next(s))), SRC.snd64(S, next(s))), SR.below(~S, ~next, 127n, 1n+m, s),
309        top_first(~S, ~next, one, h1, n, m, next(s), hv, hz, hc),
310        Equal.sym(Nat & S, SR.below(~S, ~next, 127n, 1n+m, s), cont(~S, ~next, 127n, 1n+m, SW.value(SRC.fst64(S, next(s))), SRC.snd64(S, next(s))), below_cont(~S, ~next, 127n, 1n+m, s)))
311
312def zero_word(+n: WU.U64, +h: {X.is_zero(n) == True{} : Bool}) -> {n == Z() : WU.U64}:
313  match n:
314    case WU.U64{+l, +hh}:
315      +el = UA.eq_of(l, 0, L.and_left(U32.is_zero(l), U32.is_zero(hh), h))
316      +eh = UA.eq_of(hh, 0, L.and_right(U32.is_zero(l), U32.is_zero(hh), h))
317      %Equal.sym(U32, l, 0, el) : {WU.U64{_, hh} == Z() : WU.U64}
318      %Equal.sym(U32, hh, 0, eh) : {WU.U64{0, _} == Z() : WU.U64}
319      {==}
320
321def value_vn(~S: Data, ~next: S -> WU.U64 & S, +s: S, +n: WU.U64, +vn: Nat, +hv: {SW.value(n) == vn : Nat}) -> {SRM.val_pair(S, R.uint64n(~S, ~next, s, n)) == SR.below(~S, ~next, 127n, SW.value(n), s) : Nat & S}:
322  match vn:
323    case 0n:
324      +hz = Equal.trans(Bool, X.is_zero(n), Nat.is_eq(SW.value(n), 0n), True{}, WA.is_zero_value(n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(n), 0n, hv))
325      %Equal.sym(WU.U64, n, Z(), zero_word(n, hz)) : {SRM.val_pair(S, R.uint64n(~S, ~next, s, _)) == SR.below(~S, ~next, 127n, SW.value(_), s) : Nat & S}
326      zero_pair(S, next(s))
327    case 1n+m:
328      +hz = Equal.trans(Bool, X.is_zero(n), Nat.is_eq(SW.value(n), 0n), False{}, WA.is_zero_value(n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(n), 1n+m, hv))
329      %Equal.sym(Bool, R.is_pow2(n), Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n), pow2_value(n, m, hv)) : {SRM.val_pair(S, R.uint64n_pick(~S, ~next, s, n, _)) == SR.below(~S, ~next, 127n, SW.value(n), s) : Nat & S}
330      %Equal.sym(Nat, SW.value(n), 1n+m, hv) : {SRM.val_pair(S, R.uint64n_pick(~S, ~next, s, n, Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n))) == SR.below(~S, ~next, 127n, _, s) : Nat & S}
331      value_nz(~S, ~next, 1n, {==}, s, n, m, hv, hz, Nat.is_eq(SR.and_bits(64n, 1n+m, m), 0n), {==})
332
333# THEOREM (Uint64n.value)
334def uint64n_value(~S: Data, ~next: S -> WU.U64 & S, +s: S, +n: WU.U64) -> SRM.Uint64n.value(~S, ~next, s, n):
335  value_vn(~S, ~next, s, n, SW.value(n), {==})