Rietveld Code Review Tool
Help | Bug tracker | Discussion group | Source code | Sign in
(124402)

Side by Side Diff: Modules/_decimal/libmpdec/literature/umodarith.lisp

Issue 7652: Merge C version of decimal into py3k.
Patch Set: Created 7 years, 8 months ago
Left:
Right:
Use n/p to move between diff chunks; N/P to move between comments. Please Sign in to add in-line comments.
Jump to:
View unified diff | Download patch
« no previous file with comments | « Modules/_decimal/libmpdec/literature/six-step.txt ('k') | Modules/_decimal/libmpdec/memory.c » ('j') | no next file with comments »
Toggle Intra-line Diffs ('i') | Expand Comments ('e') | Collapse Comments ('c') | Show Comments Hide Comments ('s')
OLDNEW
(Empty)
1 ;
2 ; Copyright (c) 2008-2010 Stefan Krah. All rights reserved.
3 ;
4 ; Redistribution and use in source and binary forms, with or without
5 ; modification, are permitted provided that the following conditions
6 ; are met:
7 ;
8 ; 1. Redistributions of source code must retain the above copyright
9 ; notice, this list of conditions and the following disclaimer.
10 ;
11 ; 2. Redistributions in binary form must reproduce the above copyright
12 ; notice, this list of conditions and the following disclaimer in the
13 ; documentation and/or other materials provided with the distribution.
14 ;
15 ; THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS "AS IS" AND
16 ; ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
17 ; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
18 ; ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE
19 ; FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
20 ; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
21 ; OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
22 ; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
23 ; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY
24 ; OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF
25 ; SUCH DAMAGE.
26 ;
27
28
29 (in-package "ACL2")
30
31 (include-book "arithmetic/top-with-meta" :dir :system)
32 (include-book "arithmetic-2/floor-mod/floor-mod" :dir :system)
33
34
35 ;; =====================================================================
36 ;; Proofs for several functions in umodarith.h
37 ;; =====================================================================
38
39
40
41 ;; =====================================================================
42 ;; Helper theorems
43 ;; =====================================================================
44
45 (defthm elim-mod-m<x<2*m
46 (implies (and (<= m x)
47 (< x (* 2 m))
48 (rationalp x) (rationalp m))
49 (equal (mod x m)
50 (+ x (- m)))))
51
52 (defthm modaux-1a
53 (implies (and (< x m) (< 0 x) (< 0 m)
54 (rationalp x) (rationalp m))
55 (equal (mod (- x) m)
56 (+ (- x) m))))
57
58 (defthm modaux-1b
59 (implies (and (< (- x) m) (< x 0) (< 0 m)
60 (rationalp x) (rationalp m))
61 (equal (mod x m)
62 (+ x m)))
63 :hints (("Goal" :use ((:instance modaux-1a
64 (x (- x)))))))
65
66 (defthm modaux-1c
67 (implies (and (< x m) (< 0 x) (< 0 m)
68 (rationalp x) (rationalp m))
69 (equal (mod x m)
70 x)))
71
72 (defthm modaux-2a
73 (implies (and (< 0 b) (< b m)
74 (natp x) (natp b) (natp m)
75 (< (mod (+ b x) m) b))
76 (equal (mod (+ (- m) b x) m)
77 (+ (- m) b (mod x m)))))
78
79 (defthm modaux-2b
80 (implies (and (< 0 b) (< b m)
81 (natp x) (natp b) (natp m)
82 (< (mod (+ b x) m) b))
83 (equal (mod (+ b x) m)
84 (+ (- m) b (mod x m))))
85 :hints (("Goal" :use (modaux-2a))))
86
87 (defthm linear-mod-1
88 (implies (and (< x m) (< b m)
89 (natp x) (natp b)
90 (rationalp m))
91 (equal (< x (mod (+ (- b) x) m))
92 (< x b)))
93 :hints (("Goal" :use ((:instance modaux-1a
94 (x (+ b (- x))))))))
95
96 (defthm linear-mod-2
97 (implies (and (< 0 b) (< b m)
98 (natp x) (natp b)
99 (natp m))
100 (equal (< (mod x m)
101 (mod (+ (- b) x) m))
102 (< (mod x m) b))))
103
104 (defthm linear-mod-3
105 (implies (and (< x m) (< b m)
106 (natp x) (natp b)
107 (rationalp m))
108 (equal (<= b (mod (+ b x) m))
109 (< (+ b x) m)))
110 :hints (("Goal" :use ((:instance elim-mod-m<x<2*m
111 (x (+ b x)))))))
112
113 (defthm modaux-2c
114 (implies (and (< 0 b) (< b m)
115 (natp x) (natp b) (natp m)
116 (<= b (mod (+ b x) m)))
117 (equal (mod (+ b x) m)
118 (+ b (mod x m))))
119 :hints (("Subgoal *1/8''" :use (linear-mod-3))))
120
121 (defthmd modaux-2d
122 (implies (and (< x m) (< 0 x) (< 0 m)
123 (< (- m) b) (< b 0) (rationalp m)
124 (<= x (mod (+ b x) m))
125 (rationalp x) (rationalp b))
126 (equal (+ (- m) (mod (+ b x) m))
127 (+ b x)))
128 :hints (("Goal" :cases ((<= 0 (+ b x))))
129 ("Subgoal 2'" :use ((:instance modaux-1b
130 (x (+ b x)))))))
131
132 (defthm mod-m-b
133 (implies (and (< 0 x) (< 0 b) (< 0 m)
134 (< x b) (< b m)
135 (natp x) (natp b) (natp m))
136 (equal (mod (+ (mod (- x) m) b) m)
137 (mod (- x) b))))
138
139
140 ;; =====================================================================
141 ;; addmod, submod
142 ;; =====================================================================
143
144 (defun addmod (a b m base)
145 (let* ((s (mod (+ a b) base))
146 (s (if (< s a) (mod (- s m) base) s))
147 (s (if (>= s m) (mod (- s m) base) s)))
148 s))
149
150 (defthmd addmod-correct
151 (implies (and (< 0 m) (< m base)
152 (< a m) (<= b m)
153 (natp m) (natp base)
154 (natp a) (natp b))
155 (equal (addmod a b m base)
156 (mod (+ a b) m)))
157 :hints (("Goal" :cases ((<= base (+ a b))))
158 ("Subgoal 2.1'" :use ((:instance elim-mod-m<x<2*m
159 (x (+ a b)))))))
160
161 (defun submod (a b m base)
162 (let* ((d (mod (- a b) base))
163 (d (if (< a d) (mod (+ d m) base) d)))
164 d))
165
166 (defthmd submod-aux1
167 (implies (and (< a (mod (+ a (- b)) base))
168 (< 0 base) (< a base) (<= b base)
169 (natp base) (natp a) (natp b))
170 (< a b))
171 :rule-classes :forward-chaining)
172
173 (defthmd submod-aux2
174 (implies (and (<= (mod (+ a (- b)) base) a)
175 (< 0 base) (< a base) (< b base)
176 (natp base) (natp a) (natp b))
177 (<= b a))
178 :rule-classes :forward-chaining)
179
180 (defthmd submod-correct
181 (implies (and (< 0 m) (< m base)
182 (< a m) (<= b m)
183 (natp m) (natp base)
184 (natp a) (natp b))
185 (equal (submod a b m base)
186 (mod (- a b) m)))
187 :hints (("Goal" :cases ((<= base (+ a b))))
188 ("Subgoal 2.2" :use ((:instance submod-aux1)))
189 ("Subgoal 2.2'''" :cases ((and (< 0 (+ a (- b) m))
190 (< (+ a (- b) m) m))))
191 ("Subgoal 2.1" :use ((:instance submod-aux2)))
192 ("Subgoal 1.2" :use ((:instance submod-aux1)))
193 ("Subgoal 1.1" :use ((:instance submod-aux2)))))
194
195
196 (defun submod-2 (a b m base)
197 (let* ((d (mod (- a b) base))
198 (d (if (< a b) (mod (+ d m) base) d)))
199 d))
200
201 (defthm submod-2-correct
202 (implies (and (< 0 m) (< m base)
203 (< a m) (<= b m)
204 (natp m) (natp base)
205 (natp a) (natp b))
206 (equal (submod-2 a b m base)
207 (mod (- a b) m)))
208 :hints (("Subgoal 2'" :cases ((and (< 0 (+ a (- b) m))
209 (< (+ a (- b) m) m))))))
210
211
212 ;; =========================================================================
213 ;; ext-submod is correct
214 ;; =========================================================================
215
216 ; a < 2*m, b < 2*m
217 (defun ext-submod (a b m base)
218 (let* ((a (if (>= a m) (- a m) a))
219 (b (if (>= b m) (- b m) b))
220 (d (mod (- a b) base))
221 (d (if (< a b) (mod (+ d m) base) d)))
222 d))
223
224 ; a < 2*m, b < 2*m
225 (defun ext-submod-2 (a b m base)
226 (let* ((a (mod a m))
227 (b (mod b m))
228 (d (mod (- a b) base))
229 (d (if (< a b) (mod (+ d m) base) d)))
230 d))
231
232 (defthmd ext-submod-ext-submod-2-equal
233 (implies (and (< 0 m) (< m base)
234 (< a (* 2 m)) (< b (* 2 m))
235 (natp m) (natp base)
236 (natp a) (natp b))
237 (equal (ext-submod a b m base)
238 (ext-submod-2 a b m base))))
239
240 (defthmd ext-submod-2-correct
241 (implies (and (< 0 m) (< m base)
242 (< a (* 2 m)) (< b (* 2 m))
243 (natp m) (natp base)
244 (natp a) (natp b))
245 (equal (ext-submod-2 a b m base)
246 (mod (- a b) m))))
247
248
249 ;; =========================================================================
250 ;; dw-reduce is correct
251 ;; =========================================================================
252
253 (defun dw-reduce (hi lo m base)
254 (let* ((r1 (mod hi m))
255 (r2 (mod (+ (* r1 base) lo) m)))
256 r2))
257
258 (defthmd dw-reduce-correct
259 (implies (and (< 0 m) (< m base)
260 (< hi base) (< lo base)
261 (natp m) (natp base)
262 (natp hi) (natp lo))
263 (equal (dw-reduce hi lo m base)
264 (mod (+ (* hi base) lo) m))))
265
266 (defthmd <=-multiply-both-sides-by-z
267 (implies (and (rationalp x) (rationalp y)
268 (< 0 z) (rationalp z))
269 (equal (<= x y)
270 (<= (* z x) (* z y)))))
271
272 (defthmd dw-reduce-aux1
273 (implies (and (< 0 m) (< m base)
274 (natp m) (natp base)
275 (< lo base) (natp lo)
276 (< x m) (natp x))
277 (< (+ lo (* base x)) (* base m)))
278 :hints (("Goal" :cases ((<= (+ x 1) m)))
279 ("Subgoal 1''" :cases ((<= (* base (+ x 1)) (* base m))))
280 ("subgoal 1.2" :use ((:instance <=-multiply-both-sides-by-z
281 (x (+ 1 x))
282 (y m)
283 (z base))))))
284
285 (defthm dw-reduce-aux2
286 (implies (and (< x (* base m))
287 (< 0 m) (< m base)
288 (natp m) (natp base) (natp x))
289 (< (floor x m) base)))
290
291 ;; This is the necessary condition for using _mpd_div_words().
292 (defthmd dw-reduce-second-quotient-fits-in-single-word
293 (implies (and (< 0 m) (< m base)
294 (< hi base) (< lo base)
295 (natp m) (natp base)
296 (natp hi) (natp lo)
297 (equal r1 (mod hi m)))
298 (< (floor (+ (* r1 base) lo) m)
299 base))
300 :hints (("Goal" :cases ((< r1 m)))
301 ("Subgoal 1''" :cases ((< (+ lo (* base (mod hi m))) (* base m))))
302 ("Subgoal 1.2" :use ((:instance dw-reduce-aux1
303 (x (mod hi m)))))))
304
305
306 ;; =========================================================================
307 ;; dw-submod is correct
308 ;; =========================================================================
309
310 (defun dw-submod (a hi lo m base)
311 (let* ((r (dw-reduce hi lo m base))
312 (d (mod (- a r) base))
313 (d (if (< a r) (mod (+ d m) base) d)))
314 d))
315
316 (defthmd dw-submod-aux1
317 (implies (and (natp a) (< 0 m) (natp m)
318 (natp x) (equal r (mod x m)))
319 (equal (mod (- a x) m)
320 (mod (- a r) m))))
321
322 (defthmd dw-submod-correct
323 (implies (and (< 0 m) (< m base)
324 (natp a) (< a m)
325 (< hi base) (< lo base)
326 (natp m) (natp base)
327 (natp hi) (natp lo))
328 (equal (dw-submod a hi lo m base)
329 (mod (- a (+ (* base hi) lo)) m)))
330 :hints (("Goal" :in-theory (disable dw-reduce)
331 :use ((:instance dw-submod-aux1
332 (x (+ lo (* base hi)))
333 (r (dw-reduce hi lo m base)))
334 (:instance dw-reduce-correct)))))
335
336
337 ;; =========================================================================
338 ;; ANSI C arithmetic for uint64_t
339 ;; =========================================================================
340
341 (defun add (a b)
342 (mod (+ a b)
343 (expt 2 64)))
344
345 (defun sub (a b)
346 (mod (- a b)
347 (expt 2 64)))
348
349 (defun << (w n)
350 (mod (* w (expt 2 n))
351 (expt 2 64)))
352
353 (defun >> (w n)
354 (floor w (expt 2 n)))
355
356 ;; join upper and lower half of a double word, yielding a 128 bit number
357 (defun join (hi lo)
358 (+ (* (expt 2 64) hi) lo))
359
360
361 ;; =============================================================================
362 ;; Fast modular reduction
363 ;; =============================================================================
364
365 ;; These are the three primes used in the Number Theoretic Transform.
366 ;; A fast modular reduction scheme exists for all of them.
367 (defmacro p1 ()
368 (+ (expt 2 64) (- (expt 2 32)) 1))
369
370 (defmacro p2 ()
371 (+ (expt 2 64) (- (expt 2 34)) 1))
372
373 (defmacro p3 ()
374 (+ (expt 2 64) (- (expt 2 40)) 1))
375
376
377 ;; reduce the double word number hi*2**64 + lo (mod p1)
378 (defun simple-mod-reduce-p1 (hi lo)
379 (+ (* (expt 2 32) hi) (- hi) lo))
380
381 ;; reduce the double word number hi*2**64 + lo (mod p2)
382 (defun simple-mod-reduce-p2 (hi lo)
383 (+ (* (expt 2 34) hi) (- hi) lo))
384
385 ;; reduce the double word number hi*2**64 + lo (mod p3)
386 (defun simple-mod-reduce-p3 (hi lo)
387 (+ (* (expt 2 40) hi) (- hi) lo))
388
389
390 ; ----------------------------------------------------------
391 ; The modular reductions given above are correct
392 ; ----------------------------------------------------------
393
394 (defthmd congruence-p1-aux
395 (equal (* (expt 2 64) hi)
396 (+ (* (p1) hi)
397 (* (expt 2 32) hi)
398 (- hi))))
399
400 (defthmd congruence-p2-aux
401 (equal (* (expt 2 64) hi)
402 (+ (* (p2) hi)
403 (* (expt 2 34) hi)
404 (- hi))))
405
406 (defthmd congruence-p3-aux
407 (equal (* (expt 2 64) hi)
408 (+ (* (p3) hi)
409 (* (expt 2 40) hi)
410 (- hi))))
411
412 (defthmd mod-augment
413 (implies (and (rationalp x)
414 (rationalp y)
415 (rationalp m))
416 (equal (mod (+ x y) m)
417 (mod (+ x (mod y m)) m))))
418
419 (defthmd simple-mod-reduce-p1-congruent
420 (implies (and (integerp hi)
421 (integerp lo))
422 (equal (mod (simple-mod-reduce-p1 hi lo) (p1))
423 (mod (join hi lo) (p1))))
424 :hints (("Goal''" :use ((:instance congruence-p1-aux)
425 (:instance mod-augment
426 (m (p1))
427 (x (+ (- hi) lo (* (expt 2 32) hi)))
428 (y (* (p1) hi)))))))
429
430 (defthmd simple-mod-reduce-p2-congruent
431 (implies (and (integerp hi)
432 (integerp lo))
433 (equal (mod (simple-mod-reduce-p2 hi lo) (p2))
434 (mod (join hi lo) (p2))))
435 :hints (("Goal''" :use ((:instance congruence-p2-aux)
436 (:instance mod-augment
437 (m (p2))
438 (x (+ (- hi) lo (* (expt 2 34) hi)))
439 (y (* (p2) hi)))))))
440
441 (defthmd simple-mod-reduce-p3-congruent
442 (implies (and (integerp hi)
443 (integerp lo))
444 (equal (mod (simple-mod-reduce-p3 hi lo) (p3))
445 (mod (join hi lo) (p3))))
446 :hints (("Goal''" :use ((:instance congruence-p3-aux)
447 (:instance mod-augment
448 (m (p3))
449 (x (+ (- hi) lo (* (expt 2 40) hi)))
450 (y (* (p3) hi)))))))
451
452
453 ; ---------------------------------------------------------------------
454 ; We need a number less than 2*p, so that we can use the trick from
455 ; elim-mod-m<x<2*m for the final reduction.
456 ; For p1, two modular reductions are sufficient, for p2 and p3 three.
457 ; ---------------------------------------------------------------------
458
459 ;; p1: the first reduction is less than 2**96
460 (defthmd simple-mod-reduce-p1-<-2**96
461 (implies (and (< hi (expt 2 64))
462 (< lo (expt 2 64))
463 (natp hi) (natp lo))
464 (< (simple-mod-reduce-p1 hi lo)
465 (expt 2 96))))
466
467 ;; p1: the second reduction is less than 2*p1
468 (defthmd simple-mod-reduce-p1-<-2*p1
469 (implies (and (< hi (expt 2 64))
470 (< lo (expt 2 64))
471 (< (join hi lo) (expt 2 96))
472 (natp hi) (natp lo))
473 (< (simple-mod-reduce-p1 hi lo)
474 (* 2 (p1)))))
475
476
477 ;; p2: the first reduction is less than 2**98
478 (defthmd simple-mod-reduce-p2-<-2**98
479 (implies (and (< hi (expt 2 64))
480 (< lo (expt 2 64))
481 (natp hi) (natp lo))
482 (< (simple-mod-reduce-p2 hi lo)
483 (expt 2 98))))
484
485 ;; p2: the second reduction is less than 2**69
486 (defthmd simple-mod-reduce-p2-<-2*69
487 (implies (and (< hi (expt 2 64))
488 (< lo (expt 2 64))
489 (< (join hi lo) (expt 2 98))
490 (natp hi) (natp lo))
491 (< (simple-mod-reduce-p2 hi lo)
492 (expt 2 69))))
493
494 ;; p3: the third reduction is less than 2*p2
495 (defthmd simple-mod-reduce-p2-<-2*p2
496 (implies (and (< hi (expt 2 64))
497 (< lo (expt 2 64))
498 (< (join hi lo) (expt 2 69))
499 (natp hi) (natp lo))
500 (< (simple-mod-reduce-p2 hi lo)
501 (* 2 (p2)))))
502
503
504 ;; p3: the first reduction is less than 2**104
505 (defthmd simple-mod-reduce-p3-<-2**104
506 (implies (and (< hi (expt 2 64))
507 (< lo (expt 2 64))
508 (natp hi) (natp lo))
509 (< (simple-mod-reduce-p3 hi lo)
510 (expt 2 104))))
511
512 ;; p3: the second reduction is less than 2**81
513 (defthmd simple-mod-reduce-p3-<-2**81
514 (implies (and (< hi (expt 2 64))
515 (< lo (expt 2 64))
516 (< (join hi lo) (expt 2 104))
517 (natp hi) (natp lo))
518 (< (simple-mod-reduce-p3 hi lo)
519 (expt 2 81))))
520
521 ;; p3: the third reduction is less than 2*p3
522 (defthmd simple-mod-reduce-p3-<-2*p3
523 (implies (and (< hi (expt 2 64))
524 (< lo (expt 2 64))
525 (< (join hi lo) (expt 2 81))
526 (natp hi) (natp lo))
527 (< (simple-mod-reduce-p3 hi lo)
528 (* 2 (p3)))))
529
530
531 ; -------------------------------------------------------------------------
532 ; The simple modular reductions, adapted for compiler friendly C
533 ; -------------------------------------------------------------------------
534
535 (defun mod-reduce-p1 (hi lo)
536 (let* ((y hi)
537 (x y)
538 (hi (>> hi 32))
539 (x (sub lo x))
540 (hi (if (> x lo) (+ hi -1) hi))
541 (y (<< y 32))
542 (lo (add y x))
543 (hi (if (< lo y) (+ hi 1) hi)))
544 (+ (* hi (expt 2 64)) lo)))
545
546 (defun mod-reduce-p2 (hi lo)
547 (let* ((y hi)
548 (x y)
549 (hi (>> hi 30))
550 (x (sub lo x))
551 (hi (if (> x lo) (+ hi -1) hi))
552 (y (<< y 34))
553 (lo (add y x))
554 (hi (if (< lo y) (+ hi 1) hi)))
555 (+ (* hi (expt 2 64)) lo)))
556
557 (defun mod-reduce-p3 (hi lo)
558 (let* ((y hi)
559 (x y)
560 (hi (>> hi 24))
561 (x (sub lo x))
562 (hi (if (> x lo) (+ hi -1) hi))
563 (y (<< y 40))
564 (lo (add y x))
565 (hi (if (< lo y) (+ hi 1) hi)))
566 (+ (* hi (expt 2 64)) lo)))
567
568
569 ; -------------------------------------------------------------------------
570 ; The compiler friendly versions are equal to the simple versions
571 ; -------------------------------------------------------------------------
572
573 (defthm mod-reduce-aux1
574 (implies (and (<= 0 a) (natp a) (natp m)
575 (< (- m) b) (<= b 0)
576 (integerp b)
577 (< (mod (+ b a) m)
578 (mod a m)))
579 (equal (mod (+ b a) m)
580 (+ b (mod a m))))
581 :hints (("Subgoal 2" :use ((:instance modaux-1b
582 (x (+ a b)))))))
583
584 (defthm mod-reduce-aux2
585 (implies (and (<= 0 a) (natp a) (natp m)
586 (< b m) (natp b)
587 (< (mod (+ b a) m)
588 (mod a m)))
589 (equal (+ m (mod (+ b a) m))
590 (+ b (mod a m)))))
591
592
593 (defthm mod-reduce-aux3
594 (implies (and (< 0 a) (natp a) (natp m)
595 (< (- m) b) (< b 0)
596 (integerp b)
597 (<= (mod a m)
598 (mod (+ b a) m)))
599 (equal (+ (- m) (mod (+ b a) m))
600 (+ b (mod a m))))
601 :hints (("Subgoal 1.2'" :use ((:instance modaux-1b
602 (x b))))
603 ("Subgoal 1''" :use ((:instance modaux-2d
604 (x I))))))
605
606
607 (defthm mod-reduce-aux4
608 (implies (and (< 0 a) (natp a) (natp m)
609 (< b m) (natp b)
610 (<= (mod a m)
611 (mod (+ b a) m)))
612 (equal (mod (+ b a) m)
613 (+ b (mod a m)))))
614
615
616 (defthm mod-reduce-p1==simple-mod-reduce-p1
617 (implies (and (< hi (expt 2 64))
618 (< lo (expt 2 64))
619 (natp hi) (natp lo))
620 (equal (mod-reduce-p1 hi lo)
621 (simple-mod-reduce-p1 hi lo)))
622 :hints (("Goal" :in-theory (disable expt)
623 :cases ((< 0 hi)))
624 ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1
625 (m (expt 2 64))
626 (b (+ (- HI) LO))
627 (a (* (expt 2 32) hi)))))
628 ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3
629 (m (expt 2 64))
630 (b (+ (- HI) LO))
631 (a (* (expt 2 32) hi)))))
632 ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2
633 (m (expt 2 64))
634 (b (+ (- HI) LO))
635 (a (* (expt 2 32) hi)))))
636 ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4
637 (m (expt 2 64))
638 (b (+ (- HI) LO))
639 (a (* (expt 2 32) hi)))))))
640
641
642 (defthm mod-reduce-p2==simple-mod-reduce-p2
643 (implies (and (< hi (expt 2 64))
644 (< lo (expt 2 64))
645 (natp hi) (natp lo))
646 (equal (mod-reduce-p2 hi lo)
647 (simple-mod-reduce-p2 hi lo)))
648 :hints (("Goal" :cases ((< 0 hi)))
649 ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1
650 (m (expt 2 64))
651 (b (+ (- HI) LO))
652 (a (* (expt 2 34) hi)))))
653 ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3
654 (m (expt 2 64))
655 (b (+ (- HI) LO))
656 (a (* (expt 2 34) hi)))))
657 ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2
658 (m (expt 2 64))
659 (b (+ (- HI) LO))
660 (a (* (expt 2 34) hi)))))
661 ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4
662 (m (expt 2 64))
663 (b (+ (- HI) LO))
664 (a (* (expt 2 34) hi)))))))
665
666
667 (defthm mod-reduce-p3==simple-mod-reduce-p3
668 (implies (and (< hi (expt 2 64))
669 (< lo (expt 2 64))
670 (natp hi) (natp lo))
671 (equal (mod-reduce-p3 hi lo)
672 (simple-mod-reduce-p3 hi lo)))
673 :hints (("Goal" :cases ((< 0 hi)))
674 ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1
675 (m (expt 2 64))
676 (b (+ (- HI) LO))
677 (a (* (expt 2 40) hi)))))
678 ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3
679 (m (expt 2 64))
680 (b (+ (- HI) LO))
681 (a (* (expt 2 40) hi)))))
682 ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2
683 (m (expt 2 64))
684 (b (+ (- HI) LO))
685 (a (* (expt 2 40) hi)))))
686 ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4
687 (m (expt 2 64))
688 (b (+ (- HI) LO))
689 (a (* (expt 2 40) hi)))))))
690
691
692
OLDNEW
« no previous file with comments | « Modules/_decimal/libmpdec/literature/six-step.txt ('k') | Modules/_decimal/libmpdec/memory.c » ('j') | no next file with comments »

RSS Feeds Recent Issues | This issue
This is Rietveld 894c83f36cb7+