[nicole-graus]

Motivation

The spec defines the CPU timestamp as a preprocessed column (4·(i+1)), but the code had it as a free column. That allowed two bugs:

• pc_double_read forgery: a prover could set a row's timestamp so that pc_double_read reads a register before the previous row writes it, e.g. proving exit(0) for a program that exits with 5.
• Timestamp wrap-around: the prover chose each row's timestamp step (up to ~2^32), and the verifier did not bound the number of CPU rows. With ~2^32 rows the steps could add up past p, so a later access could match stale data.

Description

• CPU TIMESTAMP is preprocessed. With several CPU tables, table k adds 4·S_k, where S_k is the total height of the previous tables. The verifier reads the heights from the proof.
• Static commitments for each height (2^2..2^19) and blowup (2, 4, 8).
• The verifier rejects more than 2^30 − 1 CPU rows per epoch.
• Removes PREV_PC_TIMESTAMP_BORROW.
• REGISTER consumes the final PC at the verifier-known 4·N + 1 (new preprocessed IS_PC column).
• HALT finalizes registers at 2^32 − 1, as in the spec.
• The spec doesn't define the timestamp for multiple CPU tables, and its 2^30 cycle limit should be < 2^30 and checked by the verifier.

[nicole-graus]

/ai-review

[nicole-graus]

/bench-gpu

[github-actions]

GPU Benchmark (ABBA) — dfa0d5c6ac vs main (14 pairs)

_{RTX 5090 · AMD Ryzen 9 5950X 16-Core Processor (32 threads) · Vast.ai datacenter @ $1.0013888888888889/hr · prover/cuda · ethrex real block, continuations · drift-free A/B/B/A}

=== ABBA paired result  (improvement: - = PR faster) ===
  pairs: 14   mean A (PR): 47.236s   mean B (base): 47.182s

  [parametric] paired-t   mean +0.12%   sd 1.31%   se 0.35%
               95% CI: [-0.64%, +0.88%]   (t df=13 = 2.16)
  [robust]     median -0.13%   Wilcoxon W+=45 W-=60  p(exact)=0.6698  (z=-0.44)

  --- server stability (this run; compare across servers) ---
  run-to-run jitter:    A CV 1.36%   B CV 0.74%        (lower = steadier)
  within-session drift: +0.11% over the run, 1st->2nd half +0.04%
    (jitter -> Tier-1 cached gate floor; drift -> whether the cached baseline can be trusted)

  VERDICT: INCONCLUSIVE - effect not separable from 0 at n=14.
           Point estimate ~-0.13% (median). Need more pairs to resolve.

  raw pairs: /tmp/abba_run/pairs.csv

_{- = PR faster. Trust the verdict when paired-t and Wilcoxon agree.}

[nicole-graus]

/bench

[github-actions]

Codex Code Review

No actionable issues found in the PR diff. Reviewed statically, including timestamp bounds, split CPU tables, continuation verification, and preprocessed commitments. No builds or tests run.

[claude]

Review: no blocking issues found.

What I checked:

• Timestamp layout. Table k uses base 4·S_k and its first row reads the PC at 4·S_k + 1, which is where the previous table's last row writes it (4·0 + 1 = 1 lines up with REG-C1 init). Padding exists only in the last table, so final_pc_timestamp(N) = 4N + 1 matches halt_ts + 4·num_padding + 1 in the trace builder.
• HALT at 2^32−1. No access offset is larger than +2; this includes ECSM, which uses ts+1 and ts+2. So with N ≤ 2^30−1, the largest access is 4N+2 ≤ 2^32−2 and the MEMW old_ts < ts check still holds.
• Verifier-side heights. The heights come from sub-proof trace_length, go through validate_heights (power of two, [4, max_rows::CPU], sum ≤ MAX_CPU_ROWS), and then select the static commitment. cpu_heights_from_proofs returns None when there are too few sub-proofs instead of panicking. include_halt = is_final is passed correctly for continuation epochs.
• REGISTER. Multiplicity::Negated(IS_PC) is 1 − is_pc, and IS_PC is preprocessed. That leaves the x255 rows' TIMESTAMP columns unconstrained, but no bus or constraint reads them.
• GPU LogUp. It folds LinearTerm::Constant(i64) into a canonical u128 accumulator, so the larger ts_base constants are fine.
• AIR prototype cache. It is bounded: only bases that are multiples of 4·max_rows::CPU are cached (≤ 2^11 entries), and REGISTER is never cached.

One optional nit (prover/src/tables/cpu.rs, inline-PC prev_ts): it rebuilds TIMESTAMP + base − 3 by hand and repeats the i64::try_from(ts_base) conversion that timestamp_slot already does. Reusing the helper and adding the 3·PC_DOUBLE_READ term would keep every CPU timestamp expression in one place.

[github-actions]

AI Review

PR #1025 · 33 changed files

Warning: the diff was truncated before review.

Findings

No non-rejected structured findings were reported.

Reviewer Lanes

Lane	Model	Prompt	Status	Findings

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 — real block (ethrex_mainnet_25368371.bin) (median of 3)

_{continuations · epoch 2^22 · 8 epochs}

Metric	main	PR	Δ
Peak heap	46791 MB	46472 MB	-319 MB (-0.7%) ⚪
Prove time	133.665s	137.165s	+3.500s (+2.6%) ⚪

✅ No significant change.

⚠️ Real-block prove-time spread: 4.9% (139.329s / 137.165s / 132.607s) — the median above is less trustworthy than usual.

_{Commit: dfa0d5c · Baseline: built from main · Runner: self-hosted bench}