		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen-pad

Pedersen hash padding.

Signature
(pedersen-pad m) → m1
Arguments: m — Guard (bit-listp m).
Returns: m1 — Type (bit-listp m1), given (bit-listp m).

[IS] says that if the input message is not a multiple of 4 bits, it is padded with 1, 2, or 3 bits to turn it into a multiple of 4 bits. [ES] does not say anything about it, but it talks about 4-bit windows, thus perhaps leaving the padding implicit. [IS] says that the zero bits are appended, which suggests that they are added at the end.

Definitions and Theorems

Function: pedersen-pad

(defun pedersen-pad (m)
  (declare (xargs :guard (bit-listp m)))
  (let ((acl2::__function__ 'pedersen-pad))
    (declare (ignorable acl2::__function__))
    (case (mod (len m) 4)
      (0 m)
      (1 (append m (list 0 0 0)))
      (2 (append m (list 0 0)))
      (3 (append m (list 0)))
      (otherwise (acl2::impossible)))))

Theorem: bit-listp-of-pedersen-pad

(defthm bit-listp-of-pedersen-pad
  (implies (bit-listp m)
           (b* ((m1 (pedersen-pad m)))
             (bit-listp m1)))
  :rule-classes :rewrite)

Theorem: len-of-pedersen-pad

(defthm len-of-pedersen-pad
  (b* ((?m1 (pedersen-pad m)))
    (equal (len m1)
           (* 4 (ceiling (len m) 4)))))

Theorem: multiple-of-4-len-of-pedersen-hash

(defthm multiple-of-4-len-of-pedersen-hash
  (b* ((?m1 (pedersen-pad m)))
    (integerp (/ (len m1) 4))))