• 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-arrsub
            • Variable-resolution-preservation
              • Var-resolve-preservep-of-exec
              • Prev-scope/frame
              • Var-resolve-of-exec
              • Var-resolve-preservep
              • Var-resolve-preservep-of-exit-scope-when-enter-scope
              • Var-resolve-preservep-of-prev-of-exit-scope-when-enter-scope
              • Var-resolve-preservep-of-pop-frame-when-push-frame
              • Var-resolve-preservep-of-exit-scope-and-exit-scope
              • Var-resolve-preservep-of-prev-scope/frame-and-prev-scope/frame
              • Var-resolve-preservep-of-prev-scope/frame-of-create-var
              • Var-resolve-preservep-of-prev-scope/frame-and-create-var
              • Var-resolve-preservep-of-trans-exit-scope-when-enter-scope
              • Var-resolve-preservep-of-write-object
            • 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-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-expr-list
            • Exec-obj-declon
            • Exec-cast
            • Exec-const
            • Eval-unary
            • Exec-stmt-dowhile
            • Exec-initer
            • 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

• Variable-resolution-preservation

Var-resolve-preservep

Check if all the variable names visible in a computation state are also visible in another computation state and they resolve to the same variables, for any number of peeled frames and scopes.

This expresses the property that we want to prove by induction.

Definitions and Theorems

Theorem: var-resolve-preservep-necc

(defthm var-resolve-preservep-necc
 (implies
  (var-resolve-preservep compst compst1)
  (implies
      (and (identp var) (natp n) (natp m))
      (b* ((peeled-compst (peel-scopes m (peel-frames n compst)))
           (peeled-compst1 (peel-scopes m (peel-frames n compst1))))
        (implies (objdesign-of-var var peeled-compst)
                 (equal (objdesign-of-var var peeled-compst1)
                        (objdesign-of-var var peeled-compst)))))))

Theorem: booleanp-of-var-resolve-preservep

(defthm booleanp-of-var-resolve-preservep
  (b* ((yes/no (var-resolve-preservep compst compst1)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: var-resolve-preservep-of-compustate-fix-compst

(defthm var-resolve-preservep-of-compustate-fix-compst
  (equal (var-resolve-preservep (compustate-fix compst)
                                compst1)
         (var-resolve-preservep compst compst1)))

Theorem: var-resolve-preservep-compustate-equiv-congruence-on-compst

(defthm var-resolve-preservep-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (var-resolve-preservep compst compst1)
                  (var-resolve-preservep compst-equiv compst1)))
  :rule-classes :congruence)

Theorem: var-resolve-preservep-of-compustate-fix-compst1

(defthm var-resolve-preservep-of-compustate-fix-compst1
  (equal (var-resolve-preservep compst (compustate-fix compst1))
         (var-resolve-preservep compst compst1)))

Theorem: var-resolve-preservep-compustate-equiv-congruence-on-compst1

(defthm var-resolve-preservep-compustate-equiv-congruence-on-compst1
  (implies (compustate-equiv compst1 compst1-equiv)
           (equal (var-resolve-preservep compst compst1)
                  (var-resolve-preservep compst compst1-equiv)))
  :rule-classes :congruence)

Theorem: var-resolve-preservep-reflexive

(defthm var-resolve-preservep-reflexive
  (var-resolve-preservep compst compst))

Theorem: var-resolve-preservep-transitive

(defthm var-resolve-preservep-transitive
  (implies (and (var-resolve-preservep compst compst1)
                (var-resolve-preservep compst1 compst2))
           (var-resolve-preservep compst compst2)))