		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-trees

Bip32-valid-depths-p

Check if all the key depths in a (tree's) set of paths are valid.

When a key is serialized, its depth in the tree is represented in 1 byte. Thus, in order for keys to be serializable, the maximum depth must be 255. Since the master key has depth 0 [BIP32], the depth of a key is the length of the key's path.

When sharing key subtrees as explained in the use cases in [BIP32], the root key is not the master key, but some descendant of the master key. That descendant has a non-0 depth in the supertree rooted at the master key. Thus, the ``real'' depth of each key in the subtree is the depth within the subtree plus the depth of the subtree's root; this ``real'' depth is the one in the supertree rooted at the master key. The init argument of this function is the depth of the root (i.e. the ``initial'' depth); this function checks that the depth in the subtree plus init does not exceed 255. If the subtree coincides with the supertree, then init is 0.

Even though this function is applied to index trees, it can be defined on general sets of paths.

We introduce this function as a constrained function, so that we can make an executable attachment for it (in bip32-executable.lisp). Since currently std::define-sk does not support defun-sk's :constrain and defun-sk forces the guard to t when :constrain is t, we use an encapsulate for now to introduce this function. A std::define-sk is used to locally define the witness, which also guard-verifies the matrix of the function, as additional validation.

The singleton tree consisting of just the root (represented as the singleton set consisting of the empty path), trivially satisfies this depth validity condition.

Extending a path of an index tree preserves the validity of the key depths, provided that the depth of the path being extended is below 255.

The tail of a set of paths with valid depths also has all valid depths.

Definitions and Theorems

Theorem: bip32-valid-depths-p-definition

(defthm bip32-valid-depths-p-definition
  (equal (bip32-valid-depths-p init paths)
         (let ((path (bip32-valid-depths-p-witness init paths)))
           (implies (in path (bip32-path-sfix paths))
                    (bytep (+ (byte-fix init) (len path))))))
  :rule-classes :definition)

Theorem: booleanp-of-bip32-valid-depths-p

(defthm booleanp-of-bip32-valid-depths-p
  (booleanp (bip32-valid-depths-p init paths))
  :rule-classes (:rewrite :type-prescription))

Theorem: bip32-valid-depths-p-necc

(defthm bip32-valid-depths-p-necc
  (implies (bip32-valid-depths-p init paths)
           (implies (in path (bip32-path-sfix paths))
                    (bytep (+ (byte-fix init) (len path))))))

Theorem: bip32-valid-depths-p-of-byte-fix-init

(defthm bip32-valid-depths-p-of-byte-fix-init
  (equal (bip32-valid-depths-p (byte-fix init)
                               paths)
         (bip32-valid-depths-p init paths)))

Theorem: bip32-valid-depths-p-byte-equiv-congruence-on-init

(defthm bip32-valid-depths-p-byte-equiv-congruence-on-init
  (implies (acl2::byte-equiv init init-equiv)
           (equal (bip32-valid-depths-p init paths)
                  (bip32-valid-depths-p init-equiv paths)))
  :rule-classes :congruence)

Theorem: bip32-valid-depths-p-of-bip32-path-sfix-paths

(defthm bip32-valid-depths-p-of-bip32-path-sfix-paths
  (equal (bip32-valid-depths-p init (bip32-path-sfix paths))
         (bip32-valid-depths-p init paths)))

Theorem: bip32-valid-depths-p-bip32-path-set-equiv-congruence-on-paths

(defthm
      bip32-valid-depths-p-bip32-path-set-equiv-congruence-on-paths
  (implies (bip32-path-set-equiv paths paths-equiv)
           (equal (bip32-valid-depths-p init paths)
                  (bip32-valid-depths-p init paths-equiv)))
  :rule-classes :congruence)

Theorem: bip32-valid-depths-p-of-singleton-empty-path

(defthm bip32-valid-depths-p-of-singleton-empty-path
  (bip32-valid-depths-p init '(nil)))

Theorem: bip32-valid-depths-p-of-insert-of-rcons

(defthm bip32-valid-depths-p-of-insert-of-rcons
 (implies (and (bip32-path-setp paths)
               (bip32-valid-depths-p init paths)
               (in path paths)
               (< (+ (byte-fix init) (len path)) 255)
               (ubyte32p index))
          (bip32-valid-depths-p init
                                (insert (rcons index path) paths))))

Theorem: bip32-valid-depths-p-of-tail

(defthm bip32-valid-depths-p-of-tail
  (implies (and (bip32-path-setp paths)
                (bip32-valid-depths-p init paths))
           (bip32-valid-depths-p init (tail paths))))

Subtopics

Bip32-valid-depths-p-executable-attachment: Executable attachment for bip32-valid-depths-p.