allaun/SilverSight
1
0
Fork 0
mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-08-20 13:27:29 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: subleq_falls_through — use omega for ¬(a ≤ 0) from a > 0

Browse source 
simp can't use h : a > 0 to rewrite if a ≤ 0. Added h_not_le by omega.

Build: 3301 jobs, 0 errors
This commit is contained in:
allaun 2026-07-05 06:33:55 -05:00
parent 9cb97c61bd
commit c834b74772
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
formal/SilverSight/Blitter6502OISC.lean
View file

@ -138,7 +138,8 @@ theorem subleq_falls_through (s : M6502State) (inst : SUBLEQ)
(h : s.mem inst.dstB.addr - s.mem inst.srcA.addr > 0) : (h : s.mem inst.dstB.addr - s.mem inst.srcA.addr > 0) :
(execSUBLEQ s inst).pc = s.pc + 3 := by (execSUBLEQ s inst).pc = s.pc + 3 := by
unfold execSUBLEQ unfold execSUBLEQ
simp [h] have h_not_le : ¬ (s.mem inst.dstB.addr - s.mem inst.srcA.addr ≤ 0) := by omega
simp [h_not_le]
/-- Blitter step count: 3 SUBLEQ instructions per byte. -/ /-- Blitter step count: 3 SUBLEQ instructions per byte. -/
theorem blitter_step_count (prog : BlitterProgram) : theorem blitter_step_count (prog : BlitterProgram) :