		Search-engine friendly clone of the ACL2 documentation.

Literal-evaluation

Eval-group-literal

Evaluate a Leo group element literal.

Signature
(eval-group-literal lit curve) → result
Arguments: lit — Guard (group-literalp lit).; curve — Guard (curvep curve).
Returns: result — Type (value-optionp result).

For now we only formalize the evaluation of pairs with explicit coordinates and scalar multiplications of the generator. We will add derivation of coordinates later; for now we return nil on pairs with derived coordinates, where in this case nil does not indicate error but lack of support. (We should probably differentiate these two kinds of errors eventually.)

Like the group arithmetic operations depend on an elliptic curve, so does the evaluation of group element literals.

For a pair (with explicit coordinates), we ensure that the point is in the subgroup; otherwise, we return nil as a defensive error indication. For a scalar multiplication of the generator, we know that the point is on the curve because the generator is, but for now we do not have a proof readily available yet, and thus we perform the check.

Definitions and Theorems

Function: eval-group-literal

(defun eval-group-literal (lit curve)
  (declare (xargs :guard (and (group-literalp lit)
                              (curvep curve))))
  (let ((__function__ 'eval-group-literal))
    (declare (ignorable __function__))
    (group-literal-case
         lit :affine
         (if (and (coordinate-case lit.x :explicit)
                  (coordinate-case lit.y :explicit))
             (b* ((p (curve-base-prime curve))
                  (x (mod (coordinate-explicit->get lit.x)
                          p))
                  (y (mod (coordinate-explicit->get lit.y)
                          p))
                  (point (ecurve::point-finite x y)))
               (and (curve-subgroupp point curve)
                    (value-group point)))
           nil)
         :product
         (b* ((gen (curve-generator curve))
              (k (mod lit.factor (curve-scalar-prime curve)))
              ((mv okp point)
               (curve-subgroup-mul k gen curve))
              ((unless okp) nil))
           (value-group point)))))

Theorem: value-optionp-of-eval-group-literal

(defthm value-optionp-of-eval-group-literal
  (b* ((result (eval-group-literal lit curve)))
    (value-optionp result))
  :rule-classes :rewrite)

Theorem: eval-group-literal-of-group-literal-fix-lit

(defthm eval-group-literal-of-group-literal-fix-lit
  (equal (eval-group-literal (group-literal-fix lit)
                             curve)
         (eval-group-literal lit curve)))

Theorem: eval-group-literal-group-literal-equiv-congruence-on-lit

(defthm eval-group-literal-group-literal-equiv-congruence-on-lit
  (implies (group-literal-equiv lit lit-equiv)
           (equal (eval-group-literal lit curve)
                  (eval-group-literal lit-equiv curve)))
  :rule-classes :congruence)

Theorem: eval-group-literal-of-curve-fix-curve

(defthm eval-group-literal-of-curve-fix-curve
  (equal (eval-group-literal lit (curve-fix curve))
         (eval-group-literal lit curve)))

Theorem: eval-group-literal-curve-equiv-congruence-on-curve

(defthm eval-group-literal-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (eval-group-literal lit curve)
                  (eval-group-literal lit curve-equiv)))
  :rule-classes :congruence)