SHA-256 relation: witness synthesis and sparse M/A construction

[wu-s-john]

S1 - SHA-256 relation: witness synthesis and sparse M/A construction

Implement the executable SHA-256 compression relation described in
docs/sha256-f2z-note.

This issue owns:

1. Native SHA-256 witness synthesis.
2. The public binary map M_mix that derives virtual XOR values.
3. The public sparse integer matrix A_x that checks the SHA-256 word
   equations.

The completed implementation must produce an exactly satisfied relation:

z = M_mix · f                    over F_2
M = [I; M_mix]
h = (1, f, z)
A_x · h = 0                     over Z

This issue stops at constructing and checking that relation. It does not commit
the witness or construct a PIOP/proof.

Source of truth

Use the SHA-256 construction in docs/sha256-f2z-note, particularly:

• Section 1, "The SHA-256 constraint system"
• Figure 3, the sparse block structure of M_mix
• Table 2, the integer row families
• Table 3, the logical matrix dimensions
• Section 2.1, the logical witness ordering

The document is normative for the mathematical relation. Prototype code may be
used as a reference, but the relation and index maps should be re-derived from
the document.

Relation variant

Implement the 206-row compression-core relation first.

The public instance consists of:

• one 512-bit message block, represented as 16 SHA-256 words
• the incoming chaining state H_in
• the terminal state S_65

The relation does not include the final feed-forward additions. The
feed-forward and digest-only variants have different witness dimensions and
are out of scope for this issue.

Round constants K_1, ..., K_64 are fixed parameters, not witness values.

1. Typed relation and index layout

Add a shared SHA-256 relation crate, tentatively:

crates/sha256-relation

It should be usable by both the prover and verifier without depending on either
crate.

Define typed identifiers for at least:

• committed witness bits
• virtual witness bits
• complete h coordinates
• SHA words and trace positions
• constraint families and row identifiers

There must be one authoritative implementation of each index mapping.
Witness synthesis, M_mix, A_x, the prover, and the verifier must not carry
independent copies of the layout arithmetic.

The logical relation layout must remain separate from the later physical
commitment layout, padding, and transpose.

2. Native witness synthesis

For one compression, synthesize the committed witness

f = (
    a[-2..=64],
    e[-2..=64],
    W[1..=64],
    bin3(mu_a[1..=64]),
    bin3(mu_e[1..=64]),
    bin2(mu_W[17..=64])
)

All word bits and carry bits are stored LSB first. Carry encodings are
round-major.

The six prologue words are initialized from the incoming state:

a[1]  = H_in[0]
a[0]  = H_in[1]
a[-1] = H_in[2]
a[-2] = H_in[3]

e[1]  = H_in[4]
e[0]  = H_in[5]
e[-1] = H_in[6]
e[-2] = H_in[7]

The synthesizer may retain a[65] and e[65] internally to construct and
check S_65, but they are public values and are not included in the committed
compression-core witness.

Schedule carries

For t = 17..=64, compute the full integer sum

s_W =
    W[t - 16]
  + sigma0(W[t - 15])
  + W[t - 7]
  + sigma1(W[t - 2])

and define

W[t]    = s_W mod 2^32
mu_W[t] = floor(s_W / 2^32)

Round carries

For each t = 1..=64, compute the full integer sums

s_a =
    e[t - 3]
  + Sigma1(e[t])
  + Ch(e[t], e[t - 1], e[t - 2])
  + K[t]
  + W[t]
  + Sigma0(a[t])
  + Maj(a[t], a[t - 1], a[t - 2])

s_e =
    a[t - 3]
  + e[t - 3]
  + Sigma1(e[t])
  + Ch(e[t], e[t - 1], e[t - 2])
  + K[t]
  + W[t]

and define

a[t + 1] = s_a mod 2^32
mu_a[t]  = floor(s_a / 2^32)

e[t + 1] = s_e mod 2^32
mu_e[t]  = floor(s_e / 2^32)

Use sufficiently wide integer intermediates, such as u64. Do not use
wrapping_add before extracting the quotient carry.

The exact carry bounds are:

0 <= mu_a[t] <= 6
0 <= mu_e[t] <= 5
0 <= mu_W[t] <= 3

If a byte-oriented message adapter is exposed, it must parse each SHA-256
message word in big-endian byte order. The relation itself stores the bits of
each resulting word LSB first.

3. Construct M_mix

Represent M_mix as typed sparse XOR taps. Do not construct a dense
13,312 × 6,816 allocation in production code.

For LSB-first word bits, define:

(R_r u)[i] = u[(i + r) mod 32]

