• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Tlb
      • Booting-linux
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • Proof-utilities
        • System-level-marking-view-proof-utilities
          • Rb-alt
          • Unwind-x86-interpreter-in-marking-view
          • Program-at-alt
          • Get-prefixes-alt
          • Get-prefixes-in-system-level-marking-view
          • Rb-in-system-level-marking-view
          • Xlate-equiv-memory-and-rml08
          • Reasoning-about-page-tables
            • Create-qword-address-list
            • Mult-8-qword-paddr-listp
            • Gather-paging-structures
            • Qword-paddr-listp
            • Find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux
            • Find-first-arg-of-disjoint-p$-candidates
            • Paging-basics
          • Las-to-pas-two-n-ind-hint
          • Find-l-addrs-from-disjoint-p-of-las-to-pas-1-aux
          • Replace-element
          • Phys-mem-values-same
        • Non-marking-view-proof-utilities
        • App-view-proof-utilities
        • Subset-p
        • Disjoint-p
        • Pos
        • Member-p
        • No-duplicates-p
        • Common-system-level-utils
        • Debugging-code-proofs
        • General-memory-utils
        • X86-row-wow-thms
      • To-do
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Reasoning-about-page-tables

Find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux

Signature

(find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux 
     vars-1 vars-2 calls) 
 
  → 
*

Arguments

vars-1 — Guard (true-listp vars-1).

vars-2 — Guard (true-listp vars-2).

Definitions and Theorems

Function: find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux

(defun find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux
       (vars-1 vars-2 calls)
  (declare (xargs :guard (and (true-listp vars-1)
                              (true-listp vars-2))))
  (declare (xargs :guard (and (equal (len vars-1) (len vars-2))
                              (equal (len vars-1) 2))))
  (let ((__function__
             'find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux))
    (declare (ignorable __function__))
    (if (atom calls)
        nil
      (b* ((one-call (car calls))
           ((unless (and (true-listp one-call)
                         (equal 3 (len one-call))))
            nil)
           (mv-nth-term-1 (nth 1 one-call))
           (mv-nth-term-2 (nth 2 one-call))
           ((unless (and (true-listp mv-nth-term-1)
                         (equal 3 (len mv-nth-term-1))
                         (true-listp mv-nth-term-2)
                         (equal 3 (len mv-nth-term-2))))
            nil)
           (term-1 (nth 2 mv-nth-term-1))
           (term-2 (nth 2 mv-nth-term-2))
           ((unless (and (true-listp term-1)
                         (equal 5 (len term-1))
                         (true-listp term-2)
                         (equal 5 (len term-2))))
            nil)
           ((list n-var-1 addr-var-1) vars-1)
           ((list n-var-2 addr-var-2) vars-2))
        (cons (list (cons n-var-1 (nth 1 term-1))
                    (cons addr-var-1 (nth 2 term-1))
                    (cons n-var-2 (nth 1 term-2))
                    (cons addr-var-2 (nth 2 term-2)))
              (find-l-addrs-from-disjoint-p$-of-two-las-to-pas-aux
                   vars-1 vars-2 (cdr calls)))))))