affected-set completeness: model the repo-process universe (incl. meta-processes) by node_query reflection

src/v2/lens/affected_set.dag

@@ -62,6 +62,7 @@ import v2.std.node {
   SyntheticOccurrence
 }
 import v2.std.witness { Holds, Witness }
+import v2.std.node_query { coproduct_arm_keys }
 import v2.lens.application { AncestorFrame, AncestorWalk, collect_ancestor_frames, find_child_by_name, subterm_at, substitute_at }
 
 
@@ -1417,3 +1418,116 @@ fn affected_set(dag: Dag, diff: Diff) -> Witness<ReExecFrontier> {
     diff: diff
   )
 }
+
+
+// ─────────────────────────────────────────────────────────────────────────────
+// Repo-process universe — the COMPLETENESS half (testgen-oracle.md §4.4).
+//
+// Everything above reasons over one `Dag = Node` and its dependency closure. But the set
+// of processes a change may invalidate is wider than one Dag's nodes: the CI gates, the
+// analysis lenses, AND the META-processes that operate on processes (this affected-set
+// lens, testgen, the CI scheduler/floor-runner). A process the universe OMITS is a blind
+// spot — a change to it never re-runs what it covers, so CI is green-but-broken (false
+// confidence). DESIGN §5: an incomplete universe is a fail-open silent-wrong-answer, so the
+// universe is built by CONSTRUCTION — reflected from declared coproducts via v2.std.node_query
+// (a new process is an *arm*, picked up automatically; no producer-local roster that can
+// silently omit one) — and any declared process kind without a reflected producer fails
+// CLOSED to UniverseIncomplete. Honesty boundary (DESIGN §5, the "never" trap): completeness
+// is over *declared* process coproducts; discovering an *undeclared* process (a new lens file
+// nobody registered as an arm) is the host-filesystem-scan residue, left for the Lane-3a
+// whole-tree producer — it is not claimed complete here.
+//
+// Selection-as-CI-gate stays shelved (0-min shadow, testgen-oracle.md §3): this models the
+// universe for completeness; it does NOT gate floor selection.
+
+// The categories of repo process the affected-set universe must cover. Each arm has a
+// reflected producer below; completeness = every arm covered (else UniverseIncomplete).
+type RepoProcessKind
+  = CiGateProcess     // a gunbc.ci_spec Gate — reflected from coproduct_arm_keys(^Gate)
+  | MetaProcessRole   // a process-over-processes — reflected from coproduct_arm_keys(^MetaProcessKind)
+
+
+// The meta-process roster — processes whose SUBJECT is other processes. Omitting one is the
+// sharpest blind spot (a change to the scheduler that never re-runs the floor = false green),
+// so it is a reflected coproduct (a new meta-process is an arm) — never a list inside a producer.
+type MetaProcessKind
+  = AffectedSetLens   // src/v2/lens/affected_set.dag — THIS lens (the universe is reflexive: not a self-blind-spot)
+  | TestgenLens       // src/v2/lens/testgen.dag — generates conformance witnesses from declared structure
+  | CiScheduler       // src/v2/workflow/ci_floor_plan.dag — derives floor batches from gunbc.ci_spec
+  | FloorRunner       // src/v2/workflow/affected_set_floor_runner.dag — per-witness node-frontier skip policy
+
+
+type RepoProcess {
+  kind: RepoProcessKind
+  identity: Symbol
+}
+
+
+// Fail-closed universe carrier (DESIGN §5): a declared kind with no reflected producer is
+// UniverseIncomplete, never a silently-shorter process list.
+type RepoProcessUniverse
+  = UniverseComplete { processes: List<RepoProcess> }
+  | UniverseIncomplete { uncovered_kind: Symbol, reason: FailClosedReason }
+
+
+data affected_set_reflect_gate_type: Symbol = ^Gate
+data affected_set_reflect_meta_process_kind_type: Symbol = ^MetaProcessKind
+data affected_set_reflect_repo_process_kind_type: Symbol = ^RepoProcessKind
+
+
+// Gate processes: one RepoProcess per reflected Gate arm — complete by construction (a new
+// Gate arm flows in automatically; no producer-local roster to drift). DESIGN §2-horizontal.
+fn ci_gate_processes() -> List<RepoProcess> {
+  fold(coproduct_arm_keys(type_name: affected_set_reflect_gate_type), init: [], f: fn(acc, key) {
+    list_snoc_item(xs: acc, item: RepoProcess { kind: CiGateProcess, identity: key })
+  })
+}
+
+
+// Meta-processes: one RepoProcess per reflected MetaProcessKind arm — same construction.
+fn meta_processes() -> List<RepoProcess> {
+  fold(coproduct_arm_keys(type_name: affected_set_reflect_meta_process_kind_type), init: [], f: fn(acc, key) {
+    list_snoc_item(xs: acc, item: RepoProcess { kind: MetaProcessRole, identity: key })
+  })
+}
+
+
+fn universe_has_process_of_kind(processes: List<RepoProcess>, kind_key: Symbol) -> Bool {
+  fold(processes, init: false, f: fn(acc, p) {
+    acc || (discriminant(v: p.kind) == kind_key)
+  })
+}
+
+
+// Coverage fold over every reflected RepoProcessKind arm: a kind with no contributing process
+// fails CLOSED (the declared category whose enumeration is missing IS the blind spot).
+fn repo_process_universe_from(processes: List<RepoProcess>) -> RepoProcessUniverse {
+  fold(
+    coproduct_arm_keys(type_name: affected_set_reflect_repo_process_kind_type),
+    init: UniverseComplete { processes: processes },
+    f: fn(acc, kind_key) {
+      match acc {
+        UniverseIncomplete { uncovered_kind: k, reason: r } =>
+          UniverseIncomplete { uncovered_kind: k, reason: r }
+        UniverseComplete { processes: ps } =>
+          if universe_has_process_of_kind(processes: ps, kind_key: kind_key) {
+            UniverseComplete { processes: ps }
+          } else {
+            UniverseIncomplete {
+              uncovered_kind: kind_key,
+              reason: ReasonSymbol { reason: ^affected_set_reason_repo_process_universe_kind_uncovered }
+            }
+          }
+      }
+    }
+  )
+}
+
+
+// Canonical universe: the reflected union of every process producer. Complete by construction
+// over declared coproducts; the reflexive `AffectedSetLens` arm closes the meta self-blind-spot.
+fn repo_process_universe() -> RepoProcessUniverse {
+  repo_process_universe_from(
+    processes: list_append(left: ci_gate_processes(), right: meta_processes())
+  )
+}

