• 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
      • Abnf
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
      • 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

Nibblelist-bytelist-map-sup-len-key

Natural number supremum of the lengths of the keys in a map from nibble arrays to byte arrays.

Signature

(nibblelist-bytelist-map-sup-len-key map) → sup

Arguments

map — Guard (nibblelist-bytelist-mapp map).

Returns

sup — Type (natp sup).

This is 0 if the map is empty. Otherwise, it is the maximum key length. Thus, if we limit the values of interest to the natural numbers, this is the supremum of the set of the key lengths, i.e. the minimum upper bound.

This function, and its property of being greater than or equal to the length of every key in the map (expressed by the linear rule below), are used to prove that the maximum defined by mmp-encode-c-max exists. See that function for details.

When updating the map, the result of this function is the maximum of the length of the udpated key and the result prior to updating.

Definitions and Theorems

Function: nibblelist-bytelist-map-sup-len-key

(defun nibblelist-bytelist-map-sup-len-key (map)
  (declare (xargs :guard (nibblelist-bytelist-mapp map)))
  (b* (((unless (mbt (nibblelist-bytelist-mapp map)))
        0)
       ((when (omap::emptyp map)) 0)
       ((mv key &) (omap::head map)))
    (max (len key)
         (nibblelist-bytelist-map-sup-len-key (omap::tail map)))))

Theorem: natp-of-nibblelist-bytelist-map-sup-len-key

(defthm natp-of-nibblelist-bytelist-map-sup-len-key
  (b* ((sup (nibblelist-bytelist-map-sup-len-key map)))
    (natp sup))
  :rule-classes :rewrite)

Theorem: nibblelist-bytelist-map-sup-len-key-geq-len-key

(defthm nibblelist-bytelist-map-sup-len-key-geq-len-key
  (implies (and (omap::assoc key map)
                (nibblelist-bytelist-mapp map))
           (>= (nibblelist-bytelist-map-sup-len-key map)
               (len key)))
  :rule-classes :linear)

Theorem: nibblelist-bytelist-map-sup-len-key-of-update

(defthm nibblelist-bytelist-map-sup-len-key-of-update
 (implies
  (and (nibble-listp key)
       (byte-listp val)
       (nibblelist-bytelist-mapp map))
  (equal
    (nibblelist-bytelist-map-sup-len-key (omap::update key val map))
    (max (nibblelist-bytelist-map-sup-len-key map)
         (len key)))))

Theorem: nibblelist-bytelist-map-sup-len-key-of-nibblelist-bytelist-mfix-map

(defthm
 nibblelist-bytelist-map-sup-len-key-of-nibblelist-bytelist-mfix-map
 (equal (nibblelist-bytelist-map-sup-len-key
             (nibblelist-bytelist-mfix map))
        (nibblelist-bytelist-map-sup-len-key map)))

Theorem: nibblelist-bytelist-map-sup-len-key-nibblelist-bytelist-mequiv-congruence-on-map

(defthm
 nibblelist-bytelist-map-sup-len-key-nibblelist-bytelist-mequiv-congruence-on-map
 (implies (nibblelist-bytelist-mequiv map map-equiv)
          (equal (nibblelist-bytelist-map-sup-len-key map)
                 (nibblelist-bytelist-map-sup-len-key map-equiv)))
 :rule-classes :congruence)