		Search-engine friendly clone of the ACL2 documentation.

Curve-parameterization

Curve-subgroup-add

Addition in the subgroup.

Signature
(curve-subgroup-add x y curve) → (mv okp x+y)
Arguments: x — Guard (curve-subgroupp x curve).; y — Guard (curve-subgroupp y curve).; curve — Guard (curvep curve).
Returns: okp — Type (booleanp okp).; x+y — Type (curve-subgroupp x+y curve).

This is the same as addition in the curve group, but it has the property that adding two subgroup elements yields a subgroup element. We plan to prove that, but for now we check that here, returning an indication of failure as the first result and the neutral point as second result; otherwise, the first result indicates success and the second result is the sum. This function should never return nil as first result; when we prove that it is the case, we will eliminate the first result.

Definitions and Theorems

Function: curve-subgroup-add

(defun curve-subgroup-add (x y curve)
  (declare (xargs :guard (and (curvep curve)
                              (curve-subgroupp x curve)
                              (curve-subgroupp y curve))))
  (let ((__function__ 'curve-subgroup-add))
    (declare (ignorable __function__))
    (b* ((x (mbe :logic
                 (if (curve-subgroupp x curve)
                     x
                   (curve-zero curve))
                 :exec x))
         (y (mbe :logic
                 (if (curve-subgroupp y curve)
                     y
                   (curve-zero curve))
                 :exec y))
         (x+y (ecurve::edwards-bls12-add x y)))
      (if (curve-subgroupp x+y curve)
          (mv t x+y)
        (mv nil (curve-zero curve))))))

Theorem: booleanp-of-curve-subgroup-add.okp

(defthm booleanp-of-curve-subgroup-add.okp
  (b* (((mv ?okp ?x+y)
        (curve-subgroup-add x y curve)))
    (booleanp okp))
  :rule-classes :rewrite)

Theorem: return-type-of-curve-subgroup-add.x+y

(defthm return-type-of-curve-subgroup-add.x+y
  (b* (((mv ?okp ?x+y)
        (curve-subgroup-add x y curve)))
    (curve-subgroupp x+y curve))
  :rule-classes :rewrite)

Theorem: pointp-of-curve-subgroup-add.x+y

(defthm pointp-of-curve-subgroup-add.x+y
  (b* (((mv ?okp ?x+y)
        (curve-subgroup-add x y curve)))
    (pointp x+y))
  :rule-classes :rewrite)

Theorem: curve-subgroup-add-of-curve-fix-curve

(defthm curve-subgroup-add-of-curve-fix-curve
  (equal (curve-subgroup-add x y (curve-fix curve))
         (curve-subgroup-add x y curve)))

Theorem: curve-subgroup-add-curve-equiv-congruence-on-curve

(defthm curve-subgroup-add-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (curve-subgroup-add x y curve)
                  (curve-subgroup-add x y curve-equiv)))
  :rule-classes :congruence)