src/v2/test/claim/affected_set_universe_test.dag

@@ -0,0 +1,92 @@
+// src/v2/test/claim/affected_set_universe_test.dag
+//
+// Discriminating witnesses for the repo-process-universe COMPLETENESS model
+// (v2.lens.affected_set, testgen-oracle.md §4.4). Proves the universe is reflected from
+// declared coproducts (so nothing declared is a blind spot) and that the completeness check
+// fails CLOSED on an omitted kind (DESIGN §5) rather than vacuously passing.
+//
+// Lives under src/v2/test/claim (the witness floor discovers `test fn` in `*_test.dag`); it
+// imports gunbc.ci_spec for the INDEPENDENT gate reference (gunbc_ci_gates), mirroring
+// ci_spec_witness_test — the floor loads both source-roots, so the cross-tree import resolves.
+
+module v2.test.claim.affected_set_universe
+
+
+import v2.std.logic { Bool }
+import v2.std.collection { List }
+import v2.std.node { Symbol }
+import v2.std.algebra { bag_eq, list_snoc_item }
+import v2.lens.affected_set {
+  RepoProcess,
+  RepoProcessUniverse,
+  UniverseComplete,
+  UniverseIncomplete,
+  ci_gate_processes,
+  meta_processes,
+  repo_process_universe,
+  repo_process_universe_from
+}
+import gunbc.ci_spec { Gate, gunbc_ci_gates }
+
+
+fn symbol_eq(a: Symbol, b: Symbol) -> Bool {
+  a == b
+}
+
+
+fn process_identities(ps: List<RepoProcess>) -> List<Symbol> {
+  fold(ps, init: [], f: fn(acc, p) { list_snoc_item(xs: acc, item: p.identity) })
+}
+
+
+fn gate_discriminants(gates: List<Gate>) -> List<Symbol> {
+  fold(gates, init: [], f: fn(acc, g) { list_snoc_item(xs: acc, item: discriminant(v: g)) })
+}
+
+
+fn identity_in(ps: List<RepoProcess>, sym: Symbol) -> Bool {
+  fold(ps, init: false, f: fn(acc, p) { acc || (p.identity == sym) })
+}
+
+
+// Anti-drift: the universe's CI-gate processes are EXACTLY the declared gate roster (the
+// independent reference `gunbc_ci_gates`, not a re-reflection of the same arm-key list), so a
+// gate dropped from the universe goes RED. Mirrors ci_spec_witness's roster↔arm-keys proof,
+// lifted to the RepoProcess wrapping.
+test fn affected_set_universe_gate_processes_match_declared_gates() -> Bool {
+  bag_eq(
+    xs: process_identities(ps: ci_gate_processes()),
+    ys: gate_discriminants(gates: gunbc_ci_gates),
+    eq: symbol_eq
+  )
+}
+
+
+// Meta-completeness: the affected-set lens (and testgen) ARE in their own universe — the lens
+// is not a self-blind-spot — and a bogus role is ABSENT (proves the membership check is sharp,
+// not a vacuous always-true).
+test fn affected_set_universe_includes_meta_self() -> Bool {
+  identity_in(ps: meta_processes(), sym: ^AffectedSetLens)
+    && identity_in(ps: meta_processes(), sym: ^TestgenLens)
+    && !identity_in(ps: meta_processes(), sym: ^NotARealMetaProcess)
+}
+
+
+// Completeness: the full reflected universe covers every declared RepoProcessKind arm.
+test fn affected_set_universe_is_complete() -> Bool {
+  match repo_process_universe() {
+    UniverseComplete { processes: _ } => true
+    UniverseIncomplete { uncovered_kind: _, reason: _ } => false
+  }
+}
+
+
+// Discrimination — the completeness check is NOT vacuous: a universe carrying only the gate
+// processes (meta-processes omitted) fails CLOSED to UniverseIncomplete, naming the uncovered
+// kind ^MetaProcessRole. This proves an omitted process category is CAUGHT, not assumed green.
+test fn affected_set_universe_incomplete_fails_closed() -> Bool {
+  match repo_process_universe_from(processes: ci_gate_processes()) {
+    UniverseComplete { processes: _ } => false
+    UniverseIncomplete { uncovered_kind: k, reason: _ } => k == ^MetaProcessRole
+  }
+}