Witness Optimizations for SHA256: Dynamic AND/XOR Bit-Width + Spread-Based Binops

[rose2221]

This PR implements two major witness-count optimizations for the R1CS compiler targeting SHA256 circuits:

1. Dynamic Bit-Width for Combined AND/XOR Lookup Table

Introduces a cost model that searches over candidate atomic widths {2, 4, 8} and selects the width minimizing total witness count (table + decomposition + complementary + overhead)
Currently only applies to 8-bit operands; wider operands fall back to w=8

2. Spread Trick for SHA256 Bitwise Operations

Replaces the generic combined AND/XOR table approach for SHA256 with the spread-based technique from Eli Ben-Sasson et al.

Key idea: "spreading" a value by interleaving zeros between bits (0b1011 → 0b01000101) converts bitwise XOR/AND into field addition/multiplication, eliminating per-operation lookup costs

Why ROTR/SHR are free: SHA256 decomposes each 32-bit word into chunks aligned to rotation boundaries. For example, Sigma_0 uses chunks [2, 11, 9, 10] bits exactly matching ROTR2, ROTR13, ROTR22. A rotation is just reading the same chunks in a different order with adjusted coefficients: ROTR2(a) reads chunks starting from index 1 instead of index 0. No new witnesses are allocated — the spread values computed during decomposition are reused with permuted coefficients. Similarly, SHR drops the lowest chunks entirely. The cost of rotation/shift is zero witnesses, zero constraints.

SHA256 operations implemented via spread: sigma_0, sigma_1, Sigma_0, Sigma_1, Ch, Maj, message schedule, compression rounds

• Uses a fixed 8-bit spread table (256 entries, 768 witnesses for LogUp)
• Multi-operand u32 addition with single carry witness per addition

Stats

SHA256 (35 compression calls )

Metric	Before	After (Spread)	Reduction
Constraints	911,769	445,739	-51.1%
Witnesses	1,588,306	1,033,576	-34.9%

SHA256 (1 compression call)

Metric	Before	Spread	Dynamic AND/XOR
Constraints	86,607	14389	44,506
Witnesses	231,044	31680	68,251

Known Soundness Limitation (for M31)

• Carry witness in u32 spread addition is range-checked to [0, 255] sound for bn254, unsound for M31. See Unsound Carry Range Check in Spread-Based u32 Addition for M31 #285
• Collision probability for fused-constraint spread table LogUp. See Track M31 collision probability for fused-constraint spread table LogUp #286

Future Work

Dynamic spread table width: Currently fixed at w=8 (256 entries). A dynamic search over {4, 8, 16} could further reduce witnesses for circuits with fewer SHA256 calls

Shared lookup table: The spread table implicitly range-checks values to [0, 2^w - 1]. Merging with the existing range-check system would eliminate redundant table entries and save additional witnesses.