Skip to content

Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via SG-RC plus SG-2 residual constraints - #4153

Merged
briansrls merged 40 commits into
mainfrom
session/neat-bee-336
Jun 1, 2026
Merged

briansrls merged 40 commits into
mainfrom
session/neat-bee-336

Conversation

@briansrls

@briansrls briansrls commented Jun 1, 2026 •

Copy link
Copy Markdown
Contributor

Auto-opened by session-dashboard for session neat-bee-336.
Pushing to session/neat-bee-336 advances this PR.

Summary

Implements SG-RC ownership lookup for Outcome<T> so Rust target ownership rows can match the generic Outcome carrier while SG-2 keeps the projected inner type arguments intact. The lookup key projection is row-authored via TargetUseSiteOwnershipSourceProjection, with Rust Outcome rows declaring UseSiteOwnershipInstantiationHeadCarrier and other rows remaining exact-keyed.

Adds a manual .dag claim proving Outcome<Node> at a function return serializes as Rc<Outcome<Node>>, plus narrow Rust smoke assertions that the modeled SG-RC/SG-2 receipt remains present.

P5 / SG-0 receipt

  • Added Rust under src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs is assertion-only smoke coverage over existing .dag model text and does not introduce a new implementation path, emitter behavior, or scaffold API.
  • Behavioral authority is the new manual .dag claim claim_sg_rc_outcome_inner_sg2_args_preserved in src/v4/test/claim/manual/sg_rc_layering.dag.
  • SG-0 census posture: +0 implementation surface. The v3 test delta only pins the presence of the .dag claim/helper strings until the existing v4 manual-claim runner evaluates this fixture directly.
  • Deferral lane: v4 TestClaim/manual-claim execution migration; dissolve trigger is direct evaluation of src/v4/test/claim/manual/sg_rc_layering.dag by the v4 claim runner, at which point the string-presence smoke can be removed.

Test plan

  • ctrl-build -- /opt/cargo/bin/cargo test -p v3-compiler --test integration v4_std_target_realization_declares_use_site_ownership_carrier -- --nocapture passed.
  • ctrl-build -- /opt/cargo/bin/cargo test -p v3-compiler --test integration v4_sg_rc_outcome_claim_preserves_sg2_inner_type_args -- --nocapture passed.
  • git diff --check && /opt/cargo/bin/cargo fmt --all --check passed.
  • Local scripts/v4-m1-rust-emit-probe.sh reaches cargo-check residuals in the known broad v4 emitted Rust floor; GitHub ci_floor remains the authoritative gate for this PR.

@briansrls
briansrls marked this pull request as ready for review June 1, 2026 02:54
@briansrls

Copy link
Copy Markdown
Contributor Author

Review metadata

  • Provider / model: openai-pro / gpt-5-5-pro
  • Commit: 6f6ae574 · Trigger: manual
  • Comparison: main @ aa1ad143 ... session/neat-bee-336 @ 6f6ae574
  • Conversation: View conversation

1. Story of the diff

This PR fixes an SG-RC/SG-2 composition failure for generic carriers such as Outcome<T>. The production change is in src/v4/std/target_model.dag: ownership lookup now derives a canonical lookup key from the source carrier, peeling an Instantiation down to its head before comparing against catalog rows, so an Outcome<Node> source can find the generic Outcome ownership row while still preserving the SG-2-projected inner type for emission at src/v4/std/target_model.dag:2413 and src/v4/std/target_model.dag:2431-2432. chatgpt-review-ae29482e-bd92-40…

The test/claim side builds a manual Outcome<Node> type node, projects it through project_type_expression_node, then applies return-site ownership and asserts the serialized result is Rc<Outcome<Node>>, not the previously-risky bare/generic Rc<Outcome> shape. That behavioral claim is declared as claim_sg_rc_outcome_inner_sg2_args_preserved at src/v4/test/claim/manual/sg_rc_layering.dag:430-436, with a Rust smoke check ensuring the fixture and claim stay present at src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs:545-563. chatgpt-review-ae29482e-bd92-40…

2. Invariant categories

  1. LAYER MODEL (substrate vs implementation).

Compliant — this touches std/ target modeling, but it does not add a Dag substrate type, a new connective, or a new variant; the new behavior is a typed target-model query surface, target_use_site_ownership_source_key, consumed immediately by the ownership lookup at src/v4/std/target_model.dag:2413 and src/v4/std/target_model.dag:2431-2432.

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

