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 · 16 changed files

Findings

Status	Sev	Location	Finding	Found by
candidate	low	executor/src/vm/instruction/execution.rs:415	Executor comment about "k bit" terminology may be misleading	moonmath zro/minimax-m3
candidate	low	prover/src/tables/ecsm.rs:596	Hardcoded id=0 in ecdas_tuple is single-curve assumption	moonmath zro/minimax-m3
candidate	low	prover/src/tables/trace_builder.rs:680	ECS MEMW op count cap mismatch with potential count	moonmath zro/minimax-m3
candidate	low	prover/src/tables/types.rs:300	BusId gap at ID 29 after removing ServeK	moonmath zro/minimax-m3

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

AI-001: Executor comment about "k bit" terminology may be misleading

• Status: candidate
• Severity: low
• Location: executor/src/vm/instruction/execution.rs:415
• Found by: moonmath:zro/minimax-m3
• Verified by: -
• Rejected by: -

Claim

The comment "overlapping addresses would cause the same memory byte to serve as both an xG limb and a k bit" uses "k bit" to mean a byte of k (since the new design stores k as bytes in memory but as bits in the AIR trace). The terminology matches the new design but could be misread.

Evidence

The executor reads k as 4 doublewords (32 bytes total) from memory. The new ECSM design then decomposes k bytes into 256 individual bit columns for the AIR constraint. The "k bit" wording aligns with the new constraint model but the byte-level memory access and the bit-level constraint reference the same scalar in different forms.

Suggested fix

Consider clarifying: "would cause the same memory byte to serve as both an xG limb (in the yG carry relation) and a k limb (whose bits feed the k<N overflow check and the Bit bus receives)". This is purely documentation; the underlying check is correct.

AI-002: Hardcoded id=0 in ecdas_tuple is single-curve assumption

• Status: candidate
• Severity: low
• Location: prover/src/tables/ecsm.rs:596
• Found by: moonmath:zro/minimax-m3
• Verified by: -
• Rejected by: -

Claim

The ecdas_tuple function hardcodes id = 0 for secp256k1. While this is correct for the current single-curve design, it ties the bus format to one curve if other curves are ever added.

Evidence

ecdas_tuple line 596: v.push(BusValue::constant(0)); // id = 0 (secp256k1). The id field is added unconditionally; there is no parameter or variant to support additional curves.

Suggested fix

For now this is fine — only secp256k1 is supported. Consider documenting this constraint near the function. No code change needed unless multi-curve support is added.

AI-003: ECS MEMW op count cap mismatch with potential count

• Status: candidate
• Severity: low
• Location: prover/src/tables/trace_builder.rs:680
• Found by: moonmath:zro/minimax-m3
• Verified by: -
• Rejected by: -

Claim

memw_ops = Vec::with_capacity(15) is the new initial capacity for collect_ecsm_ops after removing the 32 EC_SCALAR byte reads. The actual count is 1+4+1+4+1+4 = 15 MEMW ops. This is correct, but a future change adding reads could silently trigger Vec reallocation.

Evidence

Looking at lines 680-758: the code emits exactly 15 MEMW ops (1 register + 4 xG + 1 register + 4 k + 1 register + 4 xR). The pre-allocation matches.

Suggested fix

No action needed; the cap matches. Just noting for future maintainers: if you add MEMW ops to this function, update the capacity.

AI-004: BusId gap at ID 29 after removing ServeK

• Status: candidate
• Severity: low
• Location: prover/src/tables/types.rs:300
• Found by: moonmath:zro/minimax-m3
• Verified by: -
• Rejected by: -

Claim

The BusId enum has a numerical gap at ID 29 (ServeK was deleted, leaving the value unused). The adjacent Ecdas=28 and Bit=30 are still consecutive. No external consumer references the ID by numeric value, but the gap is undocumented in the enum.

Evidence

Looking at types.rs lines 304-308: Ecdas = 28 and Bit = 30 with no variant between them. The TryFrom<u64> impl returns Err(29). The diff removes ServeK = 29 without adding a comment or reusing the value. Other removed IDs (e.g., 10-13 for ALU buses, 15 for Load) have explanatory comments about being reserved.

Suggested fix

