• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • 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
      • C
        • Syntax-for-tools
        • Atc
        • Transformation-tools
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Implementation-environments
          • Dynamic-semantics
            • Exec-expr
            • Exec
              • Exec-expr
              • Exec-stmt
              • Exec-fun
              • Exec-stmt-while
              • Exec-block-item-list
              • Exec-block-item
              • Exec-obj-declon
              • Exec-stmt-dowhile
              • Exec-initer
            • Exec-expr-pure
            • Exec-arrsub
            • Variable-resolution-preservation
            • Init-value-to-value
            • Apconvert-expr-value
            • Execution-limit-monotonicity
            • Exec-memberp
            • Exec-stmt
            • Exec-address
            • Init-scope
            • Exec-unary
            • Exec-member
            • Exec-fun
            • Exec-stmt-while
            • Eval-iconst
            • Exec-expr-pure-list
            • Exec-binary-strict-pure
            • Variable-visibility-preservation
            • Object-type-preservation
            • Eval-binary-strict-pure
            • Exec-block-item-list
            • Exec-indir
            • Exec-ident
            • Exec-block-item
            • Eval-cast
            • Frame-and-scope-peeling
            • Exec-obj-declon
            • Exec-cast
            • Exec-const
            • Eval-unary
            • Exec-stmt-dowhile
            • Exec-initer
            • Pure-expression-execution
            • Eval-const
            • Execution-without-function-calls
          • Static-semantics
          • Grammar
          • Types
          • Integer-formats-definitions
          • Computation-states
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Object-designators
          • Operations
          • Errors
          • Tag-environments
          • Function-environments
          • Character-sets
          • Flexible-array-member-removal
          • Arithmetic-operations
          • Pointer-operations
          • Real-operations
          • Array-operations
          • Scalar-operations
          • Structure-operations
        • Representation
        • Insertion-sort
        • Pack
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Dynamic-semantics

Exec

Mutually recursive functions for execution.

Definitions and Theorems

Function: exec-fun

