		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-trees

Bip32-valid-keys-p

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

Given a root key, every path in a tree must correspond to a valid key. That is, all the key derivations along the path must be valid.

This function checks this condition. This function is used to define key trees later.

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 key validity condition.

Extending a path of an index tree preserves the validity of the keys, provided that the key at the end of the new extended path is valid.

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

Definitions and Theorems

Theorem: bip32-valid-keys-p-definition

(defthm bip32-valid-keys-p-definition
  (equal (bip32-valid-keys-p root paths)
         (let ((path (bip32-valid-keys-p-witness root paths)))
           (implies (in path (bip32-path-sfix paths))
                    (not (mv-nth 0 (bip32-ckd* root path))))))
  :rule-classes :definition)

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

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

Theorem: bip32-valid-keys-p-necc

(defthm bip32-valid-keys-p-necc
  (implies (bip32-valid-keys-p root paths)
           (implies (in path (bip32-path-sfix paths))
                    (not (mv-nth 0 (bip32-ckd* root path))))))

Theorem: bip32-valid-keys-p-of-bip32-ext-key-fix-root

(defthm bip32-valid-keys-p-of-bip32-ext-key-fix-root
  (equal (bip32-valid-keys-p (bip32-ext-key-fix root)
                             paths)
         (bip32-valid-keys-p root paths)))

Theorem: bip32-valid-keys-p-bip32-ext-key-equiv-congruence-on-root

(defthm bip32-valid-keys-p-bip32-ext-key-equiv-congruence-on-root
  (implies (bip32-ext-key-equiv root root-equiv)
           (equal (bip32-valid-keys-p root paths)
                  (bip32-valid-keys-p root-equiv paths)))
  :rule-classes :congruence)

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

(defthm bip32-valid-keys-p-of-bip32-path-sfix-paths
  (equal (bip32-valid-keys-p root (bip32-path-sfix paths))
         (bip32-valid-keys-p root paths)))

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

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

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

(defthm bip32-valid-keys-p-of-singleton-empty-path
  (bip32-valid-keys-p root '(nil)))

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

(defthm bip32-valid-keys-p-of-insert-of-rcons
  (implies (and (bip32-path-setp paths)
                (bip32-valid-keys-p root paths)
                (in path paths)
                (ubyte32p index)
                (not (mv-nth 0
                             (bip32-ckd* root (rcons index path)))))
           (bip32-valid-keys-p root
                               (insert (rcons index path) paths))))

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

(defthm bip32-valid-keys-p-of-tail
  (implies (and (bip32-path-setp paths)
                (bip32-valid-keys-p root paths))
           (bip32-valid-keys-p root (tail paths))))

Subtopics

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