perf(stark): fuse and hoist deep-composition reconstruction for both FRI points by Oppen · Pull Request #826 · yetanotherco/lambda_vm

Oppen · 2026-07-15T21:25:39Z

Summary

Reimplements the perf/deep-hoist branch's deep-composition fuse+hoist (originally against an older verifier.rs) on top of current main's StarkProofView/precomputed-column-split API.
Fuses the regular/symmetric FRI-point reconstruction into one traversal, and hoists the point-invariant OOD/gamma sums out of the per-query loop into a once-per-proof compute_query_invariant_deep_terms.
Adds a stricter guard: per-query opening length is now checked against the proof-level composition_poly_parts_ood_evaluation length, not just regular-vs-symmetric agreement.

Numbers

The headline figure is the base-layer regime: blowup 2 / 219 FRI queries, verifying a real ethrex block (4 transfers, 2 epochs @ 2^21) through the continuation guest. Measured with the PR #825 ladder (scripts/bench_recursion_scaling.sh, TXS=4 PRESETS=blowup2), base vs head differing only by this PR's verifier.rs:

	Guest cycles
before (`a8a3d870`)	13,364,620,265
after (`2af84167`)	10,649,255,581
Δ	−20.32% (1.255×)

Keccak calls are identical on both (3,152,604) — the win is field-op restructuring, not hashing. Sanity check: the before figure is +0.94% over the recorded post-#769 ladder value for this cell (13.24B), which is #815's own cost.

The other numbers on this PR measure different regimes and should not be read as the Ethrex-relevant win:

Regime	Δ	What it is
blowup2 / 219q / real block	−20.3%	the base-layer regime (above)
`make test-profile-recursion-multi`	−30.8% total, −63.2% step 3	`Preset::Blowup8` over the empty guest — final-wrap params, tiny tables, so deep-composition holds a larger share of the total and the % overstates
`/bench_verifier` guest cycles	−5.34%	`Preset::Min` = 1 FRI query, empty program — the per-query loop this PR optimizes is barely exercised, so the % understates
`/bench_verifier` verify time	−3.95%	native host verify, not in-VM

For reference, the test-profile-recursion-multi figures:

	Total cycles	step 3 (FRI)
before	1,325,335,927	635,418,644
after	916,824,543	233,869,693
Δ	-30.8%	-63.2%

Note that test-profile-recursion-multi cannot express the base-layer regime: its presets are only Min (blowup 2, 1 query) and Blowup8. The blowup2/219q preset lands with #825.

Test plan

cargo test -p stark --lib — 190/190 passing
cargo clippy -p stark --all-targets — clean
make test-profile-recursion-multi before/after (numbers above)
bench(recursion): measure the verifier at real query counts, over real blocks #825 ladder, TXS=4 PRESETS=blowup2 EPOCH_LOG2=21, base vs head (headline numbers above)

…FRI points reconstruct_deep_composition_poly_evaluation walked the OOD table and trace-term coefficients, and inverted denominators, independently for the regular and symmetric evaluation points, then recomputed the point-invariant OOD/gamma sums from scratch on every one of the ~80 FRI queries per proof. Rewriting coeff*(base-ood)*denom as denom*(coeff*base - coeff*ood) isolates the point-independent coeff*ood term (identical between the two points) from coeff*base, so both points can share the OOD walk and a single batch-inverse. The point-invariant ood_row_sum/z_pow/h_sum_zpow sums are now computed once per proof in compute_query_invariant_deep_terms instead of once per query. Multi-query recursion profile: 1,325,335,927 -> 916,824,543 cycles (-30.8%); step 3 (FRI) 635,418,644 -> 233,869,693 cycles (-63.2%).

Oppen · 2026-07-15T22:30:44Z

/bench_verifier

Oppen · 2026-07-15T22:30:59Z

/ai-review

github-actions · 2026-07-15T22:32:14Z

AI Review

PR #826 · 1 changed files

Findings

No non-rejected structured findings were reported.

Reviewer Lanes

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

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 · 2026-07-15T22:32:33Z

Codex Code Review

No issues found in the PR diff. The paired reconstruction preserves the prior algebra and retains malformed-proof rejection checks.

github-actions · 2026-07-15T22:34:12Z

Benchmark — ethrex 20 transfers (median of 3)

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

