• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
        • Transformations
        • Language
          • Abstract-syntax
          • Dynamic-semantics
            • Exec
              • Exec-statement
              • Exec-function
              • Exec-for-iterations
              • Exec-block
              • Exec-switch-rest
              • Exec-expression-list
              • Exec-funcall
              • Exec-statement-list
              • Exec-expression
            • Find-fun
            • Init-local
            • Write-vars-values
            • Add-vars-values
            • Add-funs
            • Eoutcome
            • Soutcome
            • Ensure-funscope-disjoint
            • Write-var-value
            • Restrict-vars
            • Add-var-value
            • Funinfo
            • Exec-top-block
            • Values
            • Cstate
            • Funinfo+funenv
            • Read-vars-values
            • Read-var-value
            • Funenv
            • Funscope-for-fundefs
            • Exec-path
            • Path-to-var
            • Funinfo+funenv-result
            • Exec-literal
            • Soutcome-result
            • Mode-set-result
            • Literal-evaluation
            • Funscope-result
            • Funinfo-result
            • Funenv-result
            • Eoutcome-result
            • Cstate-result
            • Paths-to-vars
            • Funinfo-for-fundef
            • Lstate
            • Funscope
            • Mode-set
            • Modes
          • Concrete-syntax
          • Static-soundness
          • Static-semantics
          • Errors
        • Yul-json
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Dynamic-semantics

Exec

Mutually recursive execution functions.

Executing expressions involves executing function calls, which involves executing the statements in function bodies, which involves executing the expressions in the statements.

Definitions and Theorems

Function: exec-expression

