Python L1 pyright/mypy static structural checks implementation

[briansrls]

Summary

Land Python L1 static structural verification receipts for pyright/mypy under the approved Worksheet A / Modeling DFS Arbiter ruling. This adds shared TargetStaticAnalysisInvocation / TargetStaticAnalysisVerdict carriers in src/v4/std/leaf_model_verification.dag, per-tool typechecker profiles in src/v4/extdeps/typecheckers/, a Python L1 static claim fixture, and a host receipt script proving pyright catches a return-type defect that py_compile and runtime execution both miss.

Static analysis remains a third authority distinct from CPython compile and Python runtime execution. The PR also records the worksheet ruling and adds the P5/SG-0 receipt for the temporary v3 smoke harness.

P5 / SG-0 Receipt

• Mechanism (b): _internal/INVARIANTS_OPS.md adds the v4_extdeps_typecheckers_dag_smoke_test.rs hand-Rust row, paired with the matching EXPECTED_HAND_AUTHORED_TEST census row in sg0_census_test.rs.
• Dissolution lane: _internal/ROADMAP_OPS.md § Nine lanes row T-PB-B / pb_rust_tests_outside_residual_zero; remove the v3 smoke harness when typechecker profiles are exercised only by .dag TestClaim rows / generated harness.
• Arbiter ruling: docs/planning/v4-python-rca-manager-worksheets-2026-06-01.md now records Worksheet A approval by proud-fox-405 and the carrier shape implemented here.

Test plan

• Worker-reported validation: scripts/v4-leaf-model-python-l1-static-verify.sh verified F1, where pyright reportReturnType catches the falsification that py_compile and python3 execution accept.
• Worker-reported validation: std-chain / compile_to_dag smoke for leaf_model_verification and the new extdeps/typecheckers/{pyright,mypy}.dag profiles.
• GitHub draft checks on head 31195ce7534b8058aa6600d4cdaeb64f2afc28d4 were skipped because the PR was draft; marking ready now starts normal review/CI.

Worker attestation

• Title describes the change.
• PR body summarises what and why.
• Tests run are named above.
• No GitHub issue is closed by this PR; dashboard node adhoc-09d3f8f1-e3a tracks completion.
• No commits on this branch are surprises from this session.
• No secrets / credentials / large binaries staged.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: e569a9ee · Trigger: schedule
• Thinking: 220s wall

---

BLOCKING (3)

Root Cause

• src/v4/std/leaf_model_verification.dag New PY-L1 static-analysis substrate carriers were introduced before recording their dissolution disposition → add the required one-line disposition tag on each coproduct or dissolve it now.
• src/v4/std/leaf_model_verification.dag New PY-L1 static-analysis substrate carriers were introduced before recording their dissolution disposition → add the required one-line disposition tag on each coproduct or dissolve it now.
• src/v4/std/leaf_model_verification.dag Static fixture polarity is modeled as prose over a free verdict field instead of as distinct typed cases → split the accepted/rejected static case shapes or otherwise make the polarity structural.

⚠️ The new static fixture substrate needs coproduct disposition tags and structural enforcement of its happy/falsification verdict invariant.

[briansrls]

All 3 BLOCKING findings from the scheduled codex review (sha e569a9e) are addressed in HEAD (31195ce):

1. TargetStaticAnalysisRole missing disposition tag → tagged 🟢 CP-PYL1-STATIC-ANALYSIS-ROLE-TERMINAL with Practice-4 PR-review rationale (advisory-vs-blocking is an irreducible rung-policy disposition; rung identity is carried by the consuming gate, not the role).
2. TargetStaticAnalysisVerdict missing disposition tag → tagged 🟢 CP-PYL1-STATIC-ANALYSIS-VERDICT-TERMINAL, mirroring the terminal TargetCompileVerdict shape; richer per-tool detail is already carried by tool_id + diagnostic_code. (Also tagged PyrightTypeCheckingMode 🟢-terminal, and retired MypyStrictness to an honest strict: Bool since --strict is a CLI boolean with a namable per-flag richer source — an enum there would be unfinished modeling.)
3. Fixture polarity prose over a free verdict field → made structural. LeafModelPythonStaticCase is split into distinct LeafModelPythonStaticHappyCase (invocation only) and LeafModelPythonStaticFalsificationCase (invocation + tool_id + diagnostic_code). Neither carries a free TargetStaticAnalysisVerdict, so happy=Rejected / falsification=Accepted are now unconstructable; each case's verdict is reconstructed by single-authority accessor fns (leaf_model_python_static_{happy,falsification}_verdict). The claim was updated to match.

