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
106 changes: 106 additions & 0 deletions dag/test/claim/compile_accepted_unevaluable_program_control_test.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,106 @@
module test.claim.compile_accepted_unevaluable_program_control

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

// WHY THIS FILE EXISTS. Required-floor run 32633501354 (main, head 907f19c2cc) reported
// `known_red_runtime_errored=164`: 164 identities the compiler ACCEPTED and the interpreter could
// not evaluate. That counter is the class's only observer, and it goes to zero as the 164 are
// repaired — one lane is already repairing 21 of them. The specimens are being deleted, so the
// evidence has to stop being the specimens.
//
// The partition of the 164, its producer, and the per-identity rows are
// docs/plans/receipts/floor-runtime-error-partition-2026-08-23/. Read it before adding a row here:
// it also records, with the measurements behind it, which families CANNOT be fixtured on this
// surface and why, so that this file is not mistaken for coverage of the whole 164.
//
// WHAT IS FIXTURED HERE, and it is one family of the five: HOST-PRIMITIVE-CONTRACT, 11 of the 164.
// A host primitive's argument list is not checked at compile in ANY direction — measured on this
// same surface at this head: two arguments, zero arguments, and one argument of the wrong type all
// compile clean, and `atom_identity_hash`'s host arm then refuses each at evaluation with
// `requires exactly one string argument`. The refusal text is the host's own, which is what makes
// these three REDs claims about a wall rather than guesses about intent.
//
// WHAT IS NOT FIXTURED HERE, stated so its absence is not read as its non-existence:
// REFERENCE-UNAVAILABLE, 149 of the 164 and the dominant family. Both `.dag`-callable
// compile-observation surfaces REFUSE its shape — `compile_dag_rust_emit_check` returns false on a
// bare reference to an unimported module's `data`, and `compile_dag_diagnostic_census` reports it
// blocking — while the floor's own witness loader ACCEPTS it, because that loader additionally runs
// `cli_run` `extend_with_bare_reference_closure` and resolves the name through the tree census. A
// fixture written on either surface would therefore be permanently green while the production path
// stays open, and would be cited as coverage of the class it never touches. Its next-rung trigger
// is a compile-observation surface that resolves names by the witness loader's rule.
data compile_accepted_unevaluable_program_note: String = "The subject is the v1 compile path reached through compile_dag_rust_emit_check, which returns false on any hard diagnostic. Each RED below asserts REFUSAL of a program the host will refuse at evaluation anyway, so the assertion is that the refusal moves from evaluation to compile — not that the program changes meaning. All three RED rows return false today and are enrolled in v2.workflow.floor_expected_red; when the argument contract for host primitives is checked at compile they PASS, the enrolled-but-passing arm reds the build naming them, and they stay here afterwards as the regression control that the wall is still real (DESIGN 4b(4): the climb deletes the redundant production handling, never the evidence)."

data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree

data live_tree_note: String = "ReadsLiveTree, for the same reason the two sibling files on this surface declare it: compile_dag_rust_emit_check resolves its virtual source against build_module_path_index_from_witness_roots, which walks the live tree. The declaration is honest rather than convenient — it costs floor admission under the DeclinedLiveTree arm rather than buying it, and that arm's deletion (gunbc#8977, gunbc#8982) is what admits this file to execution."

// Positive control 1 of 2. A trivial well-formed source compiles: the surface is not always-false,
// so a false below is a refusal rather than a harness that cannot say yes.
test fn control_clean_source_compiles() -> Bool {
compile_dag_rust_emit_check(
"module cauc_clean\n\nimport std.types { Int }\n\nfn f() -> Int { 1 }\n",
"src/cauc_clean.rs",
[],
[]
)
}

// Positive control 2 of 2. A source that cannot parse is refused: the surface is not always-true,
// so a true is an acceptance rather than a harness that cannot say no.
test fn control_broken_source_refuses() -> Bool {
!compile_dag_rust_emit_check(
"module cauc_broken\n\nfn f( -> Int { 1 }\n",
"src/cauc_broken.rs",
[],
[]
)
}

