		Search-engine friendly clone of the ACL2 documentation.

Mmp-trees

Mmp-write

Write a value for a key in an MMP tree.

Signature
(mmp-write key value root database) → (mv error? new-root new-database)
Arguments: key — Guard (byte-listp key).; value — Guard (byte-listp value).; root — Guard (byte-listp root).; database — Guard (databasep database).
Returns: error? — Type (member-eq error? '(nil :collision :rlp)).; new-root — Type (byte-listp new-root).; new-database — Type (databasep new-database).

We require (in the guard) that the MMP tree is valid, i.e. it encodes a finite map.

We provide a high-level definition here. We decode the MMP tree, we update the key, and we re-encode the map. The key may already be present, in which case the old value is overwritten. If the key is not present, it is added to the map.

The database argument of this function represents the global database. Thus, we return not just the database needed to encode the updated map, but the union of that with the input database. Thus, the resulting database may include more than needed to simply encode the new finite map. If we view the hashes in the database as implementation-independent pointers, updating the MMP tree may lead to ``garbage'' in the sense of garbage collection, i.e. portions of the database that are no longer referenced, directly or indirectly, starting from the ``roots'' in the Ethereum state. Presumably an Ethereum implementation could perform some garbage collection, but here we conservatively assume that it does not.

If the re-encoding of the new finite map causes a collision or produces some non-RLP-encodable data, we forward the error flag returned by mmp-encode. We also check for collision when taking the union of the initial database and the one returned by mmp-encode, returning :collision if such a collision happens.

Definitions and Theorems

Function: mmp-write

(defun mmp-write (key value root database)
  (declare (xargs :guard (and (byte-listp key)
                              (byte-listp value)
                              (byte-listp root)
                              (databasep database))))
  (declare (xargs :guard (mmp-encoding-p root database)))
  (b* (((mv & map) (mmp-decode root database))
       (new-map (omap::update (byte-list-fix key)
                              (byte-list-fix value)
                              map))
       ((mv error? new-root new-database-min)
        (mmp-encode new-map))
       ((when error?) (mv error? nil nil))
       ((unless (omap::compatiblep new-database-min
                                   (database-fix database)))
        (mv :collision nil nil))
       (new-database (omap::update* new-database-min
                                    (database-fix database))))
    (mv nil new-root new-database)))

Theorem: return-type-of-mmp-write.error?

(defthm return-type-of-mmp-write.error?
  (b* (((mv ?error? ?new-root ?new-database)
        (mmp-write key value root database)))
    (member-eq error? '(nil :collision :rlp)))
  :rule-classes :rewrite)

Theorem: byte-listp-of-mmp-write.new-root

(defthm byte-listp-of-mmp-write.new-root
  (b* (((mv ?error? ?new-root ?new-database)
        (mmp-write key value root database)))
    (byte-listp new-root))
  :rule-classes :rewrite)

Theorem: databasep-of-mmp-write.new-database

(defthm databasep-of-mmp-write.new-database
  (b* (((mv ?error? ?new-root ?new-database)
        (mmp-write key value root database)))
    (databasep new-database))
  :rule-classes :rewrite)

Theorem: mmp-write-of-byte-list-fix-key

(defthm mmp-write-of-byte-list-fix-key
  (equal (mmp-write (byte-list-fix key)
                    value root database)
         (mmp-write key value root database)))

Theorem: mmp-write-byte-list-equiv-congruence-on-key

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

Theorem: mmp-write-of-byte-list-fix-value

(defthm mmp-write-of-byte-list-fix-value
  (equal (mmp-write key (byte-list-fix value)
                    root database)
         (mmp-write key value root database)))

Theorem: mmp-write-byte-list-equiv-congruence-on-value

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

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

(defthm mmp-write-of-byte-list-fix-root
  (equal (mmp-write key value (byte-list-fix root)
                    database)
         (mmp-write key value root database)))

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

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

Theorem: mmp-write-of-database-fix-database

(defthm mmp-write-of-database-fix-database
  (equal (mmp-write key value root (database-fix database))
         (mmp-write key value root database)))

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

(defthm mmp-write-database-equiv-congruence-on-database
  (implies (database-equiv database database-equiv)
           (equal (mmp-write key value root database)
                  (mmp-write key value root database-equiv)))
  :rule-classes :congruence)