Skip to content
Merged
Show file tree
Hide file tree
Changes from 9 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion docs/briefs/extdeps-t4-lane-closeout-receipt.md
Original file line number Diff line number Diff line change
Expand Up @@ -46,7 +46,7 @@ On-disk headers contradict the *derived* “NOT STARTED” wording still shown f
- **T-4.10** `formats/spice.dag` — present (plan already marks LANDED; rework-obligation note remains operator-owned).
- **T-4.12** `llvm_ir.dag` — header: **T-4.12 PASS (B2-OMNI)** (aligns with plan).
- **T-4.13** `machine_code.dag` — substantial model + **🟢 P4-3208** ledger tag (not “absent”).
- **T-4.14** `ptx.dag` — header: **T-4.14 PASS (IN-B)**.
- **T-4.14** `ptx.dag` — **PASS (IN-B)** dispatch posture (**DECISIONS.md L-3**); file header intentionally domain-neutral (no process-axis status tag in the carrier).

T-4.11 English boundary file path is per `TASKS.md`; not re-audited in this pass (Lane B / verification.dag coupling).

Expand Down
8 changes: 4 additions & 4 deletions docs/briefs/r4-program-dispatch-plan.md
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ first) · `DESIGN` · `OP` (operator ruling) · `CP1` (needs v4 front-end output
| T-4.11 | claim/english_ingest | SCAFFOLD | T-3/verification.dag | IFACE (AssertKind) | Lane B |
| T-4.12 | languages/llvm_ir | **LANDED** (#3171 merged; +#3229 de-prose +#3300 cost-move on main) — *pre-D2-reversal canonical path; see rework-obligation note* | T-1,T-2 | LANDED | T-4 mgr |
| T-4.13 | languages/machine_code | **IMPL (modeled slice)** — D2-REV per file header; Isa-parameterized slice + zero-diagnostic smoke landed | T-3, T-4 LanguageModel | CP1 (T-4 LanguageModel; modeled slice landed) | T-4 mgr |
| T-4.14 | languages/ptx | **PASS (IN-B)** per file header | T-1,T-2 | LANDED | T-4 mgr |
| T-4.14 | languages/ptx | **PASS (IN-B)** — **DECISIONS.md L-3**; `ptx.dag` header intentionally domain-neutral | T-1,T-2 | LANDED | T-4 mgr |
| **T-9** | compiler/04_infer | SCAFFOLD | T-8/CP-1b-close (∥) + T-4 | IMPL (T-4 keystone; CP-1b-close parallel, not keystone-gated) | Lane A |
| **T-10** | 05_emit + 00_compile | SCAFFOLD | T-9, T-4 | IMPL+IFACE | Lane A |
| **T-11** | emit per-target ×5 | NOT STARTED | T-10 | IMPL | Lane A |
Expand Down Expand Up @@ -126,8 +126,8 @@ first) · `DESIGN` · `OP` (operator ruling) · `CP1` (needs v4 front-end output
- **Lens footnote:** the PREFIX driver/corpus gate is **T-23 + driver**, not
T-12 alone; T-12/T-13/T-17/T-18/T-23 rows match the running lens fan-out.
- **T-4-mgr staleness correction (verified vs main):** T-4.10 (#3168),
T-4.12 (#3171) are **already LANDED**. T-4.9 (`verilog.dag`) and T-4.14
(`ptx.dag`) now carry **PASS (IN-B)** in their file headers, and T-4.13
T-4.12 (#3171), T-4.14 (#3170) are **already LANDED**. T-4.9 (`verilog.dag`)
carries **PASS (IN-B)** in its file header (probe receipt; §2 Status column echoes that for T-4.9). **T-4.14** (`ptx.dag`) records the same **PASS (IN-B)** dispatch posture under **DECISIONS.md L-3** with a **domain-neutral** file header (no process-axis status tag in the carrier). T-4.13
(`machine_code.dag`) carries a **D2-REV Isa-parameterized modeled slice**
with a zero-diagnostic `compile_to_dag` smoke; §2 keeps T-4.13 **CP1-blocked on T-4
LanguageModel** per TASKS.md while recording the landed smoke/model
Expand Down Expand Up @@ -339,7 +339,7 @@ sessions are *not* folded in — see exceptions.
|---|---|---|---|
| **Fresh: Compiler-Pipeline (+Lens, gated)** | **Pipeline scope (active on Wave-0 go):** T-3 tail, T-6–T-8 CP-1b close, T-9, T-10, T-11, T-16, T-25-tail, T-28; **T-26 = std-authoritative, conduit-only**. **Lens scope (T-12/13/17/18/23) — GATED on the `fierce-cat-31` lens fan-out CLOSEOUT** (one lens owner at a time — see exception 2; no P2 parallel-authority drift) | Wave-0: T-3 tail / CP-1b / T-26 only | **Mirrors §4 topology (strict, codex BLOCKING):** W2 T-9 → W3 T-10 (+T-4.8, +T-12/13 refine) → W4 T-11 (+T-17, +T-18 — lens-scope, also post-closeout) → W5 **T-16** → W6 T-15 handoff. Lens scope (T-12/13/17/18/23) additionally post-`fierce-cat-31`-closeout. |
| **Fresh: Test/Bootstrap-Infra** | T-19, T-20, T-21, T-22, T-24, T-14, T-15, T-4.11, T-32 | **T-19, T-20, T-21** (full) · **T-22** (`READY*` scaffold scope) | §4-mirrored: T-24 W4 (post T-20/T-21), T-14 W4 (post T-19), **T-15 W6** (terminal, post T-16) |
| **Fresh: extdeps/T-4** | T-4 ×5, T-4.5–T-4.14 | **— (T-4.9/T-4.10/T-4.12/T-4.14 LANDED; T-4.13 modeled slice landed but LanguageModel-blocked; T-29 core #3267 merged but **residual #3277 OPEN & still a TASKS.md-declared T-4-cpp feeder**; T-4 ×5 HELD on the **full TASKS.md:286 feeder set `{P1-KEYSTONE, T-30, T-29, T-25-core}`** — all four, never keystone-only (same gate as the §2 T-4 row and this row's gated cell))** | T-4 (post the **full TASKS.md:286 feeder set `{P1-KEYSTONE + T-30 + T-29 #3277 + T-25-core}`** — not "keystone + T-29" alone; T-25-core and T-30 are hard T-4 prerequisites too). **T-4.5–4.8 follow their own §2 table deps, NOT the full ×4** (T-4.5: `T-3,T-25-core`; T-4.6: `T-25-core,T-26`; T-4.7/T-4.8: post-T-4) — §2 is the sole dependency authority; this lane cell does not widen their gate. |
| **Fresh: extdeps/T-4** | T-4 ×5, T-4.5–T-4.14 | **— (T-4.9/T-4.10/T-4.12/T-4.14 LANDED; T-4.13 modeled slice landed but LanguageModel-blocked; T-29 core #3267 merged; #3338 merged (language/extdeps smoke + doc hygiene); **residual #3277 OPEN** & still a TASKS.md-declared T-4-cpp feeder**; T-4 ×5 HELD on the **full TASKS.md:286 feeder set `{P1-KEYSTONE, T-30, T-29, T-25-core}`** — all four, never keystone-only (same gate as the §2 T-4 row and this row's gated cell))** | T-4 (post the **full TASKS.md:286 feeder set `{P1-KEYSTONE + T-30 + T-29 #3277 + T-25-core}`** — not "keystone + T-29" alone; T-25-core and T-30 are hard T-4 prerequisites too). **T-4.5–4.8 follow their own §2 table deps, NOT the full ×4** (T-4.5: `T-3,T-25-core`; T-4.6: `T-25-core,T-26`; T-4.7/T-4.8: post-T-4) — §2 is the sole dependency authority; this lane cell does not widen their gate. |
| **Fresh: Dissolution** | T-30, T-31, Wave-2 lenses, 🟡 burn-down | **T-31(b) mop-up; T-30 generated-checker** | Wave-2 lenses — *consumes* the §4 cross-lane prereqs (new std/ carriers + 3 derived lens-stages built by Compiler-Pipeline+Lens) — post A1-ratification |
| **Operator** | Keystone rulings | **see §7 decision sheet** | — |

Expand Down
4 changes: 2 additions & 2 deletions scripts/strict_deprose_dag.py
Original file line number Diff line number Diff line change
Expand Up @@ -481,10 +481,10 @@ def main() -> None:
),
(
"src/v4/extdeps/languages/ptx.dag",
"// Scope: NVIDIA PTX ISA 8.5 SIMT structural classifiers (T-4.14).",
"// Scope: NVIDIA PTX ISA 8.5 SIMT structural classifiers (param/shared state, registers, thread hierarchy).",
"// Anchor: https://docs.nvidia.com/cuda/pdf/ptx_isa_8.5.pdf — TOC https://docs.nvidia.com/cuda/parallel-thread-execution/index.html",
"// Consumes: std/nat.dag (Nat); std/cardinality.dag (PositiveUpperBoundedNat).",
"// Status: T-4.14 PASS (IN-B).",
"// Status: structural carriers present; conformance detail in DECISIONS.md Part 6.",
),
(
"src/v4/std/integer.dag",
Expand Down
2 changes: 1 addition & 1 deletion src/v4/TASKS.md
Original file line number Diff line number Diff line change
Expand Up @@ -698,7 +698,7 @@ model shape to keep the probe "parallel."

#### T-4.14: `extdeps/languages/ptx.dag` (CUDA)
- **Stress axis**: the **SIMT data-parallel execution model** vs the 5 L1 behaviors — the IN-B bet again (like Verilog's concurrency, but data-parallel). A needed 6th `Parallel`/`Kernel` behavior = C1 escalation, by design caught early.
- **Fork (PROPOSED — confirm)**: model **PTX** (the spec'd IR — clean, general, captures SIMT directly, parallel to llvm_ir; recommended) vs CUDA-C++ as a `cpp.dag` extension (entangled; the C++ surface is not where the stress is).
- **PTX path (operator-ratified / evidenced):** model **PTX** (the spec'd IR — clean, general, captures SIMT directly, parallel to `llvm_ir.dag`). The CUDA-C++-as-`cpp.dag` extension alternative is the **rejected** fork (entangled; the C++ surface is not where the stress is). **IN-B probe receipt** is **DECISIONS.md L-3** (PTX falsification posture; `ptx.dag` file header is intentionally domain-neutral). **Derived scheduling / completion state** for this slice is authoritative in **`docs/briefs/r4-program-dispatch-plan.md` §2** (Status column: **PASS (IN-B)**; **Blocked-on** `LANDED` — table-accuracy with main; *LANDED* ≠ every TASKS Scope:L tail dissolved — see that row’s rework-obligation / keystone blast-radius notes in the dispatch plan).
- **Anchor**: NVIDIA PTX ISA spec, pinned version (L-2).
- **Scope**: L.

Expand Down
4 changes: 2 additions & 2 deletions src/v4/extdeps/languages/ptx.dag
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
// src/v4/extdeps/languages/ptx.dag
// Scope: NVIDIA PTX ISA 8.5 SIMT structural classifiers (T-4.14).
// Scope: NVIDIA PTX ISA 8.5 SIMT structural classifiers (param/shared state, registers, thread hierarchy).
// Owns: ParamScope, SharedScope, StateSpace, BarrierScope, ThreadAxis, ThreadCoordSource, BitsWidth, IntegerWidth, FloatWidth, RegisterScalarKind, RegisterStateSpace, RegisterScalar, Dim3, ThreadHierarchyShape, ThreadCoord, PtxCost
// Consumes: std/nat.dag (Nat); std/cardinality.dag (PositiveUpperBoundedNat).
// Status: T-4.14 PASS (IN-B).
// Status: structural carriers present; conformance detail in DECISIONS.md Part 6.
// Anchor: https://docs.nvidia.com/cuda/pdf/ptx_isa_8.5.pdf — TOC https://docs.nvidia.com/cuda/parallel-thread-execution/index.html
// Ledger: DECISIONS.md Part 6 (PR #3229): CP-3229-GREEN-TERMINAL, SL-3229-PTX-DIM3.

Expand Down
6 changes: 3 additions & 3 deletions src/v4/extdeps/process.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// Scope: process substrate — command invocation, lifecycle, wait/capture.
// Owns: ProcessId, ExitCode, SignalNum, PosixArgument, PosixEnvironmentName, PosixEnvironmentValue, Command, Termination, TerminatedProcessState, ProcessIdentity, RunningProcess, TerminatedProcess, WaitedTerminatedProcess, CaptureSource, ProcessTable, ProcessResources, CapturedByteStream, CapturedOutputPipes, process request/result/operation carriers.
// Consumes: AbsolutePath, Filesystem, PosixByteString, Diagnostic, Outcome, Byte, FreeMonoid, Int, List, Map.
// Status: T-4.5 modeled 2026-05-16.
// Status: modeled 2026-05-16 (POSIX-oriented scaffold).

module v4.extdeps.process

Expand All @@ -14,15 +14,15 @@ import v4.std.machine { Byte }


// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/sys_types.h.html + https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/signal.h.html
// scaffold: POSIX numeric refinements; trigger T-25-core/T-30.
// scaffold: POSIX numeric refinements; staging in DECISIONS.md OS-1.
type ProcessId = Int
type ExitCode = Int
type SignalNum = Int


// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/functions/exec.html
// tag: POSIX exec byte strings.
// scaffold: POSIX exec byte refinements; trigger T-25-core/T-30.
// scaffold: POSIX exec byte refinements; staging in DECISIONS.md OS-1.
type PosixArgument {
bytes: PosixByteString
}
Expand Down
Loading