• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • Proof-checker-array
    • Soft
    • C
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Leftist-trees
    • Java
    • Riscv
      • Specification
      • Executable
      • Specialized
      • Optimized
        • State-stobj
          • Stat1
          • Stat1-iso
          • Stat1-from-stat
          • Write1-memory-unsigned64
          • Stat-from-stat1
          • Read1-memory-unsigned64
          • Write1-memory-unsigned32
          • Make-stat1
          • Write1-xreg
          • Write1-memory-unsigned8
          • Write1-memory-unsigned16
          • Stat1->memory
          • Read1-memory-unsigned32
          • Read1-instruction
          • Write1-xreg-32
          • Write1-pc
          • Read1-memory-unsigned16
          • Stat1-validp
          • Read1-xreg-unsigned32
          • Read1-xreg-unsigned
          • Read1-xreg-signed32
          • Read1-memory-unsigned8
          • Inc1-4-pc
          • Error1
          • Read1-xreg-signed
          • Read1-pc
          • Errorp1
    • Taspi
    • Bitcoin
    • Des
    • Ethereum
    • X86isa
    • Sha-2
    • Yul
    • Zcash
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Poseidon
    • Where-do-i-place-my-book
    • Axe
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• State-stobj

Stat1

State stobj.

This could be probably automatically generated from the fty::defprod that defines stat.

The unconstrained xregs and pc of stat is turned into unconstrained scalar fields of the stobj. The memory list of bytes of stat is turned into a resizable array of bytes in the stobj, initially of length 0 (the initial length does not matter here). The error boolean of stat is turned into a boolean field in the stobj.

We rename and disable the generated stobj functions.

We introduce a non-executable function to retrieve the whole memory array. This cannot be executable, because it violates stobj usage rules; however, it makes logical sense.

We introduce a function to build a stobj value from the values of its fields. While this makes logical sense, the values it returns are unrelated to the live stobj.

We also introduce some equivalences between recognizers of stobj fields and recognizers of stat field types.

Definitions and Theorems

Definition: stat1-xregs-p

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: stat1-pc-p

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: stat1-memory-p

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: stat1-error-p

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: stat1p

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: create-stat1

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: stat1->xregs

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: update-stat1->xregs

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: stat1->pc

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: update-stat1->pc

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: stat1->memory-size

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: update-stat1->memory-size

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: stat1->memory-byte

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: update-stat1->memory-byte

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: stat1->error

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Definition: update-stat1->error

(defstobj stat1
  (xregs)
  (pc)
  (memory :type (array (unsigned-byte 8) (0))
          :initially 0
          :resizable t)
  (error :type (satisfies booleanp))
  :renaming ((xregsp stat1-xregs-p)
             (acl2::pcp stat1-pc-p)
             (memoryp stat1-memory-p)
             (errorp stat1-error-p)
             (xregs stat1->xregs)
             (pc stat1->pc)
             (memory-length stat1->memory-size)
             (memoryi stat1->memory-byte)
             (error stat1->error)
             (update-xregs update-stat1->xregs)
             (acl2::update-pc update-stat1->pc)
             (resize-memory update-stat1->memory-size)
             (update-memoryi update-stat1->memory-byte)
             (update-error update-stat1->error)))

Function: stat1->memory

(defun stat1->memory (stat1)
  (declare (xargs :stobjs (stat1)))
  (declare (xargs :guard (stat1p stat1)))
  (declare (xargs :non-executable t))
  (prog2$ (acl2::throw-nonexec-error 'stat1->memory
                                     (list stat1))
          (let ((__function__ 'stat1->memory))
            (declare (ignorable __function__))
            (nth 2 stat1))))

Theorem: stat1-memory-p-of-stat1->memory

(defthm stat1-memory-p-of-stat1->memory
  (implies (stat1p stat1)
           (b* ((memory (stat1->memory stat1)))
             (stat1-memory-p memory)))
  :rule-classes :rewrite)

Function: make-stat1

(defun make-stat1 (xregs pc memory error)
  (declare (xargs :guard (and (stat1-xregs-p xregs)
                              (stat1-pc-p pc)
                              (stat1-memory-p memory)
                              (stat1-error-p error))))
  (let ((__function__ 'make-stat1))
    (declare (ignorable __function__))
    (list xregs pc memory error)))

Theorem: stat1p-of-make-stat1

(defthm stat1p-of-make-stat1
  (implies (and (stat1-xregs-p xregs)
                (stat1-pc-p pc)
                (stat1-memory-p memory)
                (stat1-error-p error))
           (b* ((stat1 (make-stat1 xregs pc memory error)))
             (stat1p stat1)))
  :rule-classes :rewrite)

Theorem: stat1-memory-p-to-ubyte8-listp

(defthm stat1-memory-p-to-ubyte8-listp
  (equal (stat1-memory-p x)
         (ubyte8-listp x)))

Theorem: ubyte8-listp-to-stat1-memory-p

(defthm ubyte8-listp-to-stat1-memory-p
  (equal (ubyte8-listp x)
         (stat1-memory-p x)))

Theorem: stat1-error-p-to-booleanp

(defthm stat1-error-p-to-booleanp
  (equal (stat1-error-p x) (booleanp x)))

Theorem: booleanp-to-stat1-error-p

(defthm booleanp-to-stat1-error-p
  (equal (booleanp x) (stat1-error-p x)))