Definition of

`mmp-encode-n` corresponds to `mmp-encode-c` corresponds to `mmp-encode-u` corresponds to the ``local function'' `mmp-encode-u`
and just included 16 calls of `mmp-encode-n`
in the definition of `mmp-encode-c`,
but instead we just include 1 call of `mmp-encode-u`,
which recursively performs the 16 iterations itself.
Introducing `mmp-encode-u` seems clearer and more elegant
than including 16 calls of `mmp-encode-n`.

Here `mmp-encode-u`.

In [YP], `mmp-encode-n`, `mmp-encode-c`, and `mmp-encode-u`
all return a database, which they construct.
This returned database contains all and only the pairs
necessary to encode

Since we cannot ignore the mathematical possibility of hash collisions,
`mmp-encode-n`, `mmp-encode-c`, and `mmp-encode-u`
all return an error flag that, when equal to `mmp-encode-n`,
the only function that directly extends the database
(the other functions merge databases from sub-computations).
If the key is already in the database but the value does not differ,
then there is no collision, and no change to the database;
if we view hashes as implementation-independent pointers
(which is a way to view MMP trees),
this situation just corresponding to two aliased pointers.

Since `rlp-encode-tree`),
the error flag returned by our functions
is

If no hash collisions occur and all RLP encodings succeed,
the error flag returned by our functions is

The definition of `mmp-encode-n` follows
the definition of `mmp-encode-c`,
the additional propagation of the database from `mmp-encode-c`,
and the additional extension of the database mentioned above.

The definition of `mmp-encode-c` follows
the definition of `mmp-encode-c` calculates
an error flag, an RLP tree, and a database according to the three cases.
Then, `mmp-encode-c` RLP encodes the tree.
If an error occurs prior to RLP encoding,
the ``inner'' computation of `mmp-encode-c` returns
an RLP tree consisting of an empty byte array and an empty database,
but these values are irrelevant.
Because of this factoring,
and because some tests relevant to termination (see section below)
appear in this factored code,
we need to extend the ACL2::rulers of `mmp-encode-c`
with

The first case of the definition of

We use `mmp-encode-c-max` to calculate the variable `mmp-encode-c`)
in the second case of the definition of `mmp-encode-c-max`,
the map must be non-empty for this `mmp-encode-c`.

Note that the scope of the universal quantifier
in the second case of the definition of

Note that the `mmp-encode-u`;
this function corresponds to
the ``local function'' `mmp-encode-c`, when it calls `mmp-encode-u`.
The latter function returns,
essentially (but see below for more precision),

`mmp-encode-u` loops through nibble 0 to 15,
extracting submaps and recursively calling `mmp-encode-n` on them.
Errors are propagated and databases are merged, checking for collisions.
`mmp-encode-u` does not quite return
the list of roots `mmp-encode-c` can more easily assemble the trees
into an RLP (branching) tree.

The variable

It is not clear whether

The termination of
`mmp-encode-n`, `mmp-encode-c`, and `mmp-encode-u`
is proved via a lexicographic measure
that consists of three components.

This termination proof relies on
some invariants satisfied by the arguments of these functions.
These invariants are added as guards,
and tested with `mbt` at the beginning of the functions.
An invariant that applies to all three functions is that
all the keys in the map have the same first `mmp-encode-c` and `mmp-encode-u`
is that the map is not empty.
An invariant that applies to `mmp-encode-u` is that
the map is not a singleton.

`mmp-encode-n` calls `mmp-encode-c`
with the same arguments `mmp-encode-c` is ``smaller'' than `mmp-encode-c`.
Similarly, `mmp-encode-c` calls `mmp-encode-u`
with the same arguments `mmp-encode-u` is ``smaller'' than `mmp-encode-u`.
Thus, we order these functions by assigning 0, 1, and 2 to them:
this is the second component of the lexicographic measure.

Since `mmp-encode-u` calls `mmp-encode-n`
and `mmp-encode-c` calls `mmp-encode-n`,
the relative ordering of these functions cannot be
the first component of the lexicographic measure.
Instead, the first component involves `mmp-encode-n`,
`mmp-encode-c` checks that

The increase of `nibblelist-bytelist-map-sup-len-key`:
the first component of the lexicographic measure is
the difference between that and `mmp-encode-c` calls `mmp-encode-n`,
`nibblelist-bytelist-map-sup-len-key` remains the same;
since it is greater than or equal to `mmp-encode-u` calls `mmp-encode-n`,
`nibblelist-bytelist-map-sup-len-key`
either stays the same or becomes smaller,
as proved in `mmp-encode-u-map`,
because we are calling `mmp-encode-n` on a submap of the map;
to show that the first component of the measure strictly decreases
as `nibblelist-bytelist-map-sup-len-key`,
as proved in `mmp-encode-c-max`,
given that the map has at least two elements,
as asserted by the invariant of `mmp-encode-u`.

