v4 T-4.5 Lane C: model extdeps/process.dag + extdeps/file_system.dag — OS-interaction substrate bundle (L-2 spec-first, // Anchor: version-pinned, C5-fidelity, forward-model)

src/v4/DECISIONS.md

@@ -61,6 +61,7 @@ authority location(s) and moves to Part 1.
 | **D4** | **[SUPERSEDED by D2-REV — see the D2-REV row below + the "D2 REVERSAL" section]** **GroundingMap-home — the shared `extdeps/languages/resolver.dag` registry** (operator-ratified 2026-05-16; co-drafted; completes **D2**). The D2 resolver's *shared* types live in ONE new file `extdeps/languages/resolver.dag` — NOT re-declared per language (parallel-declaration P2 forbids; `feedback_import_not_redeclare_carriers`) and NOT homed in `rust.dag` (which would make one language file a substrate authority for the other four, and balloon as future shared resolver types land). `type GroundingMap<IRCarrier> { spelling: String }` is its first resident. **Admission rule (STRICT):** `resolver.dag` hosts ONLY *structurally-language-INVARIANT* resolver types — a type whose structure provably cannot vary across the modeled language specs (a convergence carrier). Spec-varying types stay per-language (`OverflowDisposition` etc. — D2.5 / L-2). Test before admitting: can you prove the structure invariant across the specs? Future shared resolver types (e.g. the C5-fidelity `Modeled \| Declared-normalized \| Fail-closed` disposition classifier) land here without a fresh placement decision. Closed-tree extension: `STRUCTURE.md` `.dag` count +1. Per-language files each add a one-line `import … resolver { GroundingMap }` + their per-primitive `data <lang>_<prim>_grounding` instances (the grounding-row fan-out — canonical `rust.dag` first, then the 4 others). | new `extdeps/languages/resolver.dag` + `STRUCTURE.md` count/enumeration + `extdeps/languages/*` import lines + grounding instances; this row; cross-ref **D2** |
 | **D5** | **Operator-driven frozen-header / frozen-contract reconcile is sanctioned in-PR** (operator-ratified 2026-05-16). "Preserve-verbatim" on a frozen scaffold header forbids *unsanctioned worker contract-drift* — it does NOT forbid *sanctioned reconciliation*. When an operator-tier action (a BLOCKING finding, an operator ruling) legitimately moves a worker's body past its frozen header or I/O contract, the header/contract is **reconciled to match in the SAME PR**, with the reconcile receipt — citing the driving operator action — recorded in the **commit message**. **Amended 2026-05-17 (operator-ratified):** the receipt is a commit-message entry, *not* an in-file `HEADER RECONCILE` block — the in-file-block form is superseded by the no-prose directive / `docs/modeling-discipline.md` Practice 9. D5's intent — a conscious, reviewer-visible reconcile receipt — is preserved: it lives in the commit message + `git blame`. **Discriminator:** an operator-tier action drove the body change ⇒ reconcile the header/contract in-PR, flagged; NO operator action drove it ⇒ the body must conform to the frozen header (preserve-verbatim holds, the worker cannot move the contract). Covers BOTH header-doc drift (stale `Owns`/`Consumes` bullets after a sanctioned refactor) AND frozen-contract changes (operator BLOCKS an I/O contract as P2/§2-insufficient). Already operating: `integer.dag` #3190 (`Consumes` reconciled), #3209 finding 2 (`WaitProcessResult`). Does NOT permit free worker header edits — operator-driven only. | this row + the reconcile receipt recorded in the **commit message** (the in-file `HEADER RECONCILE` block form — `integer.dag` #3190 precedent — is retired by Practice 9, 2026-05-17); refines the frozen-scaffold-header / preserve-verbatim discipline |
 | **D2-REV** | **D2 / D4 REVERSED — fact-bundle modeling supersedes alias-identity** (operator-ratified 2026-05-17, **out-of-band** — the verbatim operator-quote provenance is in the "D2 REVERSAL" section below). An `extdeps` primitive is modeled as a fact-bundle grounded from its own spec, never a bare `std/` alias; deduplicate to a `std/` carrier only on *proven* coincidence; the structural fact-density / hollow-alias gate is `T-30`, a hard prerequisite of T-4. This is a one-line index pointer — the full record (root cause, phased plan, impact map, "coincide" definition) is the **"D2 REVERSAL + FACT-BUNDLE RESEED"** section below, which is the authority. Supersedes the **D2** and **D4** rows above. | the **"D2 REVERSAL + FACT-BUNDLE RESEED"** section of this file (authority); `#3224` executes Phase 1; `docs/modeling/grounding-worked-examples.md` companion |
+| **OS-1** | **OS extdep coproduct ledgers and refinement-scaffold disposition for #3209** (operator-audit regime, 2026-05-17). Practice-4 dissolution ledgers for `file_system.dag` / `process.dag` are architectural decision records, not source comments; the `.dag` files keep only terse tags/anchors. POSIX numeric and byte-string refinement gaps remain tracked scaffolds in #3209, not expanded fact bundles; named trigger is **T-25-core refinement substrate / T-30 fact-density gate**. | this row + "OS-1 — #3209 coproduct dissolution and scaffold record" below; terse tags in `extdeps/file_system.dag` and `extdeps/process.dag` |
 
 ---
 
@@ -118,6 +119,102 @@ remain boundary indexes until the named substrate support lands.
 
 ---
 
+## OS-1 — #3209 Coproduct Dissolution And Scaffold Record
+
+This section preserves the Practice-4 ledger content moved out of
+`src/v4/extdeps/file_system.dag` and `src/v4/extdeps/process.dag` during
+the strict de-prose pass. The source files keep only path/scope/owns/
+consumes/status, anchor lines, and terse concept/scaffold tags.
+
+### Coproduct Classifications
+
+All listed coproducts are **YELLOW, first-consumer-confirmed**. The
+named first-consumer trigger is the T-4.5 OS realization seam unless a
+more specific trigger is stated.
+
+- `PathComponent`: POSIX `.` and `..` component semantics are distinct
+  from ordinary filename spellings. Trigger: filesystem path parsing /
+  resolution realization. Ledger: fact placement fails because component
+  kind is consumed uniformly by path resolution; variant-is-data fails
+  because current/parent are semantic facts and named spelling is
+  payload; algebraic form is not applicable; dimensional fails because
+  a component is exactly current, parent, or named; parameterized family
+  fails because variants are not identical payloads over an enumerable
+  set.
+- `RelativePathHead`: non-current relative descendants can begin with
+  parent traversal or named component. Trigger: filesystem path parsing /
+  resolution realization. Ledger: fact placement fails because
+  first-component admissibility is consumed by relative path resolution;
+  variant-is-data fails because parent traversal and named payload are
+  different facts; algebraic form is not applicable; dimensional fails
+  because a non-current relative descendant head is parent or named;
+  parameterized family fails because variants are not identical payloads
+  over an enumerable set.
+- `RelativePath`: current directory, current-prefixed descendant with a
+  non-current continuation, and non-current relative descendant are
+  distinct POSIX relative-path facts. Trigger: filesystem path parsing /
+  resolution realization. Ledger: fact placement fails because the
+  partition is consumed uniformly by path operations; variant-is-data
+  fails because current-prefixed and non-current descendants carry
+  different leading facts while sharing the non-current continuation
+  head; algebraic form is not applicable; dimensional fails because a
+  relative path is current directory, current-prefixed descendant, or
+  non-current descendant; parameterized family fails because variants
+  are not identical payloads over an enumerable set.
+- `Path`: absolute-vs-relative is a POSIX root fact. Trigger:
+  filesystem path parsing / resolution realization. Ledger: fact
+  placement fails because root-ness is consumed by path resolution and
+  operation realization; variant-is-data fails because a flat
+  `absolute: Bool` duplicates the partition as a flag; algebraic form
+  is not applicable; dimensional fails because a path is absolute or
+  relative; parameterized family fails because variants are not projected
+  over a separate payload family.
+- `FileKind`: v4's bounded filesystem subset observes regular file,
+  directory, or symlink. Trigger: first `file_kind` realization. Ledger:
+  fact placement fails because file kind is consumed uniformly by
+  readers/listing/link handling; variant-is-data fails because the
+  variant is the file-kind fact and readlink target is a separate POSIX
+  observation; algebraic form is not applicable; dimensional fails
+  because one directory entry has one kind in this subset; parameterized
+  family fails because variants are not mechanically identical payloads.
+- `FileKindResolutionPolicy`: the boundary declares stat-like follow or
+  lstat-like no-follow symlink observation. Trigger: `file_kind`
+  realization. Ledger: fact placement fails because resolution policy is
+  a request-boundary fact; variant-is-data fails because each variant is
+  a distinct observation mode without shared payload; algebraic form is
+  not applicable; dimensional fails because one request follows symlinks
+  or does not; parameterized family fails because variants are not a
+  projection over an independently modeled payload family.
+- `Termination`: POSIX wait status is exit or signal. Trigger:
+  fork/exec/wait realization. Ledger: fact placement fails because
+  terminal status is consumed uniformly by wait/capture carriers;
+  variant-is-data fails because exit and signal carry different payloads
+  and a flat record admits impossible combinations; algebraic form is
+  not applicable; dimensional fails because a terminal process ended by
+  exit or signal; parameterized family fails because variants are not
+  identical payloads.
+- `CaptureSource`: capture can drain from a live spawned child or a
+  waited child whose pipe authority was preserved. Trigger: capture
+  realization. Ledger: fact placement fails because capture source state
+  is consumed uniformly by capture; variant-is-data fails because each
+  variant carries the lifecycle process authority and current or waited
+  resource authority; algebraic form is not
+  applicable; dimensional fails because one request uses live or
+  post-wait authority; parameterized family fails because variants carry
+  different lifecycle carriers.
+
+### Refinement Scaffold Disposition
+
+The following are intentionally tracked as YELLOW refinement scaffolds in
+#3209 rather than expanded into structural value-refinement or witness
+carriers: `ProcessId = Int`, `ExitCode = Int`, `SignalNum = Int`,
+`NamedPathComponent { bytes: PosixByteString }`, `PosixArgument`,
+`PosixEnvironmentName`, and `PosixEnvironmentValue`. The named trigger is
+**T-25-core refinement substrate / T-30 fact-density gate**. Expanding
+them now would be fact-bundle-rework-class work, outside the NOT-D2-held
+de-prose scope.
+
+
 ## Part 2 — RATIFIED 2026-05-15 (cascade-closures — now in Part 1)
 
 > **All three (U2, C3, C1) were ratified and are encoded — see Part 1.**

src/v4/extdeps/file_system.dag

@@ -1,37 +1,109 @@
 // src/v4/extdeps/file_system.dag
-//
-// Scope: file system model — paths, file kinds, read/write/list operations.
-// Anchor: https://en.wikipedia.org/wiki/File_system
-//         + https://pubs.opengroup.org/onlinepubs/9699919799/ (POSIX File and Directory Operations)
-//
-// Owns:
-//   - Path = AbsolutePath | RelativePath
-//   - AbsolutePath { components: NonEmptyList<PathComponent> }
-//   - RelativePath { components: List<PathComponent> }
-//   - PathComponent (NonEmptyStr, no slashes, no nulls — per POSIX portable filename charset)
-//   - FileKind = RegularFile | Directory | Symlink(target: Path)
-//   - read_file(p)        -> Result<FreeMonoid<Char>, Diagnostic>
-//   - write_file(p, body) -> Result<Unit, Diagnostic>
-//   - list_dir(p)         -> Result<List<PathComponent>, Diagnostic>
-//   - file_kind(p)        -> Result<FileKind, Diagnostic>
-//
-// Scope NOT included in v4 (subset for compiler self-hosting needs):
-//   - Permissions (mode bits) — out of scope; v4 compiler reads/writes own files
-//   - Timestamps (atime/mtime/ctime) — out of scope; not needed for emission
-//   - Memory mapping — out of scope; v4 reads files into memory wholesale
-//   - File locking — out of scope; v4 is single-process
-//
-// Consumes:
-//   - std/diagnostic.dag: Diagnostic
-//   - std/text.dag: Char, String (and their Tier-2 totalizations)
-//   - std/algebra.dag: FreeMonoid<Char>
-//   - std/collection.dag: List, NonEmptyList
-//
-// Status: scaffold — fill per TASKS.md T-4.5
-// Brief: see BRIEF_TEMPLATE.md; this file's I/O contract is the immutable
-// contract for the worker. Splitting this file requires explicit operator
-// ratification (substrate extension = stop signal).
-
+// Scope: file system substrate — paths, file kinds, read/write/list/kind operations.
+// Owns: PosixByteString, NamedPathComponent, PathComponent, AbsolutePath, RelativePathHead, RelativePath, Path, FileKind, FileKindResolutionPolicy, Filesystem, FileBody, file-system request/result/operation carriers.
+// Consumes: Diagnostic, Outcome, Byte, FreeMonoid, List.
+// Status: T-4.5 modeled 2026-05-16.
 
 module v4.extdeps.file_system
 
+
+import v4.std.algebra { FreeMonoid }
+import v4.std.diagnostic { Outcome }
+import v4.std.machine { Byte }
+
+
+// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/V1_chap03.html#tag_03_241
+// coincides: finite POSIX byte sequence.
+type PosixByteString = FreeMonoid<Byte>
+
+// tag: named pathname component spelling.
+// scaffold: POSIX byte refinements; trigger T-25-core/T-30.
+type NamedPathComponent {
+  bytes: PosixByteString
+}
+
+// 🟡 coproduct dissolution — DECISIONS.md OS-1
+type PathComponent
+  = CurrentComponent
+  | ParentComponent
+  | NamedComponent { component: NamedPathComponent }
+
+
+// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/V1_chap03.html#tag_03_271
+type AbsolutePath {
+  components: List<PathComponent>
+}
+
+// 🟡 coproduct dissolution — DECISIONS.md OS-1
+type RelativePathHead
+  = ParentHead
+  | NamedHead { component: NamedPathComponent }
+
+// 🟡 coproduct dissolution — DECISIONS.md OS-1
+type RelativePath
+  = CurrentDirectory
+  | CurrentDescendant { first: RelativePathHead, rest: List<PathComponent> }
+  | RelativeDescendant { first: RelativePathHead, rest: List<PathComponent> }
+
+// 🟡 coproduct dissolution — DECISIONS.md OS-1
+type Path
+  = Absolute { path: AbsolutePath }
+  | Relative { path: RelativePath }
+
+
+// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/sys_stat.h.html
+// 🟡 coproduct dissolution — DECISIONS.md OS-1
+type FileKind
+  = RegularFile
+  | Directory
+  | Symlink
+
+// tag: stat/lstat symlink policy.
+// 🟡 coproduct dissolution — DECISIONS.md OS-1
+type FileKindResolutionPolicy
+  = FollowSymlinks
+  | DoNotFollowSymlinks
+
+
+// Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/functions/read.html + https://pubs.opengroup.org/onlinepubs/9799919799/functions/write.html + https://pubs.opengroup.org/onlinepubs/9799919799/functions/readdir.html
+type Filesystem
+
+// coincides: finite POSIX byte sequence.
+type FileBody = FreeMonoid<Byte>
+
+type ReadFileRequest {
+  filesystem: Filesystem
+  path: AbsolutePath
+}
+
+type ReadFileResult = Outcome<FileBody>
+
+type WriteFileRequest {
+  filesystem: Filesystem
+  path: AbsolutePath
+  body: FileBody
+}
+
+type WriteFileResult = Outcome<Filesystem>
+
+type ListDirRequest {
+  filesystem: Filesystem
+  path: AbsolutePath
+}
+
+type ListDirResult = Outcome<List<PathComponent>>
+
+type FileKindRequest {
+  filesystem: Filesystem
+  path: AbsolutePath
+  resolution: FileKindResolutionPolicy
+}
+
+type FileKindResult = Outcome<FileKind>
+
+type FileSystemOperations {
+  read_file: fn(ReadFileRequest) -> ReadFileResult
+  write_file: fn(WriteFileRequest) -> WriteFileResult
+  list_dir: fn(ListDirRequest) -> ListDirResult
+  file_kind: fn(FileKindRequest) -> FileKindResult
+}