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

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-encoding-p`,
we allow a larger (global) database to encode a map.
Thus, the theorem

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 `defchoose` inside `defun-sk`
and therefore could be either map.
Thus, we defer the injectivity and left inverse proofs for now.

**Function: **

(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: **

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

**Theorem: **

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

**Theorem: **

(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: **

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

**Theorem: **

(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: **

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

**Theorem: **

(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)