Skip to content
Closed
Show file tree
Hide file tree
Changes from all 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
62 changes: 62 additions & 0 deletions src/v2/lens/wiring_liveness.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,62 @@
module v2.lens.wiring_liveness

import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
import std.disposition { RealizationDispatch }
import v2.std.algebra { any, list_snoc_item }
import v2.std.collection { List }
import v2.std.dependency { DependencyView }
import v2.std.logic { Bool }
import v2.std.node { Node }

type WiringLivenessFact {
input: Node
output: Node
wired: Bool
}

fn node_in_list(xs: List<Node>, n: Node) -> Bool {
any(xs: xs, predicate: fn(x) { x == n })
}

fn reach_step(deps: List<DependencyView>, reached: List<Node>) -> List<Node> {
fold(deps, init: reached, f: fn(acc, dep) {
if node_in_list(xs: acc, n: dep.source) {
if node_in_list(xs: acc, n: dep.dependent) {
acc
} else {
list_snoc_item(xs: acc, item: dep.dependent)
}
} else {
acc
}
})
}

fn reachable_from(deps: List<DependencyView>, from: Node) -> List<Node> {
fold(deps, init: [from], f: fn(acc, _dep) { reach_step(deps: deps, reached: acc) })
}

fn reaches(deps: List<DependencyView>, from: Node, to: Node) -> Bool {
node_in_list(xs: reachable_from(deps: deps, from: from), n: to)
}

fn input_is_wired(deps: List<DependencyView>, input: Node, output: Node) -> Bool {
reaches(deps: deps, from: input, to: output)
}

fn wiring_liveness_fact(deps: List<DependencyView>, input: Node, output: Node) -> WiringLivenessFact {
WiringLivenessFact {
input: input,
output: output,
wired: input_is_wired(deps: deps, input: input, output: output)
}
}

fn wiring_liveness_dead_wire(fact: WiringLivenessFact) -> Bool {
!fact.wired
}

data construction_justification: ConstructionJustification = ConstructionJustification {
class: WallAfterGrounding { dissolves_to: RealizationDispatch },
rationale: "Wiring-liveness lens wave 1 (docs/plans/wiring-liveness-preflight.md S2/S3a-lens, DESIGN S5/S6). A declared input is WIRED iff it influences the observable output it is declared to feed; the decidable construction-side form is static dataflow reachability over the Node DAG: a declared input with no structural path to an output it feeds is unwired, caught without running anything. This is the cache-purity oracle read backwards (purity = same input -> same output; liveness = different input -> different output), two readings of the one dependence relation already carried by v2.std.dependency (DependencyView) -- this lens reuses that authority rather than re-coining a dependence concept (S2-horizontal, S3). Wave 1 lands the dependence carrier (WiringLivenessFact) + the transitive-reachability decision over a DependencyView edge set, with a discriminating floor witness; it does not yet sweep the live corpus because the motivating fork (the auth_input REST realization) is a Rust seed opaque to .dag reflection today (plan S4 honest boundary), so the static-reach wall cannot see into it until that realization self-hosts. Grounding authority: the realization loop self-hosting each input->output relation into .dag (RealizationDispatch), at which point this carrier's reachability decision runs over the live corpus and a declared input wired into nothing becomes a compile diagnostic that fails the floor (plan item 2). Dissolves on: the static-reach lens covers every .dag-modeled input->output relation -- the wiring-liveness lens then walls any dead wire by construction"
}
55 changes: 55 additions & 0 deletions src/v2/lens/wiring_liveness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,55 @@
module v2.test.lens_wiring_liveness.wiring_liveness_test

import v2.std.dependency { DependencyView, DataDependsOn }
import v2.std.logic { Bool }
import v2.std.node { Node }
import v2.lens.wiring_liveness {
WiringLivenessFact,
input_is_wired,
wiring_liveness_fact,
wiring_liveness_dead_wire
}
import v2.test.lens_common.infer_fixture { claim_atom_node }

fn wl_input() -> Node { claim_atom_node(s: ^wiring_liveness_input) }
fn wl_mid() -> Node { claim_atom_node(s: ^wiring_liveness_mid) }
fn wl_output() -> Node { claim_atom_node(s: ^wiring_liveness_output) }
fn wl_orphan() -> Node { claim_atom_node(s: ^wiring_liveness_orphan) }

fn dep(source: Node, dependent: Node) -> DependencyView {
DependencyView {
source: source,
dependent: dependent,
kind: DataDependsOn,
usage_site: dependent
}
}

fn wired_graph() -> List<DependencyView> {
[
dep(source: wl_input(), dependent: wl_mid()),
dep(source: wl_mid(), dependent: wl_output())
]
}

fn dead_graph() -> List<DependencyView> {
[
dep(source: wl_input(), dependent: wl_orphan()),
dep(source: wl_mid(), dependent: wl_output())
]
}

test fn wiring_liveness_live_wire_is_wired() -> Bool {
return input_is_wired(deps: wired_graph(), input: wl_input(), output: wl_output())
}

test fn wiring_liveness_dead_wire_is_flagged() -> Bool {
return wiring_liveness_dead_wire(
fact: wiring_liveness_fact(deps: dead_graph(), input: wl_input(), output: wl_output())
)
}

test fn wiring_liveness_fact_carries_dead_verdict() -> Bool {
let fact = wiring_liveness_fact(deps: dead_graph(), input: wl_input(), output: wl_output())
return !fact.wired
}