		Search-engine friendly clone of the ACL2 documentation.

Twisted-edwards-curve

Make-twisted-edwards-curve

Basic constructor macro for twisted-edwards-curve structures.

Syntax

(make-twisted-edwards-curve [:p <p>] 
                            [:a <a>] 
                            [:d <d>])

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

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

Definition

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

Macro: make-twisted-edwards-curve

(defmacro make-twisted-edwards-curve (&rest args)
  (std::make-aggregate 'twisted-edwards-curve
                       args '((:p) (:a) (:d))
                       'make-twisted-edwards-curve
                       nil))

Function: twisted-edwards-curve

(defun twisted-edwards-curve (p a d)
  (declare (xargs :guard (natp p)))
  (declare (xargs :guard (and (dm::primep p)
                              (> p 2)
                              (fep a p)
                              (fep d p)
                              (not (equal a d))
                              (not (equal a 0))
                              (not (equal d 0)))))
  (let ((acl2::__function__ 'twisted-edwards-curve))
    (declare (ignorable acl2::__function__))
    (b* ((p (mbe :logic (nfix p) :exec p)))
      (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)
                             (fep d p)
                             (not (equal a d))
                             (not (equal a 0))
                             (not (equal d 0)))
                        a
                      1)
                    :exec a))
            (d (mbe :logic
                    (if (and (dm::primep p)
                             (> p 2)
                             (fep a p)
                             (fep d p)
                             (not (equal a d))
                             (not (equal a 0))
                             (not (equal d 0)))
                        d
                      2)
                    :exec d)))
        (list (cons 'p p)
              (cons 'a a)
              (cons 'd d))))))