Filtering...

pratt

books/projects/numbers/pratt
other
(in-package "DM")
other
(include-book "euclid")
other
(include-book "fermat")
other
(local (include-book "support/pratt"))
other
(defund fl
  (x)
  (declare (xargs :guard (real/rationalp x)))
  (floor x 1))
other
(set-enforce-redundancy t)
other
(set-inhibit-warnings "theory")
other
(local (in-theory nil))
find-orderfunction
(defun find-order
  (r k p)
  (declare (xargs :measure (nfix (- p k))))
  (if (or (zp k) (zp p) (>= k p))
    nil
    (if (= (mod-expt r k p) 1)
      k
      (find-order r (1+ k) p))))
orderfunction
(defun order
  (r p)
  (find-order r 1 p))
other
(defthmd order-bounds
  (implies (and (not (zp p)) (order r p))
    (and (not (zp (order r p)))
      (< (order r p) p))))
other
(defthmd order-1
  (implies (and (not (zp p)) (order r p))
    (equal (mod-expt r (order r p) p) 1)))
other
(defthmd order-minimal
  (implies (and (not (zp p))
      (order r p)
      (not (zp j))
      (< j (order r p)))
    (not (equal (mod-expt r j p) 1))))
other
(defthmd order-divides
  (implies (and (natp p)
      (> p 1)
      (natp r)
      (order r p)
      (natp m))
    (iff (equal (mod-expt r m p) 1)
      (divides (order r p) m))))
max-order-pfunction
(defun max-order-p
  (r p)
  (and (not (zp r))
    (< r p)
    (= (order r p) (1- p))))
mod-powersfunction
(defun mod-powers
  (r p n)
  (if (zp n)
    nil
    (cons (mod (expt r n) p)
      (mod-powers r p (1- n)))))
other
(defthmd powers-distinct
  (implies (and (natp p)
      (> p 1)
      (max-order-p r p)
      (natp m)
      (< m p))
    (distinct-positives (mod-powers r p m)
      (1- p))))
other
(defthmd perm-powers
  (implies (and (natp p)
      (> p 1)
      (max-order-p r p))
    (perm (positives (1- p))
      (mod-powers r p (1- p)))))
other
(defthmd divides-mod-power
  (implies (and (not (zp p))
      (not (zp q))
      (not (zp k))
      (divides q p))
    (divides q (mod (expt q k) p))))
other
(defthm max-order-p-prime
  (implies (and (not (zp p))
      (> p 1)
      (max-order-p r p))
    (primep p))
  :rule-classes nil)
fast-mod-expt-mulfunction
(defun fast-mod-expt-mul
  (b e n r)
  (if (zp e)
    r
    (if (zp (mod e 2))
      (fast-mod-expt-mul (mod (* b b) n)
        (fl (/ e 2))
        n
        r)
      (fast-mod-expt-mul (mod (* b b) n)
        (fl (/ e 2))
        n
        (mod (* r b) n)))))
fast-mod-exptfunction
(defun fast-mod-expt
  (b e n)
  (fast-mod-expt-mul b e n 1))
other
(defthm fast-mod-expt-rewrite
  (implies (and (natp b)
      (natp e)
      (not (zp n))
      (> n 1))
    (equal (fast-mod-expt b e n)
      (mod (expt b e) n))))
prod-powersfunction
(defun prod-powers
  (f e)
  (if (consp f)
    (* (expt (car f) (car e))
      (prod-powers (cdr f) (cdr e)))
    1))
distinct-factorsfunction
(defun distinct-factors
  (f)
  (if (consp f)
    (and (natp (car f))
      (> (car f) 1)
      (not (member (car f) (cdr f)))
      (distinct-factors (cdr f)))
    t))
all-positivefunction
(defun all-positive
  (e)
  (if (consp e)
    (and (not (zp (car e)))
      (all-positive (cdr e)))
    t))
factorizationfunction
(defun factorization
  (n f e)
  (and (distinct-factors f)
    (all-positive e)
    (= (len f) (len e))
    (= n (prod-powers f e))))
