The quantifier census: 100 walkable domains out of 1005 - #2793
Merged
Conversation
`tri quantifiers report`. Reading only: no parse changes, no lowering, no generated artefact, no discard count moves. WHY THIS AND NOT A LOWERING. Three independently written proposals for #2774 -- one arguing to capture and never lower, one to enumerate finite domains, one to split the four backends apart -- were judged through two adversarial lenses each and all three survived. They disagree about the lowering and they agree exactly about the FIRST STEP: report before you lower, because the ceiling cannot be chosen without the distribution of domain sizes, and nobody had measured it. quantified clauses found 1005 colon 12 invariant name: forall c : Cfg, ... prefix 858 forall input : InferenceInput suffix-all 120 assert p(a) == p(b) for all Trit suffix-any 15 ... for any a, b in {1, -1} DOMAIN, from declared types only, ceiling 65536 walkable 100 finite but over the ceiling 222 unbounded 544 no binder this can read 139 largest walkable domain 65536 (specs/igla/race/ternary_mac.t27:941) ALL 135 SUFFIX FORMS HAVE NO READABLE BINDER. `for all Trit` names a type with three values and no variable to range over it; `for any a, b in {1, -1}` names a set the language has no syntax for. The small domains are exactly the ones written without a binder, which is the opposite of convenient. WHAT `|D|` MEANS, and what it deliberately does not: * computed from DECLARED TYPES ALONE. A binder over `Trit` is 3 whatever the body says about it. * `BOTTOM` (printed `unbounded`) is absorbing, and AN UNRESOLVED NAME IS NOT ASSUMED SMALL -- `string`, `[]T` with no pinned length, and a type this cannot resolve are all unbounded. * 15 struct names have MORE THAN ONE definition in the corpus and are treated as unbounded. Picking one would change `|D|` by an unbounded factor with nothing recording which was picked. * NO GUARD IS READ. `x.len() == 4` narrows nothing here. That is the part that needs a semantics, and this report must not be the thing that quietly decides one. Six tests, four of them for what it must NOT conclude: an unknown type is unbounded rather than 1, an unpinned array length is unbounded rather than its element size, a struct defined twice is unbounded even though its fields resolve, and a prose suffix yields no binder rather than a wrong one. Refs #2774 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 09:44:55 UTC
Summary
Seal Status
|
…in (186-188) Three incompatible designs agreed on one first step, which is the step that cannot be wrong. I validated a spec fix against a line that was itself failing. And the default for an unresolvable type must be the answer that makes the tool refuse. Refs #2754, #2774 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
PR DashboardGenerated at: 2026-08-29 09:46:08 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
feat(tri): the quantifier census -- 100 walkable domains out of 1005
tri quantifiers report. Reading only: no parse changes, no lowering, nogenerated artefact, no discard count moves.
WHY THIS AND NOT A LOWERING. Three independently written proposals for #2774 --
one arguing to capture and never lower, one to enumerate finite domains, one to
split the four backends apart -- were judged through two adversarial lenses each
and all three survived. They disagree about the lowering and they agree exactly
about the FIRST STEP: report before you lower, because the ceiling cannot be
chosen without the distribution of domain sizes, and nobody had measured it.
ALL 135 SUFFIX FORMS HAVE NO READABLE BINDER.
for all Tritnames a type withthree values and no variable to range over it;
for any a, b in {1, -1}names aset the language has no syntax for. The small domains are exactly the ones
written without a binder, which is the opposite of convenient.
WHAT
|D|MEANS, and what it deliberately does not:Tritis 3 whatever thebody says about it.
BOTTOM(printedunbounded) is absorbing, and AN UNRESOLVED NAME IS NOTASSUMED SMALL --
string,[]Twith no pinned length, and a type thiscannot resolve are all unbounded.
as unbounded. Picking one would change
|D|by an unbounded factor withnothing recording which was picked.
x.len() == 4narrows nothing here. That is the part thatneeds a semantics, and this report must not be the thing that quietly
decides one.
Six tests, four of them for what it must NOT conclude: an unknown type is
unbounded rather than 1, an unpinned array length is unbounded rather than its
element size, a struct defined twice is unbounded even though its fields
resolve, and a prose suffix yields no binder rather than a wrong one.
Refs #2774
Co-Authored-By: Claude Opus 5 noreply@anthropic.com