// Positive control 3 of 3, and the one that makes the three REDs discriminating rather than a
// blanket claim that this primitive never compiles: the CORRECT call — exactly one string — must
// keep compiling. A wall that refused this would have refused the contract instead of enforcing it.
test fn control_correct_primitive_call_compiles() -> Bool {
compile_dag_rust_emit_check(
"module cauc_prim_ok\n\nimport std.types { Int }\n\nfn f() -> Int { atom_identity_hash(\"a\") }\n",
"src/cauc_prim_ok.rs",
[],
[]
)
}

// RED 1: too many arguments. Live specimens: the four v2.test.manual.bootstrap_footprint_anchor
// rows and the seven test.claim.srv3_subsumption / test.claim.host_phase_status rows in the run's
// receipt, all of which throw `atom_identity_hash requires exactly one string argument`.
test fn primitive_call_with_extra_argument_must_refuse_at_compile() -> Bool {
!compile_dag_rust_emit_check(
"module cauc_prim_over\n\nimport std.types { Int }\n\nfn f() -> Int { atom_identity_hash(\"a\", \"b\") }\n",
"src/cauc_prim_over.rs",
[],
[]
)
}

// RED 2: too few arguments. The zero-argument direction is authored separately because a check
// written as a ceiling would admit it — the same defect shape the method-frontier count rows
// record — and because a caller who deletes an argument is the likelier author of it.
test fn primitive_call_with_missing_argument_must_refuse_at_compile() -> Bool {
!compile_dag_rust_emit_check(
"module cauc_prim_under\n\nimport std.types { Int }\n\nfn f() -> Int { atom_identity_hash() }\n",
"src/cauc_prim_under.rs",
[],
[]
)
}

// RED 3: right arity, wrong type. Arity and inhabitance are two facts, and a wall that closed only
// the count would leave this one open — so it is asserted where it can flip independently.
test fn primitive_call_with_wrong_argument_type_must_refuse_at_compile() -> Bool {
!compile_dag_rust_emit_check(
"module cauc_prim_type\n\nimport std.types { Int }\n\nfn f() -> Int { atom_identity_hash(7) }\n",
"src/cauc_prim_type.rs",
[],
[]
)
}
Original file line number Diff line number Diff line change
@@ -0,0 +1,94 @@
# The 164 runtime-errored floor identities, partitioned by causal family

**Subject:** required-floor run `32633501354`, main push, head `907f19c2cc`
(`Runner slot membership becomes fleet-converge's third member family`), 2026-08-23T10:20Z.
Its ledger line reports `known_red_runtime_errored=164`; `identities.tsv` is those 164 rows,
one per line, as the run itself printed them.

**Producer:** `gh run view 32633501354 --log`, the `KNOWN-RED-RUNTIME-ERRORED` lines, split on the
run's own `is enrolled as expected-red but RUNTIME-ERRORED, not failed:` separator. Column 4 (the
missing name) is joined against a declaration scan of `dag/` and `src/` at the same head.

Columns: `identity`, `family`, `subclass`, `missing name` (empty where the family has none),
`the run's own message`.

## What every one of the 164 has in common

They are programs the compiler ACCEPTED and the interpreter could not evaluate. None is a
compile refusal, and none is a failed assertion — a claim that threw produced no verdict at all,
which is why the floor refuses to let enrollment hold them.

## The families

| family | identities | what the compiler let through |
|---|---|---|
| `REFERENCE-UNAVAILABLE` | 149 | a name resolved at typecheck that the evaluator cannot bind |
| `HOST-PRIMITIVE-CONTRACT` | 11 | a host primitive called with an argument list its host arm rejects |
| `FIELD-ON-WRONG-TYPE` | 2 | `.raw` on an `Int` |
| `CALL-CONTRACT-MISMATCH` | 1 | a call missing a required argument |
| `UNBOUNDED-RECURSION` | 1 | a divergent chain, refused by the interpreter's depth wall |

