• 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
        • Syntax-for-tools
        • Atc
          • Atc-implementation
            • Atc-abstract-syntax
            • Atc-pretty-printer
            • Atc-event-and-code-generation
              • Atc-symbolic-computation-states
              • Atc-symbolic-execution-rules
              • Atc-gen-ext-declon-lists
              • Atc-function-and-loop-generation
              • Atc-statement-generation
              • Atc-gen-fileset
              • Atc-gen-everything
              • Atc-gen-obj-declon
              • Atc-gen-fileset-event
              • Atc-tag-tables
              • Atc-expression-generation
              • Atc-generation-contexts
              • Atc-gen-wf-thm
              • Term-checkers-atc
              • Atc-variable-tables
                • Atc-var-info-list->type-list
                • Atc-var-info-list->thm-list
                • Atc-check-var
                • Atc-var-info
                • Atc-var-info-option
                • Atc-get-vars-check-innermost
                • Atc-get-var-check-innermost
                • Atc-add-var
                • Atc-get-var
                • Atc-symbol-varinfo-alist
                • Atc-symbol-varinfo-alist-list-to-thms
                • Atc-symbol-varinfo-alist-list
                • Atc-get-vars
                • Atc-symbol-varinfo-alist-to-thms
                • Atc-var-info-option-list
                • Atc-var-info-list
              • Term-checkers-common
              • Atc-gen-init-fun-env-thm
              • Atc-gen-appconds
              • Read-write-variables
              • Atc-gen-thm-assert-events
              • Test*
              • Atc-gen-prog-const
              • Atc-gen-expr-bool
              • Atc-theorem-generation
              • Atc-tag-generation
              • Atc-gen-expr-pure
              • Atc-function-tables
              • Atc-object-tables
            • Fty-pseudo-term-utilities
            • Atc-term-recognizers
            • Atc-input-processing
            • Atc-shallow-embedding
            • Atc-process-inputs-and-gen-everything
            • Atc-table
            • Atc-fn
            • Atc-pretty-printing-options
            • Atc-types
            • Atc-macro-definition
          • Atc-tutorial
        • Language
        • Representation
        • Transformation-tools
        • Pack
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • 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

• Atc-variable-tables

Atc-get-vars-check-innermost

Lift atc-get-var-check-innermost to lists.

Signature

(atc-get-vars-check-innermost vars inscope) 
  → 
(mv info?-list innermostp-list)

Arguments

vars — Guard (symbol-listp vars).

inscope — Guard (atc-symbol-varinfo-alist-listp inscope).

Returns

info?-list — Type (atc-var-info-option-listp info?-list).

innermostp-list — Type (boolean-listp innermostp-list).

This is used when we encounter an mv-let in code generation. We need to ensure that all the variables are in scope, and we need to know which ones are in the innermost scope. This function returns that information.

Definitions and Theorems

Function: atc-get-vars-check-innermost

(defun atc-get-vars-check-innermost (vars inscope)
 (declare
      (xargs :guard (and (symbol-listp vars)
                         (atc-symbol-varinfo-alist-listp inscope))))
 (let ((__function__ 'atc-get-vars-check-innermost))
   (declare (ignorable __function__))
   (b* (((when (endp vars)) (mv nil nil))
        ((mv info? innermostp)
         (atc-get-var-check-innermost (car vars)
                                      inscope))
        ((mv info?-list innermostp-list)
         (atc-get-vars-check-innermost (cdr vars)
                                       inscope)))
     (mv (cons info? info?-list)
         (cons innermostp innermostp-list)))))

Theorem: atc-var-info-option-listp-of-atc-get-vars-check-innermost.info?-list

(defthm
 atc-var-info-option-listp-of-atc-get-vars-check-innermost.info?-list
 (b* (((mv ?info?-list ?innermostp-list)
       (atc-get-vars-check-innermost vars inscope)))
   (atc-var-info-option-listp info?-list))
 :rule-classes :rewrite)

Theorem: boolean-listp-of-atc-get-vars-check-innermost.innermostp-list

(defthm
      boolean-listp-of-atc-get-vars-check-innermost.innermostp-list
  (b* (((mv ?info?-list ?innermostp-list)
        (atc-get-vars-check-innermost vars inscope)))
    (boolean-listp innermostp-list))
  :rule-classes :rewrite)

Theorem: len-of-atc-get-vars-check-innermost.info?-list

(defthm len-of-atc-get-vars-check-innermost.info?-list
  (b* (((mv ?info?-list ?innermostp-list)
        (atc-get-vars-check-innermost vars inscope)))
    (equal (len info?-list) (len vars))))

Theorem: len-of-atc-get-vars-check-innermost.innermostp-list

(defthm len-of-atc-get-vars-check-innermost.innermostp-list
  (b* (((mv ?info?-list ?innermostp-list)
        (atc-get-vars-check-innermost vars inscope)))
    (equal (len innermostp-list)
           (len vars))))