Feat/ecsm update

[jotabulacios]

Motivation

The spec received several updates after PR #657 merged. This PR brings the implementation in sync.

Description

EC_SCALAR inlined into ECSM

The separate EC_SCALAR chip is removed. The scalar k is now stored as 256 individual bit columns inside ECSM instead of 32 bytes. ECSM directly holds and validates all scalar bits via IS_BIT constraints, and interacts with the BIT bus as a receiver (one per bit). The SERVE_K self-referential bus is eliminated.

xG range check in the ECSM AIR

Adds a new column xG_sub_p (U256HL) and proves xG < p via the same carry-overflow technique already used for k < N and xR < p. Previously this was only enforced in the executor.

Disjoint memory timestamps

Separates the xG and k memory reads into different timestamp slots: xG reads at T, k register read and k dword reads at T+1, xR write at T+2.

q1[32] IS_BYTE

The yG quotient's high byte (q1[32]) was previously constrained by IS_BIT (polynomial). It is now IS_BYTE (bus lookup), fixing a completeness issue for witnesses where q1[32] > 1.

ECDAS padding simplified

Padding rows now use q0 = q1 = q2 = 0 and op = 1. The R·P term in the λ and xR convolution relations is gated with μ, so it vanishes on padding rows and the relations hold at zero carries without needing to pad quotients to r = 3p.

Curve identifier in ECDAS bus

A curve identifier id (Bit, 0 = secp256k1) is prepended to the ECDAS bus tuple in all interactions, enabling future domain separation between curves.

[jotabulacios]

/bench

[github-actions]

Benchmark — ethrex 20 transfers (median of 3)

_{Table parallelism: auto (cores / 3)}

Metric	main	PR	Δ
Peak heap	73337 MB	72878 MB	-459 MB (-0.6%) ⚪
Prove time	40.250s	40.110s	-0.140s (-0.3%) ⚪

✅ No significant change.

🔬 Looks like a small speedup (-0.3%) — below what 3 runs can confirm. Comment /bench-abba to run the drift-free ABBA tiebreaker (paired-t CI + exact Wilcoxon). Note: it occupies the bench server for ~30–40 min.
Optional pair count: /bench-abba 32 (20 resolves ~1%, 32 for ~0.6%).

✅ Low variance (time: 1.0%, heap: 0.6%)

_{Commit: 1cb8988 · Baseline: cached · Runner: self-hosted bench}

[jotabulacios]

/ai-review

[github-actions]

Codex Code Review

Findings

• Low: prover/src/tables/trace_builder.rs still documents the old ECSM / EC_SCALAR / ECDAS flow and says x12/k are read at T with EC_SCALAR byte reads at T+1. The code now reads x12 and k at T+1 and removes EC_SCALAR entirely (line 707, line 718). This timestamp schedule is part of the MEMW proof invariant, so the stale comment can mislead future changes. Update it and the remaining EC_SCALAR doc reference in crypto/ecsm/src/lib.rs.

Open Question

• The PR moves k reads to T+1, but the executor/test rationale still says overlapping xG/k is unprovable because they are read at the same proof timestamp. If overlap rejection is still intended, the rationale should be updated; if not, the guard/test are now stale.

No higher-severity safety, VM semantics, or performance issues found in the PR diff. I did not build or test, per the review constraints.

[claude]

Review — Feat/ecsm update

Reviewed the EC_SCALAR→ECSM inlining, the xG<p range check, the disjoint memory timestamps, the q1[32] IS_BYTE fix, the ECDAS padding simplification, and the curve-id addition to the ECDAS bus.

The substantive changes look correct and sound:

