		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen-addend

Addend point in the sum that yields the Pedersen hash.

Signature
(pedersen-addend segment i) → point
Arguments: segment — Guard (bit-listp segment).; i — Guard (natp i).
Returns: point — Type (baby-jubjub-pointp point).

This is the result of the scalar multiplication between the integer returned by pedersen-scalar and the generator point returned by pedersen-generator.

Definitions and Theorems

Function: pedersen-addend

(defun pedersen-addend (segment i)
  (declare (xargs :guard (and (bit-listp segment) (natp i))))
  (declare (xargs :guard (integerp (/ (len segment) 4))))
  (let ((acl2::__function__ 'pedersen-addend))
    (declare (ignorable acl2::__function__))
    (baby-jubjub-mul (pedersen-scalar segment)
                     (pedersen-generator i))))

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

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