• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
      • Zfc
      • Acre
      • Milawa
      • Smtlink
      • Abnf
      • Vwsim
      • Isar
      • Pfcs
      • Wp-gen
      • Dimacs-reader
      • Legacy-defrstobj
      • Proof-checker-array
      • Soft
      • C
      • Farray
      • Rp-rewriter
      • Instant-runoff-voting
      • Imp-language
      • Sidekick
      • Leftist-trees
      • Java
      • Taspi
      • Riscv
      • Bitcoin
      • Des
      • 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
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Aleo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Community
      • Proof-automation
      • ACL2
      • Macro-libraries
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • 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)))))