		Search-engine friendly clone of the ACL2 documentation.

Hp-encode-aux

Turn a even-length sequence of nibbles into a sequence of bytes.

Signature
(hp-encode-aux nibbles) → bytes
Arguments: nibbles — Guard (nibble-listp nibbles).
Returns: bytes — Type (byte-listp bytes).

This calculates the bytes of the result of \mathtt{HP} that come after the first byte, in the way described by [YP:(186)].

Definitions and Theorems

Function: hp-encode-aux

(defun hp-encode-aux (nibbles)
  (declare (xargs :guard (nibble-listp nibbles)))
  (declare (xargs :guard (evenp (len nibbles))))
  (b* (((when (endp nibbles)) nil)
       (nibble-hi (nibble-fix (car nibbles)))
       (nibble-lo (nibble-fix (cadr nibbles)))
       (byte (+ (* 16 nibble-hi) nibble-lo))
       (bytes (hp-encode-aux (cddr nibbles))))
    (cons byte bytes)))

Theorem: byte-listp-of-hp-encode-aux

(defthm byte-listp-of-hp-encode-aux
  (b* ((bytes (hp-encode-aux nibbles)))
    (byte-listp bytes))
  :rule-classes :rewrite)

Theorem: len-of-hp-encode-aux

(defthm len-of-hp-encode-aux
  (implies (evenp (len nibbles))
           (b* ((?bytes (hp-encode-aux nibbles)))
             (equal (len bytes)
                    (floor (len nibbles) 2)))))

Theorem: hp-encode-aux-of-nibble-list-fix-nibbles

(defthm hp-encode-aux-of-nibble-list-fix-nibbles
  (equal (hp-encode-aux (nibble-list-fix nibbles))
         (hp-encode-aux nibbles)))

Theorem: hp-encode-aux-nibble-list-equiv-congruence-on-nibbles

(defthm hp-encode-aux-nibble-list-equiv-congruence-on-nibbles
  (implies (acl2::nibble-list-equiv nibbles nibbles-equiv)
           (equal (hp-encode-aux nibbles)
                  (hp-encode-aux nibbles-equiv)))
  :rule-classes :congruence)