Check if the top block is safe.
(check-safe-top-block block) → _
We check the safety of the block
starting with no variables or functions in scope,
because this is the block at the top level.
Since the top block is not inside a function or loop,
it is only allowed to terminate regularly.
If the checking succeeds, we return nothing (i.e.
Function:
(defun check-safe-top-block (block) (declare (xargs :guard (blockp block))) (let ((__function__ 'check-safe-top-block)) (declare (ignorable __function__)) (b* (((okf modes) (check-safe-block block nil nil))) (if (equal modes (insert (mode-regular) nil)) nil (reserrf (list :top-block-mode modes))))))
Theorem:
(defthm reserr-optionp-of-check-safe-top-block (b* ((_ (check-safe-top-block block))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm check-safe-top-block-of-block-fix-block (equal (check-safe-top-block (block-fix block)) (check-safe-top-block block)))
Theorem:
(defthm check-safe-top-block-block-equiv-congruence-on-block (implies (block-equiv block block-equiv) (equal (check-safe-top-block block) (check-safe-top-block block-equiv))) :rule-classes :congruence)