		Search-engine friendly clone of the ACL2 documentation.

Group-arithmetic-operations

Op-group-sub

Leo group addition operation.

Signature
(op-group-sub left right curve) → result
Arguments: left — Guard (valuep left).; right — Guard (valuep right).; curve — Guard (curvep curve).
Returns: result — Type (value-resultp result).

Definitions and Theorems

Function: op-group-sub

(defun op-group-sub (left right curve)
  (declare (xargs :guard (and (valuep left)
                              (valuep right)
                              (curvep curve))))
  (declare (xargs :guard (and (value-case left :group)
                              (value-case right :group))))
  (let ((__function__ 'op-group-sub))
    (declare (ignorable __function__))
    (b* ((x (value-group->get left))
         (y (value-group->get right))
         ((unless (curve-subgroupp x curve))
          (reserrf (list :input-not-in-subgroup x)))
         ((unless (curve-subgroupp y curve))
          (reserrf (list :input-not-in-subgroup y)))
         ((mv okp -y)
          (curve-subgroup-neg y curve))
         ((unless okp)
          (reserrf (list :intermediate-not-in-subgroup -y)))
         ((mv okp x-y)
          (curve-subgroup-add x -y curve))
         ((unless okp)
          (reserrf (list :output-not-in-subgroup x-y))))
      (value-group x-y))))

Theorem: value-resultp-of-op-group-sub

(defthm value-resultp-of-op-group-sub
  (b* ((result (op-group-sub left right curve)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: op-group-sub-of-value-fix-left

(defthm op-group-sub-of-value-fix-left
  (equal (op-group-sub (value-fix left)
                       right curve)
         (op-group-sub left right curve)))

Theorem: op-group-sub-value-equiv-congruence-on-left

(defthm op-group-sub-value-equiv-congruence-on-left
  (implies (value-equiv left left-equiv)
           (equal (op-group-sub left right curve)
                  (op-group-sub left-equiv right curve)))
  :rule-classes :congruence)

Theorem: op-group-sub-of-value-fix-right

(defthm op-group-sub-of-value-fix-right
  (equal (op-group-sub left (value-fix right)
                       curve)
         (op-group-sub left right curve)))

Theorem: op-group-sub-value-equiv-congruence-on-right

(defthm op-group-sub-value-equiv-congruence-on-right
  (implies (value-equiv right right-equiv)
           (equal (op-group-sub left right curve)
                  (op-group-sub left right-equiv curve)))
  :rule-classes :congruence)

Theorem: op-group-sub-of-curve-fix-curve

(defthm op-group-sub-of-curve-fix-curve
  (equal (op-group-sub left right (curve-fix curve))
         (op-group-sub left right curve)))

Theorem: op-group-sub-curve-equiv-congruence-on-curve

(defthm op-group-sub-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (op-group-sub left right curve)
                  (op-group-sub left right curve-equiv)))
  :rule-classes :congruence)