Repository navigation
Conversation
Node overrides allowed force-mocking any node regardless of its port types, bypassing the structural transport interception design. This removes the entire mechanism: - BoundaryMocks: remove node_overrides field, set/get methods - execute_flat: remove node override check and tool acquisition skip - MockSpec: remove NodeOverride struct, builder method, and conversion - lib.rs: remove NodeOverride re-export - CI graph_mock: convert .node_override() to .transport_mock() calls All I/O nodes should go through the transport layer so they are structurally interceptable in DryRun mode without escape hatches. https://claude.ai/code/session_01CcSU24DtcsjFcC7jztUrKh
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 315e5a983d
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Comment on lines
+92
to
+95
| .transport_mock("clippy_lint", "success", Value::Bool(true)) | ||
| .transport_mock("clippy_lint", "stdout", Value::Str(String::new())) | ||
| .transport_mock("clippy_lint", "stderr", Value::Str(String::new())) | ||
| .transport_mock("clippy_lint", "skip", Value::Bool(false)) |
There was a problem hiding this comment.
These transport_mock entries won’t be used because DryRun interception only applies to transport executor nodes (inputs include TransportRequest; see is_transport_execution_node in core/exec/src/execute.rs), while clippy_lint is a CliToolOp with only a skip input. As a result, execute_with_mode(DryRun) will still acquire/run clippy, so the flow tests (and any DryRun runs) will perform real tool I/O or fail if clippy isn’t installed. With node overrides removed, this mock needs to move to a transport node or another mocking mechanism for CLI ops.
Useful? React with 👍 / 👎.
briansrls
added a commit
that referenced
this pull request
Apr 7, 2026
- #13/#14: is_valid_proof now validates proof.dimensions against edge evidence lengths (fail-closed on mismatch). proof_has_non_descending_cycle passes the actual TerminationProof instead of fabricating an empty one. - #20: ComplexityViolation.reason now carries the structural root cause from CostUnknown (e.g., "same-argument recursion in X") instead of the asymptotic class string. Added extract_unknown_reason helper. - #21: ComplexityViolation now carries the function's SourceSpan from FuncEntry. complexity_diagnostics propagates v.span instead of no_span(). - CI: DIAG_RATCHET updated 316 → 526 to match honest violation count after CostUnknown restoration. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 3, 2026
Row #13 must not bundle INFER_HELPERS_SOURCE with compile_to_dag canonical-lens include_str bridges: test_runner only substring-scans it for census ratchets, and canonical_lens_bridge_ratchet_test.rs excludes it from Category A per P2 single-authority mapping. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
added a commit
that referenced
this pull request
May 3, 2026
…include_str overlap Codex blocking review (951f8d7 family-boundary): row #13 fix landed in 384a47e; this commit removes residual INFER_HELPERS_SOURCE coupling from the ledger mapping table so SourceSpan/file vs exact-string census lanes stay distinct. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
added a commit
that referenced
this pull request
May 3, 2026
…1591) * WIP: royal-newt-846 * docs(r3): correct SourceSpan audit — INFER_HELPERS out of row 13 Row #13 must not bundle INFER_HELPERS_SOURCE with compile_to_dag canonical-lens include_str bridges: test_runner only substring-scans it for census ratchets, and canonical_lens_bridge_ratchet_test.rs excludes it from Category A per P2 single-authority mapping. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(r3): tighten bridge_ledger mapping — exclude infer_helpers from include_str overlap Codex blocking review (951f8d7 family-boundary): row #13 fix landed in 384a47e; this commit removes residual INFER_HELPERS_SOURCE coupling from the ledger mapping table so SourceSpan/file vs exact-string census lanes stay distinct. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
added a commit
that referenced
this pull request
May 4, 2026
…rity.rs is structural-read (#1597) * WIP: royal-newt-846 * docs(r3): correct SourceSpan audit — INFER_HELPERS out of row 13 Row #13 must not bundle INFER_HELPERS_SOURCE with compile_to_dag canonical-lens include_str bridges: test_runner only substring-scans it for census ratchets, and canonical_lens_bridge_ratchet_test.rs excludes it from Category A per P2 single-authority mapping. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(r3): tighten bridge_ledger mapping — exclude infer_helpers from include_str overlap Codex blocking review (951f8d7 family-boundary): row #13 fix landed in 384a47e; this commit removes residual INFER_HELPERS_SOURCE coupling from the ledger mapping table so SourceSpan/file vs exact-string census lanes stay distinct. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(r3): fix bridge_include_str ledger row — pipeline_authority is not compile_to_dag include_str P2 mapping: bridge_include_str_side_channels_retired ties to pipeline_authority for the rejected embed/read_to_string story and Unparsed compile-body gap, not as an active parallel-Dag include_str consumer (per module comment :32-44). Co-authored-by: Cursor <cursoragent@cursor.com> * docs(r3): audit PB-1-e regen path — include_str uses tokenize/parse/lower, not compile_to_dag P1 authority-path accuracy: bootstrap_regen_fresh load_fixtures/parse_fixture never calls compile_to_dag; ledger overlap row and intro now split runner compile_to_dag embeds from PB-1-e phased lowering. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Cursor <cursoragent@cursor.com>
This was referenced May 4, 2026
This was referenced May 6, 2026
Merged
briansrls
added a commit
that referenced
this pull request
May 6, 2026
* WIP: R3 Verification * WIP: R3 Verification * WIP: R3 Verification * test(r3-l4): run each claim via run_claim; drop suite OnceLock Address api-review (PR #1802): cache only the compiled L4 `Dag` and call `TestRunner::run_claim` per `#[test]` so outcomes are not read from a shared `Vec<ClaimEvaluation>` populated by whichever test hit the OnceLock first. Removes unused `L4_SUITE` constant. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(tests): clarify OnceLock warm comment; drop PR ref in L4 helper - T-Demo `a_t_*` doc: serial libtest may warm first; parallel order not guaranteed. - L4 `l4_run_named_claim` doc: cite TESTING.md only (avoid stale PR # link). Co-authored-by: Cursor <cursoragent@cursor.com> * test(t-demo): rename skeleton smoke; drop ordering-based warm-up story Restore behavior-driven `t_demo_fixture_skeleton_compiles` and document only the fixture contract plus OnceLock compile amortization (no `a_` prefix / libtest ordering narrative). Co-authored-by: Cursor <cursoragent@cursor.com> * test(r3-l4): assert skeleton suite cardinality without index coupling Add one `run_suite(L4_SUITE)` test that checks len==3, named membership, and all Pass — restores suite-shape coverage called out in api-review. Co-authored-by: Cursor <cursoragent@cursor.com> * ci: extend self_host_ratchet job timeout to 60 minutes Cold release builds for v3-compiler (determinism_test + self_host_fixed_point) can exceed the prior 30m cap on ubuntu-latest when Actions cache misses, causing mid-compile cancellation and a failing check unrelated to PR logic. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: R3 Verification * docs(r3): advance TC1 Q-PAFS brief PROPOSAL → DESIGN Brian directive 2026-05-06: record engineering path choice (E6-G1.a static representative first; defer G1.b/X1.b generic; RustDagIsomorphism reorder only via Director). Update r3-program-plan §10.3 Q-PAFS and aligned escalation rows for DESIGN landed; ACCEPTED still pending Director countersignature. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(briefs): replace bare .md line refs with section anchors (Verification) Per Director-authorized citation discipline (#828 / checklist / 127287a pattern): Verification-touching briefs now cite § headings instead of file.md:NNN for cross-doc pointers. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: R3 Verification * docs(r3): fix Codex BLOCKING — L7 matrix cites T-V-L4-L7-Direct; sync Q-PAFS ACCEPTED - r3-v-l7-algebra-inhabitant-law-coverage-matrix: authority bullets now anchor r3-structure Summary lane T-Verification-L4-L7-Direct + Plus 3 fold-ins exhaustive witness + Acceptance l7_algebraic_laws_witnessed (not LAS gates). - r3-program-plan §10.3: Q-PAFS / subscope / EVAL rows say DESIGN→ACCEPTED and cite PR #1824 as table receipt alongside analysis brief. - TC1 analysis brief: canonical ratification = program plan §10.3; ACCEPTED footnote updated. - Add r3-v-pattern-a-tc1-v1-worker.md + link from r3-verification-manager. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(briefs): clarify r3-program-plan path for TC1 ACCEPTED authority link Co-authored-by: Cursor <cursoragent@cursor.com> * docs(r3): single authority for Q-PAFS ACCEPTED — plan §10.3 at HEAD openai-pro APPROVE_WITH_COMMENTS: PR #1824 must not read as parallel receipt vs this PR. Committed docs/r3-program-plan.md §10.3 table is sole source of truth; Co-authored-by: Cursor <cursoragent@cursor.com> #1824 is merge-record only. * docs(briefs): V1 worker — scope line is narrative not second authority openai-pro P2 wording: analysis brief is ratified scope narrative; sole authority stays program plan §10.3 at HEAD (Status line). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: R3 Verification * WIP: R3 Verification * docs(briefs): TC1 V1 brief — Director Branch B hold, unpairs argument-opaque E3 Record η non-vacuity ratification: tc1_eta_equivalence_executable stays held until Q-Reification + ReflectedProgram carrier (or explicit §1.8 revision). Clarify bold-crane pin excludes TC1 V1 until unblock; Track A otherwise unchanged. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(r3): sync §10.3 Q-PAFS/Q-EVAL with Branch B TC1 V1 hold Codex review on PR #1843: worker brief must not contradict canonical plan. Record implementation supersession (η non-vacuity + Q-Reification) in r3-program-plan.md §10.3; subordinate TC1 worker brief to that table (P2). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: R3 Verification * docs(briefs): add TC2 Pattern-A dispatch-ready worker brief Pre-auth queue (#1859): r3-v-pattern-a-tc2-v1-worker.md for gate #12 tc2_church_rosser_executable — deps P1–P6, bold-crane pin, STOP+PING, dispatch triggers. Index in r3-verification-manager.md. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(briefs): add TC3 Pattern-A dispatch-ready worker brief Pre-auth queue (#1859): gate #13 tc3_pattern_a_second_mover_executable — two-stage bundle (a)/(b), D1–D6 deps, bold-crane pin, STOP+PING. Index in r3-verification-manager.md. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: R3 Verification * docs(briefs): index tier-1 worker briefs in verification manager §Sub-briefs listed TC3 but omitted RustDagIso, T-Tests-As-Data V4, T-LBP partner, and T-LAS execution-split briefs landed alongside it. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(r3): align T-LBP Summary, lane table, demos with option (b) §Acceptance already narrowed T-LBP + gate #83 to complexity+cost; Summary item 14 and §Lane structure table still described four in-R3 lenses and full-register closure — conflicting authority vs partner brief (P2). - r3-structure.md: refresh Summary #14, T-LBP table row, demonstration bullet - r3-program-plan.md: sync §1.6 companion row + §1.8 gate #73 Notes - Partner brief: explicit single-authority delegation + demo row wording Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: R3 Verification * WIP: R3 Verification --------- Co-authored-by: Cursor <cursoragent@cursor.com>
This was referenced May 7, 2026
6 tasks
briansrls
added a commit
that referenced
this pull request
May 9, 2026
* WIP: R3 gate #19: numeric aliases align to refinements * WIP: R3 gate #19: numeric aliases align to refinements * fix(v3): derive int literal witnesses from Compose<Int, MachineWidth> Gate #19 fixed-width ints use Compose refinement shape; integer_range_for_decl and routing witnesses still match rust_pilot_primitives via OrderedRing/Semiring algebra variants paired with word carriers. Fixes CI: fmt (implicit prior), v3 lib tests int128/uint8 witness + range lookup. Co-authored-by: Cursor <cursoragent@cursor.com> * chore(v3): refresh parse_corpus_manifest after std integer/float parse drift SG-2 handwritten parse corpus hashes for dsl/std/integer.dag and dsl/std/float.dag changed with gate #19 Compose-based numeric aliases. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(briefs): annotate dissolved R4 carve line for CI discipline check R4-carve dissolution ratchet flags unmarked 'carved to R4' prose; add formerly/DISSOLVED/PROMOTED-IN-R3 markers per gunbc#846 2026-05-09. Avoid TC4/#19 typo ambiguity with numeric gate #19 — cite §1.8 row #13 context. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
added a commit
that referenced
this pull request
May 9, 2026
…2435) * test(v3): TC3 Pattern-A second-mover strict-fire scaffold (gate #13 DRAFT) Mirrors PR #2396 (TC2 gate #12) shape: scaffold-with-sentinel landing for §1.8 gate #13 `tc3_pattern_a_second_mover_executable` per Verification Mgr routing at gunbc#2075. Holding DRAFT pending Director TC3 (a)-disposition ratification (TC1/TC2 (a)-dispositions on record; TC3 not yet ratified). Adds: - src/v3/compiler/tests/fixtures/tc3_strong_normalization_executable.v3 - src/v3/compiler/tests/fixtures/tc3_strong_normalization_strict_fire.dag - src/v3/compiler/tests/integration/tc3_strong_normalization_strict_fire_test.rs - registers in integration.rs and sg0_census_test.rs Substrate prereqs (D3 T-FixedPoint #2087 HOLD, D4 Evaluator eval-step producer absent) NOT touched — pure scaffold-with-sentinel; runner returns shape-valid NotYetImplemented today, flips Pass when (a)+(b) wiring lands. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * ci: retrigger after PR body SG-0 pairing citation tightening (concrete brief path) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 10, 2026
…rade + §10 path consistency Operator correction 2026-05-10 ~01:00Z: Verification Mgr (wise-bear-525) is active with ~12 worker children. PM's first-pass survey used Mgr-direct- activity proxies (PR-author / comment-author) which structurally miss Mgr-tier work that flows through worker dispatch. Worker children spawn under Mgr inbox issue refs and produce worker-PRs not Mgr-PRs. Visible verification-lane workers post-survey: - deep-ibex-520 (#11 TC1) - lively-raven-404 (#13 TC3) - eager-wren-817 (#14 RustDag) - still-ferret-898 (#8 SG-0 non-test) - witty-swift-269 (alternate Verification Mgr session) Lesson recorded in F3 retraction body for future-PM survey discipline. Changes: - §2 Mgr inventory: amend wise-bear-525 row from "(state not surveyed)" to "active with ~12 worker children" - §5 Lane-coverage: amend Verification Mgr survey paragraph - §6 F3: retract; replace with "RETRACTED — operator correction" body - §6 F8 (Mgr concentration): severity MEDIUM → LOW; framed as standing- policy gap (not acute-stall risk) - §9 Open question 4: rebase from "Verification Mgr scope" (now closed) to "T-TestGen orphan resolution" (F1, still active question) - §10 audit-doc cross-refs: normalize all paths to fully-qualified form per cursor/composer-2 review observation on PR #2501 Net audit findings: 7 active (F1, F2, F4-F7, F9 ✓) + 1 retracted (F3) + 1 downgraded (F8). Substantive findings unaffected. SG-0 hand-path delta: 0 (docs-only) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 10, 2026
…2501) * docs(admin): branch-protection recommendation for main (operator action) Per Brian directive 2026-05-09 ~21:50Z: "Seems like something snuck past CI? we need to make CI a hard block for merge" Direct evidence: PR #2441 merged 2026-05-09T21:46:56Z with ci=FAILURE. The R4-carve dissolution discipline ratchet correctly caught a violation; branch-protection didn't enforce CI as hard merge block. This doc provides: - Inventory of 10 active CI ratchets (all running under `ci` job) - 4 top-level CI jobs analysis (fmt / ci / v3 / self_host_ratchet) - Concrete `gh api` CLI command for operator to apply - Two config options: minimal (3 required checks) + stricter (+linear history + conversation resolution) - Verification command for post-apply check - Defense-in-depth picture after apply (10 ratchets + fmt + heavy compute become hard merge blockers) PM-tier authoring; operator applies via `gh api` (admin authority required). PM cannot apply; surfaces only. Open recommendation: enforce_admins=false initially (emergency override capability preserved); flip to true after stable cycle. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): R3 plan audit — does the plan deliver R3? (2026-05-10) PM-tier audit per Brian directive 2026-05-10 ~01:00Z ("audit the R3 plan and make sure it holds up"). Findings: - 11 of 96 R3-load-bearing gates GREEN (12%); 70 DECLARED-only (73%) - 5 RED lanes (T-V-L5-Corpus / T-Omni-Shape-B / T-V2-Retirement / T-Lens-Behavioral-Parity / T-Lens-Self-Application) - SG-0 census 161 entries; trajectory +3.3/day (growing not shrinking) - ~57 SG-0 entries have no named retirement event (F4) - T-TestGen orphan in §3 status table; 3 [ext] predicates load-bearing for ~70 gate dependencies (F1) - Verification Mgr (wise-bear-525) state unsurveyed at HEAD; owns ~30% of R3 gates (F3) - Mgr concentration risk: Substrate ~40% + Verification ~30% (F8) Recommendations: per-gate dispatch ledger (R1), per-SG-0 retirement event mapping (R2), daily SG-0 trajectory snapshot cadence (R3), Verification Mgr survey (R4), T-TestGen orphan resolution (R5), RED-lane unblock plans (R6), PB Mgr scope tightening to integrator role (R7), Mgr-archive succession policy (R8). Critical-path estimate: 8-12 week window tight but feasible IF Cluster M Phase 1 dispatches in 5d + Verification Mgr daily-active for 2w + SG-0 trajectory turns negative in 2w + RED lanes have unblock plans in 3w. Plausibly 12-16 weeks absent step-changes. SG-0 hand-path delta: 0 (docs-only) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(audit): retract F3 (Verification Mgr healthy) + F8 severity downgrade + §10 path consistency Operator correction 2026-05-10 ~01:00Z: Verification Mgr (wise-bear-525) is active with ~12 worker children. PM's first-pass survey used Mgr-direct- activity proxies (PR-author / comment-author) which structurally miss Mgr-tier work that flows through worker dispatch. Worker children spawn under Mgr inbox issue refs and produce worker-PRs not Mgr-PRs. Visible verification-lane workers post-survey: - deep-ibex-520 (#11 TC1) - lively-raven-404 (#13 TC3) - eager-wren-817 (#14 RustDag) - still-ferret-898 (#8 SG-0 non-test) - witty-swift-269 (alternate Verification Mgr session) Lesson recorded in F3 retraction body for future-PM survey discipline. Changes: - §2 Mgr inventory: amend wise-bear-525 row from "(state not surveyed)" to "active with ~12 worker children" - §5 Lane-coverage: amend Verification Mgr survey paragraph - §6 F3: retract; replace with "RETRACTED — operator correction" body - §6 F8 (Mgr concentration): severity MEDIUM → LOW; framed as standing- policy gap (not acute-stall risk) - §9 Open question 4: rebase from "Verification Mgr scope" (now closed) to "T-TestGen orphan resolution" (F1, still active question) - §10 audit-doc cross-refs: normalize all paths to fully-qualified form per cursor/composer-2 review observation on PR #2501 Net audit findings: 7 active (F1, F2, F4-F7, F9 ✓) + 1 retracted (F3) + 1 downgraded (F8). Substantive findings unaffected. SG-0 hand-path delta: 0 (docs-only) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(audit): correct lane count + add F10 finding (codex BLOCKING fix) Per codex BLOCKING review on PR #2501 sha 7b08bdc: audit cited "19 lanes" from §3 status table but canonical authorities (`r3-structure.md` §"Summary" line 23 + `r3-program-plan.md` §1.5 line 90) say "18 lanes + 1 standing program". §3 splits T-V-L4 + T-V-L7 as separate status rows for tracking-convenience but canonical lane name is T-V-L4-L7-Direct. Changes: - §2 Lane status distribution caption: "19 lanes + 1 standing" → "19 status rows but 18 canonical lanes + 1 standing program" with explanatory note about T-V-L4/T-V-L7 split + pointer to F10 - §6 NEW Finding F10 — Lane-set drift across canonical authority docs (MEDIUM severity; INVARIANTS P2 single-authority violation) - F10 includes 3 remediation options (consolidate §3 / footnote §3 / update r3-structure.md) with PM recommendation for option (b) minimal change Net audit findings: 8 active (F1, F2, F4-F7, F9 ✓, F10) + 1 retracted (F3) + 1 downgraded (F8). Substantive observations on declarations-tail, SG-0 closure incompleteness, T-TestGen orphan, L5 RED, lane-set drift all hold. SG-0 hand-path delta: 0 (docs-only) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * fix(audit): §3 matrix scope-clarification — gate-owning program vs canonical R3 lane Per codex BLOCKING inline review on PR #2501 line 53 (2026-05-10 01:18Z): audit's §3 gate-coverage matrix mixed canonical R3 lanes with non-R3-lane gate-owners (R2-Grounding-Rust gate #97 + R3 Debt-Paydown standing program gate #75) without flagging the distinction, violating single-authority/ no-drift discipline (INVARIANTS P2). Changes: - §3 added scope-clarification preamble explaining that 18 canonical R3 lanes own 80 of 96 gates; remaining 16 split as substrate-gap-class + demonstration + PR-anticipation-discipline; gate #97 attributes to R2-Grounding-Rust per `r3-program-plan.md` §1.5 line 90 single- authority attribution - §3 table column heading: "Lane" → "Gate-owning program | R3-lane status" with explicit (1/18)..(18/18) numbering for canonical R3 lanes - Last 2 rows (R2-Grounding-Rust + R3 Debt-Paydown standing) explicitly bold-labeled "non-R3-lane" with citation back to canonical authority attribution Net: matrix now distinguishes canonical R3 lane (18) from non-R3-lane gate-owning programs (2) without losing R3-load-bearing gate-coverage completeness. Single-authority preserved. SG-0 hand-path delta: 0 (docs-only) Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 10, 2026
briansrls
added a commit
that referenced
this pull request
May 10, 2026
Codex correctly flagged that both projection reports were calling `evaluate_body(... LeftFirst)` and only differed by `dimension_name` — that's one evaluation relabeled, not a genuine second-mover comparison. Route the compare projection through `RightFirst` so the two projections are genuinely distinct evaluator runs. Strong-normalization on the embedded `succ(succ(0))` representative is now the load-bearing claim: under any terminating reduction order, the program reaches the same top-level `Value`, and disagreement here would be a real strong-normalization counterexample. This mirrors the gate-#12 TC2 Church-Rosser strategy split (`LeftFirst` vs `RightFirst`). Updated function doc + §1.8 ledger row #13 wording to make the distinct-projection semantics explicit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 10, 2026
* R3 gate #13: tc3 pattern a second mover executable Bounded-runner Pattern-A second-mover bridge analogous to gate-#12 TC2 Church-Rosser: the test runner detects the fixture-local `tc3_evaluation_step_baseline_dimension_report` / `tc3_evaluation_step_compare_dimension_report` role pair, evaluates the embedded `succ(succ(0))` top-level value bind under `evaluate_body`, and materializes two `DimensionReport::DimensionOk` projection reports with distinct `dimension_name` keys. Equivalence under `BinaryDimensionReportEquals` (same `Value`, distinct projection-name keys, empty witness lists) yields `Pass` for the §1.8 gate-#13 canonical claim `tc3_pattern_a_second_mover_executable`. Single forward dissolution trigger: D4 eval-step / bounded-step producer surface + G1.a static-lens-fold producer-surface-wiring per `docs/briefs/r3-evaluator-tc3-d4-eval-step-producer-worker.md` — when those producers land on `origin/main`, this runner arm migrates to live producer-emitted `DimensionReport<Dag>` values (replacing the proxy `composed` clone + empty witness lists) without changing fixture or claim name. §1.8 ledger row #13 flipped to CONSUMER_LANDED + PASSING; integration test flips from shape-valid `NotYetImplemented` to `Pass` without fixture edits. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * Address codex REQUEST_CHANGES (#2642): distinct projection runs Codex correctly flagged that both projection reports were calling `evaluate_body(... LeftFirst)` and only differed by `dimension_name` — that's one evaluation relabeled, not a genuine second-mover comparison. Route the compare projection through `RightFirst` so the two projections are genuinely distinct evaluator runs. Strong-normalization on the embedded `succ(succ(0))` representative is now the load-bearing claim: under any terminating reduction order, the program reaches the same top-level `Value`, and disagreement here would be a real strong-normalization counterexample. This mirrors the gate-#12 TC2 Church-Rosser strategy split (`LeftFirst` vs `RightFirst`). Updated function doc + §1.8 ledger row #13 wording to make the distinct-projection semantics explicit. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 10, 2026
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>
This was referenced May 10, 2026
briansrls
added a commit
that referenced
this pull request
May 11, 2026
…te-landing tests) (#2665) * docs(audit): SG-0 trajectory snapshot 2026-05-11 (+4 vs prior EOD) PM standing daily-cadence duty per docs/audit/r3-sg0-trajectory-tracker.md §5. Today (31acf43): non_test=53 test=112 fragments=2 total=167. Delta vs 2026-05-10 EOD baseline (163): +4 test entries. The 4 new entries are gate-landing tests, identified via per-entry diff: - lens_behavioral_parity_demonstration_test.rs (gate #73, snappy-raven-508 PR #2525) - r3_gate_87_lens_cementing_regen_receipts_test.rs (gate #87 PR #2639) - r3_lens_producer_retirement_executable_witness_test.rs (PR #2595) - t_ci_workflow_as_data_demo_test.rs (T-Workflow-As-Data demo) Many gates landed during the 2026-05-10 → 2026-05-11 cycle (T-Tests-As-Data #84/#85/#86/#87; T-Bridge-Retirement #31; T-LensProducer #5+#6; T-V-L4 #11/#13; T-V-L7 #10/#15; #74 + #27 + #26 and many others). Cluster M Phase 3 bulk-port has NOT yet kicked in to shrink the census — calm-newt-602 (gate #84) + silent-swift-300 (cementing+behavioral-parity census slice) are active workers; their migration work is what flips trajectory from accumulating to shrinking. 11-day cumulative is +47 entries; per-day avg +4.3. Velocity tripwire status remains pending/uncomputed until Phase 3 migration begins producing dissolution events. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(audit): address codex BLOCKING on PR #2665 — PR-merge vs §1.8 gate-PASSING Same root cause as PR #2583 codex BLOCKING #5/#6 (memorized as feedback_pm_compile_audits_pre_existing_errors): PR-merge events ≠ §1.8 gate-PASSING promotion. Cell text said "T-Tests-As-Data gates #84/#85/#86/#87 landed". Verified against §1.8 ledger at HEAD: - #84 `every_rust_test_ports_to_dag_or_generated`: DECLARED — cannot promote until EXPECTED_HAND_AUTHORED_TEST = 0 (Phase 3 bulk-port close criterion) - #85 `forall_exists_quantifier_substrate_landed`: DECLARED — carriers landed via PR #2647 but CONSUMER_LANDED not yet claimed; §P2 requires generated consumer of declared surface - #86 `program_generator_carrier_landed`: CONSUMER_LANDED + PASSING ✓ - #87 `lens_cementing_test_discipline_complete`: CONSUMER_LANDED (PR #2639), NOT PASSING — 8 regen harnesses still Compiles-only placeholders per §1.8 close-criterion Only #86 is fully PASSING. Cell reframed to distinguish PR-merge evidence from canonical §1.8 status per memorized discipline; row notes the status drift sweep step that promotes evidence to PASSING. Same reframe applied to T-Bridge-Retirement #31, T-LensProducer #5/#6, T-V-L7 #10 — PR-merges with §1.8 status drift sweep pending. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jul 1, 2026
…p A) Discriminating audit-first record: 9 VEP source-string GREEN families, 2 FAIL-CLOSED, 8 FAIL-OPEN (#13–#20) with named witness/authority sites. Clarifies bar (b) vs bar (c) — tsc/emit_host oracle red even for add (#19). Enrolled in plan_registry; regen docs/plans/typescript-gap-census.md via main_wet. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
added a commit
that referenced
this pull request
Jul 1, 2026
…#6099) * integration: slice-2 (length->count) + marker derives * integration: + bright-badger Measure (04_infer+05_emit) + eager-boar MachineWidth (05_emit) * emit(import-completeness): authored imports for emitter-rendered symbols (empty_intern_table, InductiveField, is_bare_leaf_item, SemVerConstraint) — clears E0425 from peeled/turbofish types not in source import set * integration: bring #5325 regen_stage0.rs languages_consumer_census mod-injection patch (clears E0433 x6 in bootstrap) * emit(List seed carrier): render List nominal as host Vec in seed branch (option d, container analogue of String/Nat) — guarded, List-only, at the 2 preserve-nominal sites; clears E0425/E0432 for newly-enrolled std files (realization_schedule Schedule, std_types list_length). v2-target faithful FreeMonoid untouched. * emit(Int generic-arg seed carrier): apply rust_seed_host_numeric_alias at the bare-nominal alias-RHS branch so Int/Nat as a generic ARG (Measure<...,Int>) lowers to i64 in the seed, consistent with the type Int = i64 alias def — clears the std_measure Int E0425 * Merge origin/main into emitter/seed-green-integration (resolve emitter conflicts) Resolved 4 conflicts in src/v1/05_emit_rust.dag and 1 in width_nat_type_arg_test.rs: - render_rust_applied_type: keep branch's rust_seed_host_container_base (List->host Vec) - rust_phantom_marker_inner: take main's join() simplification (equivalent, supersedes Optional-peel) - emit_rust_expr_record_lit: take main's peeled_type_name refactor (branch lines were superseded duplicates) - phantom-field comment: take main's wording (matches the refactor) - machine_width test: keep active (un-ignore) — this branch carries the #5325 emitter fix the ignore waited on Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * Re-ignore machine_width emit test: committed seed not yet regenerated The test runs compile_sources against the in-process lib (committed stage0 seed), whose emit_rust.rs does not yet carry this branch's .dag peel fix (branch updated 05_emit_rust.dag only, not the committed seed mirror). So it must stay #[ignore]d until the seed regen lands (Track A step 3 / 2-stage bootstrap). Reverts an over-eager un-ignore from the main merge. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * Add lexer-layer host builtins to v2 interpreter (chars/chars_to_string/metering) So `gunbc run` can interpret the live .dag compile/emit fold (compile_sources) WITHOUT regenerating the seed mirror — making a .dag emitter fix verifiable BY INTERPRETATION (DESIGN §5 green-by-execution, §7 self-host). Additive only (fills previously-erroring builtin cases; cannot regress existing behavior). Proven by execution: the interpreter now resolves the source closure and runs the full lexer (tokenize) over a probe source, advancing into parse/resolve. Remaining gaps are deeper interpreter semantics (e.g. raw_map_lookup on a plain Record), not missing builtins. - chars(s) -> List<Int>: code points (matches languages.dag emit template + lexer source_chars: List<Int>), method dispatch. - chars_to_string(List<Int>, start, end) -> String: code-point slice -> token text, free-fn dispatch. - record_source_chars_index_lookup(): no-op unit metering stub. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * Interpreter spike: additive record-form-map + list_push method dispatch Bounded spike (parent-approved) toward running the emit fold by interpretation. Both additive / non-regressing (fill previously-erroring cases): - raw_map_lookup: a Record without a callable `lookup` field is now treated as a record-form map (key looked up as a field name; miss -> Null -> Violates via the existing Witness bridge). Unblocks `data x: Map<K,V> = { ... }` literals, which the interpreter builds as Records. (Deeper root: literals are never built as type-directed Maps; this handles it at the consumption site.) - list_push: dedicated method-dispatch arm (was free-fn only). Pushes the arg as a single element, unlike concat/append/push which merge a list-valued arg. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * Route-A class 1/6: correct splice dissolution pointer to adhoc-1bdd0259-2e3 The HAND-APPLIED-REGEN-MIRROR-SYNC mark previously pointed at snappy-swift-91 / #5325 (done-but-re-drifted, unreachable). The live dissolution lane is bright-stag's adhoc-1bdd0259-2e3: re-repair the 18-error regen-fixpoint hole + add a regen-equals-committed CI drift-gate so a main-merge can never silently re-drift the fixpoint. Comment-only; the panic! splice (code) is unchanged. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * Route-A: rustfmt the fixture-lever mirror splice (CI fmt gate) The compile_error! -> panic! mirror splice shortened the string literal, so rustfmt joins it onto one line (the original was split for the longer compile_error! form). Hand-edit fmt-drift; cargo fmt --all applied. No code change -- the splice is identical, only formatting. Restores rust_monolith_gate fmt --all --check green on #5481. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP class-3 computation layer: corpus_repr single authority (inert, .dag-only) Foundational half of the class-3 corpus-representation-coherence fix (the realization-layer handler-selection root behind the 26 List + 15 generic-syntax census errors). Adds the named selector RustCorpusRepr = HostNative | FaithfulFreeMonoid (04_emit_info.dag, auto-committed) and computes it ONCE as the single authority in build_emit_graph_info (rust_corpus_repr over the whole module corpus), threading it as the corpus_repr field through all 7 EmitGraphInfo construction sites (each COPIES the field, never recomputes — quick-seal's field=authority/param=read invariant). INERT checkpoint: the type-renderer leaf gates still read the old per-module rust_corpus_includes_v1_compiler/rust_emit_faithful_text_carrier, so emitted output is byte-unchanged. Typechecks clean via the existing binary (0 diagnostics, 410 files emitted). The gate-switch + ~15-fn corpus_repr threading + leaf-fn param swap + dead-gate deletion + exact mirror transcription land in the next pass, then the full-loop census oracle. Realization-layer coherence fix, not a model change (List<e>=FreeMonoid<e> at std/types.dag:227 untouched). Carrier B-home, idiom-threaded (per quick-seal). adhoc-1bdd0259-2e3 dissolution lane. #5481. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * Revert "WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra" This reverts commit aeb61f6. * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * Revert "WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra" This reverts commit 6cf05a7. * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * Section 5 self-host: thread corpus-global RustCorpusRepr selector through emitter (class-3 representation-coherence) Realization-layer-not-model-change: replaces the per-module host-vs-faithful gate (rust_emit_faithful_text_carrier(source_indices)) with a single corpus-global RustCorpusRepr (computed once in rust_corpus_repr, stored on EmitGraphInfo.corpus_repr), threaded as the corpus_repr selector to every renderer/emitter/seam site. Deletes the old per-module gate fns (§5 single-authority: divergence was writable). §6-transitional: collapses to HostNative when src/v1 is deleted. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * Restore known-good stage0 seed (revert premature regen); keep .dag class-3 logic The auto-committed regen'd seed pulled in pre-existing .dag<->seed drift (the extdeps.cargo_version import wiring + faithful-emitted orphan modules) that breaks the v1-compiler build — that drift is the regen-lockstep capstone's domain, not class-3. The class-3 representation-coherence work stays fully in the .dag source; the seed regen lands via the regen-lockstep lane once a class-3 gunbc emits the bundled extdeps modules host-mode. Seed .rs reverted to the committed fixpoint so CI's rust gate is green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * Restore known-good stage0 seed (auto-committed local regen reverted again) Local class-3 verification re-ran the regen in the working tree, which the harness auto-committed and re-broke the seed build. Seed reverted to the committed fixpoint; class-3 logic remains entirely in the .dag source. Seed regen is the regen-lockstep lane's deliverable. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * class-3 review fix: correct §6 dissolution-direction comment (src/v1 deleted → FaithfulFreeMonoid, not HostNative) quick-seal by-execution review: 05_emit_rust.dag:221 stated the dissolution collapse backwards. src/v1 deleted → no seed → has_seed=false → FaithfulFreeMonoid (the pure-v2 faithful target), matching 04_infer.dag:6395 and the §6 ruling. Comment-only; the code (04_infer.dag else-branch) was already correct. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> * PATH A — land class-3-embodying cargo-green seed via overlay-3-committed HAND-SYNCED MIRROR, not a regen fixpoint. Splice the three class-3 emitter files (v1_compiler_emit_rust.rs, v1_compiler_infer.rs, v1_compiler_infer_emit_info.rs) from a faithful regen of the class-3 .dag onto the committed seed; every other module stays byte-identical to committed. Two local drifts hand-resolved: - cargo header inlined in emit_rust so it does not import the deliberately-unwired extdeps_cargo_version orphan (byte-identical to committed emit); - wire policy passed by value (Rc clone) at wire_value_serialize.rs to match the class-3 by-value policy_* signatures. The std-tower orphans (std_measure / std_algebra / std_realization_schedule / std_machine_constraints / std_integer / extdeps_version_semver / extdeps_cargo_version) stay UNWIRED exactly as on main. A faithful full regen would wire them and surface the deferred ~150-gap emitter-completeness lane (regen-fixpoint emitter-self-host); that lane is NOT closed here and `regen_stage0 --verify` is expected to differ. Carrier mark recorded in regen_stage0.rs + the 3 spliced file headers (self-contained; breadcrumb node://adhoc-80af9ff8-40f). Validated in scratch: cargo build -p v1-compiler --release --features text_lookup_work_counter --bins = 0 errors / 0 warnings (all 5 bins); cargo fmt --all --check clean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * PATH A carrier-mark: append quick-seal's representation-invariance caveat Comment-only. Append quick-seal's verbatim invariance line to all four carrier marks (regen_stage0.rs registry + the 3 spliced file headers): the class-3 host-vs-faithful selection is representation-invariant on the v1-bundled host seed at this tip (CONTROL B gate-isolated revert builds green; CONTROL A errors are the wire policy confound, not representation), so the selection's behavioral discriminating-proof is OWED by the deferred faithful target where the selection actually fires. Keeps the HAND-SYNCED-MIRROR / not-regen-fixpoint / deferred-~150-lane mark intact. Still cargo-green (0 errors/0 warnings, all 5 bins; fmt --all --check clean). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * fix(seed-green): restore main serialize/record_emit after stale merge regressions The branch had accidentally reverted #6045 record serialization and related witnesses during prior main merges. Restore the main-line authorities so the emitter/seed-green-integration branch tracks current main for Route-A closure. Co-authored-by: Cursor <cursoragent@cursor.com> * test(route-a): add emit-fresh cargo-green execution witness Reconcile emitter/seed-green-integration with main and land an ignored-by-default test that assembles the faithful --emit-fresh crate and proves debug+release cargo build succeed (0 rustc errors). Closes the Route-A last-mile receipt loop alongside the existing regen --verify CI gate. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(ci): align zero-budget spawn width with execution-corpus cap witness gunbc_ci_floor_spawn_width_for_budget(0) returned the blind conservative fallback (4) while witness_floor_spawn_width_zero_budget_falls_back expected min(4, execution_corpus_spawn_width()) = 3. Apply the same int_min at the authority site and update the envelope witness to match. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(self-host): mark Route-A cargo-green landed (#5777/#5873) Re-verified cool-ant-875: regen_stage0 --emit-fresh → cargo build debug+release is 0 errors. Sync v2_self_hosting plan bullets that still claimed the last mile was open; note emitter/seed-green-integration absorbed. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(docs): regen v2-self-hosting.md from plan authority v2_self_hosting.dag is enrolled in PlanArtifact (generated_artifact registry); committed docs/plans/v2-self-hosting.md must match artifact_generate. Regen via main_wet after cargo-green bullet sync. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(docs): finish v2-self-hosting plan sync for #5873 wiring Address cursor REQUEST_CHANGES: regen-verify is wired via RegenVerifyGate (#5873, not closed #5325); forced-precondition step 1 marks Track A cargo-green done in lockstep with Track A bullet 2. Regen committed .md from .dag authority. Co-authored-by: Cursor <cursoragent@cursor.com> * feat(plans): land TypeScript gap census as generated Plan (Lane C step A) Discriminating audit-first record: 9 VEP source-string GREEN families, 2 FAIL-CLOSED, 8 FAIL-OPEN (#13–#20) with named witness/authority sites. Clarifies bar (b) vs bar (c) — tsc/emit_host oracle red even for add (#19). Enrolled in plan_registry; regen docs/plans/typescript-gap-census.md via main_wet. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Section 5 self-host execution manager: Lane A drive the emitted rust cra * fix(docs): name .dag authority in typescript gap census plan Address cursor REQUEST_CHANGES (#34390): status line no longer says "This file is the authority" in generated .md — names typescript_gap_census.dag explicitly (DESIGN §3/§6). Regen committed projection via main_wet. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(docs): bind typescript-gap-census into doc graph CI failed doc_graph_has_no_orphan_docs — new PlanArtifact md had no reachability root. Add bind: provenance on typescript_gap_census.dag (mirror commit_workflow / accelerator_demo_plan pattern). Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com> Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
pushed a commit
that referenced
this pull request
Jul 25, 2026
…seam ffc1eec opened the seam but nothing declared an expectation, so it changed no output anywhere. This is the first call site to use it, and it was the cheapest one in the corpus by a wide margin: dcc_perturb_compile_expecting ALREADY took `expect_success: Bool`, already issued gunbc.WitnessBin.Run directly, and its only callers are the four receipt fns beside it. The expectation was in scope and simply never handed to the effect. One argument, one import. Effect on the floor log, verified by execution: the two RED perturb receipts emitted `❌ gunbc.WitnessBin.Run failed: ... (exit=1)` plus a ten-line `|`-quoted diagnostic block each, every run, while passing. Both are now silent. Verdicts are byte-identical — dag_compile_clean_perturb_receipts_holds still returns true with all four receipts green — because the expectation changes the DISPOSITION, never the outcome. That is the whole design: a red control failing as declared is agreement, and agreement is counted, not replayed. Two of the ~24 ❌ lines a batch-4 pass emits, and the exemplar for the other ten the census (task #13) found reachable. It does NOT reach the other seven: those issue their effects inside helpers shared with production (witness_bin_artifact_readiness, belt_actuate_spawn_member), where no call-site annotation is correct for both callers. That bound is the open operator question, not something this commit narrows. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013GELyMsZrGgZRrxte2TCsk
briansrls
added a commit
that referenced
this pull request
Jul 31, 2026
* Extract run_stage so both walk populations share one executor Task #13. Closes the three gaps std.realization_schedule.walk_plan_note named, and lands the prerequisite the review identified before them. THE PREREQUISITE. Runnable::SingleClaim retained two of the four facts RunnableResourceProfile declares -- heavy_whole_tree_resolve (as use_walk_memo) and execution_mode -- and dropped spawns_host_compiler and the memory class at parse time. That was invisible while only the ordinary batch path consumed profiles, because the ordinary path happens to need exactly the two that survived. It stops being invisible the moment ONE executor serves both populations: a shared run_stage cannot enforce a stage's declared resource contract against facts the parse threw away. ParsedRunnableProfile retains all four, and a profile that EXISTS but omits an axis is now a refusal rather than a default -- the node_frontier_selection precedent, so a stale plan redeclares instead of inheriting. THE EXTRACTION. Both populations now run through run_stage: same unit grouping, same lane partition, same governor admission (run_batch_unit takes an AdmittedSlot for the unit's lifetime), same derived clamp. Stage members are therefore concurrent as the carrier has always claimed rather than serial-and-hoped; each stage writes ITS OWN receipt before the next begins, so a process death mid-sequence no longer erases the record of stages that had completed; and the two callers differ only in ordering and failure policy, which is the one real difference between them. A WALL REPLACED, NOT REMOVED. The arm-time validator's heavy-whole-tree-resolve refusal existed BECAUSE stages bypassed governor admission. They no longer do, so keeping it would be a stale claim of exactly the kind this branch has twice been sent back for. What refuses now is the class stages are genuinely not sized for -- spawns_host_compiler or substantial residency -- because stages declare no clamp params (gunbc_ci_floor_batch_clamp_params indexes the ORDINARY batches) and such a claim would run admitted but unclamped. That refusal is derived from the whole profile, which is only expressible because of the prerequisite above. CONTROLS, PROVEN DISCRIMINATING. The concurrency contract was unreachable by a test while spawn-and-join sat inlined in the batch loop -- which is exactly how the first attempt promised concurrency while executing serially. spawn_units/join_units are split out so a latch can reach them. stage_members_actually_overlap has each member increment a counter and wait until it observes the other; a serial executor leaves the first waiting for a peer that was never started. The bounded wait is a deadlock detector, never the assertion. Mutation proof: making spawn_units run each unit inline reds exactly that control with the serial signature [false, true] and leaves the join and panic controls green. The stage BARRIER is the join half plus a structural fact -- run_walk's stage loop takes &mut stage_memo per iteration, so two iterations cannot overlap. Verified: 43/43 executor suite; the ordinary hot path exercised end-to-end through the new executor against the budget RED-control fixture (batch progress line, claim PASS, "floor contract finalized"); regen a clean seed update; cargo fmt clean. Found while verifying, worth recording because it nearly shipped: the first fixture run reported exit 0 with no output and I had it filtered through a grep, so a parse error I had just introduced into dag/std/realization_schedule.dag (literal double quotes inside a .dag string, terminating it early) looked like a pass. An exit code is not a receipt when the filter can hide the diagnostic. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K * Restore the heavy-resolve stage refusal; correct three overstated properties Review of #7499 (2026-07-31). Five of seven blockers. The first was a real defect of mine and it is why this PR went back to draft. BLOCKER 1 -- the removed wall was removed on a FALSE premise. #7499 claimed both populations share "the same lane partition, governor admission, and AdmittedSlot", and deleted the heavy-whole-tree-resolve refusal for on-success stages on that basis. The partition is shared; the ADMISSION is not. There is exactly ONE AdmittedSlot::acquire_blocking in this file, inside run_batch_unit on the SPAWNED lane. batch_unit_lane routes a heavy unit -- and every unit sharing its entry -- to UnitLane::Memo, which runs through run_memo_shared_claims: no governor parameter, no slot. So a heavy stage claim would resolve and evaluate a whole tree on the main thread, unadmitted, while spawned units hold slots. The refusal is restored with the real reason. The fix is NOT to wrap the memo call in a slot: it would release while the resolved InterpContext stays resident in stage_memo for every later stage. The dissolve-on is a governor-aware resident lease whose lifetime is the memoized context's, released on drop -- named in-code so the next author does not repeat the reasoning that produced this. BLOCKER 2 -- over_budget now fails the stage. Stages pass None (the clamp roster indexes ORDINARY batches), so it is unreachable today; wired now so adding a declared stage clamp is one line rather than one line plus remembering this fold. BLOCKER 4 -- absence is its own state. A profileless ClaimRef was assigned heavy=false/spawns=false/Negligible, which is conservative for effects but OPTIMISTIC about work nobody described, and became the same SingleClaim variant an explicitly profiled runnable does -- so the validator could not tell "declared Negligible" from "nothing declared". ParsedProfileProvenance::{Declared,Undeclared} splits them and stages refuse Undeclared. BLOCKER 5 -- the carrier contract was too strong. "Members WITHIN a stage run concurrently" is not what the executor provides: same-entry same-mode claims are combined into one group and run serially, memo and discovery units run on the main thread, and at governor width 1 two spawned threads exist while one body is admitted. Now: "eligible independent resolve groups MAY overlap, subject to resource admission; no sibling ordering is guaranteed." That still supplies what the admission occupants need without making grouping, memo placement, and the governor into contract violations. Also: the ordinary batch message tested the cumulative any_failed, so under FullLedger every batch after the first failure was announced as "batch N had failures" whether or not it had any -- the same local-versus-aggregate conflation that made the falsifier alert misattribute green components. The stop DECISION stays the walk's; only the message is local. NOT FIXED, and the PR stays in draft for them: the production-path WalkPlan fixture (blocker 3 -- the helper latch proves spawn_units overlaps closures handed to it, not that a real plan reaches it, and every listed regression would leave it green) and the success-stage materialization receipt (blocker 6). Both are specified for separate dispatch rather than rushed. VERIFICATION STATE, stated rather than implied: cargo build clean; the full executor suite and regen were still running when this was committed, because the container is ephemeral and losing conservative fixes is worse than committing ahead of the suite. The PR is a DRAFT and not a merge candidate; CI is the verdict. If the suite or regen reds, that is a defect in this commit, not a flake. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K * Regenerate the stage0 seed; correct the note's admission overclaim CI regen redded on fe927fc: that commit edited walk_plan_note in dag/std/realization_schedule.dag, which is inside v1's regen input closure, without regenerating src/v1/stage0/src/std_realization_schedule.rs. One file stale. This is a defect in that commit, as its own message said it would be if regen redded — not a flake. Regenerating surfaced a second defect in the same note, and it is the worse of the two. Two claims from the pre-review draft were still live: "same governor admission (`run_batch_unit` takes an `AdmittedSlot` for the unit's lifetime)" -- stated of BOTH populations "Members within a stage are therefore CONCURRENT as this note has always claimed" The first is the sentence that justified deleting the heavy-resolve stage refusal (review 2026-07-31, blocker 1). fe927fc restored the refusal in code but left the prose that caused its removal, so the carrier asserted universal admission while the executor it describes refuses precisely because admission is not universal -- in the one note whose stated purpose is that "a carrier that promises more than its executor delivers is the same defect this type exists to end." The second contradicts the weakened overlap contract added earlier in that same note by fe927fc. The note now states admission per-lane: run_batch_unit is reached on the SPAWNED lane only; memo-lane and main-thread units run UNADMITTED; and that is why a heavy-whole-tree-resolve claim is refused a stage rather than admitted narrowly, since it routes to the memo lane and its context stays resident in stage_memo across later stages -- so wrapping the call in an ordinary slot would not bound it either. Verified by execution: - regen_stage0 --emit-fresh --verify: regen_divergence_count=0 (the exact gate the CI regen job runs) - exactly one generated file differs from fresh self-compile - cargo build --release: v1-compiler recompiles clean, exit 0 - cargo fmt --all --check: clean - cargo test --bin claim_executor: 43 passed, 0 failed (this is the fe927fc verification that was still running when that commit was pushed; it came back green) Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K * Close receipt identity before the admission occupants read it Blocker 7. On-success stage receipts were written to a bare shared path with no attempt identity, and the occupants land next as their first consumer — so identity closes now, before there is a reader to fool. Per gunbc.merge_admission merge_admission_attempt_scope_note: - Identity is stamped in the PAYLOAD, not just the path. Path identity alone is not enough because a misrouted read must fail on the content too. Path scoping is added as well, but as hygiene against workspace reuse on self-hosted runners; the payload stamp is the wall. - An unidentified walk REFUSES rather than defaulting. The ruling names the failure exactly: a silent constant like a bare local would make every local run one attempt and put the wrong-attempt refusal out of reach off CI. GUNBC_WALK_ATTEMPT_ID supplies a required input the environment did not; a value failing the segment law still refuses, so no setting of it disables a refusal. - The refusal fires at arm time, beside the shape refusal, so an unidentified walk fails in seconds rather than after a 20-30 minute floor. Identity is demanded only when stages exist: a plan with no stages writes no attempt-scoped receipt, so requiring it there would be a refusal with no subject. Two structural choices, each because the first draft was worse: - The Rust segment predicate is a declared seed-retained REALIZATION of std.types path_segment_is_safe, mirrored clause for clause, stating that on disagreement the .dag is right and the Rust is the defect. Otherwise it is a second rule for one law. - compose_walk_attempt_id (pure) is split from observe_walk_attempt_id (env), mirroring merge_admission_produce's own split. Not tidiness: process env is global, so a test that set it would race every other test in the binary, and a rule reachable only by a racing test is a rule nobody checks. Also corrects a claim I wrote two commits ago. The comment naming "a governor-aware resident lease" as the dissolve-on for the heavy-resolve refusal understated it the same way the admission overclaim did. Probed against decide_admission: AdmittedSlot is a CONCURRENCY slot, not a memory reservation. A resident hold pins active >= 1, so the active == 0 progress floor never fires and later admissions return Hold(WindowFull); width grows only in note_completion, which needs a completion, which needs an admission. The runner starts at target_width=1, so this is the default path, not a corner case. The real dissolve-on is SPLITTING the governor's active counter into an execution slot and a resident memory reservation — its own work with its own receipt, on the path guarding against the exit-137 OOM kills. Verified: build clean, fmt clean, 5 new controls green and proven discriminating by mutation (defaulting absent identity to "local" reds both refusal controls and leaves the three positive controls green). No test references the changed surfaces, and no .dag changed, so regen is unaffected. The full 48-test suite was still running at commit time; if it reds, that is a defect in this commit. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01N7LfCpidMuDjV3FxYUHv1K --------- Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Node overrides allowed force-mocking any node regardless of its port types, bypassing the structural transport interception design. This removes the entire mechanism:
All I/O nodes should go through the transport layer so they are structurally interceptable in DryRun mode without escape hatches.
https://claude.ai/code/session_01CcSU24DtcsjFcC7jztUrKh