		Search-engine friendly clone of the ACL2 documentation.

Montgomery-curve

Make-montgomery-curve

Basic constructor macro for montgomery-curve structures.

Syntax

(make-montgomery-curve [:p <p>] 
                       [:a <a>] 
                       [:b <b>])

This is the usual way to construct montgomery-curve structures. It simply conses together a structure with the specified fields.

This macro generates a new montgomery-curve structure from scratch. See also change-montgomery-curve, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-montgomery-curve

(defmacro make-montgomery-curve (&rest args)
  (std::make-aggregate 'montgomery-curve
                       args '((:p) (:a) (:b))
                       'make-montgomery-curve
                       nil))

Function: montgomery-curve

(defun montgomery-curve (p a b)
  (declare (xargs :guard (and (dm::primep p)
                              (> p 2)
                              (fep a p)
                              (fep b p)
                              (not (equal a 2))
                              (not (equal a (mod -2 p)))
                              (not (equal b 0)))))
  (let ((acl2::__function__ 'montgomery-curve))
    (declare (ignorable acl2::__function__))
    (let ((p (mbe :logic (if (and (dm::primep p) (> p 2)) p 3)
                  :exec p))
          (a (mbe :logic
                  (if (and (dm::primep p)
                           (> p 2)
                           (fep a p)
                           (not (equal a 2))
                           (not (equal a (mod -2 p))))
                      a
                    0)
                  :exec a))
          (b (mbe :logic
                  (if (and (dm::primep p)
                           (fep b p)
                           (not (equal b 0)))
                      b
                    1)
                  :exec b)))
      (list (cons 'p p)
            (cons 'a a)
            (cons 'b b)))))