other
(defthm factor-divides
  (implies (and (factorization n f e)
      (member q f))
    (divides q n)))
all-primefunction
(defun all-prime
  (f)
  (if (consp f)
    (and (primep (car f)) (all-prime (cdr f)))
    t))
prime-factorizationfunction
(defun prime-factorization
  (n f e)
  (and (factorization n f e)
    (all-prime f)))
other
(defthmd all-prime-factors
  (implies (and (prime-factorization n f e)
      (primep q)
      (divides q n))
    (member q f)))
max-order-by-factorizationfunction
(defun max-order-by-factorization
  (r p f)
  (if (consp f)
    (and (not (= (mod-expt r (/ (1- p) (car f)) p) 1))
      (max-order-by-factorization r p (cdr f)))
    t))
other
(defthmd lucas
  (implies (and (natp p)
      (> p 1)
      (prime-factorization (1- p) f e)
      (not (zp r))
      (< r p)
      (= (mod-expt r (1- p) p) 1)
      (max-order-by-factorization r p f))
    (primep p)))
other
(defund fast-max-fact
  (r p f)
  (if (consp f)
    (and (not (= (fast-mod-expt r (/ (1- p) (car f)) p)
          1))
      (fast-max-fact r p (cdr f)))
    t))
other
(defthm fast-max-fact-rewrite
  (implies (and (natp r)
      (natp p)
      (> p 1)
      (factorization (1- p) f e))
    (equal (fast-max-fact r p f)
      (max-order-by-factorization r p f))))
find-prim-rootfunction
(defun find-prim-root
  (p f k)
  (declare (xargs :measure (nfix (- p k))))
  (if (and (not (zp p))
      (not (zp k))
      (< k p))
    (if (and (= (fast-mod-expt k (1- p) p) 1)
        (fast-max-fact k p f))
      k
      (find-prim-root p f (1+ k)))
    nil))
certificate-25519function
(defun certificate-25519
  nil
  '(2 (2 3
      65147
      74058212732561358302231226437062788676166966415465897661863160754340907)
    (2 1 1 1)
    (nil nil
      nil
      (2 (2 3
          353
          57467
          132049
          1923133
          31757755568855353
          75445702479781427272750846543864801)
        (1 1 1 1 1 1 1 1)
        (nil nil
          nil
          nil
          nil
          nil
          (10 (2 3 31 107 223 4153 430751)
            (3 1 1 1 1 1 1)
            (nil nil nil nil nil nil nil))
          (7 (2 3 5 75707 72106336199 1919519569386763)
            (5 2 2 1 1 1)
            (nil nil
              nil
              nil
              nil
              (2 (2 3 7 19 47 127 8574133)
                (1 1 1 1 2 1 1)
                (nil nil nil nil nil nil nil)))))))))
certify-primesfunction
(defun certify-primes
  (listp p c)
  (if listp
    (if (consp c)
      (and (consp p)
        (certify-primes nil (car p) (car c))
        (certify-primes t (cdr p) (cdr c)))
      (null p))
    (if (consp c)
      (let ((r (car c)) (f (cadr c))
          (e (caddr c))
          (c (cadddr c)))
        (and (natp p)
          (> p 1)
          (factorization (1- p) f e)
          (not (zp r))
          (< r p)
          (= (fast-mod-expt r (1- p) p) 1)
          (fast-max-fact r p f)
          (certify-primes t f c)))
      (primep p))))
certify-primefunction
(defun certify-prime
  (p c)
  (certify-primes nil p c))
other
(defthm certification-lemma
  (implies (certify-primes listp p c)
    (if listp
      (all-prime p)
      (primep p)))
  :rule-classes nil)
other
(defthmd certification-theorem
  (implies (certify-prime p c)
    (primep p)))
other
(defthmd primep-25519
  (primep (- (expt 2 255) 19))
  :hints (("Goal" :use (:instance certification-theorem
       (p (- (expt 2 255) 19))
       (c (certificate-25519))))))