• 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-instr-of-write-memory-theorems

    Theorems about reads of instructions over writes of memory.

    Reads of instructions are really reads of memory. For now we do not provide any specific theorems, but we plan to. Since instructions consist of 4 bytes, the formulation of these theorems is somewhat complex, since the 4 bytes may be disjoint from the memory writes, or they may partially or completely overlap.