proofs/math/random/wrappers.bend

bend-collections-laws-math@1.0.0.0 · 273 lines · 32 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/source.bend as SRC
5import bend-collections-laws-math@1.0.0.0/spec/math/random.bend as SRM
6import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
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/u32.bend as U
12import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as WC
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64div.bend as W64D
20import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64div.bend as PD
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64mul.bend as W64M
22import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
23import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as LA
24import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as AR
25import bend-collections-laws-math@1.0.0.0/proofs/math/random/bounded.bend as MR
26import bend-collections-laws-math@1.0.0.0/proofs/math/random/lemire.bend as LE
27
28# The word slices (Go's Uint32, Int64, Int32) and the bounded wrappers
29# (Uint32N, IntN, lo + IntN(hi - lo)) of src/math/random/rand.bend, for every
30# source: the slices are the stated bits of the output, and the bounded ones
31# inherit Uint64n.lt.
32
33def v(+x: U32) -> Nat:
34  U32.to_nat(x)
35
36def val(+l: U32, +h: U32) -> Nat:
37  Nat.add(v(l), C.shift(32n, v(h)))
38
39# ---- Uint32: the top 32 bits ----
40
41def u32_p(-S: Data, p: W.U64 & S) -> {U32.to_nat(R.fst(U32, S, R.top32(S, p))) == C.high(32n, SW.value(SRC.fst64(S, p))) : Nat}:
42  match p:
43    case Tuple{x, s}:
44      match x:
45        case W.U64{+l, +h}:
46          Equal.sym(Nat, C.high(32n, val(l, h)), v(h), WW.high_u(32n, v(l), v(h), LW.vb(l)))
47
48def uint32_value(~S: Data, ~next: S -> W.U64 & S, +s: S) -> SRM.Uint32.value(~S, ~next, s):
49  u32_p(S, next(s))
50
51# ---- Int64: the low 63 bits ----
52
53def low63_v(+l: U32, +h: U32) -> {SW.value(W.U64{l, U32.and(h, 2147483647)}) == C.low(63n, val(l, h)) : Nat}:
54  +n = val(l, h)
55  Equal.trans(Nat, Nat.add(v(l), C.shift(32n, v(U32.and(h, 2147483647)))), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))), C.low(63n, n),
56    Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, z)), v(U32.and(h, 2147483647)), C.low(31n, v(h)), FB.andm(h, 31n, 2147483647, {==})),
57    Equal.sym(Nat, C.low(63n, n), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))),
58      Equal.trans(Nat, C.low(63n, n), Nat.add(C.low(32n, n), C.shift(32n, C.low(31n, C.high(32n, n)))), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))),
59        FB.low_split(32n, 31n, n),
60        Equal.trans(Nat, Nat.add(C.low(32n, n), C.shift(32n, C.low(31n, C.high(32n, n)))), Nat.add(v(l), C.shift(32n, C.low(31n, C.high(32n, n)))), Nat.add(v(l), C.shift(32n, C.low(31n, v(h)))),
61          Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, C.low(31n, C.high(32n, n)))), C.low(32n, n), v(l), WW.low_u(32n, v(l), v(h), LW.vb(l))),
62          Equal.cong(Nat, Nat, z => Nat.add(v(l), C.shift(32n, C.low(31n, z))), C.high(32n, n), v(h), WW.high_u(32n, v(l), v(h), LW.vb(l)))))))
63
64def i64_p(-S: Data, p: W.U64 & S) -> {SW.value(R.fst(W.U64, S, R.low63(S, p))) == C.low(63n, SW.value(SRC.fst64(S, p))) : Nat}:
65  match p:
66    case Tuple{x, s}:
67      match x:
68        case W.U64{+l, +h}:
69          low63_v(l, h)
70
71def int64_value(~S: Data, ~next: S -> W.U64 & S, +s: S) -> SRM.Int64.value(~S, ~next, s):
72  i64_p(S, next(s))
73
74# ---- Int32: the top 31 bits ----
75
76def half_bv(+b: Bool) -> {C.half(S.bit_value(b)) == 0n : Nat}:
77  match b:
78    case True{}:
79      {==}
80    case False{}:
81      {==}
82
83# x >> 1 is half of x
84def shr_half(+x: U32) -> {v(U32.shr(x)) == C.half(v(x)) : Nat}:
85  +b = S.bit_value(U.low_bit(x))
86  +y = v(U32.shr(x))
87  Equal.sym(Nat, C.half(v(x)), y,
88    Equal.trans(Nat, C.half(v(x)), C.half(Nat.add(b, Nat.double(y))), y,
89      Equal.cong(Nat, Nat, z => C.half(z), v(x), Nat.add(b, Nat.double(y)), U.shr_split(x)),
90      Equal.trans(Nat, C.half(Nat.add(b, Nat.double(y))), Nat.add(C.half(b), y), y, WW.half_dbl(b, y),
91        Equal.cong(Nat, Nat, z => Nat.add(z, y), C.half(b), 0n, half_bv(U.low_bit(x))))))
92
93def i32_p(-S: Data, p: W.U64 & S) -> {U32.to_nat(R.fst(U32, S, R.top31(S, p))) == C.high(33n, SW.value(SRC.fst64(S, p))) : Nat}:
94  match p:
95    case Tuple{x, s}:
96      match x:
97        case W.U64{+l, +h}:
98          Equal.trans(Nat, v(U32.shr(h)), C.half(v(h)), C.high(33n, val(l, h)),
99            shr_half(h),
100            Equal.sym(Nat, C.high(33n, val(l, h)), C.half(v(h)),
101              Equal.trans(Nat, C.high(Nat.add(32n, 1n), val(l, h)), C.high(1n, C.high(32n, val(l, h))), C.half(v(h)),
102                WW.high_comp(1n, 32n, val(l, h)),
103                Equal.cong(Nat, Nat, z => C.high(1n, z), C.high(32n, val(l, h)), v(h), WW.high_u(32n, v(l), v(h), LW.vb(l))))))
104
105def int32_value(~S: Data, ~next: S -> W.U64 & S, +s: S) -> SRM.Int32.value(~S, ~next, s):
106  i32_p(S, next(s))
107
108# ---- Uint32N ----
109
110def lo_le(-S: Data, r: W.U64 & S) -> {Nat.is_le(U32.to_nat(R.fst(U32, S, R.lo32(S, r))), SW.value(R.fst(W.U64, S, r))) == True{} : Bool}:
111  match r:
112    case Tuple{x, s}:
113      match x:
114        case W.U64{+l, +h}:
115          N.le_add_right(v(l), C.shift(32n, v(h)))
116
117def nz_word(+n: U32, +hn: {U32.is_zero(n) == False{} : Bool}) -> {X.is_zero(W.U64{n, 0}) == False{} : Bool}:
118  %Equal.sym(Bool, U32.is_zero(n), False{}, hn) : {Bool.and(_, U32.is_zero(0)) == False{} : Bool}
119  {==}
120
121def uint32n_lt(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: U32, +hn: {U32.is_zero(n) == False{} : Bool}) -> SRM.Uint32n.lt(~S, ~next, s, n, hn):
122  h1 = MR.uint64n_lt(~S, ~next, s, W.U64{n, 0}, nz_word(n, hn))
123  +h2 = Equal.trans(Bool, Nat.is_lt(SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, W.U64{n, 0}))), v(n)), Nat.is_lt(SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, W.U64{n, 0}))), Nat.add(v(n), C.shift(32n, 0n))), True{},
124    Equal.cong(Nat, Bool, z => Nat.is_lt(SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, W.U64{n, 0}))), z), v(n), Nat.add(v(n), C.shift(32n, 0n)), Equal.sym(Nat, Nat.add(v(n), 0n), v(n), N.add_zero(v(n)))),
125    h1)
126  N.le_lt_trans(U32.to_nat(R.fst(U32, S, R.lo32(S, R.uint64n(~S, ~next, s, W.U64{n, 0})))), SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, W.U64{n, 0}))), v(n), lo_le(S, R.uint64n(~S, ~next, s, W.U64{n, 0})), h2)
127
128# ---- Nat <-> U64 below 2^64: n48 (from proofs/math/typed/u64bgcd.bend)
129# and rand.bend's nat64, a byte at a time ----
130
131def vv(+x: W.U64) -> Nat:
132  SW.value(x)
133
134def s32(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat) -> {Nat.mul(Nat.mul(x, 65536n), 65536n) == C.shift(32n, x) : Nat}:
135  +k = W64D.k65536(one, h1)
136  +e1 = PD.mul_pow(one, h1, 16n, x, 65536n, k)
137  +e2 = Equal.trans(Nat, Nat.mul(Nat.mul(x, 65536n), 65536n), Nat.mul(WD.sc(16n, x), 65536n), WD.sc(16n, WD.sc(16n, x)), Equal.cong(Nat, Nat, z => Nat.mul(z, 65536n), Nat.mul(x, 65536n), WD.sc(16n, x), e1), PD.mul_pow(one, h1, 16n, WD.sc(16n, x), 65536n, k))
138  Equal.trans(Nat, Nat.mul(Nat.mul(x, 65536n), 65536n), WD.sc(16n, WD.sc(16n, x)), C.shift(32n, x), e2, Equal.trans(Nat, WD.sc(16n, WD.sc(16n, x)), WD.sc(32n, x), C.shift(32n, x), W64M.sc_sc(16n, 16n, x), Equal.sym(Nat, C.shift(32n, x), WD.sc(32n, x), W64M.shift_sc(32n, x))))
139
140def n48v(+one: Nat, +h1: {one == 1n : Nat}, +a: W.U64) -> {X.n48(a) == vv(a) : Nat}:
141  match a:
142    case W.U64{+l, +h}:
143      Equal.cong(Nat, Nat, z => Nat.add(U32.to_nat(l), z), Nat.mul(Nat.mul(U32.to_nat(h), 65536n), 65536n), C.shift(32n, U32.to_nat(h)), s32(one, h1, U32.to_nat(h)))
144
145
146def fits0(+a: Nat) -> {C.fits(a, 0n) == True{} : Bool}:
147  %Equal.sym(Nat, C.high(a, 0n), 0n, WC.high0(a)) : {Nat.is_eq(_, 0n) == True{} : Bool}
148  {==}
149
150# x < 2^k gives x 2^a < 2^(a + k)
151def fits_shift(+a: Nat, +k: Nat, +x: Nat, +h: {C.fits(k, x) == True{} : Bool}) -> {C.fits(Nat.add(a, k), C.shift(a, x)) == True{} : Bool}:
152  WW.limbs_fit(a, k, 0n, x, fits0(a), h)
153
154def sh8(k: Nat) -> Nat:
155  match k:
156    case 0n:
157      0n
158    case 1n+j:
159      Nat.add(8n, sh8(j))
160
161def div256(+n: Nat) -> {Nat.div(n, 256n) == C.high(8n, n) : Nat}:
162  Equal.sym(Nat, C.high(8n, n), Nat.div(n, 256n), WW.high_div(8n, n, 255n, {==}))
163
164def mod256(+n: Nat) -> {Nat.mod(n, 256n) == C.low(8n, n) : Nat}:
165  +q = C.high(8n, n)
166  +r = C.low(8n, n)
167  +e = Equal.trans(Nat, n, Nat.add(r, C.shift(8n, q)), Nat.add(Nat.mul(q, 256n), r), WW.low_high(8n, n),
168    Equal.trans(Nat, Nat.add(r, C.shift(8n, q)), Nat.add(C.shift(8n, q), r), Nat.add(Nat.mul(q, 256n), r), N.add_comm(r, C.shift(8n, q)),
169      Equal.cong(Nat, Nat, z => Nat.add(z, r), C.shift(8n, q), Nat.mul(q, 256n), WW.shift_mul(8n, q))))
170  Equal.trans(Nat, Nat.mod(n, 256n), Nat.mod(Nat.add(Nat.mul(q, 256n), r), 256n), r,
171    Equal.cong(Nat, Nat, z => Nat.mod(z, 256n), n, Nat.add(Nat.mul(q, 256n), r), e),
172    AR.mod_of(q, 255n, r, WW.lt_of_fits(8n, r, WW.low_fits(8n, n))))
173
174def byte_v(+n: Nat) -> {v(U32.from_nat(Nat.mod(n, 256n))) == C.low(8n, n) : Nat}:
175  %Equal.sym(Nat, Nat.mod(n, 256n), C.low(8n, n), mod256(n)) : {v(U32.from_nat(_)) == C.low(8n, n) : Nat}
176  U.to_nat_from_nat(C.low(8n, n), 8n, {==}, WW.lt_of_fits(8n, C.low(8n, n), WW.low_fits(8n, n)))
177
178# the words of w_go are the low 8k bits, for 8k <= 32
179def wgo(+k: Nat, +n: Nat, +hk: {Nat.is_le(sh8(k), 32n) == True{} : Bool}) -> {v(R.w_go(k, n)) == C.low(sh8(k), n) : Nat}:
180  match k:
181    case 0n:
182      {==}
183    case 1n+j:
184      +d = C.high(8n, n)
185      +hj = N.le_trans(sh8(j), Nat.add(8n, sh8(j)), 32n, LE.le_plus(8n, sh8(j)), hk)
186      +hj24 = Equal.trans(Bool, Nat.is_le(sh8(j), 24n), Nat.is_le(Nat.add(8n, sh8(j)), 32n), True{}, Equal.sym(Bool, Nat.is_le(Nat.add(8n, sh8(j)), 32n), Nat.is_le(sh8(j), 24n), AR.le_add_cancel(8n, sh8(j), 24n)), hk)
187      +ih = Equal.trans(Nat, v(R.w_go(j, Nat.div(n, 256n))), C.low(sh8(j), Nat.div(n, 256n)), C.low(sh8(j), d), wgo(j, Nat.div(n, 256n), hj), Equal.cong(Nat, Nat, z => C.low(sh8(j), z), Nat.div(n, 256n), d, div256(n)))
188      +lw = C.low(sh8(j), d)
189      +f24 = SH.fits_mono(sh8(j), 24n, lw, hj24, WW.low_fits(sh8(j), d))
190      +f32s = fits_shift(8n, 24n, lw, f24)
191      +em = Equal.trans(Nat, v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n))), C.low(32n, C.shift(8n, v(R.w_go(j, Nat.div(n, 256n))))), C.shift(8n, lw),
192        SH.mul_p2(R.w_go(j, Nat.div(n, 256n)), 8n, {==}),
193        Equal.trans(Nat, C.low(32n, C.shift(8n, v(R.w_go(j, Nat.div(n, 256n))))), C.low(32n, C.shift(8n, lw)), C.shift(8n, lw), Equal.cong(Nat, Nat, z => C.low(32n, C.shift(8n, z)), v(R.w_go(j, Nat.div(n, 256n))), lw, ih), WW.low_fit(32n, C.shift(8n, lw), f32s)))
194      +sum = Nat.add(C.low(8n, n), C.shift(8n, lw))
195      +es = Equal.sym(Nat, C.low(Nat.add(8n, sh8(j)), n), sum, FB.low_split(8n, sh8(j), n))
196      +fsum = SH.fits_mono(Nat.add(8n, sh8(j)), 32n, sum, hk, Equal.trans(Bool, C.fits(Nat.add(8n, sh8(j)), sum), C.fits(Nat.add(8n, sh8(j)), C.low(Nat.add(8n, sh8(j)), n)), True{}, Equal.cong(Nat, Bool, z => C.fits(Nat.add(8n, sh8(j)), z), sum, C.low(Nat.add(8n, sh8(j)), n), es), WW.low_fits(Nat.add(8n, sh8(j)), n)))
197      +bv = byte_v(n)
198      +vsum = Equal.trans(Nat, Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), Nat.add(C.low(8n, n), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), sum,
199        Equal.cong(Nat, Nat, z => Nat.add(z, v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), v(U32.from_nat(Nat.mod(n, 256n))), C.low(8n, n), bv),
200        Equal.cong(Nat, Nat, z => Nat.add(C.low(8n, n), z), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n))), C.shift(8n, lw), em))
201      +hf = Equal.trans(Bool, C.fits(32n, Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n))))), C.fits(32n, sum), True{}, Equal.cong(Nat, Bool, z => C.fits(32n, z), Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), sum, vsum), fsum)
202      Equal.trans(Nat, v(U32.add(U32.from_nat(Nat.mod(n, 256n)), U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), C.low(Nat.add(8n, sh8(j)), n),
203        WA.add_exact(1n, {==}, U32.from_nat(Nat.mod(n, 256n)), U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)), hf),
204        Equal.trans(Nat, Nat.add(v(U32.from_nat(Nat.mod(n, 256n))), v(U32.mul(R.w_go(j, Nat.div(n, 256n)), X.pow2(8n)))), sum, C.low(Nat.add(8n, sh8(j)), n), vsum, es))
205
206# skip(k, n) = n div 2^(8k)
207def skip_v(+k: Nat, +n: Nat) -> {R.skip(k, n) == C.high(sh8(k), n) : Nat}:
208  match k:
209    case 0n:
210      {==}
211    case 1n+j:
212      Equal.trans(Nat, R.skip(j, Nat.div(n, 256n)), C.high(sh8(j), Nat.div(n, 256n)), C.high(Nat.add(8n, sh8(j)), n),
213        skip_v(j, Nat.div(n, 256n)),
214        Equal.trans(Nat, C.high(sh8(j), Nat.div(n, 256n)), C.high(sh8(j), C.high(8n, n)), C.high(Nat.add(8n, sh8(j)), n),
215          Equal.cong(Nat, Nat, z => C.high(sh8(j), z), Nat.div(n, 256n), C.high(8n, n), div256(n)),
216          Equal.sym(Nat, C.high(Nat.add(8n, sh8(j)), n), C.high(sh8(j), C.high(8n, n)), WW.high_comp(sh8(j), 8n, n))))
217
218# THEOREM: nat64(n) denotes n, for n < 2^64
219def nat64_v(+n: Nat, +hn: {C.fits(64n, n) == True{} : Bool}) -> {vv(R.nat64(n)) == n : Nat}:
220  +l = C.low(32n, n)
221  +h = C.low(32n, C.high(32n, n))
222  +e1 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(32n, v(R.w_go(4n, R.skip(4n, n))))), v(R.w_go(4n, n)), l, wgo(4n, n, {==}))
223  +e2 = Equal.cong(Nat, Nat, z => Nat.add(l, C.shift(32n, z)), v(R.w_go(4n, R.skip(4n, n))), h, Equal.trans(Nat, v(R.w_go(4n, R.skip(4n, n))), C.low(32n, R.skip(4n, n)), h, wgo(4n, R.skip(4n, n), {==}), Equal.cong(Nat, Nat, z => C.low(32n, z), R.skip(4n, n), C.high(32n, n), skip_v(4n, n))))
224  +e3 = Equal.sym(Nat, C.low(64n, n), Nat.add(l, C.shift(32n, h)), FB.low_split(32n, 32n, n))
225  Equal.trans(Nat, Nat.add(v(R.w_go(4n, n)), C.shift(32n, v(R.w_go(4n, R.skip(4n, n))))), Nat.add(l, C.shift(32n, v(R.w_go(4n, R.skip(4n, n))))), n, e1,
226    Equal.trans(Nat, Nat.add(l, C.shift(32n, v(R.w_go(4n, R.skip(4n, n))))), Nat.add(l, C.shift(32n, h)), n, e2,
227      Equal.trans(Nat, Nat.add(l, C.shift(32n, h)), C.low(64n, n), n, e3, WW.low_fit(64n, n, hn))))
228
229# ---- IntN ----
230
231def n48_p(-S: Data, r: W.U64 & S) -> {R.fst(Nat, S, R.to_nat(S, r)) == SW.value(R.fst(W.U64, S, r)) : Nat}:
232  match r:
233    case Tuple{x, s}:
234      n48v(1n, {==}, x)
235
236def intn_pos(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +hw: {C.fits(64n, n) == True{} : Bool}) -> {Nat.is_lt(R.fst(Nat, S, R.intn_z(~S, ~next, s, n, False{})), n) == True{} : Bool}:
237  +w = {R.nat64(n) : W.U64}
238  +ev = nat64_v(n, hw)
239  +hz = Equal.trans(Bool, X.is_zero(w), Nat.is_eq(SW.value(w), 0n), False{}, WA.is_zero_value(w),
240    Equal.trans(Bool, Nat.is_eq(SW.value(w), 0n), Nat.is_eq(n, 0n), False{}, Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), SW.value(w), n, ev), N.is_eq_sym_false(0n, n, N.is_eq_lt(0n, n, hn))))
241  %Equal.sym(Nat, R.fst(Nat, S, R.to_nat(S, R.uint64n(~S, ~next, s, w))), SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, w))), n48_p(S, R.uint64n(~S, ~next, s, w))) : {Nat.is_lt(_, n) == True{} : Bool}
242  %ev : {Nat.is_lt(SW.value(R.fst(W.U64, S, R.uint64n(~S, ~next, s, w))), _) == True{} : Bool}
243  MR.uint64n_lt(~S, ~next, s, w, hz)
244
245def intn_lt(~S: Data, ~next: S -> W.U64 & S, +s: S, +n: Nat, +hn: {Nat.is_lt(0n, n) == True{} : Bool}, +hw: {C.fits(64n, n) == True{} : Bool}) -> SRM.Intn.lt(~S, ~next, s, n, hn, hw):
246  %Equal.sym(Bool, Nat.is_eq(n, 0n), False{}, N.is_eq_sym_false(0n, n, N.is_eq_lt(0n, n, hn))) : {Nat.is_lt(R.fst(Nat, S, R.intn_z(~S, ~next, s, n, _)), n) == True{} : Bool}
247  intn_pos(~S, ~next, s, n, hn, hw)
248
249# ---- int_range ----
250
251def plus_fst(-S: Data, +lo: Nat, r: Nat & S) -> {R.fst(Nat, S, R.plus(S, lo, r)) == Nat.add(lo, R.fst(Nat, S, r)) : Nat}:
252  match r:
253    case Tuple{k, s}:
254      {==}
255
256def lt_pos(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(0n, Nat.sub(b, a)) == True{} : Bool}:
257  match a b:
258    case _ 0n:
259      Empty.absurd({Nat.is_lt(0n, Nat.sub(0n, a)) == True{} : Bool}, N.lt_zero_absurd(a, h))
260    case 0n 1n+q:
261      {==}
262    case 1n+p 1n+q:
263      lt_pos(p, q, h)
264
265def int_range_bounds(~S: Data, ~next: S -> W.U64 & S, +s: S, +lo: Nat, +hi: Nat, +h: {Nat.is_lt(lo, hi) == True{} : Bool}, +hw: {C.fits(64n, Nat.sub(hi, lo)) == True{} : Bool}) -> SRM.IntRange.bounds(~S, ~next, s, lo, hi, h, hw):
266  +d = Nat.sub(hi, lo)
267  +k = R.fst(Nat, S, R.intn(~S, ~next, s, d))
268  hk = intn_lt(~S, ~next, s, d, lt_pos(lo, hi, h), hw)
269  +up = Equal.trans(Bool, Nat.is_lt(Nat.add(lo, k), hi), Nat.is_lt(Nat.add(lo, k), Nat.add(lo, d)), True{},
270    Equal.cong(Nat, Bool, z => Nat.is_lt(Nat.add(lo, k), z), hi, Nat.add(lo, d), Equal.sym(Nat, Nat.add(lo, d), hi, N.sub_add(hi, lo, N.lt_le(lo, hi, h)))),
271    N.lt_add_left(k, d, lo, hk))
272  %Equal.sym(Nat, R.fst(Nat, S, R.plus(S, lo, R.intn(~S, ~next, s, d))), Nat.add(lo, k), plus_fst(S, lo, R.intn(~S, ~next, s, d))) : {Bool.and(Nat.is_le(lo, _), Nat.is_lt(_, hi)) == True{} : Bool}
273  L.and_intro(Nat.is_le(lo, Nat.add(lo, k)), Nat.is_lt(Nat.add(lo, k), hi), N.le_add_right(lo, k), up)