• 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

Write-memory-unsigned64

Write an unsigned 64-bit integer to memory.

Signature

(write-memory-unsigned64 addr val stat feat) → new-stat

Arguments

addr — Guard (integerp addr).

val — Guard (ubyte64p val).

stat — Guard (statp stat).

feat — Guard (featp feat).

Returns

new-stat — Type (statp new-stat).

The memory address is the one of the first byte; we write that, and the subsequent bytes. We write the bytes according to endianness.

As in write-memory-unsigned8, we let the address be any integer. We use write-memory-unsigned8 four times. Note that if addr is close to 2^XLEN - 1, then the subsequent addresses may wrap around to address 0.

Definitions and Theorems

Function: write-memory-unsigned64

(defun write-memory-unsigned64 (addr val stat feat)
  (declare (xargs :guard (and (integerp addr)
                              (ubyte64p val)
                              (statp stat)
                              (featp feat))))
  (declare (xargs :guard (stat-validp stat feat)))
  (let ((__function__ 'write-memory-unsigned64))
    (declare (ignorable __function__))
    (b* ((val (ubyte64-fix val))
         (b0 (part-select val :low 0 :width 8))
         (b1 (part-select val :low 8 :width 8))
         (b2 (part-select val :low 16 :width 8))
         (b3 (part-select val :low 24 :width 8))
         (b4 (part-select val :low 32 :width 8))
         (b5 (part-select val :low 40 :width 8))
         (b6 (part-select val :low 48 :width 8))
         (b7 (part-select val :low 56 :width 8))
         ((mv 1st-byte 2nd-byte 3rd-byte 4th-byte
              5th-byte 6th-byte 7th-byte 8th-byte)
          (if (feat-little-endianp feat)
              (mv b0 b1 b2 b3 b4 b5 b6 b7)
            (mv b7 b6 b5 b4 b3 b2 b1 b0)))
         (stat (write-memory-unsigned8 addr 1st-byte stat feat))
         (stat (write-memory-unsigned8 (+ (lifix addr) 1)
                                       2nd-byte stat feat))
         (stat (write-memory-unsigned8 (+ (lifix addr) 2)
                                       3rd-byte stat feat))
         (stat (write-memory-unsigned8 (+ (lifix addr) 3)
                                       4th-byte stat feat))
         (stat (write-memory-unsigned8 (+ (lifix addr) 4)
                                       5th-byte stat feat))
         (stat (write-memory-unsigned8 (+ (lifix addr) 5)
                                       6th-byte stat feat))
         (stat (write-memory-unsigned8 (+ (lifix addr) 6)
                                       7th-byte stat feat))
         (stat (write-memory-unsigned8 (+ (lifix addr) 7)
                                       8th-byte stat feat)))
      stat)))

Theorem: statp-of-write-memory-unsigned64

(defthm statp-of-write-memory-unsigned64
  (b* ((new-stat (write-memory-unsigned64 addr val stat feat)))
    (statp new-stat))
  :rule-classes :rewrite)

Theorem: stat-validp-of-write-memory-unsigned64

(defthm stat-validp-of-write-memory-unsigned64
 (implies
      (stat-validp stat feat)
      (b* ((?new-stat (write-memory-unsigned64 addr val stat feat)))
        (stat-validp new-stat feat))))

Theorem: write-memory-unsigned64-of-ifix-addr

(defthm write-memory-unsigned64-of-ifix-addr
  (equal (write-memory-unsigned64 (ifix addr)
                                  val stat feat)
         (write-memory-unsigned64 addr val stat feat)))

Theorem: write-memory-unsigned64-int-equiv-congruence-on-addr

(defthm write-memory-unsigned64-int-equiv-congruence-on-addr
  (implies
       (acl2::int-equiv addr addr-equiv)
       (equal (write-memory-unsigned64 addr val stat feat)
              (write-memory-unsigned64 addr-equiv val stat feat)))
  :rule-classes :congruence)

Theorem: write-memory-unsigned64-of-ubyte64-fix-val

(defthm write-memory-unsigned64-of-ubyte64-fix-val
  (equal (write-memory-unsigned64 addr (ubyte64-fix val)
                                  stat feat)
         (write-memory-unsigned64 addr val stat feat)))

Theorem: write-memory-unsigned64-ubyte64-equiv-congruence-on-val

(defthm write-memory-unsigned64-ubyte64-equiv-congruence-on-val
  (implies
       (acl2::ubyte64-equiv val val-equiv)
       (equal (write-memory-unsigned64 addr val stat feat)
              (write-memory-unsigned64 addr val-equiv stat feat)))
  :rule-classes :congruence)

Theorem: write-memory-unsigned64-of-stat-fix-stat

(defthm write-memory-unsigned64-of-stat-fix-stat
  (equal (write-memory-unsigned64 addr val (stat-fix stat)
                                  feat)
         (write-memory-unsigned64 addr val stat feat)))

Theorem: write-memory-unsigned64-stat-equiv-congruence-on-stat

(defthm write-memory-unsigned64-stat-equiv-congruence-on-stat
  (implies
       (stat-equiv stat stat-equiv)
       (equal (write-memory-unsigned64 addr val stat feat)
              (write-memory-unsigned64 addr val stat-equiv feat)))
  :rule-classes :congruence)

Theorem: write-memory-unsigned64-of-feat-fix-feat

(defthm write-memory-unsigned64-of-feat-fix-feat
  (equal (write-memory-unsigned64 addr val stat (feat-fix feat))
         (write-memory-unsigned64 addr val stat feat)))

Theorem: write-memory-unsigned64-feat-equiv-congruence-on-feat

(defthm write-memory-unsigned64-feat-equiv-congruence-on-feat
  (implies
       (feat-equiv feat feat-equiv)
       (equal (write-memory-unsigned64 addr val stat feat)
              (write-memory-unsigned64 addr val stat feat-equiv)))
  :rule-classes :congruence)