Metric	main	PR	Δ
Peak heap	73403 MB	72734 MB	-669 MB (-0.9%) ⚪
Prove time	38.292s	38.038s	-0.254s (-0.7%) ⚪

✅ No significant change.

🔬 Looks like a small speedup (-0.7%) — 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: 0.5%, heap: 1.1%)

_{Commit: 2af8416 · Baseline: cached · Runner: self-hosted bench}

claude · 2026-07-15T22:34:34Z

Review: deep-composition fuse + hoist

I verified the algebraic rewrite and the guard changes against the diff and the surrounding verifier.rs / trace_term_coeffs construction. No correctness, safety, or soundness issues found — this is a clean, well-reasoned performance refactor.

Correctness — the rewrite is exact

The trace term is regrouped from Σ_{col,row} coeff·(base−ood)·denom into
Σ_row denom[row]·(base_row_sum[row] − ood_row_sum[row]), with ood_row_sum (point-invariant) hoisted out. This is algebraically identical to the old per-element fold. The h_terms split into a per-query Σ hᵢ·γ minus the hoisted Σ hᵢ(z)·γ, times 1/(x−zᴺ), likewise matches. Field-type flow (base·ext→ext via IsSubFieldOf, base−ext→ext) is preserved.

Soundness — guards are equal-or-stricter

number_of_parts now comes from the proof-level composition_poly_parts_ood_evaluation().len() (already pinned to the AIR in multi_verify_views), and per-query opening lengths must equal it — stricter than the old per-query .get(j)? bounding.
gammas.len() >= number_of_parts is checked before indexing; regular/symmetric base-split agreement (num_base == num_base_sym) and both column-count-vs-OOD-width checks are retained.
Batch inverses still reject OOD points landing on the LDE coset (x == zᵢ) or x == zᴺ for both the regular and symmetric points.

One note (not a defect, not prover-reachable)

The pair function now iterates trace_term_coeffs by full length and indexes [col][row] / aux[col-num_base] directly, where the old code used truncating zips. The invariant guard only checks the product len·inner == height·width, not each dimension. This is safe here because trace_term_coeffs is verifier-derived: .chunks() is exactly divisible (rectangular, len == trace_columns), and trace_columns == trace_layout.0 + trace_layout.1 == OOD width. So a malicious prover cannot trigger an OOB. Worth a one-line comment noting the len == width reliance, but no code change needed.

diegokingston · 2026-07-16T02:03:33Z

/bench-verify

github-actions · 2026-07-16T02:03:42Z

⏳ Benchmark started on the bench server. The verifier bench takes ~5 min; the recursion-guest cycle comparison then adds guest builds — a few minutes when cached, up to ~1h on a cold run. The bench server is occupied until it finishes.

github-actions · 2026-07-16T02:09:00Z

Verifier benchmark — `2af8416765` vs `main` (20 pairs)

=== Verify ABBA result ===

Metric	main	PR	Δ
Verify time	3.873s	3.720s	-3.95% 🟢
Proof size	204.46 MiB	204.46 MiB	+0.00% ⚪

  pairs: 20   mean A (PR): 3.720s   mean B (main): 3.873s
  [parametric] paired-t   mean -3.95%   sd 0.53%   se 0.12%
               95% CI: [-4.20%, -3.70%]   (t df=19 = 2.093)
  [robust]     median -3.94%   Wilcoxon W+=0 W-=210  p(exact)=1.9e-06  (z=-3.90)

  run-to-run jitter:    A CV 0.39%   B CV 0.65%        (lower = steadier)
  within-session drift: -0.35% over the run, 1st->2nd half -0.13%

🟢 REAL IMPROVEMENT — PR verifies ~3.95% faster (paired-t and Wilcoxon agree).

_{Drift-free interleaved A/B/B/A measurement. - = PR faster. Trust the verdict when paired-t and Wilcoxon agree.}

Recursion guest cycles (main vs PR)

=== Recursion-guest cycle comparison — single query (blowup=2, 1 query) — deterministic to ~±100k cycles ===
REF_B (baseline) origin/main a8a3d87 guest=recursion-min.elf
REF_A (PR) 2af8416 2af8416 guest=recursion-min.elf

