• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
      • Aleobft
      • Aleovm
      • Leo
        • Grammar
        • Early-version
          • Json2ast
          • Testing
          • Definition
            • Flattening
            • Abstract-syntax
            • Dynamic-semantics
              • Execution
                • Exec-expressions/statements
                  • Exec-expression
                  • Exec-statement
                  • Exec-for-loop-iterations
                  • Exec-if
                  • Exec-function
                  • Exec-statement-list
                  • Exec-block
                  • Exec-struct-init-list
                  • Exec-struct-init
                  • Exec-expression-list
                • Init-for-loop
                • Exec-file-main
                • Update-variable-value-in-scope-list
                • Step-for-loop
                • Update-variable-value-in-scope
                • Expr-value-to-value
                • Exec-binary
                • Exec-expression
                • Init-vcscope-dinfo-call
                • Value?+denv
                • Exec-statement
                • End-of-for-loop-p
                • Expr-value
                • Evalue+denv
                • Write-location
                • Read-location
                • Exec-for-loop-iterations
                • Update-variable-value
                • Exec-unary
                • Values+denv
                • Init-vcscope-dinfo-loop
                • Extend-denv-with-structdecl
                • Exec-var/const
                • Valuemap+denv
                • Namevalue+denv
                • Extend-denv-with-fundecl
                • Ensure-boolean
                • Int+denv
                • Push-vcscope-dinfo
                • Extend-denv-with-topdecl-list
                • Exec-literal
                • Build-denv-from-file
                • Namevalue+denv-result
                • Extend-denv-with-topdecl
                • Evalue+denv-result
                • Value?+denv-result
                • Values+denv-result
                • Valuemap+denv-result
                • Int+denv-result
                • Push-call-dinfo
                • Exec-print
                • Pop-vcscope-dinfo
                • Exec-if
                • Exec-function
                • Pop-call-dinfo
                • Exec-statement-list
                • Exec-block
                • Exec-struct-init-list
                • Exec-struct-init
                • Exec-expression-list
              • Values
              • Dynamic-environments
              • Arithmetic-operations
              • Curve-parameterization
              • Shift-operations
              • Errors
              • Value-expressions
              • Locations
              • Input-execution
              • Edwards-bls12-generator
              • Equality-operations
              • Logical-operations
              • Program-execution
              • Ordering-operations
              • Bitwise-operations
              • Literal-evaluation
              • Type-maps-for-struct-components
              • Output-execution
              • Tuple-operations
              • Struct-operations
            • Compilation
            • Static-semantics
            • Concrete-syntax
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Execution

Exec-expressions/statements

Execute expressions and statements.

Definitions and Theorems

Function: exec-expression

