Executable version of bip32-valid-keys-p.
(bip32-valid-keys-p-exec root paths) → 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.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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)))))