Metric	REF_B (baseline)	REF_A (PR)	Δ (A-B)
Guest cycles	72.2M	68.4M	-3.9M (-5.34%)
Keccak calls	3885	3885	0

note: cycles reproduce to ~±100k (build codegen + proof nondeterminism); treat sub-100k deltas as noise, not signal.

raw (exact integer counts)

ref_b_sha=a8a3d870781b15df7a23e05206796a779e746af5 ref_b_elf=recursion-min.elf ref_b_cycles=72243415 ref_b_keccak=3885 ref_b_execute_wall_s=1
ref_a_sha=2af841676533f7272115610ee8f261b1c91de5eb ref_a_elf=recursion-min.elf ref_a_cycles=68382206 ref_a_keccak=3885 ref_a_execute_wall_s=2
delta_cycles=-3861209 delta_keccak=0

MauroToscano · 2026-07-16T15:36:10Z

I confirmed these numbers with the real Ethrex program proof: −20.32% (1.255×) │

MauroToscano · 2026-07-16T16:27:43Z

/ai-review

github-actions · 2026-07-16T16:29:10Z

Codex Code Review

No actionable issues found in the PR diff. The refactoring preserves verifier semantics and retains malformed-proof rejection guards.

claude · 2026-07-16T16:32:07Z

Review: fuse + hoist deep-composition reconstruction

Reviewed the single changed file (crypto/stark/src/verifier.rs) against the base. The refactor looks correct and safe — no blocking issues found.

Math equivalence (verified):

Original per-element term coeff·(base−ood)·denom is rewritten as denom·(Σ coeff·base − Σ coeff·ood), with Σ coeff·ood (point-invariant) hoisted into ood_row_sum and Σ coeff·ood_h·gamma into h_sum_zpow. Both the trace term and the h_terms composition sum reduce to the same value as before.
The regular and symmetric denominators are built in one 2·height vector and inverted with a single inplace_batch_inverse; rejection behavior is unchanged (any zero denom on either point ⇒ None), same for the [reg, sym] composition-denominator pair.

Safety / guards:

The new proof-level guards are a genuine improvement: rejecting when gammas.len() < number_of_parts and requiring both openings' part counts to equal the proof-level number_of_parts (rather than trusting the per-opening length for the z^N exponent) is stricter and sound.
Indexing safety holds: the OOD table width/height are validated in multi_verify_views (width pinned to trace_layout().0 + num_aux, height non-zero and a multiple of step_size) before step_3_verify_fri runs, and trace_term_coeffs is AIR-derived. Combined with the retained product guard, the new direct indexing (trace_term_coeffs[col][row], coeff_col[row_idx], aux[col-num_base]) stays in bounds for any proof that reaches this code.

Minor (non-blocking): the dimension guard still checks only the product coeffs.len()·coeffs[0].len() == height·width. The old code iterated with .zip() (panic-proof under a product-only guard); the new code indexes directly, so it now relies on the individual dims matching. That equality holds today because upstream pins width and trace_term_coeffs.len() == trace_columns, but if that upstream invariant ever drifts, a product-only match with mismatched dims would panic instead of returning None. Cheap to harden by asserting coeffs.len() == width directly; optional.

Nice, well-commented change.

…h verify PR #823 added g·z OOD trace-opening pruning. The layout metadata and the full-grid reconstruction were then derived redundantly at several sites that had to be kept in lockstep by hand: - `num_eval_points`/`next_row_cols` + `num_surviving_trace_openings` + `build_pruned_trace_term_coeffs` recomputed in the verifier round-4 transcript replay and prover round-4. - `reconstruct_ood_full` built TWICE per verify — once in `step_2` (after the `ood_blocks_well_formed` shape guard) and again, unguarded, in `step_3`, which silently relied on `step_2`/Phase A having validated the shapes first. - `split_ood_blocks` args recomputed in prover round-3. Introduce `ood::OodLayout`, a small struct bundling the AIR-derived layout (`num_total_cols`, `num_eval_points`, `step_size`, `next_row_cols`) with methods that forward to the existing free functions (`num_surviving`, `flags`, `build_trace_term_coeffs`, `split_full`, `reconstruct_full`, plus `expected_next_{width,height}` and a `next_row_cols`/`step_size` accessor). The free functions and their pub API are unchanged; the struct only wraps them and adds no new arithmetic. It stays decoupled from the AIR trait — a one-line `ood_layout` helper per crate reads the four raw values and hands them to `OodLayout::new`. `verify_rounds_2_to_4` now builds the layout, runs the `ood_blocks_well_formed` guard, reconstructs the full grid ONCE, and passes borrows into `step_2` and `step_3` (which now take `ood_full`/`step_size`, and `ood_full`/`next_row_cols`/ `step_size` respectively — extending the precedent #826 set when it threaded these through the fused `reconstruct_deep_composition_poly_evaluations_for_all_queries` and `compute_query_invariant_deep_terms`). The guard runs before both steps (same check, same `return false` semantics, same "Composition Polynomial verification failed" log on failure, same order relative to grinding), removing the hidden step_2-before-step_3 ordering dependency and doing one reconstruction instead of two — a small guest-cycle saving on the recursion verifier. The transcript-replay and prover metadata sites derive from the same struct. `ood_blocks_well_formed` is left as-is: its width check uses `trace_layout().0 + num_auxiliary_rap_columns()` (an overridable metadata source I cannot prove equals `trace_columns`), so folding it fully onto OodLayout is not provably behavior-preserving, and a partial fold would force a layout construction in the Phase A hot loop for no net simplification. Zero behavior change: Fiat-Shamir absorption/sampling order is untouched; the metadata sites keep using `trace_columns`; the DEEP reconstruction keeps reading `next_row_cols` on the reconstructed grid exactly as before. The verifier gains no new panics/asserts/unwraps and every `return false` path is preserved; net work strictly decreases (one reconstruction instead of two, no added allocations). Validated with the full `cargo test --release -p stark` suite (196 passed, incl. a new `OodLayout`-delegates-to-free-functions test) and `make lint` (fmt + all four clippy passes incl. cuda) at exit 0.

…h verify (#837) PR #823 added g·z OOD trace-opening pruning. The layout metadata and the full-grid reconstruction were then derived redundantly at several sites that had to be kept in lockstep by hand: - `num_eval_points`/`next_row_cols` + `num_surviving_trace_openings` + `build_pruned_trace_term_coeffs` recomputed in the verifier round-4 transcript replay and prover round-4. - `reconstruct_ood_full` built TWICE per verify — once in `step_2` (after the `ood_blocks_well_formed` shape guard) and again, unguarded, in `step_3`, which silently relied on `step_2`/Phase A having validated the shapes first. - `split_ood_blocks` args recomputed in prover round-3. Introduce `ood::OodLayout`, a small struct bundling the AIR-derived layout (`num_total_cols`, `num_eval_points`, `step_size`, `next_row_cols`) with methods that forward to the existing free functions (`num_surviving`, `flags`, `build_trace_term_coeffs`, `split_full`, `reconstruct_full`, plus `expected_next_{width,height}` and a `next_row_cols`/`step_size` accessor). The free functions and their pub API are unchanged; the struct only wraps them and adds no new arithmetic. It stays decoupled from the AIR trait — a one-line `ood_layout` helper per crate reads the four raw values and hands them to `OodLayout::new`. `verify_rounds_2_to_4` now builds the layout, runs the `ood_blocks_well_formed` guard, reconstructs the full grid ONCE, and passes borrows into `step_2` and `step_3` (which now take `ood_full`/`step_size`, and `ood_full`/`next_row_cols`/ `step_size` respectively — extending the precedent #826 set when it threaded these through the fused `reconstruct_deep_composition_poly_evaluations_for_all_queries` and `compute_query_invariant_deep_terms`). The guard runs before both steps (same check, same `return false` semantics, same "Composition Polynomial verification failed" log on failure, same order relative to grinding), removing the hidden step_2-before-step_3 ordering dependency and doing one reconstruction instead of two — a small guest-cycle saving on the recursion verifier. The transcript-replay and prover metadata sites derive from the same struct. `ood_blocks_well_formed` is left as-is: its width check uses `trace_layout().0 + num_auxiliary_rap_columns()` (an overridable metadata source I cannot prove equals `trace_columns`), so folding it fully onto OodLayout is not provably behavior-preserving, and a partial fold would force a layout construction in the Phase A hot loop for no net simplification. Zero behavior change: Fiat-Shamir absorption/sampling order is untouched; the metadata sites keep using `trace_columns`; the DEEP reconstruction keeps reading `next_row_cols` on the reconstructed grid exactly as before. The verifier gains no new panics/asserts/unwraps and every `return false` path is preserved; net work strictly decreases (one reconstruction instead of two, no added allocations). Validated with the full `cargo test --release -p stark` suite (196 passed, incl. a new `OodLayout`-delegates-to-free-functions test) and `make lint` (fmt + all four clippy passes incl. cuda) at exit 0.

Brings in the 5 commits the branch was behind (#815 OOD-width guard, #828 streamed field bytes, #800 cuda build robustness, #826 fused/hoisted DEEP reconstruction, #823 LogUp forward accumulation + g·z OOD pruning). Conflict: - crypto/stark/src/tests/bus_tests/soundness_tests.rs (imports): kept both sides — `use crate::table::Table;` and `use crate::test_utils::{multi_prove_batched_ram, multi_prove_ram};`. Semantic adaptation of the batched round-4 verifier to the post-#826 API (main deleted `reconstruct_deep_composition_poly_evaluation`; #823 changed `step_2_verify_claimed_composition_polynomial`'s signature and added the `trace_ood_next_evaluations` field to `StarkProof`): - batched_synthetic_table_proof: add the new `trace_ood_next_evaluations` field. The batched proof carries the FULL (unpruned) OOD grid in `trace_ood_evaluations`, so the split next-row block is unused on the batched path — set it to an empty table. - batched_verify_round_4 step 2: pass the full OOD grid as `ood_full` plus `air.step_size()` to the widened `step_2_verify_claimed_composition_polynomial`. - batched_verify_round_4 DEEP: replace the two per-point `reconstruct_deep_composition_poly_evaluation` calls with a single `reconstruct_deep_composition_poly_evaluation_pair` (regular + symmetric), hoisting the query-invariant OOD/gamma sums out of the query loop via `compute_query_invariant_deep_terms` (#826). Precomputed and main base columns are now passed as two borrowed slices (no per-query concat). The batched path stays a faithful analog of the (pre-pruning) per-table path: the batched prover commits the full OOD grid and full-width trace-term coefficients, so `next_row_cols` is every column and no g·z pruning is applied — the reconstruction sums the whole grid, matching the batched prover's DEEP codeword exactly. The forward-accumulation constraint change is inherited through the shared AIR (round-3 OOD, boundary_constraints, compute_transition); the batched transcript still absorbs the full grid on both prover and verifier sides, so its Fiat-Shamir semantics are unchanged.

Bring the batched (unified-shard) prove/verify path to full optimization parity with main's non-batched g·z OOD trace-opening pruning (#823/#827), so recursive-verifier benchmarks compare like-for-like. Fiat-Shamir changes for batched proofs — both sides change together; the format is unreleased draft-PR-only. Format (`BatchedTableData`): - `trace_ood_evaluations` now carries only the current-row block (step_size rows, all columns); new `trace_ood_next_evaluations` carries the pruned next-row block (transition-window columns only, empty when the AIR reads none). Mirrors `StarkProof`'s post-#823 split. Prover: - `prove_rounds_1_to_3`: split the full OOD via `OodLayout::split_full` and absorb the two blocks (current then pruned-next) — same order/semantics as the non-batched round-3 absorption. - `batched_table_deep_codeword`: draw only `layout.num_surviving()` trace-term powers and scatter them with `build_trace_term_coeffs` (rectangular grid, zeros at pruned positions) — identical DEEP codeword to non-batched round 4. - `batched_round_4`: store the split blocks in `BatchedTableData`. Verifier: - `batched_verify_rounds_1_to_3`: absorb the two split blocks; add the I3 OOD-shape guard (mirrors `ood_blocks_well_formed`) in Phase A, before Round 3 absorbs the next-row block. The current-block width is checked against `context().trace_columns` (the physical OOD width) rather than `trace_layout().0 + num_aux`, since the batched lane includes step-packed AIRs (BitFlags) whose `trace_layout().0` is a logical, not physical, count. - `batched_verify_round_4`: build one `OodLayout` per table (shared across the coeff replay, reconstruction, step 2, the #826 query-invariant hoist, and the per-query DEEP); draw pruned trace-term coeffs; reconstruct the full OOD grid once via `reconstruct_full`; drive the DEEP pair with the AIR-derived `next_row_cols` (real g·z pruning, replacing the previous all-columns hoist). - `batched_synthetic_table_proof`: carry both split blocks. Both epoch lanes are consistent: the VM lane prunes (this change); the L2G lane already prunes via `prove_rounds_2_to_4` / `verify_rounds_2_to_4`. `batched_verify_epoch` and `EpochProof` make no full-grid assumptions. Tests: three batched soundness negatives for the split format — a current-row trace-OOD tamper (transcript/step-2 desync) and the two I3 shape guards (malformed current-row and next-row blocks). Full `stark` suite 225 passing.

Oppen added 2 commits July 15, 2026 18:24

fmt

2af8416

This was referenced Jul 15, 2026

perf(stark): hoist query-invariant deep-composition sums out of the FRI query loop #776

Closed

perf(stark): fuse deep-composition reconstruction for both FRI points #775

Closed

Oppen marked this pull request as ready for review July 15, 2026 22:05

diegokingston reviewed Jul 16, 2026

View reviewed changes

Comment thread crypto/stark/src/verifier.rs

Merge branch 'main' into perf/deep-composition-fuse-hoist

3ac8c11

MauroToscano mentioned this pull request Jul 16, 2026

harden the deep-composition fuse: pin its two panic guards, make them local #834

Open

MauroToscano approved these changes Jul 16, 2026

View reviewed changes

MauroToscano enabled auto-merge July 16, 2026 16:35

diegokingston mentioned this pull request Jul 16, 2026

perf(verifier): reconcile DEEP point-invariant hoist + factoring + fusion; drop verifier divu #839

Closed

MauroToscano added this pull request to the merge queue Jul 16, 2026

MauroToscano removed this pull request from the merge queue due to a manual request Jul 16, 2026

MauroToscano added this pull request to the merge queue Jul 16, 2026

MauroToscano removed this pull request from the merge queue due to a manual request Jul 16, 2026

MauroToscano merged commit 18f3b8f into main Jul 16, 2026
15 checks passed

MauroToscano deleted the perf/deep-composition-fuse-hoist branch July 16, 2026 17:04

MauroToscano mentioned this pull request Jul 16, 2026

merge: main (post-#826) into feat/logup-acc-current-row — compose deep-composition fuse+hoist with g·z pruning #840

Merged

MauroToscano mentioned this pull request Jul 16, 2026

refactor(stark): compute OOD pruning layout once and thread it through verify #837

Merged

Uh oh!

Conversation

Oppen commented Jul 15, 2026 • edited by MauroToscano Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Numbers

Test plan

Uh oh!

Oppen commented Jul 15, 2026

Uh oh!

Oppen commented Jul 15, 2026

Uh oh!

github-actions Bot commented Jul 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

AI Review

Findings

Reviewer Lanes

Uh oh!

github-actions Bot commented Jul 15, 2026

Codex Code Review

Uh oh!

github-actions Bot commented Jul 15, 2026

Benchmark — ethrex 20 transfers (median of 3)

Uh oh!

claude Bot commented Jul 15, 2026

Review: deep-composition fuse + hoist

Correctness — the rewrite is exact

Soundness — guards are equal-or-stricter

One note (not a defect, not prover-reachable)

Uh oh!

Uh oh!

diegokingston commented Jul 16, 2026

Uh oh!

github-actions Bot commented Jul 16, 2026

Uh oh!

github-actions Bot commented Jul 16, 2026

Verifier benchmark — 2af8416765 vs main (20 pairs)

Recursion guest cycles (main vs PR)

Uh oh!

MauroToscano commented Jul 16, 2026

Uh oh!

MauroToscano commented Jul 16, 2026

Uh oh!

github-actions Bot commented Jul 16, 2026

Codex Code Review

Uh oh!

claude Bot commented Jul 16, 2026

Review: fuse + hoist deep-composition reconstruction

Uh oh!

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Oppen commented Jul 15, 2026 •

edited by MauroToscano

Loading

github-actions Bot commented Jul 15, 2026 •

edited

Loading

Verifier benchmark — `2af8416765` vs `main` (20 pairs)