		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking-evm

Check-safe-top-block-evm

Check if the top block is safe, in the EVM dialect.

Signature
(check-safe-top-block-evm block) → _
Arguments: block — Guard (blockp block).
Returns: _ — Type (reserr-optionp _).

This is like check-safe-top-block for generic Yul, except that the initial function table is the one with the EVM functions.

Definitions and Theorems

Function: check-safe-top-block-evm

(defun check-safe-top-block-evm (block)
  (declare (xargs :guard (blockp block)))
  (let ((__function__ 'check-safe-top-block-evm))
    (declare (ignorable __function__))
    (b* (((okf modes)
          (check-safe-block block nil (evm-funtable))))
      (if (equal modes (insert (mode-regular) nil))
          nil
        (reserrf (list :top-block-mode modes))))))

Theorem: reserr-optionp-of-check-safe-top-block-evm

(defthm reserr-optionp-of-check-safe-top-block-evm
  (b* ((_ (check-safe-top-block-evm block)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: check-safe-top-block-evm-of-block-fix-block

(defthm check-safe-top-block-evm-of-block-fix-block
  (equal (check-safe-top-block-evm (block-fix block))
         (check-safe-top-block-evm block)))

Theorem: check-safe-top-block-evm-block-equiv-congruence-on-block

(defthm check-safe-top-block-evm-block-equiv-congruence-on-block
  (implies (block-equiv block block-equiv)
           (equal (check-safe-top-block-evm block)
                  (check-safe-top-block-evm block-equiv)))
  :rule-classes :congruence)