(S_r u)[i] =
    u[i + r], when i < 32 - r
    0,        otherwise

The virtual families are:

Sigma0[t][i] =
    a[t][i + 2]
  XOR a[t][i + 13]
  XOR a[t][i + 22]

Sigma1[t][i] =
    e[t][i + 6]
  XOR e[t][i + 11]
  XOR e[t][i + 25]

sigma0[s][i] =
    W[s][i + 7]
  XOR W[s][i + 18]
  XOR (W[s][i + 3] when i < 29)

sigma1[s][i] =
    W[s][i + 17]
  XOR W[s][i + 19]
  XOR (W[s][i + 10] when i < 22)

X_ef[t][i] =
    e[t][i] XOR e[t - 1][i]

X_eg[t][i] =
    e[t][i] XOR e[t - 2][i]

X_maj[t][i] =
    a[t][i] XOR a[t - 1][i] XOR a[t - 2][i]

Rotation indices are reduced modulo 32. Shift terms outside the word are
omitted rather than wrapped.

The family ranges are:

Sigma0       t = 1..=64
Sigma1       t = 1..=64
sigma0       s = 2..=49
sigma1       s = 15..=62
X_ef         t = 1..=64
X_eg         t = 1..=64
X_maj        t = 1..=64

The same sparse representation must support:

• forward evaluation: z = M_mix(f)
• transpose accumulation: M_mix^T(q)
• optional CSR/debug materialization for tests

z must always be derived through this map. No API may accept virtual bits as
an independent witness.

4. Construct A_x

Construct A_x as sparse signed-integer rows over

h = (1, f, z)

The leading coordinate h[0] = 1 is fixed by the relation and must not be
provided as a prover-controlled value.

For a bit-vector word u, use

[u] = sum_{j=0}^{31} 2^j u[j].

Define the bridge expressions

chi_t =
    [e[t - 1]]
  + [e[t - 2]]
  - [X_ef[t]]
  + [X_eg[t]]
  = 2[Ch_t]

m_t =
    [a[t]]
  + [a[t - 1]]
  + [a[t - 2]]
  - [X_maj[t]]
  = 2[Maj_t].

Emit the following row families.

State update C_a

For t = 1..=64:

  2[a[t + 1]]
- 2[e[t - 3]]
- 2[Sigma1[t]]
- chi_t
- 2K[t]
- 2[W[t]]
- 2[Sigma0[t]]
- m_t
+ 2^33 mu_a[t]
= 0

At t = 64, a[65] is public and is accumulated into the fixed-coordinate
coefficient.

State update C_e

For t = 1..=64:

  2[e[t + 1]]
- 2[a[t - 3]]
- 2[e[t - 3]]
- 2[Sigma1[t]]
- chi_t
- 2K[t]
- 2[W[t]]
+ 2^33 mu_e[t]
= 0

At t = 64, e[65] is public and is accumulated into the fixed-coordinate
coefficient.

Schedule update C_W

For t = 17..=64:

  [W[t]]
- [W[t - 16]]
- [sigma0[t - 15]]
- [W[t - 7]]
- [sigma1[t - 2]]
+ 2^32 mu_W[t]
= 0

Boundary rows

Emit the following 30 word equalities:

6 prologue equalities
2 initial a/e equalities
16 message equalities
6 terminal-trace equalities

Explicitly, the terminal trace pins:

a[64] = S_65[1]
a[63] = S_65[2]
a[62] = S_65[3]

e[64] = S_65[5]
e[63] = S_65[6]
e[62] = S_65[7]

The public values S_65[0] = a[65] and S_65[4] = e[65] are checked in
C_a(64) and C_e(64).

Public message words, chaining-state words, terminal-state words, and round
constants are accumulated into the coefficient of h[0].

Build and check these rows over exact signed integers. Projection into F_q
belongs to the later PIOP issue.

Expected relation size

For one SHA-256 compression core:

Object	Rows or outputs	Input/witness coordinates
Committed witness f	—	6,816 bits
Virtual witness z	—	13,312 bits
M_mix	13,312 outputs	6,816 inputs
M = [I; M_mix]	20,128 outputs	6,816 inputs
h = (1, f, z)	—	20,129 coordinates
A_x	206 constraints	20,129 coordinates

Committed-witness census

a[-2..=64]                    67 × 32 = 2,144
e[-2..=64]                    67 × 32 = 2,144
W[1..=64]                     64 × 32 = 2,048
bin3(mu_a[1..=64])            64 ×  3 =   192
bin3(mu_e[1..=64])            64 ×  3 =   192
bin2(mu_W[17..=64])           48 ×  2 =    96
------------------------------------------------
|f|                                         6,816