• ECDAS padding (op=1, q=0, μ-gated R·P): all op-constraints still hold on padding rows (op·next_op=0, next_op·(1-μ)=0, IS_BIT(op)), and the three convolution relations evaluate to 0 at zero carries. Real rows (μ=1) are unchanged; degrees unchanged.
• Bit bus balance: ECSM receives Bit[ts,i] (mult k_bit[i]) for all 256 bits, ECDAS sends per add-round (mult next_op), ECSM sends the MSB. Because ECDAS rounds only reach len_k-1 and the MSB send is at len_k, the balance forces k_bit[len_k]=1 and k_bit[i]=0 for i>len_k — sound.
• xG<p: correct reuse of the byte-path carry-overflow technique; witness (x_g_sub_p), collect_bitwise_from_ecsm, IsHalfword sends, and the +8 constraints are all consistent. Count 411 = 1 + 256 + 8 + 146 checks out.
• Disjoint timestamps: executor (collect_ecsm_ops) and AIR bus sides agree (xG@T, k@T+1 + x12/x10 regs@T+1, xR@T+2); register vs memory use separate is_register namespaces so co-located pointers don't collide. This also resolves the addr_xg == addr_k double-use of (addr, T) the old both-at-T scheme had.
• q1[32] IS_BYTE: consistent across trace / bus / bitwise collection; strictly a completeness fix.
• All ServeK / ec_scalar references are fully removed.

Minor — stale doc comments not updated by this PR:

1. prover/src/tables/trace_builder.rs:654-656 — the collect_ecsm_ops doc still says the x11/x12 register reads and the xG/k memory reads happen at T; the x10 register read and the EC_SCALAR byte reads at T + 1. After this PR the scheme is: x11 + xG at T; x12 + k + x10 at T+1; xR writes at T+2, with no EC_SCALAR byte reads. Since the disjoint-timestamp reorg is the crux of this PR, this comment is now misleading.

2. crypto/ecsm/src/lib.rs:5 — still refers to filling the ECSM / ECDAS / EC_SCALAR trace witnesses; EC_SCALAR no longer exists.

No blocking issues.

[github-actions]

AI Review

PR #753 · 12 changed files

Findings

Status	Sev	Location	Finding	Found by
candidate	low	prover/src/tables/ecsm.rs:472	Q1[32] range constraint weakened from IS_BIT to AreBytes	minimax minimax/MiniMax-M3
candidate	low	prover/src/tables/ecsm.rs:549	len_k column is a free variable constrained only by the BIT bus	minimax minimax/MiniMax-M3
candidate	low	prover/src/tables/ecsm.rs:906	256 IS_BIT constraints on k_bit columns add significant cost	minimax minimax/MiniMax-M3
candidate	low	prover/src/tests/ecsm_tests.rs:97	Test coverage gap for new XgLtP overflow constraint	minimax minimax/MiniMax-M3

Status column reflects the verdict from the verifier: deepseek-verifier (openrouter/deepseek/deepseek-v4-pro).

AI-001: Q1[32] range constraint weakened from IS_BIT to AreBytes

• Status: candidate
• Severity: low
• Location: prover/src/tables/ecsm.rs:472
• Found by: minimax:minimax/MiniMax-M3
• Verified by: -
• Rejected by: -

Claim

The old code constrained q1[32] via an unconditional IS_BIT transition constraint (forcing 0 or 1), but the new code uses AreBytes (allowing 0..255). AreBytes[32] is a stricter bound than IS_BIT, but the corresponding IS_BIT transition constraint is no longer created.

Evidence

Old code: is_byte(cols::Q1, 32, &mut out); + IsBitConstraint::unconditional(cols::q1(32), idx). New code: is_byte(cols::Q1, 33, &mut out); and no separate IS_BIT constraint for q1[32]. AreBytes[x, 0] via BITWISE constrains x in [0, 256) for real rows (mu=1); on padding mu=0 so no constraint. The mathematical range of q1[32] is in [0, ~5], so the looser AreBytes constraint is sufficient for soundness, but the previous design explicitly forced it to be a bit.

Suggested fix

No functional change needed; both forms soundly constrain q1[32]. If the design intent is to constrain q1[32] to be a bit (e.g. because it carries the high bit of a shifted quotient), add an explicit IS_BIT constraint. Otherwise, document the change.

