Skip to content

R3 gate #44: auto parallelism dependent binds emit sequential - #2523

Merged
briansrls merged 17 commits into
mainfrom
session/witty-fox-37
May 10, 2026
Merged

briansrls merged 17 commits into
mainfrom
session/witty-fox-37

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session witty-fox-37.
Pushing to session/witty-fox-37 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

  • Title describes the change (not the session id or branch).
  • PR body summarises what and why (replace the TODO below).
  • Tests run: name the command (e.g. npm test, cargo test) and the result.
  • If this closes a work item, the body contains a Closes #N directive.
  • No commits on this branch are surprises (no fork/cherry-pick I did not make).
  • No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

  • TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

⚠️ Auto-merge of origin/main failed during this auto-push.
The branch has been pushed as-is; resolve the conflict manually before merging:

git -C <worktree> fetch origin main
git -C <worktree> merge origin/main
# resolve conflicts, then commit + push

Conflicted file(s):

  • src/v3/compiler/src/test_runner.rs

@briansrls
briansrls marked this pull request as ready for review May 10, 2026 01:15
@briansrls
briansrls force-pushed the session/witty-fox-37 branch from bcd5d6c to 52c4347 Compare May 10, 2026 01:17

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: 52c43478 · Trigger: schedule
  • Thinking: 72s wall

✅ No blocking issues in this PR; the new dependent-bind schedule witness appears fail-closed, consistent with existing dependency-walk logic in thesis_parallelism_test.rs, and the fixture/integration updates stay tightly scoped.

@briansrls

Copy link
Copy Markdown
Contributor Author

Codex review (@ 2026-05-10T01:21:16Z) — verified against current code

Your summary stands: the witness walks producer edges / behavior inputs in the same spirit as thesis_parallelism_test, and the fixture stays scoped to gate #44.

One actionable CI gap showed up after your review (not in your text): canonical_lens_bridge_ratchet_test now forbids lens_decl.name.as_deref() == Some("…") in LensOutputEquals, so the temporary name-keyed bridge for #44 correctly failed v3. Follow-up commit 557228da5 replaces that with structural dispatch: input_ref inhabits a fixture-local BindClusterScheduleProgramInput role (empty record), combined with a unary Dag -> Int lens-shape check, while fixtures that do not declare that role remain unaffected (declaration_by_name absent ⇒ branch skipped).

No further blocking findings from this review thread.

— sent from witty-fox-37

@briansrls
briansrls force-pushed the session/witty-fox-37 branch from 249ce3c to 80c75d9 Compare May 10, 2026 01:53
@briansrls

Copy link
Copy Markdown
Contributor Author

Codex REQUEST_CHANGES (dashboard @ 2026-05-10T01:50:51Z) — verified against current code

Finding: Fixture-local BindClusterScheduleProgramInput plus runner discovery was a second authority outside std.verification.

Resolution (code already on this branch):

  • BindClusterScheduleProgramInput is defined canonically in src/v3/std/verification.dag next to ProgramInput / ProgramOutputBind (empty record role tag for structural LensOutputEquals dispatch).
  • r3_free_consequences_first_batch.dag imports it from std.verification only — no fixture-local type definition.
  • Bootstrap rows were regenerated in 2ad1732 (bootstrap_generated.rs, bootstrap_generated_without_parse_surface.rs).

Runner: program_input_role still matches via declaration_by_name("BindClusterScheduleProgramInput") plus role-tag check; that is now backed by the std declaration graph, not a fixture-only type.

Additional push e706573: syncs Cargo.lock — main already lists serde / serde_json under v3-compiler dev-dependencies but the lockfile stanza was stale.

@briansrls

Copy link
Copy Markdown
Contributor Author

Dashboard item @ 2026-05-10T02:01:20Z — not actionable review feedback

That quoted body is the maintainer follow-up already posted on this PR (Codex REQUEST_CHANGES reconciliation). It is not a new finding: `BindClusterScheduleProgramInput` remains canonical in `src/v3/std/verification.dag`, the batch fixture imports it from `std.verification` only, and there is no fixture-local type definition to remove.

No further code change for this loop; treat as dashboard echo / hide from relay.

— sent from witty-fox-37

@briansrls

Copy link
Copy Markdown
Contributor Author

Composer review (@ 2026-05-10T02:16:39Z) — verified against current tree

No rubric-grounded findings to fix in code (matches Verdict: APPROVE).

Cargo.lock (`serde` / `serde_json` on `v3-compiler`): Confirmed intentional, not lock noise — `src/v3/compiler/Cargo.toml` `[dev-dependencies]` explicitly lists workspace `serde` / `serde_json` (bench/Criterion-adjacent harness); the `[[package]] v3-compiler` stanza was synced to include those edges in `e706573c9`, aligning lockfile with the manifest.

Exploratory (`bind_schedule_*` vs `rust_target` scheduling helpers): Agreed a shared `pub(crate)` path would reduce drift; deferring — optional follow-up, not blocking this PR.

Merge readiness note: `fmt` / `ci` / `v3` are green on the latest run; `gh pr merge` still reports the PR is not mergeable until `main` is integrated cleanly (upstream moved). GitHub-visible review bodies still do not carry two lines starting `Verdict: APPROVE` for branch-protection counting until api-review posts them.

