spec: rework CPU for smaller footprint

[RobinJadoul]

No description provided.

[github-actions]

Codex Code Review

Findings

• High - word-instruction rows can choose an unconstrained outer instruction_length. In spec/src/cpu.toml, the outer DECODE lookup is disabled when word_instr = 1, and the delegation to CPU32 only passes timestamp and pc at spec/src/cpu.toml. But the outer CPU still computes next_pc from its own instruction_length at spec/src/cpu.toml. Since that value is not linked to the CPU32 decode row, a *W instruction proof can advance the PC by an arbitrary byte value while still satisfying the delegated CPU32 execution. This is a VM soundness issue. Pass the decoded instruction length through the CPU32 interaction or keep the outer decode lookup active enough to bind it.

• High - CPU32 uses rv1 instead of rv2 when building arg2. The constraint text says arg2[0] = rv2[:2] + imm[0], but the polynomial subtracts rv1 at spec/src/cpu32.toml. That makes ADDW/SUBW/MULW/DIVW/... with an rs2 operand use rs1 as both operands, and immediate *W instructions use rs1 + imm as the second operand. Replace the rv1 cast with rv2.

• Medium - conditional branches appear to compare against instruction_length instead of rs2. For BRANCH && !JALR, arg2 is set to instruction_length at spec/src/cpu.toml, then the ALU uses rv1, arg2 at spec/src/cpu.toml. For BEQ/BLT-style branches this should compare rs1 with rs2; otherwise branch conditions are evaluated against 2/4 instead of the second register.

No other concrete issues found in the reviewed diff.

[erik-3milabs]

Note to self for follow-up review: have a closer look at the interplay between CPU and DECODE padding.

[RobinJadoul]

Maybe 9b30b9e doesn't belong in this PR exactly, but it seemed simple enough for me to not want to deal with having a stacked PR for it :)

[erik-3milabs]

I believe this sentence is out-of-date now.

Suggested change

Instructions having the `word_instr` flag set are delegated to the `CPU32` chip, which will do its own decoding and execution of the instruction.

[RobinJadoul]

How so? We still have the CPU32 interaction for this

[erik-3milabs]

That is correct. However, this sentence is in the CPU description twice: the new one you provided when you moved the CPU32 interaction up, and this (old) one that does not add any value here.

[erik-3milabs]

That is correct. However, this sentence is in the CPU description twice: the new one you provided when you moved the CPU32 interaction up, and this (old) one that does not add any value here.

[erik-3milabs]

Green light!