AI-002: len_k column is a free variable constrained only by the BIT bus

• Status: candidate
• Severity: low
• Location: prover/src/tables/ecsm.rs:549
• Found by: minimax:minimax/MiniMax-M3
• Verified by: -
• Rejected by: -

Claim

The LEN_K column has no direct AIR transition constraint enforcing that its value matches the MSB position of the scalar k. Soundness relies entirely on the BIT bus balancing: if LEN_K doesn't equal msb_position(k), the bus is imbalanced and the verifier detects it.

Evidence

The ECSM Bit sender is Bit[ts, LEN_K] with mult=mu, and the schedule visits rounds 0..LEN_K-1 in op=0 ECDAS steps sending Bit[ts, round] with mult=k[round]. The BIT receivers expect Bit at each position i with mult=k_bit[i]. Balance requires LEN_K to equal msb_position(k). However, there is no transition constraint on LEN_K directly; a malicious prover could set LEN_K to any value, and the prover-side witness must agree (since witness.len_k is computed from k). The verifier-side check works through bus balance, but there's no direct constraint.

Suggested fix

Optionally add a transition constraint that ties LEN_K to k_bit (e.g., LEN_K = argmax of k_bit positions). Alternatively, document that LEN_K is implicitly constrained by the BIT bus balance.

AI-003: 256 IS_BIT constraints on k_bit columns add significant cost

• Status: candidate
• Severity: low
• Location: prover/src/tables/ecsm.rs:906
• Found by: minimax:minimax/MiniMax-M3
• Verified by: -
• Rejected by: -

Claim

256 IS_BIT transition constraints on k_bit columns push the ECSM constraint count to 411, more than doubling from 148. The MEMW bus read of k (via k_dword_busvalues) already implicitly constrains k_bit values to be 0 or 1 via the byte reconstruction matching memory, making most of these IS_BIT constraints arguably redundant.

Evidence

The diff comment on the create_constraints function says "411 total: 1 mu + 256 k bits + 8 xG<p + 146 others." 256 IS_BITs on k_bit is a large share. The byte value Σ 2^j · k_bit[8b..8b+7] is forced to equal the actual byte in memory by MEMW (the only decomposition of a 256-value into 8 weighted binary bits is the unique one with bits in {0,1}). However, without IS_BIT, a malicious prover could potentially set k_bit[i] = 2 for some position i, which would force other k_bits to compensate (e.g., negative contributions mod p), potentially breaking the BIT bus multiplicities in subtle ways. IS_BIT provides defense-in-depth at the cost of 256 degree-2 constraints.

Suggested fix

Consider whether the IS_BIT constraints are needed for soundness or only for defense-in-depth. If the latter, consider whether the proving-time cost justifies them or whether the BIT bus and MEMW bus interactions are sufficient.

AI-004: Test coverage gap for new XgLtP overflow constraint

• Status: candidate
• Severity: low
• Location: prover/src/tests/ecsm_tests.rs:97
• Found by: minimax:minimax/MiniMax-M3
• Verified by: -
• Rejected by: -

Claim

The new OverflowKind::XgLtP (xG<p) constraints are not exercised by constraints_hold_on_generated_trace, which only iterates over [OverflowKind::KLtN, OverflowKind::XrLtP].

Evidence

Looking at prover/src/tests/ecsm_tests.rs lines 97-118, the test only iterates [OverflowKind::KLtN, OverflowKind::XrLtP] for CarryBit and OverflowRequired, but create_constraints (lines 956-975) creates 8 XgLtP constraints (7 CarryBit + 1 OverflowRequired). These new constraints are never asserted to evaluate to zero on the generated trace.

Suggested fix

Extend the iteration to include OverflowKind::XgLtP in the test, mirroring the existing KLtN/XrLtP checks.

Reviewer Lanes

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

Verification Lanes

