		Search-engine friendly clone of the ACL2 documentation.

Bip32-valid-depths-p-executable-attachment

Bip32-valid-depths-p-exec

Executable version of bip32-valid-depths-p.

Signature
(bip32-valid-depths-p-exec init paths) → yes/no
Arguments: init — Guard (bytep init).; 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 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.

Definitions and Theorems

Function: bip32-valid-depths-p-exec

(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: booleanp-of-bip32-valid-depths-p-exec

(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: bip32-valid-depths-p-exec-of-byte-fix-init

(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: bip32-valid-depths-p-exec-byte-equiv-congruence-on-init

(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: bip32-valid-depths-p-exec-of-bip32-path-sfix-paths

(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: bip32-valid-depths-p-exec-bip32-path-set-equiv-congruence-on-paths

(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: bip32-valid-depths-p-exec-member

(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)))))