• 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
    • Transaction

    Make-transaction

    Basic constructor macro for transaction structures.

    Syntax
    (make-transaction [:nonce <nonce>] 
                      [:gas-price <gas-price>] 
                      [:gas-limit <gas-limit>] 
                      [:to <to>] 
                      [:value <value>] 
                      [:init/data <init/data>] 
                      [:sign-v <sign-v>] 
                      [:sign-r <sign-r>] 
                      [:sign-s <sign-s>]) 
    

    This is the usual way to construct transaction structures. It simply conses together a structure with the specified fields.

    This macro generates a new transaction structure from scratch. See also change-transaction, which can "change" an existing structure, instead.

    Definition

    This is an ordinary make- macro introduced by fty::defprod.

    Macro: make-transaction

    (defmacro make-transaction (&rest args)
      (std::make-aggregate 'transaction
                           args
                           '((:nonce)
                             (:gas-price)
                             (:gas-limit)
                             (:to)
                             (:value)
                             (:init/data)
                             (:sign-v)
                             (:sign-r)
                             (:sign-s))
                           'make-transaction
                           nil))

    Function: transaction

    (defun transaction (nonce gas-price gas-limit
                              to value init/data sign-v sign-r sign-s)
      (declare (xargs :guard (and (wordp nonce)
                                  (wordp gas-price)
                                  (wordp gas-limit)
                                  (maybe-byte-list20p to)
                                  (wordp value)
                                  (byte-listp init/data)
                                  (natp sign-v)
                                  (wordp sign-r)
                                  (wordp sign-s))))
      (declare (xargs :guard t))
      (let ((__function__ 'transaction))
        (declare (ignorable __function__))
        (b* ((nonce (mbe :logic (word-fix nonce)
                         :exec nonce))
             (gas-price (mbe :logic (word-fix gas-price)
                             :exec gas-price))
             (gas-limit (mbe :logic (word-fix gas-limit)
                             :exec gas-limit))
             (to (mbe :logic (maybe-byte-list20-fix to)
                      :exec to))
             (value (mbe :logic (word-fix value)
                         :exec value))
             (init/data (mbe :logic (byte-list-fix init/data)
                             :exec init/data))
             (sign-v (mbe :logic (nfix sign-v) :exec sign-v))
             (sign-r (mbe :logic (word-fix sign-r)
                          :exec sign-r))
             (sign-s (mbe :logic (word-fix sign-s)
                          :exec sign-s)))
          (cons :transaction (list nonce gas-price gas-limit to value
                                   init/data sign-v sign-r sign-s)))))