Raw constructor for honsed transactionp structures.
Syntax:
(honsed-transaction nonce gas-price gas-limit to value sig-v sig-r sig-s init-or-data)
This is identical to transaction, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-transaction (nonce gas-price gas-limit to value sig-v sig-r sig-s init-or-data) (declare (xargs :guard (and (noncep nonce) (weip gas-price) (n256p gas-limit) (maybe-addressp to) (weip value) (n256p sig-r) (n256p sig-s) (byte-arrayp init-or-data)))) (mbe :logic (transaction nonce gas-price gas-limit to value sig-v sig-r sig-s init-or-data) :exec (hons (hons 'nonce nonce) (hons (hons 'gas-price gas-price) (hons (hons 'gas-limit gas-limit) (hons (hons 'to to) (hons (hons 'value value) (hons (hons 'sig-v sig-v) (hons (hons 'sig-r sig-r) (hons (hons 'sig-s sig-s) (hons (hons 'init-or-data init-or-data) nil)))))))))))