		Search-engine friendly clone of the ACL2 documentation.

Short-weierstrass

Make-short-weierstrass

Basic constructor macro for short-weierstrass structures.

Syntax

(make-short-weierstrass [:p <p>] 
                        [:a <a>] 
                        [:b <b>])

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

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

Definition

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

Macro: make-short-weierstrass

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

Function: short-weierstrass

(defun short-weierstrass (p a b)
 (declare (xargs :guard (and (natp p) (natp a) (natp b))))
 (declare
     (xargs :guard (and (> p 3)
                        (fep a p)
                        (fep b p)
                        (posp (mod (+ (* 4 a a a) (* 27 b b)) p)))))
 (let ((acl2::__function__ 'short-weierstrass))
  (declare (ignorable acl2::__function__))
  (b* ((p (mbe :logic (nfix p) :exec p))
       (a (mbe :logic (nfix a) :exec a))
       (b (mbe :logic (nfix b) :exec b)))
   (let ((p (mbe :logic
                 (if (and (> p 3)
                          (fep a p)
                          (fep b p)
                          (posp (mod (+ (* 4 a a a) (* 27 b b)) p)))
                     p
                   5)
                 :exec p))
         (a (mbe :logic
                 (if (and (> p 3)
                          (fep a p)
                          (fep b p)
                          (posp (mod (+ (* 4 a a a) (* 27 b b)) p)))
                     a
                   0)
                 :exec a))
         (b (mbe :logic
                 (if (and (> p 3)
                          (fep a p)
                          (fep b p)
                          (posp (mod (+ (* 4 a a a) (* 27 b b)) p)))
                     b
                   1)
                 :exec b)))
     (list (cons 'p p)
           (cons 'a a)
           (cons 'b b))))))