|
|
|---|
|
|
|
|---|
Theorems about reads of program counter over writes of program counter.
The writes of program counter include not only write-pc but also inc4-pc.
The first theorem is enabled by default because the right side seems clearly always simpler. The second theorem is disabled by default because the right side still involves a call of read-pc.
Theorem:
(defthm read-pc-of-write-pc (equal (read-pc (write-pc pc stat feat) feat) (loghead (feat->xlen feat) (nfix pc))))
Theorem:
(defthm read-pc-of-inc4-pc (equal (read-pc (inc4-pc stat feat) feat) (loghead (feat->xlen feat) (+ 4 (read-pc stat feat)))))