mod-expt-fast - ACL2 Book

Included Books

top floor-mod

other

(in-package "ACL2")

local

(local (include-book "../bind-free/top"))

local

(local (include-book "floor-mod"))

local

(local (set-default-hints '((nonlinearp-default-hint stable-under-simplificationp
       hist
       pspv))))

local

(local (in-theory (e/d (ash-to-floor) (ash))))

local

(local (defthm mod-theorem-one
    (implies (and (rationalp a)
        (integerp b)
        (rationalp n)
        (not (equal n 0)))
      (equal (mod (* b (mod a n)) n) (mod (* a b) n)))))

local

(local (encapsulate nil
    (local (defun ind-fn
        (i)
        (if (zp i)
          t
          (ind-fn (+ -1 i)))))
    (local (scatter-exponents))
    (local (defthm mod-theorem-two-helper-helper
        (implies (and (not (zp i))
            (equal (mod (expt a i) n) (mod (expt (mod a n) i) n))
            (integerp a)
            (integerp b)
            (integerp n)
            (not (equal n 0)))
          (equal (mod (* b (expt (mod a n) i)) n)
            (mod (* b (expt a i)) n)))
        :hints (("Goal" :induct (ind-fn b)))))
    (local (defthm mod-theorem-two-helper
        (implies (and (not (zp i))
            (equal (mod (expt a i) n) (mod (expt (mod a n) i) n))
            (integerp a)
            (integerp n)
            (not (equal n 0)))
          (equal (mod (expt (mod a n) (+ 1 i)) n)
            (mod (expt a (+ 1 i)) n)))))
    (local (gather-exponents))
    (defthm mod-theorem-two
      (implies (and (integerp a)
          (integerp i)
          (<= 0 i)
          (integerp n)
          (not (equal n 0)))
        (equal (mod (expt (mod a n) i) n) (mod (expt a i) n)))
      :hints (("Goal" :induct (ind-fn i) :do-not '(generalize)) ("Subgoal *1/2''" :cases ((equal i 1)))
        ("Subgoal *1/2.2" :use (:instance mod-theorem-two-helper (i (+ -1 i)))
          :in-theory (disable mod-theorem-two-helper))))))

local

(local (defthm mod-theorem-three
    (implies (and (integerp a)
        (integerp i)
        (<= 0 i)
        (integerp n)
        (not (equal n 0))
        (integerp x))
      (equal (mod (* x (expt (mod a n) i)) n)
        (mod (* x (expt a i)) n)))
    :hints (("Goal" :use ((:instance mod-theorem-one (a (expt (mod a n) i)) (b x)) (:instance mod-theorem-one (a (expt a i)) (b x)))
       :in-theory (disable mod-theorem-one)))))

mod-expt-fast-1function

(defun mod-expt-fast-1
  (a i n acc)
  (declare (xargs :guard (and (integerp a)
        (natp i)
        (integerp n)
        (< 0 n)
        (integerp acc))))
  (if (zp i)
    acc
    (let ((floor-i-by-2 (ash i -1)))
      (if (oddp i)
        (mod-expt-fast-1 (mod (* a a) n)
          floor-i-by-2
          n
          (mod (* a acc) n))
        (mod-expt-fast-1 (mod (* a a) n) floor-i-by-2 n acc)))))

local

(local (defthm mod-expt-fast-1-as-mod-and-expt
    (implies (and (integerp a)
        (natp i)
        (integerp n)
        (< 0 n)
        (natp acc)
        (< acc n))
      (equal (mod-expt-fast-1 a i n acc)
        (mod (* acc (expt a i)) n)))))

mod-expt-fast-is-mod-expttheorem

(defthm mod-expt-fast-is-mod-expt
  (implies (and (integerp a) (natp i) (integerp n) (< 1 n))
    (equal (mod-expt-fast-1 a i n 1) (mod-expt a i n))))

mod-expt-fastfunction

(defun mod-expt-fast
  (a i n)
  (declare (xargs :guard (and (rationalp a)
        (integerp i)
        (not (and (eql a 0) (< i 0)))
        (<= 0 i)
        (rationalp n)
        (not (eql n 0)))))
  (mbe :exec (cond ((not (integerp a)) (mod (expt a i) n))
      ((and (integerp n) (< 1 n)) (mod-expt-fast-1 a i n 1))
      ((eql n 1) 0)
      (t (mod (expt a i) n)))
    :logic (mod (expt a i) n)))