		Search-engine friendly clone of the ACL2 documentation.

Transaction

Transactionp

Recognizer for transaction structures.

Signature
(transactionp x) → *

Definitions and Theorems

Function: transactionp

(defun transactionp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'transactionp))
    (declare (ignorable __function__))
    (and (consp x)
         (eq (car x) :transaction)
         (true-listp (cdr x))
         (eql (len (cdr x)) 9)
         (b* ((nonce (std::da-nth 0 (cdr x)))
              (gas-price (std::da-nth 1 (cdr x)))
              (gas-limit (std::da-nth 2 (cdr x)))
              (to (std::da-nth 3 (cdr x)))
              (value (std::da-nth 4 (cdr x)))
              (init/data (std::da-nth 5 (cdr x)))
              (sign-v (std::da-nth 6 (cdr x)))
              (sign-r (std::da-nth 7 (cdr x)))
              (sign-s (std::da-nth 8 (cdr x))))
           (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))))))

Theorem: consp-when-transactionp

(defthm consp-when-transactionp
  (implies (transactionp x) (consp x))
  :rule-classes :compound-recognizer)