RV32I in ACL2

We present a simple ACL2 simulator for the RISC-V 32-bit base instruction set architecture, written in the operational semantics style.Like many other ISA models, our RISC-V state object is a singlethreaded object and we prove read-over-write, write-over-write, writing-the-read, and state wellformedness theorems.Unlike some other models, we separate the instruction decoding functions from their semantic counterparts.Accordingly, we verify encoding / decoding functions for each RV32I instruction, the proofs for which are entirely automatic.