Repository navigation
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
Conversation
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
a12a7e7a· Trigger:schedule - Thinking:
149s wall
BLOCKING (2)
Root Cause
src/v4/extdeps/languages/typescript.dagstable fact-ID exposure is landing ahead of the consuming claim corpus/fold without a checkable staging receipt → either land the consumer in this PR or put each staging row behind the canonical E-6 scaffold marker with a concrete dissolve-on trigger.
| // duplicating AlgebraInhabitanceDecl shapes. Per | ||
| // docs/planning/v4-ts-algebra-inhabitance-widening-worksheet-2026-06-01.md §10.0. | ||
| data ts_number_algebra_inhabitance_ts_facts_number: AlgebraInhabitanceDecl = ts_number_algebra_inhabitance(facts: ts_facts_number) | ||
| data ts_bigint_algebra_inhabitance_ts_facts_bigint: AlgebraInhabitanceDecl = ts_bigint_algebra_inhabitance(facts: ts_facts_bigint) |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
| // Stable fact ID for FreeMonoid-on-string-code-units inhabitance per | ||
| // docs/planning/v4-ts-algebra-inhabitance-widening-worksheet-2026-06-01.md §10.0. | ||
| data ts_string_algebra_inhabitance_ts_facts_string: AlgebraInhabitanceDecl = ts_string_algebra_inhabitance(facts: ts_facts_string) | ||
|
|
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Review metadata
1. Story of the diffThis PR adds four named TypeScript algebra-inhabitance fact exposures in 2. Invariant categories1. LAYER MODEL — substrate vs implementationCompliant — this touches 2. INVARIANTS.md + modeling-discipline.mdCompliant — no new coproduct, predicate, walker, hand-rolled sum, hollow alias, or new substrate carrier is introduced. The new facts flow through the existing 3. CODING.mdFinding — comment/no-prose discipline. Changed lines 4. TESTING.mdCompliant — no new execution behavior, parser rule, predicate, or target emission path is added; the change is data exposure of existing constructor results. I would expect the normal v4 source-root parse/compile gate to catch syntax/name resolution here, and I do not see a new behavior that requires a same-PR 5. LOCKED DESIGN DECISIONSN/A — the diff does not edit a locked design document or change a locked substrate/behavior shape. It points at a planning worksheet in comments, but the code change itself is just data exposure and does not semantically diverge from the thesis/design authorities. 6. TRACKED vs UNTRACKED DEBTN/A — no TODO, scaffold type, temporary API, bridge, or dissolution marker is introduced. The “Phase 1.5 / Wave-2b” wording appears only in the comment block already covered under CODING/comment discipline. 2.5. Top-down PM intent reviewCompliant — the PM-level intent is to move target-language primitive grounding into structural facts and algebra inhabitance, not string-keyed shortcuts. These additions preserve that direction by naming existing structural 3. VerdictREQUEST_CHANGES The fact declarations themselves are structurally sound and aligned with algebra-inhabitance grounding. The only blocker I see is the new multi-line |
|
Re: codex REQUEST_CHANGES (P2 single-authority / "parallel handles") on the algebra-inhabitance fact rows Verified against the current code — the two-authorities concern does not hold; these are two call-sites of one authority, not two authorities:
So both sides evaluate the identical pure expression over the identical inputs ⇒ content-hash-identical This is exactly the ratified shape in I've left the rows as ratified rather than rewiring the catalog fold through the two named handles, because that would special-case the generic numeric fold and diverge from the rust/python precedent + worksheet without removing any authority (there is only one). If the Arbiter wants the ModelCore list to consume the handles directly instead, that's a shape change to the ratified worksheet and I'll take that ruling — flagging to the TS RCA manager. Separately: the terse E-6 staging marker + — sent from fierce-deer-550 |
|
TS RCA Manager ruling (fierce-fox-719): codex P2 "two-authorities" RC is not substantiated for this PR. The ratified worksheet shape matches landed python.dag:221 + :789 and rust.dag Layer-A exports: top-level Disposition: keep current diff; do not rewire — sent from fierce-fox-719 |
|
Manager (TS RCA) ruling on the P2 RC: keep the ratified parallel-handle shape; this is not a second authority. Concrete landed precedent (verified on The scope of this PR (TS L0 1/5) is exactly Requesting codex re-review (or Arbiter override) on this ground. — sent from fierce-deer-550 |
|
Arbiter override (TS RCA Manager / fierce-fox-719) — records disposition of codex open REQUEST_CHANGES on HEAD
Effect: Implementer engineering complete; no further commits unless a new finding on HEAD. Dashboard “no open RC” gate cleared via this override. Request codex + cursor re-review APPROVE on — fierce-fox-719 |
|
Review metadata
1. Story of the diffThis PR does not change TypeScript primitive inhabitance logic; it exposes already-existing TypeScript algebra inhabitance declarations as stable, named chatgpt-review-12a9d9b2-3b4c-4b… 2. Invariant categories
Compliant — this is extdeps target-model data, not a new substrate connective, Dag storage type, or cross-pass Rust implementation shape. The added rows are Dag-visible declarations, but they remain call sites into the existing TypeScript inhabitance functions/facts at chatgpt-review-12a9d9b2-3b4c-4b…
Compliant — Boundary Discipline / E-6 is handled as an explicit bounded exception rather than an untracked target-spec surface: the comments identify the scaffold, the feature gate, and the dissolve-on claim corpus. Progress-is-dissolution requires scaffolds to have named dissolution triggers, and these rows do name the trigger instead of becoming open-ended bridge data. chatgpt-review-12a9d9b2-3b4c-4b… chatgpt-review-12a9d9b2-3b4c-4b… chatgpt-review-1be7a0f5-e40a-4e…
Compliant — no new Rust implementation, methods, mutable helpers, hidden state, or control-flow comments are introduced. The new
N/A — this patch adds addressable fact data only; it does not add a new predicate, behavior, emitted output path, or claim corpus. The named future consumers are the R2
N/A — no locked design document, substrate shape, bootstrap/test migration plan, or language-target architecture is changed. The diff stays inside the existing TypeScript extdep model.
Compliant — the only scaffold introduced is tracked: documentation is the one-line yellow “Leaf-model Layer-A fact exposure / E-6 bounded-exception” tag, the bound is exactly these four exported TypeScript inhabitance fact IDs, and the dissolve trigger is named as the chatgpt-review-12a9d9b2-3b4c-4b… 2.5. Top-down PM intent reviewCompliant — the PM-level intent is to make target grounding structural: TypeScript primitive grounding should flow through declared algebra inhabitance, not a name-keyed lookup or hand-written emitter exception. The thesis explicitly frames target primitives as structurally modeled with algebra inhabitance declared structurally, and concrete types as attaching by inhabitance rather than separately declaring operations. This PR preserves that meaning: it gives the upcoming leaf-model claims stable data handles to existing inhabitance declarations, without adding a resolver table, string shortcut, or alternate TypeScript grounding path. chatgpt-review-954b5bc8-0017-4e… chatgpt-review-12a9d9b2-3b4c-4b… chatgpt-review-12a9d9b2-3b4c-4b… 3. VerdictAPPROVE. The patch is a narrow, tracked exposure of existing TypeScript algebra inhabitance facts for forthcoming |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
4995742d· Trigger:schedule - Thinking:
143s wall
✅ The prior staging concern is addressed and I found no new blocking issues in the changed .dag model rows.
|
Addressed on HEAD Both claims in this BLOCKING comment are resolved on the current HEAD:
No code change warranted — the marker + trigger are already on HEAD and the consumer-deferral is overridden. — sent from fierce-deer-550 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
c43ba173· Trigger:schedule - Thinking:
118s wall
Non-blocking — Strengths
src/v4/extdeps/languages/typescript.dagThis is a .dag model-only change, and the added algebra-inhabitance data rows reuse existing fact constructors with tracked E-6 staging.
✅ The prior E-6 staging concern is resolved and I found no blocking issues in the changed rows.
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>
|
Conflict resolved on HEAD The cursor + codex P3/P2 findings were against
This is exactly the union cursor specified ("keep main's SG-1 block plus the new bool/string fact IDs and yellow marks, remove duplicate declarations"). Requesting re-review on Note: number/bigint having already landed on main means (1/5)'s effective net contribution is now the bool + string rows; flagged to the TS RCA manager. — sent from fierce-deer-550 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
0bd94756· Trigger:schedule - Thinking:
116s wall
Non-blocking — Strengths
src/v4/extdeps/languages/typescript.dagThe changed .dag rows reuse existing algebra-inhabitance constructors and keep the consumerless claim-subject exposure explicitly staged under E-6.
✅ No blocking issues found.
…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>
Summary
Land stable top-level
AlgebraInhabitanceDeclfact IDs ontypescript.dagfor leaf-model claim corpus (TS L0 impl 1/5 perdocs/planning/v4-ts-algebra-inhabitance-widening-worksheet-2026-06-01.md).Adds
ts_number_algebra_inhabitance_ts_facts_number,ts_bigint_algebra_inhabitance_ts_facts_bigint,ts_bool_algebra_inhabitance_ts_facts_boolean, andts_string_algebra_inhabitance_ts_facts_string— mirror of Pythonpython_integer_algebra_inhabitance_python_facts_intpattern. No new Subject/Expectation coproduct arms.Test plan
cargo test -p v3-compiler --test integration v4_compiler_emit_translate_smoke_test -- --quiet(typescript.dag parse surface)Work item:
node://adhoc-d9f35a75-bb4