• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
        • Mmp-trees
          • Mmp-encode-n/c
          • Mmp-encode-c-max
          • Mmp-encode
          • Mmp-write
          • Mmp-decode
          • Mmp-encode-u-map
          • Nibblelist-bytelist-map-sup-len-key
          • Mmp-encode-c-forall
          • Mmp-read
          • Mmp-encoding-p
          • Bytelist-to-nibblelist-keys
          • Mmp-encode-c-exists
          • Bytelist-bytelist-map
          • Nibblelist-bytelist-map
        • Semaphore
        • Database
        • Cryptography
        • Rlp
        • Transactions
        • Hex-prefix
        • Basics
        • Addresses
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

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