Feat/shrink cpu byte alu#644
Conversation
…layout, and document the deviations
|
/bench 5 |
Benchmark — fib_iterative_8M (median of 3)Table parallelism: auto (cores / 3)
Commit: 57bd2b0 · Baseline: cached · Runner: self-hosted bench |
Codex Code ReviewFound one issue. High - CPU32 padding rows can emit disconnected bus operations prover/src/tables/cpu32.rs uses This can inject extra register reads/writes through MEMW without a corresponding executed Verification note: I tried to run the focused prover tests, but the container’s Rust toolchain failed before build because |
Code Review — Feat/shrink-cpu-byte-alu (#644)This is a significant, well-structured CPU table rework. The reduction from ~76 to ~39 columns, the unified ALU/MEMORY buses, and the delegation of Constraint CompletenessThe overall constraint set is correct and complete for valid traces:
Issues Found
Inline comments posted for each issue. Minor Notes
|
|
/bench |
|
/claude |
|
/bench |
cade3ff to
6eb329b
Compare
main advanced by PR #652 (soundness: underconstrained chips), which added IS_HALFWORD range-checks and wired LT/MUL transition constraints on the same chips this branch reworks. Conflicts resolved: - test_utils.rs: union of imports (store + BusId). - tables/shift.rs collect_bitwise_from_shift: keep BOTH #644's shift-amount range-checks AND #652's input-half (VM-3) checks. The merged bus_interactions carries both sender sets, so both lookup sets are required for the IsHalfword bus to balance. - tests/mul_tests.rs: bus-interaction count 24 (#652) with the ALU receiver label (#644); wiring-test constraint count 6 -> 8, because this branch adds the two SignedIsBit(LHS/RHS) constraints that #652's count predated. Verified: cargo build; mul/shift/dvrm/lt unit + bus-count + wiring + busless soundness tests pass; end-to-end prove+verify passes for shift_8, sllw, srli_one_zero, mul_8.
Merge main into shrink-cpu-byte-alu (resolve #652 conflicts)
|
/bench |
This PR implements the CPU rework specified in #624.
The CPU table is reduced from ~76 to ~39 columns by moving word
instructions to a dedicated table and collapsing the per-chip ALU/memory
buses into two shared buses.
Summary
Dense
packed_decode.The per-opcode one-hot ALU selectors and the
*_ext_bit/arg1columns were removed.
Each CPU row now carries a single
packed_decodefield containingflags, register indices, and the
alu_flags/mem_flagsbytes. Thisvalue is checked against the
DECODEtable.Unified buses.
The per-chip
Lt/Mul/Dvrm/Shiftbuses, together with theload/store path, were collapsed into two shared buses:
ALU[out; in1, in2, flags]MEMORY[out; timestamp, address, value, flags]The CPU now dispatches every arithmetic, comparison, and shift operation
through
ALU, and every memory operation throughMEMORY.BYTE_ALUlookup.Bitwise
AND/OR/XORnow use a singleBYTE_ALU[opsel, X, Y] -> outlookup served by theBITWISEtable.Word instructions delegated to
CPU32.*Winstructions are delegated to a newCPU32table, which has itsown decode and 32-bit execution logic.
In the main CPU table, these rows now only delegate execution, advance
the PC, and send the corresponding
CPU32lookup.New chips.
Added the following chips:
CPU32: handles word instructions.EQ: handlesBEQ/BNE.BYTEWISE: handlesAND/OR/XORthroughBYTE_ALU.STORE: split fromMEMW;MEMORYnow dispatches betweenLOADandSTORE.