Attachment of bip32-valid-depths-p-exec to bip32-valid-depths-p.
The fact that the executable function satisfies all the constraints of the non-executable one follows from their equivalence.
We prove two of the constraints as separate theorems. Attempts at proving the attachment directly fail.
Theorem:
(defthm bip32-valid-depths-p-exec-constraint1 (equal (bip32-valid-depths-p-exec init paths) (let ((path (bip32-valid-depths-p-witness init paths))) (implies (in path (bip32-path-sfix paths)) (bytep (+ (byte-fix init) (len path)))))))
Theorem:
(defthm bip32-valid-depths-p-exec-constraint2 (implies (bip32-valid-depths-p-exec init paths) (implies (in path (bip32-path-sfix paths)) (bytep (+ (byte-fix init) (len path))))))