		Search-engine friendly clone of the ACL2 documentation.

Pedersen-hash

Pedersen-pad

Pedersen hash padding [ZPS:5.4.1.7].

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

The message is padded with zero bits on the right to make its length a multiple of 3.

Definitions and Theorems

Function: pedersen-pad

(defun pedersen-pad (m)
  (declare (xargs :guard (bit-listp m)))
  (declare (xargs :guard (consp m)))
  (let ((__function__ 'pedersen-pad))
    (declare (ignorable __function__))
    (append (bit-list-fix m)
            (case (mod (len m) 3)
              (0 nil)
              (1 (list 0 0))
              (2 (list 0))))))

Theorem: bit-listp-of-pedersen-pad

(defthm bit-listp-of-pedersen-pad
  (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)
           (* 3 (ceiling (len m) 3)))))

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

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