feat(vm): add constrained SHA-256 compression precompile

[diegokingston]

No description provided.

[github-actions]

Benchmark Results for modified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head ecsm	2.6 ± 0.1	2.5	2.7	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head hashmap	112.8 ± 1.7	110.8	116.4	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head keccak	130.1 ± 2.3	126.4	133.0	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
head syscall_commit	86.1 ± 1.0	84.8	87.2	1.00

[jotabulacios]

/ai-review

[github-actions]

Codex Code Review

• Medium — SHA-256 traces bypass disk spilling. trace_builder.rs:3654 generates all five tables in RAM even under StorageMode::Disk, and the subsequent spill block omits them. At 16,384 compression calls, ROTXOR alone occupies about 6.2 GiB, retained alongside the other tables. Large SHA-heavy runs can therefore exhaust RAM despite automatic disk-mode selection. Spill each new trace immediately after generation in disk mode.

Static review only; no builds or tests run.

[github-actions]

AI Review

PR #990 · 42 changed files

Findings

No non-rejected structured findings were reported.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings
glm	openrouter/z-ai/glm-5.2	general	success	0
kimi	openrouter/moonshotai/kimi-k2.7-code	general	success	3
minimax	minimax/MiniMax-M3	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0
moonmath	zro/minimax-m3	general	error: opencode failed (provider/auth/runtime error) and no findings were submitted	0
nemotron	openrouter/nvidia/nemotron-3-ultra-550b-a55b	general	success	6

Verification Lanes

Lane	Model	Status	Confirmed	Rejected	Uncertain
deepseek-verifier	openrouter/deepseek/deepseek-v4-pro	success	0	9	0

Native Codex and Claude reviews run separately and post their own comments. They are not included in this structured provenance report.

Discarded candidates (9) — rejected by the verifier

