• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Community
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
        • Syntax-for-tools
        • Atc
        • Language
          • Abstract-syntax
          • Integer-ranges
          • Implementation-environments
          • Dynamic-semantics
            • Exec
            • Exec-arrsub
            • Exec-expr-pure
            • Exec-expr-asg
            • Init-value-to-value
            • Exec-memberp
            • Apconvert-expr-value
            • Exec-address
            • Exec-member
            • Init-scope
            • Exec-unary
            • Exec-fun
            • Exec-block-item
            • Eval-iconst
            • Exec-binary-strict-pure
            • Exec-expr-pure-list
            • Eval-binary-strict-pure
            • Exec-block-item-list
            • Exec-indir
            • Exec-expr-call-or-pure
            • Exec-without-calls
            • Exec-stmt-while
            • Exec-stmt
            • Exec-ident
            • Eval-cast
            • Exec-cast
            • Eval-unary
            • Exec-const
            • Exec-initer
            • Exec-expr-call-or-asg
            • Eval-const
            • Exec-expr-call
          • Static-semantics
          • Grammar
          • Integer-formats
          • Types
          • Portable-ascii-identifiers
          • Values
          • Integer-operations
          • Computation-states
          • Object-designators
          • Operations
          • Errors
          • Tag-environments
          • Function-environments
          • Character-sets
          • Flexible-array-member-removal
          • Arithmetic-operations
          • Pointer-operations
          • Bytes
          • Keywords
          • Real-operations
          • Array-operations
          • Scalar-operations
          • Structure-operations
        • Representation
        • Transformation-tools
        • Insertion-sort
        • Pack
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Dynamic-semantics

Exec-without-calls

Execution not involving function calls is independent from the function environment.

We express this by saying that when the execution functions are applied to constructs (expressions, statements, etc.) that do not contain function calls, they always yield the same results given any two arbitrary function environments.

Definitions and Theorems

Theorem: exec-expr-call-without-calls

(defthm exec-expr-call-without-calls
  t
  :rule-classes nil)

Theorem: exec-expr-call-or-pure-without-calls

(defthm exec-expr-call-or-pure-without-calls
  (implies (expr-nocallsp e)
           (equal (exec-expr-call-or-pure e compst fenv limit)
                  (exec-expr-call-or-pure e compst fenv1 limit)))
  :rule-classes nil)

Theorem: exec-expr-asg-without-calls

(defthm exec-expr-asg-without-calls
  (implies (expr-nocallsp e)
           (equal (exec-expr-asg e compst fenv limit)
                  (exec-expr-asg e compst fenv1 limit)))
  :rule-classes nil)

Theorem: exec-expr-call-or-asg-without-calls

(defthm exec-expr-call-or-asg-without-calls
  (implies (expr-nocallsp e)
           (equal (exec-expr-call-or-asg e compst fenv limit)
                  (exec-expr-call-or-asg e compst fenv1 limit)))
  :rule-classes nil)

Theorem: exec-fun-without-calls

(defthm exec-fun-without-calls
  t
  :rule-classes nil)

Theorem: exec-stmt-without-calls

(defthm exec-stmt-without-calls
  (implies (stmt-nocallsp s)
           (equal (exec-stmt s compst fenv limit)
                  (exec-stmt s compst fenv1 limit)))
  :rule-classes nil)

Theorem: exec-stmt-while-without-calls

(defthm exec-stmt-while-without-calls
  (implies (and (expr-nocallsp test)
                (stmt-nocallsp body))
           (equal (exec-stmt-while test body compst fenv limit)
                  (exec-stmt-while test body compst fenv1 limit)))
  :rule-classes nil)

Theorem: exec-initer-without-calls

(defthm exec-initer-without-calls
  (implies (initer-nocallsp initer)
           (equal (exec-initer initer compst fenv limit)
                  (exec-initer initer compst fenv1 limit)))
  :rule-classes nil)

Theorem: exec-block-item-without-calls

(defthm exec-block-item-without-calls
  (implies (block-item-nocallsp item)
           (equal (exec-block-item item compst fenv limit)
                  (exec-block-item item compst fenv1 limit)))
  :rule-classes nil)

Theorem: exec-block-item-list-without-calls

(defthm exec-block-item-list-without-calls
  (implies (block-item-list-nocallsp items)
           (equal (exec-block-item-list items compst fenv limit)
                  (exec-block-item-list items compst fenv1 limit)))
  :rule-classes nil)