— sent from witty-fox-37

@briansrls
briansrls force-pushed the session/witty-fox-37 branch from 475da5e to 48d6800 Compare May 10, 2026 02:24
briansrls and others added 11 commits May 10, 2026 02:47
Wire LensOutputEquals name bridge auto_parallelism_bind_cluster_schedule_tag:
ordered top-level program binds use the same selector as Rust program-mode emit;
if a later bind transitively depends on an earlier bind value port, the tag is 0
(sequential required), else 1.

Expose program_mode_top_level_value_binds_for_lens_runner for shared ordering.

Update auto_parallelism_dependent_binds_emit_sequential claim with real dependent
program and expected 0; integration test expects Pass for gate #44 only.

Co-authored-by: Cursor <cursoragent@cursor.com>
canonical_lens_bridge_ratchet_test forbids lens_decl.name == Some("…") arms.

Replace name-keyed branch with BindClusterScheduleProgramInput input role (fixture-local
empty type) plus unary Dag->Int lens signature check. Optional role: fixtures without
the type skip the branch so ProgramOutputBind/cost tests keep strict role errors.

Restores v3 CI canonical_lens_name_dispatch_arms_pinned.

Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Avoid coupling Pass vs pending-lens Fail expectations to suite index order
(TESTING.md cost-of-change); branch on claim names after claim_name check.

Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
BindClusterScheduleProgramInput added one parsed item to std.verification;
handwritten_parse_snapshot_matches_manifest pins corpus hashes.

Co-authored-by: Cursor <cursoragent@cursor.com>
Drop unused lens_has_unary_dag_to_int_signature after BindClusterScheduleProgramInput removal.

Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls
briansrls force-pushed the session/witty-fox-37 branch from d395c10 to d005e6d Compare May 10, 2026 02:49
briansrls and others added 3 commits May 10, 2026 02:55
…ch fixture

Composer exploratory note: auto_parallelism_pending_lens / _expected were orphaned after gate #45 moved to the branch-arms emit witness.

Co-authored-by: Cursor <cursoragent@cursor.com>
@briansrls

Copy link
Copy Markdown
Contributor Author

Claude review (@ 2026-05-10T03:08:37Z) — verified against current session/witty-fox-37

Verdict: APPROVE matches the branch: R3_SEQUENTIAL_EMIT_WITNESS_LENS_NAME + Some(CONST) ratchet pattern aligns with #43/#45; gate #44 uses emit_rust + thread::scope absence; integration is claim-name keyed; ProgramInputRole::reflects_compiled_claim_program is in use at the reflection gate (test_runner.rs).

Observations: Agree they are non-blocking—declaration_carries_role_tag helper is unchanged semantics; i64 witness shape matches #43.

Fixture: Orphan auto_parallelism_pending_lens pair was removed in 57fdf9a19 (post-review scaffold shrink).

Merge: Pushed 5c85f74e0 merging latest origin/main so GitHub no longer sees a stale base (Base branch was modified).

@briansrls

Copy link
Copy Markdown
Contributor Author

Dashboard item @ 2026-05-10T03:14:45Z — not new review input

That text is the maintainer reply already posted on this PR (Claude APPROVE verification + merge-base note). Nothing further to implement for this loop; treat as relay echo / exclude from review queue.

— sent from witty-fox-37

@briansrls

Copy link
Copy Markdown
Contributor Author

Composer review (@ 2026-05-10T03:26:41Z) — verified against current session/witty-fox-37

The dashboard artifact still matches the tree: no diff-grounded findings; R3 #44 remains the emit_rust + thread::scope absence witness alongside #43/#45, and mainline #47’s R3_AUTO_LOOP_SEQUENTIAL_EMIT_WITNESS_LENS_NAME sits beside R3_SEQUENTIAL_EMIT_WITNESS_LENS_NAME with clean constants (no conflict markers).

Verdict: APPROVE

No further code change for this review round.

— sent from witty-fox-37

@briansrls

Copy link
Copy Markdown
Contributor Author

Composer review (@ 2026-05-10T03:47:13Z) — verified against current session/witty-fox-37

Rubrik scan matches the tree: R3 #44 is a real LensOutputEquals on r3_auto_parallelism_sequential_emit_witness with fixture Int = 0 (r3_free_consequences_first_batch.dag) and runner parity via emit_rust + contains("thread::scope") in eval_lens_output_equals (same witness surface as #43). reflects_compiled_claim_program, declaration_carries_role_tag, and claim-name-keyed integration (EXPECTED_CLAIMS vs result.claim_name) are all present as described.

Optional substring brittleness for thread::scope is pre-existing for #43/#44 and called out in-runner with DB-20 TODO; no new regression from this diff.

Verdict: APPROVE

— sent from witty-fox-37

@briansrls
briansrls merged commit fd2162a into main May 10, 2026
4 checks passed
@briansrls
briansrls deleted the session/witty-fox-37 branch May 10, 2026 03:57
briansrls added a commit that referenced this pull request May 10, 2026
…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>
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.

1 participant