|
|
|---|
|
|
|
|---|
Raw constructor for honsed account-statep structures.
Syntax:
(honsed-account-state nonce balance storage-root codehash)
This is identical to account-state, except that we hons the structure we are creating.
This is an ordinary honsing constructor introduced by std::defaggregate.
Function:
(defun honsed-account-state (nonce balance storage-root codehash) (declare (xargs :guard (and (noncep nonce) (n256p balance) (b32p storage-root) (b32p codehash)))) (mbe :logic (account-state nonce balance storage-root codehash) :exec (hons (hons 'nonce nonce) (hons (hons 'balance balance) (hons (hons 'storage-root storage-root) (hons (hons 'codehash codehash) nil))))))