1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/math/w64.bend as SW 4 import ../../../spec/math/random/source.bend as SRC 5 import ../../../spec/math/random.bend as SRM 6 import ../../../src/math/u64.bend as W 7 import ../../../src/math/w64.bend as X 8 import ../../../src/math/random/rand.bend as R 9 import ../../lib/nat.bend as N 10 import ../../lib/logic.bend as L 11 import ../../lib/u32.bend as U 12 import ../../lib/lemmas/spec/numeric.bend as S 13 import ../typed/width.bend as WW 14 import ../typed/u32laws.bend as LW 15 import ../typed/w64add.bend as WA 16 import ../typed/f64bits.bend as FB 17 import ../typed/w64clz.bend as WC 18 import ../typed/w64sh.bend as SH 19 import ../typed/w64div.bend as W64D 20 import ../u64/u64div.bend as PD 21 import ../typed/w64mul.bend as W64M 22 import ../../lib/word.bend as WD 23 import ../../lib/arith.bend as LA 24 import ../natural/arith.bend as AR 25 import ./bounded.bend as MR 26 import ./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 33 def v(+x: U32) -> Nat: 34 U32.to_nat(x) 35 36 def val(+l: U32, +h: U32) -> Nat: 37 Nat.add(v(l), C.shift(32n, v(h))) 38 39 # ---- Uint32: the top 32 bits ---- 40 41 def 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 48 def 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 53 def 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 64 def 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 71 def 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 76 def 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 84 def 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 93 def 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 105 def 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 110 def 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 117 def 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 121 def 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 131 def vv(+x: W.U64) -> Nat: 132 SW.value(x) 133 134 def 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 140 def 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 146 def 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) 151 def 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 154 def sh8(k: Nat) -> Nat: 155 match k: 156 case 0n: 157 0n 158 case 1n+j: 159 Nat.add(8n, sh8(j)) 160 161 def 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 164 def 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 174 def 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 179 def 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) 207 def 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 219 def 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 231 def 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 236 def 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 245 def 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 251 def 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 256 def 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 265 def 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)