Repository navigation
Wave 3 Phase 1: CiSelectionReceipt extension + fixture shadow receipt (live CI deferred) - #4174
Conversation
briansrls
changed the title
… API Rebase lane split per smart-newt-797: drop duplicate wave3_shadow_roster.dag and all #4178-owned symbols from ci.dag (selection wrappers, fail-closed witnesses). #4174 now only adds CiSelectionReceipt extension carriers, claim projection rows, fixture receipt, smoke tests, and planning docs. Consumes #4178: ci_wave3_shadow_*_claim_roster, ci_wave3_shadow_testclaims_selected, ci_wave3_shadow_fail_closed_affected. Fixture uses single affected authority. Co-authored-by: Cursor <cursoragent@cursor.com>
|
Codex P5 finding (REQUEST_CHANGES) — addressed @ Valid: the Added
Cross-links: module header + inline comment above the five Local: — sent from loyal-carp-103 |
|
Codex Valid: landed carrier was missing Extended — sent from loyal-carp-103 |
|
composer REQUEST_CHANGES (provenance) — fixed @ Valid: Fix: CI: prior failure was — sent from loyal-carp-103 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
b9de4d95· Trigger:schedule - Thinking:
290s wall
BLOCKING (2)
Root Cause
src/v4/workflow/ci.dagWave 3 receipt carriers added closed enums without in-file dissolution dispositions → add valid 🟢/🟡/🔴 tags with gate/trigger, or dissolve the enums now.src/v4/workflow/ci.dagci_test_claim_shadow_projection_node drops TestClaim to input-only before hashing → hash the canonical whole TestClaim node or carry a typed deferred hash until that projection exists.
| ] | ||
|
|
||
| // Wave 3 §11.7.4 — extend existing receipt (arbiter §8 2026-06-01); no parallel shadow receipt type. | ||
| type CiSelectionMode |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| anchor: test_claim_anchor(c: claim), | ||
| label: test_claim_label(c: claim), | ||
| coproduct_variant: test_claim_coproduct_variant(c: claim), | ||
| claim_projection_hash: content_hash(n: ci_test_claim_shadow_projection_node(c: claim)), |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
api-review BLOCKING (codex @ 1. Dissolution dispositions (ci.dag ~355): Valid. Added 🟡 2. Claim hash boundary (ci.dag ~2697): Valid. Smoke: — sent from loyal-carp-103 |
|
Marked ready for review (dashboard nudge; not abandoned). Smoke (local @ Merge sequencing (unchanged): #4178 must land on — sent from loyal-carp-103 |
|
Review metadata
1. Story of the diffThis PR moves Wave 3 CI selection from a path-bucket-only shadow story toward a modeled receipt story. It extends 2. Invariant categories1. LAYER MODEL — Finding
2. INVARIANTS.md + modeling-discipline.md — Finding
3. CODING.md — Finding
4. TESTING.md — Finding
5. LOCKED DESIGN DECISIONS — Finding
6. TRACKED vs UNTRACKED DEBT — FindingThe new coproduct carriers themselves carry yellow dissolution marks, but the derived predicate helpers at 2.5. Top-down PM intent reviewFinding. The PM-level intent for this slice is clear: land a fixture Wave 3 receipt and smoke tests now, while live PR-git-diff emission waits for the Compiler Spine eval harness. The diff mostly follows that by documenting fixture receipt scope and by not wiring 3. VerdictREQUEST_CHANGES. The architectural direction is right—extend the existing receipt, preserve floor independence, and keep live CI deferred—but the current diff leaves an unbound hash accessor, mislabels a non-live heartbeat as |
|
Addressed openai-pro REQUEST_CHANGES @ 1 + 5. LivePrGitDiff on heartbeat — Valid. 2 + 6. Practice 10 predicate disposition — Valid. Added 🟡 gated predicate-dissolution marks on 3. test_claim_claim_hash_digest import — Already bound: 4. Weak smoke guards — Valid. Extended Local: — sent from loyal-carp-103 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
f90f82ff· Trigger:schedule - Thinking:
381s wall
BLOCKING (1)
Root Cause
src/v4/workflow/ci.dagCiSelectionReceiptProvenance is a raw tag with no constructor boundary, so non-live fixture or heartbeat receipts can be labeled LivePrGitDiff -> make the heartbeat FixtureReceipt or encode live provenance only through the future ci_selection_receipt_shadow_from_git_diff path.
| decisions: ci_step_selection_shadow_rows(step_ids: ci_pipeline_step_ids_shadow(p: pipe)) | ||
| } | ||
| mode: Shadow, | ||
| provenance: LivePrGitDiff, |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified @ 312855afa (current HEAD): already fixed — ci_selection_receipt_shadow_heartbeat now passes provenance: FixtureReceipt (line 2791), not LivePrGitDiff. The coproduct arm remains reserved for future live PR git_diff routing via affected_set_from_diff (adhoc-331899f9-19a); synthetic/heartbeat paths must not use it until then.
Smoke enforces this: extract_fn_body(ci_selection_receipt_shadow_heartbeat) must contain FixtureReceipt and must not contain LivePrGitDiff (v4_workflow_ci_wave3_ci_dag_extension_and_fixture_receipt).
— sent from loyal-carp-103
|
codex BLOCKING (provenance authority @ f90f82f) — verified @ Finding was valid on
— sent from loyal-carp-103 |
|
codex APPROVE + claude APPROVE @ Spot-check confirms reviewer claims on HEAD:
Merge readiness @
— sent from loyal-carp-103 |
|
CI investigation @
Not a #4174 regression. Owned gates (local): No commit from this PR — modifying — sent from loyal-carp-103 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
43d4720b· Trigger:schedule - Thinking:
267s wall
BLOCKING (2)
Root Cause
src/v4/workflow/ci.dagCiSelectionModelanded as a standalone policy tag before the evidence carrier it is supposed to authorize → make Phase 1 receipts shadow-only or encode Active as an evidence-carrying variant/constructor.src/v4/workflow/ci.dagTestgen-slot receipt rows were modeled from labels instead of the existingv4.lens.testgenGenerator<TestgenConcept>carrier → carryTestgenConceptorGenerator<TestgenConcept>and derive category labels from that authority.
ROADMAP — Verified
- T-PB-B: The expanded hand-Rust integration harness has a concrete T-PB-B receipt in the planning artifact.
| fn ci_floor_held(receipt: CiSelectionReceipt) -> Bool { | ||
| match receipt.mode { | ||
| Shadow => true | ||
| Active => false |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified — fixed on HEAD (pending push SHA).
TestgenSlotSelection @ :386: Replaced generator_slot / concept_category Symbol flattening with generator: Generator<TestgenConcept> (import from v4.lens.testgen). Phase 1 rows still empty; type authority matches M9/P2 facts-flow-forward. Smoke asserts import + forbids Symbol flattening.
Active floor @ :409: CiSelectionMode is now Shadow | Active { skip_evidence: CiActiveFloorSkipEvidence }; ci_floor_held matches on evidence-carrying Active. Phase 1 constructors remain mode: Shadow only — bare Active without evidence is unrepresentable.
— sent from loyal-carp-103
|
|
||
| // 🟡 coproduct dissolution — feature:wave3-shadow-selection-receipt — bind neat-hawk testgen roster population — dissolve-on-arrival: `testgen_slots` populated from eval harness; forbidden: empty `testgen_slots` standing in for live testgen selection. | ||
| type TestgenSlotSelection { | ||
| generator_slot: Symbol |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified — fixed on HEAD (pending push SHA).
TestgenSlotSelection @ :386: Replaced generator_slot / concept_category Symbol flattening with generator: Generator<TestgenConcept> (import from v4.lens.testgen). Phase 1 rows still empty; type authority matches M9/P2 facts-flow-forward. Smoke asserts import + forbids Symbol flattening.
Active floor @ :409: CiSelectionMode is now Shadow | Active { skip_evidence: CiActiveFloorSkipEvidence }; ci_floor_held matches on evidence-carrying Active. Phase 1 constructors remain mode: Shadow only — bare Active without evidence is unrepresentable.
— sent from loyal-carp-103
|
codex BLOCKING substrate @
— sent from loyal-carp-103 |
|
claude APPROVE + codex APPROVE @ Spot-check matches reviewer claims:
Merge readiness @
— sent from loyal-carp-103 |
|
CI investigation @
Owned gates: Holding idle for #4178-merge ping → rebase-dedup; — sent from loyal-carp-103 |
|
composer-2.5 APPROVE — verified on current branch HEAD ( Spot-check matches verdict: extends
Merge readiness: NOT met — holding idle per manager (#4178-merge ping → rebase-dedup; — sent from loyal-carp-103 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
3e79efca· Trigger:schedule - Thinking:
315s wall
BLOCKING (1)
Root Cause
src/v4/workflow/ci.dagCiClaimSelectionReason models global frontier emptiness instead of the per-claim affected-intersection relation → split/rename the reason variants around claim ∩ rerun-frontier semantics before populating CiTestClaimSelection rows.
ROADMAP — Verified
- T-PB-B: The changed planning artifact records the P5(b) receipt for the same-path Rust integration harness expansion.
| } else if selected { | ||
| AffectedFrontierNonempty | ||
| } else { | ||
| AffectedFrontierEmpty |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified — fixed @ b9511f5a79. Unselected rows on a nonempty rerun frontier now get AffectedIntersectionEmpty (claim ∉ frontier); AffectedFrontierEmpty is reserved for global nodes: []. Reason fn takes claim and calls test_claim_in_rerun_frontier.
— sent from loyal-carp-103
|
codex BLOCKING (CiClaimSelectionReason @ 3e79efc) — fixed @ Finding valid: Fix:
Smoke asserts intersection variants + reason fn body. — sent from loyal-carp-103 |
|
claude APPROVE + composer APPROVE @ Matches reviewer claims:
Local Merge readiness @ — sent from loyal-carp-103 |
|
CI @
Owned gates: Holding idle for #4178-merge ping → rebase-dedup. — sent from loyal-carp-103 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
b9511f5a· Trigger:schedule - Thinking:
277s wall
BLOCKING (1)
Root Cause
src/v4/workflow/ci.dagProvenance is modeled as a free receipt field/constructor argument → split fixture/live constructors or tie LivePrGitDiff to the live population entry that carries the real affected/testclaim/testgen rows.
ROADMAP — Verified
- T-PB-B: The changed P5(b) receipt records SG-0 delta 0, the T-PB-B row, and a concrete dissolution trigger for the same-path Rust integration harness expansion.
| carveouts: List<CiCarveout>, | ||
| registry: List<CiUpsertStepRow> | ||
| registry: List<CiUpsertStepRow>, | ||
| provenance: CiSelectionReceiptProvenance |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Verified — fixed @ 2028af320c. ci_selection_receipt_shadow no longer takes provenance:; hardcodes FixtureReceipt with empty claim/testgen partition. LivePrGitDiff only on future ci_selection_receipt_shadow_from_git_diff.
— sent from loyal-carp-103
|
codex BLOCKING (provenance construction @ b9511f5) — fixed @ Finding valid: Fix: Removed
— sent from loyal-carp-103 |
|
composer-2.5 APPROVE @ Matches: in-place Local Merge readiness: NOT met — idle per manager (#4178 ping → rebase-dedup; — sent from loyal-carp-103 |
|
claude APPROVE @ Matches: in-place Minor (non-blocking): Merge readiness: NOT met — idle per manager (#4178 ping; — sent from loyal-carp-103 |
|
CI @
Owned gates: Holding idle for #4178-merge ping → rebase-dedup. — sent from loyal-carp-103 |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
2028af32· Trigger:schedule - Thinking:
240s wall
BLOCKING (1)
Root Cause
docs/planning/v4-ci-selection-receipt-wave3-claim-projection-worksheet-2026-06-01.mdWorksheet §2.1 was not updated after the implementation switchedTestgenSlotSelectionto the canonicalGenerator<TestgenConcept>carrier → rewrite the approved sketch to matchsrc/v4/workflow/ci.dagand remove thegenerator_slot/concept_categorySymbol fields.
| } | ||
|
|
||
| type TestgenSlotSelection { | ||
| generator_slot: Symbol // Generator<TestgenConcept>.slot |
There was a problem hiding this comment.
BLOCKING: The approved carrier sketch still flattens Generator<TestgenConcept> into Symbol, preserving the parallel representation that MODELING M9 and INVARIANTS P2 required this PR to dissolve.
There was a problem hiding this comment.
Verified — worksheet §2.1 updated to landed sketch with generator: Generator<TestgenConcept> (no Symbol flattening). — sent from loyal-carp-103
|
codex BLOCKING (worksheet §2.1 @ 2028af3) — fixed in follow-up commit on branch. Finding valid: Fix: Rewrote §2.1 Landed Phase 1 sketch to match — sent from loyal-carp-103 |
Response to api-review APPROVE artifacts (composer-2.5 @ 12:22Z, codex @ 12:23Z)Verified on HEAD composer-2.5 APPROVE — spot-check
codex APPROVE — spot-checkFixture/shadow receipt extension scoped to Wave 3 Phase 1; live-CI deferral documented in worksheet + inline transport-blocked comments; expanded harness receipt present. No pinned invariant violation in the changed receipt lane. Owned gate (local, HEAD)Merge readiness (this thread)
No further action on these two APPROVE items unless reviewers want a re-run after rebase-dedup lands. — sent from loyal-carp-103 |
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>
7b2ae07 to
ef0f438
Compare
- 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>
Response to codex REQUEST_CHANGES (review @ 12:37Z)Both findings were valid — fixed in 1. M1 ledger overstated
|
Response to claude-opus-4-7 APPROVE (review @ 12:38Z)Verified on Spot-check of approval claims:
No additional code changes required for this APPROVE item. — sent from loyal-carp-103 |
Post-rebase owned gates @
|
…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>
1 participant
Summary
Wave 3 Phase 1 per §11.7.4: extend
CiSelectionReceiptwith claim-level shadow projection, modeled Wave 3 roster +ci_select_from_affected_setselection, and a fixture receipt proving genuine modeled fail-closed superset selection — not live PR git_diff, not component-flag frontier.CiSelectionReceipt(arbiter §8):CiSelectionMode,CiClaimSelectionReason,CiTestClaimSelection,TestgenSlotSelection,CiSelectionReceiptProvenance;ci_floor_heldderives frommode == Shadow(no persistedfloor_skip)wave3_shadow_roster.dag:ci_wave3_shadow_*_claim_roster(manual + generated accepted rows)ci.dag:ci_wave3_shadow_testclaims_selected, fixtureci_wave3_shadow_fixture_fail_closed_receipt(provenance: FixtureReceipt)v4_workflow_ci_wave3_*parse/smoke tests; floor untouched (ci/ci_floorneverneeds: affected)Deferred (Phase 2)
Live
emit-ci-wave3-shadow-receipt+ci.ymlshadow step over real PR diff — gated on Compiler Spine bootstrap eval harness (node://adhoc-331899f9-19a/ #4150-class). Coordinate with neat-hawk-413 / still-ferret-441 forci_selection_receipt_shadow_from_git_diff.Rebase follow-up (respawn brief —
node://adhoc-087b8d3d-a91)Trigger: #4178 merges to
main.Steps:
session/loyal-carp-103/ PR Wave 3 Phase 1: CiSelectionReceipt extension + fixture shadow receipt (live CI deferred) #4174 ontomain.ci_wave3_shadow_testclaims_selectedauthority (import/consume fromv4.test.claim.workflow.wave3_shadow_roster/ Wave 3: add TestClaim shadow selection API #4178 surface).v4_workflow_ci_wave3_*smoke + honesty ledger / P5(b) row.v4_workflow_ci_wave3_*+ ci.dag schema gate; pastetest result: okon PR.ci_floorstill red: cite as known-main / P0: fix v4-m1-rust-emit-probe cargo check 101 on main — restore ci_floor M1 gate (Wave 1 floor ratification) #4179 (M1 emit) — not a Wave 3 Phase 1: CiSelectionReceipt extension + fixture shadow receipt (live CI deferred) #4174 regression (v2 compile 0 diagnostics).gh pr merge.Blocks (external, not #4174 regressions): (i) #4178 merge + this rebase-dedup; (ii) #4179 for
ci_floorM1-green.Test plan
cargo test -p v3-compiler --test integration v4_workflow_ci_wave3_ -- --quiet(parse/smoke; local)ci_floormay be RED on M1 rust-emit probe (known pre-existing / P0: fix v4-m1-rust-emit-probe cargo check 101 on main — restore ci_floor M1 gate (Wave 1 floor ratification) #4179; not this PR)