# 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)