1;
2; Copyright (c) 2008-2016 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
693