Skip to content
Merged
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
190 changes: 189 additions & 1 deletion src/v1/stage0/src/coproduct_reflection.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,8 @@ use std::rc::Rc;
use crate::v1_compiler_infer_items::ItemKind;
use crate::v1_interpreter::{InterpContext, InterpError, InterpResult, Value};
use crate::v1_std_core::{
authored_name_at, field_node_type_expr, inferred_to_node, Connective, Node,
authored_name_at, expr_var_name_at, field_node_type_expr, inferred_to_node, param_node_name_at,
Connective, ExprData, NewlineIndex, Node, VarBindingKind,
};

pub(crate) const NULLARY_PAYLOAD_TYPE_NAME: &str = "coproduct_nullary_payload";
Expand Down Expand Up @@ -492,6 +493,193 @@ pub fn eval_concept_decl_facts_live(
Ok(crate::v1_interpreter::list_value(rows))
}

fn edge_positional(ctx: &InterpContext, target: Value) -> Value {
Value::Record {
type_name: ctx.sym("Edge"),
fields: Rc::new(HashMap::from([
(
ctx.sym("label"),
Value::Variant {
type_name: ctx.sym("EdgeLabel"),
variant_name: ctx.sym("Positional"),
fields: Rc::new(HashMap::new()),
},
),
(ctx.sym("target"), target),
])),
}
}

fn atom_identity_node(ctx: &InterpContext, identity: &str) -> Value {
node_record(
ctx,
node_kind_type_node(ctx, atom_connective_variant(ctx, identity)),
vec![],
)
}

fn node_authored_name(node: &Rc<Node>, si: &Rc<HashMap<String, Rc<NewlineIndex>>>) -> String {
if !node.name.is_empty() {
node.name.clone()
} else {
expr_var_name_at(node.clone(), si.clone())
}
}

// Does this node REFERENCE a declared parameter `name`? Two body forms reference a value
// parameter: an `ExprVar` value read (`x`) -- resolved to a `LocalValueBinding`, so a
// `FunctionValueBinding` global or `VariantValueBinding` constructor sharing the name is
// excluded; and an `ExprCall` whose callee IS the parameter (a fn-valued param applied:
// `predicate(x)`) -- the callee is the call node's own name, not a child, so it is invisible
// to a children-only walk. Both are genuine uses of a value parameter.
fn node_references_param(node: &Rc<Node>, name: &str, param_names: &[String]) -> bool {
if name.is_empty() || !param_names.iter().any(|p| p.as_str() == name) {
return false;
}
match node.expr_data.as_ref() {
ExprData::ExprVar {
binding_kind: Some(bk),
} => {
matches!(bk.as_ref(), VarBindingKind::LocalValueBinding)
}
ExprData::ExprCall { .. } => true,
_ => false,
}
}

// Project a fn body's internal expression tree onto a substrate Node skeleton: each node
// becomes a neutral `Conj` container whose positional children are the marshaled
// sub-expressions, and a node that references a declared parameter additionally carries an
// identity-bearing `Atom` leaf -- byte-identical to the declared-input atom
// `eval_fn_arrow_decl_facts_live` emits, so `v2.lens.wiring_liveness` matches it under Node
// equality. Identity lives ONLY on genuine parameter-reference sites, so a declared
// parameter is structurally reachable from the body output iff it is genuinely used.
// (Residue: a `let`/lambda local, or a global fn called as `name(..)`, that shadows a
// parameter name; see the lens construction_justification.)
fn marshal_fn_body_skeleton(
ctx: &InterpContext,
node: &Rc<Node>,
param_names: &[String],
si: &Rc<HashMap<String, Rc<NewlineIndex>>>,
) -> Value {
let name = node_authored_name(node, si);
let mut edges: Vec<Value> = Vec::with_capacity(node.children.len() + 1);
if node_references_param(node, &name, param_names) {
edges.push(edge_positional(ctx, atom_identity_node(ctx, &name)));
}
for child in node.children.iter() {
edges.push(edge_positional(
ctx,
marshal_fn_body_skeleton(ctx, child, param_names, si),
));
}
if let Some(inner) = node.body.as_ref() {
edges.push(edge_positional(
ctx,
marshal_fn_body_skeleton(ctx, inner, param_names, si),
));
}
node_record(
ctx,
node_kind_type_node(ctx, nullary_connective_variant(ctx, "Conj")),
edges,
)
}

