• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
      • Specification
        • Semantics
        • Features
        • Instructions
        • Encoding
        • States
        • Reads-over-writes
          • Read-memory-of-write-memory-theorems
          • Read-xreg-of-write-memory-theorems
          • Read-xreg-of-write-xreg-theorems
          • Read-xreg-of-write-pc-theorems
          • Read-memory-of-write-pc-theorems
          • Read-memory-of-write-xreg-theorems
          • Read-pc-of-write-pc-theorems
          • Read-pc-of-write-memory-theorems
          • Read-instr-of-write-pc-theorems
          • Read-instr-of-write-memory-theorems
          • Read-pc-of-write-xreg-theorems
          • Read-instr-of-write-xreg-theorems
        • Semantics-equivalences
        • Decoding
        • Execution
      • Executable
      • Specialized
      • Optimized
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Reads-over-writes

Read-memory-of-write-memory-theorems

Theorems about reads of memory over writes of memory.

The theorem involving a single byte has a simple form. Theorems involving multiple bytes have more complex forms, because addresses may be disjoint or they may partially or totally overlap. We have some of the theorems, and we plan to add the remaining ones.

We provide a ruleset with these theorems.

Definitions and Theorems

Theorem: read-mem8-of-write-mem8

(defthm read-mem8-of-write-mem8
  (implies (stat-validp stat feat)
           (equal (read-mem8 addr1 (write-mem8 addr2 val stat feat)
                             feat)
                  (if (equal (loghead (feat->xlen feat) addr1)
                             (loghead (feat->xlen feat) addr2))
                      (ubyte8-fix val)
                    (read-mem8 addr1 stat feat)))))

Theorem: read-mem8-of-write-mem16

(defthm read-mem8-of-write-mem16
  (implies (stat-validp stat feat)
           (equal (read-mem8 addr1 (write-mem16 addr2 val stat feat)
                             feat)
                  (cond ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat) addr2))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte16-fix val)
                                             :low 0
                                             :high 7))
                               ((feat-big-endianp feat)
                                (part-select (ubyte16-fix val)
                                             :low 8
                                             :high 15))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (1+ (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte16-fix val)
                                             :low 8
                                             :high 15))
                               ((feat-big-endianp feat)
                                (part-select (ubyte16-fix val)
                                             :low 0
                                             :high 7))))
                        (t (read-mem8 addr1 stat feat))))))

Theorem: read-mem8-of-write-mem32

(defthm read-mem8-of-write-mem32
  (implies (stat-validp stat feat)
           (equal (read-mem8 addr1 (write-mem32 addr2 val stat feat)
                             feat)
                  (cond ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat) addr2))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte32-fix val)
                                             :low 0
                                             :high 7))
                               ((feat-big-endianp feat)
                                (part-select (ubyte32-fix val)
                                             :low 24
                                             :high 31))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (+ 1 (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte32-fix val)
                                             :low 8
                                             :high 15))
                               ((feat-big-endianp feat)
                                (part-select (ubyte32-fix val)
                                             :low 16
                                             :high 23))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (+ 2 (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte32-fix val)
                                             :low 16
                                             :high 23))
                               ((feat-big-endianp feat)
                                (part-select (ubyte32-fix val)
                                             :low 8
                                             :high 15))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (+ 3 (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte32-fix val)
                                             :low 24
                                             :high 31))
                               ((feat-big-endianp feat)
                                (part-select (ubyte32-fix val)
                                             :low 0
                                             :high 7))))
                        (t (read-mem8 addr1 stat feat))))))

Theorem: read-mem8-of-write-mem64

