• 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

Prev-scope/frame

Go to the previous scope or frame.

Signature

(prev-scope/frame compst) → compst1

Arguments

compst — Guard (compustatep compst).

Returns

compst1 — Type (compustatep compst1).

That is, exit a scope if the top frame has more than one, otherwise pop a frame.

This function is used to express the exception, noted in variable-resolution-preservation, for the execution of object declarations, block items, and lists of block items. Those block items always execute in a frame (which justifies the guard of this function), but that frame may have one or more scopes, with the object declarations or block items executing in the top scope; thus, in order to always exclude the scope in which the object declarations or block items are executing, we need to pop frame if that is the only scope. Note that just using exit-scope, or just using peel-scopes with argument 1, would not work, and so we need to introduce this function here.

Definitions and Theorems

Function: prev-scope/frame

(defun prev-scope/frame (compst)
  (declare (xargs :guard (compustatep compst)))
  (declare (xargs :guard (> (compustate-frames-number compst)
                            0)))
  (if (> (compustate-top-frame-scopes-number compst)
         1)
      (exit-scope compst)
    (pop-frame compst)))

Theorem: compustatep-of-prev-scope/frame

(defthm compustatep-of-prev-scope/frame
  (b* ((compst1 (prev-scope/frame compst)))
    (compustatep compst1))
  :rule-classes :rewrite)

Theorem: prev-scope/frame-of-compustate-fix-compst

(defthm prev-scope/frame-of-compustate-fix-compst
  (equal (prev-scope/frame (compustate-fix compst))
         (prev-scope/frame compst)))

Theorem: prev-scope/frame-compustate-equiv-congruence-on-compst

(defthm prev-scope/frame-compustate-equiv-congruence-on-compst
  (implies (compustate-equiv compst compst-equiv)
           (equal (prev-scope/frame compst)
                  (prev-scope/frame compst-equiv)))
  :rule-classes :congruence)