		Search-engine friendly clone of the ACL2 documentation.

Bip32-valid-keys-p-executable-attachment

Bip32-valid-keys-p-exec

Executable version of bip32-valid-keys-p.

Signature
(bip32-valid-keys-p-exec root paths) → yes/no
Arguments: root — Guard (bip32-ext-key-p root).; paths — Guard (bip32-path-setp paths).
Returns: yes/no — Type (booleanp yes/no).

We iterate through the paths in the set, checking that each one has a valid key.

If this executable function holds, then any member of the set satisfies the key validity condition. This fact is used in the correctness proof of the attachment.

Definitions and Theorems

Function: bip32-valid-keys-p-exec

(defun bip32-valid-keys-p-exec (root paths)
  (declare (xargs :guard (and (bip32-ext-key-p root)
                              (bip32-path-setp paths))))
  (or (not (mbt (bip32-path-setp paths)))
      (emptyp paths)
      (and (b* (((mv error? &)
                 (bip32-ckd* root (head paths))))
             (not error?))
           (bip32-valid-keys-p-exec root (tail paths)))))

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

(defthm booleanp-of-bip32-valid-keys-p-exec
  (b* ((yes/no (bip32-valid-keys-p-exec root paths)))
    (booleanp yes/no))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Theorem: bip32-valid-keys-p-exec-member

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