Repository navigation
The where-refinement predicate vocabulary, joined to the compiler that decides it - #10304
Conversation
…t decides it
A where-refinement predicate is a bare identifier with no declaration
binding anywhere in the pipeline: 02_parse accepts any identifier in its
unparenthesised arm, and 04_infer decides what it MEANS by matching that
string against three hand-written name-keyed tables. So the tables are a
second authority for a predicate's meaning, forked from the declaration
that already states it wherever one exists.
Census over all 4663 .dag files: 271 declaration sites, 15 distinct
predicate spellings. Seven 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. Three grounded, decidable String -> Bool predicates
are in no table at all -- two of them declared in the same file as an
enrolled pair -- so a plainly invalid literal at those refined positions
compiles with zero refusals, while the enrolled siblings wall.
This lands the join that did not exist: one row per spelling carrying the
compiler's enforcement class and whether a declaration grounds it, and a
witness that executes every row against the real v1 compile path. The
join runs in both directions by spelling, so a spelling added to one side
alone reds rather than being skipped, and the three unenrolled rows are
held as a monotone debt contract at spelling grain -- enrolling one
without deleting its row reds, adding a fourth reds.
Honest at rung 2, mechanically preventable, and the row says so: the
invalid state stays writable and safety depends on the witness staying
enrolled. The observable is the two-way partition {refuses a violating
literal} vs {never refuses}, because the census surface projects a
diagnostic's class and subject name but not its reason; the four-way
class split is author-vouched and the file states which half executes.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
…hread Asked the lane carrying gunbc#10146 whether its ResolvedFormal / DeclarationBoundFormals coproduct generalises from call formals to where-predicates. It does not, and the reuse 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, not the carrier, so the predicate move owes its own substrate carrier keyed by DeclarationRef rather than spelling, as a follow-on after #10146 rather than folded into it. This lands in the dissolution-trigger row because a refusal that lives only in a chat message is not an authority: the next person to propose the reuse would not find it, and would re-derive the fork the refusal prevented. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
The floor refused at parse with 45 errors, all in these two files, all one class: DESIGN section 4c admits only standalone leading // blocks attached to module-scope declarations. I had field notes inside a type body, a note inside a data list literal, and a trailing ceiling block with no declaration after it. Each is moved above the declaration it describes; no prose is lost and none of it changes meaning. Also adds NonEmptyStr to the std.types import. The roster used it in where_predicate_decl without importing it, which produced two unlisted-import-use advisories -- rows in a class this lane does not own and therefore has no business creating. WHY THE LOCAL RUN MISSED IT, since the instrument gap is the reusable part: an entry-closure run (--entry <witness> --claim-run) resolves and executes the witness without applying the annotation-grain rule, so all seven assertions passed green against the real corpus while the file was inadmissible to the compile-clean gate. Those are two different claims. A whole-tree `gunbc compile --source-root dag --source-root src/v2 --target dag` DOES apply it, reports zero annotation errors here, and is what verified this fix before it was pushed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
The floor passed and required_floor_disposition.tsv shows all seven identities as planned_as_changed_witness / passed -- so they executed, and were not selected out. But they are the ONLY seven rows of that disposition in a 15984-row floor, and the arm name says why: they ran because these files CHANGED. The floor's other arms are 3595 planned (inside the gate closure) and 11824 declined_outside_gate_closure. The sibling settles which arm this 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 same run. So this is a change-triggered control, not a continuously-executing one, and the roster's claim that safety depends on the witness "executing and staying enrolled" was reading as more than the evidence supports. The consequence is narrower and worse than the general point, so both files now state it: an edit to this roster or 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 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. Enrolling a sixteenth predicate without touching either file would not red. The wall catches ROSTER drift, not COMPILER drift, and only the latter is the side that moves when someone enrols a predicate. Next-rung trigger is named as the capability: this module inside the required gate closure, reached from the gate seeds rather than by having been edited, sufficient for the join to execute on runs that touch neither file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
The brief required the witness cover the collision case -- a spelling
standing for more than one declared meaning must go loud -- and
w_roster_spellings_are_pairwise_distinct already did, since two rows
claiming one spelling is how a second meaning enters the roster. But the
file described it as a byproduct of the bidirectional join rather than as
the collision wall, so a reader could not tell that was its purpose and
nothing said what population it ranges over. An assertion that satisfies a
requirement without being legible as satisfying it is how a check later
gets cited for coverage it does not have.
It now says both halves. It ranges over the ROSTER and catches a spelling
given two groundings there. 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.
That is stated in the file rather than left as an impression, because the
earlier draft of this lane's report called name-keyed predicate identity
"silent wrongness" when nothing in the tree currently triggers it.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74
|
Landing this. Two files, no contended paths, and it clears the bar on substance rather than only on the gate. Admissibility, at the exact head Worth recording that the dashboard summary said The floor red earlier on this branch was not this change. It refused on four rows in two Why the witness earns the merge. The roster-to-probe relation is an identity join in both directions — every roster spelling has exactly one probe and every probe spelling has exactly one roster row — rather than a count comparison, with pairwise distinctness asserted separately so two rows claiming one spelling goes loud. The file also states, in its own comment, that this witness is change-triggered rather than continuously executing. That is the honest rung and the author added it after measuring their own enrolment claim and finding it weaker than they had written. A roster that says which arm it lands in is worth more than one that reports green. 🤖 Generated with Claude Code |
What this closes
A where-refinement predicate (
type NonEmptyStr = String where non_empty) has no declaration binding anywhere in the pipeline.v1.compiler.parseparse_single_predicateaccepts any identifier in its unparenthesised arm, andv1.compiler.inferthen decides what that 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 the 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 (§3).
The census that motivated it
Over every
.dagfile underdag/,src/v1,src/v2,fixtures: 271 where-refinement declaration sites, 15 distinct predicate spellings. Seven of the fifteen are grounded by a declared totalBoolfunction and eight are not — and the compiler's treatment is uncorrelated with which:oci_other_digest_algorithm/oci_other_digest_encodedare declaredString -> Bool, are enrolled, and wall at literal construction sites.oci_path_component_syntax,oci_tag_syntax,c_translation_unit_basename_safeare declaredString -> Bool, structurally identical, two of them in the same file — and are in no table at all, so they are permanently advisory.The discriminator is not decidability, grounding, or any property of the predicate. It is whether a human added a table row. That is §5's wall after grounding: decidable, grounded, unbuilt.
The instrument is a character-level state machine that strips
//annotation blocks and string literals before matching\bwhere\s+<ident>. This matters and is not fussiness: matching raw lines returns 38 "names", 23 of which are English prose out of multi-linedata …: Stringrows (the,a,construction,Symbol), and it simultaneously keeps a hit that lives inside a string. Wrong in both directions.What lands
dag/gunbc/where_refinement_predicate_vocabulary.dag— one row per predicate spelling, carrying the compiler's enforcement class and whether a declaration grounds it. The rows carry no occurrence counts and no site lists: a count copied into a row is a transcribed measurement rotting away from the tree that produced it (§6). Identity is the fact this roster owns, because identity is what the compiler gets wrong.groundingis a coproduct rather thanDeclarationRef?because "nobody wrote this down" and "somebody wrote it down and we ignore it" owe different things, and an optional would make them the same absent value.dag/test/claim/where_refinement_predicate_vocabulary_witness_test.dag— the executing consumer. Fast lane, deliberately nottest/claim/long/, whichgunbc.witness_deferral_freezedocuments as the path-deferred lane that executes nowhere; the existing where-refinement witness family already sits there carrying its own note admitting nothing has ever run it on CI.Evidence — executed, with the reds
Built from this branch and run against the real corpus. Command for each:
./target/release/gunbc run --source-root dag --source-root src/v2 --entry dag/test/claim/where_refinement_predicate_vocabulary_witness_test.dag --function <name> --claim-run.All seven assertions PASS. Two falsifiers establish that they can fail:
oci_tag_syntax's expected class from "never refuses" to "refuses"w_every_rostered_predicate_behaves_as_its_row_declaresrc=1 FAILw_every_roster_spelling_has_exactly_one_proberc=1 FAILw_unenrolled_roster_holds_exactly_three_spellingsrc=1 FAILBoth mutations were reverted; neither is in this diff.
The contrast control is the load-bearing one.
w_one_literal_two_predicates_one_refuses_and_one_does_notcompiles two sources differing only in the predicate spelling, with the same literal"NOT A TAG!!":lower_hex_40refuses it,oci_tag_syntaxaccepts it. Without that pair, everyexpected_refusal: falserow would pass for the wrong reason if the harness could not refuse anything at all — and the three unenrolled rows would read as MEASURED when they were merely UNREFUTED.The join is bidirectional and by spelling, not a count: every roster spelling has exactly one probe and every probe spelling has exactly one roster row. A count equality is satisfied by any two sets of the same size, and a one-directional check over a table you also author is satisfied by narrowing the table.
Rung, stated honestly
Rung 2, mechanically preventable, and the row says so. The invalid state stays fully writable — nothing stops an author writing
type T = String where whatever_i_typedtomorrow — and safety depends entirely on this witness executing and staying enrolled. It is not a wall and must not be cited as one.Two ceilings are written into the files rather than papered over, because both cost me the assertion I wanted:
"predicate deferred at compile time"and"predicate not enforced at compile time"are indistinguishable through it, and what executes is the two-way partition {refuses a violating literal} vs {never refuses}, not the roster's four-way class. The deferred-vs-unenrolled split is author-vouched. Next-rung trigger: the census projecting the diagnostic reason.concept_decl_facts_livemarshals onlyDisjandConjtype items and drops the refinement annotation, so the corpus population cannot be re-derived inside a.daglens without a new host reader — and adding one would be new hand-maintained Rust, which the v1 exit lane closes rather than grows. So "are these 15 all of them" is author-vouched, and the missing reader is named as the next-rung trigger instead of being written.The three unenrolled rows are a monotone debt contract at spelling grain: the subject universe is closed by the roster, membership is checked by identity rather than count, and every removal is forced — enrolling one without deleting its row reds, adding a fourth reds.
What this deliberately does NOT do
There is a standing declared trigger in the tree naming a different end-state for this same subject —
feature:where-refinement-predicate-coproduct, cited bywhere_refinement_deferral_reason_scaffold_noteinv1.std.coreand by the predicate min-length tables inv1.compiler.infer. §4b(3) is categorical that a declared drop is retired by its trigger and by nothing else, so this PR does not supersede it, and the roster's own trigger row says so explicitly. Choosing between a resolved declaration and a closed coproduct is a trigger change owed in the open as its own decision.Enrolling the three names in the existing tables is explicitly not the fix and would not discharge the row: it would grow the forked authority the row exists to record, which §2 calls a failed decomposition.
The trigger row also records a refusal obtained from the lane carrying #10146: its
ResolvedFormal/DeclarationBoundFormalscoproduct does not generalise to predicates — its fields areparameter_identity,declared_type,declaration_bound_conformance,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. What generalises is the pattern, not the carrier. The predicate move therefore owes its own substrate carrier keyed byDeclarationRefrather than spelling, as a follow-on after #10146. That is in the row rather than in a thread because a refusal that lives only in a message is not an authority.🤖 Generated with Claude Code
https://claude.ai/code/session_018WC97AtZWzFxLktD4LfF74