• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
      • X86isa
        • Program-execution
        • Sdm-instruction-set-summary
        • Tlb
        • Running-linux
        • Introduction
        • Asmtest
        • X86isa-build-instructions
        • Publications
        • Contributors
        • Machine
          • X86isa-state
          • Syscalls
          • Cpuid
          • Linear-memory
            • Reasoning-about-memory-reads-and-writes
              • Las-to-pas
                • Rb
                • Create-canonical-address-list
                • Rb-1
                • Read-from-physical-memory
                • Write-to-physical-memory
                • Wb
                • Wb-1
                • Canonical-address-listp
              • Wml256
              • Rml256
              • Wml512
              • Rml512
              • Rml128
              • Rml80
              • Program-location
              • Rml64
              • Wml128
              • Rml48
              • Rml32
              • Rml08
              • Rml16
              • Wml80
              • Wml64
              • Wml08
              • Byte-listp
              • Wml48
              • Parametric-memory-reads-and-writes
              • Combine-n-bytes
              • Wml32
              • Program-at
              • Wml16
              • Combine-bytes
              • Write-canonical-address-to-memory-user-exec
              • Write-canonical-address-to-memory
              • Riml64
              • Wml-size
              • Rml-size
              • Riml32
              • Riml16
              • Riml08
              • Wiml64
              • Wiml32
              • Wiml16
              • Wiml08
              • Wiml-size
              • Generate-xr-over-write-thms
              • Generate-write-fn-over-xw-thms
              • Generate-read-fn-over-xw-thms
              • Riml-size
            • Rflag-specifications
            • Characterizing-undefined-behavior
            • Top-level-memory
            • App-view
            • X86-decoder
            • Physical-memory
            • Decoding-and-spec-utils
            • Instructions
            • Register-readers-and-writers
            • X86-modes
            • Segmentation
            • Other-non-deterministic-computations
            • Environment
            • Paging
          • Implemented-opcodes
          • To-do
          • Proof-utilities
          • Peripherals
          • Model-validation
          • Modelcalls
          • Concrete-simulation-examples
          • Utils
          • Debugging-code-proofs
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Reasoning-about-memory-reads-and-writes

    Las-to-pas

    Signature
    (las-to-pas n lin-addr r-w-x x86) → (mv flg p-addrs x86)
    Arguments
    n — Number of bytes to be read.
        Guard (natp n).
    lin-addr — First linear address.
        Guard (integerp lin-addr).
    r-w-x — Type of memory access: read, write, or execute.
    Returns
    p-addrs — Type (true-listp p-addrs).
    x86 — Type (x86p x86), given (x86p x86).

    Definitions and Theorems

    Function: las-to-pas

    (defun las-to-pas (n lin-addr r-w-x x86)
      (declare (xargs :stobjs (x86)))
      (declare (type (member :r :w :x) r-w-x))
      (declare (xargs :guard (and (natp n) (integerp lin-addr))))
      (declare (xargs :guard (not (app-view x86))))
      (let ((__function__ 'las-to-pas))
        (declare (ignorable __function__))
        (if (zp n)
            (mv nil nil x86)
          (b* (((unless (canonical-address-p lin-addr))
                (mv t nil x86))
               ((mv flg p-addr x86)
                (ia32e-la-to-pa lin-addr r-w-x x86))
               ((when flg) (mv flg nil x86))
               ((mv flg p-addrs x86)
                (las-to-pas (1- n)
                            (1+ lin-addr)
                            r-w-x x86)))
            (mv flg (if flg nil (cons p-addr p-addrs))
                x86)))))

    Theorem: true-listp-of-las-to-pas.p-addrs

    (defthm true-listp-of-las-to-pas.p-addrs
      (b* (((mv ?flg ?p-addrs ?x86)
            (las-to-pas n lin-addr r-w-x x86)))
        (true-listp p-addrs))
      :rule-classes (:rewrite :type-prescription))

    Theorem: x86p-of-las-to-pas.x86

    (defthm x86p-of-las-to-pas.x86
      (implies (x86p x86)
               (b* (((mv ?flg ?p-addrs ?x86)
                     (las-to-pas n lin-addr r-w-x x86)))
                 (x86p x86)))
      :rule-classes :rewrite)

    Theorem: consp-mv-nth-1-las-to-pas

    (defthm consp-mv-nth-1-las-to-pas
      (implies (and (not (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
                    (not (zp n)))
               (consp (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))
      :rule-classes (:rewrite :type-prescription))

    Theorem: car-mv-nth-1-las-to-pas

    (defthm car-mv-nth-1-las-to-pas
      (implies (and (not (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
                    (not (zp n)))
               (equal (car (mv-nth 1 (las-to-pas n lin-addr r-w-x x86)))
                      (mv-nth 1
                              (ia32e-la-to-pa lin-addr r-w-x x86)))))

    Theorem: physical-address-listp-mv-nth-1-las-to-pas

    (defthm physical-address-listp-mv-nth-1-las-to-pas
      (physical-address-listp
           (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))

    Theorem: las-to-pas-n=0

    (defthm las-to-pas-n=0
      (and (equal (mv-nth 0 (las-to-pas 0 lin-addr r-w-x x86))
                  nil)
           (equal (mv-nth 1 (las-to-pas 0 lin-addr r-w-x x86))
                  nil)
           (equal (mv-nth 2 (las-to-pas 0 lin-addr r-w-x x86))
                  x86)))

    Theorem: xr-las-to-pas

    (defthm xr-las-to-pas
      (implies (and (not (equal fld :tlb))
                    (not (equal fld :mem))
                    (not (equal fld :fault)))
               (equal (xr fld index
                          (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
                      (xr fld index x86))))

    Theorem: xr-rflags-las-to-pas

    (defthm xr-rflags-las-to-pas
     (implies
       (not (mv-nth 0
                    (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
       (equal (xr :rflags nil
                  (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
              (xr :rflags nil (double-rewrite x86)))))

    Theorem: xr-fault-las-to-pas

    (defthm xr-fault-las-to-pas
     (implies
       (not (mv-nth 0
                    (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
       (equal (xr :fault nil
                  (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
              (xr :fault nil (double-rewrite x86)))))

    Theorem: las-to-pas-xw-values

    (defthm las-to-pas-xw-values
     (implies
      (and (not (equal fld :mem))
           (not (equal fld :rflags))
           (not (equal fld :fault))
           (not (equal fld :ctr))
           (not (equal fld :msr))
           (not (equal fld :app-view))
           (not (equal fld :marking-view))
           (not (equal fld :seg-visible))
           (not (equal fld :tlb))
           (not (equal fld :implicit-supervisor-access)))
      (and
        (equal
             (mv-nth 0
                     (las-to-pas n
                                 lin-addr r-w-x (xw fld index val x86)))
             (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
        (equal
             (mv-nth 1
                     (las-to-pas n
                                 lin-addr r-w-x (xw fld index val x86)))
             (mv-nth 1 (las-to-pas n lin-addr r-w-x x86))))))

    Theorem: 64-bit-modep-of-las-to-pas

    (defthm 64-bit-modep-of-las-to-pas
      (equal (64-bit-modep (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
             (64-bit-modep x86)))

    Theorem: x86-operation-mode-of-las-to-pas

    (defthm x86-operation-mode-of-las-to-pas
     (equal
       (x86-operation-mode (mv-nth 2 (las-to-pas n lin-addr r-w-x x86)))
       (x86-operation-mode x86)))

    Theorem: las-to-pas-xw-state

    (defthm las-to-pas-xw-state
     (implies
      (and (not (equal fld :mem))
           (not (equal fld :rflags))
           (not (equal fld :fault))
           (not (equal fld :ctr))
           (not (equal fld :msr))
           (not (equal fld :app-view))
           (not (equal fld :marking-view))
           (not (equal fld :seg-visible))
           (not (equal fld :tlb))
           (not (equal fld :implicit-supervisor-access)))
      (equal (mv-nth 2
                     (las-to-pas n
                                 lin-addr r-w-x (xw fld index val x86)))
             (xw fld index val
                 (mv-nth 2 (las-to-pas n lin-addr r-w-x x86))))))

    Theorem: las-to-pas-xw-rflags-not-ac

    (defthm las-to-pas-xw-rflags-not-ac
     (implies
      (equal (rflagsbits->ac value)
             (rflagsbits->ac (rflags (double-rewrite x86))))
      (and
       (equal
            (mv-nth 0
                    (las-to-pas n lin-addr
                                r-w-x (xw :rflags nil value x86)))
            (mv-nth 0
                    (las-to-pas n lin-addr r-w-x (double-rewrite x86))))
       (equal (mv-nth 1
                      (las-to-pas n lin-addr
                                  r-w-x (xw :rflags nil value x86)))
              (mv-nth 1
                      (las-to-pas n lin-addr
                                  r-w-x (double-rewrite x86)))))))

    Theorem: las-to-pas-xw-rflags-state-not-ac

    (defthm las-to-pas-xw-rflags-state-not-ac
      (implies
           (equal (rflagsbits->ac value)
                  (rflagsbits->ac (rflags x86)))
           (equal (mv-nth 2
                          (las-to-pas n lin-addr
                                      r-w-x (xw :rflags nil value x86)))
                  (xw :rflags nil value
                      (mv-nth 2 (las-to-pas n lin-addr r-w-x x86))))))

    Theorem: len-of-mv-nth-1-las-to-pas

    (defthm len-of-mv-nth-1-las-to-pas
      (implies (not (mv-nth 0 (las-to-pas n lin-addr r-w-x x86)))
               (equal (len (mv-nth 1 (las-to-pas n lin-addr r-w-x x86)))
                      (nfix n))))