The last is not a wall gap: the interpreter refuses it with a typed, located, bounded diagnostic.
It is listed because it is one of the 164, not because it is owed a fixture.

## The reference-unavailable subset, by intended compile state

Every one of the 149 names IS declared somewhere in the corpus. **`R4-undeclared-anywhere` is
empty** — not one of them is a typo. So "intended compile state" never separates *should have
refused* from *should have resolved* on the ground of the name not existing; it separates on
WHERE the declaration lives and WHAT KIND it is.

| subclass | identities | distinct names | the declaration the reference names |
|---|---|---|---|
| `R1-data-in-unimported-module` | 126 | 60 | a module-scope `data` in a module the referring file does not import |
| `R6-variant-or-type-name` | 9 | 3 | a coproduct variant / type name used as a bare value |
| `R2-fn-in-unimported-module` | 8 | 3 | a `fn` in a module the referring file does not import |
| `R3-test-decl-in-test-module` | 5 | 5 | a `test data` declared in another `*_test.dag` |
| `R5-type-only` | 1 | 1 | a type name (`Dag`) in call position |

R1 is the class, and it is 85% of the reference-unavailable subset.

## R1 measured end to end, with its discriminating control

Executed at head `907f19c2cc` with a release `gunbc` built from that tree (BuildBuddy, one
dispatch; the session's preinstalled `/usr/local/bin/gunbc` is a stale vintage and refuses the
current `dag/std/algebra.dag` at parse, so it was not used):

| probe source | compile | evaluation |
|---|---|---|
| `fn go() { argument_form_is_valid(design_argument) }`, no imports at all | accepted, silent | `NoSuchFunction { name: "design_argument" }` |
| the same call with `import gunbc.design_argument { design_argument }` | accepted | evaluates, `true` |

The import is the whole discriminator, and the compiler says nothing about its absence. The
second row is what makes the first a finding rather than a broken fixture: the declaration is
fine, the reference is fine, and only the loader's reach differs.

## Why no R1 control fixture is in this PR, stated as a measurement rather than as a plan

The two `.dag`-callable compile-observation surfaces both REFUSE the R1 shape, so a fixture built
on either would be permanently green and would be cited as coverage of a class it never touches
(DESIGN §4b: a check whose RED is unauthorable is worse than absent).

| surface | R1 shape (`bare data reference`) | bare name declared nowhere | clean control | broken control |
|---|---|---|---|---|
| `compile_dag_diagnostic_census` | `InternalError variable:design_argument`, blocking | `InternalError`, blocking | 0 rows | — |
| `compile_dag_rust_emit_check` | `false` (refuses) | `false` (refuses) | `true` | `false` |
| the floor's own witness loader (production) | **accepted** | — | — | — |

Both surfaces compile a virtual source through import-closure discovery. The floor's witness
loader additionally runs `cli_run` `extend_with_bare_reference_closure`, which resolves a bare
name through the tree census and pulls the module it names. That closure is why the reference
typechecks in production, and the interpreter then binds functions and not module-scope `data`.

**Next-rung trigger for the R1 control:** a compile-observation surface that resolves names by the
witness loader's rule — the bare-reference closure — rather than by import-closure discovery
alone. Until one exists, the class is observable only as the floor's own
`known_red_runtime_errored` counter, and that counter goes to zero as the 149 are repaired.
`gunbc#9006` is repairing 21 of them (the `*_published_mock_corpus` names) as this is written.

## What IS in this PR

`HOST-PRIMITIVE-CONTRACT` reproduces on `compile_dag_rust_emit_check` — the surface accepts
`atom_identity_hash("a", "b")` and the host arm refuses it at evaluation. That is an authorable
RED, and it is the fixture this PR lands:
`dag/test/claim/compile_accepted_unevaluable_program_control_test.dag`.
Loading
Loading