Check if the top block is safe, in the EVM dialect.
(check-safe-top-block-evm block) → _
This is like check-safe-top-block for generic Yul, except that the initial function table is the one with the EVM functions.
Function:
(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:
(defthm reserr-optionp-of-check-safe-top-block-evm (b* ((_ (check-safe-top-block-evm block))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(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:
(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)