		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen-scalar

The function that maps each message segment to a scalar.

Signature
(pedersen-scalar segment) → i
Arguments: segment — Guard (bit-listp segment).
Returns: i — Type (integerp i), given (bit-listp segment).

This is the function that maps M_i to \langle M_i \rangle in [IS], while in [IS] it is part of the double summation. Each M_i is a segment, and the result is used in the scalar multiplication of a BabyJubjub curve point: this motivates the name of this ACL2 function.

This is a weighted sum of the encodings of the 4-bit windows (see pedersen-enc). The sum in [IS] appears to be off by one: it should end at k_i, not at k_i-1, otherwise it would ignore the last 4-bit window. The sum in [ES] is correct, because W is 50, but it neglects to accommodate the fact that the last segment may consist of less than 200 bits (i.e. less than 50 4-bit windows). Nonetheless, both issues are easily resolved and fixable: it is clear what our specification should say here.

Definitions and Theorems

Function: pedersen-scalar-loop

(defun pedersen-scalar-loop (w segment)
  (declare (xargs :guard (and (natp w) (bit-listp segment))))
  (declare (xargs :guard (integerp (/ (len segment) 4))))
  (let ((acl2::__function__ 'pedersen-scalar-loop))
    (declare (ignorable acl2::__function__))
    (if (consp segment)
        (+ (* (pedersen-enc (take 4 segment))
              (expt 2 (* 5 w)))
           (pedersen-scalar-loop (1+ w)
                                 (nthcdr 4 segment)))
      0)))

Theorem: integerp-of-pedersen-scalar-loop

(defthm integerp-of-pedersen-scalar-loop
  (implies (and (natp w) (bit-listp segment))
           (b* ((i (pedersen-scalar-loop w segment)))
             (integerp i)))
  :rule-classes :rewrite)

Function: pedersen-scalar

(defun pedersen-scalar (segment)
  (declare (xargs :guard (bit-listp segment)))
  (declare (xargs :guard (integerp (/ (len segment) 4))))
  (let ((acl2::__function__ 'pedersen-scalar))
    (declare (ignorable acl2::__function__))
    (pedersen-scalar-loop 0 segment)))

Theorem: integerp-of-pedersen-scalar

(defthm integerp-of-pedersen-scalar
  (implies (bit-listp segment)
           (b* ((i (pedersen-scalar segment)))
             (integerp i)))
  :rule-classes :rewrite)