diff --git a/dag/gunbc/where_refinement_predicate_vocabulary.dag b/dag/gunbc/where_refinement_predicate_vocabulary.dag new file mode 100644 index 00000000000..cf3ff7f9ca8 --- /dev/null +++ b/dag/gunbc/where_refinement_predicate_vocabulary.dag @@ -0,0 +1,266 @@ +module gunbc.where_refinement_predicate_vocabulary + +import std.types { String, NonEmptyStr, Bool, Int, List } +import std.decl_ref { DeclarationRef, WholeDeclaration } +import std.dissolution { DissolutionCondition, unbound_dissolution } + +// THE SUBJECT IS PREDICATE IDENTITY, NOT PREDICATE COUNT. A where-refinement predicate +// (`type NonEmptyStr = String where non_empty`) is a BARE IDENTIFIER with no declaration binding +// anywhere in the pipeline. v1.compiler.parse parse_single_predicate accepts any identifier in its +// unparenthesised arm, and v1.compiler.infer then decides what the identifier MEANS by matching the +// string against three hand-written name-keyed tables (where_refinement_is_int_literal_predicate, +// where_refinement_is_string_literal_predicate, where_refinement_is_deferred_predicate). Predicate +// identity for subsumption -- where_refinement_predicates_equivalent -- is bare string equality on +// that same unresolved name. So the tables are a SECOND AUTHORITY for what a predicate means, +// forked from the declaration that already states it wherever one exists (DESIGN section 3). +// +// THIS MODULE IS THE JOIN THAT DID NOT EXIST: one row per predicate spelling authored anywhere in +// the corpus, carrying the compiler's enforcement class and whether a real declaration grounds it. +// It exists because those two facts were UNCORRELATED and nothing said so. Seven of the fifteen +// spellings are grounded by a declared total Bool function and eight are not, and the compiler's +// treatment does not track that split in either direction: two grounded String->Bool predicates are +// enrolled and WALL at literal construction sites, three structurally identical ones -- two of them +// declared in the SAME FILE as an enrolled pair -- are in no table at all and are therefore +// permanently advisory. The discriminator is not decidability, grounding, or any property of the +// predicate. It is whether a human added a table row. +// +// WHAT THE ROWS ARE NOT. They carry no occurrence counts and no site lists. A count copied into a +// row here would be a transcribed measurement rotting away from the tree that produced it +// (DESIGN section 6); the instrument that re-derives corpus membership is named under the ceiling +// below. Identity -- which spellings exist and what each one means -- is the fact this roster owns, +// because identity is what the compiler gets wrong. + +type WherePredicateEnforcement + = IntLiteralDecidable + | StringLiteralDecidable + | DeferredAtCompileTime + | UnenrolledNoTableRow + +// GROUNDING IS A COPRODUCT AND NOT AN OPTIONAL DECLARATION REF, because the two states owe +// different things. A grounded predicate has an authority the compiler is DECLINING to consult; an +// ungrounded one has no authority anywhere and its meaning exists only inside 04_infer. Collapsing +// them into `DeclarationRef?` would make "nobody wrote this down" and "somebody wrote it down and +// we ignore it" the same absent value, which is exactly the distinction this roster was built to +// surface. +type WherePredicateGrounding + = GroundedByDeclaration { declaration: DeclarationRef } + | NoDeclarationCompilerInternal + +type WherePredicateRow { + spelling: String + enforcement: WherePredicateEnforcement + grounding: WherePredicateGrounding +} + +fn where_predicate_decl(module_path: String, decl_name: String) -> WherePredicateGrounding { + GroundedByDeclaration { + declaration: DeclarationRef { + module_path: module_path as NonEmptyStr, + decl_name: decl_name as NonEmptyStr, + field: WholeDeclaration + } + } +} + +// SPELLING IS THE KEY, and it is the spelling as AUTHORED in the where clause rather than the name +// the compiler compares. The two differ for exactly one row: `where brand("...")` is folded by +// v1.compiler.parse into a predicate node named "Brand", and where_predicate_canonical_name then +// maps "brand" onto "Brand" so the two spellings meet. The authored form is the key here because +// this roster's population is what an author can write, not what the parser rewrites it into. + +// THE non_empty ROW IS THE FORK, AND IT IS THE ONE A GREP FOR THE SPELLING CANNOT FIND. It is +// recorded as NoDeclarationCompilerInternal even though `fn non_empty` EXISTS in the corpus, +// because the declaration that exists is v2.std.algebra non_empty(xs: FreeMonoid) -> Bool -- +// a different predicate over a different domain. The where-predicate `non_empty` means String +// length > 0 and that meaning is hand-written inside 04_infer +// decidable_where_string_predicate_holds. Claiming the algebra declaration as that row's grounding +// would be the fabrication DESIGN section 5 forbids: it would assert an authority that does not +// answer for this predicate. A THIRD carrier of the same concept exists at +// v2.lens.enforcement.gate non_empty_string(s: String) -> Bool. One concept, three authorities, and +// the load-bearing one is not a declaration at all. + +data where_refinement_predicate_vocabulary: List = [ + WherePredicateRow { + spelling: "brand", + enforcement: DeferredAtCompileTime, + grounding: NoDeclarationCompilerInternal + }, + WherePredicateRow { + spelling: "range", + enforcement: IntLiteralDecidable, + grounding: NoDeclarationCompilerInternal + }, + WherePredicateRow { + spelling: "gt_zero", + enforcement: IntLiteralDecidable, + grounding: NoDeclarationCompilerInternal + }, + WherePredicateRow { + spelling: "non_empty", + enforcement: StringLiteralDecidable, + grounding: NoDeclarationCompilerInternal + }, + WherePredicateRow { + spelling: "lower_hex_16", + enforcement: StringLiteralDecidable, + grounding: NoDeclarationCompilerInternal + }, + WherePredicateRow { + spelling: "lower_hex_40", + enforcement: StringLiteralDecidable, + grounding: NoDeclarationCompilerInternal + }, + WherePredicateRow { + spelling: "lower_hex_64", + enforcement: StringLiteralDecidable, + grounding: NoDeclarationCompilerInternal + }, + WherePredicateRow { + spelling: "lower_hex_128", + enforcement: StringLiteralDecidable, + grounding: NoDeclarationCompilerInternal + }, + WherePredicateRow { + spelling: "oci_other_digest_algorithm", + enforcement: StringLiteralDecidable, + grounding: where_predicate_decl( + module_path: "extdeps.container.oci.digest", + decl_name: "oci_other_digest_algorithm" + ) + }, + WherePredicateRow { + spelling: "oci_other_digest_encoded", + enforcement: StringLiteralDecidable, + grounding: where_predicate_decl( + module_path: "extdeps.container.oci.digest", + decl_name: "oci_other_digest_encoded" + ) + }, + WherePredicateRow { + spelling: "unicode_scalar", + enforcement: DeferredAtCompileTime, + grounding: where_predicate_decl( + module_path: "std.unicode.types", + decl_name: "unicode_scalar" + ) + }, + WherePredicateRow { + spelling: "is_text_readable", + enforcement: DeferredAtCompileTime, + grounding: where_predicate_decl( + module_path: "std.filesystem", + decl_name: "is_text_readable" + ) + }, + WherePredicateRow { + spelling: "oci_path_component_syntax", + enforcement: UnenrolledNoTableRow, + grounding: where_predicate_decl( + module_path: "extdeps.container.oci.reference", + decl_name: "oci_path_component_syntax" + ) + }, + WherePredicateRow { + spelling: "oci_tag_syntax", + enforcement: UnenrolledNoTableRow, + grounding: where_predicate_decl( + module_path: "extdeps.container.oci.reference", + decl_name: "oci_tag_syntax" + ) + }, + WherePredicateRow { + spelling: "c_translation_unit_basename_safe", + enforcement: UnenrolledNoTableRow, + grounding: where_predicate_decl( + module_path: "v2.extdeps.languages.c", + decl_name: "c_translation_unit_basename_safe" + ) + } +] + +fn where_predicate_spellings(rows: List) -> List { + rows |> map(r => r.spelling) +} + +fn where_predicate_rows_of_enforcement( + rows: List, + wanted: WherePredicateEnforcement +) -> List { + rows |> filter(r => r.enforcement == wanted) +} + +fn where_predicate_grounded_rows(rows: List) -> List { + rows |> filter(r => + match r.grounding { + GroundedByDeclaration { declaration: _ } => true + NoDeclarationCompilerInternal => false + } + ) +} + +// THE UNENROLLED THREE ARE DEBT, NOT A DESIGN. Each is a declared, total, decidable String -> Bool +// function that the compiler could evaluate at a literal construction site exactly as it already +// evaluates oci_other_digest_algorithm and oci_other_digest_encoded, which are declared in the same +// file as two of them. They are DESIGN section 5's wall after grounding: decidable, grounded, and +// unbuilt. Until then every construction at these three refined positions -- valid and invalid +// alike -- produces one WhereRefinementUnenforced advisory and no refusal. +// +// THE ROW IS NOT A LICENCE. Nothing here admits a fourth member. The witness beside this module +// executes the roster against the compiler's real behaviour name by name, so a new unenrolled +// predicate reds rather than joining a list. + +// CEILING AND WHAT THIS ROSTER CANNOT DO, stated because a roster read as a census is worse than +// no roster (DESIGN 4b meta-obligation 1: the reported rung must equal the rung executed evidence +// establishes). +// +// RUNG: 2, MECHANICALLY PREVENTABLE. The invalid state stays fully writable -- nothing prevents an +// author adding `type T = String where whatever_i_typed` tomorrow, and nothing prevents a second +// declaration claiming a spelling this roster already carries. Safety here depends entirely on the +// witness beside this module executing and staying enrolled on the required floor. It is not a +// wall and must not be cited as one. +// +// THE HALF THAT IS EXECUTED: every spelling in this roster is driven through the real v1 compile +// path by the witness, and its declared enforcement class is asserted against the compiler's +// observed behaviour on a synthetic source. That join is an identity join over all fifteen rows, +// not a count, and it reds if a row's class and the compiler's tables ever disagree in either +// direction -- a table row added without a roster row, or a roster row whose class was wrong. +// +// THE HALF THAT IS NOT: whether these fifteen spellings are ALL the spellings authored in the live +// tree. No substrate reader exposes where-clause predicates today. concept_decl_facts_live marshals +// only Disj and Conj type items and drops the refinement annotation, so the population cannot be +// re-derived inside a .dag lens without a new host reader -- and adding one would be new +// hand-maintained Rust, which the v1 exit lane closes rather than grows. The membership claim is +// therefore AUTHOR-VOUCHED, re-derivable only out of band, and that is this roster's real ceiling. +// NEXT-RUNG TRIGGER for the membership half, named as the capability rather than an artifact: a +// substrate reader that projects where-clause refinement predicates from type declarations over the +// live tree, SUFFICIENT FOR a .dag lens to assert checked == total over the corpus population +// without the roster being consulted. Until that exists, a new predicate spelling that never +// reaches this file is invisible to every mechanism in this repository. +// +// WHEN THE WITNESS ACTUALLY RUNS, MEASURED RATHER THAN ASSUMED, because "enrolled on the required +// floor" and "executes on every run" are different claims and the second one is FALSE here. On the +// run that admitted this module the seven identities appear in required_floor_disposition.tsv as +// planned_as_changed_witness / passed -- they are the ONLY seven rows of that disposition in a +// 15984-row floor, and they ran because these files CHANGED. The floor's other arms are 3595 +// planned (inside the gate closure, the transitive import/reference closure of the gate seeds) and +// 11824 declined_outside_gate_closure. THE SIBLING SETTLES WHICH ARM THIS FILE LANDS IN once it +// stops changing: test.claim.compile_diagnostic_census_witness -- same directory, same host +// builtin, the module this witness was modelled on -- is declined_outside_gate_closure on that very +// run. So this is a CHANGE-TRIGGERED control, not a continuously-executing one. +// +// THE CONSEQUENCE IS SPECIFIC AND IT NARROWS THE WALL, so it is stated here rather than left for +// someone to discover from a disposition file: an edit to this roster or to the witness re-runs the +// join, but AN EDIT TO THE COMPILER'S CLASSIFIER TABLES DOES NOT. The join reaches the compiler +// through the compile_dag_diagnostic_census host builtin rather than through an import edge, and +// src/v1 is not a source root under the required floor, so v1.compiler.infer cannot appear in this +// module's closure at all. Adding a sixteenth predicate to where_refinement_is_string_literal_ +// predicate without touching either of these two files would therefore NOT red. The wall catches +// ROSTER drift; it does not catch COMPILER drift, and only one of those two is the side that +// changes when someone enrols a predicate. +// +// NEXT-RUNG TRIGGER for that half, again the capability: this module inside the required gate +// closure -- reached from the gate seeds rather than selected by having been edited -- SUFFICIENT +// FOR the roster-to-compiler join to execute on runs that touch neither file, which is the only +// condition under which it can observe a table edit made elsewhere. + +data where_refinement_unenrolled_predicate_dissolve_trigger: DissolutionCondition = unbound_dissolution(description: "TRIGGER, one and checkable: a where-refinement predicate spelling is RESOLVED to its declaration rather than matched against a name-keyed table, so that the declaration is the predicate's single authority for both its meaning and its identity under subsumption. SUFFICIENT FOR: (a) deleting where_refinement_is_int_literal_predicate, where_refinement_is_string_literal_predicate, where_refinement_is_deferred_predicate and decidable_where_string_predicate_holds rather than adding rows to them, since a resolved declaration states its own semantics; (b) refusing an unresolvable predicate spelling at acceptance, which retires the 'predicate not enforced at compile time' arm of is_where_refinement_unenforced_advisory_reason; and (c) keying where_refinement_predicates_equivalent on the resolved declaration rather than on the spelling. A CHANGE THAT DELIVERS ONLY ONE OF THE THREE DOES NOT RETIRE THIS ROW, and the reason is stated because the grain mismatch is the review tell DESIGN 4b(3) names: the loss here is a CORPUS-GRAIN loss over every predicate spelling, so a trigger naming one predicate's enrolment, or one table's replacement, would be satisfied while the capability stays dead. ENROLLING THESE THREE NAMES IN THE EXISTING TABLES IS EXPLICITLY NOT THE TRIGGER AND WOULD NOT DISCHARGE THIS ROW: it would grow the forked authority this row exists to record, which DESIGN section 2 calls a failed decomposition. There is a STANDING declared trigger in the tree naming a DIFFERENT end-state for the same subject -- feature:where-refinement-predicate-coproduct, a closed WhereRefinementPredicateKind coproduct replacing the string classifiers, cited by where_refinement_deferral_reason_scaffold_note in v1.std.core and by the predicate min-length tables in v1.compiler.infer. THIS ROW DOES NOT SUPERSEDE IT AND MUST NOT BE READ AS DOING SO. DESIGN 4b(3) is categorical that a declared drop is retired by its trigger and by nothing else, so the choice between a resolved declaration and a closed coproduct is a trigger CHANGE owed in the open as its own decision, not something a better answer may outrun. Whichever wins, this roster's rows are the population that change has to cover. TWO FACTS ABOUT THE SHAPE ARE ALREADY DECIDED AND ARE RECORDED HERE RATHER THAN RE-ARGUED LATER, because the second one is a refusal and a refusal that lives only in a chat thread is not an authority. ASKED of the lane carrying gunbc#10146 (declaration-bound direct-call formal authority, the same move applied to call formals on the same file) whether its ResolvedFormal / DeclarationBoundFormals coproduct generalises to predicates. IT DOES NOT, and reusing it was REFUSED: its fields are parameter_identity, declared_type, declaration_bound_conformance and substitution_basis, and its consumers depend on formal-to-argument correspondence, so a predicate inhabiting it would give those four fields a second meaning under one name -- the DESIGN section 3 fork this row exists to close, re-created while closing it. What generalises is the PATTERN and not the carrier: resolve at the declaration-owning environment, carry an exact declaration identity or a typed unavailable cause forward to the later judgment, and prohibit reconstruction from a bare string at the consuming site. So the predicate move owes its OWN domain carrier declared in substrate, keyed by DeclarationRef rather than by spelling, with its own unavailable causes -- a predicate's ways of failing to resolve are not a call formal's. SEQUENCING, agreed with that lane: the predicate move is a FOLLOW-ON that consumes the established pattern after gunbc#10146 lands, and is NOT folded into it; that PR is integrating main and validating its direct-call floor, and widening its subject would obscure both witnesses.") diff --git a/dag/test/claim/where_refinement_predicate_vocabulary_witness_test.dag b/dag/test/claim/where_refinement_predicate_vocabulary_witness_test.dag new file mode 100644 index 00000000000..9021de7d3ee --- /dev/null +++ b/dag/test/claim/where_refinement_predicate_vocabulary_witness_test.dag @@ -0,0 +1,358 @@ +module test.claim.where_refinement_predicate_vocabulary_witness_test + +import std.types { String, NonEmptyStr, Bool, Int, List } +import v2.std.live_tree { LiveTreeDisposition, ReadsLiveTree } + +import gunbc.where_refinement_predicate_vocabulary { + WherePredicateRow, + WherePredicateEnforcement, + IntLiteralDecidable, + StringLiteralDecidable, + DeferredAtCompileTime, + UnenrolledNoTableRow, + where_refinement_predicate_vocabulary, + where_predicate_spellings, + where_predicate_rows_of_enforcement +} + +import gunbc.compile_diagnostic_census { + CompileDiagnosticCensus, + CompileDiagnosticCensusRow, + CensusObserved, + CensusNotRunnable, + census_blocking_rows, + census_advisory_rows, + census_rows_of_class, + census_total_count +} + +data live_tree_disposition: LiveTreeDisposition = ReadsLiveTree + +// ReadsLiveTree and not SubstrateInputsOnly, for the same reason the sibling census witness +// declares it: compile_dag_diagnostic_census resolves its synthetic source against +// build_module_path_index_from_witness_roots, which walks the live tree. The read is real, and an +// undeclared read is ReadsLiveTree by the fail-closed default anyway. Copying a cheaper claim from +// a neighbour would buy selection-eligibility with a false statement. + +// WHAT THIS WITNESS PROVES, AND THE ONE THING IT DELIBERATELY ASSERTS AS DEBT. +// +// It executes gunbc.where_refinement_predicate_vocabulary against the real v1 compile path, one +// probe per rostered predicate spelling, and asserts that the compiler's OBSERVED behaviour agrees +// with the class the row declares. The join is by SPELLING and it runs in both directions -- every +// roster row has a probe and every probe has a roster row -- so a spelling added to one side alone +// reds rather than being silently skipped. That bidirectional assertion is the whole point: a +// one-directional check over a table you also author is satisfied by narrowing the table, and a +// count equality is satisfied by any two sets of the same size. +// +// THE OBSERVABLE IS BINARY, AND SAYING SO IS PART OF THE RUNG. The census surface projects a +// diagnostic's CLASS and SUBJECT NAME, never its REASON. "predicate deferred at compile time" and +// "predicate not enforced at compile time" are therefore indistinguishable through it -- both are +// one advisory WhereRefinementUnenforced row keyed to the predicate. So what executes here is the +// TWO-way partition {refuses a violating literal} vs {never refuses}, not the roster's four-way +// class. The roster's split of the never-refuses bucket into DeferredAtCompileTime and +// UnenrolledNoTableRow is author-vouched and this file does not pretend otherwise. Next-rung +// trigger for that half, named as the capability: the census surface projecting the diagnostic +// reason alongside class and subject name, SUFFICIENT FOR a probe to distinguish a deliberate +// deferral from an unrecognised spelling without reading the compiler's tables. +// +// THIS WITNESS IS CHANGE-TRIGGERED, NOT CONTINUOUSLY EXECUTING, and the roster records the +// measurement: its seven identities ran as planned_as_changed_witness because these files changed, +// while the sibling it was modelled on sits in declined_outside_gate_closure on the same run. So an +// edit to the compiler's classifier tables does not re-run this join -- it reaches the compiler +// through a host builtin, not an import edge. Do not read a green floor as evidence this executed; +// read required_floor_disposition.tsv. +// +// THE THREE UNENROLLED ROWS ARE ASSERTED AS A MONOTONE DEBT CONTRACT, NOT AS CORRECT BEHAVIOUR. +// w_unenrolled_predicates_admit_a_violating_literal asserts that a plainly invalid literal at each +// of the three unenrolled refined positions compiles with ZERO refusals. That is the defect, held +// as a control so it cannot grow: a FOURTH unenrolled spelling reds +// w_every_roster_spelling_has_exactly_one_probe, and enrolling one of the three reds this +// assertion until its roster row is deleted in the same change. The subject universe is closed by +// the roster and membership is checked at spelling grain, never by count, which is what DESIGN +// section 5 requires of a debt contract before it may block a merge. + +// FIELD NOTES, hoisted here because source annotations are module-item grain and one inside a +// declaration body refuses (DESIGN 4c). `clause` is the full where-clause text as an author writes +// it and is NOT the spelling: `brand` and `range` are parenthesised forms and a bare spelling would +// not parse, so carrying only the key would have quietly restricted this witness to the +// unparenthesised predicates -- the narrowed subject that looks identical to a passing one. +// `value_text` is the literal as it appears in source, quotes included for string bases, and every +// one of them VIOLATES its predicate wherever the predicate is decidable at all, because a +// satisfying literal is silent under both arms of the partition and could not discriminate them. + +type WherePredicateProbe { + spelling: String + clause: String + base_type: String + value_text: String + expected_refusal: Bool +} + +// THE LAST THREE ROWS ARE THE FINDING. oci_path_component_syntax, oci_tag_syntax and +// c_translation_unit_basename_safe each carry a value_text no author could mistake for a valid +// instance of the type -- an OCI path component may not contain spaces or exclamation marks, an OCI +// tag may not either, and a C translation-unit basename may not. All three predicates are declared, +// total String -> Bool functions that decide exactly this. All three compile clean. + +data where_predicate_probes: List = [ + WherePredicateProbe { + spelling: "brand", + clause: "brand(\"wpv_probe_brand\")", + base_type: "String", + value_text: "\"anything\"", + expected_refusal: false + }, + WherePredicateProbe { + spelling: "range", + clause: "range(min: 1, max: 5)", + base_type: "Int", + value_text: "9", + expected_refusal: true + }, + WherePredicateProbe { + spelling: "gt_zero", + clause: "gt_zero", + base_type: "Int", + value_text: "0", + expected_refusal: true + }, + WherePredicateProbe { + spelling: "non_empty", + clause: "non_empty", + base_type: "String", + value_text: "\"\"", + expected_refusal: true + }, + WherePredicateProbe { + spelling: "lower_hex_16", + clause: "lower_hex_16", + base_type: "String", + value_text: "\"zz\"", + expected_refusal: true + }, + WherePredicateProbe { + spelling: "lower_hex_40", + clause: "lower_hex_40", + base_type: "String", + value_text: "\"zz\"", + expected_refusal: true + }, + WherePredicateProbe { + spelling: "lower_hex_64", + clause: "lower_hex_64", + base_type: "String", + value_text: "\"zz\"", + expected_refusal: true + }, + WherePredicateProbe { + spelling: "lower_hex_128", + clause: "lower_hex_128", + base_type: "String", + value_text: "\"zz\"", + expected_refusal: true + }, + WherePredicateProbe { + spelling: "oci_other_digest_algorithm", + clause: "oci_other_digest_algorithm", + base_type: "String", + value_text: "\"NOT+AN+ALGORITHM\"", + expected_refusal: true + }, + WherePredicateProbe { + spelling: "oci_other_digest_encoded", + clause: "oci_other_digest_encoded", + base_type: "String", + value_text: "\"NOT+AN+ENCODING\"", + expected_refusal: true + }, + WherePredicateProbe { + spelling: "unicode_scalar", + clause: "unicode_scalar", + base_type: "Int", + value_text: "0 - 1", + expected_refusal: false + }, + WherePredicateProbe { + spelling: "is_text_readable", + clause: "is_text_readable", + base_type: "String", + value_text: "\"anything\"", + expected_refusal: false + }, + WherePredicateProbe { + spelling: "oci_path_component_syntax", + clause: "oci_path_component_syntax", + base_type: "String", + value_text: "\"NOT A PATH COMPONENT!!\"", + expected_refusal: false + }, + WherePredicateProbe { + spelling: "oci_tag_syntax", + clause: "oci_tag_syntax", + base_type: "String", + value_text: "\"NOT A TAG!!\"", + expected_refusal: false + }, + WherePredicateProbe { + spelling: "c_translation_unit_basename_safe", + clause: "c_translation_unit_basename_safe", + base_type: "String", + value_text: "\"NOT A BASENAME!!\"", + expected_refusal: false + } +] + +fn probe_source(p: WherePredicateProbe) -> String { + concat( + concat( + concat( + concat("module wpv_probe\ntype WpvProbe = ", p.base_type), + concat(" where ", p.clause) + ), + "\nfn wpv_f() -> WpvProbe { " + ), + concat(p.value_text, " as WpvProbe }\n") + ) +} + +// A NEGATIVE COUNT IS THE COULD-NOT-MEASURE ARM AND NEVER A ZERO. CensusNotRunnable is an +// infrastructural failure of the probe compile, and folding it to 0 would make a broken harness +// read as a clean source -- the top-as-answer conflation DESIGN section 5 names. Every assertion +// below therefore compares against a non-negative expectation, so an unrunnable probe reds. + +fn probe_blocking_count(p: WherePredicateProbe) -> Int { + match compile_dag_diagnostic_census(probe_source(p: p)) { + CensusObserved { rows: rows } => census_total_count(rows: census_blocking_rows(rows: rows)) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +fn probe_where_advisory_count(p: WherePredicateProbe) -> Int { + match compile_dag_diagnostic_census(probe_source(p: p)) { + CensusObserved { rows: rows } => + census_total_count( + rows: census_advisory_rows( + rows: census_rows_of_class(rows: rows, wanted: "WhereRefinementUnenforced") + ) + ) + CensusNotRunnable { cause: _ } => 0 - 1 + } +} + +fn probe_agrees_with_roster(p: WherePredicateProbe) -> Bool { + let blocking = probe_blocking_count(p: p) + if p.expected_refusal { + blocking >= 1 + } else { + blocking == 0 && probe_where_advisory_count(p: p) >= 1 + } +} + +fn probe_spellings() -> List { + where_predicate_probes |> map(p => p.spelling) +} + +fn roster_spellings() -> List { + where_predicate_spellings(rows: where_refinement_predicate_vocabulary) +} + +fn count_occurrences(xs: List, wanted: String) -> Int { + xs |> filter(x => x == wanted) |> count +} + +// THE BIDIRECTIONAL IDENTITY JOIN. Not a count equality: two sets of the same size satisfy that +// while sharing no members, and automating a count would collapse the assertion to +// measure() == measure(). This asserts that every roster spelling appears EXACTLY ONCE among the +// probes and every probe spelling appears EXACTLY ONCE in the roster, which also carries the +// no-duplicate-spelling requirement in both tables without a separate check to keep in step. + +test fn w_every_roster_spelling_has_exactly_one_probe() -> Bool { + roster_spellings() |> all(s => count_occurrences(xs: probe_spellings(), wanted: s) == 1) +} + +test fn w_every_probe_spelling_has_exactly_one_roster_row() -> Bool { + probe_spellings() |> all(s => count_occurrences(xs: roster_spellings(), wanted: s) == 1) +} + +// THIS IS THE COLLISION ASSERTION, named rather than left to be inferred from its shape. A +// where-predicate's identity is its SPELLING -- where_refinement_predicates_equivalent compares +// predicate names for equality with no declaration binding -- so one spelling standing for two +// meanings is silently judged EQUIVALENT and the site is accepted with no diagnostic at all. That +// is the state this assertion exists to make loud: two rows claiming one spelling, which is how a +// second meaning would have to enter this roster, red here. +// +// WHAT IT CAN AND CANNOT SEE, because a collision check that quietly ranges over the wrong +// population is worse than none. It ranges over the ROSTER, so it catches a spelling given two +// groundings HERE. It does NOT range over the corpus: two declarations claiming one predicate name +// where neither reaches this file are invisible to it, for the same reason the membership half is +// author-vouched -- no substrate reader projects where-clause predicates, so there is nothing to +// join the corpus against. The corpus is collision-free as measured at authoring time (15 spellings +// each denoting one thing, and 230 brand("...") literals all distinct), and it is held that way by +// authoring diligence -- rung 1 -- not by this witness. + +test fn w_roster_spellings_are_pairwise_distinct() -> Bool { + roster_spellings() |> all(s => count_occurrences(xs: roster_spellings(), wanted: s) == 1) +} + +// THE EXECUTED HALF: every rostered spelling driven through the real v1 compile path, and the +// observed refusal behaviour asserted against the class its row declares. checked == total by +// construction, because the two joins above force the probe set and the roster set to be the same +// set before this runs over all of it. + +test fn w_every_rostered_predicate_behaves_as_its_row_declares() -> Bool { + where_predicate_probes |> all(p => probe_agrees_with_roster(p: p)) +} + +// THE CONTRAST CONTROL, and without it the assertion above proves nothing. If the probe harness +// could not refuse ANYTHING -- a malformed source shape, a cast the compiler ignores -- then every +// expected_refusal: false row would pass for the wrong reason and the three unenrolled rows would +// read as measured when they were merely unrefuted. This pins one enrolled predicate refusing and +// one unenrolled predicate not refusing, on sources differing ONLY in the predicate spelling, so +// the discriminator is the predicate and not the shape. + +data enrolled_contrast_probe: WherePredicateProbe = WherePredicateProbe { + spelling: "lower_hex_40", + clause: "lower_hex_40", + base_type: "String", + value_text: "\"NOT A TAG!!\"", + expected_refusal: true +} + +data unenrolled_contrast_probe: WherePredicateProbe = WherePredicateProbe { + spelling: "oci_tag_syntax", + clause: "oci_tag_syntax", + base_type: "String", + value_text: "\"NOT A TAG!!\"", + expected_refusal: false +} + +test fn w_one_literal_two_predicates_one_refuses_and_one_does_not() -> Bool { + probe_blocking_count(p: enrolled_contrast_probe) >= 1 + && probe_blocking_count(p: unenrolled_contrast_probe) == 0 + && probe_where_advisory_count(p: unenrolled_contrast_probe) >= 1 +} + +// THE DEBT CONTRACT, ASSERTED AT SPELLING GRAIN. The roster's UnenrolledNoTableRow rows are exactly +// the three, and each of them admits a violating literal today. Enrolling one without deleting its +// row reds here; adding a fourth reds the join above. Neither can happen quietly. + +test fn w_unenrolled_roster_holds_exactly_three_spellings() -> Bool { + let unenrolled = where_predicate_rows_of_enforcement( + rows: where_refinement_predicate_vocabulary, + wanted: UnenrolledNoTableRow + ) + count(unenrolled) == 3 + && (unenrolled |> all(r => + r.spelling == "oci_path_component_syntax" + || r.spelling == "oci_tag_syntax" + || r.spelling == "c_translation_unit_basename_safe")) +} + +test fn w_unenrolled_predicates_admit_a_violating_literal() -> Bool { + where_predicate_probes + |> filter(p => + p.spelling == "oci_path_component_syntax" + || p.spelling == "oci_tag_syntax" + || p.spelling == "c_translation_unit_basename_safe") + |> all(p => probe_blocking_count(p: p) == 0 && probe_where_advisory_count(p: p) >= 1) +}