fix(prover): align CPU sign bit constraints with SIGN template spec (#435)#460
Conversation
Codex Code ReviewNo actionable issues found in this PR diff. Residual risk/testing gap:
|
|
Overall the changes look correct and the logic is sound. Constraint equivalence: The old combined constraint MSB16 vs MSB8 for res_ext_bit: Both extract the same bit (bit 31 of Minor nits (two inline, one here):
|
|
/bench |
Benchmark — fib_iterative_2M (median of 3)Table parallelism: 32 (auto = cores / 3)
Memory GrowthMeasured with
Growth rate: 10813 MB / 1M steps (main: 10949, Δ: -1.2%)
Commit: 5824479 · Baseline: built from main · Runner: self-hosted bench |
|
/bench |
|
/bench 10 |
Aligns the CPU table's sign/extension bit handling with the updated spec (PR #435),
which replaced raw MSB16/MSB8 interactions with the SIGN template.
Changes
Column renames (no index changes):
rv1_sign_bit→rv1_ext_bitarg2_sign_bit→rv2_ext_bit(clarifies it derives from rv2, not arg2)res_sign_bit→res_ext_bitres extension bit: MSB8 → MSB16
MSB8[res[3]]— extracted bit 7 of byte 3 (= bit 31 of res)MSB16[res[2] + 256*res[3]]— extracts MSB of half at bits 16-31 (= bit 31 of res)SIGN(res::DWordHL[1], word_instr)Constraint split (CE57)
(rv1_sign_bit + arg2_sign_bit + res_sign_bit) * (1 - word_instr) = 0(1 - word_instr) * rv1_ext_bit = 0(1 - word_instr) * rv2_ext_bit = 0(1 - word_instr) * res_ext_bit = 0