		Search-engine friendly clone of the ACL2 documentation.

Hex-prefix

Hp-encode

Hex-prefix encoding function.

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

This corresponds to \mathtt{HP} [YP:(186)] [YP:(187)].

The t flag is treated as a boolean (i.e. 0 or not 0), so we use directly a boolean as argument to this function. Note also that \mathtt{HP} is called with \mathit{true} and \mathit{false} in [YP:(194)], so perhaps [YP:(187)] should be rephrased to treat t as an actual boolean (as opposed to 0 or not 0).

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)

Function: hp-encode

(defun hp-encode (nibbles flag)
  (declare (xargs :guard (and (nibble-listp nibbles)
                              (booleanp flag))))
  (b* ((ft (if flag 2 0))
       (len-nibbles (len nibbles))
       (evenp (evenp len-nibbles))
       (first-byte (if evenp (* 16 ft)
                     (b* ((first-nibble (nibble-fix (car nibbles))))
                       (+ (* 16 (1+ ft)) first-nibble))))
       (rest-nibbles (if evenp nibbles (cdr nibbles)))
       (rest-bytes (hp-encode-aux rest-nibbles)))
    (cons first-byte rest-bytes)))

Theorem: byte-listp-of-hp-encode

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

Theorem: consp-of-hp-encode

(defthm consp-of-hp-encode
  (b* ((?bytes (hp-encode nibbles flag)))
    (consp bytes))
  :rule-classes :type-prescription)

Theorem: len-of-hp-encode

(defthm len-of-hp-encode
  (b* ((?bytes (hp-encode nibbles flag)))
    (equal (len bytes)
           (1+ (floor (len nibbles) 2)))))

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

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

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

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

Theorem: hp-encode-of-bool-fix-flag

(defthm hp-encode-of-bool-fix-flag
  (equal (hp-encode nibbles (acl2::bool-fix flag))
         (hp-encode nibbles flag)))

Theorem: hp-encode-iff-congruence-on-flag

(defthm hp-encode-iff-congruence-on-flag
  (implies (iff flag flag-equiv)
           (equal (hp-encode nibbles flag)
                  (hp-encode nibbles flag-equiv)))
  :rule-classes :congruence)

Subtopics

Hp-encode-aux: Turn a even-length sequence of nibbles into a sequence of bytes.