		Search-engine friendly clone of the ACL2 documentation.

Montgomery-curve

Montgomery-curve->a

Get the a field from a montgomery-curve.

Signature
(montgomery-curve->a x) → fty::x.name
Arguments: x — Guard (montgomery-curvep x).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: montgomery-curve->a$inline

(defun montgomery-curve->a$inline (x)
  (declare (xargs :guard (montgomery-curvep x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'montgomery-curve->a))
    (declare (ignorable acl2::__function__))
    (mbe :logic
         (b* ((x (and t x))
              (p (cdr (std::da-nth 0 x)))
              (a (cdr (std::da-nth 1 x)))
              (b (cdr (std::da-nth 2 x))))
           (if (and (dm::primep p)
                    (> p 2)
                    (fep a p)
                    (not (equal a 2))
                    (not (equal a (mod -2 p))))
               a
             0))
         :exec (cdr (std::da-nth 1 x)))))

Theorem: montgomery-curve->a$inline-of-montgomery-curve-fix-x

(defthm montgomery-curve->a$inline-of-montgomery-curve-fix-x
  (equal (montgomery-curve->a$inline (montgomery-curve-fix x))
         (montgomery-curve->a$inline x)))

Theorem: montgomery-curve->a$inline-montgomery-curve-equiv-congruence-on-x

(defthm
  montgomery-curve->a$inline-montgomery-curve-equiv-congruence-on-x
  (implies (montgomery-curve-equiv x x-equiv)
           (equal (montgomery-curve->a$inline x)
                  (montgomery-curve->a$inline x-equiv)))
  :rule-classes :congruence)