		Search-engine friendly clone of the ACL2 documentation.

Mmp-trees

Mmp-decode

Decode an MMP tree into a finite map.

Signature
(mmp-decode root database) → (mv error? map)
Arguments: root — Guard (byte-listp root).; database — Guard (databasep database).
Returns: error? — Type (booleanp error?).; map — Type (bytelist-bytelist-mapp map).

If the MMP tree encodes some finite map, we return that map, along with nil as the error flag (i.e. no error). Otherwise, we return t as error flag, and nil as the map (which is irrelevant in this case).

Here the MMP tree is represented as the root and supporting database, which are the arguments of this function. These are the same arguments as mmp-encoding-p, and correspond to the results of mmp-encode (excluding the error flag). As explained in mmp-encoding-p, the database may be larger than strictly needed for representing the finite map.

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 MMP trees that are valid encodings of finite maps), as explicated by the theorem mmp-encode-of-mmp-decode. It is not quite the right inverse, because, as discussed in mmp-encoding-p, we allow a larger (global) database to encode a map. Thus, the theorem mmp-encode-of-mmp-decode is a weaker version of an actual inversion theorem: it asserts equality of roots and containment of databases.

To prove that decoding is left inverse of encoding (with respect to finite maps that can be encoded), we need to show that encoding is injective over maps 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 maps whose encodings are equal, an executable implementation of decoding, which returns a unique map, could not be shown to be equal to mmp-endoding-witness, which is introduced by a defchoose inside defun-sk and therefore could be either map. Thus, we defer the injectivity and left inverse proofs for now.

Definitions and Theorems

Function: mmp-decode

(defun mmp-decode (root database)
  (declare (xargs :guard (and (byte-listp root)
                              (databasep database))))
  (b* ((root (byte-list-fix root))
       (database (database-fix database)))
    (if (mmp-encoding-p root database)
        (mv nil
            (mmp-encoding-witness root database))
      (mv t nil))))

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

(defthm booleanp-of-mmp-decode.error?
  (b* (((mv ?error? ?map)
        (mmp-decode root database)))
    (booleanp error?))
  :rule-classes :rewrite)

Theorem: bytelist-bytelist-mapp-of-mmp-decode.map

(defthm bytelist-bytelist-mapp-of-mmp-decode.map
  (b* (((mv ?error? ?map)
        (mmp-decode root database)))
    (bytelist-bytelist-mapp map))
  :rule-classes :rewrite)

Theorem: mmp-encode-of-mmp-decode

(defthm mmp-encode-of-mmp-decode
  (implies (and (byte-listp root)
                (databasep database)
                (mmp-encoding-p root database))
           (b* (((mv d-error? d-map)
                 (mmp-decode root database))
                ((mv e-error? e-root e-database)
                 (mmp-encode d-map)))
             (and (not d-error?)
                  (not e-error?)
                  (equal e-root root)
                  (omap::submap e-database database)))))

Theorem: mmp-decode-of-byte-list-fix-root

(defthm mmp-decode-of-byte-list-fix-root
  (equal (mmp-decode (byte-list-fix root)
                     database)
         (mmp-decode root database)))

Theorem: mmp-decode-byte-list-equiv-congruence-on-root

(defthm mmp-decode-byte-list-equiv-congruence-on-root
  (implies (byte-list-equiv root root-equiv)
           (equal (mmp-decode root database)
                  (mmp-decode root-equiv database)))
  :rule-classes :congruence)

Theorem: mmp-decode-of-database-fix-database

(defthm mmp-decode-of-database-fix-database
  (equal (mmp-decode root (database-fix database))
         (mmp-decode root database)))

Theorem: mmp-decode-database-equiv-congruence-on-database

(defthm mmp-decode-database-equiv-congruence-on-database
  (implies (database-equiv database database-equiv)
           (equal (mmp-decode root database)
                  (mmp-decode root database-equiv)))
  :rule-classes :congruence)