• 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
      • Set
      • Soft
      • C
      • Bv
      • Imp-language
      • 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
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Mmp-trees

Mmp-encoding-p

Check if a root and database are an MMP encoding of a finite map from byte arrays to byte arrays.

This is a declarative, non-executable definition, which essentially characterizes the image of mmp-encode (over finite maps that can be encoded, i.e. such that mmp-encode returns a nil error flag, except that we allow the database to be larger.

The reason is the following. mmp-encode produces the minimum database that suffices to encode the map. However, it seems reasonable that there is one global database [YP:D.1] [YP:4.1], used to encode a variety of finite maps in the Ethereum state. Thus, given a root and the global database, we can say that they together encode a finite map, even though the database may be larger then needed to encode the map.

Definitions and Theorems

Theorem: mmp-encoding-p-suff

(defthm mmp-encoding-p-suff
 (implies
  (and (bytelist-bytelist-mapp map)
       (b* (((mv map-error? map-root map-database)
             (mmp-encode map)))
         (and (not map-error?)
              (equal map-root (byte-list-fix root))
              (omap::submap map-database (database-fix database)))))
  (mmp-encoding-p root database)))

Theorem: booleanp-of-mmp-encoding-p

(defthm booleanp-of-mmp-encoding-p
  (b* ((yes/no (mmp-encoding-p root database)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: mmp-encoding-p-of-byte-list-fix-root

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

Theorem: mmp-encoding-p-byte-list-equiv-congruence-on-root

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

Theorem: mmp-encoding-p-of-database-fix-database

(defthm mmp-encoding-p-of-database-fix-database
  (equal (mmp-encoding-p root (database-fix database))
         (mmp-encoding-p root database)))

Theorem: mmp-encoding-p-database-equiv-congruence-on-database

(defthm mmp-encoding-p-database-equiv-congruence-on-database
  (implies (database-equiv database database-equiv)
           (equal (mmp-encoding-p root database)
                  (mmp-encoding-p root database-equiv)))
  :rule-classes :congruence)