Compliant — Boundary Discipline / single authority is preserved: SG-2 remains responsible for the projected emitted type, while SG-RC lookup reads a canonical carrier key from the same source carrier instead of creating a second carrier representation. The Absent => source_carrier branch at src/v4/std/target_model.dag:2418 also does not fabricate a plausible generic head; malformed or headless instantiations do not accidentally match the generic row. The helper is not a predicate-dissolution case: it is not a Bool helper over a coproduct, and it is the canonical lookup surface used by the lookup itself rather than a consumer-local re-derivation.

  1. CODING.md.

Compliant — the production change is a small free function with explicit inputs and no hidden state, and the call site names the intermediate source_key before hashing at src/v4/std/target_model.dag:2431-2432. The new .dag claim helpers are similarly narrow: source type construction, projection, ownership application, and boolean claim are separated at src/v4/test/claim/manual/sg_rc_layering.dag:141-186.

  1. TESTING.md.

Compliant — the PR adds a behavior-level .dag TestClaim for the bug class, asserting the externally meaningful contract “Outcome return wraps SG-2-projected inner type as Rc<Outcome<T>>” at src/v4/test/claim/manual/sg_rc_layering.dag:430-436. The Rust-side additions are smoke/receipt checks over the manual claim file at src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs:545-563; I would not treat them as the main behavioral test, but they are acceptable as a guard that the .dag claim remains wired.

  1. LOCKED DESIGN DECISIONS.

Compliant — the diff uses Instantiation exactly as a type-parameterization connective, consistent with the thesis substrate shape; it does not add a seventh connective, alter the behavior substrate, or change a locked bootstrap/testing direction. chatgpt-review-d0235d16-5957-4e…

  1. TRACKED vs UNTRACKED DEBT.

N/A — I did not see new TODOs, scaffolds, yellow gates, temporary ledgers, or bridge APIs in the changed lines. The new helper is immediately consumed by the lookup and the new claim is a direct regression receipt, not deferred scaffolding.

2.5. Top-down PM intent review

Compliant — the PR preserves the PM-level intent that target realization be derived from modeled structure rather than special-casing emitted strings. It keeps Outcome<Node> as one type tree, projects it through the existing type-expression projection path at src/v4/test/claim/manual/sg_rc_layering.dag:160-168, and applies SG-RC ownership after projection at src/v4/test/claim/manual/sg_rc_layering.dag:171-180. That matches the thesis direction that types are Node trees with Instantiation for parameterization and that target emission derives from shared structure, not ad hoc emitter exceptions. chatgpt-review-d0235d16-5957-4e…

3. Verdict

APPROVE. The production change is narrow and located at the target-model ownership boundary, and the new claim exercises the important semantic contract: SG-RC selects the generic ownership policy while SG-2 keeps the Outcome<Node> inner argument intact. I found no blocking invariant, testing, locked-design, or debt issue in the changed lines.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: 033d15fd · Trigger: schedule
  • Thinking: 308s wall

Non-blocking — Strengths

  • src/v4/test/claim/manual/sg_rc_layering.dag The added claim projects Outcome through SG-2 before SG-RC wrapping and pins the emitted Rc<Outcome> shape.

✅ No blocking concerns found in the changed model or same-path smoke coverage.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: 57516610 · Trigger: schedule
  • Thinking: 303s wall

BLOCKING (1)

Root Cause

  • src/v4/std/target_model.dag TargetUseSiteOwnershipRealization.source_carrier: Node conflates exact carrier identity with generic-family/head keys → introduce a typed ownership lookup key/projection carried by rows and apply it uniformly rather than hard-coding Outcome.

⚠️ One blocking substrate modeling issue: make generic carrier matching row-driven before this pattern propagates.

