mod-expt-fast - ACL2 Book

Included Books

top floor-mod-basic floor-mod more-floor-mod truncate-rem

other

(in-package "ACL2")

local

(local (include-book "../basic-ops/top"))

local

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

local

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

local

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

local

(local (include-book "truncate-rem"))

local

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

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)))))

mod-expt-fastfunction

(defun mod-expt-fast
  (a i n)
  (declare (xargs :guard (and (real/rationalp a)
        (integerp i)
        (not (and (eql a 0) (< i 0)))
        (<= 0 i)
        (real/rationalp n)
        (not (eql n 0)))))
  (if (and (integerp a) (integerp n) (< 0 n))
    (mod-expt-fast-1 a i n 1)
    (mod (expt a i) n)))

local

(local (defthm mod-expt-fast-is-mod-expt-helper
    (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 (real/rationalp a) (natp i) (integerp n) (< 1 n))
    (equal (mod-expt-fast a i n) (mod-expt a i n))))

in-theory

(in-theory (disable mod-expt-fast))