Skip to content

feat(prover): add MEMW_A aligned-memory fast path table#441

Merged
MauroToscano merged 22 commits into
mainfrom
feat/memw-aligned
Mar 31, 2026
Merged

feat(prover): add MEMW_A aligned-memory fast path table#441
MauroToscano merged 22 commits into
mainfrom
feat/memw-aligned

Conversation

@nicole-graus
Copy link
Copy Markdown
Collaborator

Description

Implements the MEMW_A aligned fast path from spec PR #398.

Adds a new 30-column table for memory/register accesses where all bytes share the same
old_timestamp (aligned ops). Operations are routed at trace build time: aligned ops with uniform
timestamps go to MEMW_A, the rest go to MEMW.

  • 30 columns, 20 bus interactions, 2 algebraic constraints.
  • Address decomposed into high/mid/low parts; AND_BYTE interaction for alignment check.
  • Single shared old_timestamp instead of per-byte (8× fewer LT checks).
  • All register operations route here by default.

@github-actions
Copy link
Copy Markdown

Codex Code Review

Findings

  1. High (Security/Soundness): MEMW_A relies on off-circuit routing for a proof-critical invariant
  • The new table explicitly assumes uniform per-byte old_timestamp is “verified by the routing logic,” then stores only old_timestamp[0] and enforces only one LT check.
  • References:
  • Why this matters: prover soundness must be enforced by AIR/bus constraints, not by trusted trace-construction logic. A malicious prover is not required to use is_aligned_op.
  • Action: enforce the uniform-timestamp invariant in-circuit (or keep such ops in MEMW). Right now the invariant is only a host-side convention.
  1. Low (Bug/Robustness): possible panic on unexpected width in is_aligned_op
  • for i in 1..op.width as usize { ... op.old_timestamp[i] ... } can index out of bounds if width > 8.
  • Reference: trace_builder.rs:802
  • Action: guard width explicitly (matches!(width, 1|2|4|8)) before indexing.

Assumptions / gaps

  • I could not run tests in this sandbox because Rust toolchain update tries to write under a read-only rustup path.

Comment thread prover/src/tables/memw_aligned.rs Outdated
Comment thread prover/src/tables/trace_builder.rs
Comment thread prover/src/tables/memw_aligned.rs Outdated
@claude
Copy link
Copy Markdown

claude Bot commented Mar 18, 2026

Review: feat(prover) — MEMW_A aligned-memory fast path

Overall the implementation is correct and well-structured. The routing logic, bus interaction format, alignment/timestamp checks, and constraint set all look sound. Two minor issues noted below (see inline comments).

Security / correctness

No vulnerabilities found. Specific points verified:

  • CO24/CO25 bus fingerprint format matches the original MEMW table exactly (field ordering: old[8], is_register, addr_lo, addr_hi, value[8], ts, write_flags for reads; is_register, addr_lo, addr_hi, value[8], ts, write_flags for writes).
  • The missing R1-R3 address-overflow LT checks in collect_lt_from_memw_aligned are intentionally correct: for a power-of-2 width N, the largest N-aligned u64 is 2^64-N, so addr+(N-1) = 2^64-1 — no wrap is possible. The omission just needs a comment (see inline).
  • AND_BYTE alignment mask write2·1 + write4·3 + write8·7 correctly encodes width-1 for each valid width (1→0, 2→1, 4→3, 8→7).
  • Padding rows are all-zero; mu_sum=0 suppresses every bus interaction, so no phantom LT/bitwise entries are needed.
  • The single shared old_timestamp is gated by is_aligned_op's uniform-timestamp check before routing.

Issues

  1. Low (inline on trace_builder.rs:784) — collect_lt_from_memw_aligned silently drops R1-R3 overflow checks with no explanation; add a one-line comment.
  2. Low (inline on memw_aligned.rs:20) — PR description says "20 bus interactions" but there are 22; the file header is correct.

@yetanotherco yetanotherco deleted a comment from github-actions Bot Mar 18, 2026
@nicole-graus
Copy link
Copy Markdown
Collaborator Author

/bench

@github-actions
Copy link
Copy Markdown

github-actions Bot commented Mar 18, 2026

Benchmark — fib_iterative_8M (median of 3)

Table parallelism: 32 (auto = cores / 3)

Metric main PR Δ
Peak heap 256201 MB 250991 MB -5210 MB (-2.0%) ⚪
Prove time 105.611s 99.212s -6.399s (-6.1%) 🟢

🎉 Improvement detected — heap or time decreased by more than 5%.

✅ Low variance (time: 1.6%, heap: 0.3%)

Commit: 49bf320 · Baseline: cached · Runner: self-hosted bench

@diegokingston
Copy link
Copy Markdown
Collaborator

/bench

@nicole-graus
Copy link
Copy Markdown
Collaborator Author

/bench

2 similar comments
@diegokingston
Copy link
Copy Markdown
Collaborator

/bench

@diegokingston
Copy link
Copy Markdown
Collaborator

/bench

@nicole-graus
Copy link
Copy Markdown
Collaborator Author

/bench

@nicole-graus
Copy link
Copy Markdown
Collaborator Author

/bench

1 similar comment
@nicole-graus
Copy link
Copy Markdown
Collaborator Author

/bench

@nicole-graus
Copy link
Copy Markdown
Collaborator Author

/bench

Copy link
Copy Markdown
Contributor

@MauroToscano MauroToscano left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We need to understand why there is no improvement

@MauroToscano MauroToscano enabled auto-merge March 31, 2026 17:22
@MauroToscano MauroToscano added this pull request to the merge queue Mar 31, 2026
Merged via the queue into main with commit 35da6be Mar 31, 2026
9 checks passed
@MauroToscano MauroToscano deleted the feat/memw-aligned branch March 31, 2026 18:20
erik-3milabs pushed a commit that referenced this pull request Apr 10, 2026
* don't run executor benches all the time

* Add MEMW_A aligned-memory fast path table

* fix deviation from spec: is_half and is_byte assumptions

* add comment

* Add a prove_elf test

* add prove_elf test using both MEMW and MEMW_A chips

* fix comment: bus numbering

* Use Multiplicity::Sum3 for w2 in MEMW_A to avoid heap allocation on hot path

* change max_rows per chunk to 2^19 insted of 2^20

---------

Co-authored-by: MauroFab <maurotoscano2@gmail.com>
Co-authored-by: Mauro Toscano <12560266+MauroToscano@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants