Leo field inverse (reciprocal) operation.
(op-field-inv arg curve) → result
Function:
(defun op-field-inv (arg curve) (declare (xargs :guard (and (valuep arg) (curvep curve)))) (declare (xargs :guard (value-case arg :field))) (let ((__function__ 'op-field-inv)) (declare (ignorable __function__)) (b* ((err (list :op-field-inv (value-fix arg))) (p (curve-base-prime curve)) (x (value-field->get arg)) ((unless (pfield::fep x p)) (reserrf err)) ((when (= x 0)) (reserrf err))) (value-field (pfield::div 1 x p)))))
Theorem:
(defthm value-resultp-of-op-field-inv (b* ((result (op-field-inv arg curve))) (value-resultp result)) :rule-classes :rewrite)
Theorem:
(defthm op-field-inv-of-value-fix-arg (equal (op-field-inv (value-fix arg) curve) (op-field-inv arg curve)))
Theorem:
(defthm op-field-inv-value-equiv-congruence-on-arg (implies (value-equiv arg arg-equiv) (equal (op-field-inv arg curve) (op-field-inv arg-equiv curve))) :rule-classes :congruence)
Theorem:
(defthm op-field-inv-of-curve-fix-curve (equal (op-field-inv arg (curve-fix curve)) (op-field-inv arg curve)))
Theorem:
(defthm op-field-inv-curve-equiv-congruence-on-curve (implies (curve-equiv curve curve-equiv) (equal (op-field-inv arg curve) (op-field-inv arg curve-equiv))) :rule-classes :congruence)