		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen

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

Signature
(pedersen d m) → hash
Arguments: d — Guard (byte-listp d).; m — Guard (bit-listp m).
Returns: hash — Type (bit-listp hash).

We return nil if, instead of a point, an error is returned. This is distinguished from a valid hash, which is not empty.

Definitions and Theorems

Function: pedersen

(defun pedersen (d m)
  (declare (xargs :guard (and (byte-listp d) (bit-listp m))))
  (declare (xargs :guard (and (= (len d) 8) (consp m))))
  (let ((__function__ 'pedersen))
    (declare (ignorable __function__))
    (b* ((point (pedersen-point d m))
         ((unless (jubjub-pointp point)) nil))
      (coordinate-extract point))))

Theorem: bit-listp-of-pedersen

(defthm bit-listp-of-pedersen
  (b* ((hash (pedersen d m)))
    (bit-listp hash))
  :rule-classes :rewrite)