		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen-segment-addend

The addend point in the definition of \mathsf{PedersenHashToPoint} [ZPS:5.4.1.7].

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

This is [\langle{M_i}\rangle]\mathcal{I}_i^D.

Definitions and Theorems

Function: pedersen-segment-addend

(defun pedersen-segment-addend (d segment i)
  (declare (xargs :guard (and (byte-listp d)
                              (bit-listp segment)
                              (posp i))))
  (declare (xargs :guard (and (= (len d) 8)
                              (integerp (/ (len segment) 3)))))
  (let ((__function__ 'pedersen-segment-addend))
    (declare (ignorable __function__))
    (b* ((ipoint (pedersen-segment-point d i))
         ((unless (jubjub-pointp ipoint)) nil)
         (scalar (pedersen-segment-scalar segment)))
      (jubjub-mul scalar ipoint))))

Theorem: maybe-jubjub-pointp-of-pedersen-segment-addend

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