Comment thread src/v4/std/target_model.dag Outdated
use_site: TargetOwnershipUseSite
) -> TargetUseSiteOwnershipLookup {
if content_hash(n: row.source_carrier) == content_hash(n: source_carrier)
let source_key = target_use_site_ownership_source_key(source_carrier: source_carrier)

This comment was marked as resolved.

@briansrls

briansrls commented Jun 1, 2026 •

Copy link
Copy Markdown
Contributor Author

Addressed the codex P5 receipt finding from review 23728 by updating the PR body with a dedicated "P5 / SG-0 receipt" section. It records that the v3 Rust delta is assertion-only smoke over the modeled .dag claim, names claim_sg_rc_outcome_inner_sg2_args_preserved as behavioral authority, states SG-0 +0 implementation-surface posture, and gives the dissolve trigger for replacing the string-presence smoke with direct v4 manual-claim execution. — sent from neat-bee-336

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: d4323178 · Trigger: schedule
  • Thinking: 357s wall

BLOCKING (1)

Root Cause

  • src/v3/compiler/tests/integration/v4_std_target_realization_dag_smoke_test.rs SG-0 same-file host-test expansions are landing without an updated per-PR receipt surface → add the required PR-body receipt or changed planning row naming the concrete T-PB-B deferral/receipt.

⚠️ One P5 receipt gap remains; the substrate fix for the prior Outcome-specific lookup concern looks structurally clean.

);
}

#[test]

This comment was marked as resolved.

@briansrls

Copy link
Copy Markdown
Contributor Author

Verified against current PR head 3819c61f935df48f33cf69c68678d8a3be2c2329: this finding was from older commit d4323178. The current PR body has a dedicated P5 / SG-0 receipt section for the same-file v3 smoke expansion. It records that the Rust delta is assertion-only over modeled .dag text, names claim_sg_rc_outcome_inner_sg2_args_preserved as behavioral authority, states SG-0 +0 implementation-surface posture, and gives the v4 TestClaim/manual-claim execution migration dissolve trigger. No code change is needed for this stale receipt finding on current head. — sent from neat-bee-336

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: 3819c61f · Trigger: schedule
  • Thinking: 322s wall

⚠️ No new blocking findings; the previously flagged P5 receipt gap for the expanded src/v3 Rust smoke remains unresolved.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: d6248901 · Trigger: schedule
  • Thinking: 345s wall

Non-blocking — Strengths

  • src/v4/std/target_model.dag The new source-projection coproduct is classified on the substrate carrier and has a same-PR consumer in the SG-RC lookup path.

✅ No new blocking concerns found.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: fb4189af · Trigger: schedule
  • Thinking: 301s wall

✅ Mixed code/.dag/docs PR; the Outcome SG-RC source-projection route is row-authored, consumed, and covered by the manual-claim smoke with no new blocking concerns.

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: 7f49446d · Trigger: schedule
  • Thinking: 526s wall

Non-blocking — Strengths

  • src/v4/std/target_model.dag Mixed code/.dag/docs review found the SG-RC Outcome route row-authored, SG-2 argument-preserving, and aligned with the thesis single-authority/facts-forward discipline.

✅ No blocking concerns in the PR diff.

@briansrls
briansrls force-pushed the session/neat-bee-336 branch from 35415e2 to 0ec1ed4 Compare June 1, 2026 12:25
briansrls and others added 18 commits June 1, 2026 12:25
briansrls and others added 22 commits June 1, 2026 12:26
@briansrls
briansrls force-pushed the session/neat-bee-336 branch from 0ec1ed4 to 5251f39 Compare June 1, 2026 12:26
@briansrls
briansrls merged commit 9863d82 into main Jun 1, 2026
@briansrls
briansrls deleted the session/neat-bee-336 branch June 1, 2026 12:26

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Review metadata

  • Provider / model: codex / unknown
  • Commit: 35415e2d · Trigger: schedule
  • Thinking: 251s wall

BLOCKING (1)

Root Cause

  • src/v2/05_emit_rust.dag shared Rc ownership is applied in both render_rust_applied_type and render_rust_applied_type_shared → leave exactly one helper as the wrapping authority and make the other return the already-authored applied spelling.

⚠️ One ownership-rendering path can double-apply Rc, so this needs a small fix before merge.