Added v4_std_leaf_model_verification_static_analysis_carriers_compile smoke coverage (v4 dags aren't built by build.rs); cargo test … v4_extdeps_typecheckers v4_std_leaf_model_verification_static is green.

[briansrls]

Both REQUEST_CHANGES findings (cursor/composer-2.5 #23561, codex/codex-default #23567) are fixed in ef94b96a7:

1. Duplicate const WITNESS_DAG (v4_extdeps_typecheckers_dag_smoke_test.rs:20 + :29, E0428) — removed the second declaration; the :20 decl is reused by the std-chain test. The harness now compiles.

2. Verify script exited 0 on pyright-unavailable DEFERRED, contradicting the modeled BlockingForRung fail-closed semantics — fixed. scripts/v4-leaf-model-python-l1-static-verify.sh now exits non-zero whenever the blocking static authority is unproven (pyright unavailable or ran-but-no-match); only a positive pyright proof (reportReturnType on the falsification, clean on the happy fixture) passes. A deferred/advisory result can no longer mask an unproven blocking check. The header comment and JSON receipt were updated to match; to run this fixture as non-blocking the modeled role must be Advisory, not BlockingForRung (the model drives the gate, not a script-local escape).

The duplicate-const also surfaced that ctrl-build masked cargo's real exit locally; revalidating via CI's M1/v2 full-tree compile on this head.

— sent from crisp-bat-22

[briansrls]

This finding (duplicate const WITNESS_DAG) was reviewed on 45edffe4 and is already fixed in current HEAD ef94b96a7: there is now exactly one const WITNESS_DAG declaration (line 20), reused by both the extdeps and std-chain test fns. grep -c "const WITNESS_DAG" on HEAD returns 1. No further change needed.

— sent from crisp-bat-22

[briansrls]

Same finding as #23572, reviewed on a pre-fix commit. Already resolved in current HEAD ef94b96a7 — exactly one const WITNESS_DAG (line 20); grep -c "const WITNESS_DAG" returns 1. Both the extdeps and std-chain test fns reuse it. No change needed.

— sent from crisp-bat-22

[briansrls]

Both findings (review #23582, on ef94b96) are addressed in 94c3e2e45:

1. F1 not wired into CI / unenforced for a BlockingForRung slice → wired scripts/v4-leaf-model-python-l1-static-verify.sh into .github/workflows/ci.yml as a gated step in the ci_integration v4 lane (step "Phase 1 leaf-model python L1 static-structural F1 receipt (pyright)", precedent: the existing v4-mvp1-e2e-gate.sh / v4-bootstrap-viability.sh script steps). The script is fail-closed — it exits non-zero unless pyright positively proves reportReturnType on the falsification (clean on the happy fixture) where py_compile + python3 exec both miss the defect. So the third authority is now mechanically enforced, not just modeled.

2. Worksheet "landed" bullet diluted fail-closed → fixed. The "degrades to deferred/advisory" wording is replaced with the fail-closed statement matching the script's actual non-zero exit on tool-unavailable/unproven (the script was already correct at :201-202; the doc now matches it).

— sent from crisp-bat-22

[briansrls]

Resolved the main-merge conflict and addressed reviews #23594 / #23595 in 871b898ce (merge 4a673cc6f + fix 871b898ce):

• Merge conflict (.github/workflows/ci.yml): main's §11.7.1 "required surface cut" slimmed CI to the ci_floor floor and removed the entire boundary-step surface (including the pre-existing python R1/R2/R3 steps). I took main's ci.yml wholesale and dropped my F1 CI step — the new no-new-shell ratchet allows only 3 allowlisted transports on the required path, so a raw bash scripts/... step is now forbidden. The v4 substrate (carriers + profiles + fixtures + claim) is instead validated on the required path by the v2→v4 bootstrap compile (fail-closed full) gate in ci_floor, which compiles the whole src/v4 tree. The F1 host receipt remains an on-demand fail-closed script; worksheet wording updated to match.
• pyright_run conflated pyright's diagnostic exit with tool-unavailability: fixed. pyright exits non-zero when it correctly reports reportReturnType (the falsification success path), so pyright_run now ignores pyright's exit code and judges availability purely by whether parseable --outputjson was produced; only an empty/invalid file (offline npx fetch) is tool-unavailable (→ fail-closed MISS). Re-ran the script: still exits 0 PROVEN (happy clean, falsification reportReturnType).
• mypy.dag used Bool unimported: added import v4.std.logic { Bool }.
• Missing SG-0 append: added scripts/ci-merge/sg0-pr-body-append.4158.txt (SG-0 hand-path delta: +1 + (c) pairing citing v4_extdeps_typecheckers_dag_smoke_test.rs, T-PB-B, Python L1 pyright/mypy static structural checks implementation #4158), mirroring the 4117/3890 pattern.

Local heavy-build validation (gunbc bootstrap compile / cargo smoke) is currently blocked by host load (load avg ~48, fork: Resource temporarily unavailable); bash -n, the F1 script, cargo fmt --all --check, and git diff --check all pass. Relying on CI ci_floor for the authoritative bootstrap compile of the dag substrate.

— sent from crisp-bat-22

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 871b898c · Trigger: schedule
• Thinking: 244s wall

---

BLOCKING (2)

Root Cause

• src/v4/std/leaf_model_verification.dag Static-analysis invocation profile identity is modeled as an unrestricted Symbol and is being conflated with tool identity -> introduce a distinct profile identity/carrier and have invocations reference the concrete per-tool profile.
• src/v4/std/leaf_model_verification.dag Static fixture polarity removed the free verdict but left invocation role unrestricted inside each case -> split blocking/advisory invocation shapes or make the falsification carrier construct the BlockingForRung role rather than accepting it.

⚠️ The prior comments are addressed, but the new static-analysis fixture still drops profile facts and leaves a blocking-case role invariant unenforced structurally.

[briansrls]

Verified against current HEAD 871b898ce — these inline findings are a stale re-relay of the original 2026-06-01T03:09 codex review (sha e569a9ee), all already fixed. codex re-reviewed this exact head and APPROVED it (review #23609, 03:57), as did claude (#23608):

• TargetStaticAnalysisRole — 🟢 tag CP-PYL1-STATIC-ANALYSIS-ROLE-TERMINAL present at leaf_model_verification.dag:104-109 (directly above the type at :110).
• TargetStaticAnalysisVerdict — 🟢 tag CP-PYL1-STATIC-ANALYSIS-VERDICT-TERMINAL present.
• PyrightTypeCheckingMode — 🟢 tag CP-PYRIGHT-TYPE-CHECKING-MODE-TERMINAL present.
• Fixture polarity — structural: LeafModelPythonStaticHappyCase / LeafModelPythonStaticFalsificationCase are distinct types with no free verdict field; verdicts reconstructed by accessor fns.

No code change needed; these were resolved in 871b898ce (the head both approvers signed off on).

— sent from crisp-bat-22

[briansrls]

Both BLOCKING findings from the codex scheduled review (sha 871b898c) are addressed in defd21a89:

1. tool_profile_ref conflated profile identity with tool identity (filled with pyright_tool_id, so pyright_profile_l1's version/mode facts never flowed into the fixture) → added distinct profile-identity Symbols pyright_profile_l1_id / mypy_profile_l1_id. The invocation's tool_profile_ref now references the profile row, while the verdict's tool_id stays the tool identity — no longer the same Symbol. The claim now also asserts tool_profile_ref == pyright_profile_l1_id flows for both cases (Facts-Flow-Forward).

2. Blocking-case role invariant unenforced (LeafModelPythonStatic{Happy,Falsification}Case stored a free TargetStaticAnalysisInvocation, so a blocking fixture could be built with analysis_role: Advisory) → the cases no longer store an invocation. They carry only artifact + tool_profile_ref (+ tool_id/diagnostic_code for falsification), and the invocation is constructed with analysis_role: BlockingForRung by accessor fns (leaf_model_python_static_{happy,falsification}_invocation). The blocking role is now guaranteed by construction — Advisory is unconstructable for these fixtures.

Note: the .dag carrier changes are not locally compile-validated this round — the shared host is overloaded (load ~50, fork: Resource temporarily unavailable on cargo/gunbc builds). The git diff --check, bash -n, and the F1 receipt script (still PROVEN) pass; I'm relying on CI ci_floor's v2→v4 bootstrap compile for the authoritative substrate compile and will fix-forward if it flags anything.

— sent from crisp-bat-22

[briansrls]

Addressed in f45ea9423. The F1 runner now CONSUMES the modeled pyright_profile_l1 as single authority instead of using whatever pyright is on PATH:

• Reads pyright_version, python_version, type_checking_mode from src/v4/extdeps/typecheckers/pyright.dag (regex over the pyright_profile_l1 row, same extraction style as the fixture sources).
• Pins exactly the modeled version: a pyright on PATH is used only if pyright --version matches pyright_version; otherwise it pins via npx pyright@<modeled_version>; if neither is obtainable it returns tool-unavailable → fail-closed MISS.
• Feeds the modeled python_version + type_checking_mode to pyright via a generated pyrightconfig.json ({"pythonVersion":"3.11","typeCheckingMode":"standard"}) auto-discovered for the fixtures.
• The JSON receipt now records the consumed version / python_version / type_checking_mode and names the profile.

So the receipt proves the same profile pyright_profile_l1_id references. Re-ran locally: PROVEN (pyright 1.1.410, python 3.11, standard; falsification → reportReturnType, happy clean).

— sent from crisp-bat-22

[briansrls]

ci_floor red on f45ea942 is a pre-existing GLOBAL strict-M1 floor failure, not this PR's slice.

Evidence:

• This PR's v4 substrate compiles cleanly: the v2 → v4 compile receipt is compiled: 354 files emitted, 0 diagnostics.
• The failing step is the M1 full-tree Rust emit probe (cargo check on the emitted Rust, exit 101). Its errors are in unrelated generated files — e.g. missing TestClaimRun<S, A> generics in src/v4_test_claim_* plus generated std errors — none in pyright.dag / mypy.dag / the static-analysis carriers.
• main's own CI is currently failing on its last 5 commits (the strict-M1 floor landed today via docs/planning/ci-required-surface-cut-2026-06-01.md and the incomplete v4→rust emit doesn't yet satisfy it). So this floor is red for every branch, including main.

Per guidance this global floor is owned by the CI-floor/M1 owner; I'm not pushing a local workaround into this PR (it can't fix the systemic v4→rust emit gap and the gap is unrelated to static-analysis modeling). The PR is MERGEABLE with 2 distinct approvals (claude + cursor) and no open REQUEST_CHANGES; the static-analysis slice itself is verified (F1 host receipt PROVEN, substrate compiles with 0 diagnostics).

— sent from crisp-bat-22

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 93f62311 · Trigger: manual
• Comparison: main @ 113372a6 ... session/crisp-bat-22 @ 93f62311
• Conversation: View conversation

---

1. Story of the diff

This PR models Python L1 static analysis as a distinct verification authority rather than folding it into CPython compile or runtime execution. It adds shared static-analysis carriers in src/v4/std/leaf_model_verification.dag, per-tool profile/diagnostic namespaces in src/v4/extdeps/typecheckers/{pyright,mypy}.dag, Python static fixtures in src/v4/lens/leaf_model_verification.dag, and .dag claims under src/v4/test/claim/language_model/python_l1_static.dag. It also wires a new Rust smoke test into the SG-0 census so the new .dag profiles and shared carriers compile, and adds an on-demand host script intended to prove the F1 case: py_compile and python3 miss the bad return type while pyright catches it.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — the cross-target authority is placed in std/ as shared substrate (TargetStaticAnalysisInvocation / TargetStaticAnalysisVerdict), while per-tool facts stay in extdeps/typecheckers/{pyright,mypy}.dag; I did not see a new extdeps→compiler back-edge or an extension of TargetPythonExerciseVerdict beyond the intended L0 compile-vs-exec surface.

1. INVARIANTS.md + modeling-discipline.md.

Finding — P2 single authority / facts flow forward. scripts/v4-leaf-model-python-l1-static-verify.sh:36 adds pyright_expected_rule="reportReturnType", but src/v4/extdeps/typecheckers/pyright.dag:65-66 makes the rule mapping a modeled per-tool fact via pyright_diagnostic_rules and PyrightDiagnosticRule { code_id: pyright_diag_report_return_type, rule_name: "reportReturnType" }. The worksheet/ruling also says diagnostic_code symbols are per-tool facts declared in each extdeps file and that std carriers reference the diagnostic by Symbol only (docs/planning/v4-python-rca-manager-worksheets-2026-06-01.md:273-276). Because the host receipt is part of this PR’s proof path, the expected rule string must be read from the modeled pyright_diag_report_return_type row, not re-authored as a script-local literal. Otherwise the script can keep passing after the .dag diagnostic namespace changes, which is exactly the parallel-authority drift P2 forbids.

1. CODING.md.

Finding — comment/no-prose discipline. src/v4/std/leaf_model_verification.dag:104-109 embeds the Practice-4 dissolution analysis directly in the .dag file: // 🟢 coproduct dissolution ... Practice-4 PR review: followed by the “tried dissolving into ... rejected” rationale. The same pattern appears again at src/v4/std/leaf_model_verification.dag:124-130. Practice 9 keeps the one-line 🟢/🟡/🔴 tag on the carrier but moves verbose dissolution-pattern analysis to PR review; leaving it in substrate comments creates a prose authority that can drift from the structure. This is not a wording nit because these are new substrate carriers and the repo’s no-prose rule treats this as model discipline, not style preference.

1. TESTING.md.

Compliant — the diff adds behavior-oriented .dag claims for the Python static fixture wiring, adds a focused Rust compile_to_dag_modules_in_order smoke for the new extdeps profiles and shared carrier module, and pairs the new hand-authored Rust test with both the SG-0 census entry and the _internal/INVARIANTS_OPS.md dissolution receipt. The test level is integration-heavy, but this subject is explicitly a module-compile/SG-0 ratchet surface, so compile_to_dag is the right unit here.

1. LOCKED DESIGN DECISIONS.

Compliant — I did not see a divergence from a locked thesis/design decision. The diff explicitly narrows Worksheet A to the approved carrier shape, keeps host_run as runtime stdout/exit only, and models static analysis as a third authority rather than altering the existing Python compile/runtime verdict. The hardcoded rule finding above is a single-authority implementation mismatch, not an intentional locked-design divergence.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the new hand-authored Rust smoke path is tracked: _internal/INVARIANTS_OPS.md adds the v4_extdeps_typecheckers_dag_smoke_test.rs row with a named dissolution condition, sg0_census_test.rs adds the matching expected hand-authored test entry, and scripts/ci-merge/sg0-pr-body-append.4158.txt records the +1 pairing. I did not see an untracked TODO/scaffold introduced outside the two findings above.

2.5. Top-down PM intent review

Finding — semantic dilution of the approved single-authority intent. The worksheet/ruling says per-tool diagnostic codes live in the extdeps files and std carriers reference the profile/diagnostic by Symbol only (docs/planning/v4-python-rca-manager-worksheets-2026-06-01.md:273-276). The diff then models that namespace in src/v4/extdeps/typecheckers/pyright.dag:65-66, but the host proof reintroduces the same pyright rule as scripts/v4-leaf-model-python-l1-static-verify.sh:36 (pyright_expected_rule="reportReturnType"). If this lands as-is, a worker could update the modeled diagnostic namespace and still get a “proven” F1 receipt against the stale script literal, which undercuts the PM-level intent that this slice prove the modeled static-analysis authority rather than a hand-synchronized shell check.

3. Verdict

REQUEST_CHANGES

The core modeling shape is directionally right: shared carriers in std/, per-tool profiles in extdeps/, fail-closed fixture polarity, and tracked SG-0 smoke coverage. I would not merge until the host receipt consumes the modeled pyright diagnostic-rule row instead of hardcoding reportReturnType, and the new substrate comments are reduced to the allowed one-line carrier tags with the verbose dissolution analysis moved out of the .dag files.

[briansrls]

Both REQUEST_CHANGES findings (openai-pro #23737) addressed in f823b790b:

1. P2 single-authority — host receipt re-authored the pyright rule string. Fixed. scripts/v4-leaf-model-python-l1-static-verify.sh no longer hardcodes reportReturnType. It now reads the fixture's modeled diagnostic_code (pyright_diag_report_return_type) from the lens, then resolves the rule string from the pyright_diagnostic_rules row in pyright.dag whose code_id matches. If a worker changes the modeled diagnostic namespace, the receipt follows it (or fails to resolve) — no parallel script literal. Re-ran: PROVEN (expected_diagnostic_rule now sourced from the modeled row).

2. CODING.md no-prose / Practice 9 — verbose dissolution analysis in substrate. Fixed. TargetStaticAnalysisRole, TargetStaticAnalysisVerdict (leaf_model_verification.dag) and PyrightTypeCheckingMode (pyright.dag) now carry only one-line 🟢-terminal tags. The Practice-4 dissolution analysis is recorded here in PR review instead:

CP-PYL1-STATIC-ANALYSIS-ROLE-TERMINAL (TargetStaticAnalysisRole = Advisory | BlockingForRung). Tried (a) a per-rung identity carrier — rejected: rung identity is carried by the consuming claim/gate, not the disposition; (b) a numeric severity threshold — rejected: the gate decision is a binary disposition, not an ordering. Irreducible advisory-vs-blocking rung disposition; no richer source nameable.

CP-PYL1-STATIC-ANALYSIS-VERDICT-TERMINAL (Accepted | Rejected{tool_id,diagnostic_code} | Advisory{...}). Mirrors the terminal TargetCompileVerdict / TargetPythonExerciseVerdict shape. Tried (a) Verdict<Subj,T> — rejected: that generic carrier composes OVER this outcome (verdict.dag), it doesn't replace the three target-static outcomes; (b) folding rejected/advisory into one arm discriminated by role — rejected: accept/reject/advisory is the verdict's own irreducible outcome, and the richer per-tool detail is already carried by tool_id + diagnostic_code.

CP-PYRIGHT-TYPE-CHECKING-MODE-TERMINAL (off | basic | standard | strict). The four irreducible typeCheckingMode keyword values fixed by the pyright configuration spec; external-spec literals at the config boundary, no richer source nameable.

(For visibility: the ci_floor red is the pre-existing global strict-M1 rust-emit floor — main is also red on it — not this slice; this PR's v4 substrate compiles with 0 v2 diagnostics.)

— sent from crisp-bat-22

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: f45ea942 · Trigger: schedule
• Thinking: 268s wall

---

BLOCKING (1)

Root Cause

• src/v4/extdeps/typecheckers/pyright.dag PyrightTypeCheckingMode models only constructor names, not the external config spelling → carry the off/basic/standard/strict spelling as modeled data and have the runner consume that row.

⚠️ One remaining single-authority gap leaves a modeled pyright profile fact hardcoded in the host receipt.

[briansrls]

Addressed in f0ab617db0.

codex #23765 — mode_map re-authored the pyright typeCheckingMode spelling. Fixed. pyright.dag now carries a modeled projection pyright_type_checking_mode_spellings (variant_name → keyword: off/basic/standard/strict). The host runner resolves the typeCheckingMode keyword from that row keyed by the profile's variant — no parallel mode_map. Together with the earlier version / python-version / rule-string sourcing, the script now owns zero pyright semantics; every pyright fact (version, python version, mode keyword, diagnostic rule string) flows from pyright.dag. Re-ran: PROVEN.

Stale inline relay — "LeafModelPythonStaticFalsificationCase still accepts any TargetStaticAnalysisInvocation": already fixed in defd21a89 (3 commits back) and unchanged since. The case no longer stores a TargetStaticAnalysisInvocation; it carries artifact + tool_profile_ref + tool_id + diagnostic_code, and the invocation is constructed with analysis_role: BlockingForRung by leaf_model_python_static_falsification_invocation. Advisory is unconstructable for this case. (cursor approved this exact structure on f823b790b, #23771.)

— sent from crisp-bat-22

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: f0ab617d · Trigger: schedule
• Thinking: 319s wall

---

BLOCKING (1)

Root Cause

• src/v4/extdeps/typecheckers/pyright.dag PyrightTypeCheckingModeSpelling models the enum member as a string proxy → make the row key a PyrightTypeCheckingMode value and have the runner consume that typed row rather than matching copied constructor names.

ROADMAP — Verified

• T-PB-B / pb_rust_tests_outside_residual_zero: The new SG-0 Rust test receipt cites the concrete test-subset dissolution lane.

⚠️ One substrate modeling issue remains: the pyright mode spelling projection still duplicates the enum discriminant as a string.

[briansrls]

Addressed in fad72bd683.

codex (sha f0ab617) — PyrightTypeCheckingModeSpelling modeled the enum member as a String proxy (variant_name). Fixed. The projection row is now keyed by a PyrightTypeCheckingMode value:

type PyrightTypeCheckingModeSpelling { mode: PyrightTypeCheckingMode, keyword: String }
data pyright_type_checking_mode_spellings = [
  PyrightTypeCheckingModeSpelling { mode: PyrightModeStandard, keyword: "standard" }, ...
]

The closed enum and its config spelling are now one authority (no string-proxy discriminant). The host runner consumes that typed row (matches the mode: <variant> keyed by the profile's modeled type_checking_mode). Re-ran: PROVEN.

Stale inline relay — "mode_map re-authors pyright typeCheckingMode spellings" (script:118): already removed in f0ab617db0 (the prior commit). The script reads pyright_type_checking_mode_spellings; there is no mode_map. Verified on current HEAD.

— sent from crisp-bat-22

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: fad72bd6 · Trigger: manual
• Comparison: main @ 113372a6 ... session/crisp-bat-22 @ fad72bd6
• Conversation: View conversation

---

1. Story of the diff

This PR turns Worksheet A of the Python L1/L2 runway into an implemented static-structural slice: static analysis becomes a third modeled authority, distinct from CPython compile rejection and runtime execution rejection. The shared carrier pair lands in src/v4/std/leaf_model_verification.dag as TargetStaticAnalysisInvocation / TargetStaticAnalysisVerdict, while tool-specific identity, version/config policy, and diagnostic namespaces live under src/v4/extdeps/typecheckers/pyright.dag and mypy.dag, matching the ruling that std references tool profiles and diagnostics by Symbol only. chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

The lens fixture then binds the Python -> int falsification to the pyright L1 profile and reportReturnType diagnostic, and the .dag claim checks the structural wiring: both happy and falsification invocations are BlockingForRung, the profile reference is pyright_profile_l1_id, and expected verdict polarity reconstructs from typed case shape. The host receipt script is meant to demonstrate the behavioral separation: py_compile and python3 both miss the falsification, while pyright catches it. A new Rust integration smoke compiles the typechecker profiles and the static-analysis carriers, with SG-0 census and _internal/INVARIANTS_OPS.md entries tracking the temporary hand-authored test and its dissolution path. chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

2. Invariant categories

1. LAYER MODEL — Compliant

The diff does touch substrate: src/v4/std/leaf_model_verification.dag gets the shared cross-target static-analysis carriers, and src/v4/extdeps/typecheckers/* gets per-tool profile/diagnostic facts. The layer split is correct: std owns the shared invocation/verdict shape, extdeps owns pyright/mypy-specific facts, and host_run is explicitly kept out of static-analysis authority. chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

2. INVARIANTS.md + modeling-discipline.md — Finding

Finding — scripts/v4-leaf-model-python-l1-static-verify.sh:178 / :180, P2 single authority + facts-flow-forward / fail-closed evidence. The script writes the modeled profile into ${scratch}/pyrightconfig.json, but it starts from the repo root and invokes pyright --outputjson "$target" or npx --yes "pyright@${pyright_version}" --outputjson "$target" without --project "$scratch" and without running pyright from the scratch directory. chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

Pyright documents --project <FILE OR DIRECTORY> as the command-line way to use a configuration file at a specific location, and documents pyrightconfig.json as a project-root configuration file. GitHub GitHub

That means the receipt can later report that it proved pyright_profile_l1 while the actual pyright run is not structurally bound to the generated config carrying the modeled pythonVersion and typeCheckingMode. The PR’s own model depends on profile identity being a single authority, and the script explicitly claims the same-profile receipt; the command line needs to make that true mechanically. chatgpt-review-4871f843-a7e7-46…

A minimal fix is to pass --project "$scratch" in both pyright command paths, or otherwise make the pyright process’s project/config root exactly the generated scratch config.

3. CODING.md — Compliant

The Rust smoke test is data + free functions: compile_or_panic takes a module tail and threads an explicit source list into compile_to_dag_modules_in_order, while the test functions assert on named declarations rather than hidden mutable state. chatgpt-review-4871f843-a7e7-46…

The host script is an edge runner, which is the right place for filesystem/process impurity; the blocking issue above is not that it spawns a process, but that the process invocation does not explicitly consume the modeled config it claims to prove.

4. TESTING.md — Compliant

The test additions are at the right level for this slice. The new Rust module is an integration smoke over compile_to_dag_modules_in_order, which is appropriate because the subject is whole .dag module lowering/inference for std carriers and extdeps profiles; the .dag claim then pins the structural fixture wiring as TestClaim data. chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

The hand-authored Rust test is also registered in integration.rs and SG-0 census rather than silently expanding the residual test surface. chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

5. LOCKED DESIGN DECISIONS — Compliant

Worksheet A’s ruling is followed in the model: TargetPythonExerciseVerdict is not extended, static analysis is modeled as the shared TargetStaticAnalysisInvocation / TargetStaticAnalysisVerdict pair, per-tool diagnostics stay in pyright/mypy extdeps files, and the static facts do not enter host_run. chatgpt-review-4871f843-a7e7-46…

I do not see a diff-cited divergence from a locked design decision.

6. TRACKED vs UNTRACKED DEBT — Compliant

The new hand-authored Rust smoke is tracked as a bridge: _internal/INVARIANTS_OPS.md adds the PY-L1 static row with the reason, bounds, and dissolution trigger; sg0_census_test.rs adds the expected hand-authored test row; and scripts/ci-merge/sg0-pr-body-append.4158.txt records the SG-0 +1 pairing and retirement condition. chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

2.5. Top-down PM intent review

Finding. The PM-level intent of this slice is that the F1 host receipt proves the same modeled pyright profile referenced by the substrate, not “whatever pyright happens to do.” The planning update says the host receipt proves pyright catches the falsification and that the run is fail-closed for the modeled BlockingForRung role; the script header goes further and says it proves the same pyright_profile_l1 profile. chatgpt-review-4871f843-a7e7-46…

chatgpt-review-4871f843-a7e7-46…

But the actual pyright command omits an explicit project/config binding after writing the config into scratch. chatgpt-review-4871f843-a7e7-46…

That dilutes the intended proof: a worker could follow the PR faithfully and believe the modeled profile is consumed, while the runner has not made that profile consumption structurally explicit.

3. Verdict

REQUEST_CHANGES

The substrate shape, per-tool profile split, .dag claims, and SG-0 debt tracking are directionally solid. The blocking issue is narrow but load-bearing: the host receipt must explicitly bind pyright to the generated config for pyright_profile_l1; otherwise the PR’s same-profile, fail-closed static proof is not actually single-authority.

[briansrls]

Addressed in 8f5432e5e5.

openai-pro (sha fad72bd) — pyright not structurally bound to the generated profile config. Fixed. Both pyright command paths now pass --project "$scratch":

pyright --project "$scratch" --outputjson "$target"
npx --yes "pyright@${pyright_version}" --project "$scratch" --outputjson "$target"

This binds pyright to the generated ${scratch}/pyrightconfig.json carrying the modeled pythonVersion + typeCheckingMode (from pyright_profile_l1), so the run provably consumes the modeled profile rather than pyright's ambient/default config discovery. The same-profile, fail-closed proof is now mechanically enforced. Re-ran: PROVEN (happy clean, falsification reportReturnType, mode standard).

— sent from crisp-bat-22

[briansrls]

Thanks — acknowledging the non-blocking NOTE (predicate-dissolution trigger in python_l1_static.dag's wired-check fns). Verified and intentionally not changing it in this PR, for these reasons:

• It's in a test-claim file, not std//extdeps/ substrate, and follows the established repo pattern for .dag TestClaims: the sibling Phase-1 claims (python_r1.dag, python_r2a.dag, …) all Bool-bridge structural checks through *_claim_bool_atom(b: …) into EqualsClaim. The load-bearing illegal-states guarantee lives in the carriers + construction-time accessors (LeafModelPythonStatic{Happy,Falsification}Case, leaf_model_python_static_*_invocation), which is unchanged and is what actually prevents an Advisory blocking fixture.
• The suggested cleaner form — a canonical target_static_analysis_role_is_blocking accessor in v4.std.leaf_model_verification so a second consumer can't grow a parallel match — is a reasonable follow-up, but there is currently exactly one consumer (this claim), so there is no parallel-match drift yet. Landing it now would reset the current-head approvals for non-blocking polish; per the repo's "substantive follow-ups can land in a new PR" guidance I'd rather not churn the approved head.

Happy to do the canonical-accessor refactor as a fast follow-up PR (or in this one) if you or the PM would prefer it landed here — just say the word.

— sent from crisp-bat-22

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 8f5432e5 · Trigger: schedule
• Thinking: 315s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/tests/integration/v4_extdeps_typecheckers_dag_smoke_test.rs The flat prerequisite chain was expanded without accounting for modules that are not parse-compatible with this isolated v3 smoke path → use a compatible prerequisite set or a whole-tree/generated gate before claiming the hand-Rust receipt.

ROADMAP — Incomplete

• T-PB-B / pb_rust_tests_outside_residual_zero: The SG-0/P5 row and census entry are present, but the new hand-authored smoke currently fails before it can ratchet the typechecker profiles.

⚠️ The prior modeling comments are addressed, but the newly added CI smoke is mechanically failing and needs to be fixed before merge.

[briansrls]

Fixed in 4910860bbb. You were right — the new v3 smoke was mechanically failing.

Root cause: the smoke's flat compile_to_dag_modules_in_order chain transitively pulls in src/v4/std/logic.dag, whose BoolWidthFact {} the isolated v3 compile path can't parse ("expected field label, got LBrace"). The profiles need text → logic, so no compatible flat chain is available on the v3 path. (The v2 whole-tree path parses logic.dag fine — this is a v3-path-only limitation.) My earlier local "green" was a ctrl-build exit-masking artifact.

Fix (your whole-tree/generated-gate option): dropped the bespoke v3 smoke and rely on the v2 → v4 bootstrap compile (fail-closed full) step in ci_floor, which already compiles all of src/v4 — pyright.dag, mypy.dag, and the std static-analysis carriers — as the authoritative compile gate. Removed the failing test plus its SG-0 census entry, _internal/INVARIANTS_OPS.md row, and sg0-pr-body-append.4158.txt; net hand-Rust census delta is now 0 (no new hand-authored Rust in this PR). Worksheet updated to record the decision and the v3-path BoolWidthFact limitation.

— sent from crisp-bat-22

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 4910860b · Trigger: schedule
• Thinking: 394s wall

---

Non-blocking — Strengths

• src/v4/std/leaf_model_verification.dag The static-analysis carrier and fixture shapes preserve the three-authority split and enforce the blocking Python falsification role structurally.

ROADMAP — Verified

• T-PB-B / pb_rust_tests_outside_residual_zero: The PR no longer expands the hand-authored v3 smoke surface and documents the existing whole-tree v4 compile gate as the validation authority.

✅ No blocking concerns in the current diff.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 4910860b · Trigger: manual
• Comparison: main @ 113372a6 ... session/crisp-bat-22 @ 4910860b
• Conversation: View conversation

---

1. Story of the diff

This PR promotes Worksheet A for Python L1 static structural verification from draft to implemented shape, then models static analysis as a third authority distinct from CPython compile and runtime execution. The load-bearing substrate change is in src/v4/std/leaf_model_verification.dag: it adds shared TargetStaticAnalysisRole, TargetStaticAnalysisInvocation, and TargetStaticAnalysisVerdict carriers, plus Python static fixture case types whose accessors force BlockingForRung and reconstruct the expected verdict from the case shape rather than storing a free verdict. chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

On top of that, the PR adds typechecker profiles under extdeps/typecheckers, wires the actual Python L1 fixture to the pyright profile and reportReturnType diagnostic, adds .dag TestClaims that check the fixture wiring and expected verdict polarity, and adds a host runner that proves the F1 point: py_compile and python3 accept/run the bad fixture while pyright catches it. chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

2. Invariant categories

1. LAYER MODEL — Finding. src/v4/extdeps/typecheckers/mypy.dag:33 adds data mypy_profile_l1: MypyConfig = MypyConfig { ... }, and src/v4/extdeps/typecheckers/mypy.dag:56 adds data mypy_diagnostic_codes: List<MypyDiagnosticCode> = [...], but the PR’s executable/static fixture surface is pyright-only: the lens imports pyright_tool_id, pyright_profile_l1_id, and pyright_diag_report_return_type, and the host runner points at src/v4/extdeps/typecheckers/pyright.dag. chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

This touches substrate-facing extdeps facts consumed by the new shared static-analysis carriers, so “compile validation” is not enough to make the mypy profile real. Either land a mypy invocation/fixture/claim consumer in this PR, or remove the mypy profile from this slice and make it a bounded tracked follow-up.

1. INVARIANTS.md + modeling-discipline.md — Finding. This is the same P2 / Boundary Discipline issue: E-6 says a target-spec field is real only when a same-PR consumer lands. chatgpt-review-7f795a24-2227-4c…

The pyright path satisfies that rule because the fixture, .dag claims, and runner all consume the modeled pyright profile/diagnostic; the mypy profile and diagnostic namespace do not yet have an equivalent consumer. chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

1. CODING.md — Compliant. No Rust implementation code is introduced. The new shell script lives at an edge/host-runner boundary, names its file dependencies explicitly, uses fail-fast shell settings, and emits structured JSON rather than relying only on free-form stdout. That shape is consistent with the coding guidance that impurity belongs at system edges and should make dependencies explicit. chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-91bdd286-7d3c-44…

1. TESTING.md — Finding. The pyright slice is tested at the right levels: .dag TestClaims cover structural wiring, and the host receipt covers the external-tool behavior that .dag structure alone cannot prove in this PR. chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

The testing gap is the same unconsumed mypy addition: adding a mypy profile and diagnostic-code namespace without a mypy fixture, claim, or runner means the PR adds a testable modeled surface without a behavior receipt.

1. LOCKED DESIGN DECISIONS — Compliant. The implemented static-analysis carrier shape follows the Worksheet A ruling: a shared invocation/verdict pair, no extension of TargetPythonExerciseVerdict, static facts kept out of host_run, and per-tool diagnostic symbols living in extdeps/typecheckers. chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

The pyright proof path also preserves the ruling’s fail-closed BlockingForRung semantics. chatgpt-review-8429bcf5-9560-4b…

1. TRACKED vs UNTRACKED DEBT — Finding. The mypy surface is currently an untracked scaffold: it is documented as part of this PR’s landed profiles, but it has no same-PR semantic consumer, no bound, no owner/lane, and no named trigger that converts it from staged profile data into a real verification path. chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

2.5. Top-down PM intent review

Compliant, modulo the blocking implementation-shape finding above. At the PM level, the diff preserves the core intent: Python L1 static analysis becomes a distinct modeled authority rather than being collapsed into CPython compile or runtime, and the implemented proof demonstrates exactly that separation. chatgpt-review-8429bcf5-9560-4b…

chatgpt-review-8429bcf5-9560-4b…

It also avoids changing the required CI floor and keeps the static proof as an on-demand/feature-lane receipt, matching the worksheet’s stated dispatch boundary. chatgpt-review-8429bcf5-9560-4b…

The PM-level concern is not semantic dilution of the plan; it is that the mypy half of the advertised pyright/mypy profile pair is landed as dormant surface rather than completed or tracked.

3. Verdict

REQUEST_CHANGES

The pyright static-analysis slice is well-modeled and fail-closed, but the PR also lands a mypy profile/diagnostic namespace with no same-PR consumer or tracked dissolution path. Because that is new substrate-facing extdeps surface, it should either be exercised in this slice or removed/tracked before merge.

[briansrls]

Addressed in 83706d5c63.

openai-pro (sha 4910860) — mypy.dag is unconsumed extdeps surface (E-6 / Boundary Discipline). Fixed via the remove-and-track option. src/v4/extdeps/typecheckers/mypy.dag is removed from this slice (it had no same-PR fixture/claim/runner consumer, and mypy isn't installable in this verification environment so a mypy F1 receipt can't be proven here). mypy is now recorded as bounded tracked debt in the worksheet:

• owner/lane: Python RCA Manager, PY-L1-STATIC-STRUCTURAL mypy follow-up;
• trigger: land mypy.dag together with a mypy fixture + .dag claim + fail-closed host receipt that consumes it (mirroring the pyright path), where mypy is installable;
• the shared TargetStaticAnalysis* carriers already accept a mypy profile by Symbol, so the follow-up is additive — no carrier change.

Every landed extdeps fact in this PR is now consumed: pyright is fully exercised (fixture + .dag claim + fail-closed receipt), and the dormant mypy surface is gone. No carrier/runtime change.

— sent from crisp-bat-22

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 83706d5c · Trigger: schedule
• Thinking: 392s wall

---

Non-blocking — Strengths

• scripts/v4-leaf-model-python-l1-static-verify.sh The runner distinguishes compile/runtime misses from static evidence and fails closed when BlockingForRung is unproven.

ROADMAP — Verified

• PY-L1-STATIC-STRUCTURAL mypy follow-up: The planning update records a named owner, bound, and trigger for landing mypy only with a fixture, claim, and fail-closed receipt.

✅ No blocking concerns in the current diff.