DF5778: ==== T4 generic-slot dispatch (slot 1 HPD1) ====
DF5778: T4 set(HPD1)=1 reads=2 writes=2
DF5778: T4 ack:  r[0]=0xdead0002 w[0]=0xdead0002 wval[0]=0xa5a5a5b5 (expect r/w 0xDEAD0002, 0xA5A5A5B5)
DF5778: T4 set:  r[1]=0xdead0001 w[1]=0xdead0001 wval[1]=0xa5a5a5a7 (expect r/w 0xDEAD0001, 0xA5A5A5A7)
DF5778: T4 PASS (generic RMW uses exactly the in-table synthetic regs)
DF5778: ==== all proofs complete ====