Lane	Model	Status	Confirmed	Rejected	Uncertain
deepseek-verifier	openrouter/deepseek/deepseek-v4-pro	error: opencode failed (provider/auth/runtime error) and no verifications were submitted	0	0	0

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

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	59.9 ± 0.9	58.1	61.4	1.00
head binary_search	63.3 ± 14.7	57.6	105.1	1.06 ± 0.25

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base bitwise_ops	58.3 ± 1.3	57.4	60.8	1.00
head bitwise_ops	58.5 ± 1.4	57.4	60.5	1.00 ± 0.03

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base ecsm	3.1 ± 0.0	3.1	3.1	1.00
head ecsm	3.1 ± 0.0	3.0	3.2	1.00 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base fibonacci_26	63.5 ± 0.8	62.8	65.4	1.00
head fibonacci_26	63.7 ± 1.1	62.7	65.4	1.00 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base hashmap	131.3 ± 3.1	126.7	136.5	1.00
head hashmap	132.3 ± 1.3	130.3	134.3	1.01 ± 0.03

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base keccak	132.0 ± 2.8	127.6	137.4	1.01 ± 0.03
head keccak	131.3 ± 3.6	126.3	139.4	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base matrix_multiply	63.7 ± 1.0	62.2	65.7	1.00
head matrix_multiply	64.6 ± 1.0	63.3	66.4	1.01 ± 0.02

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base modular_exp	59.1 ± 1.0	57.9	61.0	1.01 ± 0.02
head modular_exp	58.7 ± 0.8	57.8	60.1	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base quicksort	62.6 ± 0.6	61.8	63.8	1.00
head quicksort	62.8 ± 0.4	62.1	63.2	1.00 ± 0.01

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sieve	64.4 ± 0.5	63.8	65.6	1.00
head sieve	64.7 ± 0.5	63.8	65.4	1.00 ± 0.01

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sum_array	73.9 ± 0.3	73.3	74.2	1.00 ± 0.01
head sum_array	73.8 ± 0.6	73.2	75.0	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base syscall_commit	90.4 ± 1.2	89.6	93.7	1.00
head syscall_commit	90.7 ± 0.8	89.8	91.8	1.00 ± 0.02

[jotabulacios]

Responses to AI reviewers

Council of AIs

• AI-001 (IS_BIT on q1[32]): Fixed in 53e31bd — this was a genuine soundness bug
  introduced when removing a reindexing scheme that was later reverted. The IS_BIT
  constraint is back.

• AI-002 (LEN_K unconstrained): False positive. len_k is constrained implicitly by
  the bus balance: the ECSM chip sends exactly 256 BIT interactions for k, so a wrong
  len_k would break bus balance and fail verification.

• AI-003 (256 IS_BIT receivers redundant): False positive. Each of the 256 bit columns
  holds a single bit of k. Without IS_BIT on each one, a malicious prover could set any
  column to an arbitrary field element while still satisfying the bus interaction (which
  only checks the linear combination). The individual IS_BIT constraints are required for
  soundness.

• AI-004 (XgLtP missing from test): Fixed in cd41217 — added OverflowKind::XgLtP
  to the overflow carry constraint loop in constraints_hold_on_generated_trace.

Codex

• Low (stale doc comments in trace_builder.rs and crypto/ecsm/src/lib.rs): Fixed
  in 53e31bd — collect_ecsm_ops doc now accurately describes the disjoint timestamp
  scheme (x11+xG at T; x12+k+x10 at T+1; xR at T+2), and lib.rs no longer references
  EC_SCALAR.

• Open question (executor overlap rationale): Fixed in 53e31bd — the comment now
  explains the actual reason: overlapping addresses would cause the same memory byte to
  serve as both an xG limb and a k bit, corrupting the scalar multiplication. The overlap
  guard is still intentional and correct.

Claude

• Minor (stale doc comments): Fixed in 53e31bd — same as Codex finding above.