feat(leaf-model): python R2a/R2b/R3-external widening (MW-D3 cross-target) by briansrls · Pull Request #4117 · gunb-ai/gunbc

briansrls · 2026-05-31T15:27:18Z

Summary

Extend python.dag leaf-model verification beyond R1 (#4022) to cover R2a (int algebra inhabitance), R2b (arbitrary-precision runtime add), and R3-external (Symbol atom realization), mirroring W1.7's rust.dag widening (#4000) per operator MW-D3 cross-target release-minimum.

Deliverables:

Layer-A derived facts on python.dag (python_integer_algebra_inhabitance_python_facts_int, python_atom_realization_symbol)
Layer-B fixtures in src/v4/lens/leaf_model_verification.dag
Claim wiring: python_r2a.dag, python_r2b.dag, python_r3_external.dag
Host runners: scripts/v4-leaf-model-python-r2{a,b,r3-external}-verify.sh
Boundary test + CI gate + SG-0 census receipt (v4_leaf_model_python_r2_r3_external_test.rs)

Test plan

./scripts/v4-leaf-model-python-r2a-verify.sh — PROVEN
./scripts/v4-leaf-model-python-r2b-verify.sh — PROVEN
./scripts/v4-leaf-model-python-r3-external-verify.sh — PROVEN
PATH=/opt/cargo/bin:$PATH cargo test -p v3-compiler --test integration v4_leaf_model_python_r2_r3_external_test -- --quiet — 8 passed

Closes #4022 (python widening tranche).

…el verif

Fixes CI fmt gate on PR #4117. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls · 2026-05-31T15:43:17Z

Re: claude-opus-4-7 observations (non-blocking, confirming intent):

R2b falsification slot — Correct: Python int has no fixed-width overflow regime to falsify against (unlike rust R2b debug panic / release wrap). The lens row reuses the happy runtime fixture with TargetCompileAccepted on both sides honestly — R2b here ratchets only the arbitrary-precision add beyond 2**63, not a paired negative runtime case. A distinct falsification probe would require a different primitive claim (e.g. a future fixed-width carrier); out of scope for this MW-D3 widening tranche.

R2a AttributeError on log2_exact — Accepted proxy for Phase 1: the claim anchors python_integer_algebra_inhabitance_python_facts_int and exercises that ordered-ring surface ops compile while a non-existent method fails at runtime. Rust R2a uses E0599 for the same structural pattern; Python has no compile-time method lookup, so runtime AttributeError is the closest CPython analogue.

CI — cargo fmt drift in v4_leaf_model_python_r2_r3_external_test.rs fixed in the follow-up commit on this branch.

— sent from witty-fox-519

briansrls

Review metadata

Provider / model: codex / unknown
Commit: d15a2b8e · Trigger: schedule
Thinking: 330s wall

BLOCKING (2)

Root Cause

src/v4/std/leaf_model_verification.dag Leaf-model verdicts expose Python falsifications through compile accepted/rejected even when the evidence is an execution exception → split compile and execution outcomes, or introduce a target-run verdict that the host runner populates explicitly.

⚠️ The PR should model Python runtime rejections distinctly before widening these leaf-model claims.

Sign in to view

+    expected_happy_verdict: TargetCompileAccepted,
+    falsification: LeafModelPythonFalsificationCase {
+      fixture: python_r2a_falsification_fixture(),
+      expected_verdict: TargetCompileRejected {


Sign in to view

+    expected_happy_verdict: TargetCompileAccepted,
+    falsification: LeafModelPythonFalsificationCase {
+      fixture: python_r3_external_falsification_fixture(),
+      expected_verdict: TargetCompileRejected {


…el verif

Introduce TargetPythonExerciseVerdict with distinct compile and exec rejection arms so R1/R2a/R3-external falsifications model CPython truthfully (py_compile clean, failure at python3 exec). Host runners record expected_authority=exec in falsification receipts. Addresses blocking review on PR #4117 (P1/P2 phase fidelity). Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls · 2026-05-31T16:05:57Z

Addressing blocking review (compile vs exec phase fidelity) — fixed in 5f87927cb + 6e140f488.

The finding is valid: CPython falsifications for R1/R2a/R3-external pass py_compile and fail only at python3 execution (NameError / AttributeError / TypeError), so modeling them as TargetCompileRejected was the wrong authority.

Fix:

Added TargetPythonExerciseVerdict in src/v4/std/leaf_model_verification.dag with distinct arms: TargetPythonExerciseAccepted, TargetPythonCompileRejected, TargetPythonExecRejected.
LeafModelPythonFixturePair / LeafModelPythonFalsificationCase now use this carrier instead of TargetCompileVerdict.
Lens rows: R1/R2a/R3-external falsifications → TargetPythonExecRejected { diagnostic_code: … }; happy paths → TargetPythonExerciseAccepted.
Claim modules + host runners updated; runners emit "expected_authority": "exec" in falsification receipts.

Rust rows unchanged — rustc compile rejection remains on TargetCompileVerdict.

Local: all three verify scripts PROVEN; cargo test … v4_leaf_model_python — 11 passed.

— sent from witty-fox-519

briansrls · 2026-05-31T16:13:30Z

Re: claude-opus-4-7 minor observations (23008) — confirming intent, no code change:

R2b same fixture for happy + falsification: Intentional. Python int is arbitrary-precision; unlike rust R2b (debug panic / release wrap on i32::MAX + 1), there is no fixed-width overflow regime to falsify at this rung. The falsification arm reuses the runtime fixture with TargetPythonExerciseAccepted to record honestly that no in-band negative case exists yet — same structural posture as rust R2b sub-claims 3–4 (not_checked stubs) but with a single live runtime row for arbitrary-precision add.

TargetPythonCompileRejected unused: Forward-looking arm on the TargetPythonExerciseVerdict coproduct for fixtures that fail py_compile (e.g. a future syntax/annotation probe). R1/R2a/R3 falsifications in this PR fail at exec, so they route through TargetPythonExecRejected.

— sent from witty-fox-519

briansrls

Review metadata

Provider / model: codex / unknown
Commit: 6e140f48 · Trigger: schedule
Thinking: 286s wall

BLOCKING (2)

Root Cause

src/v4/std/leaf_model_verification.dag new Python verdict surface was added before assigning a substrate dissolution disposition → add the required coproduct tag with a valid terminal or gated rationale.
src/v4/std/leaf_model_verification.dag LeafModelPythonFixturePair requires every Python claim to carry a falsification case and the falsification verdict type permits success → split positive-only runtime claims from falsification cases or make falsification verdicts rejection-only.

ROADMAP — Verified

T-PB-B: The new hand-Rust boundary test is paired with an SG-0 census entry, P5 receipt, and dissolution trigger for retiring it into modeled run_target_verification.

⚠️ Two substrate/modeling issues need fixing before this should land.

briansrls · 2026-05-31T16:53:39Z

  | TargetCompileRejected { diagnostic_code: Symbol }

+// Phase 1 python CPython boundary — py_compile and python3 exec are distinct authorities.
+type TargetPythonExerciseVerdict


BLOCKING: TargetPythonExerciseVerdict is a new substrate coproduct without the required 🟢/🟡/🔴 dissolution tag, violating modeling-discipline Practice 4/P5.

briansrls · 2026-05-31T16:53:39Z

+    expected_happy_verdict: TargetPythonExerciseAccepted,
+    falsification: LeafModelPythonFalsificationCase {
+      fixture: python_r2b_runtime_fixture(),
+      expected_verdict: TargetPythonExerciseAccepted


BLOCKING: R2b records a LeafModelPythonFalsificationCase whose expected verdict is TargetPythonExerciseAccepted, so the model admits a "falsification" that succeeds, violating P2 illegal-states-unrepresentable.

Merge tip accidentally dropped EXPECTED_HAND_AUTHORED_TEST line for the #4117 boundary test while the file, integration.rs wiring, and INVARIANTS_OPS row remained live. Restores Net +0 for PR #4124. Co-authored-by: Cursor <cursoragent@cursor.com>

…) (#4124) * WIP: SG-2 implementation per sg2-type-expression worksheet on main — TargetTy * SG-2: worksheet §6 closure + P5 smoke receipts (substrate on main #3962) Add §5–§7 to the SG-2 worksheet, expand v4_std_target_realization_dag_smoke_test with three parse/tokenize smokes for TargetTypeExpressionProjection, and pair INVARIANTS_OPS / sg0 census / sg0-pr-body-append.4124.txt (+0 SG-0 paths). Co-authored-by: Cursor <cursoragent@cursor.com> * fix(SG-2): restore v4_leaf_model_python_r2_r3_external census entry Merge tip accidentally dropped EXPECTED_HAND_AUTHORED_TEST line for the #4117 boundary test while the file, integration.rs wiring, and INVARIANTS_OPS row remained live. Restores Net +0 for PR #4124. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Cursor <cursoragent@cursor.com>

…1.8 self-compile runway, §8.5 resolutions) Per operator 2026-06-01T01 approval-with-edits: 1. **Class B wording tightened** (§11.7.2): "required if already modeled" → "Only if part of current §11.7.1 safety floor OR selected by trusted affected-set/testgen". Prevents required surface from silently growing back. 2. **Explicit Rust emit pick** (§11.7.1 gate #3): chose `M1 v4 full-tree rust emit probe` (NOT both M1 + T-22 corpus rust). Rationale: M1 drives the residual-count catalogs (#4086/#4122/#4140) that inform dispatch; T-22 corpus rust duplicates same closure compile with no unique signal → demoted to Class C scheduled. 3. **§11.8 NEW: Language self-compile runway** with explicit rungs L0-L4 per language: - L0 leaf-model verification - L1 compiler-subset emit - L2 compiler-subset execution - L3 self-output fixed point - L4 full self-compile Per-language manager scope tabled: Rust (critical path, L1 in progress); Go (release-minimum, L0; clean external verifier advantage); Python (release-minimum, L0 complete via #4117); TypeScript (alpha/preview); C++ (capacity-permitting matrix only). Mechanical rules preserved (worksheet single-authority-fact gate, shared facts through Modeling DFS Arbiter). 4. **§8.5 operator decisions resolved** per operator sign-off: - P5 runtime gate: option (ii) authorized as WORKSHEET (not impl) in parallel with P3 - SG-8 / Modeling DFS succession: dedicated manager to spawn; PM does NOT act as DFS; keen-heron stays TR - TypeScript: authorized as alpha/preview language lane - Go/Python: authorized for self-compile runway per §11.8 - CI Coverage Bankruptcy Wave 1: APPROVED; spawn CI Manager - stern-lynx closeout (c): still pending (low-priority; role reconstituting anyway) INVARIANTS P2 single-authority preserved throughout: §8.5 canonical for sign-off state; §11.7 + §11.8 reference operator framing without claiming alternate authority. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>

* docs(planning): v4 dep graph Jun 1 release-day EOD — post-cascade snapshot Successor to docs/planning/v4-predicate-dependency-graph-2026-05-31.md (#4096) capturing the 2026-05-31 P3+P5 cascade end-of-day state on Jun 1 release day. Summary of today's predicate state movement: - P5 dep-graph-framing: Layer 1 + Layer 2 BOTH CLOSED via #4115 structural-bridge implementation (positive-Y CiUpsertStep replaces shell, bridge deleted); strict TASKS.md reading still has runtime-gate upward debt at adhoc-f8699326-d69 (operator decision pending). - P3: 8 of 9 routed classes closed/retired today (SG-1/7/5/6/1b/2/RC-LAYERING/SG-3-cascade-retired) + SG-8 worksheet on main (impl gated on §8). Residual rustc count stale at 7175 (#4122 catalog); fresh probe needed. - P2: scope (a) PROVEN; bridge deletion 14-day window starts today via #4097 M2 probe. Operator decision OR window completion gates full P2 GREEN. - T-38-PR2 verdict-surface migration LANDED #4120. Org change: proud-pike-680 archived mid-day; Modeling DFS lane consolidated under keen-heron-687 de facto. §8 sign-off authority for SG-8 impl needs operator routing. Tree health: 0 active subtree work at 00:30Z 2026-06-01. All 5 overnight PRs merged; #4112 operator-landed. Managers idle. Operator decisions pending (block forward progress): - P5 runtime gate (i) M1 cargo-clean subset vs (ii) bootstrap-evaluator corpus path (load-bearing per SELF_HOSTING) - P2-B bridge deletion authorization (or 14-day window wait) - SG-8 §8 sign-off authority routing post-proud-pike-archival No code paths changed; docs-only. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 codex RC fix — P5 canonical predicate single-authority Addresses codex REQUEST_CHANGES on #4137: §10 "P5 fully GREEN today" framing violated single-authority discipline against canonical TASKS.md predicate "TestClaim suite passes". Same snapshot at §3.5 / line 102 correctly named the runtime-execution gate as still open (adhoc-f8699326-d69), creating parallel dep-graph definition risk where a worker could treat P5 as done. Fix: §10 rewritten to lead with "P5 (canonical 'TestClaim suite passes' per TASKS.md): NOT fully GREEN today" — Layer 1+2 closed but runtime-execution gate remains open; explicit "do NOT treat as done" anti-misread phrasing. INVARIANTS P2/P3 single-authority + fail-closed documentation discipline preserved by aligning §10 with §3.5. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 codex RC fix 2 — eliminate "dep-graph framing P5 GREEN" alternate-authority phrasing Addresses codex second REQUEST_CHANGES on #4137: §8:156 "per dep-graph framing, P5 is GREEN (both layers closed)" was a second P5 status authority even in a risk/honesty section, despite §10 anchoring canonical TASKS.md status. A worker could read §8 as permission to close P5 before runtime-execution gate. Fix: §8 rewritten to lead with "P5 single authority: P5 is GREEN only when the canonical TASKS.md predicate 'TestClaim suite passes' is satisfied." Today's Layer 1+2 closures explicitly framed as "partial progress toward P5, not an alternate definition of GREEN." Adds explicit "Do not treat partial layer closure as P5 GREEN" anti-misread. INVARIANTS P2 single-authority discipline fully aligned: only the canonical predicate text in TASKS.md:816 defines what GREEN means for P5. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 expansion — operator sign-offs queue + remaining-7000 protocol + TS parallel ops Per operator request "tell me anything else that needs sign off up front + get this entire sheet fresh/ready": Added three new sections: - §8.5 Operator sign-offs queue (consolidated table; tracks all PM-waits-on-operator items including P2-B AUTHORIZED + fresh M1 probe AUTHORIZED that just dispatched) - §8.6 Remaining P3 residual cascade — explicit worksheet protocol clarity (probe → §10.0 → impl → repeat); names keen-heron as de facto manager pending routing decision - §8.7 TypeScript / cross-target parallel opportunities (TR-lane work feasible parallel to Rust residual; per Wave F F3 TS is v4-alpha-only; mirrors today's Python widening pattern) Also updated §1 P2 row: TECHNICAL-PROVEN / AUTHORITY-BLOCKED → TECHNICAL-PROVEN; DELETION IN FLIGHT (operator authorized 00:28Z; work-item adhoc-4cad7e9b-558 spawned to skip 14-day window). Pending operator decisions still in queue (per §8.5): - P5 runtime gate (i) M1 cargo-clean subset vs (ii) bootstrap-evaluator corpus path - SG-8 §8 sign-off authority routing - Modeling DFS Manager succession plan - TypeScript work plan authorization - stern-lynx closeout cond (c) Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 codex RC #3 + cursor RC fix — reconcile P2-B authorization state + correct ci.yml line citation Addresses combined codex (RC #3) and cursor (RC #1 on this PR) findings: 1. **P2-B authorization desync** (codex + cursor): §3.2, §4 Path B, §6, §6.5, §7, §10 all framed P2-B as pending operator decision, while §8.5 + §1 P2 row recorded the 00:28Z AUTHORIZED state. One snapshot, two authorities. Fix: every blocker/dispatch-board/watchlist mention of P2-B updated to "AUTHORIZED + in flight" with work-item URL adhoc-4cad7e9b-558. §8.5 is the single source of truth for sign-off state. 2. **ci.yml line citation wrong** (cursor): bridge step is at ci.yml:401-410 (the `v2 → v4 bootstrap resolve-posture gate` step); lines 378-385 are the unrelated phase1/nat_semiring gate (carried over from #4096 predecessor without verification). Fixed in §3.2. 3. **Fresh M1 probe also AUTHORIZED + in flight** (carried desync): §10 listed fresh M1 probe under "PM dispatches available pending operator authorization"; updated to reflect 00:28Z authorization + work-item adhoc-7b46e080-3cd in flight. INVARIANTS P2 (single authority) preserved: §8.5 is canonical for sign-off state; every other section now references or aligns with it. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 codex RC #4 + operator-blocking reviews fix — full single-authority cleanup Addresses three operator-blocking inline reviews + codex RC #4: 1. **TASKS.md line-number drift risk**: switched all `src/v4/TASKS.md:806-817` and `:816` citations to stable section anchor `src/v4/TASKS.md` "Definition of v4-done" (operator/codex flagged line-number cite as drift risk; using header anchor is robust against future renumbering). Note: current file content confirms predicates ARE at :813-817 under :805 header; operator's :572-584 suggestion doesn't match current main but the anchor switch sidesteps the issue entirely. 2. **ci.yml line-number drift risk**: switched all `.github/workflows/ci.yml:401-410` citations to step name `v2 → v4 bootstrap resolve-posture gate (CI emit-wall bridge)` (operator/cursor flagged 401-410 as not precisely the bridge step; step-name cite is robust + names exactly what gets deleted). 3. **Fresh M1 probe desync** (operator blocking on line 89): §6 listed as pending blocker owned by sharp-otter while §8.5 marked AUTHORIZED + in flight. §6 and §6.5 updated to reflect AUTHORIZED + work-item adhoc-7b46e080-3cd in flight (sleek-heron-13 spawned; PR #4140 7,724 errors +549 vs #4122). 4. **§7 PM-actionable contradiction** (codex RC #4): "No worker implementation dispatches blocked" contradicted SG-8 needing §8 routing. §7 rewritten to explicitly enumerate blocked items (SG-8, P5 runtime) referencing §6.5 dispatch board + §8.5 operator decisions queue. INVARIANTS P2 single-authority: §8.5 is the canonical sign-off state; §6 + §6.5 + §7 + §10 now all reference §8.5 rather than maintaining parallel state. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 codex/cursor RC #5+#6 fix — reconcile probe-result state + Path A no-overclaim Addresses two more blocking reviews: 1. **Probe-result state desync** (codex + cursor RC): §1 + §3.3 + §8 still framed "fresh probe needed" while §6.5/§8.5 recorded 7,724 result. Reconciled: §1 P3 row + §3.3 residual paragraph + §8 honesty bullet all now lead with the 7,724 result (sleek-heron-13 PR #4140) and note substrate-absorbed pattern; §8 final bullet clarifies per-class delta still pending review. 2. **§4 Path A overclaim** (codex RC): "Either flips strict P5 GREEN" was wrong — neither (i) nor (ii) flips P5 GREEN by routing decision alone. Rewrote Path A to make explicit: P5 GREEN requires TestClaim suite passes bullet satisfied by actual suite execution receipt; choice (i)/(ii) authorization unblocks dispatch toward that receipt. INVARIANTS P2 single-authority preserved: §8.5/§6.5 are canonical for state; every other section now references their 7,724 reading rather than maintaining parallel stale 7,175 references. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 §11 — proposed next-iteration management structure (operator-requested) Adds §11 covering operator-requested management redesign for post-Jun-1 next-iteration. Structural principle: fan out RCA + worksheet authoring; centralize single-authority approval per INVARIANTS P2. Roles defined (with scope / deliverable-by-end-of-tenure / exit criteria for each): - Modeling DFS Arbiter (fresh-spawn, NOT PM; single-authority gate) - 5 per-language RCA Managers: Rust, Python, Go, TypeScript (alpha/preview), C++ (later) - 6 shared substrate managers: ModuleGraph, TargetTypeExpression, TargetAtom, Collection/Algebra, Runtime/TestClaim, CI CI Manager scope captures post-cascade CI state: - substrate exists (ci.dag CiPipeline/CiJob/CiGate/CiUpsertStep) but runtime still YAML+shell - four-compile-redundancy in ci_v4 still unresolved per #4091 §1.2 - affected-set testing/building NOT yet via evaluator; weeks-to-months - deliverable: collapse 4 compiles to 1; YAML→CiUpsertStep; affected-set via evaluator; shell retirement; runtime ≤10min Coordination protocol + mechanical rule (no impl without §10.0 worksheet) preserved. PM scope under new structure: routing + escalation only; explicit DO NOT list (act as Arbiter, approve substrate, spawn impl without worksheet). Pending operator re-review per their message; if ratified, §11.4 lists immediate next-wave dispatch. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 §11.6 — concrete CI migration inventory per operator request Adds §11.6 with verified counts as of 2026-06-01T01:00Z post-#4139 main: Headline: - ci.yml: 73 YAML steps across 7 jobs - ci.dag: 47 modeled CiUpsertStep rows on main (W2.3 Buckets A+B+C+E + bankruptcy Tier-0 + #4115 P5) - scripts/: ~30 shell scripts (~22 production candidates for retirement; ~8 dev/test infra stays) Migration scope categorized (A-E): - A: Already modeled + receipt-parity (47 rows) - B: Pending modeling (gate/check steps, ~10): SG-0 net-shrink, R4-carve, fabrication sentinel, T-19 testgen, release-doc authority, install.sh pinned, manager-brief, test-timeout, rust toolchain, Gate #103 - C: Pending modeling (leaf-model boundaries, ~6): Phase 1 R1/R2a/R2b/R3-external for rust + python - D: Pending modeling (toolchain/cache, ~5): per-job duplication of isolation + rustup pin - E: Already retired (testclaim-corpus-gate.sh #4115, resolve-posture-gate.sh #4139, bankruptcy #4101) Shell retirement list enumerated (22 production scripts). Structural redundancies per #4091 §1.2: four-compile in ci_v4 (~14m savings), per-job HOME isolation (4× duplication), cache cleanup. Runtime authority migration coupled with P5 runtime gate (adhoc-f8699326-d69) — both are same SELF_HOSTING substrate work. Affected-set testing/building via evaluator: modeled substrate exists (ChangeSet → AffectedSet → AffectedSetProduced in src/v4/std/change.dag); runtime gap is same as P5 runtime gate. CI Manager near-term wins (executable without operator decision): migrate B+C, collapse D duplication, collapse four-compile redundancy. Long-pole: runtime authority migration (gated on P5 runtime decision). Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 codex RC fix — P2-B state DELIVERED (#4139 merged 00:50Z) Addresses codex RC: §11.6 line 324 said #4139 deleted the bridge script while §1/§3.2/§4/§6/§6.5/§7/§10 said "in flight" — inconsistent live state. Verified via git ls-tree origin/main: #4139 MERGED 2026-06-01T00:50:17Z (squash 12d1aa6); script + ci.yml step actually gone from main. All P2-B state references updated: - §1 P2 row: "TECHNICAL-PROVEN; DELETION IN FLIGHT" → "GREEN" - §3.2 section: header + body reflect #4139 MERGED with squash SHA - §4 Path B: "IN FLIGHT" → "DONE" - §6 blocker: "RESOLVED + DELIVERED" - §6.5 dispatch board priority 2: state "DONE 2026-06-01T00:50Z" - §7 PM dispatches: "DELIVERED via #4139 MERGED 00:50Z" - §8.5 sign-off queue: "DONE" with merge SHA - §10 watchlist: "P2: fully GREEN" INVARIANTS P2 single-authority restored: one accurate live-state authority across the doc; #4139 MERGED is the canonical fact. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 §11.7 — CI Coverage Bankruptcy: bare-minimum first + cut list + reframed CI Manager charter Per operator directive 2026-06-01T01: aggressive CI cut now, bare minimum survival floor, reframe CI Manager to "make affected-set + testgen the safety net" not "migrate every shell step". Restructured §11.7: §11.7.1 BARE MINIMUM SAFETY NET (what stays) — 5 required gates explicit: 1. fmt --check 2. bootstrap minimal viability (shell exception short-term) 3. ONE Rust emit/probe path (not four — collapse four-compile redundancy) 4. ci.dag structural receipt + CiUpsertStep schema checks 5. no-new-shell ratchet Target: cold PR ~5-10min (vs current 30-75min) §11.7.2 Four CI classes (A/B/C/D) for categorization. §11.7.3 AGGRESSIVE CUT LIST: now includes operator directive to PERMANENTLY delete all v3 integration tests (ci_integration Tier-0 I3 determinism_test, full v3 job: cargo test --lib --bins, clippy --features bootstrap-regen-fresh, etc) — DELETE not demote per project_spirit + #4101 bankruptcy. §11.7.4-6 unchanged (four-wave plan, cut rule, honesty ledger). §11.7.7 CI Manager REFRAMED charter: - Old: "migrate every shell step to CiUpsertStep" - New: "get the bare minimum safety net working in CI using affected-set + testgen" - Work lane prioritizes: bankruptcy cut → four-compile collapse → affected-set + testgen shadow → first active modeled skip → affected-set as Class A authority - Shell-to-CiUpsertStep migration becomes BACKGROUND/INCREMENTAL in service of affected-set needs, not a separate front - Explicit anti-patterns: don't migrate for completeness; don't maintain retired-lane ratchets; don't trust affected-set exclusively before Wave 3 proves it Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 — operator sign-off edits (Class B, M1 pick, §11.8 self-compile runway, §8.5 resolutions) Per operator 2026-06-01T01 approval-with-edits: 1. **Class B wording tightened** (§11.7.2): "required if already modeled" → "Only if part of current §11.7.1 safety floor OR selected by trusted affected-set/testgen". Prevents required surface from silently growing back. 2. **Explicit Rust emit pick** (§11.7.1 gate #3): chose `M1 v4 full-tree rust emit probe` (NOT both M1 + T-22 corpus rust). Rationale: M1 drives the residual-count catalogs (#4086/#4122/#4140) that inform dispatch; T-22 corpus rust duplicates same closure compile with no unique signal → demoted to Class C scheduled. 3. **§11.8 NEW: Language self-compile runway** with explicit rungs L0-L4 per language: - L0 leaf-model verification - L1 compiler-subset emit - L2 compiler-subset execution - L3 self-output fixed point - L4 full self-compile Per-language manager scope tabled: Rust (critical path, L1 in progress); Go (release-minimum, L0; clean external verifier advantage); Python (release-minimum, L0 complete via #4117); TypeScript (alpha/preview); C++ (capacity-permitting matrix only). Mechanical rules preserved (worksheet single-authority-fact gate, shared facts through Modeling DFS Arbiter). 4. **§8.5 operator decisions resolved** per operator sign-off: - P5 runtime gate: option (ii) authorized as WORKSHEET (not impl) in parallel with P3 - SG-8 / Modeling DFS succession: dedicated manager to spawn; PM does NOT act as DFS; keen-heron stays TR - TypeScript: authorized as alpha/preview language lane - Go/Python: authorized for self-compile runway per §11.8 - CI Coverage Bankruptcy Wave 1: APPROVED; spawn CI Manager - stern-lynx closeout (c): still pending (low-priority; role reconstituting anyway) INVARIANTS P2 single-authority preserved throughout: §8.5 canonical for sign-off state; §11.7 + §11.8 reference operator framing without claiming alternate authority. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 cursor RC fix — propagate §8.5 resolutions through §1/§4/§6/§6.5/§7/§10 Addresses cursor RC: §8.5 marked operator decisions #3-#8 RESOLVED at 01Z but §1/§4/§6/§6.5/§7/§10 still listed them as pending blockers / operator decisions. Single-authority violation per INVARIANTS P2. Reconciliation: - §1 P5 row: removed "operator decision pending"; added "option (ii) authorized as WORKSHEET per §8.5 #3" - §4 Path A: removed "operator decision required"; replaced with worksheet-authorized framing - §6 blockers table: P5 runtime gate + SG-8 §8 sign-off both struck-through with RESOLVED references - §6.5 dispatch board: P5 runtime gate + SG-8 §8 rows reframed to "RESOLVED; <next-step>" with Modeling DFS Arbiter as owner - §7 PM-actionable: SG-8 + P5 impl rephrased from "BLOCKED on operator decision" to "pending Modeling DFS Arbiter spawn + worksheet authoring" (sequenced post-resolution) - §10 watchlist: all 5 RESOLVED decisions struck-through with resolution summaries; added "Next dispatch actions" subsection listing the spawn-to-do queue (Modeling DFS Arbiter, CI Manager, language RCA Managers, P5 worksheet) INVARIANTS P2 single-authority restored: §8.5 is canonical; every other section now defers to §8.5 numbering with resolution status. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 operator-blocking RC fix — gate-vs-decision distinction + P2-GREEN propagation Addresses 3 operator-blocking inline reviews at lines 85/86/87: 1. **P5 runtime gate vs P5 routing DECISION** (operator line 86): §8.5 #3 conflated "routing decision resolved" with "gate resolved". The OPERATOR CHOICE between (i) and (ii) is resolved; the GATE itself (runtime executes + suite passes) is STILL OPEN. Reconciled: - §8.5 #3: "DECISION RESOLVED" not "RESOLVED"; explicit "gate itself remains OPEN" - §6 blockers: "(still OPEN)" qualifier on P5 runtime gate row - §6.5 dispatch board priority 1: "(gate OPEN; routing RESOLVED)" + exit-receipt sequence extended through ship+execute - §3.5 P5 + §10 + §1 P5 row unchanged (correctly already showed gate OPEN) 2. **SG-8 §8 sign-off authority routing vs §8 ratification** (operator line 87): §8.5 #4 conflated "authority routing resolved" with "§8 ratification resolved". The AUTHORITY question (who reviews) is resolved; the actual §8 RATIFICATION on SG-8 worksheet is a separate step that gates impl dispatch. Reconciled: - §8.5 #4: "ROUTING RESOLVED" with note that §8 ratification is separate post-Arbiter-spawn step - §6 blockers: "(authority routing resolved; ratification still open)" qualifier 3. **P2 stale-reference propagation** (operator line 85 related): §1 P4 row + §3.4 still said "hard-gated on P2 full PROVEN + P3 binary builds" — P2 is fully GREEN per #4139. Fixed both to reference only P3 binary builds as remaining gate. INVARIANTS P2 single-authority preserved: each predicate state distinguishes routing-decision-resolved vs gate-closure-pending; no parallel authorities for the same predicate state. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 codex RC fix — §3.5 P5 line 98 stale "decision pending" → reflect §8.5 #3 resolution Addresses codex RC at line 98: §3.5 still said "Operator decision pending" for (i) vs (ii) routing while §8.5 #3 records RESOLVED at 01Z with option (ii) WORKSHEET authorized. Single-authority violation per INVARIANTS P2. Fixed: §3.5 P5 paragraph now lead-frames the routing decision as RESOLVED (option (ii) WORKSHEET, per §8.5 #3) while preserving the canonical gate-OPEN reading (runtime ships + suite executes + passes). (i) noted as patient-wait alternative path downstream of P3 cascade. INVARIANTS P2 single-authority preserved: §8.5 canonical for sign-off state; §3.5 references it consistently. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> * docs(planning): #4137 codex RC fix — §6.5 priority 3 SG-8 routing-vs-ratification rename Addresses codex finding on §6.5 priority 3: state column said "RESOLVED" but exit receipt still required "§8 ratification → SG-8 impl worker dispatchable", creating ambiguous live-state. Fix: rename title from "SG-8 §8 sign-off authority" to "SG-8 §8 sign-off **routing** (NOT the ratification itself)"; state column now explicit about what's resolved (routing) vs pending (ratification). Sequence noted: Arbiter spawn → §8 ratification → SG-8 impl. This was the codex review on sha 4242a83 (3 commits behind HEAD); line 98 fix at 21b0b35 + gate-vs-decision distinction at f246e9d also already address the broader pattern. This rename is the final piece on the §6.5 row itself. INVARIANTS P2 single-authority preserved: state column reflects only what's actually resolved (routing); exit-receipt column names the remaining dispatchability gate. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 <noreply@anthropic.com>

… CI, L1 Author five ready-for-review worksheets per #4137 §11.8 Go row: leaf-model R1/R2a/R2b/R3-external (#4117 mirror), TargetAtomRealization extension, TargetTypeExpressionProjection extension, CiUpsertStep go build runners, and L1 compiler-slice go build receipt. Routes ratification through Modeling DFS Arbiter; TR lane for atom rows after §8. Co-authored-by: Cursor <cursoragent@cursor.com>

Replace optional boundary-test wording with mandatory Mechanism (b) checklist (INVARIANTS row + sg0 census +1 + scripts pairing) mirroring Co-authored-by: Cursor <cursoragent@cursor.com> #4117. Worksheet PR #4147 remains docs-only; no hand-Rust here.

…e) (#4147) * WIP: TypeScript RCA Manager — per #4137 §11.8 ALPHA/PREVIEW lane (NOT release * fix(planning): ECMA-faithful Symbol() factory for TS R3-external worksheets Symbol is callable but not constructable; new Symbol() must be falsification, not the happy path. Addresses PR #4147 blocking review (P1 / MDN grounding). Co-authored-by: Cursor <cursoragent@cursor.com> * fix(planning): pin §P5(b) hand-Rust receipt for TS leaf-model impl PR Replace optional boundary-test wording with mandatory Mechanism (b) checklist (INVARIANTS row + sg0 census +1 + scripts pairing) mirroring Co-authored-by: Cursor <cursoragent@cursor.com> #4117. Worksheet PR #4147 remains docs-only; no hand-Rust here. --------- Co-authored-by: Cursor <cursoragent@cursor.com>

* docs(planning): Go RCA §10.0 worksheets for L0 leaf-model, SG-1/SG-2, CI, L1 Author five ready-for-review worksheets per #4137 §11.8 Go row: leaf-model R1/R2a/R2b/R3-external (#4117 mirror), TargetAtomRealization extension, TargetTypeExpressionProjection extension, CiUpsertStep go build runners, and L1 compiler-slice go build receipt. Routes ratification through Modeling DFS Arbiter; TR lane for atom rows after §8. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(planning): fix Go leaf-model worksheet per openai-pro RC Practice 11: drop TargetGoCompileVerdict; R1/R2a/R3 use TargetCompileVerdict with toolchain data; R2b uses TargetRuntimeExerciseVerdict. Split compile-bound vs runtime-bound falsification contracts (R2b is go run/test, not compile FAIL). Co-authored-by: Cursor <cursoragent@cursor.com> * docs(planning): Go leaf-model worksheet — P5(b) bridge + R2b typed overflow §5: shell-only default; v3 boundary test forbidden without SG-0 + ROADMAP receipt bundle. §4.2: R2b fixtures use typed int64 var + runtime want (not MaxInt64+1 const). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Modeling DFS Arbiter — fresh dedicated role per #4137 §11.2 + §8.5 #4-#5 * docs: refresh authority map — Go worksheets APPROVED on #4149 Mark Go TargetAtomRealization and TargetTypeExpressionProjection rows APPROVED; note #4149 supersedes gentle-lynx draft #4145 for §8 closure. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Cursor <cursoragent@cursor.com>

…tic verifier). L0 complete (#4117 R1+R2a+R2b+R3-external on main). Goal by end of next iteration: L1 fixture-scale + L2 cross-target behavioral parity receipts (vs Rust/Go). Author worksheets for pyright/mypy structural checks, run (#4356) * WIP: Python RCA Manager — per #4137 §11.8 release-minimum lane (weaker static * feat(v4): Python L2 cross-target behavioral parity receipt (Worksheet C) Positive cross-target PARITY receipt — the exact complement of the merged cross-runtime DRIFT lane (python_cross_runtime_drift). The same modeled program realized in each target's native types AGREES on the common domain: - R2a: small-value integer add (2 + 3 = 5), inside the subdomain where arbitrary-precision (Python) and two's-complement (Rust/Go) coincide. - R3-external: Symbol nominal/value projection to the same payload ("x"). Drift proves divergence at the fixed-width boundary; parity proves agreement on the common domain — so the verifier demonstrably DISTINGUISHES the two rather than collapsing them. Substrate (mirrors the drift carrier, Facts Flow Forward): - std: LeafModelCrossTargetParityProbe + two claim ids (reuses ValueDiff<String>; PARITY is the positive property expected == actual). - lens: python_l2_parity_{r2a,r3}_probe + roster + per-target sources/values. - claim: src/v4/test/claim/language_model/python_l2_cross_target_parity.dag (wiring + positive-parity TestClaims). - boundary: v4_leaf_model_python_l2_cross_target_parity_test.rs (Python+Rust mandatory, Go corroborating) + SG-0 census registration. Drive-by: fix pre-existing EXPECTED_HAND_AUTHORED_NON_TEST sort violation introduced by #4338 (boundary_emit_gates.rs listed after process_exit.rs), which was failing sg0_expected_list_is_sorted_and_unique on the same test file. Closes Worksheet C in docs/planning/v4-python-rca-manager-worksheets-2026-06-01.md. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: Python RCA Manager — per #4137 §11.8 release-minimum lane (weaker static * fix(v4): ci_floor v4 bootstrap parse + strengthen SG-0 P5 receipt Two fixes for PR review/CI: 1. ci_floor (v2->v4 bootstrap full compile) was failing: the v4 production lexer's `should_start_interpolation` treats `{` immediately followed by an identifier char as a string interpolation start, so the Go R3 source literal `Symbol{value: "x"}` opened an interpolation that broke on the `:`. (v3's per-file `parse_for_test` is more lenient, so the local boundary test missed it.) Add a space — `Symbol{ value: "x" }` — matching the Rust R3 literal's `{ value: ... }` spacing, which already compiled clean. Still valid Go. Verified: `gunbc compile --source-root src/v4 --target dag` -> 0 diagnostics. 2. Strengthen the SG-0 EXPECTED_HAND_AUTHORED_TEST P5 receipt for the new boundary test to match the drift/Go siblings (codex + cursor REQUEST_CHANGES): cite the concrete ROADMAP.md `PB-Runtime-External-Toolchain-TestClaims` row (the exact deferral for host-spawned toolchain boundary tests) plus the "Tests as `.dag` TestClaim data" / "Pure bootstrap" rows, and state the census ratchet (+1 now, -1 at dissolution). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

briansrls added 3 commits May 31, 2026 15:27

WIP: Python R2a/R2b/R3-external widening — extend python.dag leaf-mod…

c8866f7

…el verif

WIP: Python R2a/R2b/R3-external widening — extend python.dag leaf-mod…

81a4280

…el verif

WIP: Python R2a/R2b/R3-external widening — extend python.dag leaf-mod…

d15a2b8

…el verif

briansrls marked this pull request as ready for review May 31, 2026 15:39

chore: apply cargo fmt to python R2/R3 boundary test

652abec

Fixes CI fmt gate on PR #4117. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls commented May 31, 2026

View reviewed changes

briansrls and others added 2 commits May 31, 2026 16:04

WIP: Python R2a/R2b/R3-external widening — extend python.dag leaf-mod…

5f87927

…el verif

briansrls merged commit 3d53b9d into main May 31, 2026
10 checks passed

briansrls commented May 31, 2026

View reviewed changes

This was referenced Jun 1, 2026

docs(planning): Go RCA §10.0 worksheets (L0 leaf-model, SG-1/SG-2, CI, L1) #4145

Closed

docs(planning): TypeScript L0 §10.0 worksheets (#4137 §11.8 alpha lane) #4147

Merged

briansrls mentioned this pull request Jun 1, 2026

[codex] draft Python RCA L1/L2 worksheets #4146

Merged

briansrls deleted the session/witty-fox-519 branch June 1, 2026 18:43

briansrls mentioned this pull request Jun 1, 2026

docs(ts): add L0 RCA authority receipts #4257

Closed

2 tasks done

briansrls mentioned this pull request Jun 3, 2026

docs(planning): TypeScript RCA L0 worksheets (alpha lane #4137 §11.8) #4396

Closed

7 of 8 tasks

Navigation Menu

Repository navigation

feat(leaf-model): python R2a/R2b/R3-external widening (MW-D3 cross-target) - #4117

feat(leaf-model): python R2a/R2b/R3-external widening (MW-D3 cross-target)#4117
briansrls merged 6 commits into
mainfrom
session/witty-fox-519

briansrls commented May 31, 2026 •

edited

Loading

Uh oh!

briansrls commented May 31, 2026

Uh oh!

briansrls left a comment

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls commented May 31, 2026

Uh oh!

briansrls commented May 31, 2026

Uh oh!

Uh oh!

briansrls left a comment

Uh oh!

briansrls May 31, 2026

Uh oh!

briansrls May 31, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

briansrls commented May 31, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Test plan

Uh oh!

briansrls commented May 31, 2026

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

This comment was marked as resolved.

Uh oh!

This comment was marked as resolved.

Uh oh!

briansrls commented May 31, 2026

Uh oh!

briansrls commented May 31, 2026

Uh oh!

Uh oh!

briansrls left a comment

Choose a reason for hiding this comment

Uh oh!

briansrls May 31, 2026

Choose a reason for hiding this comment

Uh oh!

briansrls May 31, 2026

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

briansrls commented May 31, 2026 •

edited

Loading