(defun exec-expression (expr env limit)
 (declare (xargs :guard (and (expressionp expr)
                             (denvp env)
                             (natp limit))))
 (let ((__function__ 'exec-expression))
  (declare (ignorable __function__))
  (b* (((when (zp limit)) (reserrf :limit)))
   (expression-case
    expr
    :literal (exec-literal expr.get env)
    :var/const
    (exec-var/const expr.name env)
    :assoc-const (reserrf :todo)
    :unary
    (b*
     (((when
        (and (unop-case expr.op :neg)
             (equal expr.arg
                    (expression-literal
                         (make-literal-signed :val (expt 2 7)
                                              :size (bitsize-8))))))
       (make-evalue+denv
            :evalue (expr-value-value (value-i8 (- (expt 2 7))))
            :denv env))
      ((when
        (and
            (unop-case expr.op :neg)
            (equal expr.arg
                   (expression-literal
                        (make-literal-signed :val (expt 2 15)
                                             :size (bitsize-16))))))
       (make-evalue+denv
            :evalue (expr-value-value (value-i16 (- (expt 2 15))))
            :denv env))
      ((when
        (and
            (unop-case expr.op :neg)
            (equal expr.arg
                   (expression-literal
                        (make-literal-signed :val (expt 2 31)
                                             :size (bitsize-32))))))
       (make-evalue+denv
            :evalue (expr-value-value (value-i32 (- (expt 2 31))))
            :denv env))
      ((when
        (and
            (unop-case expr.op :neg)
            (equal expr.arg
                   (expression-literal
                        (make-literal-signed :val (expt 2 63)
                                             :size (bitsize-64))))))
       (make-evalue+denv
            :evalue (expr-value-value (value-i64 (- (expt 2 63))))
            :denv env))
      ((when
        (and
           (unop-case expr.op :neg)
           (equal expr.arg
                  (expression-literal
                       (make-literal-signed :val (expt 2 127)
                                            :size (bitsize-128))))))
       (make-evalue+denv
            :evalue (expr-value-value (value-i128 (- (expt 2 127))))
            :denv env))
      ((okf arg+denv)
       (exec-expression expr.arg env (1- limit)))
      ((evalue+denv arg+denv) arg+denv)
      (arg arg+denv.evalue)
      (env arg+denv.denv))
     (exec-unary expr.op arg env))
    :binary
    (b* (((okf arg1+denv)
          (exec-expression expr.arg1 env (1- limit)))
         ((evalue+denv arg1+denv) arg1+denv)
         (arg1 arg1+denv.evalue)
         (env arg1+denv.denv)
         ((okf arg2+denv)
          (exec-expression expr.arg2 env (1- limit)))
         ((evalue+denv arg2+denv) arg2+denv)
         (arg2 arg2+denv.evalue)
         (env arg2+denv.denv))
      (exec-binary expr.op arg1 arg2 env))
    :cond
    (b* (((okf test+denv)
          (exec-expression expr.test env (1- limit)))
         ((evalue+denv test+denv) test+denv)
         (test test+denv.evalue)
         (env test+denv.denv)
         ((okf test) (ensure-boolean test env)))
      (if test (exec-expression expr.then env (1- limit))
        (exec-expression expr.else env (1- limit))))
    :unit
    (make-evalue+denv :evalue (expr-value-value (op-tuple-make nil))
                      :denv env)
    :tuple
    (b* (((okf vals+env)
          (exec-expression-list expr.components env (1- limit)))
         (vals (values+denv->values vals+env))
         (env (values+denv->denv vals+env))
         (val (op-tuple-make vals))
         (eval (expr-value-value val)))
      (make-evalue+denv :evalue eval
                        :denv env))
    :tuple-component
    (b* (((okf eval+env)
          (exec-expression expr.tuple env (1- limit)))
         (eval (evalue+denv->evalue eval+env))
         (env (evalue+denv->denv eval+env)))
     (expr-value-case
      eval :location
      (make-evalue+denv
          :evalue (expr-value-location
                       (make-location-tuple-comp :tuple eval.get
                                                 :index expr.index))
          :denv env)
      :value
      (b* (((okf comp)
            (op-tuple-read eval.get expr.index)))
        (make-evalue+denv :evalue (expr-value-value comp)
                          :denv env))))
    :struct
    (b* (((okf valmap+env)
          (exec-struct-init-list expr.components env (1- limit)))
         (valmap (valuemap+denv->valuemap valmap+env))
         (env (valuemap+denv->denv valmap+env))
         ((okf val)
          (op-struct-make expr.type valmap (denv->structs env)))
         (eval (expr-value-value val)))
      (make-evalue+denv :evalue eval
                        :denv env))
    :struct-component
    (b* (((okf eval+env)
          (exec-expression expr.struct env (1- limit)))
         (eval (evalue+denv->evalue eval+env))
         (env (evalue+denv->denv eval+env)))
     (expr-value-case
         eval :location
         (make-evalue+denv
              :evalue
              (expr-value-location
                   (make-location-struct-comp :struct eval.get
                                              :name expr.component))
              :denv env)
         :value
         (b* (((okf comp)
               (op-struct-read eval.get expr.component)))
           (make-evalue+denv :evalue (expr-value-value comp)
                             :denv env))))
    :internal-call
    (b* (((okf vals+denv)
          (exec-expression-list expr.args env (1- limit)))
         ((values+denv vals+denv) vals+denv)
         (vals vals+denv.values)
         (env vals+denv.denv))
      (exec-function expr.fun vals env (1- limit)))
    :external-call (reserrf :todo)
    :static-call (reserrf :todo)))))

Function: exec-expression-list

(defun exec-expression-list (exprs env limit)
  (declare (xargs :guard (and (expression-listp exprs)
                              (denvp env)
                              (natp limit))))
  (let ((__function__ 'exec-expression-list))
    (declare (ignorable __function__))
    (b* (((when (zp limit)) (reserrf :limit))
         ((when (endp exprs))
          (make-values+denv :values nil
                            :denv (denv-fix env)))
         ((okf eval+denv)
          (exec-expression (car exprs)
                           env (1- limit)))
         ((evalue+denv eval+denv) eval+denv)
         (eval eval+denv.evalue)
         (env eval+denv.denv)
         ((okf val)
          (expr-value-to-value eval env))
         ((okf vals+denv)
          (exec-expression-list (cdr exprs)
                                env (1- limit)))
         ((values+denv vals+denv) vals+denv)
         (vals vals+denv.values)
         (env vals+denv.denv))
      (make-values+denv :values (cons val vals)
                        :denv env))))

Function: exec-struct-init

(defun exec-struct-init (init env limit)
  (declare (xargs :guard (and (struct-initp init)
                              (denvp env)
                              (natp limit))))
  (let ((__function__ 'exec-struct-init))
    (declare (ignorable __function__))
    (b* (((when (zp limit)) (reserrf :limit))
         ((okf eval+env)
          (exec-expression (struct-init->expr init)
                           env (1- limit)))
         (eval (evalue+denv->evalue eval+env))
         (env (evalue+denv->denv eval+env))
         ((okf val)
          (expr-value-to-value eval env))
         (nameval (make-name+value :name (struct-init->name init)
                                   :value val)))
      (make-namevalue+denv :namevalue nameval
                           :denv env))))

Function: exec-struct-init-list

(defun exec-struct-init-list (inits env limit)
  (declare (xargs :guard (and (struct-init-listp inits)
                              (denvp env)
                              (natp limit))))
  (let ((__function__ 'exec-struct-init-list))
    (declare (ignorable __function__))
    (b* (((when (zp limit)) (reserrf :limit))
         ((when (endp inits))
          (make-valuemap+denv :valuemap nil
                              :denv (denv-fix env)))
         ((okf nameval+env)
          (exec-struct-init (car inits)
                            env (1- limit)))
         (nameval (namevalue+denv->namevalue nameval+env))
         (env (namevalue+denv->denv nameval+env))
         (name (name+value->name nameval))
         (val (name+value->value nameval))
         ((okf valmap+env)
          (exec-struct-init-list (cdr inits)
                                 env (1- limit)))
         (valmap (valuemap+denv->valuemap valmap+env))
         (env (valuemap+denv->denv valmap+env))
         ((when (consp (omap::assoc name valmap)))
          (reserrf (list :duplicate-component name)))
         (valmap (omap::update name val valmap)))
      (make-valuemap+denv :valuemap valmap
                          :denv env))))

Function: exec-function

(defun exec-function (fun args env limit)
  (declare (xargs :guard (and (identifierp fun)
                              (value-listp args)
                              (denvp env)
                              (natp limit))))
  (let ((__function__ 'exec-function))
    (declare (ignorable __function__))
    (b* (((when (zp limit)) (reserrf :limit))
         (finfo (get-function-dinfo fun (denv->functions env)))
         ((unless finfo)
          (reserrf (list :function-not-found (identifier-fix fun))))
         ((function-dinfo finfo) finfo)
         ((okf scope)
          (init-vcscope-dinfo-call finfo.inputs args))
         (frame (make-call-dinfo :fun fun
                                 :scopes (list scope)))
         (env (push-call-dinfo frame env))
         ((okf val?+env)
          (exec-statement-list finfo.body env (1- limit)))
         (val? (value?+denv->value? val?+env))
         (env (value?+denv->denv val?+env))
         ((unless val?)
          (reserrf (list :no-value-returned (identifier-fix fun))))
         ((unless (equal (type-of-value val?)
                         finfo.output))
          (reserrf (list :return-type-mismatch
                         :required finfo.output
                         :returned val?)))
         ((okf env) (pop-call-dinfo env)))
      (make-evalue+denv :evalue (expr-value-value val?)
                        :denv env))))

Function: exec-statement

(defun exec-statement (stmt env limit)
 (declare (xargs :guard (and (statementp stmt)
                             (denvp env)
                             (natp limit))))
 (let ((__function__ 'exec-statement))
  (declare (ignorable __function__))
  (b* (((when (zp limit)) (reserrf :limit)))
   (statement-case
    stmt :let
    (b* (((vardecl decl) stmt.get)
         ((okf eval+env)
          (exec-expression decl.init env (1- limit)))
         (env (evalue+denv->denv eval+env))
         ((okf val)
          (expr-value-to-value (evalue+denv->evalue eval+env)
                               env))
         ((unless (equal (type-of-value val) decl.type))
          (reserrf (list :let-mismatch
                         :required decl.type
                         :supplied val)))
         (info (make-var/const-dinfo :value val
                                     :constp nil))
         (env (add-var/const-dinfo decl.name info env))
         ((unless env)
          (reserrf (list :variable-exists decl.name))))
      (make-value?+denv :value? nil
                        :denv env))
    :const
    (b* (((constdecl decl) stmt.get)
         ((okf eval+env)
          (exec-expression decl.init env (1- limit)))
         (env (evalue+denv->denv eval+env))
         ((okf val)
          (expr-value-to-value (evalue+denv->evalue eval+env)
                               env))
         ((unless (equal (type-of-value val) decl.type))
          (reserrf (list :let-mismatch
                         :required decl.type
                         :supplied val)))
         (info (make-var/const-dinfo :value val
                                     :constp t))
         (env (add-var/const-dinfo decl.name info env))
         ((unless env)
          (reserrf (list :variable-exists decl.name))))
      (make-value?+denv :value? nil
                        :denv env))
    :assign
    (b* (((okf left+env)
          (exec-expression stmt.left env (1- limit)))
         (left (evalue+denv->evalue left+env))
         (env (evalue+denv->denv left+env))
         ((unless (expr-value-case left :location))
          (reserrf (list :assignment-to-non-location left)))
         (loc (expr-value-location->get left))
         ((okf right+env)
          (exec-expression stmt.right env (1- limit)))
         (right (evalue+denv->evalue right+env))
         (env (evalue+denv->denv right+env))
         ((okf right)
          (expr-value-to-value right env))
         ((okf env)
          (write-location loc right env)))
      (make-value?+denv :value? nil
                        :denv env))
    :return
    (b* (((okf val+env)
          (exec-expression stmt.value env (1- limit)))
         (val (evalue+denv->evalue val+env))
         (env (evalue+denv->denv val+env))
         ((okf val)
          (expr-value-to-value val env)))
      (make-value?+denv :value? val
                        :denv env))
    :for
    (b* (((okf from+env)
          (exec-expression stmt.from env (1- limit)))
         (from (evalue+denv->evalue from+env))
         (env (evalue+denv->denv from+env))
         ((okf to+env)
          (exec-expression stmt.to env (1- limit)))
         (to (evalue+denv->evalue to+env))
         (env (evalue+denv->denv to+env))
         ((okf bound+env)
          (init-for-loop stmt.name stmt.type from to env))
         (bound (int+denv->int bound+env))
         (env (int+denv->denv bound+env)))
      (exec-for-loop-iterations stmt.name
                                bound stmt.body env (1- limit)))
    :if (exec-if stmt.branches stmt.else env (1- limit))
    :console
    (console-case
        stmt.get :assert
        (b* (((okf test+env)
              (exec-expression stmt.get.arg env (1- limit)))
             (test (evalue+denv->evalue test+env))
             (env (evalue+denv->denv test+env))
             ((okf test) (ensure-boolean test env)))
          (if test (make-value?+denv :value? nil :denv env)
            (reserrf (list :assert-fail stmt.get.arg))))
        :error
        (b* (((okf vals+env)
              (exec-expression-list stmt.get.exprs env (1- limit)))
             (vals (values+denv->values vals+env))
             (env (values+denv->denv vals+env))
             (msg (make-screen-message-error :string stmt.get.string
                                             :values vals))
             (env (exec-print msg env)))
          (make-value?+denv :value? nil
                            :denv env))
        :log
        (b* (((okf vals+env)
              (exec-expression-list stmt.get.exprs env (1- limit)))
             (vals (values+denv->values vals+env))
             (env (values+denv->denv vals+env))
             (msg (make-screen-message-log :string stmt.get.string
                                           :values vals))
             (env (exec-print msg env)))
          (make-value?+denv :value? nil
                            :denv env)))
    :finalize
    (reserrf :execution-of-finalize-statement-not-yet-implemented)
    :increment
    (reserrf :execution-of-increment-statement-not-yet-implemented)
    :decrement
    (reserrf :execution-of-decrement-statement-not-yet-implemented)
    :block (exec-block stmt.get env (1- limit))))))

Function: exec-statement-list

(defun exec-statement-list (stmts env limit)
  (declare (xargs :guard (and (statement-listp stmts)
                              (denvp env)
                              (natp limit))))
  (let ((__function__ 'exec-statement-list))
    (declare (ignorable __function__))
    (b* (((when (zp limit)) (reserrf :limit))
         ((when (endp stmts))
          (make-value?+denv :value? nil
                            :denv (denv-fix env)))
         ((okf val?+env)
          (exec-statement (car stmts)
                          env (1- limit)))
         (val? (value?+denv->value? val?+env))
         (env (value?+denv->denv val?+env))
         ((when val?)
          (make-value?+denv :value? val?
                            :denv env)))
      (exec-statement-list (cdr stmts)
                           env (1- limit)))))

Function: exec-block

(defun exec-block (stmts env limit)
  (declare (xargs :guard (and (statement-listp stmts)
                              (denvp env)
                              (natp limit))))
  (let ((__function__ 'exec-block))
    (declare (ignorable __function__))
    (b* (((when (zp limit)) (reserrf :limit))
         ((okf env) (push-vcscope-dinfo nil env))
         ((okf val?+env)
          (exec-statement-list stmts env (1- limit)))
         (val? (value?+denv->value? val?+env))
         (env (value?+denv->denv val?+env))
         ((when val?)
          (make-value?+denv :value? val?
                            :denv env))
         ((okf env) (pop-vcscope-dinfo env)))
      (make-value?+denv :value? nil
                        :denv env))))

Function: exec-for-loop-iterations

(defun exec-for-loop-iterations (name bound body env limit)
  (declare (xargs :guard (and (identifierp name)
                              (integerp bound)
                              (statement-listp body)
                              (denvp env)
                              (natp limit))))
  (let ((__function__ 'exec-for-loop-iterations))
    (declare (ignorable __function__))
    (b* (((when (zp limit)) (reserrf :limit))
         ((when (end-of-for-loop-p name bound env))
          (b* (((okf env) (pop-vcscope-dinfo env)))
            (make-value?+denv :value? nil
                              :denv env)))
         ((okf val?+env)
          (exec-block body env (1- limit)))
         (val? (value?+denv->value? val?+env))
         (env (value?+denv->denv val?+env))
         ((when val?)
          (make-value?+denv :value? val?
                            :denv env))
         ((okf env) (step-for-loop name env)))
      (exec-for-loop-iterations name bound body env (1- limit)))))

Function: exec-if

(defun exec-if (branches else env limit)
  (declare (xargs :guard (and (branch-listp branches)
                              (statement-listp else)
                              (denvp env)
                              (natp limit))))
  (let ((__function__ 'exec-if))
    (declare (ignorable __function__))
    (b* (((when (zp limit)) (reserrf :limit))
         ((when (endp branches))
          (exec-block else env (1- limit)))
         ((branch branch) (car branches))
         ((okf test+env)
          (exec-expression branch.test env (1- limit)))
         (test (evalue+denv->evalue test+env))
         (env (evalue+denv->denv test+env))
         ((okf test) (ensure-boolean test env))
         ((when test)
          (exec-block branch.body env (1- limit))))
      (exec-if (cdr branches)
               else env (1- limit)))))

Theorem: return-type-of-exec-expression.evalue+denv

(defthm return-type-of-exec-expression.evalue+denv
  (b* ((?evalue+denv (exec-expression expr env limit)))
    (evalue+denv-resultp evalue+denv))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-expression-list.values+denv

(defthm return-type-of-exec-expression-list.values+denv
  (b* ((?values+denv (exec-expression-list exprs env limit)))
    (values+denv-resultp values+denv))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-struct-init.nameval+env

(defthm return-type-of-exec-struct-init.nameval+env
  (b* ((?nameval+env (exec-struct-init init env limit)))
    (namevalue+denv-resultp nameval+env))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-struct-init-list.valmap+env

(defthm return-type-of-exec-struct-init-list.valmap+env
  (b* ((?valmap+env (exec-struct-init-list inits env limit)))
    (valuemap+denv-resultp valmap+env))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-function.evalue+denv

(defthm return-type-of-exec-function.evalue+denv
  (b* ((?evalue+denv (exec-function fun args env limit)))
    (evalue+denv-resultp evalue+denv))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-statement.value?+denv

(defthm return-type-of-exec-statement.value?+denv
  (b* ((?value?+denv (exec-statement stmt env limit)))
    (value?+denv-resultp value?+denv))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-statement-list.value?+denv

(defthm return-type-of-exec-statement-list.value?+denv
  (b* ((?value?+denv (exec-statement-list stmts env limit)))
    (value?+denv-resultp value?+denv))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-block.val?+denv

(defthm return-type-of-exec-block.val?+denv
  (b* ((?val?+denv (exec-block stmts env limit)))
    (value?+denv-resultp val?+denv))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-for-loop-iterations.value?+denv

(defthm return-type-of-exec-for-loop-iterations.value?+denv
  (b* ((?value?+denv
            (exec-for-loop-iterations name bound body env limit)))
    (value?+denv-resultp value?+denv))
  :rule-classes :rewrite)

Theorem: return-type-of-exec-if.value?+denv

(defthm return-type-of-exec-if.value?+denv
  (b* ((?value?+denv (exec-if branches else env limit)))
    (value?+denv-resultp value?+denv))
  :rule-classes :rewrite)

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

(defthm exec-expression-of-expression-fix-expr
  (equal (exec-expression (expression-fix expr)
                          env limit)
         (exec-expression expr env limit)))

Theorem: exec-expression-of-denv-fix-env

(defthm exec-expression-of-denv-fix-env
  (equal (exec-expression expr (denv-fix env)
                          limit)
         (exec-expression expr env limit)))

Theorem: exec-expression-of-nfix-limit

(defthm exec-expression-of-nfix-limit
  (equal (exec-expression expr env (nfix limit))
         (exec-expression expr env 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)
                               env limit)
         (exec-expression-list exprs env limit)))

Theorem: exec-expression-list-of-denv-fix-env

(defthm exec-expression-list-of-denv-fix-env
  (equal (exec-expression-list exprs (denv-fix env)
                               limit)
         (exec-expression-list exprs env limit)))

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

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

Theorem: exec-struct-init-of-struct-init-fix-init

(defthm exec-struct-init-of-struct-init-fix-init
  (equal (exec-struct-init (struct-init-fix init)
                           env limit)
         (exec-struct-init init env limit)))

Theorem: exec-struct-init-of-denv-fix-env

(defthm exec-struct-init-of-denv-fix-env
  (equal (exec-struct-init init (denv-fix env)
                           limit)
         (exec-struct-init init env limit)))

Theorem: exec-struct-init-of-nfix-limit

(defthm exec-struct-init-of-nfix-limit
  (equal (exec-struct-init init env (nfix limit))
         (exec-struct-init init env limit)))

Theorem: exec-struct-init-list-of-struct-init-list-fix-inits

(defthm exec-struct-init-list-of-struct-init-list-fix-inits
  (equal (exec-struct-init-list (struct-init-list-fix inits)
                                env limit)
         (exec-struct-init-list inits env limit)))

Theorem: exec-struct-init-list-of-denv-fix-env

(defthm exec-struct-init-list-of-denv-fix-env
  (equal (exec-struct-init-list inits (denv-fix env)
                                limit)
         (exec-struct-init-list inits env limit)))

Theorem: exec-struct-init-list-of-nfix-limit

(defthm exec-struct-init-list-of-nfix-limit
  (equal (exec-struct-init-list inits env (nfix limit))
         (exec-struct-init-list inits env limit)))

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

(defthm exec-function-of-identifier-fix-fun
  (equal (exec-function (identifier-fix fun)
                        args env limit)
         (exec-function fun args env 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)
                        env limit)
         (exec-function fun args env limit)))

Theorem: exec-function-of-denv-fix-env

(defthm exec-function-of-denv-fix-env
  (equal (exec-function fun args (denv-fix env)
                        limit)
         (exec-function fun args env limit)))

Theorem: exec-function-of-nfix-limit

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

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

(defthm exec-statement-of-statement-fix-stmt
  (equal (exec-statement (statement-fix stmt)
                         env limit)
         (exec-statement stmt env limit)))

Theorem: exec-statement-of-denv-fix-env

(defthm exec-statement-of-denv-fix-env
  (equal (exec-statement stmt (denv-fix env)
                         limit)
         (exec-statement stmt env limit)))

Theorem: exec-statement-of-nfix-limit

(defthm exec-statement-of-nfix-limit
  (equal (exec-statement stmt env (nfix limit))
         (exec-statement stmt env 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)
                              env limit)
         (exec-statement-list stmts env limit)))

Theorem: exec-statement-list-of-denv-fix-env

(defthm exec-statement-list-of-denv-fix-env
  (equal (exec-statement-list stmts (denv-fix env)
                              limit)
         (exec-statement-list stmts env limit)))

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

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

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

(defthm exec-block-of-statement-list-fix-stmts
  (equal (exec-block (statement-list-fix stmts)
                     env limit)
         (exec-block stmts env limit)))

Theorem: exec-block-of-denv-fix-env

(defthm exec-block-of-denv-fix-env
  (equal (exec-block stmts (denv-fix env) limit)
         (exec-block stmts env limit)))

Theorem: exec-block-of-nfix-limit

(defthm exec-block-of-nfix-limit
  (equal (exec-block stmts env (nfix limit))
         (exec-block stmts env limit)))

Theorem: exec-for-loop-iterations-of-identifier-fix-name

(defthm exec-for-loop-iterations-of-identifier-fix-name
  (equal (exec-for-loop-iterations (identifier-fix name)
                                   bound body env limit)
         (exec-for-loop-iterations name bound body env limit)))

Theorem: exec-for-loop-iterations-of-ifix-bound

(defthm exec-for-loop-iterations-of-ifix-bound
  (equal (exec-for-loop-iterations name (ifix bound)
                                   body env limit)
         (exec-for-loop-iterations name bound body env limit)))

Theorem: exec-for-loop-iterations-of-statement-list-fix-body

(defthm exec-for-loop-iterations-of-statement-list-fix-body
 (equal
      (exec-for-loop-iterations name bound (statement-list-fix body)
                                env limit)
      (exec-for-loop-iterations name bound body env limit)))

Theorem: exec-for-loop-iterations-of-denv-fix-env

(defthm exec-for-loop-iterations-of-denv-fix-env
  (equal (exec-for-loop-iterations name bound body (denv-fix env)
                                   limit)
         (exec-for-loop-iterations name bound body env limit)))

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

(defthm exec-for-loop-iterations-of-nfix-limit
  (equal (exec-for-loop-iterations name bound body env (nfix limit))
         (exec-for-loop-iterations name bound body env limit)))

Theorem: exec-if-of-branch-list-fix-branches

(defthm exec-if-of-branch-list-fix-branches
  (equal (exec-if (branch-list-fix branches)
                  else env limit)
         (exec-if branches else env limit)))

Theorem: exec-if-of-statement-list-fix-else

(defthm exec-if-of-statement-list-fix-else
  (equal (exec-if branches (statement-list-fix else)
                  env limit)
         (exec-if branches else env limit)))

Theorem: exec-if-of-denv-fix-env

(defthm exec-if-of-denv-fix-env
  (equal (exec-if branches else (denv-fix env)
                  limit)
         (exec-if branches else env limit)))

Theorem: exec-if-of-nfix-limit

(defthm exec-if-of-nfix-limit
  (equal (exec-if branches else env (nfix limit))
         (exec-if branches else env 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 env limit)
                  (exec-expression expr-equiv env limit)))
  :rule-classes :congruence)

Theorem: exec-expression-denv-equiv-congruence-on-env

(defthm exec-expression-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-expression expr env limit)
                  (exec-expression expr env-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 env limit)
                  (exec-expression expr env 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 env limit)
                  (exec-expression-list exprs-equiv env limit)))
  :rule-classes :congruence)

Theorem: exec-expression-list-denv-equiv-congruence-on-env

(defthm exec-expression-list-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-expression-list exprs env limit)
                  (exec-expression-list exprs env-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 env limit)
                  (exec-expression-list exprs env limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-struct-init-struct-init-equiv-congruence-on-init

(defthm exec-struct-init-struct-init-equiv-congruence-on-init
  (implies (struct-init-equiv init init-equiv)
           (equal (exec-struct-init init env limit)
                  (exec-struct-init init-equiv env limit)))
  :rule-classes :congruence)

Theorem: exec-struct-init-denv-equiv-congruence-on-env

(defthm exec-struct-init-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-struct-init init env limit)
                  (exec-struct-init init env-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-struct-init-nat-equiv-congruence-on-limit

(defthm exec-struct-init-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-struct-init init env limit)
                  (exec-struct-init init env limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-struct-init-list-struct-init-list-equiv-congruence-on-inits

(defthm
   exec-struct-init-list-struct-init-list-equiv-congruence-on-inits
  (implies (struct-init-list-equiv inits inits-equiv)
           (equal (exec-struct-init-list inits env limit)
                  (exec-struct-init-list inits-equiv env limit)))
  :rule-classes :congruence)

Theorem: exec-struct-init-list-denv-equiv-congruence-on-env

(defthm exec-struct-init-list-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-struct-init-list inits env limit)
                  (exec-struct-init-list inits env-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-struct-init-list-nat-equiv-congruence-on-limit

(defthm exec-struct-init-list-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-struct-init-list inits env limit)
                  (exec-struct-init-list inits env 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 env limit)
                  (exec-function fun-equiv args env 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 env limit)
                  (exec-function fun args-equiv env limit)))
  :rule-classes :congruence)

Theorem: exec-function-denv-equiv-congruence-on-env

(defthm exec-function-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-function fun args env limit)
                  (exec-function fun args env-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 env limit)
                  (exec-function fun args env 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 env limit)
                  (exec-statement stmt-equiv env limit)))
  :rule-classes :congruence)

Theorem: exec-statement-denv-equiv-congruence-on-env

(defthm exec-statement-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-statement stmt env limit)
                  (exec-statement stmt env-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 env limit)
                  (exec-statement stmt env 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 env limit)
                  (exec-statement-list stmts-equiv env limit)))
  :rule-classes :congruence)

Theorem: exec-statement-list-denv-equiv-congruence-on-env

(defthm exec-statement-list-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-statement-list stmts env limit)
                  (exec-statement-list stmts env-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 env limit)
                  (exec-statement-list stmts env limit-equiv)))
  :rule-classes :congruence)

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

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

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

(defthm exec-block-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-block stmts env limit)
                  (exec-block stmts env-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 stmts env limit)
                  (exec-block stmts env limit-equiv)))
  :rule-classes :congruence)

Theorem: exec-for-loop-iterations-identifier-equiv-congruence-on-name

(defthm exec-for-loop-iterations-identifier-equiv-congruence-on-name
 (implies
   (identifier-equiv name name-equiv)
   (equal
        (exec-for-loop-iterations name bound body env limit)
        (exec-for-loop-iterations name-equiv bound body env limit)))
 :rule-classes :congruence)

Theorem: exec-for-loop-iterations-int-equiv-congruence-on-bound

(defthm exec-for-loop-iterations-int-equiv-congruence-on-bound
 (implies
   (acl2::int-equiv bound bound-equiv)
   (equal
        (exec-for-loop-iterations name bound body env limit)
        (exec-for-loop-iterations name bound-equiv body env limit)))
 :rule-classes :congruence)

Theorem: exec-for-loop-iterations-statement-list-equiv-congruence-on-body

(defthm
   exec-for-loop-iterations-statement-list-equiv-congruence-on-body
 (implies
   (statement-list-equiv body body-equiv)
   (equal
        (exec-for-loop-iterations name bound body env limit)
        (exec-for-loop-iterations name bound body-equiv env limit)))
 :rule-classes :congruence)

Theorem: exec-for-loop-iterations-denv-equiv-congruence-on-env

(defthm exec-for-loop-iterations-denv-equiv-congruence-on-env
 (implies
   (denv-equiv env env-equiv)
   (equal
        (exec-for-loop-iterations name bound body env limit)
        (exec-for-loop-iterations name bound body env-equiv limit)))
 :rule-classes :congruence)

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

(defthm exec-for-loop-iterations-nat-equiv-congruence-on-limit
 (implies
   (acl2::nat-equiv limit limit-equiv)
   (equal
        (exec-for-loop-iterations name bound body env limit)
        (exec-for-loop-iterations name bound body env limit-equiv)))
 :rule-classes :congruence)

Theorem: exec-if-branch-list-equiv-congruence-on-branches

(defthm exec-if-branch-list-equiv-congruence-on-branches
  (implies (branch-list-equiv branches branches-equiv)
           (equal (exec-if branches else env limit)
                  (exec-if branches-equiv else env limit)))
  :rule-classes :congruence)

Theorem: exec-if-statement-list-equiv-congruence-on-else

(defthm exec-if-statement-list-equiv-congruence-on-else
  (implies (statement-list-equiv else else-equiv)
           (equal (exec-if branches else env limit)
                  (exec-if branches else-equiv env limit)))
  :rule-classes :congruence)

Theorem: exec-if-denv-equiv-congruence-on-env

(defthm exec-if-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (exec-if branches else env limit)
                  (exec-if branches else env-equiv limit)))
  :rule-classes :congruence)

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

(defthm exec-if-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-if branches else env limit)
                  (exec-if branches else env limit-equiv)))
  :rule-classes :congruence)

Subtopics

Exec-expression

Execute an expression.

Exec-statement

Execute a statement.

Exec-for-loop-iterations

Execute the iterations of a for loop.

Exec-if

Execute the constituents of a conditional statement.

Exec-function

Execute a function call.

Exec-statement-list

Execute a list of statements.

Exec-block

Execute a block.

Exec-struct-init-list

Execute a list of struct component initializers.

Exec-struct-init

Execute a struct component initializer.

Exec-expression-list

Execute a list of expressions.