Turn an entropy value into a seed.
(bip39-entropy-to-seed entropy passphrase) → seed
This combines bip39-entropy-to-mnemonic and bip39-mnemonic-to-seed.
The limit on the passphrase is the same as in bip39-mnemonic-to-seed. The mnemonic is always below the limit in bip39-mnemonic-to-seed: see the upper bound theorem for bip39-entropy-to-mnemonic.
Function:
(defun bip39-entropy-to-seed (entropy passphrase) (declare (xargs :guard (and (bip39-entropyp entropy) (stringp passphrase)))) (declare (xargs :guard (< (length passphrase) (- (expt 2 125) (+ 128 4 8))))) (b* ((mnemonic (bip39-entropy-to-mnemonic entropy)) (seed (bip39-mnemonic-to-seed mnemonic passphrase))) seed))
Theorem:
(defthm byte-listp-of-bip39-entropy-to-seed (b* ((seed (bip39-entropy-to-seed entropy passphrase))) (byte-listp seed)) :rule-classes :rewrite)
Theorem:
(defthm len-of-bip39-entropy-to-seed (equal (len (bip39-entropy-to-seed entropy passphrase)) 64))
Theorem:
(defthm bip39-entropy-to-seed-of-bip39-entropy-fix-entropy (equal (bip39-entropy-to-seed (bip39-entropy-fix entropy) passphrase) (bip39-entropy-to-seed entropy passphrase)))
Theorem:
(defthm bip39-entropy-to-seed-bip39-entropy-equiv-congruence-on-entropy (implies (bip39-entropy-equiv entropy entropy-equiv) (equal (bip39-entropy-to-seed entropy passphrase) (bip39-entropy-to-seed entropy-equiv passphrase))) :rule-classes :congruence)
Theorem:
(defthm bip39-entropy-to-seed-of-str-fix-passphrase (equal (bip39-entropy-to-seed entropy (acl2::str-fix passphrase)) (bip39-entropy-to-seed entropy passphrase)))
Theorem:
(defthm bip39-entropy-to-seed-streqv-congruence-on-passphrase (implies (acl2::streqv passphrase passphrase-equiv) (equal (bip39-entropy-to-seed entropy passphrase) (bip39-entropy-to-seed entropy passphrase-equiv))) :rule-classes :congruence)