(defun exec-fun (fun args compst fenv limit)
  (declare (xargs :guard (and (identp fun)
                              (value-listp args)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (b* (((when (zp limit))
        (mv (error :limit)
            (compustate-fix compst)))
       (info (fun-env-lookup fun fenv))
       ((when (not info))
        (mv (error (list :function-undefined (ident-fix fun)))
            (compustate-fix compst)))
       ((fun-info info) info)
       (scope (init-scope info.params args))
       ((when (errorp scope))
        (mv scope (compustate-fix compst)))
       (frame (make-frame :function fun
                          :scopes (list scope)))
       (compst (push-frame frame compst))
       ((mv sval compst)
        (exec-block-item-list info.body compst fenv (1- limit)))
       (compst (pop-frame compst))
       ((when (errorp sval)) (mv sval compst))
       (val? (stmt-value-case sval
                              :none nil
                              :return sval.value?))
       ((unless (equal (type-of-value-option val?)
                       (tyname-to-type info.result)))
        (mv (error (list :return-value-mistype
                         :required info.result
                         :supplied (type-of-value-option val?)))
            compst)))
    (mv val? compst)))

Function: exec-expr

(defun exec-expr (e compst fenv limit)
 (declare (xargs :guard (and (exprp e)
                             (compustatep compst)
                             (fun-envp fenv)
                             (natp limit))))
 (b* (((when (zp limit))
       (mv (error :limit)
           (compustate-fix compst))))
  (expr-case
   e :ident
   (mv (exec-ident e.get compst)
       (compustate-fix compst))
   :const
   (mv (exec-const e.get)
       (compustate-fix compst))
   :arrsub
   (b* (((unless (and (expr-purep e.arr)
                      (expr-purep e.sub)))
         (mv (error (list :arrsub-nonpure-arg (expr-fix e)))
             (compustate-fix compst)))
        ((mv arr compst)
         (exec-expr e.arr compst fenv (1- limit)))
        ((when (errorp arr)) (mv arr compst))
        ((unless arr)
         (mv (error (list :arrsub-void-expr e.arr))
             compst))
        ((mv sub compst)
         (exec-expr e.sub compst fenv (1- limit)))
        ((when (errorp sub)) (mv sub compst))
        ((unless sub)
         (mv (error (list :arrsub-void-expr e.sub))
             compst)))
     (mv (exec-arrsub arr sub compst)
         compst))
   :call
   (b* ((vals (exec-expr-pure-list e.args compst))
        ((when (errorp vals))
         (mv vals (compustate-fix compst)))
        ((mv val? compst)
         (exec-fun e.fun vals compst fenv (1- limit)))
        ((when (errorp val?)) (mv val? compst)))
     (if val? (mv (make-expr-value :value val?
                                   :object nil)
                  compst)
       (mv nil compst)))
   :member
   (b* (((mv str compst)
         (exec-expr e.target compst fenv (1- limit)))
        ((when (errorp str)) (mv str compst))
        ((unless str)
         (mv (error (list :member-void-expr (expr-fix e)))
             compst)))
     (mv (exec-member str e.name) compst))
   :memberp
   (b* (((mv str compst)
         (exec-expr e.target compst fenv (1- limit)))
        ((when (errorp str)) (mv str compst))
        ((unless str)
         (mv (error (list :memberp-void-expr (expr-fix e)))
             compst)))
     (mv (exec-memberp str e.name compst)
         compst))
   :postinc
   (mv (error (list :expression-not-supported (expr-fix e)))
       (compustate-fix compst))
   :postdec
   (mv (error (list :expression-not-supported (expr-fix e)))
       (compustate-fix compst))
   :preinc
   (mv (error (list :expression-not-supported (expr-fix e)))
       (compustate-fix compst))
   :predec
   (mv (error (list :expression-not-supported (expr-fix e)))
       (compustate-fix compst))
   :unary
   (b* (((mv arg compst)
         (exec-expr e.arg compst fenv (1- limit)))
        ((when (errorp arg)) (mv arg compst))
        ((unless arg)
         (mv (error (list :unary-void-expr e.arg))
             compst)))
     (mv (exec-unary e.op arg compst)
         compst))
   :cast
   (b* (((mv arg compst)
         (exec-expr e.arg compst fenv (1- limit)))
        ((when (errorp arg)) (mv arg compst))
        ((unless arg)
         (mv (error (list :cast-void-expr e.arg))
             compst)))
     (mv (exec-cast e.type arg) compst))
   :binary
   (cond
    ((and (binop-strictp e.op)
          (binop-purep e.op))
     (b*
      (((unless (and (expr-purep e.arg1)
                     (expr-purep e.arg2)))
        (mv
          (error
               (list :pure-strict-binary-nonpure-args (expr-fix e)))
          (compustate-fix compst)))
       ((mv arg1-eval compst)
        (exec-expr e.arg1 compst fenv (1- limit)))
       ((when (errorp arg1-eval))
        (mv arg1-eval compst))
       ((unless arg1-eval)
        (mv (error (list :binary-void-expr e.arg1))
            compst))
       ((mv arg2-eval compst)
        (exec-expr e.arg2 compst fenv (1- limit)))
       ((when (errorp arg2-eval))
        (mv arg2-eval compst))
       ((unless arg2-eval)
        (mv (error (list :binary-void-expr e.arg2))
            compst)))
      (mv (exec-binary-strict-pure e.op arg1-eval arg2-eval)
          compst)))
    ((binop-case e.op :logand)
     (b* (((mv arg1-eval compst)
           (exec-expr e.arg1 compst fenv (1- limit)))
          ((when (errorp arg1-eval))
           (mv arg1-eval compst))
          ((unless arg1-eval)
           (mv (error (list :logand-void-arg (expr-fix e)))
               compst))
          (arg1 (apconvert-expr-value arg1-eval))
          ((when (errorp arg1)) (mv arg1 compst))
          (test1 (test-value (expr-value->value arg1)))
          ((when (errorp test1))
           (mv test1 compst))
          ((when (not test1))
           (mv (make-expr-value :value (value-sint 0)
                                :object nil)
               compst))
          ((mv arg2-eval compst)
           (exec-expr e.arg2 compst fenv (1- limit)))
          ((when (errorp arg2-eval))
           (mv arg2-eval compst))
          ((unless arg2-eval)
           (mv (error (list :logand-void-arg (expr-fix e)))
               compst))
          (arg2 (apconvert-expr-value arg2-eval))
          ((when (errorp arg2)) (mv arg2 compst))
          (test2 (test-value (expr-value->value arg2)))
          ((when (errorp test2))
           (mv test2 compst)))
       (if test2 (mv (make-expr-value :value (value-sint 1)
                                      :object nil)
                     compst)
         (mv (make-expr-value :value (value-sint 0)
                              :object nil)
             compst))))
    ((binop-case e.op :logor)
     (b* (((mv arg1-eval compst)
           (exec-expr e.arg1 compst fenv (1- limit)))
          ((when (errorp arg1-eval))
           (mv arg1-eval compst))
          ((unless arg1-eval)
           (mv (error (list :logor-void-arg (expr-fix e)))
               compst))
          (arg1 (apconvert-expr-value arg1-eval))
          ((when (errorp arg1)) (mv arg1 compst))
          (test1 (test-value (expr-value->value arg1)))
          ((when (errorp test1))
           (mv test1 compst))
          ((when test1)
           (mv (make-expr-value :value (value-sint 1)
                                :object nil)
               compst))
          ((mv arg2-eval compst)
           (exec-expr e.arg2 compst fenv (1- limit)))
          ((when (errorp arg2-eval))
           (mv arg2-eval compst))
          ((unless arg2-eval)
           (mv (error (list :logor-void-arg (expr-fix e)))
               compst))
          (arg2 (apconvert-expr-value arg2-eval))
          ((when (errorp arg2)) (mv arg2 compst))
          (test2 (test-value (expr-value->value arg2)))
          ((when (errorp test2))
           (mv test2 compst)))
       (if test2 (mv (make-expr-value :value (value-sint 1)
                                      :object nil)
                     compst)
         (mv (make-expr-value :value (value-sint 0)
                              :object nil)
             compst))))
    ((binop-case e.op :asg)
     (b* ((left (expr-binary->arg1 e))
          (right (expr-binary->arg2 e))
          ((unless (expr-purep left))
           (mv (error (list :asg-left-nonpure (expr-fix e)))
               (compustate-fix compst)))
          ((unless (or (expr-case left :ident)
                       (expr-purep right)))
           (mv (error (list :asg-right-nonpure (expr-fix e)))
               (compustate-fix compst)))
          ((mv left-eval compst)
           (exec-expr left compst fenv (1- limit)))
          ((when (errorp left-eval))
           (mv left-eval compst))
          ((unless left-eval)
           (mv (error (list :asg-left-void (expr-fix e)))
               compst))
          (left-eval (apconvert-expr-value left-eval))
          ((when (errorp left-eval))
           (mv left-eval compst))
          (objdes (expr-value->object left-eval))
          ((unless objdes)
           (mv (error (list :asg-not-lvalue left))
               compst))
          ((mv right-eval compst)
           (exec-expr right compst fenv (1- limit)))
          ((when (errorp right-eval))
           (mv right-eval compst))
          ((when (not right-eval))
           (mv (error (list :asg-right-void right))
               compst))
          (right-eval (apconvert-expr-value right-eval))
          ((when (errorp right-eval))
           (mv right-eval compst))
          (val (expr-value->value right-eval))
          (compst/error (write-object objdes val compst))
          ((when (errorp compst/error))
           (mv compst/error compst))
          (compst compst/error))
       (mv (make-expr-value :value val :object nil)
           compst)))
    (t (mv (error (list :expression-not-supported (expr-fix e)))
           (compustate-fix compst))))
   :cond
   (b* (((mv test compst)
         (exec-expr e.test compst fenv (1- limit)))
        ((when (errorp test)) (mv test compst))
        ((unless test)
         (mv (error (list :cond-void-test (expr-fix e)))
             compst))
        (test (apconvert-expr-value test))
        ((when (errorp test)) (mv test compst))
        (test (test-value (expr-value->value test)))
        ((when (errorp test)) (mv test compst)))
     (if test (b* (((mv eval compst)
                    (exec-expr e.then compst fenv (1- limit)))
                   ((when (errorp eval)) (mv eval compst))
                   ((unless eval)
                    (mv (error (list :cond-void-then (expr-fix e)))
                        compst))
                   (eval (apconvert-expr-value eval))
                   ((when (errorp eval)) (mv eval compst)))
                (mv (change-expr-value eval :object nil)
                    compst))
       (b* (((mv eval compst)
             (exec-expr e.else compst fenv (1- limit)))
            ((when (errorp eval)) (mv eval compst))
            ((unless eval)
             (mv (error (list :cond-void-else (expr-fix e)))
                 compst))
            (eval (apconvert-expr-value eval))
            ((when (errorp eval)) (mv eval compst)))
         (mv (change-expr-value eval :object nil)
             compst)))))))

Function: exec-stmt

(defun exec-stmt (s compst fenv limit)
 (declare (xargs :guard (and (stmtp s)
                             (compustatep compst)
                             (fun-envp fenv)
                             (natp limit))))
 (declare (xargs :guard (> (compustate-frames-number compst)
                           0)))
 (b* (((when (zp limit))
       (mv (error :limit)
           (compustate-fix compst)))
      (s (stmt-fix s)))
  (stmt-case
     s :labeled
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :compound
     (b* ((compst (enter-scope compst))
          ((mv sval compst)
           (exec-block-item-list s.items compst fenv (1- limit))))
       (mv sval (exit-scope compst)))
     :expr
     (b* (((mv eval compst)
           (exec-expr s.get compst fenv (1- limit)))
          ((when (errorp eval)) (mv eval compst)))
       (mv (stmt-value-none) compst))
     :null
     (mv (stmt-value-none)
         (compustate-fix compst))
     :if
     (b* (((mv test compst)
           (exec-expr s.test compst fenv (1- limit)))
          ((when (errorp test)) (mv test compst))
          ((unless test)
           (mv (error (list :void-if-test s.test))
               compst))
          (test (apconvert-expr-value test))
          ((when (errorp test)) (mv test compst))
          (test (expr-value->value test))
          (test (test-value test))
          ((when (errorp test)) (mv test compst)))
       (if test (exec-stmt s.then compst fenv (1- limit))
         (mv (stmt-value-none) compst)))
     :ifelse
     (b* (((mv test compst)
           (exec-expr s.test compst fenv (1- limit)))
          ((when (errorp test)) (mv test compst))
          ((unless test)
           (mv (error (list :void-ifelse-test s.test))
               compst))
          (test (apconvert-expr-value test))
          ((when (errorp test)) (mv test compst))
          (test (expr-value->value test))
          (test (test-value test))
          ((when (errorp test)) (mv test compst)))
       (if test (exec-stmt s.then compst fenv (1- limit))
         (exec-stmt s.else compst fenv (1- limit))))
     :switch
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :while
     (exec-stmt-while s.test s.body compst fenv (1- limit))
     :dowhile
     (b* ((compst (enter-scope compst))
          ((mv sval compst)
           (exec-stmt-dowhile s.body s.test compst fenv (1- limit)))
          ((when (errorp sval))
           (mv sval (exit-scope compst)))
          (compst (exit-scope compst)))
       (mv sval compst))
     :for
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :goto
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :continue
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :break
     (mv (error (list :exec-stmt s))
         (compustate-fix compst))
     :return
     (if (exprp s.value)
         (b* (((mv eval? compst)
               (exec-expr s.value compst fenv (1- limit)))
              ((when (errorp eval?))
               (mv eval? compst))
              ((when (not eval?))
               (mv (error (list :return-void-expr s.value))
                   compst))
              (eval eval?)
              (eval (apconvert-expr-value eval))
              ((when (errorp eval)) (mv eval compst))
              (val (expr-value->value eval)))
           (mv (stmt-value-return val) compst))
       (mv (stmt-value-return nil)
           (compustate-fix compst))))))

Function: exec-stmt-while

(defun exec-stmt-while (test body compst fenv limit)
  (declare (xargs :guard (and (exprp test)
                              (stmtp body)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (b* (((when (zp limit))
        (mv (error :limit)
            (compustate-fix compst)))
       ((mv test-eval compst)
        (exec-expr test compst fenv (1- limit)))
       ((when (errorp test-eval))
        (mv test-eval compst))
       ((unless test-eval)
        (mv (error (list :void-while-test (expr-fix test)))
            compst))
       (test-eval (apconvert-expr-value test-eval))
       ((when (errorp test-eval))
        (mv test-eval compst))
       (test-val (expr-value->value test-eval))
       (continuep (test-value test-val))
       ((when (errorp continuep))
        (mv continuep compst))
       ((when (not continuep))
        (mv (stmt-value-none) compst))
       ((mv sval compst)
        (exec-stmt body compst fenv (1- limit)))
       ((when (errorp sval)) (mv sval compst))
       ((when (stmt-value-case sval :return))
        (mv sval compst)))
    (exec-stmt-while test body compst fenv (1- limit))))

Function: exec-stmt-dowhile

(defun exec-stmt-dowhile (body test compst fenv limit)
  (declare (xargs :guard (and (stmtp body)
                              (exprp test)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (b* (((when (zp limit))
        (mv (error :limit)
            (compustate-fix compst)))
       (compst (enter-scope compst))
       ((mv sval compst)
        (exec-stmt body compst fenv (1- limit)))
       ((when (errorp sval))
        (mv sval (exit-scope compst)))
       (compst (exit-scope compst))
       ((when (stmt-value-case sval :return))
        (mv sval compst))
       ((mv test-eval compst)
        (exec-expr test compst fenv (1- limit)))
       ((when (errorp test-eval))
        (mv test-eval compst))
       ((unless test-eval)
        (mv (error (list :void-dowhile-test (expr-fix test)))
            compst))
       (test-eval (apconvert-expr-value test-eval))
       ((when (errorp test-eval))
        (mv test-eval compst))
       (test-val (expr-value->value test-eval))
       (continuep (test-value test-val))
       ((when (errorp continuep))
        (mv continuep compst))
       ((when (not continuep))
        (mv (stmt-value-none) compst)))
    (exec-stmt-dowhile body test compst fenv (1- limit))))

Function: exec-initer

(defun exec-initer (initer compst fenv limit)
 (declare (xargs :guard (and (initerp initer)
                             (compustatep compst)
                             (fun-envp fenv)
                             (natp limit))))
 (declare (xargs :guard (> (compustate-frames-number compst)
                           0)))
 (b* (((when (zp limit))
       (mv (error :limit)
           (compustate-fix compst))))
  (initer-case
      initer :single
      (b* (((mv eval compst)
            (exec-expr initer.get compst fenv (1- limit)))
           ((when (errorp eval)) (mv eval compst))
           ((when (not eval))
            (mv (error (list :void-initializer (initer-fix initer)))
                compst))
           (eval (apconvert-expr-value eval))
           ((when (errorp eval)) (mv eval compst))
           (val (expr-value->value eval))
           (ival (init-value-single val)))
        (mv ival compst))
      :list
      (b* ((vals (exec-expr-pure-list initer.get compst))
           ((when (errorp vals))
            (mv vals (compustate-fix compst)))
           (ival (init-value-list vals)))
        (mv ival (compustate-fix compst))))))

Function: exec-obj-declon

(defun exec-obj-declon (declon compst fenv limit)
  (declare (xargs :guard (and (obj-declonp declon)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (b* (((when (zp limit)) (error :limit))
       ((mv var scspec tyname init?)
        (obj-declon-to-ident+scspec+tyname+init declon))
       ((unless (scspecseq-case scspec :none))
        (error :unsupported-storage-class-specifier))
       (type (tyname-to-type tyname))
       ((when (type-case type :array))
        (error :unsupported-local-array))
       ((when (not init?))
        (error :unsupported-no-initializer))
       (init init?)
       ((mv ival compst)
        (exec-initer init compst fenv (1- limit)))
       ((when (errorp ival)) ival)
       (val (init-value-to-value type ival))
       ((when (errorp val)) val))
    (create-var var val compst)))

Function: exec-block-item

(defun exec-block-item (item compst fenv limit)
 (declare (xargs :guard (and (block-itemp item)
                             (compustatep compst)
                             (fun-envp fenv)
                             (natp limit))))
 (declare (xargs :guard (> (compustate-frames-number compst)
                           0)))
 (b* (((when (zp limit))
       (mv (error :limit)
           (compustate-fix compst))))
  (block-item-case
    item :declon
    (b*
     ((new-compst (exec-obj-declon item.get compst fenv (1- limit)))
      ((when (errorp new-compst))
       (mv new-compst (compustate-fix compst))))
     (mv (stmt-value-none) new-compst))
    :stmt (exec-stmt item.get compst fenv (1- limit)))))

Function: exec-block-item-list

(defun exec-block-item-list (items compst fenv limit)
  (declare (xargs :guard (and (block-item-listp items)
                              (compustatep compst)
                              (fun-envp fenv)
                              (natp limit))))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (b* (((when (zp limit))
        (mv (error :limit)
            (compustate-fix compst)))
       ((when (endp items))
        (mv (stmt-value-none)
            (compustate-fix compst)))
       ((mv sval compst)
        (exec-block-item (car items)
                         compst fenv (1- limit)))
       ((when (errorp sval)) (mv sval compst))
       ((when (stmt-value-case sval :return))
        (mv sval compst)))
    (exec-block-item-list (cdr items)
                          compst fenv (1- limit))))

Theorem: return-type-of-exec-fun.result

(defthm return-type-of-exec-fun.result
  (b* (((mv ?result ?new-compst)
        (exec-fun fun args compst fenv limit)))
    (value-option-resultp result))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-fun.new-compst

(defthm return-type-of-exec-fun.new-compst
  (b* (((mv ?result ?new-compst)
        (exec-fun fun args compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-expr.eval

(defthm return-type-of-exec-expr.eval
  (b* (((mv common-lisp::?eval ?new-compst)
        (exec-expr e compst fenv limit)))
    (expr-value-option-resultp eval))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-expr.new-compst

(defthm return-type-of-exec-expr.new-compst
  (b* (((mv common-lisp::?eval ?new-compst)
        (exec-expr e compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-stmt.sval

(defthm return-type-of-exec-stmt.sval
  (b* (((mv ?sval ?new-compst)
        (exec-stmt s compst fenv limit)))
    (stmt-value-resultp sval))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-stmt.new-compst

(defthm return-type-of-exec-stmt.new-compst
  (b* (((mv ?sval ?new-compst)
        (exec-stmt s compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-stmt-while.sval

(defthm return-type-of-exec-stmt-while.sval
  (b* (((mv ?sval ?new-compst)
        (exec-stmt-while test body compst fenv limit)))
    (stmt-value-resultp sval))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-stmt-while.new-compst

(defthm return-type-of-exec-stmt-while.new-compst
  (b* (((mv ?sval ?new-compst)
        (exec-stmt-while test body compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-stmt-dowhile.sval

(defthm return-type-of-exec-stmt-dowhile.sval
  (b* (((mv ?sval ?new-compst)
        (exec-stmt-dowhile body test compst fenv limit)))
    (stmt-value-resultp sval))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-stmt-dowhile.new-compst

(defthm return-type-of-exec-stmt-dowhile.new-compst
  (b* (((mv ?sval ?new-compst)
        (exec-stmt-dowhile body test compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-initer.result

(defthm return-type-of-exec-initer.result
  (b* (((mv ?result ?new-compst)
        (exec-initer initer compst fenv limit)))
    (init-value-resultp result))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-initer.new-compst

(defthm return-type-of-exec-initer.new-compst
  (b* (((mv ?result ?new-compst)
        (exec-initer initer compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-obj-declon.new-compst

(defthm return-type-of-exec-obj-declon.new-compst
  (b* ((?new-compst (exec-obj-declon declon compst fenv limit)))
    (compustate-resultp new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-block-item.sval

(defthm return-type-of-exec-block-item.sval
  (b* (((mv ?sval ?new-compst)
        (exec-block-item item compst fenv limit)))
    (stmt-value-resultp sval))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-block-item.new-compst

(defthm return-type-of-exec-block-item.new-compst
  (b* (((mv ?sval ?new-compst)
        (exec-block-item item compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-block-item-list.sval

(defthm return-type-of-exec-block-item-list.sval
  (b* (((mv ?sval ?new-compst)
        (exec-block-item-list items compst fenv limit)))
    (stmt-value-resultp sval))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-block-item-list.new-compst

(defthm return-type-of-exec-block-item-list.new-compst
  (b* (((mv ?sval ?new-compst)
        (exec-block-item-list items compst fenv limit)))
    (compustatep new-compst))
  :rule-classes :rewrite)

Theorem: compustate-frames-number-of-exec-fun

(defthm compustate-frames-number-of-exec-fun
  (b* (((mv ?result ?new-compst)
        (exec-fun fun args compst fenv limit)))
    (equal (compustate-frames-number new-compst)
           (compustate-frames-number compst))))

Theorem: compustate-frames-number-of-exec-expr

(defthm compustate-frames-number-of-exec-expr
  (b* (((mv common-lisp::?eval ?new-compst)
        (exec-expr e compst fenv limit)))
    (equal (compustate-frames-number new-compst)
           (compustate-frames-number compst))))

Theorem: compustate-frames-number-of-exec-stmt

(defthm compustate-frames-number-of-exec-stmt
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?sval ?new-compst)
                 (exec-stmt s compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-stmt-while

(defthm compustate-frames-number-of-exec-stmt-while
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?sval ?new-compst)
                 (exec-stmt-while test body compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-stmt-dowhile

(defthm compustate-frames-number-of-exec-stmt-dowhile
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?sval ?new-compst)
                 (exec-stmt-dowhile body test compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-initer

(defthm compustate-frames-number-of-exec-initer
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?result ?new-compst)
                 (exec-initer initer compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-block-item

(defthm compustate-frames-number-of-exec-block-item
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?sval ?new-compst)
                 (exec-block-item item compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-frames-number-of-exec-obj-declon

(defthm compustate-frames-number-of-exec-obj-declon
 (implies
      (> (compustate-frames-number compst) 0)
      (b* ((?new-compst (exec-obj-declon declon compst fenv limit)))
        (implies (compustatep new-compst)
                 (equal (compustate-frames-number new-compst)
                        (compustate-frames-number compst))))))

Theorem: compustate-frames-number-of-exec-block-item-list

(defthm compustate-frames-number-of-exec-block-item-list
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?sval ?new-compst)
                 (exec-block-item-list items compst fenv limit)))
             (equal (compustate-frames-number new-compst)
                    (compustate-frames-number compst)))))

Theorem: compustate-scopes-numbers-of-exec-fun

(defthm compustate-scopes-numbers-of-exec-fun
  (b* (((mv ?result ?new-compst)
        (exec-fun fun args compst fenv limit)))
    (equal (compustate-scopes-numbers new-compst)
           (compustate-scopes-numbers compst)))
  :rule-classes nil)

Theorem: compustate-scopes-numbers-of-exec-expr

(defthm compustate-scopes-numbers-of-exec-expr
  (b* (((mv common-lisp::?eval ?new-compst)
        (exec-expr e compst fenv limit)))
    (equal (compustate-scopes-numbers new-compst)
           (compustate-scopes-numbers compst))))

Theorem: compustate-scopes-numbers-of-exec-stmt

(defthm compustate-scopes-numbers-of-exec-stmt
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?sval ?new-compst)
                 (exec-stmt s compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-stmt-while

(defthm compustate-scopes-numbers-of-exec-stmt-while
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?sval ?new-compst)
                 (exec-stmt-while test body compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-stmt-dowhile

(defthm compustate-scopes-numbers-of-exec-stmt-dowhile
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?sval ?new-compst)
                 (exec-stmt-dowhile body test compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-initer

(defthm compustate-scopes-numbers-of-exec-initer
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?result ?new-compst)
                 (exec-initer initer compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-obj-declon

(defthm compustate-scopes-numbers-of-exec-obj-declon
 (implies
      (> (compustate-frames-number compst) 0)
      (b* ((?new-compst (exec-obj-declon declon compst fenv limit)))
        (implies (compustatep new-compst)
                 (equal (compustate-scopes-numbers new-compst)
                        (compustate-scopes-numbers compst))))))

Theorem: compustate-scopes-numbers-of-exec-block-item

(defthm compustate-scopes-numbers-of-exec-block-item
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?sval ?new-compst)
                 (exec-block-item item compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: compustate-scopes-numbers-of-exec-block-item-list

(defthm compustate-scopes-numbers-of-exec-block-item-list
  (implies (> (compustate-frames-number compst) 0)
           (b* (((mv ?sval ?new-compst)
                 (exec-block-item-list items compst fenv limit)))
             (equal (compustate-scopes-numbers new-compst)
                    (compustate-scopes-numbers compst)))))

Theorem: exec-fun-of-ident-fix-fun

(defthm exec-fun-of-ident-fix-fun
  (equal (exec-fun (ident-fix fun)
                   args compst fenv limit)
         (exec-fun fun args compst fenv limit)))

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

(defthm exec-fun-of-value-list-fix-args
  (equal (exec-fun fun (value-list-fix args)
                   compst fenv limit)
         (exec-fun fun args compst fenv limit)))

Theorem: exec-fun-of-compustate-fix-compst

(defthm exec-fun-of-compustate-fix-compst
  (equal (exec-fun fun args (compustate-fix compst)
                   fenv limit)
         (exec-fun fun args compst fenv limit)))

Theorem: exec-fun-of-fun-env-fix-fenv

(defthm exec-fun-of-fun-env-fix-fenv
  (equal (exec-fun fun args compst (fun-env-fix fenv)
                   limit)
         (exec-fun fun args compst fenv limit)))

Theorem: exec-fun-of-nfix-limit

(defthm exec-fun-of-nfix-limit
  (equal (exec-fun fun args compst fenv (nfix limit))
         (exec-fun fun args compst fenv limit)))

Theorem: exec-expr-of-expr-fix-e

(defthm exec-expr-of-expr-fix-e
  (equal (exec-expr (expr-fix e)
                    compst fenv limit)
         (exec-expr e compst fenv limit)))

Theorem: exec-expr-of-compustate-fix-compst

(defthm exec-expr-of-compustate-fix-compst
  (equal (exec-expr e (compustate-fix compst)
                    fenv limit)
         (exec-expr e compst fenv limit)))

Theorem: exec-expr-of-fun-env-fix-fenv

(defthm exec-expr-of-fun-env-fix-fenv
  (equal (exec-expr e compst (fun-env-fix fenv)
                    limit)
         (exec-expr e compst fenv limit)))

Theorem: exec-expr-of-nfix-limit

(defthm exec-expr-of-nfix-limit
  (equal (exec-expr e compst fenv (nfix limit))
         (exec-expr e compst fenv limit)))

Theorem: exec-stmt-of-stmt-fix-s

(defthm exec-stmt-of-stmt-fix-s
  (equal (exec-stmt (stmt-fix s)
                    compst fenv limit)
         (exec-stmt s compst fenv limit)))

Theorem: exec-stmt-of-compustate-fix-compst

(defthm exec-stmt-of-compustate-fix-compst
  (equal (exec-stmt s (compustate-fix compst)
                    fenv limit)
         (exec-stmt s compst fenv limit)))

Theorem: exec-stmt-of-fun-env-fix-fenv

(defthm exec-stmt-of-fun-env-fix-fenv
  (equal (exec-stmt s compst (fun-env-fix fenv)
                    limit)
         (exec-stmt s compst fenv limit)))

Theorem: exec-stmt-of-nfix-limit

(defthm exec-stmt-of-nfix-limit
  (equal (exec-stmt s compst fenv (nfix limit))
         (exec-stmt s compst fenv limit)))

Theorem: exec-stmt-while-of-expr-fix-test

(defthm exec-stmt-while-of-expr-fix-test
  (equal (exec-stmt-while (expr-fix test)
                          body compst fenv limit)
         (exec-stmt-while test body compst fenv limit)))

Theorem: exec-stmt-while-of-stmt-fix-body

(defthm exec-stmt-while-of-stmt-fix-body
  (equal (exec-stmt-while test (stmt-fix body)
                          compst fenv limit)
         (exec-stmt-while test body compst fenv limit)))

Theorem: exec-stmt-while-of-compustate-fix-compst

(defthm exec-stmt-while-of-compustate-fix-compst
  (equal (exec-stmt-while test body (compustate-fix compst)
                          fenv limit)
         (exec-stmt-while test body compst fenv limit)))

Theorem: exec-stmt-while-of-fun-env-fix-fenv

(defthm exec-stmt-while-of-fun-env-fix-fenv
  (equal (exec-stmt-while test body compst (fun-env-fix fenv)
                          limit)
         (exec-stmt-while test body compst fenv limit)))

Theorem: exec-stmt-while-of-nfix-limit

(defthm exec-stmt-while-of-nfix-limit
  (equal (exec-stmt-while test body compst fenv (nfix limit))
         (exec-stmt-while test body compst fenv limit)))

Theorem: exec-stmt-dowhile-of-stmt-fix-body

(defthm exec-stmt-dowhile-of-stmt-fix-body
  (equal (exec-stmt-dowhile (stmt-fix body)
                            test compst fenv limit)
         (exec-stmt-dowhile body test compst fenv limit)))

Theorem: exec-stmt-dowhile-of-expr-fix-test

(defthm exec-stmt-dowhile-of-expr-fix-test
  (equal (exec-stmt-dowhile body (expr-fix test)
                            compst fenv limit)
         (exec-stmt-dowhile body test compst fenv limit)))

Theorem: exec-stmt-dowhile-of-compustate-fix-compst

(defthm exec-stmt-dowhile-of-compustate-fix-compst
  (equal (exec-stmt-dowhile body test (compustate-fix compst)
                            fenv limit)
         (exec-stmt-dowhile body test compst fenv limit)))

Theorem: exec-stmt-dowhile-of-fun-env-fix-fenv

(defthm exec-stmt-dowhile-of-fun-env-fix-fenv
  (equal (exec-stmt-dowhile body test compst (fun-env-fix fenv)
                            limit)
         (exec-stmt-dowhile body test compst fenv limit)))

Theorem: exec-stmt-dowhile-of-nfix-limit

(defthm exec-stmt-dowhile-of-nfix-limit
  (equal (exec-stmt-dowhile body test compst fenv (nfix limit))
         (exec-stmt-dowhile body test compst fenv limit)))

Theorem: exec-initer-of-initer-fix-initer

(defthm exec-initer-of-initer-fix-initer
  (equal (exec-initer (initer-fix initer)
                      compst fenv limit)
         (exec-initer initer compst fenv limit)))

Theorem: exec-initer-of-compustate-fix-compst

(defthm exec-initer-of-compustate-fix-compst
  (equal (exec-initer initer (compustate-fix compst)
                      fenv limit)
         (exec-initer initer compst fenv limit)))

Theorem: exec-initer-of-fun-env-fix-fenv

(defthm exec-initer-of-fun-env-fix-fenv
  (equal (exec-initer initer compst (fun-env-fix fenv)
                      limit)
         (exec-initer initer compst fenv limit)))

Theorem: exec-initer-of-nfix-limit

(defthm exec-initer-of-nfix-limit
  (equal (exec-initer initer compst fenv (nfix limit))
         (exec-initer initer compst fenv limit)))

Theorem: exec-obj-declon-of-obj-declon-fix-declon

(defthm exec-obj-declon-of-obj-declon-fix-declon
  (equal (exec-obj-declon (obj-declon-fix declon)
                          compst fenv limit)
         (exec-obj-declon declon compst fenv limit)))

Theorem: exec-obj-declon-of-compustate-fix-compst

(defthm exec-obj-declon-of-compustate-fix-compst
  (equal (exec-obj-declon declon (compustate-fix compst)
                          fenv limit)
         (exec-obj-declon declon compst fenv limit)))

Theorem: exec-obj-declon-of-fun-env-fix-fenv

(defthm exec-obj-declon-of-fun-env-fix-fenv
  (equal (exec-obj-declon declon compst (fun-env-fix fenv)
                          limit)
         (exec-obj-declon declon compst fenv limit)))

Theorem: exec-obj-declon-of-nfix-limit

(defthm exec-obj-declon-of-nfix-limit
  (equal (exec-obj-declon declon compst fenv (nfix limit))
         (exec-obj-declon declon compst fenv limit)))

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

(defthm exec-block-item-of-block-item-fix-item
  (equal (exec-block-item (block-item-fix item)
                          compst fenv limit)
         (exec-block-item item compst fenv limit)))

Theorem: exec-block-item-of-compustate-fix-compst

(defthm exec-block-item-of-compustate-fix-compst
  (equal (exec-block-item item (compustate-fix compst)
                          fenv limit)
         (exec-block-item item compst fenv limit)))

Theorem: exec-block-item-of-fun-env-fix-fenv

(defthm exec-block-item-of-fun-env-fix-fenv
  (equal (exec-block-item item compst (fun-env-fix fenv)
                          limit)
         (exec-block-item item compst fenv limit)))

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

(defthm exec-block-item-of-nfix-limit
  (equal (exec-block-item item compst fenv (nfix limit))
         (exec-block-item item compst fenv limit)))

Theorem: exec-block-item-list-of-block-item-list-fix-items

(defthm exec-block-item-list-of-block-item-list-fix-items
  (equal (exec-block-item-list (block-item-list-fix items)
                               compst fenv limit)
         (exec-block-item-list items compst fenv limit)))

Theorem: exec-block-item-list-of-compustate-fix-compst

(defthm exec-block-item-list-of-compustate-fix-compst
  (equal (exec-block-item-list items (compustate-fix compst)
                               fenv limit)
         (exec-block-item-list items compst fenv limit)))

Theorem: exec-block-item-list-of-fun-env-fix-fenv

(defthm exec-block-item-list-of-fun-env-fix-fenv
  (equal (exec-block-item-list items compst (fun-env-fix fenv)
                               limit)
         (exec-block-item-list items compst fenv limit)))

Theorem: exec-block-item-list-of-nfix-limit

(defthm exec-block-item-list-of-nfix-limit
  (equal (exec-block-item-list items compst fenv (nfix limit))
         (exec-block-item-list items compst fenv limit)))

Theorem: exec-fun-ident-equiv-congruence-on-fun

(defthm exec-fun-ident-equiv-congruence-on-fun
  (implies (ident-equiv fun fun-equiv)
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun fun-equiv args compst fenv limit)))
  :rule-classes :congruence)

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

(defthm exec-fun-value-list-equiv-congruence-on-args
  (implies (value-list-equiv args args-equiv)
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun fun args-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-fun-compustate-equiv-congruence-on-compst

(defthm exec-fun-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun fun args compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-fun-fun-env-equiv-congruence-on-fenv

(defthm exec-fun-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun fun args compst fenv-equiv limit)))
  :rule-classes :congruence)

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

(defthm exec-fun-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-fun fun args compst fenv limit)
                  (exec-fun fun args compst fenv limit-equiv)))
  :rule-classes :congruence)

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

(defthm exec-expr-expr-equiv-congruence-on-e
  (implies (expr-equiv e e-equiv)
           (equal (exec-expr e compst fenv limit)
                  (exec-expr e-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-expr-compustate-equiv-congruence-on-compst

(defthm exec-expr-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-expr e compst fenv limit)
                  (exec-expr e compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-expr-fun-env-equiv-congruence-on-fenv

(defthm exec-expr-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-expr e compst fenv limit)
                  (exec-expr e compst fenv-equiv limit)))
  :rule-classes :congruence)

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

(defthm exec-expr-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-expr e compst fenv limit)
                  (exec-expr e compst fenv limit-equiv)))
  :rule-classes :congruence)

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

(defthm exec-stmt-stmt-equiv-congruence-on-s
  (implies (stmt-equiv s s-equiv)
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt s-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-compustate-equiv-congruence-on-compst

(defthm exec-stmt-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt s compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-fun-env-equiv-congruence-on-fenv

(defthm exec-stmt-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt s compst fenv-equiv limit)))
  :rule-classes :congruence)

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

(defthm exec-stmt-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt s compst fenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-stmt-while-expr-equiv-congruence-on-test

(defthm exec-stmt-while-expr-equiv-congruence-on-test
  (implies
       (expr-equiv test test-equiv)
       (equal (exec-stmt-while test body compst fenv limit)
              (exec-stmt-while test-equiv body compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-while-stmt-equiv-congruence-on-body

(defthm exec-stmt-while-stmt-equiv-congruence-on-body
  (implies
       (stmt-equiv body body-equiv)
       (equal (exec-stmt-while test body compst fenv limit)
              (exec-stmt-while test body-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-while-compustate-equiv-congruence-on-compst

(defthm exec-stmt-while-compustate-equiv-congruence-on-compst
  (implies
       (compustate-equiv compst compst-equiv)
       (equal (exec-stmt-while test body compst fenv limit)
              (exec-stmt-while test body compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-while-fun-env-equiv-congruence-on-fenv

(defthm exec-stmt-while-fun-env-equiv-congruence-on-fenv
  (implies
       (fun-env-equiv fenv fenv-equiv)
       (equal (exec-stmt-while test body compst fenv limit)
              (exec-stmt-while test body compst fenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-stmt-while-nat-equiv-congruence-on-limit

(defthm exec-stmt-while-nat-equiv-congruence-on-limit
  (implies
       (acl2::nat-equiv limit limit-equiv)
       (equal (exec-stmt-while test body compst fenv limit)
              (exec-stmt-while test body compst fenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-stmt-dowhile-stmt-equiv-congruence-on-body

(defthm exec-stmt-dowhile-stmt-equiv-congruence-on-body
 (implies
      (stmt-equiv body body-equiv)
      (equal (exec-stmt-dowhile body test compst fenv limit)
             (exec-stmt-dowhile body-equiv test compst fenv limit)))
 :rule-classes :congruence)

Theorem: exec-stmt-dowhile-expr-equiv-congruence-on-test

(defthm exec-stmt-dowhile-expr-equiv-congruence-on-test
 (implies
      (expr-equiv test test-equiv)
      (equal (exec-stmt-dowhile body test compst fenv limit)
             (exec-stmt-dowhile body test-equiv compst fenv limit)))
 :rule-classes :congruence)

Theorem: exec-stmt-dowhile-compustate-equiv-congruence-on-compst

(defthm exec-stmt-dowhile-compustate-equiv-congruence-on-compst
 (implies
      (compustate-equiv compst compst-equiv)
      (equal (exec-stmt-dowhile body test compst fenv limit)
             (exec-stmt-dowhile body test compst-equiv fenv limit)))
 :rule-classes :congruence)

Theorem: exec-stmt-dowhile-fun-env-equiv-congruence-on-fenv

(defthm exec-stmt-dowhile-fun-env-equiv-congruence-on-fenv
 (implies
      (fun-env-equiv fenv fenv-equiv)
      (equal (exec-stmt-dowhile body test compst fenv limit)
             (exec-stmt-dowhile body test compst fenv-equiv limit)))
 :rule-classes :congruence)

Theorem: exec-stmt-dowhile-nat-equiv-congruence-on-limit

(defthm exec-stmt-dowhile-nat-equiv-congruence-on-limit
 (implies
      (acl2::nat-equiv limit limit-equiv)
      (equal (exec-stmt-dowhile body test compst fenv limit)
             (exec-stmt-dowhile body test compst fenv limit-equiv)))
 :rule-classes :congruence)

Theorem: exec-initer-initer-equiv-congruence-on-initer

(defthm exec-initer-initer-equiv-congruence-on-initer
  (implies (initer-equiv initer initer-equiv)
           (equal (exec-initer initer compst fenv limit)
                  (exec-initer initer-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-initer-compustate-equiv-congruence-on-compst

(defthm exec-initer-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-initer initer compst fenv limit)
                  (exec-initer initer compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-initer-fun-env-equiv-congruence-on-fenv

(defthm exec-initer-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-initer initer compst fenv limit)
                  (exec-initer initer compst fenv-equiv limit)))
  :rule-classes :congruence)

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

(defthm exec-initer-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-initer initer compst fenv limit)
                  (exec-initer initer compst fenv limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-obj-declon-obj-declon-equiv-congruence-on-declon

(defthm exec-obj-declon-obj-declon-equiv-congruence-on-declon
  (implies (obj-declon-equiv declon declon-equiv)
           (equal (exec-obj-declon declon compst fenv limit)
                  (exec-obj-declon declon-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-obj-declon-compustate-equiv-congruence-on-compst

(defthm exec-obj-declon-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-obj-declon declon compst fenv limit)
                  (exec-obj-declon declon compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-obj-declon-fun-env-equiv-congruence-on-fenv

(defthm exec-obj-declon-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-obj-declon declon compst fenv limit)
                  (exec-obj-declon declon compst fenv-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-obj-declon-nat-equiv-congruence-on-limit

(defthm exec-obj-declon-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-obj-declon declon compst fenv limit)
                  (exec-obj-declon declon compst fenv limit-equiv)))
  :rule-classes :congruence)

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

(defthm exec-block-item-block-item-equiv-congruence-on-item
  (implies (block-item-equiv item item-equiv)
           (equal (exec-block-item item compst fenv limit)
                  (exec-block-item item-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-block-item-compustate-equiv-congruence-on-compst

(defthm exec-block-item-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (exec-block-item item compst fenv limit)
                  (exec-block-item item compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-block-item-fun-env-equiv-congruence-on-fenv

(defthm exec-block-item-fun-env-equiv-congruence-on-fenv
  (implies (fun-env-equiv fenv fenv-equiv)
           (equal (exec-block-item item compst fenv limit)
                  (exec-block-item item compst fenv-equiv limit)))
  :rule-classes :congruence)

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

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

Theorem: exec-block-item-list-block-item-list-equiv-congruence-on-items

(defthm
     exec-block-item-list-block-item-list-equiv-congruence-on-items
  (implies
       (block-item-list-equiv items items-equiv)
       (equal (exec-block-item-list items compst fenv limit)
              (exec-block-item-list items-equiv compst fenv limit)))
  :rule-classes :congruence)

Theorem: exec-block-item-list-compustate-equiv-congruence-on-compst

(defthm exec-block-item-list-compustate-equiv-congruence-on-compst
  (implies
       (compustate-equiv compst compst-equiv)
       (equal (exec-block-item-list items compst fenv limit)
              (exec-block-item-list items compst-equiv fenv limit)))
  :rule-classes :congruence)

Theorem: exec-block-item-list-fun-env-equiv-congruence-on-fenv

(defthm exec-block-item-list-fun-env-equiv-congruence-on-fenv
  (implies
       (fun-env-equiv fenv fenv-equiv)
       (equal (exec-block-item-list items compst fenv limit)
              (exec-block-item-list items compst fenv-equiv limit)))
  :rule-classes :congruence)

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

(defthm exec-block-item-list-nat-equiv-congruence-on-limit
  (implies
       (acl2::nat-equiv limit limit-equiv)
       (equal (exec-block-item-list items compst fenv limit)
              (exec-block-item-list items compst fenv limit-equiv)))
  :rule-classes :congruence)

Subtopics

Exec-expr

Execute an expression.

Exec-stmt

Execute a statement.

Exec-fun

Execute a function on argument values.

Exec-stmt-while

Execute a while statement.

Exec-block-item-list

Execute a list of block items.

Exec-block-item

Execute a block item.

Exec-obj-declon

Execute an object declaration.

Exec-stmt-dowhile

Execute a do-while statement.

Exec-initer

Execute an initializer.