; This is a proof of a simple arbitrary precision multiplication
; implemted in C then converted to lisp.
; The input is two arrays of 32-bit numbers that represent the
; operands and the result is placed in a third array.  The first
; element of the array represent the least significant 32 bits etc.
; In lisp, we use lists to represent the arrays.  We assume that C
; provides us with correct 32 and 64-bit operations.
;
; Many proofs below contain hints.  Some of the hints may not be
; necessary, but they can make the proof faster by disabling rules
; that do not apply, but slow down the theorem prover which tries to
; apply them anyways only to discover that the hypotheses of the
; theorem do not hold.  Also we often have :do-not generalize hint,
; that is almost always unnecessary, but during the proof attempts it
; is generalily desirable to disable generalization since most of the
; time this leads to failed proofs.

; First we include some useful books
(include-book "/l/acl2/v2-5/acl2-sources/books/ihs/quotient-remainder-lemmas")
(include-book "/l/acl2/v2-5/acl2-sources/books/arithmetic/top")
(include-book "/l/acl2/v2-5/acl2-sources/books/ihs/math-lemmas")

; The following disables floor and mod, so that the theorems about
; them can be used.  If we did not enable them, they would be expanded
; befory the theorems could be applied.  In addition we disable (:elim
; floor-mod-elim) since this often makes the proofs more difficult.
(in-theory (disable (:definition floor) (:definition mod)
		    (:elim floor-mod-elim)))

; Now we will admit a bunch of trivial general purpose theorems that
; we need for our proofs.  Probably some of these should be added to
; the standard acl2 books.

; First rules to cancel the middle term of a 3-term sum.  There is a
; rule for canceling the third argument, but not the second.  The
; theorems would work without the hint, but takes much more time.

