• 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
        • Soft
        • 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
            • Insertion-sort
            • Pack
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Riscv
          • 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
    • 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))))