Executable version of bip32-valid-depths-p.
(bip32-valid-depths-p-exec init paths) → yes/no
We iterate through the paths in the set, checking that each one has a valid depth.
If this executable function holds, then any member of the set satisfies the depth validity condition. This fact is used in the correctness proof of the attachment.
Function:
(defun bip32-valid-depths-p-exec (init paths) (declare (xargs :guard (and (bytep init) (bip32-path-setp paths)))) (or (not (mbt (bip32-path-setp paths))) (emptyp paths) (and (bytep (+ (byte-fix init) (len (head paths)))) (bip32-valid-depths-p-exec init (tail paths)))))
Theorem:
(defthm booleanp-of-bip32-valid-depths-p-exec (b* ((yes/no (bip32-valid-depths-p-exec init paths))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm bip32-valid-depths-p-exec-of-byte-fix-init (equal (bip32-valid-depths-p-exec (byte-fix init) paths) (bip32-valid-depths-p-exec init paths)))
Theorem:
(defthm bip32-valid-depths-p-exec-byte-equiv-congruence-on-init (implies (acl2::byte-equiv init init-equiv) (equal (bip32-valid-depths-p-exec init paths) (bip32-valid-depths-p-exec init-equiv paths))) :rule-classes :congruence)
Theorem:
(defthm bip32-valid-depths-p-exec-of-bip32-path-sfix-paths (equal (bip32-valid-depths-p-exec init (bip32-path-sfix paths)) (bip32-valid-depths-p-exec init paths)))
Theorem:
(defthm bip32-valid-depths-p-exec-bip32-path-set-equiv-congruence-on-paths (implies (bip32-path-set-equiv paths paths-equiv) (equal (bip32-valid-depths-p-exec init paths) (bip32-valid-depths-p-exec init paths-equiv))) :rule-classes :congruence)
Theorem:
(defthm bip32-valid-depths-p-exec-member (implies (and (bip32-valid-depths-p-exec init paths) (in path (bip32-path-sfix paths))) (bytep (+ (byte-fix init) (len path)))))