		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen

Point resulting from the Pedersen hash.

Signature
(pedersen m) → hash
Arguments: m — Guard (bit-listp m).
Returns: hash — Type (baby-jubjub-pointp hash).

We pad the message if needed, and then we go through each segment and add the addend points together.

Definitions and Theorems

Function: pedersen-loop

(defun pedersen-loop (i m)
  (declare (xargs :guard (and (natp i) (bit-listp m))))
  (declare (xargs :guard (integerp (/ (len m) 4))))
  (let ((acl2::__function__ 'pedersen-loop))
    (declare (ignorable acl2::__function__))
    (b* (((when (<= (len m) 200))
          (pedersen-addend m i))
         (point1 (pedersen-addend (take 200 m) i))
         (point2 (pedersen-loop (1+ i) (nthcdr 200 m))))
      (baby-jubjub-add point1 point2))))

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

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

Function: pedersen

(defun pedersen (m)
  (declare (xargs :guard (bit-listp m)))
  (let ((acl2::__function__ 'pedersen))
    (declare (ignorable acl2::__function__))
    (b* ((m1 (pedersen-pad m)))
      (pedersen-loop 0 m1))))

Theorem: baby-jubjub-pointp-of-pedersen

(defthm baby-jubjub-pointp-of-pedersen
  (b* ((hash (pedersen m)))
    (baby-jubjub-pointp hash))
  :rule-classes :rewrite)