• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Bitcoin
        • Ethereum
          • Mmp-trees
          • Semaphore
          • Database
          • Cryptography
          • Rlp
          • Transactions
            • Make-signed-transaction
            • Transaction
              • Transaction-fix
              • Make-transaction
              • Transaction-equiv
              • Transactionp
              • Change-transaction
              • Transaction->init/data
              • Transaction->gas-price
              • Transaction->gas-limit
              • Transaction->value
              • Transaction->to
              • Transaction->sign-v
              • Transaction->sign-s
              • Transaction->sign-r
              • Transaction->nonce
            • Maybe-byte-list20
            • Rlp-decode-transaction
            • Rlp-encode-transaction
            • Rlp-transaction-encoding-p
          • Hex-prefix
          • Basics
          • Addresses
        • Yul
        • Zcash
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Transactions

Transaction

Fixtype of transactions.

This is a product type introduced by fty::defprod.

Fields
nonce — word
gas-price — word
gas-limit — word
to — maybe-byte-list20
value — word
init/data — byte-list
sign-v — natp
sign-r — word
sign-s — word

A transaction is a 9-tuple [YP:(15)]. The type of each component is specified in [YP:(16)].

We use words to model natural numbers in \mathbb{N}_{256}: this is the type of the nonce, gas price, gas limit, and value fields.

The type of the recipient field is maybe-byte-list20. See the documentation of that fixtype for details.

The sixth component of the tuple is always a byte array, whether it is initialization code (when the recipient is nil) or it is data (when the recipient is an address).

The remaining three components are for the signature. The \mathbf{r} and \mathbf{s} components are words. The other signature component is \mathbf{v} in the text that describes it in [YP:4.2], but it is denoted as T_{\mathrm{w}} in [YP:(15)] and [YP:(16)] (presumably to avoid a conflict with the T_{\mathrm{v}} value component). We pick sign-v (instead of sign-w) for the corresponding field name in our product fixtype. However, there is an issue with the type of this component: [YP:(16)] says that it is a natural number below 32, but [YP:F] says that T_{\mathrm{w}} may be a chain identifier doubled plus 35 or 36, in which case it is above 32. It looks like [YP:F] was updated according to [EIP155], while [YP:4.2] was not; this EIP describes an improved signature scheme that involves chain identifiers. [EIP155] lists some chain identifiers, one of which is larger than a byte. So we use the library type nat for this component of a transaction.

Subtopics

Transaction-fix
Fixing function for transaction structures.
Make-transaction
Basic constructor macro for transaction structures.
Transaction-equiv
Basic equivalence relation for transaction structures.
Transactionp
Recognizer for transaction structures.
Change-transaction
Modifying constructor for transaction structures.
Transaction->init/data
Get the init/data field from a transaction.
Transaction->gas-price
Get the gas-price field from a transaction.
Transaction->gas-limit
Get the gas-limit field from a transaction.
Transaction->value
Get the value field from a transaction.
Transaction->to
Get the to field from a transaction.
Transaction->sign-v
Get the sign-v field from a transaction.
Transaction->sign-s
Get the sign-s field from a transaction.
Transaction->sign-r
Get the sign-r field from a transaction.
Transaction->nonce
Get the nonce field from a transaction.