• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
      • Program-execution
      • Introduction
      • X86isa-build-instructions
      • Publications
      • Contributors
      • Machine
        • Syscalls
        • Cpuid
        • X86isa-state
        • Linear-memory
        • Rflag-specifications
        • Characterizing-undefined-behavior
        • Top-level-memory
        • App-view
        • X86-decoder
        • Physical-memory
        • Decoding-and-spec-utils
        • Instructions
        • X86-modes
        • Segmentation
        • Register-readers-and-writers
        • Other-non-deterministic-computations
        • Environment
          • Components-of-the-environment-field
            • Write-x86-file-des-logic
            • Write-x86-file-contents-logic
            • Read-x86-file-des-logic
            • Read-x86-file-contents-logic
            • Delete-x86-file-des-logic
            • Delete-x86-file-contents-logic
            • Pop-x86-oracle-logic
            • Write-x86-file-des
            • Write-x86-file-contents
            • Pop-x86-oracle
            • Env-read
            • Delete-x86-file-des
            • Delete-x86-file-contents
            • Env-write
            • Read-x86-file-des
            • Read-x86-file-contents
            • Env-write-logic
            • Env-read-logic
          • Reading-memory-as-strings-or-bytes
          • Converting-between-strings-and-bytes
          • Writing-strings-or-bytes-to-memory
        • Paging
      • Implemented-opcodes
      • Proof-utilities
      • To-do
      • Concrete-simulation-examples
      • Model-validation
      • Utils
      • Debugging-code-proofs
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Environment

Components-of-the-environment-field

We don't check for ill-formed environment very rigorously. For example, one can have STANDARD-INPUT's mode as O_WRONLY, and it'll still be a good env-alistp.

'((:FILE-DESCRIPTORS . ((0 . ((:NAME . "STANDARD-INPUT") 
                              (:OFFSET . 0) 
                              (:MODE . 0))) 
                        (1 . ((:NAME . "STANDARD-OUTPUT") 
                              (:OFFSET . 0) 
                              (:MODE . 1))) 
                        (2 . ((:NAME . "ERROR") 
                              (:OFFSET . 0) 
                              (:MODE . 2))) 
                        (3 . ((:NAME . "FOO.TXT") 
                              (:OFFSET . 0) 
                              (:MODE . 8))))) 
 
  (:FILE-CONTENTS    . (("STANDARD-INPUT"  . ((:CONTENTS . "Contents 0"))) 
                        ("STANDARD-OUTPUT" . ((:CONTENTS . "Contents 1"))) 
                        ("ERROR"           . ((:CONTENTS . "Contents 2"))) 
                        ("FOO.TXT"         . ((:CONTENTS . "Contents 3"))) 
                        )) 
 
  (:ORACLE           . ((1 . ((-1 . "hello") 5000)) 
                        (2 . (0))))) 

Definitions and Theorems

Theorem: alistp-put-assoc-equal-equal

(defthm alistp-put-assoc-equal-equal
  (implies (force (alistp x))
           (alistp (put-assoc-equal i y x)))
  :rule-classes :type-prescription)

Theorem: alistp-remove1-assoc-equal-equal

(defthm alistp-remove1-assoc-equal-equal
  (implies (force (alistp x))
           (alistp (remove1-assoc-equal i x)))
  :rule-classes :type-prescription)

Function: env-read-logic

(defun env-read-logic (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'env-read-logic))
    (declare (ignorable __function__))
    (env x86)))

Function: env-read$notinline

(defun env-read$notinline (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'env-read))
    (declare (ignorable __function__))
    (env-read-logic x86)))

Theorem: env-alistp-env-read

(defthm env-alistp-env-read
  (implies (x86p x86)
           (env-alistp (env-read x86)))
  :rule-classes :forward-chaining)

Function: env-write-logic