(defthm cancel-mod-+-middle
  (implies
   (and (equal i (/ y z))
        (integerp i)
        (force (rationalp w))
        (force (rationalp x))
        (force (rationalp y))
        (force (rationalp z))
        (force (not (equal z 0))))
   (equal (mod (+ w y x) z)
          (mod (+ w x) z)))
  :hints (("Goal" :in-theory '(cancel-mod-+-3 commutativity-of-+))))

(defthm cancel-floor-+-middle
  (implies
   (and (equal i (/ y z))
        (integerp i)
        (force (rationalp w))
        (force (rationalp x))
        (force (rationalp y))
        (force (rationalp z))
        (force (not (equal z 0))))
   (equal (floor (+ w y x) z)
          (+ i (floor (+ w x) z))))
  :hints (("Goal" :in-theory '(cancel-floor-+-3 commutativity-of-+))))

(defthm swap-floor-mod
  (implies (and (integerp i) (rationalp x) (integerp y) (< 0 i) (< 0 y))
	   (equal (floor (mod x (* i y)) y)
		  (mod (floor x y) i)))
  :hints (("Goal" :in-theory (e/d (mod) (FLOOR-BOUNDS MOD-BOUNDS MOD-TYPE)))))

(defthm swap-floor-mod2
  (implies (and (integerp i) (rationalp x) (integerp y) (< 0 i) (< 0 y))
	   (equal (floor (mod x (* y i)) y)
		  (mod (floor x y) i)))
  :hints (("Goal" :in-theory '(COMMUTATIVITY-OF-* SWAP-FLOOR-MOD))))

(defthm mod-range
  (implies (and (integerp x) (integerp y) (< 0 y))
	   (<= (mod x y) (1- y)))
  :hints (("Goal" :use mod-bounds)))

; Define some constants.  For simplicity, we do not prove our results
; to arbitrary word sizes, as this would require to pass an extra size
; arguments to most functions, but the proof does not rely on the
; value of these constants, so changing the definition below the proof
; applies to arbitrary word sizes.

(defconst *wbits* 32)
(defconst *dwbits* (* 2 *wbits*))
(defconst *wmod* (expt 2 *wbits*))
(defconst *dwmod* (expt 2 (* 2 *wbits*)))
(defconst *wmax* (1- *wmod*))
(defconst *dwmax* (1- *dwmod*))
(defconst *mulwmax* (* *wmax* *wmax*))

; These are assertions we can use in an implementation.  Logically
; they are identity functions, they are only used for guard proofs.
; These express that a value is 32 or 64 bit integer

(defmacro word_t (x) `(the (unsigned-byte 32) ,x))
(defmacro dword_t (x) `(the (unsigned-byte 64) ,x))

; Macros for recognizing naturals and 32/64-bit unsigned integers.
(defmacro naturalp (x) `(and (integerp ,x) (<= 0 ,x)))

(defmacro wordp (x)
  `(and (integerp ,x)
	(<= 0 ,x)
	(<= ,x *wmax*)))

(defmacro dwordp (x)
  `(and (integerp ,x)
	(<= 0 ,x)
	(<= ,x *dwmax*)))

; Extractor macros.  hi-word really just removes the least significant
; 32-bit word from an integer.

(defmacro lo-dword (x)
  `(mod ,x *dwmod*))

(defmacro lo-word (x)
  `(mod ,x *wmod*))

(defmacro hi-dword (x)
  `(floor ,x *dwmod*))

(defmacro hi-word (x)
  `(floor ,x *wmod*))

; If the sum of nonnegatives <= 0, they are zero: x+y<=0 iff x=0 and
; y=0, but we have to write in negative form, because <= is a macro
; that expands to not >

(defthm nat-sum-<=-0
  (implies (and (naturalp i) (naturalp j))
	   (equal (< 0 (+ i j))
		  (not (and (equal i 0) (equal j 0))))))

(defthm cross-cancellation-for-*
   (equal (equal (* x z) (* z y))
          (or (equal 0 (fix z))
              (equal (fix x) (fix y)))))

(defthm <-+-left-cancel
  (implies (and (rationalp x) (rationalp y) (rationalp z))
	   (equal (< (+ x y) (+ x z)) (< y z))))

(defthm <-+-right-cancel
  (implies (and (rationalp x) (rationalp y) (rationalp z))
	   (equal (< (+ x z) (+ y z)) (< x y))))

; The multiple of two unsigned 32-bit integer is at most (2^32-1)^2
(defthm mul-range
  (implies (and (wordp x)
		(wordp y))
	   (and (<= 0 (* x y))
		(<= (* x y) *mulwmax*)))
  :hints
  (("Goal''" :use ((:instance *-PRESERVES->=-FOR-NONNEGATIVES
			      (x2 x) (y2 y)
			      (x1 *wmax*) (y1 *wmax*)))))
  :rule-classes ((:linear) (:rewrite)))

; This function recognizes our input representation format: a
; nil-terminated list of nonnegative 32-bit integers

(defun word-listp (x)
  (declare (xargs :guard t))
  (if (consp x)
      (and (wordp (car x))
	   (word-listp (cdr x)))
    (equal x nil)))

(defthm word-lists-are-lists
  (implies (word-listp x) (true-listp x)))

; This converts from the list representation to the real mathematical
; value.  Note that acl2 has arbitrary precision rational arithmetic.

(defun int-value (a)
  (declare (xargs :guard (word-listp a)))
  (if (consp a)
      (+ (car a) (* *wmod* (int-value (cdr a))))
    0))

(defthm int-value-naturalp
  (implies (word-listp a)
	   (naturalp (int-value a)))
  :rule-classes :type-prescription)

; This is the C `+' operator between on uint64_t type numbers, that is
; really modulo arithmetic base 2^64.

(defun +<64> (x y)
  (declare (type (unsigned-byte 64) x y))
  (lo-dword (+ x y)))

; This is an alternative definition that we state as a theorem,
; sometime we wil disable the above definition and enable onlt this

(defthm +<64>-altdef
  (implies (and (dwordp x) (dwordp y))
	   (equal (+<64> x y)
		  (if (< (+ x y) *dwmod*)
		      (+ x y) (+ x y (- *dwmod*)))))
  :hints (("Subgoal 1" :in-theory (disable mod-x-y-=-x)
	   :use ((:instance mod-x-y-=-x (x (+ -18446744073709551616 X Y))
			    (y *dwmod*))))))

(in-theory (disable +<64>-altdef))

; This function provide random access to the nth element of an array
; represented as a list.  Note the difference from the built-in nth
; function, this returns 0 instead of nil if we access past the end of
; the array.  This makes many proofs easier.  However, we use guards
; to ensure that out-of-bounds access does not happen.

(defun my-nth (n a)
  (declare (xargs :guard (and (true-listp a) (integerp n)
			      (<= 0 n) (< n (len a)))))
  (if (endp a)
      0
    (if (zp n)
	(car a)
      (my-nth (1- n) (cdr a)))))

; This theorem says that reading after the end of the array you get 0

(defthm my-nth-len-is-zero
  (implies (and (integerp i) (<= (len a) i))
	   (equal (my-nth i a) 0)))

(defthm nth-word-list-is-wordp
  (implies (word-listp a)
	   (wordp (my-nth n a)))
    :rule-classes :type-prescription)

(defthm nth-word-list-range
  (implies (word-listp a)
	   (and (<= 0 (my-nth n a))
		(<= (my-nth n a) *wmax*)))
  :rule-classes :linear)

; This is the inverse of int-value, converts an integer back to its
; list representation.  We do not really need this, but proving that
; this is really an inverse is easy:

(defun uint-to-word-list (i)
  (declare (xargs :guard (naturalp i)))
  (if (zp i) nil
    (cons (lo-word i) (uint-to-word-list (hi-word i)))))

; One direction of the inverse proof:

(defthm inv-int-value
  (implies (naturalp i)
	   (equal (int-value (uint-to-word-list i)) i)))

; The other direction is only partially true, since adding zeros at
; the end (at the most significant position) does not change the
; int-value, so the inverse is only unique up to this congruence: two
; list are equivalent if they only differ in trailing zeros.

(defun wlist-equal (x y)
  (declare (xargs :measure (+ (len x) (len y))))
  (cond ((endp x) (or (endp y)
		      (and (equal (car y) 0) (wlist-equal nil (cdr y)))))
	((endp y) (and (equal (car x) 0) (wlist-equal (cdr x) nil)))
	(t (and (equal (car x) (car y))
		(wlist-equal (cdr x) (cdr y))))))

(defthm int-value-wlist-equal-invariant
  (implies (wlist-equal x y)
	   (equal (int-value x) (int-value y)))
  :rule-classes nil)

(defthm inv-int-value2
  (implies (word-listp l)
	   (wlist-equal (uint-to-word-list (int-value l)) l)))

; The functions w+ and dw+ are logically equivalent to +, but they
; have a guards that ensures that they are only called with 32/64-bit
; integers and the sum does not overflow.

(defun w+ (x y)
  (declare (xargs :guard (and (wordp x) (wordp y) (wordp (+ x y)))))
  (+ x y))

(defun dw+ (x y)
  (declare (xargs :guard (and (dwordp x) (dwordp y) (dwordp (+ x y)))))
  (+ x y))

; This is the same as * but with a guard to requite word args.  The
; multiple of two words is always a valid 64-bit word, so there is not
; overflow.

(defun w* (x y)
  (declare (xargs :guard (and (wordp x) (wordp y))))
  (* x y))

; This concludes the preparation phase, now we can get to the meat.
; Here is the exacy copy of the C function we would like to verify:
;
;void Multiply(uint32_t *a, uint32_t abits, uint32_t *b, uint32_t bbits,
;	       uint32_t *r, uint32_t nbits)
;{
;    uint32_t i;
;    uint64_t sum = 0;
;    uint32_t n  = (nbits - 1) / 32;
;    uint32_t an = (abits - 1) / 32;
;    uint32_t bn = (bbits - 1) / 32;
;    for (i = 0; i != n; i++) {
;	 uint32_t carry = 0;
;	 uint32_t jmax = min(i, an);
;	 for (uint32_t j = i <= bn ? 0 : i - bn; j <= jmax; j++) {
;	     uint64_t prod = a[j] * uint64_t(b[i-j]);
;	     if (prod > ~sum)
;		 carry++;
;	     sum += prod;
;	 }
;	 r[i] = sum;
;	 sum = (uint64_t(carry) << 32) + (sum >> 32);
;    }
;
;    uint32_t s32 = sum;
;    i = min(n, an);
;    do {
;	 if (n-i <= bn)
;	     s32 += a[i] * b[n-i];
;    } while (i--);
;
;    uint32_t part = nbits % 32;
;    if (part)
;	 s32 &= (1ul << part) - 1;
;    r[n] = s32;
;}
;
; We convert this into lisp starting from the innermost loop.  That
; loop calculates the ith word of the result using the carry from the
; previous words.  For simplicity, we do not use abit and bbits,
; instead we assume that the number of words is the length of the list
; operands.  We want this function to return \sum_{k=j}^i a_kb_{i-k} +
; sum + carry * 2^64.  The result is actually a pair, low-order 64 bit
; of the sum and the rest.  The loop variable is increasing, so we
; have to define a measure, otherwise acl2 cannot prove the
; termination.  The guards of the function assure that this function
; is always called by the proper arguments.  Since this is a recursive
; function, we need to prove that the function never calls itself with
; incorrect arguments.  This means that i cannot be 2^32-1 since the
; recursion in j stops when j exceeds i, that's why the guard for i
; has to be stronger than (wordp i).  Similarly, to ensure that carry
; does not overflow, we need carry + 1 + i - j < 2^32, since there are
; i-j+1 iterations, and each iteration can increase carry by 1.

(defun long-mult-ith-word (a b i sum carry j)
  (declare (xargs :measure (nfix (- (len a) j))
		  :guard (and (word-listp a) (word-listp b) (naturalp i)
			      (< i *wmax*) (wordp j) (wordp carry)
			      (wordp (+ (nfix (+ 1 i (- j))) carry))
			      (dwordp sum) (< (- i j) (len b)))))
  (let* ((an (1- (len a)))
	 (jmax (min i an)))
    (if (and (integerp j) (<= j jmax))
	(let ((prod (w* (my-nth j a) (my-nth (- i j) b))))
	  (long-mult-ith-word a b i (+<64> sum prod)
			      (if (> prod (- *dwmax* sum))
				  (w+ 1 carry) carry) (w+ 1 j)))
      (mv sum carry))))

; The above function is tail-recursive and returns a pair, but it is
; usually easier to argue about non-tail-recursive scalar valued
; functions that have fewer arguments and simpler recursive structure,
; so first we rewrite the above function.

(defun ith-sum (a b i j)
  (declare (xargs :measure (nfix (- (len a) j))
		  :guard (and (word-listp a) (word-listp b)
			      (naturalp i) (naturalp j)
			      (< (- i j) (len b)))
		  :guard-hints (("Goal" :do-not generalize :do-not-induct t))))
  (let* ((an (1- (len a)))
	 (jmax (min i an)))
    (if (and (integerp j) (<= j jmax))
	(let ((prod (* (my-nth j a) (my-nth (- i j) b))))
	  (+ prod (ith-sum a b i (1+ j))))
      0)))

; The following theorem proves that (long-mult-ith-word a b i sum
; carry j) returns \sum_{k=j}^i a_k b_{i-k} + sum + carry * 2^64 after
; the pair it returns is converted to int by adding the second element
; multiplied by 2^64 to the first element.  In the proof we use
; +<64>-altdef, disable +<64>.  This way the theorem prover can
; replace +<64> by + after a case split on the overflow condition,
; which greatly simplifies the proof.  Note that that we try to state
; this theorem in the most general form, without requiring anything
; about carry, and we do not have any upper bounds on i and j.

(defthm long-mult-ith-word-is-sum
  (implies (and (word-listp a) (word-listp b)
		(naturalp i) (naturalp j) (dwordp sum))
	   (equal (+ (mv-nth 0 (long-mult-ith-word a b i sum carry j))
		     (* *dwmod*
			(mv-nth 1 (long-mult-ith-word a b i sum carry j))))
		  (+ sum (ith-sum a b i j) (* *dwmod* carry))))
  :hints (("Goal" :do-not generalize
	   :in-theory (e/d (+<64>-altdef) (+<64>)))))

; The above rule can only be used when the pair returned by the loop
; is used exactly as it appears on the left-hand side of the avove
; equality.  A more useful rule can rewrite the pair independently.
; For that, we need more lemmas.  First we have to show that the first
; element of the returned pair is a dword:

(defthm first-is-dwordp
  (implies (and (word-listp a) (word-listp b) (dwordp sum))
	   (dwordp (mv-nth 0 (long-mult-ith-word a b i sum carry j))))
  :rule-classes ((:type-prescription) (:rewrite)))

(defthm first-bounds
  (implies (and (word-listp a) (word-listp b) (dwordp sum))
	   (and (<= 0 (mv-nth 0 (long-mult-ith-word a b i sum carry j)))
		(<= (mv-nth 0 (long-mult-ith-word a b i sum carry j))
		    *dwmax*)))
  :hints (("Goal" :use first-is-dwordp :in-theory nil))
  :rule-classes :linear)

; And the second element is natural
(defthm second-is-naturalp
  (implies (and (word-listp a) (word-listp b) (naturalp carry))
	   (naturalp (mv-nth 1 (long-mult-ith-word a b i sum carry
						   j))))
  :rule-classes ((:type-prescription) (:rewrite)))

; And ith-sum is natural too
(defthm ith-sum-type
  (implies (and (word-listp a) (word-listp b))
	   (naturalp  (ith-sum a b i j)))
  :rule-classes :type-prescription)

; The next one is the same for the ith-sum of a cons, we need that,
; because to satisfy the hypothesis of a type-prescription rule only
; type-prescription rules are applied, therefore the theorem prover
; does not know about (word-listp (cons a1 a2))
(defthm ith-sum-cons-type
  (implies (and (wordp a1) (word-listp a2) (word-listp b))
	   (naturalp (ith-sum (cons a1 a2) b i j)))
  :hints (("Goal" :use ((:instance ith-sum-type (a (cons a1 a2))))))
  :rule-classes :type-prescription)

; This lemma is required for the subsequent theorems

(defthm mul-equal-lemma
  (implies (and (rationalp x) (integerp y) (rationalp z) (rationalp m)
		(< 0 m) (<= 0 x) (< x m))
	   (equal (equal (+ x (* m y)) z)
		  (and (equal (mod z m) x)
		       (equal (floor z m) y))))
  :hints (("[1]Subgoal 1'" :in-theory (enable mod))
	  ("[1]Subgoal 2'" :in-theory (enable mod))))

; And this is the theorem that can be use to replace all instances of
; long-mult-ith-word with an ith-sum expression.

(defthm long-mult-ith-word-is-sum-01
  (implies (and (word-listp a) (word-listp b) (naturalp i)
		(naturalp j) (naturalp carry) (dwordp sum))
	   (and (equal (mv-nth 0 (long-mult-ith-word a b i sum carry j))
		       (lo-dword (+ sum (ith-sum a b i j) (* *dwmod* carry))))
		(equal (mv-nth 1 (long-mult-ith-word a b i sum carry j))
		       (floor (+ sum (ith-sum a b i j) (* *dwmod* carry))
			      *dwmod*))))
  :hints (("Goal" :use long-mult-ith-word-is-sum :do-not generalize
	   :in-theory (disable mv-nth long-mult-ith-word-is-sum))))

; This gives an upper bound to ith-sum
(defthm ith-sum-range
  (implies (and (word-listp a) (word-listp b) (naturalp i) (naturalp j))
	   (<= (ith-sum a b i j) (* (nfix (+ i (- j) 1)) *mulwmax*)))
  :rule-classes ((:linear) (:rewrite)))

; And here is the lisp version of the outer for loop:

(defun long-mult-forloop (a b n i sum)
  (declare (xargs :measure (nfix (- n i))
		  :guard (and (word-listp a) (word-listp b) (consp a) (consp b)
			      (wordp i) (wordp n) (dwordp sum) (<= i n))))
  (if (zp (- n i))
      nil
    (let* ((bn (1- (len b)))
	   (j  (if (<= i bn) 0 (- i bn))))
      (mv-let (sum2 carry) (long-mult-ith-word a b i sum 0 j)
	      (cons (lo-word sum2)
		    (long-mult-forloop a b n (1+ i)
				       (+ (hi-word sum2)
					  (* *wmod* carry))))))))

; The above loop returns a list of words as a result, the next is an
; equivalent function that returns a single integer.  It will be
; easier to reason abot this version.

(defun long-mult-forloop-int (a b n i sum)
  (declare (xargs :measure (nfix (- n i))))
  (if (zp (- n i))
      0
    (let ((sum2 (+ sum (ith-sum a b i 0))))
      (+ (lo-word sum2)
	 (* *wmod* (long-mult-forloop-int a b n (1+ i) (hi-word sum2)))))))

; To prove that the two are the same, first notice that we use
; (ith-sum a b i 0) above instead of (ith-sum a b i j) where j is
; assigned in an if statement.  This is because in the C program we
; are not allowed to access beyond the end of an array (and we do not,
; this is guaranteed by the guard of my-nth that was verified).  But
; my-nth, like all acl2 functions is defined everywhere, and returns 0
; when reading past the end of the list, so we do not have to worry
; about out-of bounds access.  We prove first that we can use (ith-sum
; a b i 0) here.  We need some lemmas about ith-sum.

(defthm ith-sum-big-i
  (implies (and (integerp i) (< (+ -2 (len a) (len b)) i))
	   (equal (ith-sum a b i j) 0)))

(defthm ith-sum-nil
  (implies (atom x)
	   (and (equal (ith-sum x b i j) 0)
		(equal (ith-sum a x i j) 0))))

(defun j<=n-induction (i n)
  (declare (xargs :measure (nfix (- n i))))
  (if (zp (- n i)) i
    (j<=n-induction (1+ i) n)))

; This is almost what we want.  We need to prove, that if j <=
; i+1-len(b), then (ith-sum a b i j) = (ith-sum a b i 0), but the
; basecase of the induction is difficult to prove.  So instead, we
; prove that it is (ith-sum a b i (+ 1 i (- (len b)))), which have a
; trivial base-case, then use this lemma to obtain the result.

(defthm ith-sum-0-lemma
  (implies (and (naturalp i) (naturalp j) (<= j (+ 1 i (- (len b)))))
	   (equal (ith-sum a b i j) (ith-sum a b i (+ 1 i (- (len b))))))
  :hints (("Goal'" :do-not generalize
	   :induct (j<=n-induction j (+ 1 i (- (len b))))))
  :rule-classes nil)

; This rewrites (ith-sum a b i j) to (ith-sum a b i 0) but the rule
; would also match the result, (ith-sum a b i 0), so we have to
; restrict it, if j is already rewritten to 0, the rule should not
; apply.  This is done in the syntaxp hypothesis.  We do not want to
; write (not (equal j 0)) since then acl2 would only apply the rule if
; it can prove that j is not 0.  It is OK to apply this rule even is j
; may be 0 as long as the formula is simplified.  Perhaps a
; :definition rule would work too, I have not tried that.

(defthm ith-sum-0
  (implies (and (syntaxp (not (and (equal j (list 'quote 0)))))
		(naturalp i) (naturalp j) (<= j (+ 1 i (- (len b)))))
	   (equal (ith-sum a b i j) (ith-sum a b i 0)))
  :hints (("Goal" :in-theory nil :use
	   (ith-sum-0-lemma (:instance ith-sum-0-lemma (j 0))))))

; With that lemma, we can proove that the two loops are really the same

(defthm forloop-is-forloop-int
  (implies (and (word-listp a) (word-listp b) (wordp i) (wordp n) (dwordp sum))
	   (equal (int-value (long-mult-forloop a b n i sum))
		  (long-mult-forloop-int a b n i sum)))
  :hints (("Goal" :do-not generalize :in-theory
	   (disable long-mult-ith-word ith-sum mv-nth mod-bounds mod-type
		    mod-x-y-=-x+y mod-x-y-=-x floor-=-x/y floor-type-4))))

; Now we wold like to rewrite the forloop using the following simpler
; function:

(defun sum-ith-sum (a b n i)
  (declare (xargs :measure (nfix (- n i))))
  (if (zp (- n i)) 0
    (+ (ith-sum a b i 0)
       (* *wmod* (sum-ith-sum a b n (+ 1 i))))))

(defthm sum-ith-sum-naturalp
  (implies (and (word-listp a) (word-listp b))
	   (naturalp (sum-ith-sum a b n i)))
  :rule-classes :type-prescription)

; The forloop really calculates (sum-ith-sum a b n i) + sum modulo
; 2^32n ACL2 has a built-int expt function to calculate a^b, but it
; has a set of rules associated with it, which we do not need, and
; actually it makes our proof more difficult, so we define out own exp
; function:

(defun my-exp (m n)
  (if (zp n) 1
    (* m (my-exp m (1- n)))))

(defthm my-exp-integerp
  (implies (integerp m) (integerp (my-exp m n)))
  :rule-classes :type-prescription)

(defthm my-exp-rationalp
  (implies (rationalp m) (rationalp (my-exp m n)))
  :rule-classes :type-prescription)

(defthm my-exp-positive
  (implies (and (rationalp m) (< 0 m))
	   (< 0 (my-exp m n)))
  :rule-classes ((:type-prescription) (:linear)))

; And my-exp is really the same as expt:

(defthm my-exp-is-expt
  (implies (naturalp n) (equal (my-exp m n) (expt m n))))

(in-theory (disable my-exp-is-expt))

; And this is the expression of the forloop with sum-ith-sum:

(defthm forloop-int-thm
  (implies (and (word-listp a) (word-listp b) (acl2-numberp i)
		(acl2-numberp n) (integerp sum))
	   (equal (long-mult-forloop-int a b n i sum)
		  (mod (+ sum (sum-ith-sum a b n i))
		       (my-exp *wmod* (nfix (+ n (- i)))))))
  :hints (("Goal" :do-not generalize :in-theory
	   (disable ith-sum ith-sum-range floor-bounds floor-type-4))))

; Now all we need to do is reason about sum-ith-sum.  The problem is
; that sum-th-sum can only be rewritten using multiplication if its
; last argument, i=0.  This means that we do not have a good invariant
; for the sum-ith-sum recursion.  To solve this problem, we will again
; find an alternative definition for sum-ith-sum that use a recursion
; with a good invariant.  To do that, we will define sum-ith-sum by a
; recursion that decomposes the list arguments.  This is the goal in
; the following list of lemmas.

; First we deal with ith-sum, we find a set of rules that allows us to
; disable the original definition.

(defthm ith-sum-i<j
  (implies (and (naturalp i) (integerp j) (< i j))
	   (equal (ith-sum a b i j) 0)))

(defthm ith-sum-i-i
  (implies (naturalp i)
	   (equal (ith-sum a b i i)
		  (* (my-nth i a) (my-nth 0 b)))))

(defthm ith-sum-cons
  (implies (and (naturalp i) (naturalp j) (< 0 i) (<= j i))
	   (equal (ith-sum a (cons b c) i j)
		  (+ (* (my-nth i a) b)
		     (ith-sum a c (- i 1) j)))))

(in-theory (disable ith-sum))

; Now we want to do similar things to sum-ith-sum

(defthm sum-ith-sum-nil
  (implies (atom x)
	   (and (equal (sum-ith-sum x a n i) 0)
		(equal (sum-ith-sum a x n i) 0))))

(defthm sum-ith-sum-0
  (implies (<= n i) (equal (sum-ith-sum a b n i) 0)))

(defun ith-simple-mul-sum (a b i)
  (declare (xargs :measure (nfix (- (len a) i))))
  (if (and (integerp i) (< i (len a)))
      (+ (* (my-nth i a) b) (* *wmod* (ith-simple-mul-sum a b (+ 1 i))))
    0))

(defmacro all-ith-sum (a b i)
  `(sum-ith-sum ,a ,b (+ -1 (len ,a) (len ,b)) ,i))

(defthm sum-ith-sum-single-lemma
  (implies (naturalp i)
	   (equal (sum-ith-sum a (list b) (len a) i)
		  (+ (* (my-nth i a) b)
		     (* *wmod* (sum-ith-sum a (list b) (len a) (+ 1 i))))))
  :rule-classes nil)

(defthm sum-ith-sum-single
  (implies (naturalp i)
	   (equal (sum-ith-sum a (list b) (len a) i)
		  (ith-simple-mul-sum a b i)))
  :hints (("Subgoal *1/3'" :use sum-ith-sum-single-lemma)))

(defthm sum-ith-sum-consp-lemma
  (implies (and	(naturalp i) (< 0 i))
	   (equal (all-ith-sum a (cons b c) i)
		  (+ (all-ith-sum a (list b) i)
		     (all-ith-sum a c (- i 1)))))
  :hints (("Goal" :do-not generalize :in-theory (disable sum-ith-sum-single)
	   :induct (all-ith-sum a (cons b c) i)))
  :rule-classes nil)

(defthm sum-ith-sum-consp-positive
  (implies (and (consp b) (naturalp i) (< 0 i))
	   (equal (all-ith-sum a b i)
		  (+ (ith-simple-mul-sum a (car b) i)
		     (all-ith-sum a (cdr b) (- i 1)))))
  :hints (("Goal" :use ((:instance sum-ith-sum-consp-lemma
				   (b (car b)) (c (cdr b))))))
  :rule-classes nil)

(defthm sum-ith-sum-consp
  (implies (consp b)
	   (equal (all-ith-sum a b 0)
		  (+ (ith-simple-mul-sum a (car b) 0)
		     (* *wmod* (all-ith-sum a (cdr b) 0)))))
  :hints (("Goal" :use ((:instance sum-ith-sum-consp-positive (i 1)))))
  :rule-classes nil)

(defthm cdr-ith-simple-mul-sum
  (implies (and (consp a) (naturalp i))
	   (equal (ith-simple-mul-sum a b i)
		  (+ (* (my-nth i a) b)
		     (* *wmod* (ith-simple-mul-sum (cdr a) b i)))))
  :hints (("Goal" :do-not generalize)))

; Now attack the goal

(defthm simple-mul-sum-is-mul
  (equal (ith-simple-mul-sum a b 0) (* (int-value a) b)))

; This is almost what we need.

(defthm all-ith-sum-is-mul
  (equal (all-ith-sum a b 0) (* (int-value a) (int-value b)))
  :hints (("Goal" :in-theory (disable sum-ith-sum)
	   :do-not generalize :induct (int-value b))
	  ("Subgoal *1/1" :use sum-ith-sum-consp)))

(defthm sum-ith-sum-big-i
  (implies (and (integerp i) (< (+ -1 (len a) (len b)) i))
	   (equal (sum-ith-sum a b n i) 0)))

(defthm sum-ith-sum-big-n
  (implies (and (naturalp n) (naturalp i) (< (+ -1 (len a) (len b)) n))
	   (equal (sum-ith-sum a b n i)
		  (all-ith-sum a b i))))

(defthm sum-ith-sum-altdef
  (implies (and (naturalp i) (integerp n) (< i n))
	   (equal (sum-ith-sum a b n i)
		  (+ (* (my-exp *wmod* (+ -1 n (- i))) (ith-sum a b (1- n) 0))
		     (sum-ith-sum a b (1- n) i)))))

(in-theory (disable sum-ith-sum))

(defun zp-induction (x)
  (if (zp x) x (zp-induction (- x 1))))

(defthm sum-ith-sum-plus
  (implies (and (naturalp n) (naturalp j))
	   (equal (sum-ith-sum a b (+ j n) 0)
		  (+ (* (my-exp *wmod* n) (sum-ith-sum a b (+ j n) n))
		     (sum-ith-sum a b n 0))))
  :hints (("Goal''" :do-not generalize :induct (zp-induction j)
	   :in-theory (enable my-exp-is-expt)))
  :rule-classes nil)

(defthm sum-ith-sum-mod-lemma1
  (implies (and (word-listp a) (word-listp b) (integerp n)
		(<= 0 n) (< n (+ -1 (len a) (len b))))
	   (equal (mod (sum-ith-sum a b n 0)
		       (my-exp *wmod* n))
		  (mod (+ (sum-ith-sum a b n 0)
			  (* (my-exp *wmod* n)
			     (sum-ith-sum a b (+ -1 (len a) (len b))
					  n)))
		       (my-exp *wmod* n))))
  :rule-classes nil)

(defthm sum-ith-sum-mod-lemma2
  (implies (and (word-listp a) (word-listp b) (naturalp n)
		(< n (+ -1 (len a) (len b))))
	   (equal (mod (sum-ith-sum a b n 0) (my-exp *wmod* n))
		  (mod (all-ith-sum a b 0) (my-exp *wmod* n))))
  :hints (("Goal" :do-not generalize :do-not-induct t
	   :in-theory (disable all-ith-sum-is-mul sum-ith-sum-altdef)
	   :use ((:instance sum-ith-sum-plus
			    (j (+ -1 (- n) (len a) (len b))))))
	  ("Subgoal 1''" :use sum-ith-sum-mod-lemma1)))

(defthm sum-ith-sum-mod
  (implies (and (word-listp a) (word-listp b) (naturalp n))
	   (equal (mod (sum-ith-sum a b n 0) (my-exp *wmod* n))
		  (mod (all-ith-sum a b 0) (my-exp *wmod* n))))
  :hints (("Goal" :do-not generalize :do-not-induct t
	   :in-theory (disable all-ith-sum-is-mul)
	   :cases ((< n (+ -1 (len a) (len b)))
		   (> n (+ -1 (len a) (len b)))
		   (= n (+ -1 (len a) (len b)))))))

; And finally, here is the program proven correct:

(defthm multiple-correct
  (implies (and (word-listp a) (word-listp b) (wordp n))
	   (equal (int-value (long-mult-forloop a b n 0 0))
		  (mod (* (int-value a) (int-value b))
		       (my-exp *wmod* (nfix n)))))
  :hints (("Goal" :do-not generalize :do-not-induct t)))