| ; |
| ; Copyright (c) 2008-2016 Stefan Krah. All rights reserved. |
| ; |
| ; Redistribution and use in source and binary forms, with or without |
| ; modification, are permitted provided that the following conditions |
| ; are met: |
| ; |
| ; 1. Redistributions of source code must retain the above copyright |
| ; notice, this list of conditions and the following disclaimer. |
| ; |
| ; 2. Redistributions in binary form must reproduce the above copyright |
| ; notice, this list of conditions and the following disclaimer in the |
| ; documentation and/or other materials provided with the distribution. |
| ; |
| ; THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS "AS IS" AND |
| ; ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE |
| ; IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE |
| ; ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR CONTRIBUTORS BE LIABLE |
| ; FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL |
| ; DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS |
| ; OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) |
| ; HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
| ; LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY |
| ; OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF |
| ; SUCH DAMAGE. |
| ; |
| |
| |
| (in-package "ACL2") |
| |
| (include-book "arithmetic/top-with-meta" :dir :system) |
| (include-book "arithmetic-2/floor-mod/floor-mod" :dir :system) |
| |
| |
| ;; ===================================================================== |
| ;; Proofs for several functions in umodarith.h |
| ;; ===================================================================== |
| |
| |
| |
| ;; ===================================================================== |
| ;; Helper theorems |
| ;; ===================================================================== |
| |
| (defthm elim-mod-m<x<2*m |
| (implies (and (<= m x) |
| (< x (* 2 m)) |
| (rationalp x) (rationalp m)) |
| (equal (mod x m) |
| (+ x (- m))))) |
| |
| (defthm modaux-1a |
| (implies (and (< x m) (< 0 x) (< 0 m) |
| (rationalp x) (rationalp m)) |
| (equal (mod (- x) m) |
| (+ (- x) m)))) |
| |
| (defthm modaux-1b |
| (implies (and (< (- x) m) (< x 0) (< 0 m) |
| (rationalp x) (rationalp m)) |
| (equal (mod x m) |
| (+ x m))) |
| :hints (("Goal" :use ((:instance modaux-1a |
| (x (- x))))))) |
| |
| (defthm modaux-1c |
| (implies (and (< x m) (< 0 x) (< 0 m) |
| (rationalp x) (rationalp m)) |
| (equal (mod x m) |
| x))) |
| |
| (defthm modaux-2a |
| (implies (and (< 0 b) (< b m) |
| (natp x) (natp b) (natp m) |
| (< (mod (+ b x) m) b)) |
| (equal (mod (+ (- m) b x) m) |
| (+ (- m) b (mod x m))))) |
| |
| (defthm modaux-2b |
| (implies (and (< 0 b) (< b m) |
| (natp x) (natp b) (natp m) |
| (< (mod (+ b x) m) b)) |
| (equal (mod (+ b x) m) |
| (+ (- m) b (mod x m)))) |
| :hints (("Goal" :use (modaux-2a)))) |
| |
| (defthm linear-mod-1 |
| (implies (and (< x m) (< b m) |
| (natp x) (natp b) |
| (rationalp m)) |
| (equal (< x (mod (+ (- b) x) m)) |
| (< x b))) |
| :hints (("Goal" :use ((:instance modaux-1a |
| (x (+ b (- x)))))))) |
| |
| (defthm linear-mod-2 |
| (implies (and (< 0 b) (< b m) |
| (natp x) (natp b) |
| (natp m)) |
| (equal (< (mod x m) |
| (mod (+ (- b) x) m)) |
| (< (mod x m) b)))) |
| |
| (defthm linear-mod-3 |
| (implies (and (< x m) (< b m) |
| (natp x) (natp b) |
| (rationalp m)) |
| (equal (<= b (mod (+ b x) m)) |
| (< (+ b x) m))) |
| :hints (("Goal" :use ((:instance elim-mod-m<x<2*m |
| (x (+ b x))))))) |
| |
| (defthm modaux-2c |
| (implies (and (< 0 b) (< b m) |
| (natp x) (natp b) (natp m) |
| (<= b (mod (+ b x) m))) |
| (equal (mod (+ b x) m) |
| (+ b (mod x m)))) |
| :hints (("Subgoal *1/8''" :use (linear-mod-3)))) |
| |
| (defthmd modaux-2d |
| (implies (and (< x m) (< 0 x) (< 0 m) |
| (< (- m) b) (< b 0) (rationalp m) |
| (<= x (mod (+ b x) m)) |
| (rationalp x) (rationalp b)) |
| (equal (+ (- m) (mod (+ b x) m)) |
| (+ b x))) |
| :hints (("Goal" :cases ((<= 0 (+ b x)))) |
| ("Subgoal 2'" :use ((:instance modaux-1b |
| (x (+ b x))))))) |
| |
| (defthm mod-m-b |
| (implies (and (< 0 x) (< 0 b) (< 0 m) |
| (< x b) (< b m) |
| (natp x) (natp b) (natp m)) |
| (equal (mod (+ (mod (- x) m) b) m) |
| (mod (- x) b)))) |
| |
| |
| ;; ===================================================================== |
| ;; addmod, submod |
| ;; ===================================================================== |
| |
| (defun addmod (a b m base) |
| (let* ((s (mod (+ a b) base)) |
| (s (if (< s a) (mod (- s m) base) s)) |
| (s (if (>= s m) (mod (- s m) base) s))) |
| s)) |
| |
| (defthmd addmod-correct |
| (implies (and (< 0 m) (< m base) |
| (< a m) (<= b m) |
| (natp m) (natp base) |
| (natp a) (natp b)) |
| (equal (addmod a b m base) |
| (mod (+ a b) m))) |
| :hints (("Goal" :cases ((<= base (+ a b)))) |
| ("Subgoal 2.1'" :use ((:instance elim-mod-m<x<2*m |
| (x (+ a b))))))) |
| |
| (defun submod (a b m base) |
| (let* ((d (mod (- a b) base)) |
| (d (if (< a d) (mod (+ d m) base) d))) |
| d)) |
| |
| (defthmd submod-aux1 |
| (implies (and (< a (mod (+ a (- b)) base)) |
| (< 0 base) (< a base) (<= b base) |
| (natp base) (natp a) (natp b)) |
| (< a b)) |
| :rule-classes :forward-chaining) |
| |
| (defthmd submod-aux2 |
| (implies (and (<= (mod (+ a (- b)) base) a) |
| (< 0 base) (< a base) (< b base) |
| (natp base) (natp a) (natp b)) |
| (<= b a)) |
| :rule-classes :forward-chaining) |
| |
| (defthmd submod-correct |
| (implies (and (< 0 m) (< m base) |
| (< a m) (<= b m) |
| (natp m) (natp base) |
| (natp a) (natp b)) |
| (equal (submod a b m base) |
| (mod (- a b) m))) |
| :hints (("Goal" :cases ((<= base (+ a b)))) |
| ("Subgoal 2.2" :use ((:instance submod-aux1))) |
| ("Subgoal 2.2'''" :cases ((and (< 0 (+ a (- b) m)) |
| (< (+ a (- b) m) m)))) |
| ("Subgoal 2.1" :use ((:instance submod-aux2))) |
| ("Subgoal 1.2" :use ((:instance submod-aux1))) |
| ("Subgoal 1.1" :use ((:instance submod-aux2))))) |
| |
| |
| (defun submod-2 (a b m base) |
| (let* ((d (mod (- a b) base)) |
| (d (if (< a b) (mod (+ d m) base) d))) |
| d)) |
| |
| (defthm submod-2-correct |
| (implies (and (< 0 m) (< m base) |
| (< a m) (<= b m) |
| (natp m) (natp base) |
| (natp a) (natp b)) |
| (equal (submod-2 a b m base) |
| (mod (- a b) m))) |
| :hints (("Subgoal 2'" :cases ((and (< 0 (+ a (- b) m)) |
| (< (+ a (- b) m) m)))))) |
| |
| |
| ;; ========================================================================= |
| ;; ext-submod is correct |
| ;; ========================================================================= |
| |
| ; a < 2*m, b < 2*m |
| (defun ext-submod (a b m base) |
| (let* ((a (if (>= a m) (- a m) a)) |
| (b (if (>= b m) (- b m) b)) |
| (d (mod (- a b) base)) |
| (d (if (< a b) (mod (+ d m) base) d))) |
| d)) |
| |
| ; a < 2*m, b < 2*m |
| (defun ext-submod-2 (a b m base) |
| (let* ((a (mod a m)) |
| (b (mod b m)) |
| (d (mod (- a b) base)) |
| (d (if (< a b) (mod (+ d m) base) d))) |
| d)) |
| |
| (defthmd ext-submod-ext-submod-2-equal |
| (implies (and (< 0 m) (< m base) |
| (< a (* 2 m)) (< b (* 2 m)) |
| (natp m) (natp base) |
| (natp a) (natp b)) |
| (equal (ext-submod a b m base) |
| (ext-submod-2 a b m base)))) |
| |
| (defthmd ext-submod-2-correct |
| (implies (and (< 0 m) (< m base) |
| (< a (* 2 m)) (< b (* 2 m)) |
| (natp m) (natp base) |
| (natp a) (natp b)) |
| (equal (ext-submod-2 a b m base) |
| (mod (- a b) m)))) |
| |
| |
| ;; ========================================================================= |
| ;; dw-reduce is correct |
| ;; ========================================================================= |
| |
| (defun dw-reduce (hi lo m base) |
| (let* ((r1 (mod hi m)) |
| (r2 (mod (+ (* r1 base) lo) m))) |
| r2)) |
| |
| (defthmd dw-reduce-correct |
| (implies (and (< 0 m) (< m base) |
| (< hi base) (< lo base) |
| (natp m) (natp base) |
| (natp hi) (natp lo)) |
| (equal (dw-reduce hi lo m base) |
| (mod (+ (* hi base) lo) m)))) |
| |
| (defthmd <=-multiply-both-sides-by-z |
| (implies (and (rationalp x) (rationalp y) |
| (< 0 z) (rationalp z)) |
| (equal (<= x y) |
| (<= (* z x) (* z y))))) |
| |
| (defthmd dw-reduce-aux1 |
| (implies (and (< 0 m) (< m base) |
| (natp m) (natp base) |
| (< lo base) (natp lo) |
| (< x m) (natp x)) |
| (< (+ lo (* base x)) (* base m))) |
| :hints (("Goal" :cases ((<= (+ x 1) m))) |
| ("Subgoal 1''" :cases ((<= (* base (+ x 1)) (* base m)))) |
| ("subgoal 1.2" :use ((:instance <=-multiply-both-sides-by-z |
| (x (+ 1 x)) |
| (y m) |
| (z base)))))) |
| |
| (defthm dw-reduce-aux2 |
| (implies (and (< x (* base m)) |
| (< 0 m) (< m base) |
| (natp m) (natp base) (natp x)) |
| (< (floor x m) base))) |
| |
| ;; This is the necessary condition for using _mpd_div_words(). |
| (defthmd dw-reduce-second-quotient-fits-in-single-word |
| (implies (and (< 0 m) (< m base) |
| (< hi base) (< lo base) |
| (natp m) (natp base) |
| (natp hi) (natp lo) |
| (equal r1 (mod hi m))) |
| (< (floor (+ (* r1 base) lo) m) |
| base)) |
| :hints (("Goal" :cases ((< r1 m))) |
| ("Subgoal 1''" :cases ((< (+ lo (* base (mod hi m))) (* base m)))) |
| ("Subgoal 1.2" :use ((:instance dw-reduce-aux1 |
| (x (mod hi m))))))) |
| |
| |
| ;; ========================================================================= |
| ;; dw-submod is correct |
| ;; ========================================================================= |
| |
| (defun dw-submod (a hi lo m base) |
| (let* ((r (dw-reduce hi lo m base)) |
| (d (mod (- a r) base)) |
| (d (if (< a r) (mod (+ d m) base) d))) |
| d)) |
| |
| (defthmd dw-submod-aux1 |
| (implies (and (natp a) (< 0 m) (natp m) |
| (natp x) (equal r (mod x m))) |
| (equal (mod (- a x) m) |
| (mod (- a r) m)))) |
| |
| (defthmd dw-submod-correct |
| (implies (and (< 0 m) (< m base) |
| (natp a) (< a m) |
| (< hi base) (< lo base) |
| (natp m) (natp base) |
| (natp hi) (natp lo)) |
| (equal (dw-submod a hi lo m base) |
| (mod (- a (+ (* base hi) lo)) m))) |
| :hints (("Goal" :in-theory (disable dw-reduce) |
| :use ((:instance dw-submod-aux1 |
| (x (+ lo (* base hi))) |
| (r (dw-reduce hi lo m base))) |
| (:instance dw-reduce-correct))))) |
| |
| |
| ;; ========================================================================= |
| ;; ANSI C arithmetic for uint64_t |
| ;; ========================================================================= |
| |
| (defun add (a b) |
| (mod (+ a b) |
| (expt 2 64))) |
| |
| (defun sub (a b) |
| (mod (- a b) |
| (expt 2 64))) |
| |
| (defun << (w n) |
| (mod (* w (expt 2 n)) |
| (expt 2 64))) |
| |
| (defun >> (w n) |
| (floor w (expt 2 n))) |
| |
| ;; join upper and lower half of a double word, yielding a 128 bit number |
| (defun join (hi lo) |
| (+ (* (expt 2 64) hi) lo)) |
| |
| |
| ;; ============================================================================= |
| ;; Fast modular reduction |
| ;; ============================================================================= |
| |
| ;; These are the three primes used in the Number Theoretic Transform. |
| ;; A fast modular reduction scheme exists for all of them. |
| (defmacro p1 () |
| (+ (expt 2 64) (- (expt 2 32)) 1)) |
| |
| (defmacro p2 () |
| (+ (expt 2 64) (- (expt 2 34)) 1)) |
| |
| (defmacro p3 () |
| (+ (expt 2 64) (- (expt 2 40)) 1)) |
| |
| |
| ;; reduce the double word number hi*2**64 + lo (mod p1) |
| (defun simple-mod-reduce-p1 (hi lo) |
| (+ (* (expt 2 32) hi) (- hi) lo)) |
| |
| ;; reduce the double word number hi*2**64 + lo (mod p2) |
| (defun simple-mod-reduce-p2 (hi lo) |
| (+ (* (expt 2 34) hi) (- hi) lo)) |
| |
| ;; reduce the double word number hi*2**64 + lo (mod p3) |
| (defun simple-mod-reduce-p3 (hi lo) |
| (+ (* (expt 2 40) hi) (- hi) lo)) |
| |
| |
| ; ---------------------------------------------------------- |
| ; The modular reductions given above are correct |
| ; ---------------------------------------------------------- |
| |
| (defthmd congruence-p1-aux |
| (equal (* (expt 2 64) hi) |
| (+ (* (p1) hi) |
| (* (expt 2 32) hi) |
| (- hi)))) |
| |
| (defthmd congruence-p2-aux |
| (equal (* (expt 2 64) hi) |
| (+ (* (p2) hi) |
| (* (expt 2 34) hi) |
| (- hi)))) |
| |
| (defthmd congruence-p3-aux |
| (equal (* (expt 2 64) hi) |
| (+ (* (p3) hi) |
| (* (expt 2 40) hi) |
| (- hi)))) |
| |
| (defthmd mod-augment |
| (implies (and (rationalp x) |
| (rationalp y) |
| (rationalp m)) |
| (equal (mod (+ x y) m) |
| (mod (+ x (mod y m)) m)))) |
| |
| (defthmd simple-mod-reduce-p1-congruent |
| (implies (and (integerp hi) |
| (integerp lo)) |
| (equal (mod (simple-mod-reduce-p1 hi lo) (p1)) |
| (mod (join hi lo) (p1)))) |
| :hints (("Goal''" :use ((:instance congruence-p1-aux) |
| (:instance mod-augment |
| (m (p1)) |
| (x (+ (- hi) lo (* (expt 2 32) hi))) |
| (y (* (p1) hi))))))) |
| |
| (defthmd simple-mod-reduce-p2-congruent |
| (implies (and (integerp hi) |
| (integerp lo)) |
| (equal (mod (simple-mod-reduce-p2 hi lo) (p2)) |
| (mod (join hi lo) (p2)))) |
| :hints (("Goal''" :use ((:instance congruence-p2-aux) |
| (:instance mod-augment |
| (m (p2)) |
| (x (+ (- hi) lo (* (expt 2 34) hi))) |
| (y (* (p2) hi))))))) |
| |
| (defthmd simple-mod-reduce-p3-congruent |
| (implies (and (integerp hi) |
| (integerp lo)) |
| (equal (mod (simple-mod-reduce-p3 hi lo) (p3)) |
| (mod (join hi lo) (p3)))) |
| :hints (("Goal''" :use ((:instance congruence-p3-aux) |
| (:instance mod-augment |
| (m (p3)) |
| (x (+ (- hi) lo (* (expt 2 40) hi))) |
| (y (* (p3) hi))))))) |
| |
| |
| ; --------------------------------------------------------------------- |
| ; We need a number less than 2*p, so that we can use the trick from |
| ; elim-mod-m<x<2*m for the final reduction. |
| ; For p1, two modular reductions are sufficient, for p2 and p3 three. |
| ; --------------------------------------------------------------------- |
| |
| ;; p1: the first reduction is less than 2**96 |
| (defthmd simple-mod-reduce-p1-<-2**96 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (natp hi) (natp lo)) |
| (< (simple-mod-reduce-p1 hi lo) |
| (expt 2 96)))) |
| |
| ;; p1: the second reduction is less than 2*p1 |
| (defthmd simple-mod-reduce-p1-<-2*p1 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (< (join hi lo) (expt 2 96)) |
| (natp hi) (natp lo)) |
| (< (simple-mod-reduce-p1 hi lo) |
| (* 2 (p1))))) |
| |
| |
| ;; p2: the first reduction is less than 2**98 |
| (defthmd simple-mod-reduce-p2-<-2**98 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (natp hi) (natp lo)) |
| (< (simple-mod-reduce-p2 hi lo) |
| (expt 2 98)))) |
| |
| ;; p2: the second reduction is less than 2**69 |
| (defthmd simple-mod-reduce-p2-<-2*69 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (< (join hi lo) (expt 2 98)) |
| (natp hi) (natp lo)) |
| (< (simple-mod-reduce-p2 hi lo) |
| (expt 2 69)))) |
| |
| ;; p3: the third reduction is less than 2*p2 |
| (defthmd simple-mod-reduce-p2-<-2*p2 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (< (join hi lo) (expt 2 69)) |
| (natp hi) (natp lo)) |
| (< (simple-mod-reduce-p2 hi lo) |
| (* 2 (p2))))) |
| |
| |
| ;; p3: the first reduction is less than 2**104 |
| (defthmd simple-mod-reduce-p3-<-2**104 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (natp hi) (natp lo)) |
| (< (simple-mod-reduce-p3 hi lo) |
| (expt 2 104)))) |
| |
| ;; p3: the second reduction is less than 2**81 |
| (defthmd simple-mod-reduce-p3-<-2**81 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (< (join hi lo) (expt 2 104)) |
| (natp hi) (natp lo)) |
| (< (simple-mod-reduce-p3 hi lo) |
| (expt 2 81)))) |
| |
| ;; p3: the third reduction is less than 2*p3 |
| (defthmd simple-mod-reduce-p3-<-2*p3 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (< (join hi lo) (expt 2 81)) |
| (natp hi) (natp lo)) |
| (< (simple-mod-reduce-p3 hi lo) |
| (* 2 (p3))))) |
| |
| |
| ; ------------------------------------------------------------------------- |
| ; The simple modular reductions, adapted for compiler friendly C |
| ; ------------------------------------------------------------------------- |
| |
| (defun mod-reduce-p1 (hi lo) |
| (let* ((y hi) |
| (x y) |
| (hi (>> hi 32)) |
| (x (sub lo x)) |
| (hi (if (> x lo) (+ hi -1) hi)) |
| (y (<< y 32)) |
| (lo (add y x)) |
| (hi (if (< lo y) (+ hi 1) hi))) |
| (+ (* hi (expt 2 64)) lo))) |
| |
| (defun mod-reduce-p2 (hi lo) |
| (let* ((y hi) |
| (x y) |
| (hi (>> hi 30)) |
| (x (sub lo x)) |
| (hi (if (> x lo) (+ hi -1) hi)) |
| (y (<< y 34)) |
| (lo (add y x)) |
| (hi (if (< lo y) (+ hi 1) hi))) |
| (+ (* hi (expt 2 64)) lo))) |
| |
| (defun mod-reduce-p3 (hi lo) |
| (let* ((y hi) |
| (x y) |
| (hi (>> hi 24)) |
| (x (sub lo x)) |
| (hi (if (> x lo) (+ hi -1) hi)) |
| (y (<< y 40)) |
| (lo (add y x)) |
| (hi (if (< lo y) (+ hi 1) hi))) |
| (+ (* hi (expt 2 64)) lo))) |
| |
| |
| ; ------------------------------------------------------------------------- |
| ; The compiler friendly versions are equal to the simple versions |
| ; ------------------------------------------------------------------------- |
| |
| (defthm mod-reduce-aux1 |
| (implies (and (<= 0 a) (natp a) (natp m) |
| (< (- m) b) (<= b 0) |
| (integerp b) |
| (< (mod (+ b a) m) |
| (mod a m))) |
| (equal (mod (+ b a) m) |
| (+ b (mod a m)))) |
| :hints (("Subgoal 2" :use ((:instance modaux-1b |
| (x (+ a b))))))) |
| |
| (defthm mod-reduce-aux2 |
| (implies (and (<= 0 a) (natp a) (natp m) |
| (< b m) (natp b) |
| (< (mod (+ b a) m) |
| (mod a m))) |
| (equal (+ m (mod (+ b a) m)) |
| (+ b (mod a m))))) |
| |
| |
| (defthm mod-reduce-aux3 |
| (implies (and (< 0 a) (natp a) (natp m) |
| (< (- m) b) (< b 0) |
| (integerp b) |
| (<= (mod a m) |
| (mod (+ b a) m))) |
| (equal (+ (- m) (mod (+ b a) m)) |
| (+ b (mod a m)))) |
| :hints (("Subgoal 1.2'" :use ((:instance modaux-1b |
| (x b)))) |
| ("Subgoal 1''" :use ((:instance modaux-2d |
| (x I)))))) |
| |
| |
| (defthm mod-reduce-aux4 |
| (implies (and (< 0 a) (natp a) (natp m) |
| (< b m) (natp b) |
| (<= (mod a m) |
| (mod (+ b a) m))) |
| (equal (mod (+ b a) m) |
| (+ b (mod a m))))) |
| |
| |
| (defthm mod-reduce-p1==simple-mod-reduce-p1 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (natp hi) (natp lo)) |
| (equal (mod-reduce-p1 hi lo) |
| (simple-mod-reduce-p1 hi lo))) |
| :hints (("Goal" :in-theory (disable expt) |
| :cases ((< 0 hi))) |
| ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 32) hi))))) |
| ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 32) hi))))) |
| ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 32) hi))))) |
| ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 32) hi))))))) |
| |
| |
| (defthm mod-reduce-p2==simple-mod-reduce-p2 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (natp hi) (natp lo)) |
| (equal (mod-reduce-p2 hi lo) |
| (simple-mod-reduce-p2 hi lo))) |
| :hints (("Goal" :cases ((< 0 hi))) |
| ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 34) hi))))) |
| ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 34) hi))))) |
| ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 34) hi))))) |
| ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 34) hi))))))) |
| |
| |
| (defthm mod-reduce-p3==simple-mod-reduce-p3 |
| (implies (and (< hi (expt 2 64)) |
| (< lo (expt 2 64)) |
| (natp hi) (natp lo)) |
| (equal (mod-reduce-p3 hi lo) |
| (simple-mod-reduce-p3 hi lo))) |
| :hints (("Goal" :cases ((< 0 hi))) |
| ("Subgoal 1.2.2'" :use ((:instance mod-reduce-aux1 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 40) hi))))) |
| ("Subgoal 1.2.1'" :use ((:instance mod-reduce-aux3 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 40) hi))))) |
| ("Subgoal 1.1.2'" :use ((:instance mod-reduce-aux2 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 40) hi))))) |
| ("Subgoal 1.1.1'" :use ((:instance mod-reduce-aux4 |
| (m (expt 2 64)) |
| (b (+ (- HI) LO)) |
| (a (* (expt 2 40) hi))))))) |
| |
| |
| |
