• 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
          • Specialized-features
          • Rv64im
          • Rv32im
          • Specialized-states
            • States32i
              • Stat32i
              • Memory32i
              • Xregs32i
              • Stat32i-iso
              • Read32i-xreg-unsigned
              • Stat-rv32i-p
              • Read32i-xreg-signed{3}
              • Read32i-xreg-unsigned{2}
              • Read32i-xreg-signed{2}
              • Read32i-xreg-unsigned{0}
              • Read32i-xreg-signed
              • Read32i-xreg-unsigned{1}
              • Read32i-xreg-signed{1}
              • Read32i-xreg-signed{0}
              • Stat32i-from-stat
              • Stat-from-stat32i
              • Read-xreg-unsigned-to-read32i-xreg-unsigned
            • States64i
            • States64e
            • States32e
        • Optimized
      • Ethereum
      • Taspi
      • Bitcoin
      • Zcash
      • Des
      • X86isa
      • Sha-2
      • Yul
      • 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
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Specialized-states

States32i

Specialized states for features with the RV32I base.

We define a recognizer for the valid states for the RV32I base. We introduce a fixtype that is isomorphic to that recognizer. We specialize the operations on states to operate on that fixtype. This is work in progress.

Subtopics

Stat32i
Fixtype of states for the RV32I base.
Memory32i
Fixtype of memories for the RV32I base.
Xregs32i
Fixtype of the x registers for the RV32I base.
Stat32i-iso
Isomorphism between stat-rv32i-p and stat32i.
Read32i-xreg-unsigned
Simplify read32i-xreg-unsigned{2} after the isomorphic state transformation.
Stat-rv32i-p
Recognizer of states with base RV32I.
Read32i-xreg-signed{3}
Simplify the body of read32i-xreg-signed{2} to call read32i-xreg-unsigned.
Read32i-xreg-unsigned{2}
Refine read32i-xreg-unsigned{1} to use the isomorphic states stat32i.
Read32i-xreg-signed{2}
Refine read32i-xreg-signed{1} to use the isomorphic states stat32i.
Read32i-xreg-unsigned{0}
Partially evaluate read-xreg-unsigned for the RV32I base.
Read32i-xreg-signed
Simplify the guard of read32i-xreg-signed{3} to eliminate the isomorphic conversion.
Read32i-xreg-unsigned{1}
Simplify read32i-xreg-unsigned{0} after partial evaluation.
Read32i-xreg-signed{1}
Simplify read32i-xreg-signed{0} after partial evaluation.
Read32i-xreg-signed{0}
Partially evaluate read-xreg-unsigned for the RV32I base.
Stat32i-from-stat
Convert from stat-rv32i-p to stat32i.
Stat-from-stat32i
Convert from stat32i to stat-rv32i-p.
Read-xreg-unsigned-to-read32i-xreg-unsigned
Rewriting of read-xreg-unsigned to read32i-xreg-unsigned.