		Search-engine friendly clone of the ACL2 documentation.

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.
Stat-rv32i-p: Recognizer of states with base RV32I.
Read32i-xreg-unsigned{2}: Refine read32i-xreg-unsigned{1} to use the isomorphic states stat32i.
Read32i-xreg-unsigned{0}: Partially evaluate read-xreg-unsigned for the RV32I base.
Read32i-xreg-unsigned{1}: Simplify read32i-xreg-unsigned{0} after partial evaluation.
Stat32i-from-stat: Convert from stat-rv32i-p to stat32i.
Stat-from-stat32i: Convert from stat32i to stat-rv32i-p.