(defthm read-mem8-of-write-mem64
  (implies (stat-validp stat feat)
           (equal (read-mem8 addr1 (write-mem64 addr2 val stat feat)
                             feat)
                  (cond ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat) addr2))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 0
                                             :high 7))
                               ((feat-big-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 56
                                             :high 63))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (+ 1 (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 8
                                             :high 15))
                               ((feat-big-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 48
                                             :high 55))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (+ 2 (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 16
                                             :high 23))
                               ((feat-big-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 40
                                             :high 47))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (+ 3 (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 24
                                             :high 31))
                               ((feat-big-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 32
                                             :high 39))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (+ 4 (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 32
                                             :high 39))
                               ((feat-big-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 24
                                             :high 31))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (+ 5 (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 40
                                             :high 47))
                               ((feat-big-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 16
                                             :high 23))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (+ 6 (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 48
                                             :high 55))
                               ((feat-big-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 8
                                             :high 15))))
                        ((equal (loghead (feat->xlen feat) addr1)
                                (loghead (feat->xlen feat)
                                         (+ 7 (ifix addr2))))
                         (cond ((feat-little-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 56
                                             :high 63))
                               ((feat-big-endianp feat)
                                (part-select (ubyte64-fix val)
                                             :low 0
                                             :high 7))))
                        (t (read-mem8 addr1 stat feat))))))

Theorem: read-mem16-of-write-mem8

(defthm read-mem16-of-write-mem8
 (implies
  (stat-validp stat feat)
  (equal
   (read-mem16 addr1 (write-mem8 addr2 val stat feat)
               feat)
   (cond
       ((equal (loghead (feat->xlen feat) addr2)
               (loghead (feat->xlen feat) addr1))
        (cond ((feat-little-endianp feat)
               (logappn 8 (ubyte8-fix val)
                        8
                        (read-mem8 (loghead (feat->xlen feat)
                                            (+ 1 (ifix addr1)))
                                   stat feat)))
              ((feat-big-endianp feat)
               (logappn 8
                        (read-mem8 (loghead (feat->xlen feat)
                                            (+ 1 (ifix addr1)))
                                   stat feat)
                        8 (ubyte8-fix val)))))
       ((equal (loghead (feat->xlen feat) addr2)
               (loghead (feat->xlen feat)
                        (+ 1 (ifix addr1))))
        (cond ((feat-little-endianp feat)
               (logappn 8
                        (read-mem8 (loghead (feat->xlen feat) addr1)
                                   stat feat)
                        8 (ubyte8-fix val)))
              ((feat-big-endianp feat)
               (logappn 8 (ubyte8-fix val)
                        8
                        (read-mem8 (loghead (feat->xlen feat) addr1)
                                   stat feat)))))
       (t (read-mem16 addr1 stat feat))))))

Theorem: read-mem16-of-write-mem16

(defthm read-mem16-of-write-mem16
 (implies
  (stat-validp stat feat)
  (equal
   (read-mem16 addr1 (write-mem16 addr2 val stat feat)
               feat)
   (cond
       ((equal (loghead (feat->xlen feat) addr2)
               (loghead (feat->xlen feat) addr1))
        (ubyte16-fix val))
       ((equal (loghead (feat->xlen feat) addr2)
               (loghead (feat->xlen feat)
                        (1+ (ifix addr1))))
        (cond ((feat-little-endianp feat)
               (logappn 8
                        (read-mem8 (loghead (feat->xlen feat) addr1)
                                   stat feat)
                        8
                        (part-select (ubyte16-fix val)
                                     :low 0
                                     :high 7)))
              ((feat-big-endianp feat)
               (logappn 8
                        (part-select (ubyte16-fix val)
                                     :low 8
                                     :high 15)
                        8
                        (read-mem8 (loghead (feat->xlen feat) addr1)
                                   stat feat)))))
       ((equal (loghead (feat->xlen feat) addr1)
               (loghead (feat->xlen feat)
                        (1+ (ifix addr2))))
        (cond ((feat-little-endianp feat)
               (logappn 8
                        (part-select (ubyte16-fix val)
                                     :low 8
                                     :high 15)
                        8
                        (read-mem8 (loghead (feat->xlen feat)
                                            (1+ (ifix addr1)))
                                   stat feat)))
              ((feat-big-endianp feat)
               (logappn 8
                        (read-mem8 (loghead (feat->xlen feat)
                                            (1+ (ifix addr1)))
                                   stat feat)
                        8
                        (part-select (ubyte16-fix val)
                                     :low 0
                                     :high 7)))))
       (t (read-mem16 addr1 stat feat))))))