• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
        • Command-error
        • Sign
        • Init-from-mnemonic
        • Command-error-message
        • Stat
        • Next-key
        • Init-from-entropy
        • Process-command
        • Transaction-message
        • Maybe-command-error
        • Maybe-stat
        • Check-stat-file-present
        • Valid-key-path-p
        • String-to-byte-list
        • Load-stat
        • Mnemonic-message
        • Process-sign
        • Process-init-from-entropy
        • All-valid-key-paths-p
        • String-to-word
        • String-to-nat
        • Process-next-key
        • Wallet
        • Process-init-from-mnemonic
        • Check-stat-file-absent
        • Stat-wfp
        • Save-stat
        • Stat-addresses-bounded-p
        • Stat-all-valid-key-paths-p
        • Stat-priv-keys-p
        • Stat-root-depth-zero-p
        • Stat-path-prefix-in-tree-p
        • Crypto-hdwallet-executable
        • *stat-filepath*
        • *key-path-prefix*
        • *coin-type-index*
        • *purpose-index*
        • *external-chain-index*
        • *command-name-init-from-mnemonic*
        • *command-name-init-from-entropy*
        • *account-index*
        • *command-name-sign*
        • *command-name-next-key*
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • Event-macros
      • C
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Crypto-hdwallet

Transaction-message

Build a message that describes a (signed) transaction.

Signature

(transaction-message transaction) → msg

Arguments

transaction — Guard (byte-listp transaction).

Returns

msg — Type (msgp msg).

When signing a transaction, the signed transaction (a list of bytes) must be submitted to the Ethereum network. Since this wallet is meant to run on an air-gapped machine, the transaction must be copied to a connected machine for submission. Thus, the command to sign the transaction must show it on the screen.

This function builds a message that consists of all the bytes, each in hex form, separated by single spaces, 16 bytes per line, each line indented by two spaces. In fact, this function handles any list of bytes, not just specifically signed transactions.

Definitions and Theorems

Function: transaction-message-line-aux

(defun transaction-message-line-aux (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (cond ((endp bytes) "")
        (t (cat " "
                (ubyte8s=>hexstring (list (car bytes)))
                (transaction-message-line-aux (cdr bytes))))))

Theorem: stringp-of-transaction-message-line-aux

(defthm stringp-of-transaction-message-line-aux
  (b* ((string (transaction-message-line-aux bytes)))
    (stringp string))
  :rule-classes :rewrite)

Function: transaction-message-line

(defun transaction-message-line (bytes)
  (declare (xargs :guard (byte-listp bytes)))
  (declare (xargs :guard (consp bytes)))
  (msg " ~@0~%"
       (transaction-message-line-aux bytes)))

Theorem: msgp-of-transaction-message-line

(defthm msgp-of-transaction-message-line
  (b* ((msg (transaction-message-line bytes)))
    (msgp msg))
  :rule-classes :rewrite)

Function: transaction-message

(defun transaction-message (transaction)
  (declare (xargs :guard (byte-listp transaction)))
  (cond ((endp transaction) "")
        ((< (len transaction) 16)
         (transaction-message-line transaction))
        (t (msg "~@0~@1"
                (transaction-message-line (take 16 transaction))
                (transaction-message (nthcdr 16 transaction))))))

Theorem: msgp-of-transaction-message

(defthm msgp-of-transaction-message
  (b* ((msg (transaction-message transaction)))
    (msgp msg))
  :rule-classes :rewrite)