|
|
|---|
|
|
|
|---|
Map each 11-bit index to a word from the predefined wordlist, which consists of 2,048 words.
(bip39-word-indexes-to-words indexes) → words
The resulting words have always a length bounded by the maximum length of the English words, namely 8. This is because the words are taken from the English worlist. This theorem is proved from the fact that nth applied to *bip39-english-words* always yields a value whose length is less than or equal to 8. This fact should be provable directly by forcing the expansion of nth, but it seem to take a long time, presumably due to the length of the wordlist. So instead we prove it via a few local lemmas that use a locally defined function.
Function:
(defun bip39-word-indexes-to-words (indexes) (declare (xargs :guard (ubyte11-listp indexes))) (cond ((endp indexes) nil) (t (cons (nth (ubyte11-fix (car indexes)) *bip39-english-words*) (bip39-word-indexes-to-words (cdr indexes))))))
Theorem:
(defthm string-listp-of-bip39-word-indexes-to-words (b* ((words (bip39-word-indexes-to-words indexes))) (string-listp words)) :rule-classes :rewrite)
Theorem:
(defthm len-of-bip39-word-indexes-to-words (equal (len (bip39-word-indexes-to-words indexes)) (len indexes)))
Theorem:
(defthm bip39-words-bounded-p-of-bip39-word-indexes-to-words (bip39-english-words-bound-p (bip39-word-indexes-to-words indexes)))
Theorem:
(defthm bip39-word-indexes-to-words-of-ubyte11-list-fix-indexes (equal (bip39-word-indexes-to-words (acl2::ubyte11-list-fix indexes)) (bip39-word-indexes-to-words indexes)))
Theorem:
(defthm bip39-word-indexes-to-words-ubyte11-list-equiv-congruence-on-indexes (implies (acl2::ubyte11-list-equiv indexes indexes-equiv) (equal (bip39-word-indexes-to-words indexes) (bip39-word-indexes-to-words indexes-equiv))) :rule-classes :congruence)