		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen-generator

Generator points for Pedersen hash.

Signature
(pedersen-generator i) → point
Arguments: i — Guard (natp i).
Returns: point — Type (baby-jubjub-pointp point).

The scalars returned by pedersen-scalar are used to multiply a sequence of BabyJubjub points, and the resulting points are added up together. This is described by equation (1) in [IS], and by the double summation in [ES]. The points are denoted P_0,\ldots,P_l in [IS] and g_s in [ES]. These points are fixed for Semaphore, so they can be precomputed.

We have precomputed the points in pedersen-hash-base-points. The constant *pedersen-base-points-for-semaphore* lists them. Even though Pedersen hash should allow any number of points in general, for Semaphore we only need ten points (the ones in the list constant). The outer summation in [ES] goes from 0 to S-1, and Sleq10.

We define this function to return one of the ten points when the index is below 10, or the zero point otherwise. The index will always be below 10, when used in the Semaphore.

Definitions and Theorems

Function: pedersen-generator

(defun pedersen-generator (i)
  (declare (xargs :guard (natp i)))
  (let ((acl2::__function__ 'pedersen-generator))
    (declare (ignorable acl2::__function__))
    (b* ((i (nfix i)))
      (if (< i 10)
          (nth i *pedersen-base-points-for-semaphore*)
        (ecurve::twisted-edwards-zero)))))

Theorem: baby-jubjub-pointp-of-pedersen-generator

(defthm baby-jubjub-pointp-of-pedersen-generator
  (b* ((point (pedersen-generator i)))
    (baby-jubjub-pointp point))
  :rule-classes :rewrite)