• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Soft
      • Bv
      • Imp-language
      • C
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
        • Transformations
        • Language
          • Abstract-syntax
          • Dynamic-semantics
            • Exec
            • Find-fun
            • Init-local
            • Mode
            • Write-vars-values
            • Add-vars-values
            • Add-funs
            • Eoutcome
            • Soutcome
            • Ensure-funscope-disjoint
            • Write-var-value
            • Restrict-vars
            • Add-var-value
            • Funinfo
            • Exec-top-block
            • Values
            • Cstate
            • Funinfo+funenv
            • Read-vars-values
            • Read-var-value
            • Funenv
            • Funscope-for-fundefs
            • Exec-path
            • Path-to-var
            • Funinfo+funenv-result
            • Exec-literal
            • Soutcome-result
            • Mode-set-result
            • Funscope-result
            • Funinfo-result
            • Funenv-result
            • Eoutcome-result
            • Cstate-result
            • Paths-to-vars
            • Funinfo-for-fundef
            • Literal-evaluation
            • Lstate
            • Funscope
            • Mode-set
          • Concrete-syntax
          • Static-soundness
          • Static-semantics
          • Errors
        • Yul-json
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Number-theory
      • Cryptography
      • Lists-light
      • Builtins
      • Axe
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Dynamic-semantics

Ensure-funscope-disjoint

Ensure that a function scope is disjoint from a function environment.

Signature

(ensure-funscope-disjoint funscope funenv) → _

Arguments

funscope — Guard (funscopep funscope).

funenv — Guard (funenvp funenv).

Returns

_ — Type (reserr-optionp _).

That is, ensure that the function names in the scope are disjoint from all the function names in the environment's scopes. This is used to ensure that there is no function shadowing: see add-funs.

Definitions and Theorems

Function: ensure-funscope-disjoint

(defun ensure-funscope-disjoint (funscope funenv)
 (declare (xargs :guard (and (funscopep funscope)
                             (funenvp funenv))))
 (let ((__function__ 'ensure-funscope-disjoint))
   (declare (ignorable __function__))
   (b*
     (((when (endp funenv)) nil)
      (overlap (intersect (omap::keys (funscope-fix funscope))
                          (omap::keys (funscope-fix (car funenv)))))
      ((unless (emptyp overlap))
       (reserrf (list :duplicate-functions overlap))))
     (ensure-funscope-disjoint funscope (cdr funenv)))))

Theorem: reserr-optionp-of-ensure-funscope-disjoint

(defthm reserr-optionp-of-ensure-funscope-disjoint
  (b* ((_ (ensure-funscope-disjoint funscope funenv)))
    (reserr-optionp _))
  :rule-classes :rewrite)

Theorem: ensure-funscope-disjoint-of-empty-funscope-not-error

(defthm ensure-funscope-disjoint-of-empty-funscope-not-error
  (not (reserrp (ensure-funscope-disjoint nil funenv))))

Theorem: error-info-wfp-of-ensure-funscope-disjoint

(defthm error-info-wfp-of-ensure-funscope-disjoint
  (b* ((?_ (ensure-funscope-disjoint funscope funenv)))
    (implies (reserrp _)
             (error-info-wfp _))))

Theorem: ensure-funscope-disjoint-of-funscope-fix-funscope

(defthm ensure-funscope-disjoint-of-funscope-fix-funscope
  (equal (ensure-funscope-disjoint (funscope-fix funscope)
                                   funenv)
         (ensure-funscope-disjoint funscope funenv)))

Theorem: ensure-funscope-disjoint-funscope-equiv-congruence-on-funscope

(defthm
     ensure-funscope-disjoint-funscope-equiv-congruence-on-funscope
  (implies (funscope-equiv funscope funscope-equiv)
           (equal (ensure-funscope-disjoint funscope funenv)
                  (ensure-funscope-disjoint funscope-equiv funenv)))
  :rule-classes :congruence)

Theorem: ensure-funscope-disjoint-of-funenv-fix-funenv

(defthm ensure-funscope-disjoint-of-funenv-fix-funenv
  (equal (ensure-funscope-disjoint funscope (funenv-fix funenv))
         (ensure-funscope-disjoint funscope funenv)))

Theorem: ensure-funscope-disjoint-funenv-equiv-congruence-on-funenv

(defthm ensure-funscope-disjoint-funenv-equiv-congruence-on-funenv
  (implies (funenv-equiv funenv funenv-equiv)
           (equal (ensure-funscope-disjoint funscope funenv)
                  (ensure-funscope-disjoint funscope funenv-equiv)))
  :rule-classes :congruence)