• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Riscv
        • Specification
          • Semantics
          • Features
          • Instructions
          • Encoding
          • States
            • Stat
            • Stat-validp
            • Read-instruction
            • Write-memory-unsigned64
            • Write-memory-unsigned32
            • Write-memory-unsigned8
            • Write-memory-unsigned16
            • Write-xreg-32
            • Read-xreg-unsigned
            • Write-xreg
            • Read-memory-unsigned64
            • Read-memory-unsigned8
            • Read-memory-unsigned32
            • Read-xreg-signed
            • Read-memory-unsigned16
            • Read-xreg-unsigned32
            • Write-pc
            • Read-xreg-signed32
            • Inc4-pc
            • Read-pc
            • Errorp
            • Error
          • Reads-over-writes
          • Semantics-equivalences
          • Decoding
          • Execution
        • Executable
        • Specialized
        • Optimized
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• States

Read-pc

Read the program counter.

Signature

(read-pc stat feat) → pc

Arguments

stat — Guard (statp stat).

feat — Guard (featp feat).

Returns

pc — Type (unsigned-byte-p (feat->xlen feat) pc).

The result is always an unsigned XLEN-bit integer, which is an address in memory; recall that the memory address space goes from 0 to 2^XLEN - 1, as explained in stat.

Definitions and Theorems

Function: read-pc

(defun read-pc (stat feat)
  (declare (xargs :guard (and (statp stat) (featp feat))))
  (declare (xargs :type-prescription (natp (read-pc stat feat))
                  :guard (stat-validp stat feat)))
  (let ((__function__ 'read-pc))
    (declare (ignorable __function__))
    (unsigned-byte-fix (feat->xlen feat)
                       (stat->pc stat))))

Theorem: return-type-of-read-pc

(defthm return-type-of-read-pc
  (b* ((pc (read-pc stat feat)))
    (unsigned-byte-p (feat->xlen feat) pc))
  :rule-classes :rewrite)

Theorem: ubyte32p-of-read-pc-when-32p

(defthm ubyte32p-of-read-pc-when-32p
  (implies (and (stat-validp stat feat)
                (feat-32p feat))
           (b* ((acl2::?pc (read-pc stat feat)))
             (ubyte32p pc))))

Theorem: ubyte64p-of-read-pc-when-64p

(defthm ubyte64p-of-read-pc-when-64p
  (implies (and (stat-validp stat feat)
                (feat-64p feat))
           (b* ((acl2::?pc (read-pc stat feat)))
             (ubyte64p pc))))

Theorem: read-pc-of-stat-fix-stat

(defthm read-pc-of-stat-fix-stat
  (equal (read-pc (stat-fix stat) feat)
         (read-pc stat feat)))

Theorem: read-pc-stat-equiv-congruence-on-stat

(defthm read-pc-stat-equiv-congruence-on-stat
  (implies (stat-equiv stat stat-equiv)
           (equal (read-pc stat feat)
                  (read-pc stat-equiv feat)))
  :rule-classes :congruence)

Theorem: read-pc-of-feat-fix-feat

(defthm read-pc-of-feat-fix-feat
  (equal (read-pc stat (feat-fix feat))
         (read-pc stat feat)))

Theorem: read-pc-feat-equiv-congruence-on-feat

(defthm read-pc-feat-equiv-congruence-on-feat
  (implies (feat-equiv feat feat-equiv)
           (equal (read-pc stat feat)
                  (read-pc stat feat-equiv)))
  :rule-classes :congruence)