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
2 changes: 1 addition & 1 deletion dag/gunbc/prose_row_frontier.dag
Original file line number Diff line number Diff line change
Expand Up @@ -239,7 +239,7 @@ data prose_row_migration_scope: List<String> = [
"dag/test/claim/state_response_totality_witness_test.dag",
"dag/test/claim/test_module_hygiene_hand_rust_equivalence_witness_test.dag",
"dag/test/claim/tool_pin_witness_test.dag",
"dag/test/claim/long/transport_script_wall_compile_red_test.dag",
"dag/test/claim/transport_script_wall_compile_red_test.dag",
"dag/test/claim/type_ref_hit_ne_bind_measure_witness_test.dag",
"dag/test/claim/type_reference_containment_binding_witness_test.dag",
"dag/test/claim/v1_complexity_capability_census_witness_test.dag",
Expand Down
2 changes: 1 addition & 1 deletion dag/test/claim/compile_diagnostic_census_witness_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

data census_live_tree_note: String = "ReadsLiveTree, and the divergence from the sibling is deliberate. compile_dag_diagnostic_census resolves the synthetic source against build_module_path_index_from_witness_roots, which walks the live tree - so the read is real. dag/test/claim/transport_script_wall_compile_red_test.dag declares SubstrateInputsOnly while calling compile_dag_rust_emit_check, which takes the SAME host path; that row is either a latent mis-declaration or a judgment that the index is substrate, and the falsifier cadence is what would surface it either way. This file does not copy the claim it cannot verify: undeclared is ReadsLiveTree by the fail-closed default and the honest declaration costs only selection-eligibility."
data census_live_tree_note: String = "ReadsLiveTree, and the divergence from the sibling is deliberate. compile_dag_diagnostic_census resolves the synthetic source against build_module_path_index_from_witness_roots, which walks the live tree - so the read is real. RESOLVED 2026-08-19 (FIRSTTOUCH-1, dashboard adhoc-c5b4375f-4cb): dag/test/claim/transport_script_wall_compile_red_test.dag previously declared SubstrateInputsOnly while calling compile_dag_rust_emit_check, which takes the SAME build_module_path_index_from_witness_roots host path as this file; that was flagged here as 'either a latent mis-declaration or a judgment call' pending the falsifier cadence, which is since deleted (2026-08-15 floor cut, DESIGN.md CI section) and never adjudicated it. Tracing the call confirmed it reads the live tree, so it was the mis-declaration, not a judgment call; that file now declares ReadsLiveTree. This file does not copy claims it cannot verify: undeclared is ReadsLiveTree by the fail-closed default and the honest declaration costs only selection-eligibility."

data census_scope_note: String = "WHAT THESE WITNESSES PROVE, and what they do not. They prove the observation SURFACE reports the three facts a Bool discards - which class fired, whether it blocks, and how many times - on the v1-pipeline / Rust-target / synthetic-single-module path, and that a clean source is distinguishable from a refusing one so the harness is not always-refusing. They prove NOTHING about the walls themselves: a wall's own regression control is its migrated probe pair, not this file. BOTH SEVERITY DIRECTIONS HAVE LIVE SPECIMENS, and the way the advisory one was found is worth recording because the first answer was wrong. An earlier pass concluded no advisory specimen could be conjured synthetically: a where-refinement alias, an unlisted-import shape, and an unresolved method on a bare type parameter each either compiled silent or refused BLOCKING. That conclusion was an artifact of the PROBE, not the compiler - and the first diagnosis of why was ALSO wrong, which is the part worth carrying. The initial account blamed the closure: those probes ran through a fixture-only CLI compile with no std in its single source root, so the refinement supposedly never resolved to a refinement. A discriminating control refuted that. Under the full dag + src/v2 pool the where-refinement ALIAS shape (type Tight = String where non_empty) is STILL silent - zero diagnostics with std fully available - while the shape asserted below, a cast to std's refined brand, fires WhereRefinementUnenforced as a counted advisory on the same harness. So the closure was not the discriminator; the probe SHAPE was. A 2x2 pins the real axis, and it is not what either explanation guessed: crossing declaration site (local alias vs std brand - structurally identical declarations, same predicate) against cast subject (literal vs unknown parameter), local+parameter FIRES, local+literal silent, std+parameter FIRES, std+literal silent. Declaration site is irrelevant; the diagnostic names the axis itself - non-literal value at refined position. The original probe cast the literal x, and a literal at a refined position is deliberately EXEMPT, so its silence is CORRECT BEHAVIOUR and it is a dead probe rather than a finding: it looked like it exercised the judgment (it casts, at a fn boundary) while the judgment exempts its exact form. The intermediate guess that its predicate resolves nowhere is also retired - the predicate resolves fine, as local+parameter firing proves. The corpus reading that prompted the recheck: a whole-tree compile carries 1981 where-refinement advisories, so the class was demonstrably reachable and a probe finding none was evidence against the probe. CONSEQUENCE: AcceptedCounted has a producer - the surface does not merely REPRESENT a counted-advisory observation, a probe PRODUCES one. They also do not prove the host EMITS CensusNotRunnable on a real infrastructural failure - the last witness asserts only that the coproduct keeps the two arms distinct, which is the property that lets a caller map could-not-measure to ProbeNotRunnable without guessing; provoking a genuine host panic on demand is not something a synthetic source can do, and asserting it as though it were measured would be the fabrication this corpus exists to count."

Expand Down
51 changes: 0 additions & 51 deletions dag/test/claim/long/transport_script_wall_compile_red_test.dag

This file was deleted.

63 changes: 63 additions & 0 deletions dag/test/claim/transport_script_wall_compile_red_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
module test.claim.transport_script_wall_compile_red

import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree }

data transport_script_wall_compile_red_note: String = "§5.E wall REDs (operator acceptance 2026-07-24): the two documented transport-script fake patterns, reconstructed AS WRITTEN, must FAIL TO COMPILE — not merely fail review. Each fake is compiled as an inline virtual source through compile_dag_rust_emit_check, which returns false on any hard diagnostic; the tests assert refusal (!compile). The construction wall — ShellOnHost.script retyped to the RetainedShellScript RECORD, and the free minter extdeps.shell.exec.transport_script_from_body DELETED — is what makes both fakes non-compiling. The host_language_transport_script lens never caught these (a computed concat is ComputedApplication, deliberately green); only construction closes the class. If either wall is ever loosened (record widened back to String, or the free minter reintroduced), the corresponding fake starts compiling clean, compile_dag_rust_emit_check flips to true, and the RED goes red — the wall's regression alarm."

data firsttouch_1_restoration_note: String = "FIRSTTOUCH-1 (dashboard adhoc-c5b4375f-4cb, 2026-08-19) -- a finding and a disposition correction, NOT a restoration; corrected 2026-08-19 after this note's first version wrongly read a green floor run as evidence the witness now executes cheaply. This module was quarantined out of test.claim.long. and back in, twice, on two different readings of one artifact. First quarantined by #8457's blanket over-budget sweep. RESTORE WAVE A un-quarantined it, then 021d17e6a7 dropped it straight back after observing it cost 1394ms pre-quarantine (docs/plans/measurements/floor-slow-rows-2026-08-17.tsv, CI run ci) but 48963ms in the restore run with nothing about the witness changed -- 35.1x, and the commit named the mechanism without yet fixing it: compile_dag_rust_emit_check_uncached calls build_module_path_index_from_witness_roots (src/v1/stage0/src/cli_run.rs), a THREAD-LOCAL memo keyed on the default source roots -- exactly the module_path_index shared fill of the #8455 ledger (docs/plans/floor-shared-fill-ledger.md). #8470 (7e4871be86, already on this branch's main ancestry) DID fix that exact call site, warming build_module_path_index_from_witness_roots during floor preparation and naming this witness's own two RED rows in its measurement table -- but fixing a cost and being ADMITTED to pay it are two different facts, and this note's first version conflated them.

The module moves out of long. here for a reason independent of cost: its long-home name asserted a quarantine reason (cost) that is no longer the operative one now that live_tree_disposition below is corrected. Carrying a stale reason beside a live one is exactly the drift the long/-versus-module-name split exists to end.

THE DISPOSITION CORRECTION IS THE SUBSTANTIVE CHANGE. live_tree_disposition was declared SubstrateInputsOnly while this witness calls compile_dag_rust_emit_check, which reaches the identical build_module_path_index_from_witness_roots live-tree walk its sibling (compile_diagnostic_census_witness_test.dag) already declares ReadsLiveTree for. That sibling's census_live_tree_note had flagged this as 'either a latent mis-declaration or a judgment call' pending the falsifier cadence -- since deleted (2026-08-15 floor cut) and never adjudicated. SubstrateInputsOnly was the mis-declaration; ReadsLiveTree is declared here honestly, even though it costs admission rather than buying it.