The guard verification of
`mmp-encode-n`, `mmp-encode-c`, and `mmp-encode-u`
involves proving the preservation, in the recursive calls,
of the invariants used for the termination proof, mentioned above.

This is easy for most recursive calls,
where

In the call of `mmp-encode-n` from `mmp-encode-c`,

In the call of `mmp-encode-n` from `mmp-encode-u`,
the map becomes the submap and

**Function: **

(defun mmp-encode-n (map i) (declare (xargs :guard (and (nibblelist-bytelist-mapp map) (natp i)))) (declare (xargs :guard (mmp-encode-c-max.elementp map i))) (b* (((unless (mbt (mmp-encode-c-max.elementp map i))) (mv nil nil nil)) ((when (or (not (mbt (nibblelist-bytelist-mapp map))) (omap::empty map))) (mv nil nil nil)) ((mv c-error? c-root c-database) (mmp-encode-c map i)) ((when c-error?) (mv c-error? nil nil)) ((when (< (len c-root) 32)) (mv nil c-root c-database)) (hash (keccak-256-bytes c-root)) (pair? (omap::in hash c-database)) (collisionp (and pair? (not (equal (cdr pair?) c-root)))) ((when collisionp) (mv :collision nil nil)) (database (omap::update hash c-root c-database))) (mv nil hash database)))

**Function: **

(defun mmp-encode-c (map i) (declare (xargs :guard (and (nibblelist-bytelist-mapp map) (natp i)))) (declare (xargs :guard (and (mmp-encode-c-max.elementp map i) (not (omap::empty map))))) (b* (((unless (mbt (and (mmp-encode-c-max.elementp map i) (nibblelist-bytelist-mapp map) (not (omap::empty map))))) (mv nil nil nil)) ((mv error? rlp-tree database) (b* (((when (= (omap::size map) 1)) (b* (((mv key val) (omap::head map)) (key-rest (nthcdr i key))) (mv nil (rlp-tree-branch (list (rlp-tree-leaf (hp-encode key-rest t)) (rlp-tree-leaf val))) nil))) (j (mmp-encode-c-max map)) ((when (/= (nfix i) j)) (b* (((mv n-error? n-root n-database) (mmp-encode-n map j)) ((when n-error?) (mv n-error? (rlp-tree-leaf nil) nil)) ((mv any-key &) (omap::head map)) (key-part (nthcdr i (take j any-key)))) (mv nil (rlp-tree-branch (list (rlp-tree-leaf (hp-encode key-part nil)) (rlp-tree-leaf n-root))) n-database))) ((mv u-error? u-trees u-database) (mmp-encode-u map i 0)) ((when u-error?) (mv u-error? (rlp-tree-leaf nil) nil)) ((mv any-key &) (omap::head map)) (key-prefix (take i any-key)) (pair (omap::in key-prefix map)) (v (and pair (cdr pair))) (v-tree (if v (rlp-tree-leaf v) (rlp-tree-branch nil)))) (mv nil (rlp-tree-branch (rcons v-tree u-trees)) u-database))) ((when error?) (mv error? nil nil)) ((mv rlp-error? rlp-encoding) (rlp-encode-tree rlp-tree)) ((when rlp-error?) (mv :rlp nil nil))) (mv nil rlp-encoding database)))

**Function: **

(defun mmp-encode-u (map i nibble-counter) (declare (xargs :guard (and (nibblelist-bytelist-mapp map) (natp i) (natp nibble-counter)))) (declare (xargs :guard (and (mmp-encode-c-max.elementp map i) (not (omap::empty map)) (not (equal (omap::size map) 1))))) (b* (((unless (mbt (and (mmp-encode-c-max.elementp map i) (nibblelist-bytelist-mapp map) (not (omap::empty map)) (not (equal (omap::size map) 1))))) (mv nil nil nil)) ((when (> (nfix nibble-counter) 15)) (mv nil nil nil)) (submap (mmp-encode-u-map map i nibble-counter)) ((mv n-error? n-root n-database) (mmp-encode-n submap (1+ (nfix i)))) ((when n-error?) (mv n-error? nil nil)) ((mv u-error? u-trees u-database) (mmp-encode-u map i (1+ (nfix nibble-counter)))) ((when u-error?) (mv u-error? nil nil)) ((unless (omap::compatiblep n-database u-database)) (mv :collision nil nil)) (trees (cons (rlp-tree-leaf n-root) u-trees)) (database (omap::update* n-database u-database))) (mv nil trees database)))

**Theorem: **

