		Search-engine friendly clone of the ACL2 documentation.

Mmp-trees

Mmp-read

Read the value associated to a key in an MMP tree.

Signature
(mmp-read key root database) → (mv presentp value)
Arguments: key — Guard (byte-listp key).; root — Guard (byte-listp root).; database — Guard (databasep database).
Returns: presentp — Type (booleanp presentp).; value — Type (byte-listp value).

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 and we look up the key. We return a flag indicating whether the key is present, and we return the byte array value associated to key (nil if the key is absent.

Definitions and Theorems

Function: mmp-read

(defun mmp-read (key root database)
  (declare (xargs :guard (and (byte-listp key)
                              (byte-listp root)
                              (databasep database))))
  (declare (xargs :guard (mmp-encoding-p root database)))
  (b* (((mv & map) (mmp-decode root database))
       (pair? (omap::assoc (byte-list-fix key)
                           (bytelist-bytelist-mfix map))))
    (if (consp pair?)
        (mv t (cdr pair?))
      (mv nil nil))))

Theorem: booleanp-of-mmp-read.presentp

(defthm booleanp-of-mmp-read.presentp
  (b* (((mv ?presentp acl2::?value)
        (mmp-read key root database)))
    (booleanp presentp))
  :rule-classes :rewrite)

Theorem: byte-listp-of-mmp-read.value

(defthm byte-listp-of-mmp-read.value
  (b* (((mv ?presentp acl2::?value)
        (mmp-read key root database)))
    (byte-listp value))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Theorem: mmp-read-of-database-fix-database

(defthm mmp-read-of-database-fix-database
  (equal (mmp-read key root (database-fix database))
         (mmp-read key root database)))

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

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