		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen-enc

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

Signature
(pedersen-enc 3bits) → enc
Arguments: 3bits — Guard (bit-listp 3bits).
Returns: enc — Type (integerp enc).

Definitions and Theorems

Function: pedersen-enc

(defun pedersen-enc (3bits)
  (declare (xargs :guard (bit-listp 3bits)))
  (declare (xargs :guard (= (len 3bits) 3)))
  (let ((__function__ 'pedersen-enc))
    (declare (ignorable __function__))
    (b* ((s0 (mbe :logic (bfix (first 3bits))
                  :exec (first 3bits)))
         (s1 (mbe :logic (bfix (second 3bits))
                  :exec (second 3bits)))
         (s2 (mbe :logic (bfix (third 3bits))
                  :exec (third 3bits))))
      (* (- 1 (* 2 s2)) (+ 1 s0 (* 2 s1))))))

Theorem: integerp-of-pedersen-enc

(defthm integerp-of-pedersen-enc
  (b* ((enc (pedersen-enc 3bits)))
    (integerp enc))
  :rule-classes (:type-prescription :rewrite))

Theorem: pedersen-enc-lower-bound

(defthm pedersen-enc-lower-bound
  (b* ((?enc (pedersen-enc 3bits)))
    (>= enc -4))
  :rule-classes :linear)

Theorem: pedersen-enc-upper-bound

(defthm pedersen-enc-upper-bound
  (b* ((?enc (pedersen-enc 3bits)))
    (<= enc 4))
  :rule-classes :linear)

Theorem: pedersen-enc-not-zero

(defthm pedersen-enc-not-zero
  (b* ((?enc (pedersen-enc 3bits)))
    (not (equal enc 0)))
  :rule-classes :type-prescription)

Theorem: pedersen-enc-injectivity

(defthm pedersen-enc-injectivity
  (implies (and (bit-listp x)
                (bit-listp y)
                (equal (len x) 3)
                (equal (len y) 3))
           (equal (equal (pedersen-enc x)
                         (pedersen-enc y))
                  (equal x y))))