		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Exec-top-block

Execute the top block.

Signature
(exec-top-block block limit) → cstate
Arguments: block — Guard (blockp block).; limit — Guard (natp limit).
Returns: cstate — Type (cstate-resultp cstate).

This is used for the top-level block. Starting with the empty computation state and the empty function environment, we execute the block, propagating errors. Since the top-level block is not inside a function or loop, we defensively check that the execution terminates regularly, returning an error if it does not. In case of success, we return the final computation state.

Definitions and Theorems

Function: exec-top-block

(defun exec-top-block (block limit)
  (declare (xargs :guard (and (blockp block) (natp limit))))
  (let ((__function__ 'exec-top-block))
    (declare (ignorable __function__))
    (b* ((cstate (make-cstate :local nil))
         (funenv nil)
         ((okf (soutcome outcome))
          (exec-block block cstate funenv limit))
         ((unless (equal outcome.mode (mode-regular)))
          (reserrf (list :top-block-move outcome.mode))))
      outcome.cstate)))

Theorem: cstate-resultp-of-exec-top-block

(defthm cstate-resultp-of-exec-top-block
  (b* ((cstate (exec-top-block block limit)))
    (cstate-resultp cstate))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-exec-top-block

(defthm error-info-wfp-of-exec-top-block
  (b* ((?cstate (exec-top-block block limit)))
    (implies (reserrp cstate)
             (error-info-wfp cstate))))

Theorem: exec-top-block-of-block-fix-block

(defthm exec-top-block-of-block-fix-block
  (equal (exec-top-block (block-fix block) limit)
         (exec-top-block block limit)))

Theorem: exec-top-block-block-equiv-congruence-on-block

(defthm exec-top-block-block-equiv-congruence-on-block
  (implies (block-equiv block block-equiv)
           (equal (exec-top-block block limit)
                  (exec-top-block block-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-top-block-of-nfix-limit

(defthm exec-top-block-of-nfix-limit
  (equal (exec-top-block block (nfix limit))
         (exec-top-block block limit)))

Theorem: exec-top-block-nat-equiv-congruence-on-limit

(defthm exec-top-block-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-top-block block limit)
                  (exec-top-block block limit-equiv)))
  :rule-classes :congruence)