• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • 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
      • Implemented-opcodes
      • To-do
      • Proof-utilities
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
        • 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
          • 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
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• System-level-marking-view-proof-utilities

Program-at-alt

Signature

(program-at-alt prog-addr bytes x86) → *

Arguments

prog-addr — Guard (canonical-address-p prog-addr).

bytes — Guard (byte-listp bytes).

Definitions and Theorems

Function: program-at-alt

(defun program-at-alt (prog-addr bytes x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (and (canonical-address-p prog-addr)
                             (byte-listp bytes))))
 (declare (xargs :non-executable t))
 (prog2$
  (acl2::throw-nonexec-error 'program-at-alt
                             (list prog-addr bytes x86))
  (let ((__function__ 'program-at-alt))
   (declare (ignorable __function__))
   (if
    (and
      (marking-view x86)
      (64-bit-modep x86)
      (not (app-view x86))
      (canonical-address-p prog-addr)
      (canonical-address-p (+ -1 (len bytes) prog-addr))
      (disjoint-p$
           (mv-nth 1
                   (las-to-pas (len bytes)
                               prog-addr
                               :x x86))
           (open-qword-paddr-list
                (gather-all-paging-structure-qword-addresses x86))))
    (program-at prog-addr bytes x86)
    nil))))

Theorem: program-at-alt-implies-program-addresses-properties

(defthm program-at-alt-implies-program-addresses-properties
 (implies
  (program-at-alt prog-addr bytes (double-rewrite x86))
  (and (marking-view x86)
       (not (app-view x86))
       (canonical-address-p prog-addr)
       (canonical-address-p (+ -1 (len bytes) prog-addr))
       (disjoint-p$
            (mv-nth 1
                    (las-to-pas (len bytes)
                                prog-addr
                                :x x86))
            (open-qword-paddr-list
                 (gather-all-paging-structure-qword-addresses x86)))
       (program-at prog-addr bytes x86))))

Theorem: rewrite-program-at-to-program-at-alt

(defthm rewrite-program-at-to-program-at-alt
 (implies
  (forced-and
    (disjoint-p$ (mv-nth 1
                         (las-to-pas (len bytes)
                                     prog-addr
                                     :x (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
    (canonical-address-p prog-addr)
    (canonical-address-p (+ -1 (len bytes) prog-addr))
    (marking-view x86)
    (not (app-view x86))
    (64-bit-modep (double-rewrite x86)))
  (equal (program-at prog-addr bytes x86)
         (program-at-alt prog-addr bytes (double-rewrite x86)))))

Theorem: program-at-alt-and-paging-equiv-memory

(defthm program-at-alt-and-paging-equiv-memory
  (implies (and (paging-equiv-memory x86-1 x86-2)
                (xlate-equiv-memory x86-1 x86-2))
           (equal (program-at-alt prog-addr bytes x86-1)
                  (program-at-alt prog-addr bytes x86-2))))

Theorem: program-at-alt-and-mv-nth-2-las-to-pas

(defthm program-at-alt-and-mv-nth-2-las-to-pas
 (implies
    (64-bit-modep x86)
    (equal (program-at-alt prog-addr bytes
                           (mv-nth 2 (las-to-pas n addr r-w-x x86)))
           (program-at-alt prog-addr bytes x86))))

Theorem: program-at-alt-wb-disjoint-in-sys-view

(defthm program-at-alt-wb-disjoint-in-sys-view
 (implies
  (and
    (disjoint-p$ (mv-nth 1
                         (las-to-pas n-w write-addr
                                     :w (double-rewrite x86)))
                 (mv-nth 1
                         (las-to-pas (len bytes)
                                     prog-addr
                                     :x (double-rewrite x86))))
    (disjoint-p$ (mv-nth 1
                         (las-to-pas n-w write-addr
                                     :w (double-rewrite x86)))
                 (open-qword-paddr-list (gather-all-paging-structure-qword-addresses
                                             (double-rewrite x86))))
    (canonical-address-p (+ -1 n-w write-addr))
    (canonical-address-p write-addr)
    (tlb-consistent-n (len bytes)
                      prog-addr
                      :x x86))
  (equal (program-at-alt prog-addr bytes
                         (mv-nth 1 (wb n-w write-addr w value x86)))
         (program-at-alt prog-addr bytes (double-rewrite x86)))))

Theorem: program-at-alt-xw-ms

(defthm program-at-alt-xw-ms
  (equal (program-at-alt prog-addr bytes (xw :ms index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-env

(defthm program-at-alt-xw-env
  (equal (program-at-alt prog-addr bytes (xw :env index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-undef

(defthm program-at-alt-xw-undef
  (equal (program-at-alt prog-addr
                         bytes (xw :undef index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-enable-peripherals

(defthm program-at-alt-xw-enable-peripherals
  (equal (program-at-alt prog-addr bytes
                         (xw :enable-peripherals index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-handle-exceptions

(defthm program-at-alt-xw-handle-exceptions
  (equal (program-at-alt prog-addr bytes
                         (xw :handle-exceptions index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-os-info

(defthm program-at-alt-xw-os-info
  (equal (program-at-alt prog-addr
                         bytes (xw :os-info index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-rgf

(defthm program-at-alt-xw-rgf
  (equal (program-at-alt prog-addr bytes (xw :rgf index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-rip

(defthm program-at-alt-xw-rip
  (equal (program-at-alt prog-addr bytes (xw :rip index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-str

(defthm program-at-alt-xw-str
  (equal (program-at-alt prog-addr bytes (xw :str index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-ssr-visible

(defthm program-at-alt-xw-ssr-visible
  (equal (program-at-alt prog-addr
                         bytes (xw :ssr-visible index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-ssr-hidden-base

(defthm program-at-alt-xw-ssr-hidden-base
  (equal (program-at-alt prog-addr bytes
                         (xw :ssr-hidden-base index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-ssr-hidden-limit

(defthm program-at-alt-xw-ssr-hidden-limit
  (equal (program-at-alt prog-addr bytes
                         (xw :ssr-hidden-limit index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-ssr-hidden-attr

(defthm program-at-alt-xw-ssr-hidden-attr
  (equal (program-at-alt prog-addr bytes
                         (xw :ssr-hidden-attr index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-dbg

(defthm program-at-alt-xw-dbg
  (equal (program-at-alt prog-addr bytes (xw :dbg index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-fp-data

(defthm program-at-alt-xw-fp-data
  (equal (program-at-alt prog-addr
                         bytes (xw :fp-data index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-fp-ctrl

(defthm program-at-alt-xw-fp-ctrl
  (equal (program-at-alt prog-addr
                         bytes (xw :fp-ctrl index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-fp-status

(defthm program-at-alt-xw-fp-status
  (equal (program-at-alt prog-addr
                         bytes (xw :fp-status index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-fp-tag

(defthm program-at-alt-xw-fp-tag
  (equal (program-at-alt prog-addr
                         bytes (xw :fp-tag index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-fp-last-inst

(defthm program-at-alt-xw-fp-last-inst
  (equal (program-at-alt prog-addr
                         bytes (xw :fp-last-inst index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-fp-last-data

(defthm program-at-alt-xw-fp-last-data
  (equal (program-at-alt prog-addr
                         bytes (xw :fp-last-data index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-fp-opcode

(defthm program-at-alt-xw-fp-opcode
  (equal (program-at-alt prog-addr
                         bytes (xw :fp-opcode index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-mxcsr

(defthm program-at-alt-xw-mxcsr
  (equal (program-at-alt prog-addr
                         bytes (xw :mxcsr index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-opmsk

(defthm program-at-alt-xw-opmsk
  (equal (program-at-alt prog-addr
                         bytes (xw :opmsk index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-zmm

(defthm program-at-alt-xw-zmm
  (equal (program-at-alt prog-addr bytes (xw :zmm index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-inhibit-interrupts-one-instruction

(defthm program-at-alt-xw-inhibit-interrupts-one-instruction
  (equal (program-at-alt prog-addr bytes
                         (xw :inhibit-interrupts-one-instruction
                             index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-time-stamp-counter

(defthm program-at-alt-xw-time-stamp-counter
  (equal (program-at-alt prog-addr bytes
                         (xw :time-stamp-counter index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-last-clock-event

(defthm program-at-alt-xw-last-clock-event
  (equal (program-at-alt prog-addr bytes
                         (xw :last-clock-event index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-tty-in

(defthm program-at-alt-xw-tty-in
  (equal (program-at-alt prog-addr
                         bytes (xw :tty-in index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-tty-out

(defthm program-at-alt-xw-tty-out
  (equal (program-at-alt prog-addr
                         bytes (xw :tty-out index val x86))
         (program-at-alt prog-addr bytes (double-rewrite x86))))

Theorem: program-at-alt-xw-rflags

(defthm program-at-alt-xw-rflags
 (implies
  (and
      (equal (rflagsbits->ac value)
             (rflagsbits->ac (xr :rflags nil (double-rewrite x86))))
      (not (app-view x86))
      (x86p x86))
  (equal (program-at-alt l-addrs
                         bytes (xw :rflags nil value x86))
         (program-at-alt l-addrs bytes (double-rewrite x86)))))

Theorem: program-at-alt-xw-tlb-atom

(defthm program-at-alt-xw-tlb-atom
  (implies
       (and (tlb-consistent-n (len bytes)
                              l-addrs
                              :x x86)
            (atom atm))
       (equal (program-at-alt l-addrs bytes (xw :tlb nil atm x86))
              (program-at-alt l-addrs bytes (double-rewrite x86)))))

Theorem: program-at-alt-after-mv-nth-2-rb

(defthm program-at-alt-after-mv-nth-2-rb
 (implies
     (not (mv-nth 0
                  (las-to-pas n lin-addr r-x (double-rewrite x86))))
     (equal (program-at-alt prog-addr bytes
                            (mv-nth 2 (rb n lin-addr r-x x86)))
            (program-at-alt prog-addr bytes (double-rewrite x86)))))