• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • 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
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Mmp-trees

Mmp-encode-c-max

Value of the maximum operator in the second case of the definition of c [YP:(194)].

This is used in the definition of mmp-encode-c, hence the name.

The x in the set being maximized is a natural number, because it is equated to a length. Therefore, we use defmax-nat to introduce this maximum.

This maximum always exists if the map is not empty. We can establish this by showing that:

1. The set \{x\mid\ldots\} being maximized is never empty because 0 is always in the set. This is expressed by theorem mmp-encode-c-max-set-nonempty below, which does not actually need the map to be non-empty.
2. The elements of the set cannot exceed the maximum length of the keys of the map, which is returned by nibblelist-bytelist-map-sup-len-key. This is expressed by theorem mmp-encode-c-max-set-bounded below. The reason why this theorem holds is that the elements of the set are the xs that are lengths of prefixes of the keys in the map, which are therefore no larger than the lengths of the whole keys, which are no larger than their maximum. Here the non-emptiness of the map is needed: without it, x could be arbitrarily large because there would be no keys to take the prefix of, mmp-encode-c-forall would be trivially true, mmp-encode-c-exists would be also true because there is always an l of any length. Concretely, in the proof of the theorem, we need to instantiate the key variable in both the linear rule of nibblelist-bytelist-map-sup-len-key and the inequality theorem about mmp-encode-c-exists, which we do with the key returned by omap::head: any other key in the map would have worked, but the point is that the map must be non-empty for a key to exist.

With these two theorems in hand, we use a suitable instance of the helper theorem mmp-encode-c-max.existsp-when-nonempty-and-bounded generated by defmax-nat, whose proof uses the two theorems as rewrite rules.

Since nibblelist-bytelist-map-sup-len-key is an upper bound, it is greater than or equal to mmp-encode-c-max and any element in the set. This is expressed by two additional linear rules below, whose hypotheses match the ones under which nibblelist-bytelist-map-sup-len-key is an upper bound.

When the map has two or more keys, nibblelist-bytelist-map-sup-len-key is a strict upper bound, i.e. it is not equal to any element in the set. This is proved below by taking the first two keys in the map, called key1 and key2 in the lemmas, and showing that:

1. The two keys differ, because they are strictly ordered in the map.
2. If nibblelist-bytelist-map-sup-len-key were an element of the set, then the two keys would have the same prefix, of length nibblelist-bytelist-map-sup-len-key.
3. nibblelist-bytelist-map-sup-len-key is an upper bound of the lengths of the keys, by its definition.
4. If nibblelist-bytelist-map-sup-len-key were an element of the set, then it would also be an upper bound of the lengths of the keys, by the definition of the set.
5. If nibblelist-bytelist-map-sup-len-key were an element of the set, then by (2), (3), and (4) above it would be the length of both keys and thus the two keys would be equal. But this contradicts (1) above, and thus nibblelist-bytelist-map-sup-len-key must differ from any element i of the set.

Every element of the set, including the maximum if it exists, is less than or equal to the length of every key in the map.

If the map is empty, then all the natural numbers are in the set.

Definitions and Theorems

Function: mmp-encode-c-max.elementp

(defun mmp-encode-c-max.elementp (map x)
  (declare (xargs :guard (and (nibblelist-bytelist-mapp map)
                              (natp x))))
  (mmp-encode-c-exists map x))

Theorem: mmp-encode-c-max.uboundp-necc

(defthm mmp-encode-c-max.uboundp-necc
  (implies (and (mmp-encode-c-max.uboundp map x)
                (natp x1)
                (mmp-encode-c-max.elementp map x1))
           (>= (nfix x) x1)))

Theorem: booleanp-ofmmp-encode-c-max.uboundp

(defthm booleanp-ofmmp-encode-c-max.uboundp
  (booleanp (mmp-encode-c-max.uboundp map x)))

Theorem: mmp-encode-c-max.existsp-suff

(defthm mmp-encode-c-max.existsp-suff
  (implies (and (natp x)
                (mmp-encode-c-max.elementp map x)
                (mmp-encode-c-max.uboundp map x))
           (mmp-encode-c-max.existsp map)))

