		Search-engine friendly clone of the ACL2 documentation.

Twisted-edwards

Twisted-edwards-compress

Turn a point on a twisted Edwards curve into compressed form.

Signature
(twisted-edwards-compress point curve) → (mv p y)
Arguments: point — Guard (pointp point).; curve — Guard (twisted-edwards-curvep curve).
Returns: p — Type (bitp p).; y — Type (natp y).

This is based on Appendix A.3.3.2 of the Zcash Protocol Specification (Version 2020.1.15), but quite likely it is much more general than not only Zcash, but also twisted Edwards curves.

The compression consists in keeping the whole y coordinate but only the lowest bit (i.e. the parity) of the x coordinate. This, together with the information that the point is on the curve, should suffice to reconstruct the full x coordinate. Eventually we should prove this, and define a decompression function.

Definitions and Theorems

Theorem: returns-lemma

(defthm returns-lemma
  (implies (and (natp x) (not (equal (mod x 2) 0)))
           (equal (mod x 2) 1)))

Function: twisted-edwards-compress

(defun twisted-edwards-compress (point curve)
  (declare (xargs :guard (and (pointp point)
                              (twisted-edwards-curvep curve))))
  (declare (ignore curve))
  (declare (xargs :guard (point-on-twisted-edwards-p point curve)))
  (let ((acl2::__function__ 'twisted-edwards-compress))
    (declare (ignorable acl2::__function__))
    (mv (mod (point-finite->x point) 2)
        (point-finite->y point))))

Theorem: bitp-of-twisted-edwards-compress.p

(defthm bitp-of-twisted-edwards-compress.p
  (b* (((mv ?p ?y)
        (twisted-edwards-compress point curve)))
    (bitp p))
  :rule-classes :rewrite)

Theorem: natp-of-twisted-edwards-compress.y

(defthm natp-of-twisted-edwards-compress.y
  (b* (((mv ?p ?y)
        (twisted-edwards-compress point curve)))
    (natp y))
  :rule-classes :rewrite)

Theorem: twisted-edwards-compress-of-point-fix-point

(defthm twisted-edwards-compress-of-point-fix-point
  (equal (twisted-edwards-compress (point-fix point)
                                   curve)
         (twisted-edwards-compress point curve)))

Theorem: twisted-edwards-compress-point-equiv-congruence-on-point

(defthm twisted-edwards-compress-point-equiv-congruence-on-point
  (implies (point-equiv point point-equiv)
           (equal (twisted-edwards-compress point curve)
                  (twisted-edwards-compress point-equiv curve)))
  :rule-classes :congruence)

Theorem: twisted-edwards-compress-of-twisted-edwards-curve-fix-curve

(defthm twisted-edwards-compress-of-twisted-edwards-curve-fix-curve
 (equal
  (twisted-edwards-compress point (twisted-edwards-curve-fix curve))
  (twisted-edwards-compress point curve)))

Theorem: twisted-edwards-compress-twisted-edwards-curve-equiv-congruence-on-curve

(defthm
 twisted-edwards-compress-twisted-edwards-curve-equiv-congruence-on-curve
 (implies (twisted-edwards-curve-equiv curve curve-equiv)
          (equal (twisted-edwards-compress point curve)
                 (twisted-edwards-compress point curve-equiv)))
 :rule-classes :congruence)