		Search-engine friendly clone of the ACL2 documentation.

Secp256k1-types

Secp256k1-point-to-bytes

Represent a secp256k1 point in compressed or uncompressed form.

Signature
(secp256k1-point-to-bytes point compressp) → bytes
Arguments: point — Guard (secp256k1-pointp point).; compressp — Guard (booleanp compressp).
Returns: bytes — Type (byte-listp bytes).

This is specified in Section 2.3.3 of SEC 1.

Definitions and Theorems

Function: secp256k1-point-to-bytes

(defun secp256k1-point-to-bytes (point compressp)
  (declare (xargs :guard (and (secp256k1-pointp point)
                              (booleanp compressp))))
  (b* (((secp256k1-point point) point))
    (cond ((secp256k1-point-infinityp point)
           (list 0))
          (compressp (cons (if (evenp point.y) 2 3)
                           (nat=>bebytes 32 point.x)))
          (t (cons 4
                   (append (nat=>bebytes 32 point.x)
                           (nat=>bebytes 32 point.y)))))))

Theorem: byte-listp-of-secp256k1-point-to-bytes

(defthm byte-listp-of-secp256k1-point-to-bytes
  (b* ((bytes (secp256k1-point-to-bytes point compressp)))
    (byte-listp bytes))
  :rule-classes :rewrite)

Theorem: len-of-secp256k1-point-to-bytes

(defthm len-of-secp256k1-point-to-bytes
  (equal (len (secp256k1-point-to-bytes point compressp))
         (cond ((secp256k1-point-infinityp point) 1)
               (compressp 33)
               (t 65))))

Theorem: secp256k1-point-to-bytes-of-secp256k1-point-fix-point

(defthm secp256k1-point-to-bytes-of-secp256k1-point-fix-point
  (equal (secp256k1-point-to-bytes (secp256k1-point-fix point)
                                   compressp)
         (secp256k1-point-to-bytes point compressp)))

Theorem: secp256k1-point-to-bytes-secp256k1-point-equiv-congruence-on-point

(defthm
 secp256k1-point-to-bytes-secp256k1-point-equiv-congruence-on-point
 (implies (secp256k1-point-equiv point point-equiv)
          (equal (secp256k1-point-to-bytes point compressp)
                 (secp256k1-point-to-bytes point-equiv compressp)))
 :rule-classes :congruence)

Theorem: secp256k1-point-to-bytes-of-bool-fix-compressp

(defthm secp256k1-point-to-bytes-of-bool-fix-compressp
  (equal (secp256k1-point-to-bytes point (bool-fix compressp))
         (secp256k1-point-to-bytes point compressp)))

Theorem: secp256k1-point-to-bytes-iff-congruence-on-compressp

(defthm secp256k1-point-to-bytes-iff-congruence-on-compressp
  (implies (iff compressp compressp-equiv)
           (equal (secp256k1-point-to-bytes point compressp)
                  (secp256k1-point-to-bytes point compressp-equiv)))
  :rule-classes :congruence)