(defthm return-type-of-mmp-encode-n.error? (b* (((mv ?error? ?root ?database) (mmp-encode-n map i))) (member-eq error? '(nil :collision :rlp))) :rule-classes :rewrite)

**Theorem: **

(defthm return-type-of-mmp-encode-n.root (b* (((mv ?error? ?root ?database) (mmp-encode-n map i))) (byte-listp root)) :rule-classes :rewrite)

**Theorem: **

(defthm return-type-of-mmp-encode-n.database (b* (((mv ?error? ?root ?database) (mmp-encode-n map i))) (databasep database)) :rule-classes :rewrite)

**Theorem: **

(defthm return-type-of-mmp-encode-c.error? (b* (((mv ?error? ?root ?database) (mmp-encode-c map i))) (member-eq error? '(nil :collision :rlp))) :rule-classes :rewrite)

**Theorem: **

(defthm return-type-of-mmp-encode-c.root (b* (((mv ?error? ?root ?database) (mmp-encode-c map i))) (byte-listp root)) :rule-classes :rewrite)

**Theorem: **

(defthm return-type-of-mmp-encode-c.database (b* (((mv ?error? ?root ?database) (mmp-encode-c map i))) (databasep database)) :rule-classes :rewrite)

**Theorem: **

(defthm return-type-of-mmp-encode-u.error? (b* (((mv ?error? ?trees ?database) (mmp-encode-u map i nibble-counter))) (member-eq error? '(nil :collision :rlp))) :rule-classes :rewrite)

**Theorem: **

(defthm return-type-of-mmp-encode-u.trees (b* (((mv ?error? ?trees ?database) (mmp-encode-u map i nibble-counter))) (rlp-tree-listp trees)) :rule-classes :rewrite)

**Theorem: **

(defthm return-type-of-mmp-encode-u.database (b* (((mv ?error? ?trees ?database) (mmp-encode-u map i nibble-counter))) (databasep database)) :rule-classes :rewrite)

**Theorem: **

(defthm mmp-encode-n-of-nibblelist-bytelist-mfix-map (equal (mmp-encode-n (nibblelist-bytelist-mfix map) i) (mmp-encode-n map i)))

**Theorem: **

(defthm mmp-encode-n-of-nfix-i (equal (mmp-encode-n map (nfix i)) (mmp-encode-n map i)))

**Theorem: **

(defthm mmp-encode-c-of-nibblelist-bytelist-mfix-map (equal (mmp-encode-c (nibblelist-bytelist-mfix map) i) (mmp-encode-c map i)))

**Theorem: **

(defthm mmp-encode-c-of-nfix-i (equal (mmp-encode-c map (nfix i)) (mmp-encode-c map i)))

**Theorem: **

(defthm mmp-encode-u-of-nibblelist-bytelist-mfix-map (equal (mmp-encode-u (nibblelist-bytelist-mfix map) i nibble-counter) (mmp-encode-u map i nibble-counter)))

**Theorem: **

(defthm mmp-encode-u-of-nfix-i (equal (mmp-encode-u map (nfix i) nibble-counter) (mmp-encode-u map i nibble-counter)))

**Theorem: **

(defthm mmp-encode-u-of-nfix-nibble-counter (equal (mmp-encode-u map i (nfix nibble-counter)) (mmp-encode-u map i nibble-counter)))

**Theorem: **

(defthm mmp-encode-n-nibblelist-bytelist-mequiv-congruence-on-map (implies (nibblelist-bytelist-mequiv map map-equiv) (equal (mmp-encode-n map i) (mmp-encode-n map-equiv i))) :rule-classes :congruence)

**Theorem: **

(defthm mmp-encode-n-nat-equiv-congruence-on-i (implies (acl2::nat-equiv i i-equiv) (equal (mmp-encode-n map i) (mmp-encode-n map i-equiv))) :rule-classes :congruence)

**Theorem: **

(defthm mmp-encode-c-nibblelist-bytelist-mequiv-congruence-on-map (implies (nibblelist-bytelist-mequiv map map-equiv) (equal (mmp-encode-c map i) (mmp-encode-c map-equiv i))) :rule-classes :congruence)

**Theorem: **

(defthm mmp-encode-c-nat-equiv-congruence-on-i (implies (acl2::nat-equiv i i-equiv) (equal (mmp-encode-c map i) (mmp-encode-c map i-equiv))) :rule-classes :congruence)

**Theorem: **

(defthm mmp-encode-u-nibblelist-bytelist-mequiv-congruence-on-map (implies (nibblelist-bytelist-mequiv map map-equiv) (equal (mmp-encode-u map i nibble-counter) (mmp-encode-u map-equiv i nibble-counter))) :rule-classes :congruence)

**Theorem: **

(defthm mmp-encode-u-nat-equiv-congruence-on-i (implies (acl2::nat-equiv i i-equiv) (equal (mmp-encode-u map i nibble-counter) (mmp-encode-u map i-equiv nibble-counter))) :rule-classes :congruence)

**Theorem: **

(defthm mmp-encode-u-nat-equiv-congruence-on-nibble-counter (implies (acl2::nat-equiv nibble-counter nibble-counter-equiv) (equal (mmp-encode-u map i nibble-counter) (mmp-encode-u map i nibble-counter-equiv))) :rule-classes :congruence)