• SHA-256 state read timestamp not tracked, causing old_timestamp=0 instead of syscall timestamp (prover/src/tables/trace_builder.rs:4933, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The first loop's memory.read_byte().0 only reads byte values to populate the sha256::Operation struct (which stores only [u8; 32] and [u8; 64] — no timestamps). It does not create MEMW operations and is intentionally read-only. The second loop's memory.read_bytes(addr, 8) correctly returns both values and timestamps from MemoryState. If the state bytes were written by a prior instruction, old_ts reflects that write timestamp; if never written, old_ts=0 matches the initial (value, 0) cell from from_image. The Keccak path follows the same pattern (read_byte with .0 at line 1490, then read_byte with both parts for the MEMW operation).
• SHA-256 state write recorded as read instead of write in MEMW operations (prover/src/tables/trace_builder.rs:4956, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The is_read=true flag on the state MemwOperation matches how Keccak handles combined read+write (collect_keccak_memw_ops line 1499: MemwOperation::new(false, lane_addr, value_bytes, ts, 8, true)). The comment at lines 1475-1477 explicitly explains: 'single combined read+write MEMW per lane... The MEMW table sees: old=input_state, value=output_state, is_read=true.' SHA-256 follows the same pattern. The memory.write_bytes call at line 4963 updates MemoryState internally, and the core table's bus_interactions (lines 129-137) sends both old (H) and new (OUT) bytes through the MEMW token — the bus carries both, so the table correctly models the read-modify-write.
• Duplicate MEMW read operations for SHA-256 message input (prover/src/tables/trace_builder.rs:4934, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The first loop at lines 4933-4934 reads byte values from MemoryState only to assemble the sha256::Operation struct. It does NOT create MemwOperation entries. The second loop at lines 4954-4963 is where the actual MEMW operations are created. There are no duplicate MEMW rows — the first loop produces no MEMW operations at all. This is identical to how Keccak's collect_keccak_memw_ops first reads values for the state array then creates a single MEMW per lane.
• SHA-256 state read at wrong timestamp (t+1 instead of t) (prover/src/tables/trace_builder.rs:4956, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The comment at line 4923 explicitly states the design: 'SHA compression memory accesses: registers at T, message at T, then state read/write at T+1.' The sha256 core table's bus_interactions (lines 129-137) uses ts=2 (= columns 2,3 = t+1) for the state MEMW interactions. The generate function stores t+1 in columns 2,3 (lines 52-53). The single MEMW row at t+1 carries old=H (pre-compression), new=OUT (post-compression) — this is an intentional single-row representation of a read-modify-write, not a bug. Pushing state to t+1 avoids timestamp conflicts between message reads (at t) and state accesses when operands overlap.
• Missing SHA-256 cycle counting in flamegraph execution path (bin/cli/src/main.rs:411, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — The flamegraph execution path never tallied ANY accelerator counts (Keccak, ECSM, or SHA-256). The comment at lines 411-414 is explicit: 'Accelerator invocation counts, tallied only in the plain streaming path below (the flamegraph path drives execution inside the executor and does not expose per-log data).' Before this PR, accel_counts was Option<(u64, u64)> and the flamegraph path set it to None for both Keccak and ECSM too. The PR only extends the non-flamegraph path — the pre-existing flamegraph limitation affects all accelerators equally and is not introduced here.
• SHA256 ecall does not reject low 32-bit limb address overflow (executor/src/vm/instruction/execution.rs:501, found by kimi:openrouter/moonshotai/kimi-k2.7-code) — The addr_limb_ok check used by ECSM (lines 560-562) and HINT (line 612) is needed because those tables send raw [lo32, hi32] address pairs to the memory bus where the offset is added to lo32 alone. SHA-256 uses a different approach: 14 explicit pointer columns (PTR + 4*i) with full 64-bit arithmetic in the Constraints (lines 192-218) — the INV_SHIFT_32 carry propagation handles limb boundaries. The u64 checked_add checks are sufficient because the AIR carries the overflow across the 32-bit boundary through the constraint system. The docs in sha256.md say 'Overflowing address ranges are rejected before writing' which refers to u64 overflow, exactly what checked_add catches.
• SHA256 core table lacks explicit byte-range constraints on state/message bytes (prover/src/tables/sha256.rs:171, found by kimi:openrouter/moonshotai/kimi-k2.7-code) — While the core table's Constraints don't locally check_bits on H (columns 60-91) or M (columns 92-155), these columns are sent to the MEMW bus via the mem() function (lines 125-137). The MEMW table's internal Memory consistency bus enforces byte range-checking on received byte values. OUT columns ARE locally sent on the AreBytes bus (lines 141-147). M columns are additionally constrained through the schedule table's word decomposition with bit constraints (sha256_schedule.rs check_bits at line 76). The cross-table approach ensures overall soundness — this is a design choice consistent with how other tables (e.g., KECCAK core) rely on external byte checks for some columns.
• SHA256 core emits 48 spurious AreBytes lookups (prover/src/tables/sha256.rs:268, found by kimi:openrouter/moonshotai/kimi-k2.7-code) — The 48 AreBytes[i, 0] lookups (lines 270-272) correspond exactly to the schedule table's AreBytes sends (sha256_schedule.rs lines 64-68: send(BusId::AreBytes, MU, vec![col(44), constant(0)])). The schedule table has 48 rows per operation (indices 16..63), each setting col(44) = i - 16 = 0..47. The schedule sends AreBytes[0,0] through AreBytes[47,0] with multiplicity 1 each. The core table's bitwise_ops adds the matching 48 entries to the BITWISE histogram so the BITWISE table can receive these sends. They are not spurious — they are the receiver-side multiplicity for the schedule's index-16 byte range checks.
• ROTXOR constraint uses xy = x + y - 2xy for XOR but variable naming is confusing (prover/src/tables/sha256_rotxor.rs:85, found by nemotron:openrouter/nvidia/nemotron-3-ultra-550b-a55b) — This is a purely cosmetic naming observation. The variable xy at line 85 holds the column value constrained to equal x XOR y (since for bits, x + y - 2xy = XOR). While the name is slightly misleading (suggests multiplication), the constraint algebra is correct and there is no functional issue. The code is clear in context with the preceding comment about XOR. This does not warrant a finding.

Raw lane outputs, candidates, final issues, and model metrics are uploaded as workflow artifacts.

[github-actions]

Benchmark Results for unmodified programs 🚀

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base binary_search	37.6 ± 1.5	35.9	40.9	1.04 ± 0.05
head binary_search	36.1 ± 0.8	35.1	37.9	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base bitwise_ops	36.4 ± 1.6	35.0	40.1	1.03 ± 0.05
head bitwise_ops	35.3 ± 0.6	34.8	36.7	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base fibonacci_26	38.0 ± 0.6	36.9	38.7	1.00
head fibonacci_26	39.9 ± 1.3	38.3	41.7	1.05 ± 0.04

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base matrix_multiply	37.8 ± 1.0	36.4	39.7	1.00
head matrix_multiply	38.7 ± 0.8	37.6	40.2	1.03 ± 0.03

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base modular_exp	35.9 ± 0.5	35.1	36.5	1.00
head modular_exp	40.8 ± 8.9	35.1	62.3	1.14 ± 0.25

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base quicksort	39.5 ± 0.5	38.7	40.5	1.03 ± 0.02
head quicksort	38.3 ± 0.7	37.5	39.2	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sieve	39.3 ± 1.0	37.6	40.7	1.01 ± 0.03
head sieve	39.1 ± 0.5	38.3	39.7	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sum_array	45.6 ± 0.6	44.5	46.4	1.01 ± 0.02
head sum_array	45.3 ± 0.7	44.5	46.5	1.00