		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen-point

The function \mathsf{PedersenHashToPoint} [ZPS:5.4.1.7].

Signature
(pedersen-point d m) → point?
Arguments: d — Guard (byte-listp d).; m — Guard (bit-listp m).
Returns: point? — Type (maybe-jubjub-pointp point?).

Definitions and Theorems

Function: pedersen-point-loop

(defun pedersen-point-loop (i d m1)
 (declare (xargs :guard (and (posp i)
                             (byte-listp d)
                             (bit-listp m1))))
 (declare (xargs :guard (and (= (len d) 8)
                             (integerp (/ (len m1) 3)))))
 (let ((__function__ 'pedersen-point-loop))
   (declare (ignorable __function__))
   (b*
    (((when (<= (len m1) (* 3 *pedersen-c*)))
      (pedersen-segment-addend d m1 i))
     (point1 (pedersen-segment-addend d (take (* 3 *pedersen-c*) m1)
                                      i))
     ((unless (jubjub-pointp point1)) nil)
     (point2 (pedersen-point-loop (1+ i)
                                  d (nthcdr (* 3 *pedersen-c*) m1)))
     ((unless (jubjub-pointp point2)) nil))
    (jubjub-add point1 point2))))

Theorem: maybe-jubjub-pointp-of-pedersen-point-loop

(defthm maybe-jubjub-pointp-of-pedersen-point-loop
  (b* ((point? (pedersen-point-loop i d m1)))
    (maybe-jubjub-pointp point?))
  :rule-classes :rewrite)

Function: pedersen-point

(defun pedersen-point (d m)
  (declare (xargs :guard (and (byte-listp d) (bit-listp m))))
  (declare (xargs :guard (and (= (len d) 8) (consp m))))
  (let ((__function__ 'pedersen-point))
    (declare (ignorable __function__))
    (b* ((m1 (pedersen-pad m)))
      (pedersen-point-loop 1 d m1))))

Theorem: maybe-jubjub-pointp-of-pedersen-point

(defthm maybe-jubjub-pointp-of-pedersen-point
  (b* ((point? (pedersen-point d m)))
    (maybe-jubjub-pointp point?))
  :rule-classes :rewrite)