Comment thread src/v2/05_emit_rust.dag
if n.children |> count == 0 {
let applied = if n.children |> count == 0 {
base
} else {

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

BLOCKING: render_rust_applied_type now wraps shared applied types, but render_rust_applied_type_shared already wraps its result, so Outcome paths through render_rust_type_with_applied_binding can emit Rc<Rc<Outcome>> instead of the SG-RC single ownership layer, violating P2 single authority.

briansrls added a commit that referenced this pull request Jun 1, 2026
…shells (#4162)

* docs: add v4 modeling DFS ratification log

Adds the §8 ratification audit trail and reconciles planning cross-references for Modeling DFS worksheet approvals.

* Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via SG-RC plus SG-2 residual constraints (#4153)

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* fix SG-RC Outcome claim projection argument

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via SG-RC

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via SG-RC

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* Remove temporary stage0 emitter debug

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* Remove stage0 emitter diagnostic

* Document Outcome smoke P5 receipt

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* WIP: Outcome ownership implementation — Outcome/Rc<Outcome> E0308 route via S

* Wave 3 Phase 1: CiSelectionReceipt extension + fixture shadow receipt (live CI deferred) (#4174)

* fix: rebase #4174 on main — receipt extension only (consume #4178)

Rebase onto origin/main after #4178 merged wave3_shadow_roster.dag and the
runtime selection API. Drop duplicate #4178-owned symbols from this PR;
reference main for roster + ci_wave3_shadow_testclaims_selected*.

Keeps CiSelectionReceipt extension (mode/provenance/claim rows/fixture
receipt), v4_workflow_ci_wave3_* smoke, and planning docs.

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

* WIP: Wave 3: affected-set + testgen shadow integration (coordinate neat-hawk-

* fix: restore M1 ledger honesty + smoke parity after rebase (#4174)

- Revert ci-required-surface-cut gate-3 row to match modeled authority
  (V4_M1_RUST_EMIT_PROBE_STRICT=0 in ci.dag/ci.yml; preconditions fail-closed).
- Restore testclaim_corpus_eval binding assertion to CiLiveWorkflowStepSignal.
- Restore M1 smoke: nested M1CiLiveWorkflowSignal.step access, strict_env_binding
  helper, VariantRecord-aware record_body_field, policy parity checks.

Addresses codex REQUEST_CHANGES on ef0f438.

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

---------

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

* Python L1 pyright/mypy static structural checks implementation (#4158)

* WIP: Python L1 pyright/mypy static structural checks implementation

* WIP: Python L1 pyright/mypy static structural checks implementation

* WIP: Python L1 pyright/mypy static structural checks implementation

* fix: address python static CI failures

* fix: clean up python static smoke test

* WIP: Python L1 pyright/mypy static structural checks implementation

* fix(v4): address review #23594/#23595 on PY-L1 static slice

- mypy.dag: import Bool from v4.std.logic (unresolved symbol broke the
  compile_to_dag smoke contract for the mypy profile).
- v4-leaf-model-python-l1-static-verify.sh: pyright EXITS NON-ZERO when it
  correctly reports reportReturnType, so pyright_run no longer conflates that
  expected-rejection exit with tool-unavailability — availability is judged
  purely by whether parseable --outputjson was produced; an empty/invalid file
  (offline npx fetch) is the only tool-unavailable path (fail-closed MISS).
- Add 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 + #4158).
- Worksheet: F1 host receipt is on-demand (no CI step) — the no-new-shell ratchet
  (§11.7.1 required surface cut) allows only 3 transports on the required floor;
  the v4 substrate is validated on the required path by the v2→v4 bootstrap
  compile in ci_floor.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* WIP: Python L1 pyright/mypy static structural checks implementation

* fix(v4): de-conflate profile/tool identity + make BlockingForRung structural

Addresses codex scheduled review (sha 871b898) — 2 BLOCKING:

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 (Facts-Flow-Forward / single-authority). Add 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.

2. LeafModelPythonStatic{Happy,Falsification}Case stored a free TargetStaticAnalysisInvocation,
   so a blocking fixture could be built with analysis_role: Advisory. Cases now carry only
   artifact + tool_profile_ref (+ tool_id/diagnostic_code for falsification); the invocation
   is CONSTRUCTED with analysis_role: BlockingForRung by accessor fns
   (leaf_model_python_static_{happy,falsification}_invocation). The blocking role and the
   profile/tool distinction are guaranteed by construction, not accepted as free fields.

Lens + claim updated to the new case shape; claim now also asserts tool_profile_ref ==
pyright_profile_l1_id flows. Verify script unchanged (fixture sources identical) — re-ran
PROVEN. NOTE: .dag changes not locally compile-validated (host load ~50, fork EAGAIN);
relying on CI ci_floor bootstrap compile.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* docs(v4): clarify static tool identity comments

* fix(v4): F1 runner consumes the modeled pyright profile (single authority)

Addresses codex REQUEST_CHANGES #23685: the runner used any pyright on PATH
without pinning the modeled version/config, so the F1 receipt could pass under a
different tool profile than pyright_profile_l1_id references.

Now the runner reads pyright_profile_l1 facts from pyright.dag (single authority):
- pyright_version → pins exactly that version (PATH pyright used only if its
  --version matches; otherwise npx pins it; else fail-closed unavailable),
- python_version + type_checking_mode → written to a generated pyrightconfig.json
  that pyright auto-discovers for the fixtures.
The receipt records the consumed version/python_version/mode. Re-ran: PROVEN
(pyright 1.1.410, python 3.11, standard; falsification reportReturnType).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* WIP: Python L1 pyright/mypy static structural checks implementation

* fix(v4): address openai-pro REQUEST_CHANGES (single-authority + no-prose)

1. P2 single-authority: the F1 host receipt no longer hardcodes the pyright rule
   string. It reads the fixture's modeled expected diagnostic_code from the lens and
   resolves the rule_name from the pyright_diagnostic_rules row in pyright.dag, so the
   receipt can't drift from the modeled diagnostic namespace. Re-ran: PROVEN.
2. CODING.md no-prose / Practice 9: reduced the verbose "tried X, rejected Y"
   dissolution analysis embedded in TargetStaticAnalysisRole / TargetStaticAnalysisVerdict
   (leaf_model_verification.dag) and PyrightTypeCheckingMode (pyright.dag) to one-line
   🟢-terminal carrier tags; the full dissolution analysis is recorded in PR #4158 review.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* WIP: Python L1 pyright/mypy static structural checks implementation

* fix(v4): model pyright typeCheckingMode keyword spelling (single authority)

Addresses codex REQUEST_CHANGES #23765: the host receipt's mode_map re-authored
the PyrightTypeCheckingMode → config-keyword mapping (off/basic/standard/strict),
a second authority for a modeled profile fact (P2 / Practices 3,5).

pyright.dag now carries the modeled projection pyright_type_checking_mode_spellings
(variant_name → keyword). The runner resolves the typeCheckingMode keyword from that
row keyed by the profile's variant — no parallel mode map. Combined with the earlier
version/python-version/rule-string sourcing, the script now owns ZERO pyright
semantics; every pyright fact flows from pyright.dag. Re-ran: PROVEN.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* fix(v4): key pyright mode-spelling projection by the enum variant (M4/P2)

Addresses codex REQUEST_CHANGES (sha f0ab617): PyrightTypeCheckingModeSpelling
modeled the enum member as a string proxy (variant_name: String), splitting the
closed PyrightTypeCheckingMode enum from its config spelling into two authorities.

The row is now keyed by a PyrightTypeCheckingMode value
(`PyrightTypeCheckingModeSpelling { mode: PyrightTypeCheckingMode, keyword: String }`,
rows use PyrightModeOff/Basic/Standard/Strict), so the enum and its spelling are one
authority. The host runner consumes that typed row (matches `mode: <variant>`) keyed by
the profile's modeled variant. Re-ran: PROVEN.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* fix(v4): bind pyright to the generated profile config (--project)

Addresses openai-pro REQUEST_CHANGES (sha fad72bd): the F1 runner wrote the
modeled profile into ${scratch}/pyrightconfig.json but invoked pyright from the
repo root without --project, so pyright's config discovery was not structurally
bound to the generated config — the same-profile proof was not mechanically
guaranteed (P2 single authority / facts-flow-forward).

Both pyright command paths now pass `--project "$scratch"`, binding pyright to the
pyrightconfig.json carrying the modeled pythonVersion + typeCheckingMode. The run
provably consumes pyright_profile_l1 rather than ambient/default config. Re-ran:
PROVEN (happy clean, falsification reportReturnType).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* WIP: Python L1 pyright/mypy static structural checks implementation

* fix(v4): drop broken v3 smoke; validate profiles via whole-tree v2 gate

Addresses codex REQUEST_CHANGES (sha 8f5432e): the bespoke v3 hand-Rust smoke
`v4_extdeps_typecheckers_dag_smoke_test.rs` was mechanically failing. Its flat
`compile_to_dag_modules_in_order` chain transitively pulls in src/v4/std/logic.dag,
which the isolated v3 compile path cannot parse (`BoolWidthFact {}` → "expected field
label, got LBrace"). The profiles need text → logic, so a compatible flat chain isn't
available on the v3 path.

Per codex's whole-tree/generated-gate alternative: drop the v3 smoke and rely on the
`v2 → v4 bootstrap compile (fail-closed full)` step in ci_floor, which compiles all of
src/v4 (pyright.dag + mypy.dag + the std static-analysis carriers) — the v2 path parses
logic.dag fine. Removes the failing test plus its SG-0 census entry, INVARIANTS_OPS row,
and sg0-pr-body-append.4158.txt (net hand-Rust census delta is now 0). Worksheet updated.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* fix(v4): remove unconsumed mypy profile (E-6); track as bounded follow-up

Addresses openai-pro REQUEST_CHANGES (sha 4910860): mypy.dag added a
mypy_profile_l1 + diagnostic namespace with NO same-PR consumer — the fixture,
.dag claim, and host runner are pyright-only. Per INVARIANTS E-6 / Boundary
Discipline a new target-spec extdeps fact is real only when a same-PR consumer
lands; an unconsumed mypy profile is dormant scaffold.

Per the offered remove-or-track option (and since mypy is not installable in the
current env, so a mypy F1 receipt can't be proven here): remove
src/v4/extdeps/typecheckers/mypy.dag from this slice and record mypy as bounded
tracked debt in the worksheet (owner = Python RCA Manager; trigger = land mypy.dag
together with a mypy fixture/claim/fail-closed receipt). The shared
TargetStaticAnalysis* carriers already accept a mypy profile by Symbol, so the
follow-up is additive — no carrier change. pyright remains fully consumed.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* fix(merge): resolve conflict markers left in the main merge commit

The auto-committed merge ab3c1fc landed with conflict markers still present in
src/v4/std/leaf_model_verification.dag, src/v4/lens/leaf_model_verification.dag, and
the worksheet. This commit applies the resolved content: keep BOTH the Python
PY-L1 static-analysis carriers/fixtures (this PR) and main's TypeScript
leaf-model carriers/fixtures (additive, distinct types); merge the import lists and
claim-id lists; take main's worksheet status line updated to note Worksheet A is
implemented in #4158.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* TS L0 impl (1/5): algebra inhabitance widening — ts_*_facts_* data lines per v4-ts-algebra-inhabitance-widening-worksheet-2026-06-01.md §10.0 (#4155)

* WIP: TS L0 impl (1/5): algebra inhabitance widening — ts_*_facts_* data lines

* WIP: TS L0 impl (1/5): algebra inhabitance widening — ts_*_facts_* data lines

* Merge origin/main into session/fierce-deer-550

Resolve typescript.dag conflict: main landed the number/bigint
algebra-inhabitance fact rows (+ SG-1 atom-realization block) via a
sibling PR. Dedupe — keep main's number/bigint rows once and the
atom-realization block; this PR's net-new content is the boolean row
(ts_bool_algebra_inhabitance_ts_facts_boolean, with E-6 staging marker)
and the string row (ts_string_algebra_inhabitance_ts_facts_string,
clean-merged).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* chore: delete internal-only content for public repo visibility flip (#4192)

* WIP: Release Jun1 one-shot public-repo cleanup (operator decision 2026-06-01:

* WIP: Release Jun1 one-shot public-repo cleanup (operator decision 2026-06-01:

* Add TypeScript TargetAtomRealization rows (#4189)

* WIP: TS L0 impl (3/5): TargetAtomRealization rows (Symbol/boolean/string) per

* Add TypeScript target atom realization rows

* Dissolve duplicate TypeScript symbol atom row

* Use structural String carrier for TypeScript atom row

* WIP: TS L0 impl (3/5): TargetAtomRealization rows (Symbol/boolean/string) per

* Fail closed for string value templates

* Use projections for string value templates

* Add FreeMonoid node projection receipt

* Declare SourceAtomValue as coproduct

* Document SourceAtomString raw node bridge

* TS L0 impl (5/5): grammar-inverse TestClaims G1+G2 — mvp1 add-fn + wave2a type_alias per v4-ts-grammar-inverse-testclaims-worksheet (#4156)

* WIP: TS L0 impl (5/5): grammar-inverse TestClaims G1+G2 — mvp1 add-fn + wave2

* WIP: TS L0 impl (5/5): grammar-inverse TestClaims G1+G2 — mvp1 add-fn + wave2

* WIP: TS L0 impl (5/5): grammar-inverse TestClaims G1+G2 — mvp1 add-fn + wave2

* docs: add P5 receipt for TS grammar inverse ratchet

* WIP: TS L0 impl (5/5): grammar-inverse TestClaims G1+G2 — mvp1 add-fn + wave2

* test: assert TS grammar inverse anchor bindings

* style: rustfmt TS grammar inverse test

---------

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

* T-38: restore corpus receipt smoke coverage (#4191)

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* fix(t38): require generated corpus tally conjunction

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* fix(t38): match modeled manual corpus gate

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* Tighten generated corpus eval receipt probes

* Merge origin/main into T-38 receipt follow-up

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* Test inverted corpus tally receipt rejection

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* Tighten T-38 receipt smoke needle

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* Anchor T-38 tally receipt to body tail

* WIP: Runtime/TestClaim Manager — authority over T-22 eval execution, T-38 str

* Pin T-38 inverted tally receipt subject

* Fix shared applied type Rc authority (#4190)

* ci_floor: de-churn cargo cache key (stop-the-bleeding) + model note for the right-way sccache projection (#4197)

* WIP: CI floor

* ci.dag: cite durable in-repo cache authority (worksheets deleted in #4192 public flip)

* ci_floor: route M1 emit-probe through host compute governor (memory-denominated dynamic jobs + jobserver + sccache) (#4210)

* WIP: CI floor

* WIP: CI floor

* WIP: CI floor

* chore: close Jun1 public cleanup gaps (#4200)

* WIP: Release Jun1 public-repo cleanup gap-fix (follow-on to merged PR #4192):

* chore: remove stale public cleanup test anchors

* WIP: Release Jun1 public-repo cleanup gap-fix (follow-on to merged PR #4192):

* docs: remove stale CI carrier regeneration wording

* docs: drop orphaned workflow brief receipt claim

* WIP: Release Jun1 public-repo cleanup gap-fix (follow-on to merged PR #4192):

* docs: align cleanup receipts with static CI carrier

* WIP: Release Jun1 public-repo cleanup gap-fix (follow-on to merged PR #4192):

* WIP: Release Jun1 public-repo cleanup gap-fix (follow-on to merged PR #4192):

* docs: clarify P5 dissolution receipts

* WIP: Release Jun1 public-repo cleanup gap-fix (follow-on to merged PR #4192):

* ci: refresh pinned workflow carrier

* ci_floor: M1 emit-probe fail-closed on host governor (remove static --jobs fallback) (#4212)

* WIP: CI floor

* WIP: CI floor

* WIP: CI floor

* WIP: CI floor

* ci_floor: M1 emit-probe fail-closed (no static fallback) + sync regen artifact SHA/env

* ci_floor: M1 emit-probe couples to host jobserver (MAKEFLAGS on GHA / ctrl-build in session), fail-closed on neither

ctrl-build is not installed on GHA runners — #4210's ctrl-build routing was a silent no-op
(always hit the --jobs 4 fallback). GHA couples to the jobserver via the actions-runner@.service
MAKEFLAGS instead, so raw cargo joins the pool directly (jobserver bounds rustc processes
host-wide: fill when idle, pare under load). Probe now runs jobserver-coupled with no fallback,
capped per-invocation at the ceiling; echoes MAKEFLAGS for verification.

* ci_floor: reframe M1 parallelism comments as jobserver-coupled (not ctrl-build-centric); sync ci.yml Source-SHA256

Addresses cursor review nit on #4212: ci.yml + smoke-test comments framed governance as
ctrl-build, but GHA is MAKEFLAGS-coupled without ctrl-build. Comments now match the authoritative
ci.dag/probe logic. ci.yml comment change → recomputed Source-SHA256 pin in the regen artifact.

* Go leaf-model: R1/R2a/R2b/R3-external claims, lens fixtures, verify scripts

Admin-merge onto main post-#4164/#4168 (orphan #4162 path-b).
Leaf-only diff: scripts, go_r*.dag, lens/std leaf_model_verification carriers.

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

---------

Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant