• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
      • Bip32
      • Bech32
      • Bip39
      • Bip44
      • Base58
        • Base58-encode
        • Base58-decode
        • Base58-character
        • Base58-value
        • Base58-val=>char
        • Base58-vals=>chars
        • Base58-chars=>vals
          • Base58-vals<=>chars-inverses-theorems
        • Base58-char=>val
        • *base58-characters*
        • Base58-value-list
        • Base58-character-list
        • *base58-zero*
      • Bip43
      • Bytes
      • Base58check
      • Cryptography
      • Bip-350
      • Bip-173
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Base58

Base58-chars=>vals

Lift base58-char=>val to lists.

Signature

(base58-chars=>vals chars) → vals

Arguments

chars — Guard (base58-character-listp chars).

Returns

vals — Type (base58-value-listp vals).

Definitions and Theorems

Function: base58-chars=>vals

(defun base58-chars=>vals (chars)
  (declare (xargs :guard (base58-character-listp chars)))
  (let ((__function__ 'base58-chars=>vals))
    (declare (ignorable __function__))
    (cond ((endp chars) nil)
          (t (cons (base58-char=>val (car chars))
                   (base58-chars=>vals (cdr chars)))))))

Theorem: base58-value-listp-of-base58-chars=>vals

(defthm base58-value-listp-of-base58-chars=>vals
  (b* ((vals (base58-chars=>vals chars)))
    (base58-value-listp vals))
  :rule-classes :rewrite)

Theorem: len-of-base58-chars=>vals

(defthm len-of-base58-chars=>vals
  (equal (len (base58-chars=>vals chars))
         (len chars)))

Theorem: base58-chars=>vals-of-append

(defthm base58-chars=>vals-of-append
  (equal (base58-chars=>vals (append chars1 chars2))
         (append (base58-chars=>vals chars1)
                 (base58-chars=>vals chars2))))

Theorem: base58-chars=>vals-of-repeat

(defthm base58-chars=>vals-of-repeat
  (equal (base58-chars=>vals (repeat n char))
         (repeat n (base58-char=>val char))))

Theorem: base58-chars=>vals-of-base58-character-list-fix-chars

(defthm base58-chars=>vals-of-base58-character-list-fix-chars
  (equal (base58-chars=>vals (base58-character-list-fix chars))
         (base58-chars=>vals chars)))

Theorem: base58-chars=>vals-base58-character-list-equiv-congruence-on-chars

(defthm
 base58-chars=>vals-base58-character-list-equiv-congruence-on-chars
 (implies (base58-character-list-equiv chars chars-equiv)
          (equal (base58-chars=>vals chars)
                 (base58-chars=>vals chars-equiv)))
 :rule-classes :congruence)

Subtopics

Base58-vals<=>chars-inverses-theorems

base58-vals=>chars and base58-chars=>vals are mutual inverses.