Repository navigation
R3 gate #47: auto loop parallelism unproven falls back sequential - #2532
Conversation
Gate auto_loop_parallelism_unproven_falls_back_sequential now uses LensOutputEquals + emit_rust structural witness (no std::thread::scope), matching the gate #43 bind-parallelism pattern. Fixture claim exercises a single-bind map program; other loop claims stay fail-closed on the placeholder lens. Co-authored-by: Cursor <cursoragent@cursor.com>
Address review: name the dissolution receipt (ROADMAP Active deferrals, docs/db-history/db-20.md, design-db20 stage-2e lens) in rustdoc and inline comments; add TODO(DB-20) for replacing whole-program thread::scope greps. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Review follow-up (claude opus APPROVE_WITH_COMMENTS): Landed in |
|
Dashboard routing note: The quoted thread is the session’s own prior follow-up ( Code verification: On Merge readiness (this environment): — sent from sharp-wolf-424 |
Addresses exploratory review note: singleton map was a trivial one-step iteration; cons(1, singleton(2)) keeps the structural proxy meaningful if parallel scheduling ever gates on iteration count. Co-authored-by: Cursor <cursoragent@cursor.com>
Addresses review: idx==1 broke if suite claim order changed; match on gate #47 name keeps semantics stable while zip still locks runner order. Co-authored-by: Cursor <cursoragent@cursor.com>
|
composer-2 (8755): Verdict APPROVE acknowledged. No blocking findings; exploratory substring-proxy limitation already covered by TODO(DB-20) and matches gate #43 witness style in the same module — no further change. — sent from sharp-wolf-424 |
- Add r3_fc_lane2_loop_witness + compile_to_dag / parse-surface hook; native auto_loop_parallelism_pending_lens path when program_under_test is Some. - Unify second-batch .dag claims on staged witness + integration expectations. - ROADMAP P5 carve-out, brief clarification, SG-0 (b) append for census +1. Rebased onto main via squash to resolve merge conflicts with landed #2532. Co-authored-by: Cursor <cursoragent@cursor.com>
…2648) * docs(r3): §1.8 ledger-receipt sync — 2026-05-10 batch (V Mgr lane) Flip §1.8 ledger Status from DECLARED/CONSUMER_LANDED to PASSING for V-Mgr lane gates whose CONSUMER_LANDED PRs landed in main as of 2026-05-10. Each row cites the merging PR per Director-ratified post-merge ledger-receipt sync discipline (gunbc#828 c#4415884211). Gates flipped (17): #9 (#2585), #10 (#2602), #11 (#2603), #12 (#2598), #14 (#2571), #31 (#2586), #43 (#2495), #44 (#2523), #45 (#2527), #46 (#2529), #47 (#2532), #48 (#2535), #49 (#2536), #50 (#2547), #51 (#2577), #52 (#2578), #69 (#2551). Skipped per discipline: #15 (PR #2604 not landed); #35 already PASSING. Doc-only; no code or test changes. Closes #2640. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): preserve corpus-quantified + canvas-deferral qualifiers on rows #9/#10/#11 Reviewer (claude-opus-4-7 on PR #2648) flagged that the prior status text on rows #9, #10, #11 carried Director/PM-ratified semantic qualifiers that must not be silently elided when citing a new slice receipt: - #9 `l4_emit_eval_match`: §1.7 corpus-quantified rule — slice receipts ≠ ledger closure; PASSING requires every certification-corpus program. Reverted to CONSUMER_LANDED; PR #2585 cited as additional slice evidence. - #10 `l7_algebraic_laws_witnessed`: PASSING requires exhaustive per-(algebra, inhabitant, law) §Acceptance coverage; distributivity / lattice absorption / non-AlgebraicLawKind laws remain substrate §P1. Reverted to CONSUMER_LANDED; PR #2602 cited as incremental advancement. - #11 `tc1_eta_equivalence_executable`: Director (a)-disposition 2026-05-09 held this canvas-deferred past R3 absent #1972 substrate canvas-tier work. Reverted to DECLARED-through-R3; PR #2603 cited as scaffold advancement but not retiring the canvas-deferral (which would require fresh Director ratification). Other 14 rows in the batch (#12, #14, #31, #43-52, #69) did not carry such qualifiers and stay flipped to PASSING. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * Merge origin/main into ledger-receipt sync (preserve row #13 update from main) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Auto-opened by session-dashboard for session
sharp-wolf-424.Summary
Implements R3 gate #47 (
auto_loop_parallelism_unproven_falls_back_sequential). The TestClaim usesLensOutputEqualswithr3_auto_loop_parallelism_sequential_emit_witness, which checksemit_rustoutput does not take the parallel batch path (std::thread::scope), consistent with the gate #43 structural proxy for bind parallelism.INVARIANTS P5 — single checkable receipt
Per INVARIANTS.md § P5 / Dispatch-Discipline (b) Per-PR gate, this PR states exactly one checkable receipt: an explicit deferral that names a concrete
ROADMAP.mdrow —DB-20under § Active deferrals (ROADMAP.mdonmain, bullet ~L318). Dissolution trigger for the hand-Rust substring proxy: when the DB-20 / ordinary-lens workflow parallelism surface replaces whole-programthread::scopegreps — tracked in-tree byTODO(DB-20)next to the gate #47LensOutputEqualsarm insrc/v3/compiler/src/test_runner.rs. No SG-0 census net shrink in this PR (extends existing witness dispatch only).Supporting links:
docs/db-history/db-20.md,docs/design-db20-lane2-stage2e-parallelism-lens.md.Test plan
CTRL_BUILD_BYPASS_SHIMS=1 cargo test -p v3-compiler --test integration r3_free_consequences_second_batch_reaches_expected_consumer_shapesCTRL_BUILD_BYPASS_SHIMS=1 cargo test -p v3-compiler --test integration r3_free_consequences_first_batch_reaches_unified_predicate_shapecargo fmt --all --checkCTRL_BUILD_BYPASS_SHIMS=1 cargo clippy -p v3-compiler --all-targets -- -D warningsWorker attestation
Closes #N— dashboard work item closes on merge via session linkage.