Theorem: booleanp-ofmmp-encode-c-max.existsp

(defthm booleanp-ofmmp-encode-c-max.existsp
  (booleanp (mmp-encode-c-max.existsp map)))

Function: mmp-encode-c-max

(defun mmp-encode-c-max (map)
  (declare (xargs :guard (nibblelist-bytelist-mapp map)))
  (if (mmp-encode-c-max.existsp map)
      (mmp-encode-c-max.existsp-witness map)
    nil))

Theorem: maybe-natp-of-mmp-encode-c-max

(defthm maybe-natp-of-mmp-encode-c-max
  (acl2::maybe-natp (mmp-encode-c-max map)))

Theorem: natp-of-mmp-encode-c-max-equal-mmp-encode-c-max.existsp

(defthm natp-of-mmp-encode-c-max-equal-mmp-encode-c-max.existsp
  (equal (natp (mmp-encode-c-max map))
         (mmp-encode-c-max.existsp map)))

Theorem: natp-of-mmp-encode-c-max-when-mmp-encode-c-max.existsp

(defthm natp-of-mmp-encode-c-max-when-mmp-encode-c-max.existsp
  (implies (mmp-encode-c-max.existsp map)
           (natp (mmp-encode-c-max map)))
  :rule-classes :type-prescription)

Theorem: mmp-encode-c-max-iff-mmp-encode-c-max.existsp

(defthm mmp-encode-c-max-iff-mmp-encode-c-max.existsp
  (iff (mmp-encode-c-max map)
       (mmp-encode-c-max.existsp map)))

Theorem: not-mmp-encode-c-max-when-not-mmp-encode-c-max.existsp

(defthm not-mmp-encode-c-max-when-not-mmp-encode-c-max.existsp
  (implies (not (mmp-encode-c-max.existsp map))
           (not (mmp-encode-c-max map)))
  :rule-classes :type-prescription)

Theorem: mmp-encode-c-max.elementp-of-mmp-encode-c-max-when-mmp-encode-c-max.existsp

(defthm
 mmp-encode-c-max.elementp-of-mmp-encode-c-max-when-mmp-encode-c-max.existsp
 (implies (mmp-encode-c-max.existsp map)
          (mmp-encode-c-max.elementp map (mmp-encode-c-max map))))

Theorem: mmp-encode-c-max.uboundp-of-mmp-encode-c-max-when-existsp

(defthm mmp-encode-c-max.uboundp-of-mmp-encode-c-max-when-existsp
  (implies (mmp-encode-c-max.existsp map)
           (mmp-encode-c-max.uboundp map (mmp-encode-c-max map))))

Theorem: mmp-encode-c-max-geq-when-mmp-encode-c-max.existsp-linear

(defthm mmp-encode-c-max-geq-when-mmp-encode-c-max.existsp-linear
  (implies (and (mmp-encode-c-max.existsp map)
                (mmp-encode-c-max.elementp map x1)
                (natp x1))
           (>= (mmp-encode-c-max map) x1))
  :rule-classes :linear)

Theorem: mmp-encode-c-max-geq-when-mmp-encode-c-max.existsp-rewrite

(defthm mmp-encode-c-max-geq-when-mmp-encode-c-max.existsp-rewrite
  (implies (and (mmp-encode-c-max.existsp map)
                (mmp-encode-c-max.elementp map x1)
                (natp x1))
           (>= (mmp-encode-c-max map) x1)))

Theorem: mmp-encode-c-max-leq-when-mmp-encode-c-max.existsp-linear

(defthm mmp-encode-c-max-leq-when-mmp-encode-c-max.existsp-linear
  (implies (and (mmp-encode-c-max.existsp map)
                (mmp-encode-c-max.uboundp map x1)
                (natp x1))
           (<= (mmp-encode-c-max map) x1))
  :rule-classes :linear)

Theorem: mmp-encode-c-max-leq-when-mmp-encode-c-max.existsp-rewrite

(defthm mmp-encode-c-max-leq-when-mmp-encode-c-max.existsp-rewrite
  (implies (and (mmp-encode-c-max.existsp map)
                (mmp-encode-c-max.uboundp map x1)
                (natp x1))
           (<= (mmp-encode-c-max map) x1)))

Theorem: mmp-encode-c-max.existsp-when-nonempty-and-bounded

(defthm mmp-encode-c-max.existsp-when-nonempty-and-bounded
  (implies (and (natp x0)
                (mmp-encode-c-max.elementp map x0)
                (natp x1)
                (mmp-encode-c-max.uboundp map x1))
           (mmp-encode-c-max.existsp map))
  :rule-classes nil)

Theorem: mmp-encode-c-max.equal-when-member-and-ubound

(defthm mmp-encode-c-max.equal-when-member-and-ubound
  (implies (and (natp x)
                (mmp-encode-c-max.elementp map x)
                (mmp-encode-c-max.uboundp map x))
           (equal (mmp-encode-c-max map) x))
  :rule-classes nil)

Theorem: mmp-encode-c-max.elementp-of-nibblelist-bytelist-mfix-map

(defthm mmp-encode-c-max.elementp-of-nibblelist-bytelist-mfix-map
  (equal (mmp-encode-c-max.elementp (nibblelist-bytelist-mfix map)
                                    x)
         (mmp-encode-c-max.elementp map x)))

Theorem: mmp-encode-c-max.elementp-nibblelist-bytelist-mequiv-congruence-on-map

(defthm
 mmp-encode-c-max.elementp-nibblelist-bytelist-mequiv-congruence-on-map
 (implies (nibblelist-bytelist-mequiv map map-equiv)
          (equal (mmp-encode-c-max.elementp map x)
                 (mmp-encode-c-max.elementp map-equiv x)))
 :rule-classes :congruence)

Theorem: mmp-encode-c-max.elementp-of-nfix-x

(defthm mmp-encode-c-max.elementp-of-nfix-x
  (equal (mmp-encode-c-max.elementp map (nfix x))
         (mmp-encode-c-max.elementp map x)))

Theorem: mmp-encode-c-max.elementp-nat-equiv-congruence-on-x

(defthm mmp-encode-c-max.elementp-nat-equiv-congruence-on-x
  (implies (acl2::nat-equiv x x-equiv)
           (equal (mmp-encode-c-max.elementp map x)
                  (mmp-encode-c-max.elementp map x-equiv)))
  :rule-classes :congruence)

Theorem: mmp-encode-c-max.elementp-when-not-natp-x

(defthm mmp-encode-c-max.elementp-when-not-natp-x
  (implies (and (syntaxp (not (equal x ''0)))
                (not (natp x)))
           (equal (mmp-encode-c-max.elementp map x)
                  (mmp-encode-c-max.elementp map 0))))

Theorem: mmp-encode-c-max.uboundp-of-nibblelist-bytelist-mfix-map

(defthm mmp-encode-c-max.uboundp-of-nibblelist-bytelist-mfix-map
  (equal (mmp-encode-c-max.uboundp (nibblelist-bytelist-mfix map)
                                   x)
         (mmp-encode-c-max.uboundp map x)))

Theorem: mmp-encode-c-max.uboundp-nibblelist-bytelist-mequiv-congruence-on-map

(defthm
 mmp-encode-c-max.uboundp-nibblelist-bytelist-mequiv-congruence-on-map
 (implies (nibblelist-bytelist-mequiv map map-equiv)
          (equal (mmp-encode-c-max.uboundp map x)
                 (mmp-encode-c-max.uboundp map-equiv x)))
 :rule-classes :congruence)

Theorem: mmp-encode-c-max.uboundp-of-nfix-x

(defthm mmp-encode-c-max.uboundp-of-nfix-x
  (equal (mmp-encode-c-max.uboundp map (nfix x))
         (mmp-encode-c-max.uboundp map x)))

Theorem: mmp-encode-c-max.uboundp-nat-equiv-congruence-on-x