(defun exec-expression (expr cstate funenv limit)
 (declare (xargs :guard (and (expressionp expr)
                             (cstatep cstate)
                             (funenvp funenv)
                             (natp limit))))
 (let ((__function__ 'exec-expression))
  (declare (ignorable __function__))
  (b* (((when (zp limit))
        (reserrf (list :limit (expression-fix expr)))))
   (expression-case
       expr
       :path (exec-path expr.get cstate)
       :literal (exec-literal expr.get cstate)
       :funcall (exec-funcall expr.get cstate funenv (1- limit))))))

Function: exec-expression-list

(defun exec-expression-list (exprs cstate funenv limit)
  (declare (xargs :guard (and (expression-listp exprs)
                              (cstatep cstate)
                              (funenvp funenv)
                              (natp limit))))
  (let ((__function__ 'exec-expression-list))
    (declare (ignorable __function__))
    (b* (((when (zp limit))
          (reserrf (list :limit (expression-list-fix exprs))))
         ((when (endp exprs))
          (make-eoutcome :cstate cstate
                         :values nil))
         ((okf (eoutcome outcome))
          (exec-expression (car exprs)
                           cstate funenv (1- limit)))
         ((unless (equal (len outcome.values) 1))
          (reserrf (list :not-single-value outcome.values)))
         (val (car outcome.values))
         ((okf (eoutcome outcome))
          (exec-expression-list (cdr exprs)
                                outcome.cstate funenv (1- limit))))
      (make-eoutcome :cstate outcome.cstate
                     :values (cons val outcome.values)))))

Function: exec-funcall

(defun exec-funcall (call cstate funenv limit)
  (declare (xargs :guard (and (funcallp call)
                              (cstatep cstate)
                              (funenvp funenv)
                              (natp limit))))
  (let ((__function__ 'exec-funcall))
    (declare (ignorable __function__))
    (b* (((when (zp limit))
          (reserrf (list :limit (funcall-fix call))))
         ((funcall call) call)
         ((okf (eoutcome outcome))
          (exec-expression-list (rev call.args)
                                cstate funenv (1- limit))))
      (exec-function call.name outcome.values
                     outcome.cstate funenv (1- limit)))))

Function: exec-function

(defun exec-function (fun args cstate funenv limit)
 (declare (xargs :guard (and (identifierp fun)
                             (value-listp args)
                             (cstatep cstate)
                             (funenvp funenv)
                             (natp limit))))
 (let ((__function__ 'exec-function))
   (declare (ignorable __function__))
   (b*
    (((when (zp limit))
      (reserrf (list :limit (identifier-fix fun)
                     (value-list-fix args))))
     ((okf (funinfo+funenv info+env))
      (find-fun fun funenv))
     ((funinfo info) info+env.info)
     (lstate-before (cstate->local cstate))
     ((okf cstate)
      (init-local info.inputs args info.outputs cstate))
     ((okf (soutcome outcome))
      (exec-block info.body
                  cstate info+env.env (1- limit)))
     ((when (mode-case outcome.mode :break))
      (reserrf (list :break-from-function (identifier-fix fun))))
     ((when (mode-case outcome.mode :continue))
      (reserrf (list :continue-from-function (identifier-fix fun))))
     ((okf vals)
      (read-vars-values info.outputs outcome.cstate))
     (cstate (change-cstate outcome.cstate
                            :local lstate-before)))
    (make-eoutcome :cstate cstate
                   :values vals))))

Function: exec-statement

(defun exec-statement (stmt cstate funenv limit)
 (declare (xargs :guard (and (statementp stmt)
                             (cstatep cstate)
                             (funenvp funenv)
                             (natp limit))))
 (let ((__function__ 'exec-statement))
  (declare (ignorable __function__))
  (b* (((when (zp limit))
        (reserrf (list :limit (statement-fix stmt)))))
   (statement-case
    stmt :block
    (exec-block stmt.get cstate funenv (1- limit))
    :variable-single
    (expression-option-case
     stmt.init :some
     (b* (((okf (eoutcome outcome))
           (exec-expression stmt.init.val cstate funenv (1- limit)))
          ((unless (equal (len outcome.values) 1))
           (reserrf (list :not-single-value outcome.values)))
          ((okf cstate)
           (add-var-value stmt.name (car outcome.values)
                          outcome.cstate)))
       (make-soutcome :cstate cstate
                      :mode (mode-regular)))
     :none
     (b* (((okf cstate)
           (add-var-value stmt.name (value 0)
                          cstate)))
       (make-soutcome :cstate cstate
                      :mode (mode-regular))))
    :variable-multi
    (if
     (>= (len stmt.names) 2)
     (funcall-option-case
        stmt.init :some
        (b* (((okf (eoutcome outcome))
              (exec-funcall stmt.init.val cstate funenv (1- limit)))
             ((okf cstate)
              (add-vars-values stmt.names
                               outcome.values outcome.cstate)))
          (make-soutcome :cstate cstate
                         :mode (mode-regular)))
        :none
        (b* (((okf cstate)
              (add-vars-values stmt.names
                               (repeat (len stmt.names) (value 0))
                               cstate)))
          (make-soutcome :cstate cstate
                         :mode (mode-regular))))
     (reserrf (list :non-multiple-variables stmt.names)))
    :assign-single
    (b* (((okf var) (path-to-var stmt.target))
         ((okf (eoutcome outcome))
          (exec-expression stmt.value cstate funenv (1- limit)))
         ((unless (equal (len outcome.values) 1))
          (reserrf (list :not-single-value outcome.values)))
         ((okf cstate)
          (write-var-value var (car outcome.values)
                           outcome.cstate)))
      (make-soutcome :cstate cstate
                     :mode (mode-regular)))
    :assign-multi
    (b* (((unless (>= (len stmt.targets) 2))
          (reserrf (list :non-multiple-variables stmt.targets)))
         ((okf vars)
          (paths-to-vars stmt.targets))
         ((okf (eoutcome outcome))
          (exec-funcall stmt.value cstate funenv (1- limit)))
         ((okf cstate)
          (write-vars-values vars outcome.values outcome.cstate)))
      (make-soutcome :cstate cstate
                     :mode (mode-regular)))
    :funcall
    (b*
     (((okf (eoutcome outcome))
       (exec-funcall stmt.get cstate funenv (1- limit)))
      ((when (consp outcome.values))
       (reserrf (list :funcall-statement-returns outcome.values))))
     (make-soutcome :cstate outcome.cstate
                    :mode (mode-regular)))
    :if
    (b* (((okf (eoutcome outcome))
          (exec-expression stmt.test cstate funenv (1- limit)))
         ((unless (equal (len outcome.values) 1))
          (reserrf (list :if-test-not-single-value outcome.values)))
         (val (car outcome.values)))
      (if (equal val (value 0))
          (make-soutcome :cstate outcome.cstate
                         :mode (mode-regular))
        (exec-block stmt.body
                    outcome.cstate funenv (1- limit))))
    :for
    (b*
      ((vars-before (omap::keys (cstate->local cstate)))
       (stmts (block->statements stmt.init))
       ((okf funenv)
        (add-funs (statements-to-fundefs stmts)
                  funenv))
       ((okf (soutcome outcome))
        (exec-statement-list stmts cstate funenv (1- limit)))
       ((when (mode-case outcome.mode :break))
        (reserrf (list :break-from-for-init (statement-fix stmt))))
       ((when (mode-case outcome.mode :continue))
        (reserrf
             (list :continue-from-for-init (statement-fix stmt))))
       ((when (mode-case outcome.mode :leave))
        (b* ((cstate (restrict-vars vars-before outcome.cstate)))
          (make-soutcome :cstate cstate
                         :mode (mode-leave))))
       ((okf (soutcome outcome))
        (exec-for-iterations stmt.test stmt.update stmt.body
                             outcome.cstate funenv (1- limit)))
       ((when (mode-case outcome.mode :break))
        (reserrf (list :break-from-for (statement-fix stmt))))
       ((when (mode-case outcome.mode :continue))
        (reserrf (list :continue-from-for (statement-fix stmt))))
       (cstate (restrict-vars vars-before outcome.cstate)))
      (make-soutcome :cstate cstate
                     :mode outcome.mode))
    :switch
    (b* (((okf (eoutcome outcome))
          (exec-expression stmt.target cstate funenv (1- limit)))
         ((unless (equal (len outcome.values) 1))
          (reserrf (list :not-single-value outcome.values))))
      (exec-switch-rest stmt.cases
                        stmt.default (car outcome.values)
                        outcome.cstate funenv (1- limit)))
    :leave (make-soutcome :cstate cstate
                          :mode (mode-leave))
    :break (make-soutcome :cstate cstate
                          :mode (mode-break))
    :continue (make-soutcome :cstate cstate
                             :mode (mode-continue))
    :fundef (make-soutcome :cstate cstate
                           :mode (mode-regular))))))

Function: exec-statement-list

(defun exec-statement-list (stmts cstate funenv limit)
  (declare (xargs :guard (and (statement-listp stmts)
                              (cstatep cstate)
                              (funenvp funenv)
                              (natp limit))))
  (let ((__function__ 'exec-statement-list))
    (declare (ignorable __function__))
    (b* (((when (zp limit))
          (reserrf (list :limit (statement-list-fix stmts))))
         ((when (endp stmts))
          (make-soutcome :cstate cstate
                         :mode (mode-regular)))
         ((okf (soutcome outcome))
          (exec-statement (car stmts)
                          cstate funenv (1- limit)))
         ((unless (mode-case outcome.mode :regular))
          outcome))
      (exec-statement-list (cdr stmts)
                           outcome.cstate funenv (1- limit)))))

Function: exec-block

(defun exec-block (block cstate funenv limit)
  (declare (xargs :guard (and (blockp block)
                              (cstatep cstate)
                              (funenvp funenv)
                              (natp limit))))
  (let ((__function__ 'exec-block))
    (declare (ignorable __function__))
    (b* (((when (zp limit))
          (reserrf (list :limit (block-fix block))))
         (vars-before (omap::keys (cstate->local cstate)))
         (stmts (block->statements block))
         ((okf funenv)
          (add-funs (statements-to-fundefs stmts)
                    funenv))
         ((okf (soutcome outcome))
          (exec-statement-list stmts cstate funenv (1- limit)))
         (cstate (restrict-vars vars-before outcome.cstate)))
      (make-soutcome :cstate cstate
                     :mode outcome.mode))))

Function: exec-for-iterations

(defun exec-for-iterations (test update body cstate funenv limit)
 (declare (xargs :guard (and (expressionp test)
                             (blockp update)
                             (blockp body)
                             (cstatep cstate)
                             (funenvp funenv)
                             (natp limit))))
 (let ((__function__ 'exec-for-iterations))
   (declare (ignorable __function__))
   (b*
    (((when (zp limit))
      (reserrf (list :limit (expression-fix test)
                     (block-fix update)
                     (block-fix body))))
     ((okf (eoutcome outcome))
      (exec-expression test cstate funenv (1- limit)))
     ((unless (equal (len outcome.values) 1))
      (reserrf (list :for-test-not-single-value outcome.values)))
     ((when (equal (car outcome.values) (value 0)))
      (make-soutcome :cstate outcome.cstate
                     :mode (mode-regular)))
     ((okf (soutcome outcome))
      (exec-block body outcome.cstate funenv (1- limit)))
     ((when (mode-case outcome.mode :break))
      (make-soutcome :cstate outcome.cstate
                     :mode (mode-regular)))
     ((when (mode-case outcome.mode :leave))
      (make-soutcome :cstate outcome.cstate
                     :mode outcome.mode))
     ((okf (soutcome outcome))
      (exec-block update
                  outcome.cstate funenv (1- limit)))
     ((when (mode-case outcome.mode :break))
      (reserrf (list :break-from-for-update (block-fix update))))
     ((when (mode-case outcome.mode :continue))
      (reserrf (list :continue-from-for-update (block-fix update))))
     ((when (mode-case outcome.mode :leave))
      (make-soutcome :cstate outcome.cstate
                     :mode outcome.mode)))
    (exec-for-iterations test update body
                         outcome.cstate funenv (1- limit)))))

Function: exec-switch-rest

(defun exec-switch-rest (cases default target cstate funenv limit)
 (declare (xargs :guard (and (swcase-listp cases)
                             (block-optionp default)
                             (valuep target)
                             (cstatep cstate)
                             (funenvp funenv)
                             (natp limit))))
 (let ((__function__ 'exec-switch-rest))
  (declare (ignorable __function__))
  (b* (((when (zp limit))
        (reserrf (list :limit (swcase-list-fix cases)
                       (block-option-fix default))))
       ((when (endp cases))
        (block-option-case
             default
             :some (exec-block default.val cstate funenv (1- limit))
             :none (make-soutcome :cstate cstate
                                  :mode (mode-regular))))
       ((swcase case) (car cases))
       ((okf caseval)
        (eval-literal case.value))
       ((when (value-equiv target caseval))
        (exec-block case.body cstate funenv (1- limit))))
    (exec-switch-rest (cdr cases)
                      default
                      target cstate funenv (1- limit)))))

Theorem: return-type-of-exec-expression.outcome

(defthm return-type-of-exec-expression.outcome
  (b* ((?outcome (exec-expression expr cstate funenv limit)))
    (eoutcome-resultp outcome))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-expression-list.outcome

(defthm return-type-of-exec-expression-list.outcome
  (b* ((?outcome (exec-expression-list exprs cstate funenv limit)))
    (eoutcome-resultp outcome))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-funcall.outcome

(defthm return-type-of-exec-funcall.outcome
  (b* ((?outcome (exec-funcall call cstate funenv limit)))
    (eoutcome-resultp outcome))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-function.outcome

(defthm return-type-of-exec-function.outcome
  (b* ((?outcome (exec-function fun args cstate funenv limit)))
    (eoutcome-resultp outcome))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-statement.outcome

(defthm return-type-of-exec-statement.outcome
  (b* ((?outcome (exec-statement stmt cstate funenv limit)))
    (soutcome-resultp outcome))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-statement-list.outcome

(defthm return-type-of-exec-statement-list.outcome
  (b* ((?outcome (exec-statement-list stmts cstate funenv limit)))
    (soutcome-resultp outcome))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-block.outcome

(defthm return-type-of-exec-block.outcome
  (b* ((?outcome (exec-block block cstate funenv limit)))
    (soutcome-resultp outcome))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-for-iterations.outcome

(defthm return-type-of-exec-for-iterations.outcome
 (b*
  ((?outcome
        (exec-for-iterations test update body cstate funenv limit)))
  (soutcome-resultp outcome))
 :rule-classes :rewrite)

Theorem: return-type-of-exec-switch-rest.outcome

(defthm return-type-of-exec-switch-rest.outcome
 (b*
  ((?outcome (exec-switch-rest cases
                               default target cstate funenv limit)))
  (soutcome-resultp outcome))
 :rule-classes :rewrite)

Theorem: exec-expression-of-expression-fix-expr

(defthm exec-expression-of-expression-fix-expr
  (equal (exec-expression (expression-fix expr)
                          cstate funenv limit)
         (exec-expression expr cstate funenv limit)))

Theorem: exec-expression-of-cstate-fix-cstate

(defthm exec-expression-of-cstate-fix-cstate
  (equal (exec-expression expr (cstate-fix cstate)
                          funenv limit)
         (exec-expression expr cstate funenv limit)))

Theorem: exec-expression-of-funenv-fix-funenv

(defthm exec-expression-of-funenv-fix-funenv
  (equal (exec-expression expr cstate (funenv-fix funenv)
                          limit)
         (exec-expression expr cstate funenv limit)))

Theorem: exec-expression-of-nfix-limit

(defthm exec-expression-of-nfix-limit
  (equal (exec-expression expr cstate funenv (nfix limit))
         (exec-expression expr cstate funenv limit)))

Theorem: exec-expression-list-of-expression-list-fix-exprs

(defthm exec-expression-list-of-expression-list-fix-exprs
  (equal (exec-expression-list (expression-list-fix exprs)
                               cstate funenv limit)
         (exec-expression-list exprs cstate funenv limit)))

Theorem: exec-expression-list-of-cstate-fix-cstate

(defthm exec-expression-list-of-cstate-fix-cstate
  (equal (exec-expression-list exprs (cstate-fix cstate)
                               funenv limit)
         (exec-expression-list exprs cstate funenv limit)))

Theorem: exec-expression-list-of-funenv-fix-funenv

(defthm exec-expression-list-of-funenv-fix-funenv
  (equal (exec-expression-list exprs cstate (funenv-fix funenv)
                               limit)
         (exec-expression-list exprs cstate funenv limit)))

Theorem: exec-expression-list-of-nfix-limit

(defthm exec-expression-list-of-nfix-limit
  (equal (exec-expression-list exprs cstate funenv (nfix limit))
         (exec-expression-list exprs cstate funenv limit)))

Theorem: exec-funcall-of-funcall-fix-call

(defthm exec-funcall-of-funcall-fix-call
  (equal (exec-funcall (funcall-fix call)
                       cstate funenv limit)
         (exec-funcall call cstate funenv limit)))

Theorem: exec-funcall-of-cstate-fix-cstate

(defthm exec-funcall-of-cstate-fix-cstate
  (equal (exec-funcall call (cstate-fix cstate)
                       funenv limit)
         (exec-funcall call cstate funenv limit)))

Theorem: exec-funcall-of-funenv-fix-funenv

(defthm exec-funcall-of-funenv-fix-funenv
  (equal (exec-funcall call cstate (funenv-fix funenv)
                       limit)
         (exec-funcall call cstate funenv limit)))

Theorem: exec-funcall-of-nfix-limit

(defthm exec-funcall-of-nfix-limit
  (equal (exec-funcall call cstate funenv (nfix limit))
         (exec-funcall call cstate funenv limit)))

Theorem: exec-function-of-identifier-fix-fun

(defthm exec-function-of-identifier-fix-fun
  (equal (exec-function (identifier-fix fun)
                        args cstate funenv limit)
         (exec-function fun args cstate funenv limit)))

Theorem: exec-function-of-value-list-fix-args

(defthm exec-function-of-value-list-fix-args
  (equal (exec-function fun (value-list-fix args)
                        cstate funenv limit)
         (exec-function fun args cstate funenv limit)))

Theorem: exec-function-of-cstate-fix-cstate

(defthm exec-function-of-cstate-fix-cstate
  (equal (exec-function fun args (cstate-fix cstate)
                        funenv limit)
         (exec-function fun args cstate funenv limit)))

Theorem: exec-function-of-funenv-fix-funenv

(defthm exec-function-of-funenv-fix-funenv
  (equal (exec-function fun args cstate (funenv-fix funenv)
                        limit)
         (exec-function fun args cstate funenv limit)))

Theorem: exec-function-of-nfix-limit

(defthm exec-function-of-nfix-limit
  (equal (exec-function fun args cstate funenv (nfix limit))
         (exec-function fun args cstate funenv limit)))

Theorem: exec-statement-of-statement-fix-stmt

(defthm exec-statement-of-statement-fix-stmt
  (equal (exec-statement (statement-fix stmt)
                         cstate funenv limit)
         (exec-statement stmt cstate funenv limit)))

Theorem: exec-statement-of-cstate-fix-cstate

(defthm exec-statement-of-cstate-fix-cstate
  (equal (exec-statement stmt (cstate-fix cstate)
                         funenv limit)
         (exec-statement stmt cstate funenv limit)))

Theorem: exec-statement-of-funenv-fix-funenv

(defthm exec-statement-of-funenv-fix-funenv
  (equal (exec-statement stmt cstate (funenv-fix funenv)
                         limit)
         (exec-statement stmt cstate funenv limit)))

Theorem: exec-statement-of-nfix-limit

(defthm exec-statement-of-nfix-limit
  (equal (exec-statement stmt cstate funenv (nfix limit))
         (exec-statement stmt cstate funenv limit)))

Theorem: exec-statement-list-of-statement-list-fix-stmts

(defthm exec-statement-list-of-statement-list-fix-stmts
  (equal (exec-statement-list (statement-list-fix stmts)
                              cstate funenv limit)
         (exec-statement-list stmts cstate funenv limit)))

Theorem: exec-statement-list-of-cstate-fix-cstate

(defthm exec-statement-list-of-cstate-fix-cstate
  (equal (exec-statement-list stmts (cstate-fix cstate)
                              funenv limit)
         (exec-statement-list stmts cstate funenv limit)))

Theorem: exec-statement-list-of-funenv-fix-funenv

(defthm exec-statement-list-of-funenv-fix-funenv
  (equal (exec-statement-list stmts cstate (funenv-fix funenv)
                              limit)
         (exec-statement-list stmts cstate funenv limit)))

Theorem: exec-statement-list-of-nfix-limit

(defthm exec-statement-list-of-nfix-limit
  (equal (exec-statement-list stmts cstate funenv (nfix limit))
         (exec-statement-list stmts cstate funenv limit)))

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

(defthm exec-block-of-block-fix-block
  (equal (exec-block (block-fix block)
                     cstate funenv limit)
         (exec-block block cstate funenv limit)))

Theorem: exec-block-of-cstate-fix-cstate

(defthm exec-block-of-cstate-fix-cstate
  (equal (exec-block block (cstate-fix cstate)
                     funenv limit)
         (exec-block block cstate funenv limit)))

Theorem: exec-block-of-funenv-fix-funenv

(defthm exec-block-of-funenv-fix-funenv
  (equal (exec-block block cstate (funenv-fix funenv)
                     limit)
         (exec-block block cstate funenv limit)))

Theorem: exec-block-of-nfix-limit

(defthm exec-block-of-nfix-limit
  (equal (exec-block block cstate funenv (nfix limit))
         (exec-block block cstate funenv limit)))

Theorem: exec-for-iterations-of-expression-fix-test

(defthm exec-for-iterations-of-expression-fix-test
 (equal (exec-for-iterations (expression-fix test)
                             update body cstate funenv limit)
        (exec-for-iterations test update body cstate funenv limit)))

Theorem: exec-for-iterations-of-block-fix-update

(defthm exec-for-iterations-of-block-fix-update
 (equal (exec-for-iterations test (block-fix update)
                             body cstate funenv limit)
        (exec-for-iterations test update body cstate funenv limit)))

Theorem: exec-for-iterations-of-block-fix-body

(defthm exec-for-iterations-of-block-fix-body
 (equal (exec-for-iterations test update (block-fix body)
                             cstate funenv limit)
        (exec-for-iterations test update body cstate funenv limit)))

Theorem: exec-for-iterations-of-cstate-fix-cstate

(defthm exec-for-iterations-of-cstate-fix-cstate
 (equal (exec-for-iterations test update body (cstate-fix cstate)
                             funenv limit)
        (exec-for-iterations test update body cstate funenv limit)))

Theorem: exec-for-iterations-of-funenv-fix-funenv

(defthm exec-for-iterations-of-funenv-fix-funenv
 (equal (exec-for-iterations test
                             update body cstate (funenv-fix funenv)
                             limit)
        (exec-for-iterations test update body cstate funenv limit)))

Theorem: exec-for-iterations-of-nfix-limit

(defthm exec-for-iterations-of-nfix-limit
 (equal (exec-for-iterations test
                             update body cstate funenv (nfix limit))
        (exec-for-iterations test update body cstate funenv limit)))

Theorem: exec-switch-rest-of-swcase-list-fix-cases

(defthm exec-switch-rest-of-swcase-list-fix-cases
  (equal (exec-switch-rest (swcase-list-fix cases)
                           default target cstate funenv limit)
         (exec-switch-rest cases
                           default target cstate funenv limit)))

Theorem: exec-switch-rest-of-block-option-fix-default

(defthm exec-switch-rest-of-block-option-fix-default
  (equal (exec-switch-rest cases (block-option-fix default)
                           target cstate funenv limit)
         (exec-switch-rest cases
                           default target cstate funenv limit)))

Theorem: exec-switch-rest-of-value-fix-target

(defthm exec-switch-rest-of-value-fix-target
  (equal (exec-switch-rest cases default (value-fix target)
                           cstate funenv limit)
         (exec-switch-rest cases
                           default target cstate funenv limit)))

Theorem: exec-switch-rest-of-cstate-fix-cstate

(defthm exec-switch-rest-of-cstate-fix-cstate
  (equal (exec-switch-rest cases default target (cstate-fix cstate)
                           funenv limit)
         (exec-switch-rest cases
                           default target cstate funenv limit)))

Theorem: exec-switch-rest-of-funenv-fix-funenv

(defthm exec-switch-rest-of-funenv-fix-funenv
  (equal (exec-switch-rest cases default
                           target cstate (funenv-fix funenv)
                           limit)
         (exec-switch-rest cases
                           default target cstate funenv limit)))

Theorem: exec-switch-rest-of-nfix-limit

(defthm exec-switch-rest-of-nfix-limit
  (equal (exec-switch-rest cases default
                           target cstate funenv (nfix limit))
         (exec-switch-rest cases
                           default target cstate funenv limit)))

Theorem: exec-expression-expression-equiv-congruence-on-expr

(defthm exec-expression-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (exec-expression expr cstate funenv limit)
                  (exec-expression expr-equiv cstate funenv limit)))
  :rule-classes :congruence)

Theorem: exec-expression-cstate-equiv-congruence-on-cstate

(defthm exec-expression-cstate-equiv-congruence-on-cstate
  (implies (cstate-equiv cstate cstate-equiv)
           (equal (exec-expression expr cstate funenv limit)
                  (exec-expression expr cstate-equiv funenv limit)))
  :rule-classes :congruence)

Theorem: exec-expression-funenv-equiv-congruence-on-funenv

(defthm exec-expression-funenv-equiv-congruence-on-funenv
  (implies (funenv-equiv funenv funenv-equiv)
           (equal (exec-expression expr cstate funenv limit)
                  (exec-expression expr cstate funenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-expression-nat-equiv-congruence-on-limit

(defthm exec-expression-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-expression expr cstate funenv limit)
                  (exec-expression expr cstate funenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-expression-list-expression-list-equiv-congruence-on-exprs

(defthm
     exec-expression-list-expression-list-equiv-congruence-on-exprs
 (implies
     (expression-list-equiv exprs exprs-equiv)
     (equal (exec-expression-list exprs cstate funenv limit)
            (exec-expression-list exprs-equiv cstate funenv limit)))
 :rule-classes :congruence)

Theorem: exec-expression-list-cstate-equiv-congruence-on-cstate

(defthm exec-expression-list-cstate-equiv-congruence-on-cstate
 (implies
     (cstate-equiv cstate cstate-equiv)
     (equal (exec-expression-list exprs cstate funenv limit)
            (exec-expression-list exprs cstate-equiv funenv limit)))
 :rule-classes :congruence)

Theorem: exec-expression-list-funenv-equiv-congruence-on-funenv

(defthm exec-expression-list-funenv-equiv-congruence-on-funenv
 (implies
     (funenv-equiv funenv funenv-equiv)
     (equal (exec-expression-list exprs cstate funenv limit)
            (exec-expression-list exprs cstate funenv-equiv limit)))
 :rule-classes :congruence)

Theorem: exec-expression-list-nat-equiv-congruence-on-limit

(defthm exec-expression-list-nat-equiv-congruence-on-limit
 (implies
     (acl2::nat-equiv limit limit-equiv)
     (equal (exec-expression-list exprs cstate funenv limit)
            (exec-expression-list exprs cstate funenv limit-equiv)))
 :rule-classes :congruence)

Theorem: exec-funcall-funcall-equiv-congruence-on-call

(defthm exec-funcall-funcall-equiv-congruence-on-call
  (implies (funcall-equiv call call-equiv)
           (equal (exec-funcall call cstate funenv limit)
                  (exec-funcall call-equiv cstate funenv limit)))
  :rule-classes :congruence)

Theorem: exec-funcall-cstate-equiv-congruence-on-cstate

(defthm exec-funcall-cstate-equiv-congruence-on-cstate
  (implies (cstate-equiv cstate cstate-equiv)
           (equal (exec-funcall call cstate funenv limit)
                  (exec-funcall call cstate-equiv funenv limit)))
  :rule-classes :congruence)

Theorem: exec-funcall-funenv-equiv-congruence-on-funenv

(defthm exec-funcall-funenv-equiv-congruence-on-funenv
  (implies (funenv-equiv funenv funenv-equiv)
           (equal (exec-funcall call cstate funenv limit)
                  (exec-funcall call cstate funenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-funcall-nat-equiv-congruence-on-limit

(defthm exec-funcall-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-funcall call cstate funenv limit)
                  (exec-funcall call cstate funenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-function-identifier-equiv-congruence-on-fun

(defthm exec-function-identifier-equiv-congruence-on-fun
  (implies
       (identifier-equiv fun fun-equiv)
       (equal (exec-function fun args cstate funenv limit)
              (exec-function fun-equiv args cstate funenv limit)))
  :rule-classes :congruence)

Theorem: exec-function-value-list-equiv-congruence-on-args

(defthm exec-function-value-list-equiv-congruence-on-args
  (implies
       (value-list-equiv args args-equiv)
       (equal (exec-function fun args cstate funenv limit)
              (exec-function fun args-equiv cstate funenv limit)))
  :rule-classes :congruence)

Theorem: exec-function-cstate-equiv-congruence-on-cstate

(defthm exec-function-cstate-equiv-congruence-on-cstate
  (implies
       (cstate-equiv cstate cstate-equiv)
       (equal (exec-function fun args cstate funenv limit)
              (exec-function fun args cstate-equiv funenv limit)))
  :rule-classes :congruence)

Theorem: exec-function-funenv-equiv-congruence-on-funenv

(defthm exec-function-funenv-equiv-congruence-on-funenv
  (implies
       (funenv-equiv funenv funenv-equiv)
       (equal (exec-function fun args cstate funenv limit)
              (exec-function fun args cstate funenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-function-nat-equiv-congruence-on-limit

(defthm exec-function-nat-equiv-congruence-on-limit
  (implies
       (acl2::nat-equiv limit limit-equiv)
       (equal (exec-function fun args cstate funenv limit)
              (exec-function fun args cstate funenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-statement-statement-equiv-congruence-on-stmt

(defthm exec-statement-statement-equiv-congruence-on-stmt
  (implies (statement-equiv stmt stmt-equiv)
           (equal (exec-statement stmt cstate funenv limit)
                  (exec-statement stmt-equiv cstate funenv limit)))
  :rule-classes :congruence)

Theorem: exec-statement-cstate-equiv-congruence-on-cstate

(defthm exec-statement-cstate-equiv-congruence-on-cstate
  (implies (cstate-equiv cstate cstate-equiv)
           (equal (exec-statement stmt cstate funenv limit)
                  (exec-statement stmt cstate-equiv funenv limit)))
  :rule-classes :congruence)

Theorem: exec-statement-funenv-equiv-congruence-on-funenv

(defthm exec-statement-funenv-equiv-congruence-on-funenv
  (implies (funenv-equiv funenv funenv-equiv)
           (equal (exec-statement stmt cstate funenv limit)
                  (exec-statement stmt cstate funenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-statement-nat-equiv-congruence-on-limit

(defthm exec-statement-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-statement stmt cstate funenv limit)
                  (exec-statement stmt cstate funenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-statement-list-statement-list-equiv-congruence-on-stmts

(defthm exec-statement-list-statement-list-equiv-congruence-on-stmts
 (implies
      (statement-list-equiv stmts stmts-equiv)
      (equal (exec-statement-list stmts cstate funenv limit)
             (exec-statement-list stmts-equiv cstate funenv limit)))
 :rule-classes :congruence)

Theorem: exec-statement-list-cstate-equiv-congruence-on-cstate

(defthm exec-statement-list-cstate-equiv-congruence-on-cstate
 (implies
      (cstate-equiv cstate cstate-equiv)
      (equal (exec-statement-list stmts cstate funenv limit)
             (exec-statement-list stmts cstate-equiv funenv limit)))
 :rule-classes :congruence)

Theorem: exec-statement-list-funenv-equiv-congruence-on-funenv

(defthm exec-statement-list-funenv-equiv-congruence-on-funenv
 (implies
      (funenv-equiv funenv funenv-equiv)
      (equal (exec-statement-list stmts cstate funenv limit)
             (exec-statement-list stmts cstate funenv-equiv limit)))
 :rule-classes :congruence)

Theorem: exec-statement-list-nat-equiv-congruence-on-limit

(defthm exec-statement-list-nat-equiv-congruence-on-limit
 (implies
      (acl2::nat-equiv limit limit-equiv)
      (equal (exec-statement-list stmts cstate funenv limit)
             (exec-statement-list stmts cstate funenv limit-equiv)))
 :rule-classes :congruence)

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

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

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

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

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

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

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

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

Theorem: exec-for-iterations-expression-equiv-congruence-on-test

(defthm exec-for-iterations-expression-equiv-congruence-on-test
 (implies
   (expression-equiv test test-equiv)
   (equal (exec-for-iterations test update body cstate funenv limit)
          (exec-for-iterations test-equiv
                               update body cstate funenv limit)))
 :rule-classes :congruence)

Theorem: exec-for-iterations-block-equiv-congruence-on-update

(defthm exec-for-iterations-block-equiv-congruence-on-update
 (implies
  (block-equiv update update-equiv)
  (equal
       (exec-for-iterations test update body cstate funenv limit)
       (exec-for-iterations test
                            update-equiv body cstate funenv limit)))
 :rule-classes :congruence)

Theorem: exec-for-iterations-block-equiv-congruence-on-body

(defthm exec-for-iterations-block-equiv-congruence-on-body
 (implies
  (block-equiv body body-equiv)
  (equal
       (exec-for-iterations test update body cstate funenv limit)
       (exec-for-iterations test
                            update body-equiv cstate funenv limit)))
 :rule-classes :congruence)

Theorem: exec-for-iterations-cstate-equiv-congruence-on-cstate

(defthm exec-for-iterations-cstate-equiv-congruence-on-cstate
 (implies
  (cstate-equiv cstate cstate-equiv)
  (equal
       (exec-for-iterations test update body cstate funenv limit)
       (exec-for-iterations test
                            update body cstate-equiv funenv limit)))
 :rule-classes :congruence)

Theorem: exec-for-iterations-funenv-equiv-congruence-on-funenv

(defthm exec-for-iterations-funenv-equiv-congruence-on-funenv
 (implies
  (funenv-equiv funenv funenv-equiv)
  (equal
       (exec-for-iterations test update body cstate funenv limit)
       (exec-for-iterations test
                            update body cstate funenv-equiv limit)))
 :rule-classes :congruence)

Theorem: exec-for-iterations-nat-equiv-congruence-on-limit

(defthm exec-for-iterations-nat-equiv-congruence-on-limit
 (implies
  (acl2::nat-equiv limit limit-equiv)
  (equal
       (exec-for-iterations test update body cstate funenv limit)
       (exec-for-iterations test
                            update body cstate funenv limit-equiv)))
 :rule-classes :congruence)

Theorem: exec-switch-rest-swcase-list-equiv-congruence-on-cases

(defthm exec-switch-rest-swcase-list-equiv-congruence-on-cases
 (implies
      (swcase-list-equiv cases cases-equiv)
      (equal (exec-switch-rest cases
                               default target cstate funenv limit)
             (exec-switch-rest cases-equiv
                               default target cstate funenv limit)))
 :rule-classes :congruence)

Theorem: exec-switch-rest-block-option-equiv-congruence-on-default

(defthm exec-switch-rest-block-option-equiv-congruence-on-default
  (implies
       (block-option-equiv default default-equiv)
       (equal (exec-switch-rest cases
                                default target cstate funenv limit)
              (exec-switch-rest cases default-equiv
                                target cstate funenv limit)))
  :rule-classes :congruence)

Theorem: exec-switch-rest-value-equiv-congruence-on-target

(defthm exec-switch-rest-value-equiv-congruence-on-target
  (implies
       (value-equiv target target-equiv)
       (equal (exec-switch-rest cases
                                default target cstate funenv limit)
              (exec-switch-rest cases default
                                target-equiv cstate funenv limit)))
  :rule-classes :congruence)

Theorem: exec-switch-rest-cstate-equiv-congruence-on-cstate

(defthm exec-switch-rest-cstate-equiv-congruence-on-cstate
  (implies
       (cstate-equiv cstate cstate-equiv)
       (equal (exec-switch-rest cases
                                default target cstate funenv limit)
              (exec-switch-rest cases default
                                target cstate-equiv funenv limit)))
  :rule-classes :congruence)

Theorem: exec-switch-rest-funenv-equiv-congruence-on-funenv

(defthm exec-switch-rest-funenv-equiv-congruence-on-funenv
  (implies
       (funenv-equiv funenv funenv-equiv)
       (equal (exec-switch-rest cases
                                default target cstate funenv limit)
              (exec-switch-rest cases default
                                target cstate funenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-switch-rest-nat-equiv-congruence-on-limit

(defthm exec-switch-rest-nat-equiv-congruence-on-limit
  (implies
       (acl2::nat-equiv limit limit-equiv)
       (equal (exec-switch-rest cases
                                default target cstate funenv limit)
              (exec-switch-rest cases default
                                target cstate funenv limit-equiv)))
  :rule-classes :congruence)

Theorem: error-info-wfp-of-exec-expression

(defthm error-info-wfp-of-exec-expression
  (b* ((?outcome (exec-expression expr cstate funenv limit)))
    (implies (reserrp outcome)
             (error-info-wfp outcome))))

Theorem: error-info-wfp-of-exec-expression-list

(defthm error-info-wfp-of-exec-expression-list
  (b* ((?outcome (exec-expression-list exprs cstate funenv limit)))
    (implies (reserrp outcome)
             (error-info-wfp outcome))))

Theorem: error-info-wfp-of-exec-funcall

(defthm error-info-wfp-of-exec-funcall
  (b* ((?outcome (exec-funcall call cstate funenv limit)))
    (implies (reserrp outcome)
             (error-info-wfp outcome))))

Theorem: error-info-wfp-of-exec-function

(defthm error-info-wfp-of-exec-function
  (b* ((?outcome (exec-function fun args cstate funenv limit)))
    (implies (reserrp outcome)
             (error-info-wfp outcome))))

Theorem: error-info-wfp-of-exec-statement

(defthm error-info-wfp-of-exec-statement
  (b* ((?outcome (exec-statement stmt cstate funenv limit)))
    (implies (reserrp outcome)
             (error-info-wfp outcome))))

Theorem: error-info-wfp-of-exec-statement-list

(defthm error-info-wfp-of-exec-statement-list
  (b* ((?outcome (exec-statement-list stmts cstate funenv limit)))
    (implies (reserrp outcome)
             (error-info-wfp outcome))))

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

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

Theorem: error-info-wfp-of-exec-for-iterations

(defthm error-info-wfp-of-exec-for-iterations
 (b*
  ((?outcome
        (exec-for-iterations test update body cstate funenv limit)))
  (implies (reserrp outcome)
           (error-info-wfp outcome))))

Theorem: error-info-wfp-of-exec-switch-rest

(defthm error-info-wfp-of-exec-switch-rest
 (b*
  ((?outcome (exec-switch-rest cases
                               default target cstate funenv limit)))
  (implies (reserrp outcome)
           (error-info-wfp outcome))))

Theorem: statement-kind-when-mode-regular

(defthm statement-kind-when-mode-regular
  (b* ((outcome (exec-statement stmt cstate funenv limit)))
    (implies (and (soutcomep outcome)
                  (mode-case (soutcome->mode outcome)
                             :regular))
             (and (not (equal (statement-kind stmt) :leave))
                  (not (equal (statement-kind stmt) :break))
                  (not (equal (statement-kind stmt)
                              :continue))))))

Subtopics

Exec-statement

Execute a statement.

Exec-function

Execution a function on some values.

Exec-for-iterations

Execute the iterations of a loop statement.

Exec-block

Execute a block.

Exec-switch-rest

Execute the rest of a switch statement, after evaluating the target.

Exec-expression-list

Execute a list of expressions.

Exec-funcall

Execute a function call.

Exec-statement-list

Execute a list of statements.

Exec-expression

Execute an expression.