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
40 changes: 39 additions & 1 deletion dag/test/claim/normalize_retention_contract_probe_test.dag
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import v2.std.logic { Bool }
import v2.std.node { Symbol }
import v2.std.collection { List }
import v2.std.algebra { fold_list }
import std.content_hash { compare_content_hash, ContentHashEqual }
import v2.std.diagnostic { Diagnostic, NonEmptyDiagnostics, module_unavailable_diagnostic }
import gunbc.tools.frontier_ingestion_probe {
FrontendStage,
Expand All @@ -24,6 +25,8 @@ import gunbc.tools.frontier_ingestion_probe {
reconcile_census,
verify_roster,
verify_frontier_roster,
roster_identity,
frontier_roster_identity,
FrontierMember,
FrontierRosterValid,
FrontierRosterDuplicateLabel,
Expand All @@ -37,6 +40,8 @@ import gunbc.tools.frontier_ingestion_probe {

data permanent_witness_scope_note: String = "WHAT THIS WITNESS MAY ASSERT, and why the live-corpus rows are NOT here. A required witness whose success depends on the current defects continuing to exist inverts the moment the defect is repaired: it would go RED on the repair and GREEN on a regression. So the assertions below validate the STAGE CLASSIFIER, the containment-read discipline, and the roster join on specimens whose stage is a property of the specimen rather than of the frontier. The per-member live population is a revision-scoped OBSERVATION recorded in docs/plans/v2-frontend-std-ingestion-frontier-exact-head.md and reproducible from gunbc.tools.frontier_ingestion_probe, which is deliberately NOT a test module for exactly this reason. Every classifier and roster symbol is imported from that one authority rather than restated here, so the thing under test and the thing used for measurement cannot drift apart."

data census_execution_not_enrolled_note: String = "THE CENSUS STILL DOES NOT EXECUTE HERE, and this increment did not change that — it changed what executing would COST. take_frontend_census prepares the lex rules and the parse grammar once and classifies all fifteen members through that one prepared world, instead of rebuilding the grammar per member as the previous shape did; 02_parse's own prepared_grammar_carrier_note is the authority for why that seam exists.\n\nWhat is NOT claimed: that the result now fits the per-PR fast lane. No claim below runs take_frontend_census, because doing so reads fifteen live files and builds the grammar once, and one grammar construction alone was previously measured over the five-second budget. Preparing once removes a fifteen-times multiplier from a cost that may still exceed the budget by itself, and I have not measured the result — the local container has no claim_batch binary, so any number stated here would be invented rather than observed.\n\nSo the enrollment decision is deferred to a measurement, not to an opinion, and the arithmetic that makes it a real question is what landed. If the prepared census is still over budget, the answer is realization or materialization, not a long/ directory and not silence."

data stage_separation_cost_note: String = "WHY TWO STAGE-SEPARATION CLAIMS ARE NOT HERE, stated rather than hidden. classify_source reaching parse_module builds dag_grammar(), and that construction alone measured 5002-5003ms thread-CPU against the 5000ms fast-lane budget on CI — so an ACCEPTED claim and a PARSE claim cannot execute per-PR, while the LEX claim below can, because a lex refusal returns before any grammar is built.\n\nThey are DELETED, not relocated. Moving them under a long/ directory would remove them from per-PR discovery without giving them an executing consumer, which deletes the coverage while retaining the source — the gunbc#7762 specimen the 2026-08-04 admission ruling exists to forbid. Nothing here claims those two stages are covered.\n\nWHAT IS OWED, and to which lane: the 15-member census needs a batched or realized instrument precisely because the interpreted path also exceeds budget on the larger members. Closing the result space and reconciling the census against the roster (this increment) does not discharge that; it only means the instrument those two claims return to now has a total verdict type and a denominator to join against."

data empty_reason_set_control_retirement_note: String = "WHERE THE EMPTY-REASON-SET RED WENT. A previous revision asserted classify_normalize_reasons(rs: []) == NORM_REASON_SET_INVALID_EMPTY, guarding the collapse in which a missing observation reads as an accepted stage. The classifier now takes NonEmptyDiagnostics, whose head field is not optional, so that input has no representation and the arm it exercised has no subject.\n\nThis is the one case where the dissolution rule's keep-the-evidence clause does not apply, and the distinction is worth being exact about: the rule preserves a discriminating control when the invalid state stays WRITABLE and a mechanism keeps it out. Here the state became unwritable, so the control cannot be authored at all — not because it was judged redundant, but because it has no input. Retaining it would require re-widening the parameter type to admit the value it tests, which is the wall itself run backwards. The class did not stop being guarded; it stopped being expressible."
Expand All @@ -59,8 +64,41 @@ fn classify_reasons(first: Symbol, rest: List<Symbol>) -> FrontendStage {
}


// classify_source now returns an Outcome, because grammar preparation can refuse and that is a
// fact about the world rather than about this source. The claim matches the Accepted arm
// explicitly: collapsing it would let a refused preparation satisfy a claim about lexing.
test fn classifier_separates_lex_from_accepted() -> Bool {
frontend_stage_eq(a: classify_source(source: unterminated_string_source), b: LexRefused)
match classify_source(source: unterminated_string_source) {
v2.std.diagnostic.Accepted { value: st, diagnostics: _ } => frontend_stage_eq(a: st, b: LexRefused)
v2.std.diagnostic.Rejected { diagnostics: _ } => false
}
}

// The roster identity separates denominators rather than naming one. Same rows in the same order
// give the same identity; a changed path gives a different one. Both directions are asserted,
// because an identity function that returned a constant would satisfy the first alone.
test fn roster_identity_is_stable_across_calls() -> Bool {
let c = compare_content_hash(left: frontier_roster_identity(), right: frontier_roster_identity())
c == ContentHashEqual
}

test fn roster_identity_separates_different_paths_RED() -> Bool {
let c = compare_content_hash(
left: roster_identity(rows: two_row_roster),
right: roster_identity(rows: duplicate_path_roster)
)
(c == ContentHashEqual) == false
}

// Order is part of the denominator, so a reordering is a different identity even though
// verify_roster calls both rosters valid. The two claims say different things and both are load
// bearing: validity is order-insensitive, identity is not.
test fn roster_identity_separates_reordered_rows_RED() -> Bool {
let c = compare_content_hash(
left: roster_identity(rows: two_row_roster),
right: roster_identity(rows: two_row_roster_reordered)
)
(c == ContentHashEqual) == false
}


Expand Down
Loading
Loading