		Search-engine friendly clone of the ACL2 documentation.

Montgomery-curve

Montgomery-curve->p

Get the p field from a montgomery-curve.

Signature
(montgomery-curve->p 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->p$inline

(defun montgomery-curve->p$inline (x)
  (declare (xargs :guard (montgomery-curvep x)))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'montgomery-curve->p))
    (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)) p 3))
         :exec (cdr (std::da-nth 0 x)))))

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

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

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

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