• Top
    • Documentation
      • Xdoc
        • Undocumented
          • Interp-flags
          • Simpcode
          • Npn4
          • Cutinfo
          • Glcp-config-p
          • Glmc-config-p
          • Defsvtv-args
          • Vl-renaming-alist-p
          • Vcd-pathmap-p
          • Vcd-idxhash-p
          • *atc-exec-binary-strict-pure-rules*
          • Ecut-wirename-alistp
          • Context
          • Incremental-extremize-config-p
          • Block-headerp
          • Ctrex-rule
          • Execution-environmentp
          • Glmc-fsm-p
          • Transactionp
            • Transaction
            • Make-transaction
            • Change-transaction
            • Honsed-transaction
            • Make-honsed-transaction
              • Transaction->value
              • Transaction->to
              • Transaction->sig-v
              • Transaction->sig-s
              • Transaction->sig-r
              • Transaction->nonce
              • Transaction->init-or-data
              • Transaction->gas-price
              • Transaction->gas-limit
            • Eqbylbp-config-p
            • Proof-obligation
            • Cgraph-edge
            • Wcp-instance-rule-p
            • Fgl-casesplit-config
            • Wcp-witness-rule-p
            • Obligation-hyp
            • Vl-parsestate
            • Ecutnames-p
            • Te-args
            • Fgl-satlink-monolithic-sat-config
            • Fn-info-elt-p
            • Wcp-template-p
            • Truth-idx
            • Polarity4
            • Phase-fsm-params
            • Propiso-info-p
            • Cutscore
            • Vl-rhs
            • Truth6
            • Constraint-tuple
            • Truth5
            • Truth4
            • Truth3
            • Svexl-node
            • Ringosc3
            • Prof-entry-p
            • Constraint-tuple-p
            • Fgl-rune
            • Stv-spec-p
            • Run-snippet-file-info
            • Svex-scc-consts
            • Fsm
            • Machine-statep
            • Xor-signature-p
            • Run-snippet-info
            • Svtv-precompose-data
            • Pipeline-setup
            • Maybe-svar-p
            • Svl-module
            • Maybe-fgl-generic-rule
            • Frames
            • Maybe-snippet-mismatch
            • Cpuid-info-p
            • Vl-warningtree
            • Maybe-proof-obligation
            • Svtv-override-check
            • Maybe-svtv-chase-evaldata
            • Fty-info
            • Prof-entry
            • Substatep
            • Vl-maybe-rhs
            • Vl-parsed-ports
            • Svex-context
            • Account-statep
            • Maybe-simpcode
            • Maybe-rational
            • Maybe-svex
            • Flatten-res
            • Svex-reduce-config
            • Fty-type
            • Rewrite
            • Snippet-info
            • Addnames-indices
            • Svtv*-phase
            • Segment-driver
            • Satlink-parser-state
            • Fgl-binder-rune
            • Congruence-rule
            • Snippet-mismatch
            • Vl-ctxexpr
            • Rsh-of-concat-table
            • Chase-position
            • Hyp-tuple-p
            • Glcp-obj-ctrex-p
            • Glcp-bit-ctrex-p
            • Block$-p
            • Boundrw-subst-p
            • Svtv-cyclephase
            • Svar-split
            • Scopetree
            • Flatnorm-res
            • Fgl-rule
            • Constraint-rule
            • Vl-user-paramsetting
            • Svtv-override-triple
            • Svtv-evaldata
            • Svtv-composedata
            • Width-of-svex-extn
            • Array-fieldinfo-p
            • Wcp-example-app-p
            • Svtv*-input
            • Svex-override-triple
            • Svar-override-triple
            • 3col4vecline
            • Constraint-rule-p
            • Vl-parsed-ports
            • Svtv-chase-evaldata
            • Svtv-assigns-override-config
            • Svex/index
            • Svl-env
            • Svl-aliasdb
            • Inverter
            • Fgl-binder-rule
            • Bvar-db-consistency-error
            • Wcp-lit-actions-p
            • Vcd-multivector-p
            • Svtv-fsm
            • Svexl
            • Constraint-instance
            • Vl-parsestate
            • Partsum-comp
            • Classname/params
            • Vcd-vector-p
            • Tmp-occ
            • Svl-occ
            • Svexllist
            • Svexl-alist
            • Integerp-of-svex-extn
            • Uninterpreted
            • Rw-pair
            • Vl-echar-raw
            • Vl-echar-raw
            • Use-set
            • Svtv-probe
            • Svex-phase-varname
            • Svex-cycle-varname
            • Range
            • Phase-fsm-config
            • Overridekey-syntaxcheck-data
            • Constraint
            • Alias
            • Sig
            • Sandwich
            • Cgraph-derivstate
            • Candidate-assign
            • Svex-alist-eval-equiv!
            • Svex-alist-eval-equiv
            • Scalar-fieldinfo-p
            • Fe-list-listp
            • Fgl-ev-congruence-rulelist-correct-p
            • N-outputs-dom-supergates-sweep-config
            • Svex-envlists-equivalent
            • Svex-alistlist-eval-equiv
            • Flatnorm-setup
            • G-map-tag
            • Obs-sdom-array
            • Dom-supergates-sweep-config
            • Truth4arr
            • Npn4arr
            • Syndef::acid4
            • Svex-envlists-similar
            • Svex-alist-compose-equiv
            • Sym-prod
            • Fgl-congruence-rune
            • Svex-envs-1mask-equiv
            • U32arr
            • Litarr
            • Aigtrans
            • Svexlist-eval-equiv
            • N-outputs-unreachability-config
            • Svex-eval-equiv
            • Unreachability-config
            • Keys-equiv
            • Vl-maybe-exprtype-list-p
            • Svex-alistlist
            • Svar-overridetype-p
            • Vcd-indexlist-p
            • Alternative-spec-listp
            • Variable-listp
            • Vcd-vectorlist-p
            • Vcd-multivectorlist-p
            • Field-spec-listp
            • Neteval-ordering
            • Prof-entrylist-p
            • Hyp-tuplelist-p
            • Glcp-obj-ctrexlist-p
            • Symbol-path-list-p
            • Pseudo-input-listp
            • Input-listp
            • Ecutname-list-p
            • Boundrw-substlist-p
            • Constraintlist
            • Fgl-object-bindings
            • Fgl-generic-rule
            • 4v-equiv
            • Sdm-instruction-table
            • Svexl-node-array
            • Sig-path
            • Func-alist
            • Fgl-generic-rune
            • Fgl-ev-iff-equiv
            • Pseudo-term-subst
            • Nth-lit-equiv
            • Frames-equiv
            • Eval-formula-equiv
            • Svex-s4env
            • Svex-env-keys-equiv
            • Svex-alist-keys-equiv
            • Pseudo-term-alist
            • Fgl-ev-equiv
            • Lits-equiv
            • Nth-nat-equiv
            • Faig-const-equiv
            • Bdd-equiv
            • Byte-list
            • Vl-user-paramsettings
            • Classname/params-unparam-map
            • Obligation-hyp-list
            • Svtv*-output-alist
            • Svtv*-input-alist
            • Svtv-probealist
            • Svtv-override-triplemap
            • Svtv-cyclephaselist
            • Svex/index-maybenat-alist
            • Svex-context-alist
            • Segment-driver-map
            • Rangemap
            • Fnsym-svexlistlist-alist
            • Tmp-occ-alist
            • Svl-module-alist
            • Svexl-node-alist
            • Occ-name-alist
            • Integerp-of-svex-extn-list
            • Alias-alist
            • Special-char-alist
            • Fty-info-alist
            • Bfr-updates
            • Term-equivs
            • Term-bvars
            • Sig-table
            • Fn-indices
            • Fgl-function-mode-alist
            • Ctrex-ruletable
            • Constraint-db
            • Congruence-rule-table
            • Cgraph-derivstates
            • Cgraph-alist
            • Cgraph
            • Casesplit-alist
            • Truthmap
            • Named-lit-list-map
            • Axi-map
            • Nth-equiv
            • Faig-fix-equiv
            • Vl-string/int-alist
            • Vl-reservedtable
            • Vl-echarlist
            • Vl-ctxexprlist
            • Vl-coredatatype-infolist
            • Vl-usertypes
            • Vl-coredatatype-infolist
            • Proof-obligation-list
            • Use-set-summaries
            • Svtv-rev-probealist
            • Svex/index-nat-alist
            • Svex/index-key-alist
            • Svex-key-alist
            • Svex-envlist
            • Svar-widths
            • Svar-width-map
            • Svar-splittab
            • Svar-proplist
            • Svar-key-alist
            • Rsh-of-concat-alist
            • Path-alist
            • Name-alist
            • Address-alist
            • Width-of-svex-extn-list
            • Svl-occ-alist
            • Svex-to-natp-alist
            • Symbol-string-alist
            • Symbol-integer-alist
            • Sym-nat-alist
            • String-string-alist
            • Fty-types
            • Fty-field-alist
            • Any-table
            • Obj-alist
            • Nat-nat-alist
            • Constraint-instancelist
            • Congruence-rulelist
            • Calist
            • Bvar-db-consistency-errorlist
            • Var-counts-alist
            • Pseudo-var-list
            • Equiv-contextslist
            • Nat-val-alistp
            • Id-neg-alist
            • String-keyed-alist-p
            • Snippet-table
            • Snippet-mismatch-list
            • Vl-reportcardkeylist
            • Partsumlist
            • Partsum-elt
            • Classname/paramslist
            • Vl-reportcardkeylist
            • Vl-locationlist
            • Vl-echarlist
            • Perm4-list
            • Svtv*-phaselist
            • Svtv-override-triplemaplist
            • Svtv-override-triplelist
            • Svtv-override-checklist
            • Svtv-name-lhs-map-list
            • Svex/indexlist
            • Svexlistlist
            • Svex-override-triplelist
            • Svex-contextlist
            • Svarlist-list
            • Svar-widthslist
            • Svar-overridetypelist
            • Svar-override-triplelist
            • Segment-driverlist
            • Rangelist
            • Chase-stack
            • Addresslist
            • 4veclistlist
            • 3col4vecs
            • Occ-name-list
            • Alias-lst
            • Word-list
            • Sig-path-list
            • Function-option-name-lst
            • Any-trace
            • Bfr-varnamelist
            • Aig-varlist
            • Scratch-nontagidxlist
            • Prof-entrylist
            • Interp-st-field-p
            • Fgl-runelist
            • Fgl-rulelist
            • Fgl-object-bindingslist
            • Fgl-congruence-runelist
            • Fgl-binder-runelist
            • Fgl-binder-rulelist
            • Ctrex-rulelist
            • Constraint-tuplelist
            • Cgraph-edgelist
            • Candidate-assigns
            • Rw-pairlist
            • Rewritelist
            • Equiv-contexts
            • Bindinglist
            • Pos-list
            • Obs-sdom-info-list
            • Cutinfolist
            • Bit-list
            • Axi-termlist
            • Axi-litlist
            • Symbol-pseudoterm-alist
            • Symbol-pseudoeventform-alist
            • Inst-list
            • Vl-user-paramsettings-mode-p
            • Svtv-data$c-field-p
            • Ctrex-ruletype-p
            • String-stringlist-alist
            • Ipasir-status-p
            • Fgl-toplevel-sat-check-mode-p
            • Axi-op-p
            • Vl-opacity-p
            • St-hyp-method-p
            • Scratchobj-kind-p
            • Logicman-field-p
            • Bvar-db$c-field-p
            • Env$-field-p
            • Axi
            • *smt-architecture*
            • *vl-directions-kwds*
            • *vl-directions-kwd-alist*
            • Rlp-trees
          • Save
          • Defsection
          • Markup
          • Preprocessor
          • Terminal
          • Emacs-links
          • Defxdoc
          • Katex-integration
          • Constructors
          • Entities
          • Defxdoc+
          • Save-rendered
          • Add-resource-directory
          • Testing
          • Order-subtopics
          • Save-rendered-event
          • Archive-matching-topics
          • Archive-xdoc
          • Xdoc-extend
          • Set-default-parents
          • Missing-parents
          • Defpointer
          • Defxdoc-raw
          • Xdoc-tests
          • Xdoc-prepend
          • Defsection-progn
          • Gen-xdoc-for-file
        • ACL2-doc
        • Recursion-and-induction
        • Loop$-primer
        • Operational-semantics
        • Pointers
        • Doc
        • Documentation-copyright
        • Course-materials
        • Args
        • ACL2-doc-summary
        • Finding-documentation
        • Broken-link
        • Doc-terminal-test-2
        • Doc-terminal-test-1
      • Books
      • Boolean-reasoning
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Transactionp

    Make-honsed-transaction

    Constructor macro for honsed transactionp structures.

    Syntax:

    (make-honsed-transaction [:nonce <nonce>] 
                             [:gas-price <gas-price>] 
                             [:gas-limit <gas-limit>] 
                             [:to <to>] 
                             [:value <value>] 
                             [:sig-v <sig-v>] 
                             [:sig-r <sig-r>] 
                             [:sig-s <sig-s>] 
                             [:init-or-data <init-or-data>]) 
    

    This is identical to make-transaction, except that we hons the structure we are creating.

    Definition

    This is an ordinary honsing make- macro introduced by std::defaggregate.

    Macro: make-honsed-transaction

    (defmacro make-honsed-transaction (&rest args)
      (std::make-aggregate 'transaction
                           args
                           '((:nonce)
                             (:gas-price)
                             (:gas-limit)
                             (:to)
                             (:value)
                             (:sig-v)
                             (:sig-r)
                             (:sig-s)
                             (:init-or-data))
                           'make-honsed-transaction
                           t))