~/jendhub

proofs/math/typed/f64divn.bend

bend-collections-laws-math@1.0.0.0 · 192 lines · 22 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
3import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
6import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
7import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as NR
8import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
9import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
10import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rtools.bend as RT
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF
12
13# The quotient and sticky bit of a division, at two scales: the spec's
14# 2 * floor(MX * 2^200 / MY) + [remainder != 0] cut at bit d is floor(MX *
15# 2^P / MY) with the same sticky bit (P + d = 201), and SoftFloat's two
16# 32-bit digits of (a - b) * 2^64 / b give floor(a * 2^62 / b) and its
17# sticky bit.
18
19def add_eq0(+a: Nat, +b: Nat) -> {Nat.is_eq(Nat.add(a, b), 0n) == Bool.and(Nat.is_eq(a, 0n), Nat.is_eq(b, 0n)) : Bool}:
20  FL.add_eq0(a, b)
21
22def mul_eq0(+a: Nat, +yp: Nat) -> {Nat.is_eq(Nat.mul(a, 1n+yp), 0n) == Nat.is_eq(a, 0n) : Bool}:
23  match a:
24    case 0n:
25      {==}
26    case 1n+ +ap:
27      {==}
28
29def min1_eq0(+b: Nat) -> {Nat.is_eq(Nat.min(b, 1n), 0n) == Nat.is_eq(b, 0n) : Bool}:
30  match b:
31    case 0n:
32      {==}
33    case 1n+ +bq:
34      {==}
35
36def min1_le(+b: Nat) -> {Nat.is_le(Nat.min(b, 1n), 1n) == True{} : Bool}:
37  match b:
38    case 0n:
39      {==}
40    case 1n+ +bq:
41      match bq:
42        case 0n:
43          {==}
44        case 1n+ +bz:
45          {==}
46
47def and_comm(+a: Bool, +b: Bool) -> {Bool.and(a, b) == Bool.and(b, a) : Bool}:
48  match a b:
49    case True{} True{}:
50      {==}
51    case True{} False{}:
52      {==}
53    case False{} True{}:
54      {==}
55    case False{} False{}:
56      {==}
57
58def mul1(+y: Nat) -> {Nat.mul(1n, y) == y : Nat}:
59  Equal.trans(Nat, Nat.mul(1n, y), Nat.mul(y, 1n), y, NA.mul_comm(1n, y), NA.mul_one(y))
60
61# 2^k * y as a product
62def sh_y(+k: Nat, +y: Nat) -> {Nat.mul(C.shift(k, 1n), y) == C.shift(k, y) : Nat}:
63  Equal.trans(Nat, Nat.mul(C.shift(k, 1n), y), C.shift(k, Nat.mul(1n, y)), C.shift(k, y), WW.shift_mul_l(k, 1n, y), Equal.cong(Nat, Nat, z => C.shift(k, z), Nat.mul(1n, y), y, mul1(y)))
64
65# le/lt under a common shift
66def le_sh(+k: Nat, +a: Nat, +b: Nat) -> {Nat.is_le(C.shift(k, a), C.shift(k, b)) == Nat.is_le(a, b) : Bool}:
67  Equal.cong(Cmp, Bool, c => Cmp.is_le(c), Nat.cmp(C.shift(k, a), C.shift(k, b)), Nat.cmp(a, b), NC.cmp_shift(k, a, b))
68
69def lt_sh(+k: Nat, +a: Nat, +b: Nat) -> {Nat.is_lt(C.shift(k, a), C.shift(k, b)) == Nat.is_lt(a, b) : Bool}:
70  Equal.cong(Cmp, Bool, c => Cmp.is_lt(c), Nat.cmp(C.shift(k, a), C.shift(k, b)), Nat.cmp(a, b), NC.cmp_shift(k, a, b))
71
72# the spec's significand cut at bit 1+dp, where P + dp = 200
73def specA(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat, +hP: {Nat.add(dp, P) == 200n : Nat}) -> {Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))) == Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)) : Nat}:
74  +e0 = NR.dm_eq(yp, C.shift(P, MX))
75  +e1 = Equal.trans(Nat, C.shift(200n, MX), C.shift(Nat.add(dp, P), MX), C.shift(dp, C.shift(P, MX)), Equal.cong(Nat, Nat, z => C.shift(z, MX), 200n, Nat.add(dp, P), Equal.sym(Nat, Nat.add(dp, P), 200n, hP)), WW.shift_comp(dp, P, MX))
76  +e2 = Equal.cong(Nat, Nat, z => C.shift(dp, z), C.shift(P, MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp)), e0)
77  +e3 = WW.shift_add(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))
78  +e4 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Equal.sym(Nat, Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), WW.shift_mul_l(dp, Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)))
79  +e5 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), z), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), NR.dm_eq(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))))
80  +e6 = Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.add_assoc(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
81  +e7 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Equal.sym(Nat, Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), NA.mul_add_right(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)))
82  +eN = Equal.trans(Nat, C.shift(200n, MX), C.shift(dp, C.shift(P, MX)), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e1, Equal.trans(Nat, C.shift(dp, C.shift(P, MX)), C.shift(dp, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e2, Equal.trans(Nat, C.shift(dp, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e3, Equal.trans(Nat, Nat.add(C.shift(dp, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e4, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e5, Equal.trans(Nat, Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(Nat.add(Nat.mul(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), 1n+yp), Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp)), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), e6, e7))))))
83  +hb = NR.dm_lt(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)))
84  +eD = Equal.trans(Nat, Nat.div(C.shift(200n, MX), 1n+yp), Nat.div(Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Equal.cong(Nat, Nat, z => Nat.div(z, 1n+yp), C.shift(200n, MX), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eN), NR.div_of(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), yp, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), hb))
85  +eR = Equal.trans(Nat, Nat.mod(C.shift(200n, MX), 1n+yp), Nat.mod(Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+yp), C.shift(200n, MX), Nat.add(Nat.mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eN), NR.mod_of(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), yp, Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), hb))
86  +m1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, z), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.div(C.shift(200n, MX), 1n+yp), Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), eD)
87  +m2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(z, 1n)), Nat.mod(C.shift(200n, MX), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), eR)
88  +m3 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Equal.sym(Nat, Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.double_mul(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))))
89  +m4 = Equal.cong(Nat, Nat, z => Nat.add(z, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.double_add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
90  +m5 = NA.add_assoc(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))
91  +m6 = NA.add_comm(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)))
92  +m7 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), NA.add_comm(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)))
93  +ch = Equal.trans(Nat, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m1, Equal.trans(Nat, Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m2, Equal.trans(Nat, Nat.add(Nat.mul(2n, Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m3, Equal.trans(Nat, Nat.add(Nat.double(Nat.add(C.shift(dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m4, Equal.trans(Nat, Nat.add(Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m5, Equal.trans(Nat, Nat.add(C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp)), Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n))), Nat.add(Nat.add(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n)), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), m6, m7))))))
94  Equal.sym(Nat, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, MX), 1n+yp)), Nat.min(Nat.mod(C.shift(200n, MX), 1n+yp), 1n)), Nat.add(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), C.shift(1n+dp, Nat.div(C.shift(P, MX), 1n+yp))), ch)
95
96# the low part fits 1+dp bits
97def specA_fit(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat) -> {C.fits(1n+dp, Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))) == True{} : Bool}:
98  +l1 = Equal.trans(Bool, Nat.is_le(C.shift(dp, 1n), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), Nat.is_le(Nat.mul(C.shift(dp, 1n), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), False{}, NR.le_div(yp, C.shift(dp, 1n), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Equal.trans(Bool, Nat.is_le(Nat.mul(C.shift(dp, 1n), 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.is_le(C.shift(dp, 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), False{}, Equal.cong(Nat, Bool, z => Nat.is_le(z, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.mul(C.shift(dp, 1n), 1n+yp), C.shift(dp, 1n+yp), sh_y(dp, 1n+yp)), Equal.trans(Bool, Nat.is_le(C.shift(dp, 1n+yp), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.is_le(1n+yp, Nat.mod(C.shift(P, MX), 1n+yp)), False{}, le_sh(dp, 1n+yp, Nat.mod(C.shift(P, MX), 1n+yp)), N.lt_not_le(Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp, NR.dm_lt(yp, C.shift(P, MX))))))
99  +l2 = N.not_le_lt(C.shift(dp, 1n), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), l1)
100  +fa = WW.fits_one(dp, 1n, {==}, Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), l2)
101  Equal.trans(Bool, C.fits(1n+dp, Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))), C.fits(dp, Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), True{}, RT.fit_td(dp, Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), min1_le(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), fa)
102
103# the low part is zero exactly when MX * 2^P is a multiple of MY
104def specA_z(+MX: Nat, +yp: Nat, +P: Nat, +dp: Nat) -> {Nat.is_eq(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), 0n) == Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n) : Bool}:
105  +z1 = add_eq0(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
106  +z2 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), min1_eq0(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
107  +z3 = Equal.cong(Bool, Bool, t => Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), t), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), WW.dbl_eq0(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
108  +z4 = and_comm(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n))
109  +z5 = Equal.sym(Bool, Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), mul_eq0(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), yp))
110  +z6 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), z5)
111  +z7 = Equal.sym(Bool, Nat.is_eq(Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), add_eq0(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)))
112  +z8 = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.sym(Nat, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), NR.dm_eq(yp, C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)))))
113  +z9 = WW.shift_eq0(dp, Nat.mod(C.shift(P, MX), 1n+yp))
114  Equal.trans(Bool, Nat.is_eq(Nat.add(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp))), 0n), Bool.and(Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z1, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.min(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z2, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.double(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n)), Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z3, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Bool.and(Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z4, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z6, Equal.trans(Bool, Bool.and(Nat.is_eq(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), 0n), Nat.is_eq(Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 0n)), Nat.is_eq(Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z7, Equal.trans(Bool, Nat.is_eq(Nat.add(Nat.mul(Nat.div(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp), 1n+yp), Nat.mod(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+yp)), 0n), Nat.is_eq(C.shift(dp, Nat.mod(C.shift(P, MX), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), z8, z9)))))))
115
116
117# SoftFloat's quotient: (a - b) * 2^64 = Q * b + r2 with r2 < b gives
118# a * 2^62 = T * b + e with T = 2^62 + floor(Q / 4) and e < b
119def iq_parts(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)) == C.shift(2n, C.shift(62n, R)) : Nat}:
120  +q1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(z, B), r2), Q, Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), WW.low_high(2n, Q))
121  +q2 = Equal.cong(Nat, Nat, z => Nat.add(z, r2), Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), NA.mul_add_right(C.low(2n, Q), C.shift(2n, C.high(2n, Q)), B))
122  +q3 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), z), r2), Nat.mul(C.shift(2n, C.high(2n, Q)), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), WW.shift_mul_l(2n, C.high(2n, Q), B))
123  +q4 = NA.add_assoc(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)
124  +q5 = NA.add_swap(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)
125  +q7 = Equal.trans(Nat, C.shift(64n, R), C.shift(Nat.add(2n, 62n), R), C.shift(2n, C.shift(62n, R)), {==}, WW.shift_comp(2n, 62n, R))
126  +x1 = Equal.trans(Nat, Nat.add(Nat.mul(Q, B), r2), Nat.add(Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q1, Equal.trans(Nat, Nat.add(Nat.mul(Nat.add(C.low(2n, Q), C.shift(2n, C.high(2n, Q))), B), r2), Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q2, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), Nat.mul(C.shift(2n, C.high(2n, Q)), B)), r2), Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B))), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q3, Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(C.low(2n, Q), B), C.shift(2n, Nat.mul(C.high(2n, Q), B))), r2), Nat.add(Nat.mul(C.low(2n, Q), B), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), r2)), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), q4, q5))))
127  Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), Nat.add(Nat.mul(Q, B), r2), C.shift(2n, C.shift(62n, R)), Equal.sym(Nat, Nat.add(Nat.mul(Q, B), r2), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), x1), Equal.trans(Nat, Nat.add(Nat.mul(Q, B), r2), C.shift(64n, R), C.shift(2n, C.shift(62n, R)), hQ, q7))
128
129# h * b <= (a - b) * 2^62
130def iq_le(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)) == True{} : Bool}:
131  +p = iq_parts(B, R, Q, r2, hQ)
132  +l = L.subst(Nat, z => {Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), z) == True{} : Bool}, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), C.shift(2n, C.shift(62n, R)), p, N.le_add_right(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)))
133  Equal.trans(Bool, Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)), Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, C.shift(62n, R))), True{}, Equal.sym(Bool, Nat.is_le(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, C.shift(62n, R))), Nat.is_le(Nat.mul(C.high(2n, Q), B), C.shift(62n, R)), le_sh(2n, Nat.mul(C.high(2n, Q), B), C.shift(62n, R))), l)
134
135# the remainder e = (a - b) * 2^62 - h * b, and 4 e = low2(Q) * b + r2
136def iq_eps(+B: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, B), r2) == C.shift(64n, R) : Nat}) -> {C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))) == Nat.add(Nat.mul(C.low(2n, Q), B), r2) : Nat}:
137  +p = iq_parts(B, R, Q, r2, hQ)
138  +e1 = N.sub_add(C.shift(62n, R), Nat.mul(C.high(2n, Q), B), iq_le(B, R, Q, r2, hQ))
139  +e2 = Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, C.shift(62n, R)), Equal.sym(Nat, C.shift(2n, Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), WW.shift_add(2n, Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), Equal.cong(Nat, Nat, z => C.shift(2n, z), Nat.add(Nat.mul(C.high(2n, Q), B), Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))), C.shift(62n, R), e1))
140  NR.add_cancel(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B))), Nat.add(Nat.mul(C.low(2n, Q), B), r2), Equal.trans(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), B)))), C.shift(2n, C.shift(62n, R)), Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), e2, Equal.sym(Nat, Nat.add(C.shift(2n, Nat.mul(C.high(2n, Q), B)), Nat.add(Nat.mul(C.low(2n, Q), B), r2)), C.shift(2n, C.shift(62n, R)), p)))
141
142def low2_le(+Q: Nat, +bp: Nat) -> {Nat.is_le(Nat.mul(1n+C.low(2n, Q), 1n+bp), C.shift(2n, 1n+bp)) == True{} : Bool}:
143  +l = N.lt_succ_le_succ(C.low(2n, Q), 4n, WW.low_lt(2n, Q))
144  +m = NF.mul_le_r(1n+bp, 1n+C.low(2n, Q), 4n, l)
145  +e = Equal.trans(Nat, Nat.mul(1n+bp, 4n), Nat.mul(4n, 1n+bp), C.shift(2n, 1n+bp), NA.mul_comm(1n+bp, 4n), sh_y(2n, 1n+bp))
146  L.subst(Nat, z => {Nat.is_le(Nat.mul(1n+C.low(2n, Q), 1n+bp), z) == True{} : Bool}, Nat.mul(1n+bp, 4n), C.shift(2n, 1n+bp), e, L.subst(Nat, z => {Nat.is_le(z, Nat.mul(1n+bp, 4n)) == True{} : Bool}, Nat.mul(1n+bp, 1n+C.low(2n, Q)), Nat.mul(1n+C.low(2n, Q), 1n+bp), NA.mul_comm(1n+bp, 1n+C.low(2n, Q)), m))
147
148# e < b
149def iq_lt(+bp: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, 1n+bp), r2) == C.shift(64n, R) : Nat}, +hr2: {Nat.is_lt(r2, 1n+bp) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp) == True{} : Bool}:
150  +E = Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2)
151  +l1 = Equal.trans(Bool, Nat.is_lt(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp)), Nat.is_lt(r2, 1n+bp), True{}, WW.lt_cancel_l(Nat.mul(C.low(2n, Q), 1n+bp), r2, 1n+bp), hr2)
152  +e1 = Equal.trans(Nat, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Nat.add(1n+bp, Nat.mul(C.low(2n, Q), 1n+bp)), Nat.mul(1n+C.low(2n, Q), 1n+bp), NA.add_comm(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), {==})
153  +l2 = N.lt_le_trans(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), C.shift(2n, 1n+bp), l1, L.subst(Nat, z => {Nat.is_le(z, C.shift(2n, 1n+bp)) == True{} : Bool}, Nat.mul(1n+C.low(2n, Q), 1n+bp), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Equal.sym(Nat, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), 1n+bp), Nat.mul(1n+C.low(2n, Q), 1n+bp), e1), low2_le(Q, bp)))
154  +l3 = L.subst(Nat, z => {Nat.is_lt(z, C.shift(2n, 1n+bp)) == True{} : Bool}, Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Equal.sym(Nat, C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), iq_eps(1n+bp, R, Q, r2, hQ)), l2)
155  Equal.trans(Bool, Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp), Nat.is_lt(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), C.shift(2n, 1n+bp)), True{}, Equal.sym(Bool, Nat.is_lt(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), C.shift(2n, 1n+bp)), Nat.is_lt(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp), lt_sh(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 1n+bp)), l3)
156
157# e is zero exactly when the low two quotient bits and r2 are
158def iq_z(+bp: Nat, +R: Nat, +Q: Nat, +r2: Nat, +hQ: {Nat.add(Nat.mul(Q, 1n+bp), r2) == C.shift(64n, R) : Nat}) -> {Nat.is_eq(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 0n) == Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)) : Bool}:
159  +z1 = Equal.sym(Bool, Nat.is_eq(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), 0n), Nat.is_eq(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 0n), WW.shift_eq0(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))))
160  +z2 = Equal.cong(Nat, Bool, t => Nat.is_eq(t, 0n), C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), iq_eps(1n+bp, R, Q, r2, hQ))
161  +z3 = add_eq0(Nat.mul(C.low(2n, Q), 1n+bp), r2)
162  +z4 = Equal.cong(Bool, Bool, t => Bool.and(t, Nat.is_eq(r2, 0n)), Nat.is_eq(Nat.mul(C.low(2n, Q), 1n+bp), 0n), Nat.is_eq(C.low(2n, Q), 0n), mul_eq0(C.low(2n, Q), bp))
163  Equal.trans(Bool, Nat.is_eq(Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp)), 0n), Nat.is_eq(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), 0n), Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)), z1, Equal.trans(Bool, Nat.is_eq(C.shift(2n, Nat.sub(C.shift(62n, R), Nat.mul(C.high(2n, Q), 1n+bp))), 0n), Nat.is_eq(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), 0n), Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)), z2, Equal.trans(Bool, Nat.is_eq(Nat.add(Nat.mul(C.low(2n, Q), 1n+bp), r2), 0n), Bool.and(Nat.is_eq(Nat.mul(C.low(2n, Q), 1n+bp), 0n), Nat.is_eq(r2, 0n)), Bool.and(Nat.is_eq(C.low(2n, Q), 0n), Nat.is_eq(r2, 0n)), z3, z4)))
164
165
166# the two scales agree: a * 2^62 = T * b + e with e < b, a = MX * 2^u and
167# b = MY * 2^w give T = floor(MX * 2^P / MY) and e = 0 iff MY | MX * 2^P
168def jn_eq(+MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}) -> {C.shift(62n, C.shift(u, MX)) == Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))) : Nat}:
169  +j1 = Equal.sym(Nat, C.shift(Nat.add(62n, u), MX), C.shift(62n, C.shift(u, MX)), WW.shift_comp(62n, u, MX))
170  +j2 = Equal.cong(Nat, Nat, z => C.shift(z, MX), Nat.add(62n, u), Nat.add(w, P), hP)
171  +j3 = WW.shift_comp(w, P, MX)
172  +j4 = Equal.cong(Nat, Nat, z => C.shift(w, z), C.shift(P, MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp)), NR.dm_eq(yp, C.shift(P, MX)))
173  +j5 = WW.shift_add(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))
174  +j6 = Equal.cong(Nat, Nat, z => Nat.add(z, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), C.shift(w, 1n+yp)), Equal.sym(Nat, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), C.shift(w, 1n+yp)), C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), WW.shift_mul_r(w, Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)))
175  +j7 = Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), z), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), C.shift(w, 1n+yp), 1n+bp, hB)
176  Equal.trans(Nat, C.shift(62n, C.shift(u, MX)), C.shift(Nat.add(62n, u), MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j1, Equal.trans(Nat, C.shift(Nat.add(62n, u), MX), C.shift(Nat.add(w, P), MX), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j2, Equal.trans(Nat, C.shift(Nat.add(w, P), MX), C.shift(w, C.shift(P, MX)), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j3, Equal.trans(Nat, C.shift(w, C.shift(P, MX)), C.shift(w, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j4, Equal.trans(Nat, C.shift(w, Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp), Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j5, Equal.trans(Nat, Nat.add(C.shift(w, Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+yp)), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), C.shift(w, 1n+yp)), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), j6, j7))))))
177
178def jn_lt(+MX: Nat, +yp: Nat, +w: Nat, +P: Nat, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}) -> {Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), 1n+bp) == True{} : Bool}:
179  L.subst(Nat, z => {Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), z) == True{} : Bool}, C.shift(w, 1n+yp), 1n+bp, hB, Equal.trans(Bool, Nat.is_lt(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), C.shift(w, 1n+yp)), Nat.is_lt(Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp), True{}, lt_sh(w, Nat.mod(C.shift(P, MX), 1n+yp), 1n+yp), NR.dm_lt(yp, C.shift(P, MX))))
180
181def jn_q(+MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}, +T: Nat, +e: Nat, +hE: {Nat.add(Nat.mul(T, 1n+bp), e) == C.shift(62n, C.shift(u, MX)) : Nat}, +he: {Nat.is_lt(e, 1n+bp) == True{} : Bool}) -> {T == Nat.div(C.shift(P, MX), 1n+yp) : Nat}:
182  +eq = Equal.trans(Nat, Nat.add(Nat.mul(T, 1n+bp), e), C.shift(62n, C.shift(u, MX)), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), hE, jn_eq(MX, yp, u, w, P, hP, bp, hB))
183  +dT = NR.div_of(T, bp, e, he)
184  +dQ = NR.div_of(Nat.div(C.shift(P, MX), 1n+yp), bp, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), jn_lt(MX, yp, w, P, bp, hB))
185  Equal.trans(Nat, T, Nat.div(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), Nat.div(C.shift(P, MX), 1n+yp), Equal.sym(Nat, Nat.div(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), T, dT), Equal.trans(Nat, Nat.div(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), Nat.div(Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), 1n+bp), Nat.div(C.shift(P, MX), 1n+yp), Equal.cong(Nat, Nat, z => Nat.div(z, 1n+bp), Nat.add(Nat.mul(T, 1n+bp), e), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), eq), dQ))
186
187def jn_z(+MX: Nat, +yp: Nat, +u: Nat, +w: Nat, +P: Nat, +hP: {Nat.add(62n, u) == Nat.add(w, P) : Nat}, +bp: Nat, +hB: {C.shift(w, 1n+yp) == 1n+bp : Nat}, +T: Nat, +e: Nat, +hE: {Nat.add(Nat.mul(T, 1n+bp), e) == C.shift(62n, C.shift(u, MX)) : Nat}, +he: {Nat.is_lt(e, 1n+bp) == True{} : Bool}) -> {Nat.is_eq(e, 0n) == Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n) : Bool}:
188  +eq = Equal.trans(Nat, Nat.add(Nat.mul(T, 1n+bp), e), C.shift(62n, C.shift(u, MX)), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), hE, jn_eq(MX, yp, u, w, P, hP, bp, hB))
189  +mT = NR.mod_of(T, bp, e, he)
190  +mQ = NR.mod_of(Nat.div(C.shift(P, MX), 1n+yp), bp, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), jn_lt(MX, yp, w, P, bp, hB))
191  +ee = Equal.trans(Nat, e, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), e, mT), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(T, 1n+bp), e), 1n+bp), Nat.mod(Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), Equal.cong(Nat, Nat, z => Nat.mod(z, 1n+bp), Nat.add(Nat.mul(T, 1n+bp), e), Nat.add(Nat.mul(Nat.div(C.shift(P, MX), 1n+yp), 1n+bp), C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp))), eq), mQ))
192  Equal.trans(Bool, Nat.is_eq(e, 0n), Nat.is_eq(C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), 0n), Nat.is_eq(Nat.mod(C.shift(P, MX), 1n+yp), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), e, C.shift(w, Nat.mod(C.shift(P, MX), 1n+yp)), ee), WW.shift_eq0(w, Nat.mod(C.shift(P, MX), 1n+yp)))