• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
        • Dynamic-instrumentation
        • Initialize-x86-state
          • Init-x86-state-64
          • Load-program-into-memory
          • Init-x86-state
          • !seg-hidden-limiti-from-alist
          • !seg-hidden-basei-from-alist
          • !seg-hidden-attri-from-alist
          • Seg-hidden-limiti-alistp
          • Seg-hidden-basei-alistp
          • !seg-visiblei-from-alist
          • Seg-visiblei-alistp
          • Seg-hidden-attri-alistp
          • Rgfi-alistp
          • N64p-byte-alistp
          • !rgfi-from-alist
          • !msri-from-alist
          • !ctri-from-alist
          • Msri-alistp
          • Ctri-alistp
        • Binary-file-load-fn
        • Read-channel-into-byte-list1
        • Setting-up-page-tables
        • Init-zero-page
        • Load-file-into-memory
        • Linux-load
        • Init-sys-view
        • Load-elf-sections
        • Chars-to-c-str
        • String-to-c-str
        • Pack-u64
        • Pack-u32
        • Concrete-simulation-examples
        • Gdt-entry
      • Tlb
      • Booting-linux
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Peripherals
      • Model-validation
      • Modelcalls
      • Concrete-simulation-examples
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Initialize-x86-state

!seg-hidden-basei-from-alist

Update hidden portion of segment registers as dictated by seg-hidden-alist, which is required to be a seg-hidden-basei-alistp.

Signature

(!seg-hidden-basei-from-alist seg-hidden-alist x86) → x86

Definitions and Theorems

Function: !seg-hidden-basei-from-alist

(defun !seg-hidden-basei-from-alist (seg-hidden-alist x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (seg-hidden-basei-alistp seg-hidden-alist)))
 (let ((__function__ '!seg-hidden-basei-from-alist))
   (declare (ignorable __function__))
   (cond ((endp seg-hidden-alist) x86)
         (t (let ((x86 (!seg-hidden-basei (caar seg-hidden-alist)
                                          (cdar seg-hidden-alist)
                                          x86)))
              (!seg-hidden-basei-from-alist (cdr seg-hidden-alist)
                                            x86))))))

Theorem: x86p-!seg-hidden-basei-from-alist

(defthm x86p-!seg-hidden-basei-from-alist
  (implies (and (seg-hidden-basei-alistp alist)
                (x86p x86))
           (x86p (!seg-hidden-basei-from-alist alist x86))))