// A generic type parameter (`<T>`) and a value parameter (`(xs: List<T>)`) both land in the
// runtime item's `params` (parser: `all_params = concat(type_params, value_params)`). They
// are NOT value inputs and never appear as body value-expressions, so they must be excluded
// from the wiring check. A type parameter is built as `make_param_node(name,
// leaf_type_node(name), ..)` -- its sole type-expr child is a leaf named after the parameter
// itself (`T : T`) -- whereas a value parameter's type-expr names a different type
// (`xs : List`). So: a parameter is a type parameter iff its first child's authored name
// equals its own.
fn param_is_type_param(p: &Rc<Node>, si: &Rc<HashMap<String, Rc<NewlineIndex>>>) -> bool {
let pname = authored_name_at(si.clone(), p.clone());
if pname.is_empty() {
return false;
}
match p.children.first() {
Some(child0) => authored_name_at(si.clone(), child0.clone()) == pname,
None => false,
}
}

fn fn_arrow_param_record(ctx: &InterpContext, param_name: &str) -> Value {
Value::Record {
type_name: ctx.sym("FnArrowParam"),
fields: Rc::new(HashMap::from([
(ctx.sym("name"), Value::Str(param_name.to_string())),
(ctx.sym("node"), atom_identity_node(ctx, param_name)),
])),
}
}

// Corpus-wide fn/arrow reflection: the gunbc#5364 widen trigger named in
// `v2.lens.wiring_liveness`'s construction_justification. Sibling of
// `eval_concept_decl_facts_live` (which filters to `ItemKind::TypeItem`); this yields
// one `FnArrowDecl` per declared function across every loaded module -- the body
// projected to a reachability skeleton (`output`) plus its declared parameter atoms
// (`params`) -- so the wiring lens folds over REAL fn params corpus-wide, not synthetic
// arrows. Host SOURCE half; dissolves with `concept_decl_facts_live` on the same #5364
// corpus-as-node accessor.
pub fn eval_fn_arrow_decl_facts_live(
ctx: &InterpContext,
_args: &[(Option<String>, Value)],
) -> InterpResult<Value> {
let si = ctx.source_indices();
let mut rows: Vec<Value> = Vec::new();
for module in ctx.modules.iter() {
for item in module.items.iter() {
let name = authored_name_at(si.clone(), item.clone());
if name.is_empty() {
continue;
}
let info = module
.item_registry
.get(&name)
.or_else(|| module.item_registry.get(&item.name));
let Some(info) = info else { continue };
if info.kind != ItemKind::FnItem && info.kind != ItemKind::FuncItem {
continue;
}
let Some(body) = item.body.as_ref() else {
continue;
};
let mut param_names: Vec<String> = Vec::new();
for p in item.params.iter() {
if param_is_type_param(p, &si) {
continue;
}
let pn = param_node_name_at(p.clone(), si.clone());
// A `_`-prefixed name is the established declared-inert convention (e.g.
// node.dag `step: fn(acc, _edge, sub)`): the author has declared the input
// genuinely irrelevant, so it is not a dead wire (plan section 4). Skip it.
if pn.is_empty() || pn.starts_with('_') || param_names.iter().any(|q| q == &pn) {
continue;
}
param_names.push(pn);
}
let output = marshal_fn_body_skeleton(ctx, body, &param_names, &si);
let params: Vec<Value> = param_names
.iter()
.map(|pn| fn_arrow_param_record(ctx, pn))
.collect();
let qualified_name = logical_qualified_name(&info.module_name, &name);
rows.push(Value::Record {
type_name: ctx.sym("FnArrowDecl"),
fields: Rc::new(HashMap::from([
(ctx.sym("qualified_name"), Value::Str(qualified_name)),
(ctx.sym("name"), Value::Str(name.clone())),
(ctx.sym("output"), output),
(ctx.sym("params"), crate::v1_interpreter::list_value(params)),
])),
});
}
}
Ok(crate::v1_interpreter::list_value(rows))
}

