		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen-enc

Encode a window of 4 bits.

Signature
(pedersen-enc 4bits) → i
Arguments: 4bits — Guard (bit-listp 4bits).
Returns: i — Type (integerp i), given (bit-listp 4bits).

This is the function \mathit{enc} in [IS], while in [ES] it is part of the double summation.

There is a discrepancy between [ES] and [IS] in the treatment of the fourth bit: [ES] maps 0 to 1 and 1 to -1, while [IS] maps 0 to -1 and 1 to 1. The Circom code in the Semaphore repository is consistent with [ES], so we follow [ES] here.

There is also a discrepancy between [ES] and [IS] in the treatment of the other three bits: [IS] adds 1 to their weighted sum, while [ES] does not. The Circom code in the Semaphore repository is consistent with [IS], and we have confirmed with the authors of Semaphore that the sum must include the 1 addend and that [IS] should be fixed, which we have done in Overleaf.

Definitions and Theorems

Function: pedersen-enc

(defun pedersen-enc (4bits)
  (declare (xargs :guard (bit-listp 4bits)))
  (declare (xargs :guard (= (len 4bits) 4)))
  (let ((acl2::__function__ 'pedersen-enc))
    (declare (ignorable acl2::__function__))
    (b* ((b0 (first 4bits))
         (b1 (second 4bits))
         (b2 (third 4bits))
         (b3 (fourth 4bits)))
      (* (if (= b3 0) 1 -1)
         (+ 1 b0 (* 2 b1) (* 4 b2))))))

Theorem: integerp-of-pedersen-enc

(defthm integerp-of-pedersen-enc
  (implies (bit-listp 4bits)
           (b* ((i (pedersen-enc 4bits)))
             (integerp i)))
  :rule-classes :rewrite)