Wave-1 Worker C — infer lens-import cleanup + std/outcome.dag traverse + extdeps/file_system.dag effects

src/v4/compiler/04_infer.dag

@@ -1,16 +1,15 @@
 // src/v4/compiler/04_infer.dag
 // Scope: Stage 4 — ResolvedTree -> InferredTree; bounded Find phase (DECISIONS C1 / IR-1).
 // Owns: AlgebraRef, InferredFacts, InferredTree, infer_stage_locus_port, infer_coercion_fold_not_realized, infer_coercion_fold_not_realized_diagnostic, infer.
-// Consumes: v4.compiler.resolve, v4.lens.cost, v4.std.cardinality, v4.std.collection, v4.std.diagnostic, v4.std.node.
-// Status: scaffold — TASKS T-9; Wave-1 fail-closed boundary.
+// Consumes: v4.compiler.resolve, v4.std.cardinality, v4.std.collection, v4.std.diagnostic, v4.std.node.
+// Status: scaffold — TASKS T-9; Wave-1 fail-closed boundary; no lens imports (P3 commitment 4).
 // Anchor: https://en.wikipedia.org/wiki/Type_inference
 
 
 module v4.compiler.infer
 
 
 import v4.compiler.resolve { ResolvedTree }
-import v4.lens.cost { SymbolicCost }
 import v4.std.cardinality { TerminationProof }
 import v4.std.collection { Map }
 import v4.std.diagnostic {
@@ -19,6 +18,7 @@ import v4.std.diagnostic {
   Locus,
   Outcome,
   PortLocus,
+  Rejected,
   Unavailable
 }
 import v4.std.node { Node, Symbol }
@@ -31,11 +31,10 @@ type AlgebraRef {
 }
 
 
-// RULING-1: needs-more-work — cost/inhabitance coordinates remain T-9/T-12 bridged.
+// RULING-1: needs-more-work — compiler-core semantic facts only; dimensional cost is lens-side (P3).
 type InferredFacts {
   resolved_type: Node
   inhabits: AlgebraRef
-  cost: SymbolicCost
   descent: TerminationProof
 }
 

src/v4/extdeps/file_system.dag

@@ -1,15 +1,24 @@
 // src/v4/extdeps/file_system.dag
-// 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.
+// Scope: file system substrate — paths, file kinds, modeled peripheral I/O effects.
+// Owns: PosixByteString, NamedPathComponent, PathComponent, AbsolutePath, RelativePathHead, RelativePath, Path, FileKind, FileKindResolutionPolicy, Filesystem, FileBody, FileResource, FilePath, FileContent, FileRead, FileWrite, NodeFileBinding, FileEffectWitness, FileWriteWitness, file-system request/result/operation carriers, file_read, file_write.
+// Consumes: std diagnostic, std outcome, std node, std algebra, std machine.
+// Status: T-4.5 modeled; peripheral effect surface per design-v4-compiler-homomorphism (not compile-core).
+
 
 module v4.extdeps.file_system
 
 
 import v4.std.algebra { FreeMonoid }
-import v4.std.diagnostic { Outcome }
+import v4.std.diagnostic {
+  Diagnostic,
+  ExternalContractUnknown,
+  Outcome,
+  PortLocus,
+  Rejected,
+  Unavailable
+}
 import v4.std.machine { Byte }
+import v4.std.node { Node, Symbol }
 
 
 // Anchor: https://pubs.opengroup.org/onlinepubs/9799919799/basedefs/V1_chap03.html#tag_03_241
@@ -71,6 +80,37 @@ type Filesystem
 // coincides: finite POSIX byte sequence.
 type FileBody = FreeMonoid<Byte>
 
+// Modeled resource — effects are explicit parameters against this carrier (B-5 DI).
+type FileResource {
+  filesystem: Filesystem
+}
+
+// Peripheral effect path coordinate (absolute path for MVP shims).
+type FilePath {
+  absolute: AbsolutePath
+}
+
+// Effect payload for read results.
+type FileContent = FileBody
+
+type FileWriteWitness {
+  resource: FileResource
+  path: FilePath
+}
+
+type NodeFileBinding {
+  node: Node
+  path: FilePath
+}
+
+// 🟡 coproduct dissolution — W-TRAVERSE-OUTCOME-FILE-EFFECT-WITNESS.
+// Trigger: ResourceDependsOn/EffectDependsOn wiring when std/dependency.dag lands (Worker A A1).
+type FileEffectWitness
+  = ReadWitness { path: FilePath, content: FileContent }
+  | WriteWitness { witness: FileWriteWitness }
+
+data file_effect_dependency_wiring_deferred: Symbol = file_effect_dependency_wiring_deferred
+
 type ReadFileRequest {
   filesystem: Filesystem
   path: AbsolutePath
@@ -107,3 +147,36 @@ type FileSystemOperations {
   list_dir: fn(ListDirRequest) -> ListDirResult
   file_kind: fn(FileKindRequest) -> FileKindResult
 }
+
+data file_read_effect_not_wired: Symbol = file_read_effect_not_wired
+
+data file_write_effect_not_wired: Symbol = file_write_effect_not_wired
+
+fn file_effect_not_wired_diagnostic(reason: Symbol) -> Diagnostic {
+  Diagnostic {
+    reason: reason,
+    at: PortLocus { port: reason },
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+
+fn file_read(
+  resource: FileResource,
+  path: FilePath,
+  ops: FileSystemOperations
+) -> Outcome<FileContent> {
+  Rejected {
+    diagnostic: file_effect_not_wired_diagnostic(reason: file_read_effect_not_wired)
+  }
+}
+
+fn file_write(
+  resource: FileResource,
+  path: FilePath,
+  content: FileContent,
+  ops: FileSystemOperations
+) -> Outcome<FileWriteWitness> {
+  Rejected {
+    diagnostic: file_effect_not_wired_diagnostic(reason: file_write_effect_not_wired)
+  }
+}

src/v4/std/diagnostic.dag

@@ -1,9 +1,9 @@
 // src/v4/std/diagnostic.dag
 // Scope: fail-closed diagnostic schema.
 // Anchor: THESIS.md "show the correct code" + INVARIANTS P3.
-// Owns: Diagnostic, Outcome, Locus, Extent, Correction, NoCorrectionReason.
+// Owns: Diagnostic, Outcome, NonEmptyDiagnostics, PluralDiagnostics, Locus, Extent, Correction, NoCorrectionReason.
 // Consumes: std node.
-// Status: T-3 modeled.
+// Status: T-3 modeled; Outcome stays legacy Produced/Rejected until Pass A correction packet.
 
 
 module v4.std.diagnostic
@@ -33,7 +33,18 @@ type Diagnostic {
   at: Locus
   correction: Correction
 }
-// 🟢 coproduct dissolution — CP-3229-GREEN-TERMINAL.
+// 🟡 coproduct dissolution — W-TRAVERSE-OUTCOME-NON-EMPTY-DIAGNOSTICS.
+// Trigger: dissolve to substrate NonEmptyList refinement (T-25-core); not yet in Outcome sum.
+type NonEmptyDiagnostics
+  = One { diagnostic: Diagnostic }
+  | More { head: Diagnostic, tail: NonEmptyDiagnostics }
+// Plural only — ≥2 diagnostics; not yet in Outcome sum (Pass A correction packet).
+type PluralDiagnostics {
+  head: Diagnostic
+  tail: NonEmptyDiagnostics
+}
+// 🟡 coproduct dissolution — W-TRAVERSE-OUTCOME-LEGACY-PRODUCED.
+// Trigger: Pass A correction collapses to Accepted/Rejected with Diagnostics substrate.
 type Outcome<T>
   = Produced { value: T }
   | Rejected { diagnostic: Diagnostic }

src/v4/std/outcome.dag

@@ -0,0 +1,134 @@
+// src/v4/std/outcome.dag
+// Scope: Outcome traverse combinators + diagnostic policy carriers + traverse law witnesses.
+// Owns: DiagnosticAccumulationPolicy, StageDiagnosticPolicy, NodeOutcomeFold, traverse_node, sequence_node, map_node_outcome, traverse_outcome, map_outcome, bind_outcome, append_non_empty, TraverseIdentityLaw, TraverseCompositionLaw, TraverseFailureMonotonicityLaw.
+// Consumes: std diagnostic, std node, std collection, std algebra.
+// Status: W-TraverseOutcome substrate (design-v4-compiler-homomorphism Ratified Q4 companion).
+
+
+module v4.std.outcome
+
+
+import v4.std.algebra { Empty, Cons }
+import v4.std.collection { List }
+import v4.std.diagnostic {
+  Diagnostic,
+  ExternalContractUnknown,
+  More,
+  NonEmptyDiagnostics,
+  One,
+  Outcome,
+  PortLocus,
+  Produced,
+  Rejected,
+  Unavailable
+}
+import v4.std.node { Edge, Node, Symbol }
+
+
+// 🟡 coproduct dissolution — W-TRAVERSE-OUTCOME-DIAGNOSTIC-POLICY.
+// Trigger: per-stage policy drives accumulate vs short-circuit in traverse_node fill.
+type DiagnosticAccumulationPolicy
+  = Accumulate
+  | ShortCircuit
+
+
+type StageDiagnosticPolicy {
+  accumulation: DiagnosticAccumulationPolicy
+}
+
+
+data traverse_identity_law: TraverseIdentityLaw = traverse_identity_law
+
+
+data traverse_composition_law: TraverseCompositionLaw = traverse_composition_law
+
+
+data traverse_failure_monotonicity_law: TraverseFailureMonotonicityLaw = traverse_failure_monotonicity_law
+
+
+type TraverseIdentityLaw {}
+
+
+type TraverseCompositionLaw {}
+
+
+type TraverseFailureMonotonicityLaw {}
+
+
+fn append_non_empty(front: NonEmptyDiagnostics, back: NonEmptyDiagnostics) -> NonEmptyDiagnostics {
+  match front {
+    One { diagnostic: d } => match back {
+      One { diagnostic: d2 } => More { head: d, tail: One { diagnostic: d2 } }
+      More { head: h, tail: t } => More { head: d, tail: More { head: h, tail: t } }
+    }
+    More { head: h, tail: t } => More { head: h, tail: append_non_empty(front: t, back: back) }
+  }
+}
+
+
+type NodeOutcomeFold<R> {
+  policy: StageDiagnosticPolicy
+  init: fn(Node) -> Outcome<R>
+  step: fn(Outcome<R>, Edge, Node) -> Outcome<R>
+}
+
+
+data traverse_node_not_realized: Symbol = traverse_node_not_realized
+
+
+fn traverse_node_not_realized_diagnostic() -> Diagnostic {
+  Diagnostic {
+    reason: traverse_node_not_realized,
+    at: PortLocus { port: traverse_node_not_realized },
+    correction: Unavailable { reason: ExternalContractUnknown }
+  }
+}
+
+
+fn traverse_node<R>(n: Node, algebra: NodeOutcomeFold<R>) -> Outcome<R> {
+  Rejected { diagnostic: traverse_node_not_realized_diagnostic() }
+}
+
+
+fn sequence_node<R>(nodes: List<Node>, algebra: NodeOutcomeFold<R>) -> Outcome<List<R>> {
+  Rejected { diagnostic: traverse_node_not_realized_diagnostic() }
+}
+
+
+fn map_node_outcome<T, U>(o: Outcome<T>, f: fn(T) -> Outcome<U>) -> Outcome<U> {
+  match o {
+    Rejected { diagnostic: d } => Rejected { diagnostic: d }
+    Produced { value: v } => f(v)
+  }
+}
+
+
+fn traverse_outcome<T, U>(xs: List<T>, f: fn(T) -> Outcome<U>) -> Outcome<List<U>> {
+  match xs {
+    Empty => Produced { value: Empty }
+    Cons { head: h, tail: t } => match f(h) {
+      Rejected { diagnostic: d } => Rejected { diagnostic: d }
+      Produced { value: u } =>
+        match traverse_outcome(xs: t, f: f) {
+          Rejected { diagnostic: d } => Rejected { diagnostic: d }
+          Produced { value: rest } => Produced { value: Cons { head: u, tail: rest } }
+        }
+    }
+  }
+}
+
+
+fn map_outcome<T, U>(o: Outcome<T>, f: fn(T) -> U) -> Outcome<U> {
+  match o {
+    Rejected { diagnostic: d } => Rejected { diagnostic: d }
+    Produced { value: v } => Produced { value: f(v) }
+  }
+}
+
+
+fn bind_outcome<T, U>(o: Outcome<T>, f: fn(T) -> Outcome<U>) -> Outcome<U> {
+  match o {
+    Rejected { diagnostic: d } => Rejected { diagnostic: d }
+    Produced { value: v } => f(v)
+  }
+}