10. Operand Pipeline
The pipelined-fetch cell overlaps only instruction fetch, which is safe because a prefetched instruction never depends on a writeback. Overlapping the operand reads is different: the resident-weight, streamed-operand, and scalar-data reads of one instruction can be launched a cycle early, before the previous instruction has committed, and then the early value is stale if that previous instruction changed what was read. This is a genuine data hazard, and this chapter proves exactly when the early read is safe.
The registers, accumulator, and pointers are small flip-flops read at execute time, so they are never stale. Only the three memory reads are launched early. The theorem below is the data-hazard core: if the intervening instruction does not write what a memory operand depends on, the early read equals the committed read, and the overlapped execution equals the sequential one.
First, how one instruction touches each state component. These projections say
that execDecoded leaves the resident-weight and streamed-operand memories
untouched (no instruction writes them), leaves the scalar-data memory untouched
unless it is a store, leaves the pointers untouched unless the instruction moves
them, and leaves a register untouched unless the instruction targets it.
namespace Honeycomb
theorem exec_weights (d : DecodedInstr) (s : State defaultConfig) :
(execDecoded d s).weights = s.weights := d:DecodedInstrs:State defaultConfig⊢ (execDecoded d s).weights = s.weights
s:State defaultConfigop:CellOprd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weights
s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weights s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weightss:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).weights = s.weights
All goals completed! 🐙
theorem exec_stream (d : DecodedInstr) (s : State defaultConfig) :
(execDecoded d s).stream = s.stream := d:DecodedInstrs:State defaultConfig⊢ (execDecoded d s).stream = s.stream
s:State defaultConfigop:CellOprd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.stream
s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.stream s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.streams:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nat⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).stream = s.stream
All goals completed! 🐙
theorem exec_data_of_ne_st (d : DecodedInstr) (s : State defaultConfig)
(h : d.op ≠ .st) : (execDecoded d s).data = s.data := d:DecodedInstrs:State defaultConfigh:d.op ≠ CellOp.st⊢ (execDecoded d s).data = s.data
s:State defaultConfigop:CellOprd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.data
s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.data s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.datas:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:{ op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.st⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).data = s.data
All goals completed! 🐙
theorem exec_wptr_off (d : DecodedInstr) (s : State defaultConfig)
(hk : d.op ≠ .kmac) (hw : d.op ≠ .setwptr) :
(execDecoded d s).wptr = s.wptr := d:DecodedInstrs:State defaultConfighk:d.op ≠ CellOp.kmachw:d.op ≠ CellOp.setwptr⊢ (execDecoded d s).wptr = s.wptr
s:State defaultConfigop:CellOprd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptr
s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptr s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachw:{ op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setwptr⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).wptr = s.wptr
All goals completed! 🐙
theorem exec_sptr_off (d : DecodedInstr) (s : State defaultConfig)
(hk : d.op ≠ .kmac) (hs : d.op ≠ .setsptr) :
(execDecoded d s).sptr = s.sptr := d:DecodedInstrs:State defaultConfighk:d.op ≠ CellOp.kmachs:d.op ≠ CellOp.setsptr⊢ (execDecoded d s).sptr = s.sptr
s:State defaultConfigop:CellOprd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptr
s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptr s:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:{ op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.kmachs:{ op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.op ≠ CellOp.setsptr⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).sptr = s.sptr
All goals completed! 🐙
def WritesReg (d : DecodedInstr) (r : Reg defaultConfig) : Prop :=
(d.op = .movacc \/ d.op = .li \/ d.op = .ld) /\ d.rd = r
theorem exec_reg_off (d : DecodedInstr) (s : State defaultConfig)
(r : Reg defaultConfig) (h : ¬ WritesReg d r) :
(execDecoded d s).regs r = s.regs r := d:DecodedInstrs:State defaultConfigr:Reg defaultConfigh:¬WritesReg d r⊢ (execDecoded d s).regs r = s.regs r
s:State defaultConfigr:Reg defaultConfigop:CellOprd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs r
s:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs r s:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs rs:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬WritesReg { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } r⊢ (execDecoded { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).regs r = s.regs r
All goals completed! 🐙
all_goals (s:State defaultConfigr:Reg defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:¬rd = rhrd:r = rd⊢ readData s (memIndexOfWord defaultConfig (readReg s ra)) = s.regs rd; All goals completed! 🐙)
end Honeycomb
memOps reads an instruction's three memory operands from a state: the loaded
scalar-data word, the resident weight, and the streamed operand. Indep
captures when the preceding instruction cannot disturb them — a load is safe if
the previous instruction is not a store and does not write the load's address
register; a kernel MAC is safe if the previous instruction does not move the
pointers.
namespace Honeycomb
def memOps (d : DecodedInstr) (s : State defaultConfig) :
Word defaultConfig × Elem defaultConfig × Elem defaultConfig :=
(readData s (memIndexOfWord defaultConfig (readReg s d.ra)),
readWeight s (memIndexOfLocal defaultConfig s.wptr),
readStream s (memIndexOfLocal defaultConfig s.sptr))
def Indep (d1 d2 : DecodedInstr) : Prop :=
match d2.op with
| .ld => d1.op ≠ .st /\ ¬ WritesReg d1 d2.ra
| .kmac => d1.op ≠ .kmac /\ d1.op ≠ .setwptr /\ d1.op ≠ .setsptr
| _ => True
The data-hazard theorem: if d2 is independent of d1, then executing d2
against the committed post-d1 state using operands read early from the
pre-d1 state gives exactly the sequential result. The early read is safe
because independence makes the two reads equal.
theorem safe_overlap (d1 d2 : DecodedInstr) (s : State defaultConfig)
(h : Indep d1 d2) :
execLatched d2 (memOps d2 s).1 (memOps d2 s).2.1 (memOps d2 s).2.2
(execDecoded d1 s)
= execDecoded d2 (execDecoded d1 s) := d1:DecodedInstrd2:DecodedInstrs:State defaultConfigh:Indep d1 d2⊢ execLatched d2 (memOps d2 s).fst (memOps d2 s).snd.fst (memOps d2 s).snd.snd (execDecoded d1 s) =
execDecoded d2 (execDecoded d1 s)
d1:DecodedInstrd2:DecodedInstrs:State defaultConfigh:Indep d1 d2⊢ execLatched d2 (memOps d2 s).fst (memOps d2 s).snd.fst (memOps d2 s).snd.snd (execDecoded d1 s) =
execLatched d2 (readData (execDecoded d1 s) (memIndexOfWord defaultConfig (readReg (execDecoded d1 s) d2.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)
obtain ⟨op, rd, ra, rb, imm, addr⟩ := d2 d1:DecodedInstrs:State defaultConfigop:CellOprd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := op, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)
cases op mac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)kmac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)clracc d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s)
{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)movacc d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s)
{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)li d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)ld d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)st d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)setwptr d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s)
{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)setsptr d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s)
{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)blz d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)halt d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s) <;> mac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.mac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)kmac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)clracc d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s)
{ op := CellOp.clracc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)movacc d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s)
{ op := CellOp.movacc, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)li d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.li, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)ld d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)st d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.st, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)setwptr d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s)
{ op := CellOp.setwptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)setsptr d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s)
{ op := CellOp.setsptr, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)blz d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd (execDecoded d1 s) =
execLatched { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.blz, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)halt d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ execLatched { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(memOps { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).fst
(memOps { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.fst
(memOps { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr } s).snd.snd
(execDecoded d1 s) =
execLatched { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }
(readData (execDecoded d1 s)
(memIndexOfWord defaultConfig
(readReg (execDecoded d1 s) { op := CellOp.halt, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }.ra)))
(readWeight (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(readStream (execDecoded d1 s) (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr)) (execDecoded d1 s)
simp only [memOps, execLatched, readWeight, readStream, readData, readReg] All goals completed! 🐙 <;> kmac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc (s.weights (memIndexOfLocal defaultConfig s.wptr))
(s.stream (memIndexOfLocal defaultConfig s.sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc
((execDecoded d1 s).weights (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
((execDecoded d1 s).stream (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc)ld d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ retire
(setRegs (execDecoded d1 s) (updReg (execDecoded d1 s).regs rd (s.data (memIndexOfWord defaultConfig (s.regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setRegs (execDecoded d1 s)
(updReg (execDecoded d1 s).regs rd
((execDecoded d1 s).data (memIndexOfWord defaultConfig ((execDecoded d1 s).regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc)
(try rfl ld d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ retire
(setRegs (execDecoded d1 s) (updReg (execDecoded d1 s).regs rd (s.data (memIndexOfWord defaultConfig (s.regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setRegs (execDecoded d1 s)
(updReg (execDecoded d1 s).regs rd
((execDecoded d1 s).data (memIndexOfWord defaultConfig ((execDecoded d1 s).regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc))
· kmac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.kmac, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc (s.weights (memIndexOfLocal defaultConfig s.wptr))
(s.stream (memIndexOfLocal defaultConfig s.sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc
((execDecoded d1 s).weights (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
((execDecoded d1 s).stream (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) simp only [Indep] at h kmac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:d1.op ≠ CellOp.kmac ∧ d1.op ≠ CellOp.setwptr ∧ d1.op ≠ CellOp.setsptr⊢ retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc (s.weights (memIndexOfLocal defaultConfig s.wptr))
(s.stream (memIndexOfLocal defaultConfig s.sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc
((execDecoded d1 s).weights (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
((execDecoded d1 s).stream (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc)
obtain ⟨hk, hw, hs⟩ := h kmac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:d1.op ≠ CellOp.kmachw:d1.op ≠ CellOp.setwptrhs:d1.op ≠ CellOp.setsptr⊢ retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc (s.weights (memIndexOfLocal defaultConfig s.wptr))
(s.stream (memIndexOfLocal defaultConfig s.sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc
((execDecoded d1 s).weights (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
((execDecoded d1 s).stream (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc)
rw [exec_weights d1 s, kmac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:d1.op ≠ CellOp.kmachw:d1.op ≠ CellOp.setwptrhs:d1.op ≠ CellOp.setsptr⊢ retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc (s.weights (memIndexOfLocal defaultConfig s.wptr))
(s.stream (memIndexOfLocal defaultConfig s.sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc
(s.weights (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
((execDecoded d1 s).stream (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) exec_stream d1 s, kmac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:d1.op ≠ CellOp.kmachw:d1.op ≠ CellOp.setwptrhs:d1.op ≠ CellOp.setsptr⊢ retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc (s.weights (memIndexOfLocal defaultConfig s.wptr))
(s.stream (memIndexOfLocal defaultConfig s.sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc
(s.weights (memIndexOfLocal defaultConfig (execDecoded d1 s).wptr))
(s.stream (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr))))
(nextLocal defaultConfig (execDecoded d1 s).wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) exec_wptr_off d1 s hk hw, kmac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:d1.op ≠ CellOp.kmachw:d1.op ≠ CellOp.setwptrhs:d1.op ≠ CellOp.setsptr⊢ retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc (s.weights (memIndexOfLocal defaultConfig s.wptr))
(s.stream (memIndexOfLocal defaultConfig s.sptr))))
(nextLocal defaultConfig s.wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc (s.weights (memIndexOfLocal defaultConfig s.wptr))
(s.stream (memIndexOfLocal defaultConfig (execDecoded d1 s).sptr))))
(nextLocal defaultConfig s.wptr) (nextLocal defaultConfig (execDecoded d1 s).sptr))
(nextPC defaultConfig (execDecoded d1 s).pc)
exec_sptr_off d1 s hk hs kmac d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathk:d1.op ≠ CellOp.kmachw:d1.op ≠ CellOp.setwptrhs:d1.op ≠ CellOp.setsptr⊢ retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc (s.weights (memIndexOfLocal defaultConfig s.wptr))
(s.stream (memIndexOfLocal defaultConfig s.sptr))))
(nextLocal defaultConfig s.wptr) (nextLocal defaultConfig s.sptr))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setPtrs
(setAcc (execDecoded d1 s)
(accAddProduct defaultConfig (execDecoded d1 s).acc (s.weights (memIndexOfLocal defaultConfig s.wptr))
(s.stream (memIndexOfLocal defaultConfig s.sptr))))
(nextLocal defaultConfig s.wptr) (nextLocal defaultConfig s.sptr))
(nextPC defaultConfig (execDecoded d1 s).pc)] All goals completed! 🐙
· ld d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:Indep d1 { op := CellOp.ld, rd := rd, ra := ra, rb := rb, imm := imm, addr := addr }⊢ retire
(setRegs (execDecoded d1 s) (updReg (execDecoded d1 s).regs rd (s.data (memIndexOfWord defaultConfig (s.regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setRegs (execDecoded d1 s)
(updReg (execDecoded d1 s).regs rd
((execDecoded d1 s).data (memIndexOfWord defaultConfig ((execDecoded d1 s).regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc) simp only [Indep] at h ld d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nath:d1.op ≠ CellOp.st ∧ ¬WritesReg d1 ra⊢ retire
(setRegs (execDecoded d1 s) (updReg (execDecoded d1 s).regs rd (s.data (memIndexOfWord defaultConfig (s.regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setRegs (execDecoded d1 s)
(updReg (execDecoded d1 s).regs rd
((execDecoded d1 s).data (memIndexOfWord defaultConfig ((execDecoded d1 s).regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc)
obtain ⟨hst, hreg⟩ := h ld d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathst:d1.op ≠ CellOp.sthreg:¬WritesReg d1 ra⊢ retire
(setRegs (execDecoded d1 s) (updReg (execDecoded d1 s).regs rd (s.data (memIndexOfWord defaultConfig (s.regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setRegs (execDecoded d1 s)
(updReg (execDecoded d1 s).regs rd
((execDecoded d1 s).data (memIndexOfWord defaultConfig ((execDecoded d1 s).regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc)
rw [exec_data_of_ne_st d1 s hst, ld d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathst:d1.op ≠ CellOp.sthreg:¬WritesReg d1 ra⊢ retire
(setRegs (execDecoded d1 s) (updReg (execDecoded d1 s).regs rd (s.data (memIndexOfWord defaultConfig (s.regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setRegs (execDecoded d1 s)
(updReg (execDecoded d1 s).regs rd (s.data (memIndexOfWord defaultConfig ((execDecoded d1 s).regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc) exec_reg_off d1 s ra hreg ld d1:DecodedInstrs:State defaultConfigrd:Reg defaultConfigra:Reg defaultConfigrb:Reg defaultConfigimm:Intaddr:Nathst:d1.op ≠ CellOp.sthreg:¬WritesReg d1 ra⊢ retire
(setRegs (execDecoded d1 s) (updReg (execDecoded d1 s).regs rd (s.data (memIndexOfWord defaultConfig (s.regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc) =
retire
(setRegs (execDecoded d1 s) (updReg (execDecoded d1 s).regs rd (s.data (memIndexOfWord defaultConfig (s.regs ra)))))
(nextPC defaultConfig (execDecoded d1 s).pc)] All goals completed! 🐙
This is the interlock. A pipeline may read d2's operands early only when the
interlock reports independence; otherwise it stalls and reads them late, from the
committed state. Either way the commit equals the sequential step: the late read
is the direct execLatched identity, and the early read is safe by the theorem
above. So an interlocked operand pipeline commits the sequential trace exactly,
with a stall bubble only where a genuine dependency forces it.
theorem interlock_commit (d1 d2 : DecodedInstr) (s : State defaultConfig)
(early : Bool) (h : early = true -> Indep d1 d2) :
(if early then
execLatched d2 (memOps d2 s).1 (memOps d2 s).2.1 (memOps d2 s).2.2
(execDecoded d1 s)
else
execLatched d2 (memOps d2 (execDecoded d1 s)).1
(memOps d2 (execDecoded d1 s)).2.1 (memOps d2 (execDecoded d1 s)).2.2
(execDecoded d1 s))
= execDecoded d2 (execDecoded d1 s) := by d1:DecodedInstrd2:DecodedInstrs:State defaultConfigearly:Boolh:early = true → Indep d1 d2⊢ (if early = true then execLatched d2 (memOps d2 s).fst (memOps d2 s).snd.fst (memOps d2 s).snd.snd (execDecoded d1 s)
else
execLatched d2 (memOps d2 (execDecoded d1 s)).fst (memOps d2 (execDecoded d1 s)).snd.fst
(memOps d2 (execDecoded d1 s)).snd.snd (execDecoded d1 s)) =
execDecoded d2 (execDecoded d1 s)
by_cases he : early = true pos d1:DecodedInstrd2:DecodedInstrs:State defaultConfigearly:Boolh:early = true → Indep d1 d2he:early = true⊢ (if early = true then execLatched d2 (memOps d2 s).fst (memOps d2 s).snd.fst (memOps d2 s).snd.snd (execDecoded d1 s)
else
execLatched d2 (memOps d2 (execDecoded d1 s)).fst (memOps d2 (execDecoded d1 s)).snd.fst
(memOps d2 (execDecoded d1 s)).snd.snd (execDecoded d1 s)) =
execDecoded d2 (execDecoded d1 s)neg d1:DecodedInstrd2:DecodedInstrs:State defaultConfigearly:Boolh:early = true → Indep d1 d2he:¬early = true⊢ (if early = true then execLatched d2 (memOps d2 s).fst (memOps d2 s).snd.fst (memOps d2 s).snd.snd (execDecoded d1 s)
else
execLatched d2 (memOps d2 (execDecoded d1 s)).fst (memOps d2 (execDecoded d1 s)).snd.fst
(memOps d2 (execDecoded d1 s)).snd.snd (execDecoded d1 s)) =
execDecoded d2 (execDecoded d1 s)
· pos d1:DecodedInstrd2:DecodedInstrs:State defaultConfigearly:Boolh:early = true → Indep d1 d2he:early = true⊢ (if early = true then execLatched d2 (memOps d2 s).fst (memOps d2 s).snd.fst (memOps d2 s).snd.snd (execDecoded d1 s)
else
execLatched d2 (memOps d2 (execDecoded d1 s)).fst (memOps d2 (execDecoded d1 s)).snd.fst
(memOps d2 (execDecoded d1 s)).snd.snd (execDecoded d1 s)) =
execDecoded d2 (execDecoded d1 s) rw [if_pos he pos d1:DecodedInstrd2:DecodedInstrs:State defaultConfigearly:Boolh:early = true → Indep d1 d2he:early = true⊢ execLatched d2 (memOps d2 s).fst (memOps d2 s).snd.fst (memOps d2 s).snd.snd (execDecoded d1 s) =
execDecoded d2 (execDecoded d1 s)] pos d1:DecodedInstrd2:DecodedInstrs:State defaultConfigearly:Boolh:early = true → Indep d1 d2he:early = true⊢ execLatched d2 (memOps d2 s).fst (memOps d2 s).snd.fst (memOps d2 s).snd.snd (execDecoded d1 s) =
execDecoded d2 (execDecoded d1 s)
exact safe_overlap d1 d2 s (h he) All goals completed! 🐙
· neg d1:DecodedInstrd2:DecodedInstrs:State defaultConfigearly:Boolh:early = true → Indep d1 d2he:¬early = true⊢ (if early = true then execLatched d2 (memOps d2 s).fst (memOps d2 s).snd.fst (memOps d2 s).snd.snd (execDecoded d1 s)
else
execLatched d2 (memOps d2 (execDecoded d1 s)).fst (memOps d2 (execDecoded d1 s)).snd.fst
(memOps d2 (execDecoded d1 s)).snd.snd (execDecoded d1 s)) =
execDecoded d2 (execDecoded d1 s) rw [if_neg he neg d1:DecodedInstrd2:DecodedInstrs:State defaultConfigearly:Boolh:early = true → Indep d1 d2he:¬early = true⊢ execLatched d2 (memOps d2 (execDecoded d1 s)).fst (memOps d2 (execDecoded d1 s)).snd.fst
(memOps d2 (execDecoded d1 s)).snd.snd (execDecoded d1 s) =
execDecoded d2 (execDecoded d1 s)] neg d1:DecodedInstrd2:DecodedInstrs:State defaultConfigearly:Boolh:early = true → Indep d1 d2he:¬early = true⊢ execLatched d2 (memOps d2 (execDecoded d1 s)).fst (memOps d2 (execDecoded d1 s)).snd.fst
(memOps d2 (execDecoded d1 s)).snd.snd (execDecoded d1 s) =
execDecoded d2 (execDecoded d1 s)
exact execLatched_eq d2 (execDecoded d1 s) All goals completed! 🐙
end Honeycomb
The interlock as written is conservative: it stalls a load behind any store and a kernel MAC behind any pointer move, whether or not the addresses actually collide. That is enough for correctness and for overlapping the common independent cases — a load after an unrelated arithmetic instruction, or a MAC after a register update. The kernel's own hot path, a run of dependent MACs whose pointers chain, is the case this interlock always stalls; its throughput comes instead from the scheduling chapter's latency pipeline, whose conservation law already commits the same accumulator at full rate. Refining the interlock with address disambiguation, or forwarding the pointer chain, would let the two meet; both build on the independence theorem proved here.