pub fn eval_syntactic_coproduct_arm_keys(
ctx: &InterpContext,
args: &[(Option<String>, Value)],
Expand Down
24 changes: 24 additions & 0 deletions src/v1/stage0/src/v1_interpreter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2073,6 +2073,8 @@ pub(crate) const STD_NODE_QUERY_BRIDGE_FNS: &[&str] = &["coproduct_nullary_inhab

pub(crate) const STD_CONCEPT_INDEX_BRIDGE_FNS: &[&str] = &["concept_decl_facts_live"];

pub(crate) const STD_FN_INDEX_BRIDGE_FNS: &[&str] = &["fn_arrow_decl_facts_live"];

pub fn std_node_bridge_fn_names() -> &'static [&'static str] {
STD_NODE_BRIDGE_FNS
}
Expand All @@ -2085,6 +2087,10 @@ pub fn std_concept_index_bridge_fn_names() -> &'static [&'static str] {
STD_CONCEPT_INDEX_BRIDGE_FNS
}

pub fn std_fn_index_bridge_fn_names() -> &'static [&'static str] {
STD_FN_INDEX_BRIDGE_FNS
}

fn is_v4_std_node_bridge_call(ctx: &InterpContext, func_name: &str) -> bool {
if !STD_NODE_BRIDGE_FNS.contains(&func_name) {
return false;
Expand Down Expand Up @@ -2112,6 +2118,15 @@ fn is_v4_std_concept_index_bridge_call(ctx: &InterpContext, func_name: &str) ->
.is_some_and(|info| info.module_name == "v2.std.concept_index")
}

fn is_v4_std_fn_index_bridge_call(ctx: &InterpContext, func_name: &str) -> bool {
if !STD_FN_INDEX_BRIDGE_FNS.contains(&func_name) {
return false;
}
ctx.item_registry
.get(func_name)
.is_some_and(|info| info.module_name == "v2.std.fn_index")
}

fn is_v4_std_lexing_bridge_call(ctx: &InterpContext, func_name: &str) -> bool {
if !STD_LEXING_BRIDGE_FNS.contains(&func_name) {
return false;
Expand Down Expand Up @@ -2175,6 +2190,15 @@ fn eval_call(node: &Rc<Node>, env: &Rc<Env>, ctx: &InterpContext) -> InterpResul
};
}

if is_v4_std_fn_index_bridge_call(ctx, &func_name) {
return match func_name.as_str() {
"fn_arrow_decl_facts_live" => {
crate::coproduct_reflection::eval_fn_arrow_decl_facts_live(ctx, &args)
}
_ => unreachable!("fn_index bridge fn set mismatch"),
};
}

match func_name.as_str() {
"fold_list" => return eval_fold_list_native(&args, env, ctx),
"fold_list_right" => return eval_fold_list_right_native(&args, env, ctx),
Expand Down
10 changes: 10 additions & 0 deletions src/v1/tests/src/coproduct_reflection_conformance_test.rs
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,12 @@ fn coproduct_reflection_std_node_bridge_fns_are_intercept_wired() {
"eval_call intercept must wire v2.std.concept_index bridge `{name}`"
);
}
for name in v1_interpreter::std_fn_index_bridge_fn_names() {
assert!(
source.contains(&format!("\"{name}\" =>")),
"eval_call intercept must wire v2.std.fn_index bridge `{name}`"
);
}
assert!(
source.contains("is_v4_std_node_bridge_call"),
"eval_call must gate v2.std.node bridge dispatch"
Expand All @@ -101,6 +107,10 @@ fn coproduct_reflection_std_node_bridge_fns_are_intercept_wired() {
source.contains("is_v4_std_concept_index_bridge_call"),
"eval_call must gate v2.std.concept_index bridge dispatch"
);
assert!(
source.contains("is_v4_std_fn_index_bridge_call"),
"eval_call must gate v2.std.fn_index bridge dispatch"
);
}

#[test]
Expand Down
56 changes: 52 additions & 4 deletions src/v2/lens/wiring_liveness.dag
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,13 @@ module v2.lens.wiring_liveness

import v2.lens.common.construction_justification { ConstructionJustification, WallAfterGrounding }
import std.disposition { RealizationDispatch }
import v2.std.algebra { contains, length, list_snoc_item }
import v2.std.algebra { contains, length, list_append, list_snoc_item }
import v2.std.collection { List }
import v2.std.dependency { DependencyView, dependency_lens }
import v2.std.dependency { DependencyView, dependency_lens, ready_set }
import v2.std.fn_index { FnArrowDecl, FnArrowParam, fn_arrow_decl_facts_live }
import v2.std.logic { Bool }
import v2.std.node { Node }
import v2.std.node { Node, Symbol }
import v2.std.text { String }

type WiringRelation {
output: Node
Expand Down Expand Up @@ -92,7 +94,53 @@ fn wiring_input_is_wired(output: Node, declared_input: Node) -> Bool {
)
}


type WiringDeadWire {
fn_qualified_name: String
param: Symbol
}

fn wiring_output_reachable_nodes(output: Node) -> List<Node> {
ready_set(graph_node: output)
}

fn wiring_param_reaches_output(reachable: List<Node>, declared_input: Node) -> Bool {
wiring_reach_contains(reached: reachable, n: declared_input)
}

fn wiring_fn_dead_wires(decl: FnArrowDecl) -> List<WiringDeadWire> {
let reachable = wiring_output_reachable_nodes(output: decl.output)
fold(decl.params, init: [], f: fn(acc, p) {
if wiring_param_reaches_output(reachable: reachable, declared_input: p.node) {
acc
} else {
list_snoc_item(
xs: acc,
item: WiringDeadWire { fn_qualified_name: decl.qualified_name, param: p.name }
)
}
})
}

fn wiring_dead_wires_over(decls: List<FnArrowDecl>) -> List<WiringDeadWire> {
fold(decls, init: [], f: fn(acc, decl) {
list_append(left: acc, right: wiring_fn_dead_wires(decl: decl))
})
}

fn wiring_liveness_corpus_dead_wires() -> List<WiringDeadWire> {
wiring_dead_wires_over(decls: fn_arrow_decl_facts_live())
}

fn wiring_liveness_corpus_dead_wire_count() -> Int {
length(xs: wiring_liveness_corpus_dead_wires())
}

fn wiring_liveness_corpus_is_clean() -> Bool {
wiring_liveness_corpus_dead_wire_count() == 0
}

data construction_justification: ConstructionJustification = ConstructionJustification {
class: WallAfterGrounding { dissolves_to: RealizationDispatch },
rationale: "Wiring-liveness is the cache-purity perturbation oracle read backwards: purity asks same-input-same-output (a declared input absent from the cache key is impure); liveness asks different-input-different-output (a declared input with no structural path to the output it feeds is a dead wire). One kernel, two readings -- this lens reuses std.dependency DependencyView/dependency_lens as the dependence carrier (no new dependence type minted) and decides reachability of a declared input from its output over that graph. It is NOT the unused_parameters reference-count: that asks referenced-at-least-once; this asks transitive-path-to-output, which goes RED when an input is referenced only inside structure that itself never reaches the output. HONEST BOUNDARY (DESIGN 5/6): this is the COMPILE-TIME wall and covers only .dag-modeled / reflectable structure (type declarations via resolve_type_node and synthetic-or-real Node trees via dependency_lens). The motivating GCP IAM auth_input bug lives in the Rust-seed resolve_auth realization, which is OPAQUE to compile-time reflection -- that is the wave-2 opaque-realization perturbation witness, not this slice. The corpus also has NO fn/arrow reflection (resolve_type_node + concept_decl_facts_live yield only ItemKind::TypeItem), so a corpus-wide scan of real fn params is also opaque today. Grounding authority: realization self-host (DESIGN 5/7) bringing resolve_auth into .dag, plus gunbc#5364 (.dag compile-graph / fn reflection) letting the wall scan real fn bodies. Dissolves on: every input->output realization being .dag-reflectable, at which point a declared input with no path to its output is unwritable by construction and this lens's residue is empty."
rationale: "Wiring-liveness is the cache-purity perturbation oracle read backwards: purity asks same-input-same-output (a declared input absent from the cache key is impure); liveness asks different-input-different-output (a declared input with no structural path to the output it feeds is a dead wire). One kernel, two readings -- this lens reuses std.dependency DependencyView/dependency_lens (and ready_set) as the dependence carrier (no new dependence type minted) and decides reachability of a declared input from its output over that graph. It is NOT the unused_parameters reference-count: that asks referenced-at-least-once; this asks transitive-path-to-output, which goes RED when an input is referenced only inside structure that itself never reaches the output. WAVE-2(b) CORPUS COVERAGE: the gunbc#5364 widen trigger named below is now consumed -- v2.std.fn_index.fn_arrow_decl_facts_live (host SOURCE, sibling of concept_decl_facts_live but ItemKind::FnItem/FuncItem) yields one FnArrowDecl per declared fn across every loaded module: the body projected to a reachability skeleton (parameter references become identity Atom leaves, all else neutral Conj containers) plus its declared parameter atoms. wiring_liveness_corpus_is_clean folds the wave-1 reachability over every REAL fn param corpus-wide (not synthetic arrows) and fails the floor on any declared input with no path to its output. HONEST BOUNDARY (DESIGN 5/6): (1) the motivating GCP IAM auth_input bug lives in the Rust-seed resolve_auth realization, OPAQUE to compile-time reflection -- the wave-2 opaque-realization perturbation witness, not this slice. (2) Over a pure expression body the containment-reachable set equals the referenced set, so for fns this wall coincides in result with unused-parameter detection while remaining the transitive-path mechanism (the shared dependence reachability, not a per-edge BindsTo count); the genuine transitive residue (a param referenced only inside a dead let RHS) needs typed data-edges directed at the return, a named follow-on. (3) Skeleton identity lives only on genuine parameter-reference sites (ExprVar LocalValueBinding reads and ExprCall param-callee applications), so type-parameters, global callees, constructors and field-names cannot mask a dead wire -- the lone fail-open is a let/lambda local, or a same-named global fn call, that shadows a parameter name. (4) A legitimately-irrelevant input (e.g. a NodeFold step's ignored edge) is DECLARED inert by the established `_`-prefix convention (node.dag `step: fn(acc, _edge, sub)`); fn_arrow_decl_facts_live skips `_`-prefixed params, so declaring-inert resolves the diagnostic without a false RED (plan section 4) while a normally-named dead param still fails the floor. Grounding authority: realization self-host (DESIGN 5/7) bringing resolve_auth into .dag; gunbc#5364 (.dag compile-graph corpus-as-node accessor) folds fn_arrow_decl_facts_live's host SOURCE half into a pure .dag walk. Dissolves on: every input->output realization being .dag-reflectable AND the dead-let typed-data-edge residue grounded, at which point a declared input with no path to its output is unwritable by construction and this lens's residue is empty."
}
Loading