		Search-engine friendly clone of the ACL2 documentation.

Hex-prefix

Hp-decode

Hex-prefix decoding function.

Signature
(hp-decode encoding) → (mv error? nibbles flag)
Arguments: encoding — Guard (byte-listp encoding).
Returns: error? — Type (booleanp error?).; nibbles — Type (nibble-listp nibbles).; flag — Type (booleanp flag).

If the argument byte array is the result of encoding some nibble array and boolean flag, we return the nibble array and boolean flag, along with a nil error flag. Otherwise, we return a t error flag, along with an empty byte array and a false flag (but these two values are irrelevant in this case).

This is a declarative, non-executable definition, which says that decoding is the inverse of encoding.

More precisely, we define decoding as, essentially, the right inverse of encoding (with respect to byte arrays that are valid encodings), as explicated by the theorem hp-encode-of-hp-decode. To prove that decoding is left inverse of encoding (with respect to nibble arrays and boolean flags that can be encoded), we need to show that encoding is injective over nibble arrays and boolean flags that can be encoded. We conjecture that the proof of this property may be a by-product of deriving an executable implementation of decoding via stepwise refinement (e.g. using APT): if there were two different pairs of nibble arrays and boolean flags whose encodings are equal, an executable implementation of decoding, which returns a unique nibble array and boolean flag, could not be shown to be equal to hp-endoding-witness, which is introduced by a defchoose inside defun-sk and therefore could be either pair (of a nibble array and a boolean flag). Thus, we defer the injectivity and left inverse proofs for now.

Definitions and Theorems

Function: hp-decode

(defun hp-decode (encoding)
  (declare (xargs :guard (byte-listp encoding)))
  (b* ((encoding (byte-list-fix encoding)))
    (if (hp-encoding-p encoding)
        (b* (((mv nibbles flag)
              (hp-encoding-witness encoding)))
          (mv nil nibbles flag))
      (mv t nil nil))))

Theorem: booleanp-of-hp-decode.error?

(defthm booleanp-of-hp-decode.error?
  (b* (((mv ?error? ?nibbles ?flag)
        (hp-decode encoding)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: nibble-listp-of-hp-decode.nibbles

(defthm nibble-listp-of-hp-decode.nibbles
  (b* (((mv ?error? ?nibbles ?flag)
        (hp-decode encoding)))
    (nibble-listp nibbles))
  :rule-classes :rewrite)

Theorem: booleanp-of-hp-decode.flag

(defthm booleanp-of-hp-decode.flag
  (b* (((mv ?error? ?nibbles ?flag)
        (hp-decode encoding)))
    (booleanp flag))
  :rule-classes :rewrite)

Theorem: hp-encode-of-hp-decode

(defthm hp-encode-of-hp-decode
  (implies (and (byte-listp encoding)
                (hp-encoding-p encoding))
           (b* (((mv d-error? d-nibbles d-flag)
                 (hp-decode encoding))
                (e-encoding (hp-encode d-nibbles d-flag)))
             (and (not d-error?)
                  (equal e-encoding encoding)))))

Theorem: hp-decode-of-byte-list-fix-encoding

(defthm hp-decode-of-byte-list-fix-encoding
  (equal (hp-decode (byte-list-fix encoding))
         (hp-decode encoding)))

Theorem: hp-decode-byte-list-equiv-congruence-on-encoding

(defthm hp-decode-byte-list-equiv-congruence-on-encoding
  (implies (byte-list-equiv encoding encoding-equiv)
           (equal (hp-decode encoding)
                  (hp-decode encoding-equiv)))
  :rule-classes :congruence)