(defthm mmp-encode-c-max.uboundp-nat-equiv-congruence-on-x
  (implies (acl2::nat-equiv x x-equiv)
           (equal (mmp-encode-c-max.uboundp map x)
                  (mmp-encode-c-max.uboundp map x-equiv)))
  :rule-classes :congruence)

Theorem: mmp-encode-c-max.existsp-of-nibblelist-bytelist-mfix-map

(defthm mmp-encode-c-max.existsp-of-nibblelist-bytelist-mfix-map
  (equal (mmp-encode-c-max.existsp (nibblelist-bytelist-mfix map))
         (mmp-encode-c-max.existsp map)))

Theorem: mmp-encode-c-max.existsp-nibblelist-bytelist-mequiv-congruence-on-map

(defthm
 mmp-encode-c-max.existsp-nibblelist-bytelist-mequiv-congruence-on-map
 (implies (nibblelist-bytelist-mequiv map map-equiv)
          (equal (mmp-encode-c-max.existsp map)
                 (mmp-encode-c-max.existsp map-equiv)))
 :rule-classes :congruence)

Theorem: mmp-encode-c-max-set-nonempty

(defthm mmp-encode-c-max-set-nonempty
  (mmp-encode-c-max.elementp map 0))

Theorem: mmp-encode-c-max-set-bounded

(defthm mmp-encode-c-max-set-bounded
  (implies (and (nibblelist-bytelist-mapp map)
                (not (omap::emptyp map)))
           (mmp-encode-c-max.uboundp
                map
                (nibblelist-bytelist-map-sup-len-key map))))

Theorem: mmp-encode-c-max-exists

(defthm mmp-encode-c-max-exists
  (implies (and (nibblelist-bytelist-mapp map)
                (not (omap::emptyp map)))
           (mmp-encode-c-max.existsp map)))

Theorem: nibblelist-bytelist-map-sup-len-key-geq-mmp-encode-c-max

(defthm nibblelist-bytelist-map-sup-len-key-geq-mmp-encode-c-max
  (implies (and (nibblelist-bytelist-mapp map)
                (not (omap::emptyp map)))
           (>= (nibblelist-bytelist-map-sup-len-key map)
               (mmp-encode-c-max map)))
  :rule-classes :linear)

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

(defthm nibblelist-bytelist-map-sup-len-key-geq-element
  (implies (and (nibblelist-bytelist-mapp map)
                (not (omap::emptyp map))
                (mmp-encode-c-max.elementp map x))
           (>= (nibblelist-bytelist-map-sup-len-key map)
               (nfix x)))
  :rule-classes :linear)

Theorem: nibblelist-bytelist-map-sup-len-key-neq-element-when-2+-keys

(defthm nibblelist-bytelist-map-sup-len-key-neq-element-when-2+-keys
  (implies (and (nibblelist-bytelist-mapp map)
                (not (omap::emptyp map))
                (not (equal (omap::size map) 1))
                (natp x)
                (mmp-encode-c-max.elementp map x))
           (not (equal (nibblelist-bytelist-map-sup-len-key map)
                       x))))

Theorem: mmp-encode-c-max-element-leq-len-key

(defthm mmp-encode-c-max-element-leq-len-key
  (implies (and (nibblelist-bytelist-mapp map)
                (natp x)
                (mmp-encode-c-max.elementp map x)
                (omap::assoc key map))
           (<= x (len key)))
  :rule-classes
  ((:linear :trigger-terms ((mmp-encode-c-max.elementp map x)))))

Theorem: mmp-encode-c-max-leq-len-key

(defthm mmp-encode-c-max-leq-len-key
  (implies (and (nibblelist-bytelist-mapp map)
                (not (omap::emptyp map))
                (omap::assoc key map))
           (<= (mmp-encode-c-max map) (len key)))
  :rule-classes ((:linear :trigger-terms ((mmp-encode-c-max map)))))

Theorem: mmp-encode-c-max.elementp-of-emptyp-map

(defthm mmp-encode-c-max.elementp-of-emptyp-map
  (implies (and (nibblelist-bytelist-mapp map)
                (omap::emptyp map))
           (mmp-encode-c-max.elementp map x)))