(defun env-write-logic (env x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (env-alistp env)))
  (let ((__function__ 'env-write-logic))
    (declare (ignorable __function__))
    (!env env x86)))

Function: env-write$notinline

(defun env-write$notinline (env x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (env-alistp env)))
  (let ((__function__ 'env-write))
    (declare (ignorable __function__))
    (env-write-logic env x86)))

Theorem: x86p-env-write

(defthm x86p-env-write
  (implies (and (x86p x86) (env-alistp env))
           (x86p (env-write env x86))))

Theorem: alistp-of-xr-env

(defthm alistp-of-xr-env
  (alistp (xr :env i x86$a)))

Function: read-x86-file-des-logic

(defun read-x86-file-des-logic (id x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (integerp id)))
  (let ((__function__ 'read-x86-file-des-logic))
    (declare (ignorable __function__))
    (b* ((env (env-read x86))
         (file-des-field (assoc-equal :file-descriptors env))
         (fd-name-field (if (atom file-des-field)
                            nil
                          (assoc-equal id (cdr file-des-field))))
         (name-field (if (atom fd-name-field)
                         nil
                       (cdr fd-name-field))))
      name-field)))

Function: read-x86-file-des$notinline

(defun read-x86-file-des$notinline (id x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (integerp id)))
  (let ((__function__ 'read-x86-file-des))
    (declare (ignorable __function__))
    (read-x86-file-des-logic id x86)))

Theorem: read-x86-file-des-xw

(defthm read-x86-file-des-xw
  (implies (not (equal fld :env))
           (equal (read-x86-file-des id (xw fld index value x86))
                  (read-x86-file-des id x86))))

Theorem: rip-ret-alistp-of-xr-env

(defthm rip-ret-alistp-of-xr-env
  (rip-ret-alistp (cdr (assoc-equal :oracle (xr :env i x86$a)))))

Function: write-x86-file-des-logic

(defun write-x86-file-des-logic (fd fd-field x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (integerp fd)))
 (let ((__function__ 'write-x86-file-des-logic))
  (declare (ignorable __function__))
  (b*
   ((env (env-read x86))
    (file-des-field (cdr (assoc-equal :file-descriptors env)))
    (x86
     (env-write (acons ':file-descriptors
                       (put-assoc-equal fd fd-field file-des-field)
                       (acons ':file-contents
                              (cdr (assoc-equal :file-contents env))
                              (acons ':oracle
                                     (cdr (assoc-equal :oracle env))
                                     nil)))
                x86)))
   x86)))

Function: write-x86-file-des$notinline

(defun write-x86-file-des$notinline (fd fd-field x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (integerp fd)))
  (let ((__function__ 'write-x86-file-des))
    (declare (ignorable __function__))
    (write-x86-file-des-logic fd fd-field x86)))

Theorem: x86p-write-x86-file-des

(defthm x86p-write-x86-file-des
  (implies (and (x86p x86) (integerp fd))
           (x86p (write-x86-file-des fd fd-field x86))))

Theorem: xr-write-x86-file-des

(defthm xr-write-x86-file-des
  (implies (not (equal fld :env))
           (equal (xr fld index
                      (write-x86-file-des fd fd-field x86))
                  (xr fld index x86))))

Theorem: 64-bit-modep-of-write-x86-file-des

(defthm 64-bit-modep-of-write-x86-file-des
  (equal (64-bit-modep (write-x86-file-des fd fd-field x86))
         (64-bit-modep x86)))

Theorem: x86-operation-mode-of-write-x86-file-des

(defthm x86-operation-mode-of-write-x86-file-des
  (equal (x86-operation-mode (write-x86-file-des fd fd-field x86))
         (x86-operation-mode x86)))

Theorem: write-x86-file-des-xw

(defthm write-x86-file-des-xw
  (implies (not (equal fld :env))
           (equal (write-x86-file-des i v (xw fld index value x86))
                  (xw fld index
                      value (write-x86-file-des i v x86)))))

Function: delete-x86-file-des-logic

(defun delete-x86-file-des-logic (fd x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (integerp fd)))
 (let ((__function__ 'delete-x86-file-des-logic))
  (declare (ignorable __function__))
  (b*
   ((env (env-read x86))
    (file-des-field (cdr (assoc-equal :file-descriptors env)))
    (x86
     (env-write (acons ':file-descriptors
                       (remove1-assoc-equal fd file-des-field)
                       (acons ':file-contents
                              (cdr (assoc-equal :file-contents env))
                              (acons ':oracle
                                     (cdr (assoc-equal :oracle env))
                                     nil)))
                x86)))
   x86)))

Function: delete-x86-file-des$notinline

(defun delete-x86-file-des$notinline (fd x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (integerp fd)))
  (let ((__function__ 'delete-x86-file-des))
    (declare (ignorable __function__))
    (delete-x86-file-des-logic fd x86)))

Theorem: x86p-delete-x86-file-des

(defthm x86p-delete-x86-file-des
  (implies (and (x86p x86) (integerp fd))
           (x86p (delete-x86-file-des fd x86))))

Theorem: xr-delete-x86-file-des

(defthm xr-delete-x86-file-des
  (implies (not (equal fld :env))
           (equal (xr fld index (delete-x86-file-des fd x86))
                  (xr fld index x86))))

Theorem: delete-x86-file-des-xw

(defthm delete-x86-file-des-xw
  (implies (not (equal fld :env))
           (equal (delete-x86-file-des i (xw fld index value x86))
                  (xw fld index
                      value (delete-x86-file-des i x86)))))

Function: read-x86-file-contents-logic

(defun read-x86-file-contents-logic (name x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (stringp name)))
 (let ((__function__ 'read-x86-file-contents-logic))
  (declare (ignorable __function__))
  (b*
   ((env (env-read x86))
    (name-file-contents-field (assoc-equal :file-contents env))
    (file-contents-field
        (if (atom name-file-contents-field)
            nil
          (cdr (assoc-equal name (cdr name-file-contents-field))))))
   file-contents-field)))

Function: read-x86-file-contents$notinline

(defun read-x86-file-contents$notinline (name x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (stringp name)))
  (let ((__function__ 'read-x86-file-contents))
    (declare (ignorable __function__))
    (read-x86-file-contents-logic name x86)))

Theorem: read-x86-file-contents-xw

(defthm read-x86-file-contents-xw
  (implies
       (not (equal fld :env))
       (equal (read-x86-file-contents name (xw fld index value x86))
              (read-x86-file-contents name x86))))

Function: write-x86-file-contents-logic

(defun write-x86-file-contents-logic (name contents-field x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (stringp name)))
 (let ((__function__ 'write-x86-file-contents-logic))
  (declare (ignorable __function__))
  (b*
   ((env (env-read x86))
    (file-contents-field (cdr (assoc-equal :file-contents env)))
    (x86
     (env-write
      (acons
       ':file-descriptors
       (cdr (assoc-equal :file-descriptors env))
       (acons
           ':file-contents
           (put-assoc-equal name contents-field file-contents-field)
           (acons ':oracle
                  (cdr (assoc-equal :oracle env))
                  nil)))
      x86)))
   x86)))

Function: write-x86-file-contents$notinline

(defun write-x86-file-contents$notinline (name contents x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (stringp name)))
  (let ((__function__ 'write-x86-file-contents))
    (declare (ignorable __function__))
    (write-x86-file-contents-logic name contents x86)))

Theorem: x86p-write-x86-file-contents

(defthm x86p-write-x86-file-contents
  (implies (and (x86p x86) (stringp name))
           (x86p (write-x86-file-contents name contents x86))))

Theorem: xr-write-x86-file-contents

(defthm xr-write-x86-file-contents
  (implies (not (equal fld :env))
           (equal (xr fld index
                      (write-x86-file-contents name contents x86))
                  (xr fld index x86))))

Theorem: write-x86-file-contents-xw

(defthm write-x86-file-contents-xw
  (implies
       (not (equal fld :env))
       (equal (write-x86-file-contents i v (xw fld index value x86))
              (xw fld index value
                  (write-x86-file-contents i v x86)))))

Function: delete-x86-file-contents-logic

(defun delete-x86-file-contents-logic (name x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard (stringp name)))
 (let ((__function__ 'delete-x86-file-contents-logic))
  (declare (ignorable __function__))
  (b*
   ((env (env-read x86))
    (file-contents-field (cdr (assoc-equal :file-contents env)))
    (x86
     (env-write
        (acons ':file-descriptors
               (cdr (assoc-equal :file-descriptors env))
               (acons ':file-contents
                      (remove1-assoc-equal name file-contents-field)
                      (acons ':oracle
                             (cdr (assoc-equal :oracle env))
                             nil)))
        x86)))
   x86)))

Function: delete-x86-file-contents$notinline

(defun delete-x86-file-contents$notinline (name x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard (stringp name)))
  (let ((__function__ 'delete-x86-file-contents))
    (declare (ignorable __function__))
    (delete-x86-file-contents-logic name x86)))

Theorem: x86p-delete-x86-file-contents

(defthm x86p-delete-x86-file-contents
  (implies (and (x86p x86) (stringp name))
           (x86p (delete-x86-file-contents name x86))))

Theorem: xr-delete-x86-file-contents

(defthm xr-delete-x86-file-contents
  (implies (not (equal fld :env))
           (equal (xr fld index
                      (delete-x86-file-contents name x86))
                  (xr fld index x86))))

Theorem: delete-x86-file-contents-xw

(defthm delete-x86-file-contents-xw
  (implies
       (not (equal fld :env))
       (equal (delete-x86-file-contents i (xw fld index value x86))
              (xw fld index value
                  (delete-x86-file-contents i x86)))))

Theorem: alistp-of-oracle-of-xr-env

(defthm alistp-of-oracle-of-xr-env
  (alistp (cdr (assoc-equal :oracle (xr :env i x86$a))))
  :rule-classes (:rewrite :type-prescription))

Function: pop-x86-oracle-logic

(defun pop-x86-oracle-logic (x86)
 (declare (xargs :stobjs (x86)))
 (declare (xargs :guard t))
 (let ((__function__ 'pop-x86-oracle-logic))
  (declare (ignorable __function__))
  (b*
   ((rip (rip x86))
    (env (env-read x86))
    (oracle (cdr (assoc-equal :oracle env)))
    (vals (assoc-equal rip oracle))
    (lst (if (consp vals)
             (if (consp (cdr vals)) (cdr vals) nil)
           nil))
    ((mv val x86)
     (if (atom lst)
         (let ((x86 (!ms (list :syscall-oracle-pop-empty rip)
                         x86)))
           (mv -1 x86))
      (let
       ((x86
         (env-write
           (acons
                ':file-descriptors
                (cdr (assoc-equal :file-descriptors env))
                (acons ':file-contents
                       (cdr (assoc-equal :file-contents env))
                       (acons ':oracle
                              (put-assoc-equal rip (cdr lst) oracle)
                              nil)))
           x86)))
       (mv (car lst) x86)))))
   (mv val x86))))

Function: pop-x86-oracle$notinline

(defun pop-x86-oracle$notinline (x86)
  (declare (xargs :stobjs (x86)))
  (declare (xargs :guard t))
  (let ((__function__ 'pop-x86-oracle))
    (declare (ignorable __function__))
    (pop-x86-oracle-logic x86)))

Theorem: x86p-mv-nth-1-pop-x86-oracle

(defthm x86p-mv-nth-1-pop-x86-oracle
  (implies (x86p x86)
           (x86p (mv-nth 1 (pop-x86-oracle x86)))))

Theorem: xr-pop-x86-oracle-state

(defthm xr-pop-x86-oracle-state
  (implies (and (not (equal fld :env))
                (not (equal fld :ms)))
           (equal (xr fld
                      index (mv-nth 1 (pop-x86-oracle x86)))
                  (xr fld index x86))))

Theorem: pop-x86-oracle-xw

(defthm pop-x86-oracle-xw
  (implies (and (not (equal fld :env))
                (not (equal fld :rip)))
           (equal (mv-nth 0
                          (pop-x86-oracle (xw fld index value x86)))
                  (mv-nth 0 (pop-x86-oracle x86)))))

Theorem: xw-pop-x86-oracle-state

(defthm xw-pop-x86-oracle-state
  (implies (and (not (equal fld :env))
                (not (equal fld :rip))
                (not (equal fld :ms)))
           (equal (mv-nth 1
                          (pop-x86-oracle (xw fld index value x86)))
                  (xw fld index value
                      (mv-nth 1 (pop-x86-oracle x86))))))

Subtopics

Write-x86-file-des-logic

Write-x86-file-contents-logic

Read-x86-file-des-logic

Read File Descriptor Field

Read-x86-file-contents-logic

Read File Contents Field

Delete-x86-file-des-logic

Delete-x86-file-contents-logic

Pop-x86-oracle-logic

Write-x86-file-des

Write-x86-file-contents

Pop-x86-oracle

Env-read

Delete-x86-file-des

Delete-x86-file-contents

Env-write

Read-x86-file-des

Read-x86-file-contents

Env-write-logic

Env-read-logic