		Search-engine friendly clone of the ACL2 documentation.

Field-arithmetic-operations

Op-field-square-root

Leo field square-root operation.

Signature
(op-field-square-root arg curve) → result
Arguments: arg — Guard (valuep arg).; curve — Guard (curvep curve).
Returns: result — Type (value-resultp result).

If the argument has a modular square root in the field, then the larger of the square roots is returned. Returns zero if the argument is a quadradic non-residue.

Definitions and Theorems

Function: op-field-square-root

(defun op-field-square-root (arg curve)
  (declare (xargs :guard (and (valuep arg) (curvep curve))))
  (declare (xargs :guard (value-case arg :field)))
  (let ((__function__ 'op-field-square-root))
    (declare (ignorable __function__))
    (b* ((err (list :op-field-square-root (value-fix arg)))
         (p (curve-base-prime curve))
         (x (value-field->get arg))
         ((unless (pfield::fep x p))
          (reserrf err))
         ((when (or (<= p 11)
                    (primes::has-square-root? 11 p)))
          (reserrf err))
         (sqrt (primes::tonelli-shanks-greater-sqrt x p 11))
         ((unless (pfield::fep sqrt p))
          (reserrf err)))
      (value-field sqrt))))

Theorem: value-resultp-of-op-field-square-root

(defthm value-resultp-of-op-field-square-root
  (b* ((result (op-field-square-root arg curve)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-field-square-root-of-value-fix-arg

(defthm op-field-square-root-of-value-fix-arg
  (equal (op-field-square-root (value-fix arg)
                               curve)
         (op-field-square-root arg curve)))

Theorem: op-field-square-root-value-equiv-congruence-on-arg

(defthm op-field-square-root-value-equiv-congruence-on-arg
  (implies (value-equiv arg arg-equiv)
           (equal (op-field-square-root arg curve)
                  (op-field-square-root arg-equiv curve)))
  :rule-classes :congruence)

Theorem: op-field-square-root-of-curve-fix-curve

(defthm op-field-square-root-of-curve-fix-curve
  (equal (op-field-square-root arg (curve-fix curve))
         (op-field-square-root arg curve)))

Theorem: op-field-square-root-curve-equiv-congruence-on-curve

(defthm op-field-square-root-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (op-field-square-root arg curve)
                  (op-field-square-root arg curve-equiv)))
  :rule-classes :congruence)