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
4 changes: 2 additions & 2 deletions dag/gunbc/systemctl_list_units.dag
Original file line number Diff line number Diff line change
Expand Up @@ -54,10 +54,10 @@ fn systemctl_list_units_active_services(instance_glob: NonEmptyStr) -> List<NonE
// accepts a comma-joined --state list in one argv (no --all flag needed, and no second
// ListUnits operation to keep parallel with this one): this is the SAME declared
// operation, called with a different `state` binding, not a new op.
data systemctl_list_units_all_states: String = "active,inactive,failed"
data systemctl_all_unit_states_selector: String = "active,inactive,failed"

fn systemctl_list_units_all_states_local(instance_glob: NonEmptyStr) -> String? {
let result = systemd.Systemctl.ListUnits(pattern: instance_glob, state: systemctl_list_units_all_states)
let result = systemd.Systemctl.ListUnits(pattern: instance_glob, state: systemctl_all_unit_states_selector)
if result.success {
Present { value: result.stdout }
} else {
Expand Down
101 changes: 101 additions & 0 deletions dag/test/claim/duplicate_declaration_wall_witness_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,101 @@
module test.claim.duplicate_declaration_wall_witness

import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }
import std.types { String, Bool }

data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly

// THE WALL THIS ROW GUARDS, and why it exists at the FIXTURE boundary rather than over the corpus.
// A module declaring one name TWICE was accepted with ZERO diagnostics and the SECOND declaration
// silently won: `v1.compiler.env` `symbol_index_insert` is a `map_insert` keyed on the qualified
// name, so the second write REPLACED the first and every reference bound the survivor. Measured by
// execution through our own binary before the wall landed: a module with `fn probe_dup() -> Int { 1 }`
// then `fn probe_dup() -> Int { 2 }` ran its caller to 2, and the one-definition control to 1 --
// same harness, duplication the only variable. `v1.compiler.resolve` `check_duplicate_declarations`
// now refuses it with a blocking `DuplicateDeclaration`.
//
// WHY THE RED IS AUTHORABLE HERE AND NOWHERE ELSE (DESIGN 4b): no `Accepted` module may now carry
// the state, so the refusal is unreachable from the corpus -- but a fixture hands the compiler
// source text, and a compiler's regression probes are invalid programs by definition. Declining to
// author it because the accepted tree cannot hold it would be the specification-without-execution
// failure, not a saving.
//
// THE BOUND THIS ROW EXISTS TO STATE, and it is about the repository's evidence discipline rather
// than about the compiler: where two definitions of one name are semantically EQUIVALENT, no
// behavioural witness can discriminate them whichever one wins. Green-by-execution proves
// BEHAVIOUR and is structurally blind to duplicate AUTHORSHIP. That is why this row is a
// compile-seam refusal and not a runtime probe, and it is why the live specimens this wall's
// landing repaired had passed every witness over them.
//
// WHAT THIS SURFACE OBSERVES, stated so no receipt reads more coverage than it has:
// `compile_dag_rust_emit_check` answers false when the compile carries ANY hard diagnostic, so a
// red row alone does not establish WHICH judgment refused. The discrimination is carried by the
// PAIR: each red fixture and its green control differ by exactly the duplicated declaration and
// nothing else, so a red that survives its control's green is a red caused by the duplication.
// The path measured is source -> `.dag` acceptance through the v1 pipeline to the Rust render
// target, single module. NOT measured here: the interpreter's disposition of the same source, and
// cross-module name collisions, which are a different class (two keys, not one).

fn duplicate_fn_source() -> String {
"module test.claim.duplicate_declaration_wall_duplicate_fn\nimport std.types { Int }\n\nfn which_one() -> Int { 1 }\n\nfn which_one() -> Int { 2 }\n"
}

fn single_fn_source() -> String {
"module test.claim.duplicate_declaration_wall_single_fn\nimport std.types { Int }\n\nfn which_one() -> Int { 1 }\n"
}

// The collision is NOT fn/fn only. A `data` and a `fn` of one name share one symbol-index key, and
// that shape had LIVE exposure on main: `dag/gunbc/systemctl_list_units.dag` declared
// `data systemctl_list_units_all_states: String` and `fn systemctl_list_units_all_states(..)`, so
// the reference intended for the string bound the FUNCTION. Repaired in the same change that
// landed the wall.
fn duplicate_data_and_fn_source() -> String {
"module test.claim.duplicate_declaration_wall_duplicate_kind\nimport std.types { Int }\n\ndata thing: Int = 1\n\nfn thing() -> Int { 2 }\n"
}

fn distinct_data_and_fn_source() -> String {
"module test.claim.duplicate_declaration_wall_distinct_kind\nimport std.types { Int }\n\ndata thing: Int = 1\n\nfn other() -> Int { 2 }\n"
}

// THE DISCRIMINATING REDS.

test fn two_function_declarations_of_one_name_are_refused() -> Bool {
compile_dag_rust_emit_check(
duplicate_fn_source(),
"src/test_claim_duplicate_declaration_wall_duplicate_fn.rs",
[],
[]
) == false
}

test fn a_data_and_a_function_sharing_one_name_are_refused() -> Bool {
compile_dag_rust_emit_check(
duplicate_data_and_fn_source(),
"src/test_claim_duplicate_declaration_wall_duplicate_kind.rs",
[],
[]
) == false
}

// THE POSITIVE CONTROLS. Each is its red's fixture with the duplication removed and nothing else
// changed, so a red above cannot pass by its fixture being broken some other way. Per DESIGN 4b(4)
// these stay enrolled after the wall lands: they are the executing evidence that the rung is real,
// and deleting them would recreate specification-without-execution one rung up.

test fn one_function_declaration_compiles_clean() -> Bool {
compile_dag_rust_emit_check(
single_fn_source(),
"src/test_claim_duplicate_declaration_wall_single_fn.rs",
["which_one"],
[]
)
}

test fn a_data_and_a_function_with_distinct_names_compile_clean() -> Bool {
compile_dag_rust_emit_check(
distinct_data_and_fn_source(),
"src/test_claim_duplicate_declaration_wall_distinct_kind.rs",
["other"],
[]
)
}
19 changes: 19 additions & 0 deletions dag/test/claim/duplicate_definition_binding_probe.dag
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,25 @@ data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree
// `test fn` collides with a plain `fn` of the same name. Each is its own row when someone
// measures it; none is claimed by this one.

// THE WALL LANDED (2026-08-27, this lane). `v1.compiler.resolve` `check_duplicate_declarations`
// folds each module's own item list and emits a blocking `DuplicateDeclaration` on the second
// declaration of one name, so the two rows below assert the behaviour the compiler now has rather
// than the behaviour it lacked. THE ROW STILL DOES NOT EXECUTE HERE: the disposition above is
// unchanged and this site is still `DeclinedLiveTree`, so what flipped is the SUBJECT, not this
// row's reach -- the execution trigger recorded above is still the only thing that retires it.
// The executing evidence for the wall is `duplicate_declaration_wall_witness` in
// `v1.compiler.compiler_tests_rust`, at the fixture boundary; that harness runs LOCALLY only,
// which is stated in the gap-analysis row rather than claimed as CI coverage here.
// WHERE THE WALL SITS vs where this row said it should: at RESOLVE, over each module's item list,
// not at ingestion. It reads nothing outside the module it judges, so the "no corpus walk"
// property that made the class decidable is preserved; what is NOT yet done is the R4 climb the
// row above implies, a keyed declaration roster at ingestion that cannot HOLD two entries for one
// name. That remains this class's next-rung trigger.
// TWO SHAPES THIS ROW STILL DOES NOT MEASURE, and the second had LIVE exposure: a `data` and a
// `fn` sharing one name (the wall refuses it; measured on `dag/gunbc/systemctl_list_units.dag`,
// where a bare reference intended for a `data` String bound the function instead), and the Rust
// emission path. Both are covered by the seed witness, neither by this module.

fn census_of(source: String) -> CompileDiagnosticCensus {
compile_dag_diagnostic_census(source)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -249,7 +249,6 @@ test fn the_listing_banner_is_not_read_as_an_entry() -> Bool {
// It is not written against #8860's variant shape, deliberately: it reads only the population's
// rendered command strings, so it compiles identically before and after that PR and measures the
// one fact the ordering depends on.
data measured_installed_linger_command: String = "/usr/bin/loginctl enable-linger gunbc-automation"

test fn the_modeled_linger_command_is_byte_equal_to_the_line_the_hosts_hold() -> Bool {
any(spark_managed_grant_population, g =>
Expand Down
Loading
Loading