THE FINDING, terminal, not pending: v2.workflow.required_floor's admission test is long_home(module) -> DeclinedLongModule; else reads_live_tree -> DeclinedLiveTree; else Planned (src/v1/stage0/src/cli_run.rs run_required_floor, disposition_rows construction) -- an OR of two independent decline arms, not one quarantine gate. Moving this module out of test.claim.long. does not admit it: it moves the three identities straight from DeclinedLongModule into DeclinedLiveTree. Measured at identity grain -- RequiredFloorDispositionRow, the per-identity receipt that made this decidable at all -- comparing this PR's floor run against a main baseline run at the same head: claims=9686 unchanged in both, declined_long 539->536 (-3), declined_live 763->766 (+3); the exact three identities moved buckets and never became Planned. THIS WITNESS CANNOT BE ADMITTED TO THE REQUIRED FLOOR WHILE IT READS THE LIVE TREE. That is independent of #8470: the first-touch cost fix and the admission question are two separate facts about this module, and fixing the first does not touch the second.

CONSEQUENCE FOR THE COST QUESTION: it cannot be closed by a floor run at all, not now and not after any further first-touch repair, because the witness is never planned into one. A standalone claim run is not a substitute measurement either -- it disables the per-floor-process memo #8470 warms, so it would measure a different, uncached quantity, not this module's floor-fold cost; using it to answer the floor question would be a fourth false reading of the same defect docs/plans/floor-shared-fill-ledger.md exists to stop people repeating. The cost question is therefore an open item with a NAMED BLOCKER -- this witness's own inadmissibility -- not a task the next session should attempt against the floor.

SCALE NOTE, unrelated to this witness's own resolution but recorded where it will be seen: at the same measurement, declined_live=766 vastly outnumbers declined_long=536 (763 vs 539 pre-move). This whole lane -- three restore waves, an attribution pass, a policy cut, a night of argument across six sessions -- has been aimed entirely at the smaller of the two declined populations."

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

// Positive control: a clean shell service source compiles and emits src/wallctl.rs containing the argv-shaped Command invocation, so compile_dag_rust_emit_check returns true. Proves the harness is discriminating — the two false results below are genuine refusals of the fakes, not a harness that always returns false.
fn w_control_clean_shell_service() -> Bool {
compile_dag_rust_emit_check(
"module wallctl\n\nservice shell.Run {\n operation Exec {\n input { script: String }\n output { result: String }\n transport shell { argv: [\"sh\", \"-lc\", \"\{script\}\"] }\n mock_response {\n 0 => \"done\" \"result\"\n }\n }\n}\n",
"src/wallctl.rs",
["Command::new(\"sh\")", ".arg(\"-lc\")"],
[]
)
}

data red_a_note: String = "RED A — the #7064 / vivid-wolf 'build the argv properly, then join it back into a string and feed the realization edge' class. The fake hands a computed String (argv join + \" 2>/dev/null || true\") to retained_shell_script_to_transport, whose parameter is the RetainedShellScript RECORD. A String cannot fill a record position, so infer refuses (hard diagnostic) and the source does not compile. The only sanctioned route is to author a counted RetainedShellScript row (retained_srvn / retained_transport), which forces a reason + dissolve-on."

fn w_red_a_string_join_into_retained_record() -> Bool {
compile_dag_rust_emit_check(
"module wallreda\n\nimport std.types { String }\nimport extdeps.shell.exec { TransportScript }\nimport gunbc.retained_shell_script { retained_shell_script_to_transport }\n\nfn argv_joined() -> String { concat(\"hostname\", concat(\" \", \"-s\")) }\n\nfn fake_join_into_record() -> TransportScript {\n retained_shell_script_to_transport(rss: concat(argv_joined(), \" 2>/dev/null || true\"))\n}\n",
"src/wallreda.rs",
[],
[]
)
}

data red_b_note: String = "RED B — #7064's exact textual pattern: transport_script_from_body(argv_join(...) + \" 2>/dev/null || true\"). The free minter is deleted from extdeps.shell.exec, so the import resolves nothing and the call is unresolved (hard diagnostic) — the source does not compile. Reintroducing the free minter would make this fake compile again and red this control."

fn w_red_b_deleted_free_minter() -> Bool {
compile_dag_rust_emit_check(
"module wallredb\n\nimport std.types { String }\nimport extdeps.shell.exec { TransportScript, transport_script_from_body }\n\nfn argv_joined() -> String { concat(\"hostname\", concat(\" \", \"-s\")) }\n\nfn fake_deleted_minter() -> TransportScript {\n transport_script_from_body(body: concat(argv_joined(), \" 2>/dev/null || true\"))\n}\n",
"src/wallredb.rs",
[],
[]
)
}

test fn wall_control_clean_shell_service_compiles() -> Bool {
w_control_clean_shell_service()
}

test fn wall_red_string_join_into_retained_record_refuses() -> Bool {
!w_red_a_string_join_into_retained_record()
}

test fn wall_red_deleted_free_minter_refuses() -> Bool {
!w_red_b_deleted_free_minter()
}