		Search-engine friendly clone of the ACL2 documentation.

Bip32-key-trees

Bip32-path-set-closedp

Check if a set of key tree paths is closed under prefix.

The set of paths of a tree is closed under prefix: if a path is in the tree, every prefix path is in the tree too. Thus, in order to represent a tree (of keys), a set of paths must satisfy this condition.

The condition that the prefix is a true list is needed because prefixp ignores the final cdrs. Without this condition, prefixes that are not true lists would be required to be in the set, which would be impossible because the set's elements are all true lists.

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.

A closed non-empty set of paths always contains the empty path, because the empty path is a prefix of every path.

The singleton set consisting of the empty path is closed.

If a set of paths is closed under prefix, extending a path in the set (more precisely, extending the set with the path obtained by extending an existing path in the set) results in a set of paths that is still closed under prefix. This is because every strict prefix of the new path is also a prefix of the existing path, and therefore already in the set by hypothesis.

Definitions and Theorems

Theorem: bip32-path-set-closedp-definition

(defthm bip32-path-set-closedp-definition
  (equal (bip32-path-set-closedp paths)
         (mv-let (path prefix)
                 (bip32-path-set-closedp-witness paths)
           (b* ((paths (bip32-path-sfix paths)))
             (implies (and (in path paths)
                           (true-listp prefix)
                           (prefixp prefix path))
                      (in prefix paths)))))
  :rule-classes :definition)

Theorem: booleanp-of-bip32-path-set-closedp

(defthm booleanp-of-bip32-path-set-closedp
  (booleanp (bip32-path-set-closedp paths))
  :rule-classes (:rewrite :type-prescription))

Theorem: bip32-path-set-closedp-necc

(defthm bip32-path-set-closedp-necc
  (implies (bip32-path-set-closedp paths)
           (b* ((paths (bip32-path-sfix paths)))
             (implies (and (in path paths)
                           (true-listp prefix)
                           (prefixp prefix path))
                      (in prefix paths)))))

Theorem: bip32-path-set-closedp-of-bip32-path-sfix-paths

(defthm bip32-path-set-closedp-of-bip32-path-sfix-paths
  (equal (bip32-path-set-closedp (bip32-path-sfix paths))
         (bip32-path-set-closedp paths)))

Theorem: bip32-path-set-closedp-bip32-path-set-equiv-congruence-on-paths

(defthm
    bip32-path-set-closedp-bip32-path-set-equiv-congruence-on-paths
  (implies (bip32-path-set-equiv paths paths-equiv)
           (equal (bip32-path-set-closedp paths)
                  (bip32-path-set-closedp paths-equiv)))
  :rule-classes :congruence)

Theorem: empty-path-in-closed-nonempty-bip32-path-set

(defthm empty-path-in-closed-nonempty-bip32-path-set
  (implies (and (bip32-path-setp paths)
                (not (emptyp paths))
                (bip32-path-set-closedp paths))
           (in nil paths)))

Theorem: bip32-path-set-closedp-of-singleton-empty-path

(defthm bip32-path-set-closedp-of-singleton-empty-path
  (bip32-path-set-closedp '(nil)))

Theorem: bip32-path-set-closedp-of-insert-of-rcons

(defthm bip32-path-set-closedp-of-insert-of-rcons
  (implies
       (and (bip32-path-setp paths)
            (bip32-path-set-closedp paths)
            (in path paths)
            (ubyte32p index))
       (bip32-path-set-closedp (insert (rcons index path) paths))))

Subtopics

Bip32-path-set-closedp-executable-attachment: Executable attachment for bip32-path-set-closedp.