Virtual-witness census

Sigma0                           64 × 32 = 2,048
Sigma1                           64 × 32 = 2,048
sigma0                           48 × 32 = 1,536
sigma1                           48 × 32 = 1,536
X_ef                             64 × 32 = 2,048
X_eg                             64 × 32 = 2,048
X_maj                            64 × 32 = 2,048
------------------------------------------------
|z|                                        13,312

Constraint-row census

C_a state updates                  64
C_e state updates                  64
C_W schedule updates               48
Boundary equalities                30
-------------------------------------
A_x rows                           206

Expected bounds

The implementation must enforce or assert the following structural bounds:

• Every prover-dependent coordinate of h is a bit.

• M_mix has exactly 35,216 nonzero entries, all equal to one.

• Every M_mix row has support at most three.

• The largest non-fixed coefficient magnitude in A_x is 2^35.

• Maximum structural sparse-row widths, including the fixed coordinate, are:

  C_a        <= 420 terms
  C_e        <= 292 terms
  C_W        <= 162 terms
  boundary   <=  33 terms
  

For each emitted row define

B_row = sum_j |A_x[row, j]|.

The current construction must satisfy the conservative bound

max_row B_row < 34 * 2^32.

Expose or calculate this bound from the emitted rows so the downstream PIOP can
check

q > 2 * max_row B_row.

For the configured q = 2^100 - 15, this leaves a wide margin against modular
aliasing.

Downstream shape contract

This issue does not implement the PIOP, but it must expose enough stable shape
metadata for the PIOP issue to assert:

live constraint rows             206
padded constraint-row domain     256 = 2^8

logical h length              20,129
padded h domain               32,768 = 2^15

The later evaluation-shaping sumcheck will therefore use 15 variables and
individual degree two.

Suggested API shape

The exact names are flexible, but the resulting interface should support the
equivalent of:

let relation = Sha256Relation::compression_core(public_instance);
let witness = relation.synthesize()?;

assert_eq!(witness.f.len(), 6_816);

let z = relation.m_mix().apply(&witness.f)?;
let h = relation.assemble_h(&witness.f, &z)?;

assert_eq!(z.len(), 13_312);
assert_eq!(h.len(), 20_129);

let rows = relation.integer_rows();
assert_eq!(rows.len(), 206);

relation.check_integer_rows(&h)?;

The verifier-facing relation and index definitions must not require access to
the native witness synthesizer.

Out of scope

• projection from the integer rows into F_q
• PIOP row collapse
• evaluation-shaping sumcheck
• the mod-q chunked opener from E6 - Prover core: mod-q chunked opener, pre-sumcheck, sumcheck prover #7
• commitment, encoding, or Merkle construction
• transcript messages
• merged GKR
• ring switching
• commitment tensor padding and transposition
• optimized virtual-claim or tap-collapse routing
• feed-forward rows
• digest-only relation
• dense production representations of M_mix or A_x

Validation

Done when all of the following hold:

• Standard SHA-256 compression vectors match an independent implementation.

• Random compression instances produce exactly 6,816 committed bits.

• M_mix(f) produces exactly 13,312 virtual bits.

• M_mix has exactly 35,216 nonzero entries.

• Every generated valid instance satisfies A_x h = 0 exactly over the
  integers.

• The A_x row count is exactly 206 with the expected family census.

• Every generated row satisfies the documented coefficient, sparsity, and
  B_row bounds.

• The adjoint identity passes for randomized binary vectors:

  <q, M_mix f> = <M_mix^T q, f> over F_2.
  

• Negative tests independently mutate:

  • one state-trace bit
  • one schedule bit
  • one carry bit
  • one virtual XOR bit
  • one public message word
  • one public initial-state word
  • one public terminal-state word

  and demonstrate rejection by the appropriate relation.

• Dedicated tests cover the zero-filled portions of SHR^3 and SHR^10.

• Golden index tests pin representative coordinates from every committed and
  virtual family.

• Boundary tests pin the complete prologue, initial-state, message, and
  terminal-state mappings.

• The fixed coordinate is always one and cannot be supplied by the prover.

• Production code does not allocate either matrix densely.

• The workspace passes:

  cargo test --workspace --all-features
  cargo clippy --workspace --all-targets --all-features -- -D warnings
  cargo fmt --all --check
  

Dependencies

• The SHA-256 F2Z engineering note from docs: add SHA-256 F2Z note #14 must be landed or its exact revision
  pinned before this relation is frozen.
• This issue does not depend on the generic prover-core issue E6 - Prover core: mod-q chunked opener, pre-sumcheck, sumcheck prover #7.

Effort M.