Either add a brief comment noting ID 29 was ServeK and is now reserved/unused, or simply note that the gap is intentional. This is a minor stylistic issue, not a correctness bug.

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	0
moonmath	zro/minimax-m3	general	success	4
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.8 ± 0.6	59.2	60.9	1.00
head binary_search	63.4 ± 5.8	58.4	74.9	1.06 ± 0.10

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base bitwise_ops	59.8 ± 1.6	58.1	62.3	1.02 ± 0.04
head bitwise_ops	58.8 ± 1.3	57.9	61.4	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base ecsm	3.4 ± 0.1	3.4	3.6	1.07 ± 0.03
head ecsm	3.2 ± 0.1	3.1	3.3	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base fibonacci_26	63.0 ± 0.2	62.7	63.5	1.00
head fibonacci_26	63.5 ± 0.7	62.9	64.9	1.01 ± 0.01

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base hashmap	129.4 ± 3.7	123.0	135.0	1.00
head hashmap	133.1 ± 4.9	124.9	141.4	1.03 ± 0.05

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base keccak	128.6 ± 2.7	125.6	134.1	1.00
head keccak	132.1 ± 6.0	124.9	145.3	1.03 ± 0.05

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base matrix_multiply	65.5 ± 1.1	64.0	67.8	1.02 ± 0.02
head matrix_multiply	64.5 ± 0.7	63.1	65.7	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base modular_exp	59.4 ± 0.6	58.5	60.3	1.00
head modular_exp	60.1 ± 0.6	59.2	61.3	1.01 ± 0.01

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base quicksort	63.1 ± 0.5	62.4	63.6	1.00
head quicksort	63.7 ± 0.4	63.1	64.5	1.01 ± 0.01

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sieve	65.4 ± 0.5	64.8	66.1	1.00 ± 0.01
head sieve	65.2 ± 0.4	64.7	65.7	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base sum_array	74.7 ± 0.5	74.0	75.4	1.00 ± 0.02
head sum_array	74.4 ± 1.2	73.3	77.7	1.00

Command	Mean [ms]	Min [ms]	Max [ms]	Relative
base syscall_commit	91.5 ± 0.7	90.7	92.7	1.00
head syscall_commit	96.8 ± 17.9	90.5	147.7	1.06 ± 0.20

[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.

[jotabulacios]

/ai-review

[github-actions]

Codex Code Review

Findings: None.

I reviewed the PR diff only, focusing on the ECSM/EC_SCALAR removal, ECDAS padding changes, MEMW timestamp shifts, bus interactions, and verifier/prover table shape. I did not find a concrete safety, correctness, or significant performance issue in the changed code.

Static review only; I did not build or run tests per the sandbox instructions.

[claude]

Review — ECSM spec sync (EC_SCALAR inline, xG<p, disjoint timestamps, padding)

I traced the cross-chip logic (Bit bus balance, memory timestamps, padding closures, and the new xG < p range check). No Critical / High / Medium issues found. The change is well-constructed and the constraint/bus reasoning holds up. A few notes below.

Verified sound

• Bit bus balance after inlining EC_SCALAR. ECSM now receives Bit[ts,i] (mult k_bit[i]) for all 256 bits and sends Bit[ts,len_k] (mult µ); ECDAS sends Bit[ts,round] (mult next_op). Global balance forces k_bit[len_k]=1, zeroes bits above len_k, and ties each ECDAS add to the matching scalar bit — so len_k is pinned to the true MSB and constrained into 0..255 (no receiver exists for out-of-range indices). The k=1 edge case (start round -1 == final round, xR=xG) is correct.
• KBitsZeroOnPadding (Σ k_bit)·(1−µ) correctly blocks phantom Bit receives on padding, and IS_BIT on k is emitted un-gated so padding bits are pinned to 0.
• Disjoint timestamps in collect_ecsm_ops (xG@T, k@T+1, xR@T+2, regs x11@T/x12@T+1/x10@T+2) match the bus timestamps in ecsm.rs one-for-one.
• xG < p carry chain sums xG from byte columns with P_BYTES; the 16 xg_sub_p halfwords get IsHalfword checks and the bitwise table feeds matching is_half_ops. Consistent.
• ECDAS padding (q0=q1=q2=0, op=1, µ-gated R·P): all three relations close at zero carries with all-coord-zero rows, and real-row behavior (µ=1) is unchanged.
• q1 range: is_byte(Q1, 33) + the AreBytes balance in collect_bitwise_from_ecsm (explicit q1[32] push, with a comment against merging the loop) line up. Restored IS_BIT on q1[32] is correct — q1 < 2p < 2^257, so byte 32 ∈ {0,1}.

Minor notes (non-blocking)

• execution.rs overlap comment (~L415): the new rationale ("same byte serves as both an xG limb and a k bit, corrupting the scalar multiplication") is imprecise. The executor reads xG and k as independent values; overlap yields an unusual-but-valid input, not corruption. The real reason to keep the check is trace provability with overlapping unaligned MEMW accesses — now that xG@T and k@T+1 are at different timestamps the same-timestamp argument no longer applies, but partial/unaligned overlap can still break MEMW, so keeping the guard is right. Worth rewording so a future maintainer doesn't remove it on false premises.
• PR description still lists "q1[32] IS_BYTE … fixing a completeness issue for witnesses where q1[32] > 1", which the restored IS_BIT (patch 07) contradicts. Description-only; consider updating.

Table/AIR bookkeeping (FIXED_TABLE_COUNT 11→10, trace collection order, count functions) is consistent throughout. Compile-level completeness of the EC_SCALAR/ServeK removal is covered by CI.