Repository navigation
Call-shape wall: refuse unknown argument labels and surplus positionals at the direct-call seam - #7519
Merged
Conversation
The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rections adopted, receipts verified
Adopted (all verified on main this pass):
- Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not
statically propagated: v2.std.refinement exists, NonEmptyList fixture +
green cardinality_fold_propagation_test exist, and
refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the
carrier proves nothing). New Sec 4b: the operator independently
re-directed this exact guarantee on 2026-07-04
(interface-summary-declared-use-arity.md Sec 3.1, "hard error in the
language") — the intent is not lost; the lattice design pass (FLAG E)
never started.
- Failure history rewritten (Sec 2): the exemption dates to 2026-06-08
(a13fb57), pre-bankruptcy; correctness-dimensions.md marked type
safety "Yes (blocking)" while return position was unchecked — so the
ledger overstated, then the auditable contract was deleted. The
pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a
deliberate total semantics, not a priced-out wall.
- Status vocabulary widened to the review's 11-state lattice; v2 terminal
calibrated (validate_then_compile door + loop-bound wall are real;
InferredTree is still not a proof boundary); application-arity row added
(formal-driven walk, positional fallback for misspelled labels,
ArityMismatch is constructor-arity); PatternLookupBlocked's silent []
arm confirmed (PatternDynamic does diagnose — review corrected there).
- Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5
behaviors" is stale against v2.std.node's six (Match) — the guarantee
authority lands as .dag rows, never hand-edited prose.
- Sequencing reconciled to 7 stages: claims authority + expecting-red
probe corpus together; zero-resolution method wall now, ambiguity wall
census-first; cardinality vertical slice third.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…el (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…guarantee-ladder roadmap section
Corrections, each verified against main before adoption:
1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record
specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque
... every proof-carrier is presently forgeable") was false as stated;
corrected to an audited-status claim: sole_constructor is the
candidate wall, completeness for generic carriers unverified. The
earlier keyword-set inference is withdrawn in the Sec 10 ledger.
2. Subject grain: rung honesty is measured at a declared acceptance
boundary; a class's rung is the MINIMUM across in-scope paths (the
interpreter refuses the mislabeled call that order_typed_call_args
reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1
carrier gains subject_grain/acceptance_boundary/compile_mode/
realization_target/covered_population.
3. Seed rungs demoted: return/data/generic, field-through-generics,
exhaustiveness, cardinality, full ==-class, and L4 all to
UnknownUnmeasured (compile admission proven is not runtime
disposition proven); census marked specimen-denominated; unknown-
method R0 scoped to the interpretation path.
4. Dissolution on climb amended in DESIGN 4b: production handling
dissolves; the RED + positive controls REMAIN enrolled as the
evidence the higher rung stays real.
5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows +
witness-test fixture migrated); the guarantee-recovery row now
carries BOTH anchors typed, not one typed + one in prose. Carrier
note records that List admits [] — the exact cardinality gap the
ladder tracks — with the doc-graph witnesses as the interim wall.
6. cardinality_fold_propagation_test relabeled everywhere as manual
value-level specimens (length homomorphism over literals + runtime
refine_byte); "not new design" softened to the accurate scope
statement; the roadmap cardinality node re-briefed accordingly.
7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a
generic dimension mechanism; extension-vs-redesign is an open audit
question that roadmap pricing must carry.
8. Sec 1 "was not built" -> "never completed as an exhaustive
acceptance contract"; Sec 11 queue updated (correctness-dimensions
done; sole_constructor completeness audit added).
Additions (operator direction): ROADMAP gains the "Guarantee ladder —
climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes
in ticket format with dependency edges (probe corpus gates the four
floor walls; carrier gates cardinality slice, emitters, prevalence;
exemption removal gates on the call-shape + inhabitance walls). The
capability node is the sole_constructor completeness audit. State-vs-
work split recorded on the carrier: rung STATE lives in the Stage-1
claims carrier and is emitted (ladder-census-emitters node); roadmap
nodes track CLIMBS.
Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md
projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap
authority 35/35, model 9/9, focus 12/12.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…bol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ruction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…icket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…r (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…ne, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…r (review 45545) The first edge set let compiler-accepted-obligation-closure land while floor-method-ambiguity-wall and cardinality-vertical-slice stayed open — the door would have certified "every required judgment established" over two required-open judgments (the grid marks the cardinality seam P0.2 minimum-R2 and ambiguity part of resolved identity; the verdict's spine routes ALL P0 obligations through the door). Both are now prerequisites of the closure; residual prevalence depends on the door alone. Authority 38/38, focus 12/12, page 28/28, drift 8/8; regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
ct_call_shape_wall_witness_test joined compiler_tests_rust without its LanguageSourceScaffoldRow, so the exact-equality enrollment witness (compiler_tests_rust_blobs_are_all_rostered, 29 declared vs 28 rostered) would red on CI. Row added with the same hand-assertion scaffold trigger as its peers and enrolled in the roster; witness re-run green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Contributor
Author
|
review 45655 (cursor REQUEST_CHANGES) addressed: |
added 2 commits
July 31, 2026 21:04
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
The floor failed on src/v2/test/claim/bash_program_fold_support.dag with eight "call shape mismatch calling 'list_append': no parameter named 'xs'" refusals. Not this lane's code: the file is byte-identical to origin/main and no commit here touches it. It is main's own #7519 call-shape wall firing on a call site that predates it — list_append is declared (left, right) in v2.std.algebra and this file passed xs:/ys:, which the wall now correctly refuses and which was silently accepted before it existed. Exactly the fail-open class #7519 closes. It surfaced here rather than on #7519 because the two runs have different reach: a PR-scoped compile-clean does not open test entries, and the discovery corpus does. This merge is the first full-corpus run since that wall landed. Same lesson this lane already paid for twice — the instrument's reach decides what the wall appears to prove. Relabelled the eight arguments left:/right: in call order, preserving operand order. One edit had to be backed out immediately: line 205's inner call is list_map, whose parameter genuinely IS xs (v2.std.algebra list_map(xs, f)), and a blind label rewrite had renamed it. Printing the result caught it; a same-name-different-function rename is precisely what a mechanical sweep gets wrong. Scanned the rest of the corpus for the same idiom: every other list_append call site already uses left:/right:, and the remaining xs: matches belong to fold_list, length and list_map, which declare xs. This file was the only offender. Verified: the previously failing entry resolves (claim_batch exit 0); whole-tree compile-clean 0 blocking, 5639 advisory, zero call-shape mismatches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Scope addition on this head (rode in with the same lane's work): repair of a silent-red enrolled wall found by tidy-deer-730 during the #7484 main integration. |
22 of 24 tasks
briansrls
pushed a commit
that referenced
this pull request
Aug 1, 2026
* WIP: p0 - protect the live system
* Refuse an unresolved method instead of inheriting the receiver type
An unknown method reached `method_pipe_map_keys_values_fallback`'s else-arm,
which returned the RECEIVER's type with an empty diagnostic list. So
`xs |> filter_map(..)` on a `List<Int>` typed as another `List<Int>` — a
success-shaped answer that survives a whole collection pipeline and looks
plausible to downstream inference, with the expression stamped
`PlainMethodSemantics` as if it had resolved. Nothing refused until the
interpreter hit its closed dispatch default and returned
`InterpError::Unimplemented { what: "method 'filter_map'" }`: whole-tree
compile reported zero blocking errors while live dispatch returned HTTP 500
(#7479).
That arm is deleted. Method absence is now decided at compile time and split
into the two states it actually has (DESIGN §5 — state-space conflation):
MethodNotFound receiver type fully resolved, so the method is
PROVABLY absent — the decidable refusal.
MethodExistenceUndecided receiver under-resolved (type variables present),
so absence cannot be proven — a typed, located,
COUNTED frontier refusal, never a silent widen
back to `recv_rt`.
Both arms return `error_type`, not `recv_rt`: `node_type_compatible` treats
`error_type` as compatible with everything, so one located refusal does not
cascade into derived mismatches at every downstream consumer.
Green by execution, with the controls:
xs |> deliberately_nonexistent_method() RED, names method + receiver type
xs |> filter_map(x => x) RED — the literal #7479 incident
xs |> filter(..) |> map(..) GREEN — algebra templates resolve
at tier0 and never reach the arm
Rationale rides on the carrier (`method_existence_wall_note`) with its
dissolve-on: primitive-realization-single-authority, at which point existence
is decided against one PrimitiveDefinition identity rather than the
structural/service tier pair, and the Undecided frontier closes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Decide method existence and declared-type conformance at compile time
Two v1 fail-opens in the same shape: knowledge is missing, so the compiler
constructs a success-shaped answer and the lie surfaces at runtime.
METHOD EXISTENCE. An unresolved method fell through
`method_pipe_map_keys_values_fallback`'s else-arm, which returned the
RECEIVER's type with an empty diagnostic list, and the expression was stamped
`PlainMethodSemantics` as if it had resolved. So `xs |> filter_map(..)` on a
`List<Int>` typed as another `List<Int>` and survived the whole pipeline;
nothing refused until `InterpError::Unimplemented { what: "method
'filter_map'" }` — whole-tree compile green, live dispatch HTTP 500 (#7479).
The predicate deciding absence is the load-bearing part, and the two obvious
ones are unsound — both rejected on measured whole-tree evidence, not taste:
is_fully_resolved alone A type can carry no type variables and still be
an inference artifact. `NonEmptyStr` (declared
`String where non_empty`) arrives as
Product(NonEmptyStr) instead of peeling to its
String base, reding 8 correct `.length()` sites
in extdeps/filesystem/linux.dag while the
identical `text.length()` in extdeps/mercurial
stays green; a coproduct payload bound by
pattern destructuring arrives typed
Primitive(ok) and reds a correct `list_push`.
the receiver algebra profile free_monoid_scalar_templates omits `count`
while the interpreter dispatches it natively,
so `String.count()` reds against a profile the
runtime contradicts — the five-way primitive
fork, measured.
Fabricating a refusal is the mirror image of the fabricated success being
deleted, so the predicate is composed of two declared authorities rather than
one minted here: refuse when the name is absent from `std.methods`
declared_method_names AND the receiver is fully resolved. The roster answers
"is this a substrate method at all"; the receiver gate answers "could this be
a product field holding a callable" — exactly the legitimate
`LexMatchThunk { apply: fn(s) }` idiom in v2's tokenizer, whose 7 sites would
red without it. Whole-corpus verdict: zero false positives, and a second real
latent defect caught beside #7479 — `env.clone()` (05_emit_rust.dag:9009,9831),
a Rust-ism with no .dag definition and no interpreter arm, fixed here.
The undecidable residue is `MethodExistenceUndecided`: typed, located and
COUNTED but non-blocking (the is_error_diagnostic partition, UnlistedImportUse
precedent), so the frequency of the frontier stays observable rather than
zeroed by construction. Both arms return error_type, never recv_rt, so one
located refusal does not cascade downstream.
DECLARED-TYPE CONFORMANCE. infer_item passed the declared return into body
inference as `expected` but then kept the declaration's inferred return
regardless of what the body produced, so `fn f() -> Int { "wrong" }`
typechecked with zero diagnostics. Three positions now check against their
declaration — fn body vs declared return (both arms) and `data` value vs
annotation — through the EXISTING node_type_compatible, which is permissive by
design: an error type, type variable, or under-resolved shape answers
compatible, so the wall fires only where the mismatch is proven.
Green by execution. REDs: `deliberately_nonexistent_method`, `filter_map`,
`fn f() -> Int { "a string" }`, `data d: Int = "a string"`. GREENs:
filter/map/fold/flat_map pipelines, `String |> count`, `Int?` from `first`,
and the full [src/v1, dag] closure through regen.
Two upstream defects are named by the measurement and deliberately not fixed
here, each a promotion trigger that would let the wall decide more: a
where-refinement alias resolving to a Product instead of peeling to its base,
and a coproduct payload binding typed as the variant name.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Narrow the conformance wall to what it can actually prove
The method-existence wall landed sound. The declared-type conformance wall
did not: running it over the corpus found FOUR independent classes of correct
code that node_type_compatible reports as a mismatch, because it compares
names across representations it never peels.
optionality, two ways `-> String?` carries optionality in
return_cardinality while the body produces the
nominal Optional coproduct — 4 correct sites in
05_emit_rust.dag
brand aliases `Hash` is `ContentHash` is a branded String — 3
correct sites in dag_collect_support.dag, the same
class as NonEmptyStr arriving as Product(NonEmptyStr)
anonymous literals the corpus writes `[ { name: .., .. } ]` without
repeating the nominal type — 8+ correct rows in
dag/std/algebra.dag
cardinality location resolved_type() drops the declaration's optional
marker (fixed: the declared side now goes through
preserve_outer_optional_cardinality)
Each was found by RUNNING the wall, never by reasoning about it, and the list
is not known to be exhaustive — which is exactly why chasing them with
exemptions was the wrong move. Four ad-hoc carve-outs leave a wall that is
neither principled nor trustworthy, and fabricating a refusal is the mirror
image of the fabricated success the wall exists to delete.
So conformance uses the same predicate shape the method wall settled on:
positive establishment. Judge only when both sides are ground kernel scalars —
plain shape, Required cardinality, name in std.types kernel_type_set — because
then a name difference IS a real difference, with no alias, brand, container,
coproduct or cardinality representation in between. That admits the whole class
the report named and admits nothing it cannot prove. Everything wider is
UNJUDGED rather than silently passed: it is the wall's declared frontier, and
each class above is a promotion trigger carried on the carrier note.
Witnesses are enrolled and executing, not scratchpad probes:
method_existence_wall_witness and declared_type_conformance_witness in the
emitted compiler_tests, both green, both discriminating (the asserted
diagnostic lists were empty before the walls).
4 REDs deliberately_nonexistent_method · filter_map · fn f() -> Int
{ "a string" } · data d: Int = "a string"
8 GREEN filter/map/fold/flat_map pipelines · String |> count · Int? from
first · conforming returns and data
regen_stage0 --verify: regen_divergence_count=0 — committed stage0 matches a
fresh self-compile, so the seed is at its fixed point with both walls active.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* chore: regenerate drifted generated artifacts (ci auto-heal)
* WIP: p0 - protect the live system
* Restore the seed the auto-WIP commit stripped
7b0ecdd8ea ("WIP: p0 - protect the live system") captured my working tree
mid-experiment and committed it. The tree at that moment held a deliberately
reverted seed: I had checked out the pre-wall stage0 to run a CONTROL — to
establish whether the OOM in
module_grain_affected_decision_discriminates_under_wiring_perturbation was
caused by this PR or pre-existing. (It is pre-existing: the test is SIGKILLed
identically on the pre-wall seed with 101 GB free, consistent with the repo's
own "whole-tree resolve OOM risk in test harness" note.)
The commit therefore deleted the walls from the seed while leaving them in the
.dag authority: 300 deletions across v1_std_core.rs (both diagnostic variants),
v1_compiler_infer.rs (the composed predicate and the conformance gate),
cli_run.rs (the histogram arms), compiler_tests.rs (both witnesses), and
lib.rs (the std_methods module). That is the exact drift the regen gate exists
to catch, and it was pushed.
The seed is restored byte-identical to 2b4380df3c ("chore: regenerate drifted
generated artifacts"), the last state where authority and seed agreed.
Re-verified after restore, not assumed:
regen_stage0 --verify regen_divergence_count=0 — committed stage0 matches a
fresh self-compile
control matrix 4 REDs (deliberately_nonexistent_method, filter_map,
fn f() -> Int { "a string" }, data d: Int =
"a string"), 8 positive controls green
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Decide method existence per receiver, not per name (codex review 45327)
The review is correct, and confirmed by execution. Gating on membership in a
declared method-NAME roster admits any rostered name on ANY receiver, so:
fn g(xs: List<Int>) -> Bool { xs |> starts_with("x") } compiled clean
fn h(xs: List<Int>) -> String { xs |> to_upper() } compiled clean
Both landed in MethodExistenceUndecided, which is non-blocking, so
`emittable_graph` accepted them — a fail-open route to exactly the runtime
failure this P0 wall exists to remove. Worse, the diagnostic LIED about its
cause: it reported the receiver as "under-resolved" when
Container(List,Primitive(Int)) is fully resolved. I had also reported
`String |> count` as a passing positive control; it was passing through this
same hole and emitting an advisory, so that green was hollow.
The predicate is now PER-RECEIVER: refuse when kernel_profile_lookup returns a
profile for the receiver's canonical container kind. tier0 has already
consulted that profile's algebra templates and missed, so reaching this arm
with a kernel-profiled receiver PROVES absence from the receiver's complete
declared surface. Same authority tier0 reads; no second relation.
That predicate was blocked by ONE thing, and it is a real §3 fork now fixed
rather than worked around: the kernel profiles disagreed with the interpreter
about `count`. The interpreter dispatches "length" | "count" | "size" natively,
while free_monoid_scalar_templates (String) and partial_function_templates
(Map) declared only `length`. Measured over the whole [src/v1, dag] closure the
gap was exactly two shapes — String |> count and Map |> count (9 sites) — and
both profiles now declare `count`, mirroring their own `length` row. So those
calls resolve at tier0 and never reach the wall.
Non-kernel receivers stay Undecided, and refusing there WOULD fabricate: a
where-refinement alias arrives as Product(NonEmptyStr) rather than peeling to
String, a coproduct payload arrives typed Primitive(ok), and `apply` is a
product FIELD holding a callable (the LexMatchThunk idiom). Undecided now means
exactly one thing — receiver surface not established — instead of doubling as a
name-grain escape hatch.
The name roster added in the previous commit is deleted along with its
generated module and registry row: the per-receiver predicate does not consult
it, and an unused authority is dead scaffolding.
6 REDs deliberately_nonexistent_method · filter_map · starts_with · to_upper
· fn f() -> Int { "a string" } · data d: Int = "a string"
9 GREEN 0 diagnostics, not merely no MethodNotFound — incl. String |> count
and Map |> count, now genuinely resolved rather than fail-open
The witness carries the review's two cases as REDs, so a regression to a
name-grain predicate fails the test rather than passing it.
regen_stage0 --verify: regen_divergence_count=0.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Fix the missing list separator, and re-derive the seed after the main merge
TWO defects, one found by review and one by the merge.
MISSING SEPARATOR (claude review 45347, correct). The `count` row added to
`partial_function_templates` was not comma-separated from the `length` row
above it, so two record literals sat adjacent inside the list. Fixed.
The reason it survived is worth recording, because it is the same class this
PR is about: THE PARSER SILENTLY ACCEPTS A MISSING LIST SEPARATOR. Probed
directly — `[ { name: "a" }, { name: "b" } { name: "c" } ]` compiles with 0
diagnostics. So the malformed literal passed regen, a whole-corpus compile,
the fixed-point verify, and a 15-case control matrix without a murmur, and
`Map |> count` resolved green off it. No amount of execution would have caught
this; it took someone reading the diff. A grammar that accepts juxtaposed
elements cannot tell a two-element list from a three-element one, which makes
a dropped comma a silent semantic change — unowned, and named here.
STALE SEED AFTER THE MERGE. Merging origin/main brought #7481, which added
literal CR/NUL characters to dag/std/types.dag AND the emitter fix that
escapes them (\x0d / \x00, target-independent). The merge kept my side of the
seed, which predates that fix, so the committed stage0 could no longer emit
the .dag it is derived from: `regen_stage0 --verify` failed with "bare CR not
allowed in string" in a freshly emitted std_types.rs. Authority and seed had
diverged — precisely the drift the regen gate exists to catch, caught.
Re-derived by bootstrapping from main's seed (which carries the escaping fix)
and running the two-pass regen, rather than by hand-patching the seed.
Re-verified after both fixes, not assumed:
regen_stage0 --verify regen_divergence_count=0
control matrix 6 REDs; positive controls 0 diagnostics
witnesses method_existence_wall_witness ok,
declared_type_conformance_witness ok
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Make the positive controls assert zero diagnostics (codex review 45357)
The review's second finding is correct: both witnesses filtered the green
module's diagnostics to the BLOCKING variant only (MethodNotFound /
TypeMismatch), so an advisory MethodExistenceUndecided passed unnoticed.
That is not hypothetical — it is exactly how I came to report `String |> count`
as a passing positive control when it was in fact resolving through the
non-blocking arm and emitting an advisory. The witness was structurally unable
to tell "this call resolves" from "this call does not resolve but the arm is
advisory", which is the whole distinction the wall turns on.
Both controls now assert `green_result.diagnostics.is_empty()` — no diagnostic
of any severity. A legitimate method that stops resolving, or a conforming
declaration that starts producing an advisory, now fails the witness instead of
passing it.
Verified: both witnesses green under the strengthened assertion, so the
positive controls demonstrably resolve rather than being admitted by an arm.
regen_stage0 --verify: regen_divergence_count=0.
The review's first finding — that MethodExistenceUndecided is non-blocking, so
emittable_graph still emits — is answered separately on the PR with the
measured site list, because the fix is not available in this PR: 7 of the
Undecided sites are the v2 tokenizer's own LexMatchThunk { apply: fn(s) }
idiom, so blocking today refuses the compiler v2 depends on.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Remove a foreign PR's Rust slice that a bootstrap checkout dragged in
Bootstrapping the seed required a compiler that could emit the merged .dag, so
I ran `git checkout origin/main -- src/v1/stage0/src/`. origin/main had
advanced past this branch's merge base (da37e37f9b) to b519142647, so that
path-scoped checkout imported the stage0 slice of #7483 ("Exclusive cost
partition + selected-set closure overlap") — its hand-maintained bins — while
leaving the rest of that PR behind.
The result was four files in this diff that are not this PR's work:
measure_selected_closure_overlap.rs (a new file, and orphaned — Cargo.toml at
this branch's base does not declare the bin, so nothing built it), plus edits
to claim_batch.rs, claim_executor.rs and measure_whole_tree_resolve.rs.
Half of someone else's merged change, presented as mine, is not something to
carry to review: it misattributes the work and it is a partial import whose
.dag half is absent. All four are restored to the merge base; main's own
versions land normally when this branch merges.
Caught by reading the diff surface after a reviewer's summary described "two
new measurement bins" I had not written — a reminder that a path-scoped
checkout against a moving ref imports whatever else has landed there.
Verified after the strip: cargo build clean, regen_stage0 --verify
regen_divergence_count=0.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* WIP: p0 - protect the live system
* Peel the refinement base so the wall DECIDES, and key the frontier on receiver shape
Two independent signals said the same thing about the (module, method)
frontier key: codex review 45398 found it as a fail-open (a NEW `apply` in
v2.compiler.tokenize inherited the pass on any receiver, so the note's claim
that no new fail-open could enter was false), and the first whole-corpus CI run
found it as an undercount — the roster was measured over the v1 self-compile
closure alone and seven sites in three unseen modules went red.
The larger finding is that the biggest "undecidable" class was never
undecidable. resolve_method_receiver_type short-circuits on connective == Conj,
and a where-refinement type IS a Conj, so `String where non_empty` reached
method lookup as Product(NonEmptyStr) and String's algebra profile was never
consulted. Peeling to the base moves 12 corpus sites out of the residue in both
directions at once: the correct `.length()` calls resolve, AND a method genuinely
absent from the base now refuses as MethodNotFound instead of resting in the
frontier. Widening what the wall can decide is the only move that shrinks the
frontier without fabricating either a success or a refusal.
codex review 45410 then caught that the first peel hand-rolled a SECOND walker
over the refinement shape while this note asserted it was "one traversal
authority, second consumer" — the prose claiming a property the code did not
establish. where_refinement_chain is now the one walk, with exactly two
consumers: predicate collection flat_maps over it, base peeling takes its last
link. The shape test is held once in is_where_refinement_type.
The residue is 13 sites in four shapes, each an upstream receiver-resolution
defect rather than a method-existence fact, and the frontier key now carries the
receiver shape as its third component — so a new call is refused unless it
reproduces the exact unestablished shape the row was measured on. The residual
widening (a second identically-failing call in the same module) is stated in the
note rather than claimed away; closing it needs the content-addressed occurrence
identity the namespace lane is landing.
Verified by execution: two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); the whole dag + src/v2 corpus compiles clean, which
is what proves the 12 peeled sites were DECIDED and not excused (their roster
rows are deleted); the wall witness gains a both-directions RED for the peel and
a control asserting each frontier key component is load-bearing.
Pre-existing and NOT from this PR, reported not fixed:
compiler_tests::rust_btree_set_ord_eligibility_requires_nominal_carrier_shape
fails here and at origin/main — rust_btree_set_element_ord_eligible,
rust_nominal_ord_type_eligible and the test body are all byte-identical to main,
so identical inputs to an identical pure function. The Rust suite was removed
from CI 2026-07-11, which is why it sits unnoticed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Reach the wall from every arm, and judge containers of ground scalars
Two review findings, both verified against the code and both real.
codex review 45430: the method-existence decision lived inline in the FINAL
else of method_pipe_map_keys_values_fallback, so an unresolved map_keys,
sorted_map_keys or map_values whose receiver is not a keyed collection took an
earlier branch and returned recv_rt with an empty diagnostic list — the identical
success-shaped fallback this PR deletes, preserved in the two arms that ran
before it. A wall reachable only from the default arm is not a wall. The
decision is now method_existence_decision, held once and called from all three.
codex review 45398 (second finding): the conformance gate required a plain
shape, so a List is not one, and a declared List<Int> whose body produced a
List<String> was indistinguishable from a conforming declaration. The widening
is the same positive-establishment argument rather than an exception to it — a
container of a ground kernel scalar has no alias, brand, coproduct,
anonymous-literal or cardinality representation standing between the two sides
either, so a difference in the element name is a real difference exactly as a
difference in a scalar name is. Keyed collections are deliberately NOT admitted:
the key and value axes need their own corpus measurement, and assuming the
element argument transfers is the move these notes refuse elsewhere.
Both controls were run against the PRIOR binary rather than reasoned about,
because a predicate that looks discriminating is exactly the artifact that isn't:
List<Int> |> map_keys / |> map_values exit 0 before, 2 located refusals now
fn f() -> List<Int> { ["a","b"] } exit 0 before, 2 located refusals now
Verified by execution: two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); whole dag + src/v2 corpus clean, which is the same
instrument that found the four conformance false-positive classes; both witnesses
green with the new REDs; compiler_tests 30 passed / 1 failed, that one being the
pre-existing rust_btree_set_ord_eligibility failure reported in the previous
commit (byte-identical to origin/main, Rust suite not in CI since 2026-07-11).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* WIP: p0 - protect the live system
* Split the residue on a decidable line, and fix the instrument that hid 12 sites
The most transferable finding here is that the INSTRUMENT was wrong before the
wall was. This wall had been measured with `gunbc run --entry
dag/tools/generated_artifact_gate.dag`, which reaches only that gate's import
closure. It reported CLEAN while twelve real sites sat outside it, and they
surfaced from CI instead. The whole-corpus instrument is the compile-clean gate
CI actually runs — `gunbc compile --source-root dag --source-root src/v2
--target dag` — which resolves 1629 sources against 2740 indexed modules. A
narrow instrument reporting clean is indistinguishable from a wall that works.
What the wide instrument found, and what each turned out to be:
TWO REAL DEFECTS, caught by the container widening from the previous commit.
`pure_dag_seam_unreachable() -> Int { 1 / 0 }` is a divergent seam, and the simd
and wgsl FLOAT kernels declared `-> List<Float>` while returning `List<Int>`
from it. The declarations are the correct half — those are float kernels taking
List<Float> arguments. The bodies are unreachable, so nothing ever misbehaved,
which is exactly why this had to be caught by construction rather than by a
consumer. Fixed with a Float projection of the same seam, marked as one
duplication with a bottom-type dissolution trigger: a divergent expression has
no result type to project from, so typing it Int alone was a silent lie
wherever the enclosing declaration was not Int.
EIGHT MORE UNESTABLISHED RECEIVERS, which forced a better model rather than more
roster rows. A receiver with NO AUTHORED NAME is not weak evidence about the
method — it is no evidence about anything, because the receiver's own type was
never established upstream. That is a different judgment failure from "this
receiver has a surface and the method is not on it", so it now gets its own
typed, counted, non-blocking ReceiverTypeUnestablished keyed on the CAUSE (empty
authored name — a decidable test) instead of a row per site. It cannot hide the
case the reviews worried about, because a receiver that DID resolve never
reaches it. That collapsed the roster from six rows to four.
ONE SHAPE NOT FIXED, and the machinery for it deleted. A brand alias can also
arrive as a plain qualified LEAF, Primitive(std.types.NonEmptyStr), rather than
the refinement Conj the peel walks. Three head-resolution strategies were
implemented and measured — lookup_type_for on the node, lookup_type_by_name on
the qualified name, and on its last segment — and none recovered the refinement.
The machinery was deleted rather than shipped unproven, and the site is a
declared row that says plainly that the cause is not yet understood. Unproven
machinery that decides nothing is worse than a declared row that admits what it
cannot decide.
Verified by execution: whole-tree compile-clean 12 blocking diagnostics -> 0,
with 18 ReceiverTypeUnestablished + 4 MethodExistenceFrontierAdmitted counted as
advisories so both classes stay observable; two-pass bootstrap + regen_stage0
--verify (regen_divergence_count=0); compiler_tests 30 passed / 1 failed, that
one the pre-existing rust_btree_set_ord_eligibility failure byte-identical to
origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Pin the ReceiverTypeUnestablished classification, and say what the evidence is
The behavioural evidence for this class is the corpus census — 18 sites
whole-tree, counted as advisories with the compile-clean gate at zero blocking
diagnostics — not a synthetic source. A synthetic reproducer WAS attempted, an
untyped lambda parameter inside a record-field fn, which is the shape the real
sites have; it produced no diagnostic at all, so it did not reproduce the shape
and is not asserted here as though it did. Recording the failed attempt beside
the control, because a witness that quietly asserts something weaker than its
comment claims is the same defect as prose asserting what code does not
establish — the one the reviews caught twice already in this PR.
What the control does pin is the classification, which is the part a later edit
could silently flip in either direction: blocking it fabricates a refusal over
18 correct sites, dropping it restores the #7479 silence. Both directions are
asserted against the three severity partitions directly.
Verified: regen_stage0 --verify (regen_divergence_count=0); wall witness green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Bound the anonymous-receiver admission on the roster (codex review 45459)
The finding is correct and the correction is worth stating precisely, because
the original reasoning was sound about one thing and wrong about another.
When a receiver has NO authored name, the wall cannot tell an existing method
from a nonexistent one — the receiver's own type was never established upstream.
That is true, and it is why refusing the whole class would refuse 18 correct
corpus sites. But it is a fact about DECIDABILITY, and I used it to justify
ADMISSION: every anonymous-receiver call was admitted on the cause alone,
non-blocking, which made every FUTURE such call green including one whose method
does not exist. Unbounded, exactly where existence is unknown. Counting a
diagnostic does not stop invalid code reaching the live system.
The two halves are now separated. The diagnostic still names the real cause —
ReceiverTypeUnestablished says the receiver's type was never established rather
than implying the method is missing, which is the review 45327 lesson. But
admission is gated on the same declared roster as every other unestablished
shape, keyed (module, method, "Primitive()"). The seven measured occurrences are
declared; a new anonymous-receiver call anywhere else REFUSES as
MethodExistenceUndecided. That is a ratchet that can only shrink, and blocking a
new instance of a known deficit class is the factory model, not an
inconvenience.
The gate is already covered by the existing witness: the perturbation loop
asserts, for every one of the 11 rows, that changing the module, the method, or
the receiver shape withdraws the admission.
Verified by execution: whole-tree compile-clean 0 blocking, with 18
ReceiverTypeUnestablished + 4 MethodExistenceFrontierAdmitted counted, so the
roster exactly covers the corpus and nothing is admitted that is not declared;
two-pass bootstrap + regen_stage0 --verify (regen_divergence_count=0);
compiler_tests 30 passed / 1 failed, that one the pre-existing
rust_btree_set_ord_eligibility failure byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Make the frontier a ratchet: declare each row's occurrence count and refuse excess
codex review 45464: the (module, method, receiver_shape) key bounds WHERE an
unresolved call may live but not HOW MANY, so a second call in the same module,
on the same method, failing to resolve the same way, inherited the admission.
That is not hypothetical — the measured rows are not singletons.
v2.compiler.tokenize admits seven `apply`, extdeps.mercurial three `any`,
gunbc.scm_compatibility.mercurial three `map` — so a row admitting seven would
silently admit an eighth.
Each row now declares its measured occurrence count and a per-module fold
refuses the excess with a located, typed FrontierOccurrenceBudgetExceeded. The
comparison is observed > declared, NEVER observed != declared, and that
asymmetry is load-bearing: a narrower compile closure legitimately sees fewer
occurrences, so equality would red any partial build, while fixing a call
legitimately lowers the count and must never red. The budget can only be
exceeded, never undershot — it ratchets down for free and refuses upward
movement.
Why not a stable per-occurrence key, which would close this exactly:
std.occurrence_identity is the corpus authority for the concept, and its own
scope law forbids filename, SourceSpan, authored name, structural Node equality
and content hash as identity inputs, allocating OccurrenceId inside one
graph-scoped allocator. An allocator-assigned integer is not stable across
compiles and so cannot appear as a literal in a declared row. A per-occurrence
key is not merely unimplemented here — it is unavailable from the authority that
owns the concept, which is why the count is the strongest bound the substrate
currently supports. Dissolve-on: content-addressed occurrence identity from the
namespace lane, at which point rows key on the occurrence and the count deletes.
The control is exercised at the mechanism, not through a corpus compile, so the
boundary is exact: declared occurrences pass, declared+1 refuses AND that
refusal blocks, and zero occurrences never red.
On the hand-Rust question raised in review 45469: the cli_run.rs delta is 14
lines, all of them arms of two EXISTING total matches over CompilerDiagnostic,
forced by exhaustiveness once variants are added in .dag — remove them and the
seed does not compile. Hand-written function count is unchanged at 742 before
and after. No new host transport, capability, or carrier.
Verified by execution: whole-tree compile-clean 0 blocking with 18 + 4 counted,
so declared counts equal observed exactly; two-pass bootstrap + regen_stage0
--verify (regen_divergence_count=0); compiler_tests 30 passed / 1 failed, that
one the pre-existing rust_btree_set_ord_eligibility failure byte-identical to
origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Check every explicit return against the declared type (codex review 45472)
Verified before fixing, and the finding was exactly right:
fn f(cond: Bool) -> Int { if cond { return "wrong" } 1 } exit 0
The wall compared only the body's FINAL inferred type. The block's value is the
trailing 1, which conforms, so the wrong-typed early exit was never compared
against anything. An early return is a second exit from the same declaration and
must meet the same declared type.
The first attempt threaded the check onto the `expected` already flowing into the
ExprReturn arm, and it did NOT work — measured, not assumed: a return inside a
statement-position `if` carries no expected type, so the probe still compiled
clean. Threading a declared-return field through InferScope would have reached
it, but that is ~14 construction sites across three files including the emitter.
The check is instead a post-pass at infer_item, which is local, needs no scope
change, and reuses declared_type_conformance_diags rather than minting a second
relation — so an early exit is judged by exactly the ground-kernel-scalar and
ground-element-collection discipline the trailing expression is judged by, and
widens with that gate rather than beside it.
Verified by execution: the probe above now refuses with a located
`expected 'Primitive(Int)', got 'Primitive(String)'`; whole-tree compile-clean
still 0 blocking, so no legitimate early return in the corpus reds; two-pass
bootstrap + regen_stage0 --verify (regen_divergence_count=0).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Hold the frontier-occurrence key in the diagnostic authority (codex review 45476)
The occurrence-budget fold hand-rolled a match over CompilerDiagnostic inside
v1.compiler.infer, which put a second reader of the coproduct outside the
coproduct's own authority: adding a variant could leave the budget silently
blind to it, and two places would decide what a diagnostic means.
diagnostic_frontier_occurrence_key now lives in 00_core beside diagnostic_to_span
and diagnostic_to_message, and the budget consumes it. Only two variants carry an
occurrence against a row — MethodExistenceFrontierAdmitted names its receiver
shape directly, and ReceiverTypeUnestablished always arises from a receiver with
no authored name, whose shape renders as Primitive(), which is why that literal
is the key rather than a field on the variant. A new variant that should be
budgeted is added in that one fn, next to the variants it joins.
Verified by execution: whole-tree compile-clean 0 blocking with 18 + 4 counted,
unchanged, so the routing is behaviour-preserving; two-pass bootstrap +
regen_stage0 --verify (regen_divergence_count=0); compiler_tests 30 passed /
1 failed, the pre-existing rust_btree_set_ord_eligibility failure.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Stop the return walk at lambda boundaries, and give the seed projection its receipt
codex review 45481, finding 1 — confirmed by execution before fixing:
fn apply_it(g: fn(Int) -> String, v: Int) -> String { g(v) }
fn outer(v: Int) -> Int { apply_it(g: x => { return "inner" }, v: v) 1 }
-> expected 'Primitive(Int)', got 'Primitive(String)'
collect_explicit_return_types recursed through ExprLambda, so a return belonging
to the LAMBDA's callable return type was checked against the enclosing
declaration. That is a fabricated refusal — the mirror image of the hole the walk
was added to close, and §5 forbids one exactly as it forbids the other. Every
callable boundary is a new declaration and its returns are judged against it. The
walk now stops at ExprLambda, which also means lambda returns are not yet judged
at all; that narrowing is stated on the note rather than implied, and it
dissolves when the walk carries each callable's own declared return.
The discriminating PAIR is now witnessed, since one direction alone proves
nothing here: the early return must refuse AND the lambda return must not.
codex reviews 45469/45481/45484, hand-Rust gate — receipt added in the gate's own
form, both on the carrier (v1.compiler.core compiler_diagnostic_seed_projection_note,
beside the coproduct whose extension forces the arms) and in the changed planning
artifact. It is an explicit deferral naming lane
(compiler-static-failure-closure) and ROADMAP row (hand-MAINTAINED Rust -> zero
at v2 self-host), with the argument that an exhaustiveness arm is a different
class from the gate's usual subject: the gate's other deferrals are decision
surfaces that COULD live in .dag and therefore owe their own schedule, while an
arm cannot live anywhere but the seed's projection of the coproduct and
disappears exactly when the seed does.
Checkable receipt: hand-written fn count in cli_run.rs is 742 at origin/main and
742 here; the diff is 13 added lines with zero `fn`. The 322 lines review 45484
attributes to hand-Rust in compiler_tests.rs are not hand-written at all — that
file is GENERATED, listed in gunbc.stage0_emit_model.generated_stage0_files and
emitted by regen_stage0 from src/v1/compiler_tests_rust.dag, so its growth is
witness text authored in .dag.
Verified by execution: both probes correct in both directions; whole-tree
compile-clean 0 blocking; two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); compiler_tests 30 passed / 1 failed, the pre-existing
rust_btree_set_ord_eligibility failure.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* chore: regenerate drifted generated artifacts (ci auto-heal)
* WIP: p0 - protect the live system
* Make the budget a real ratchet, fix the witness arity, and make the seam diverge
Three findings, all correct, and one of them was mine to catch before review.
cursor review 45494 finding 2 — THE WITNESS DID NOT COMPILE. I changed
frontier_occurrence_budget_diags to take a locating module_span and did not
re-run the suite, so three call sites in the witness still passed two arguments.
Reading caught what I skipped running; the run would have caught it immediately
and I did not do the run. Fixed, and the suite is green again.
codex review 45491 — the ceiling did not ratchet. `observed > declared` let
seven shrink to six while the declared seven stood, so a seventh call could
return silently: a static limit, not a ratchet, and the note claimed the ratchet
anyway. My stated justification for the ceiling — that a narrower closure sees
fewer occurrences — was simply wrong about this check, which runs per MODULE:
every occurrence of a module's rows is present whenever that module is
typechecked at all, and a closure omitting the module never runs its rows. So
there was no partial-visibility case to protect and the asymmetry bought
nothing. The comparison is now equality, which removes the headroom a
reintroduction slips into: fixing a call reds until the declared count is
lowered. Both directions are asserted in the witness, since the under-count half
is what makes it a ratchet and is the half an author is tempted to relax.
cursor review 45494 finding 1 also flagged the equality as contradicting the
note. It contradicted the note because the note was stale, not because the code
was wrong — the note has been rewritten to describe what the code does and to
record why the ceiling reasoning failed.
codex review 45493 — `1.0 / 0.0` IS NOT DIVERGENT. Under IEEE-754 it is positive
infinity, not a trap, so the Float seam RETURNED and the kernels asserted
unreachable would have produced [+inf]. A fabricated plausible output, the exact
thing §5 forbids, introduced while fixing a different fabrication. Integer
division by zero traps; float division by zero does not, however similar they
look. The Float projection now forces the Int seam to evaluate in its condition,
so divergence happens before any Float is produced. Confirmed in the emitted
Rust: `if (pure_dag_seam_unreachable() == 0)` over `pub fn
pure_dag_seam_unreachable() -> i64 { (1 / 0) }`.
Verified by execution: two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); whole-tree compile-clean 0 blocking; compiler_tests
30 passed / 1 failed, that one the pre-existing rust_btree_set_ord_eligibility
failure byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Count the unjudged conformance residue, and author the receipt where it survives
codex review 45500 — the conformance wall's unjudged branch returned an empty
diagnostic list, so an unproven declaration was byte-for-byte indistinguishable
in the output from a proven-conforming one: the absence of a check reading as
the presence of a proof. It now emits DeclaredTypeConformanceUnjudged, counted
and non-blocking, so the wall's frontier has a SIZE — 3005 declarations
whole-tree — a number that falls as the relation widens and is therefore a
prioritizable measure of the gap rather than an invisible one.
It fires only where the declared and produced SHAPES DIFFER. Identical shapes
have nothing to prove, and counting them would bury the signal under
declarations nobody doubts; the residue that matters is exactly the set where a
mismatch could hide.
codex review 45501 finding 2 — the HAND-RUST receipt had gone stale, reading
five variants and 13 lines after a sixth variant landed. That made the receipt
itself the stale-prose defect it exists to prevent. Corrected to six variants
and 18 lines, with both figures now marked as re-derived from their two commands
on every variant addition rather than carried forward.
AND THE RECEIPT WAS IN THE WRONG FILE, which is why it vanished: I had written it
into docs/plans/compile-clean-forcecheck.md, and that .md is a GENERATED
PROJECTION of dag/gunbc/plans/compile_clean_forcecheck.dag — the CI auto-heal
commit regenerated the doc and silently reverted it. The receipt is now authored
in the .dag plan authority and survives the heal, which is verified by running
the generated-artifact gate and seeing the text reappear in the projection. The
plan carrier says so in-place, so the next author does not repeat it.
review 45499 — the count/length pair on the algebra templates is a §3 nicknaming
fork RECORDED rather than introduced, and the row now says so. The fork's
authority is the interpreter, which dispatches length, count and size to one
native arm and predates this change; the templates listed only length, so
`String |> count` resolved at runtime with no declared row, which the
method-existence wall exposed the moment it began proving absence from the
roster. Reconciling the declaration to the runtime is the honest direction —
inventing a distinct meaning for count would be the fabrication, and dropping the
row would refuse a working call. Dissolve-on: one name across the interpreter
arm, the templates, and the corpus, which is a corpus-wide rename and its own
lane.
Verified by execution: whole-tree compile-clean 0 blocking; two-pass bootstrap +
regen_stage0 --verify (regen_divergence_count=0); generated-artifact gate green
with the receipt present in the projection; compiler_tests 30 passed / 1 failed,
the pre-existing rust_btree_set_ord_eligibility failure.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* WIP: p0 - protect the live system
* Ground filesystem_read's return type; count the residue the gate was not counting
CI red on the last push was my own wall firing on a site my instrument never
reached, and chasing it found three defects underneath it.
ROOT CAUSE. filesystem_read was registered in 04_method as a bare
type_variable_node, so `filesystem_read(path: p).content` established nothing:
the field lookup had nothing to look in and the result was a fabricated
Primitive() carrying no name. A later `.split` on that value was then accepted
with no judgment behind it — #7479's exact shape one layer down, surviving
because the interpreter dispatches split on the native String regardless, so
nothing ever failed loudly. The return type was never unknown: runtime_rust.dag
already emits `pub struct FilesystemReadResult { pub content: String }`.
Declaring it makes the seed's struct and the compiler's type one fact instead of
two, via a make_kernel_record_type helper that builds the same
Conj-with-named-children shape lookup_field_type_node already walks for authored
records — so the kernel path and the authored path cannot drift.
WHY MY INSTRUMENT MISSED IT, WHICH IS THE MORE USEFUL FINDING. Whole-tree
compile-clean reported zero blocking while this site sat outside its closure;
the discovery corpus resolves entries compile-clean never opens. That is the
SECOND time this lane's instrument was narrower than the wall it was measuring —
the first was main_wet hiding twelve sites. The measurement was wrong before the
wall was, both times.
THE RESIDUE WAS NOT ACTUALLY COUNTED. compile_clean_diagnostic_is_advisory is a
CLOSED ALLOWLIST, not the complement of is_hard, so all three non-blocking
variants this lane adds matched neither predicate: they rendered to the terminal
while every count the gate reported read zero for them. I had been telling
reviewers the frontier was counted, and the population figures I quoted came
from grepping log text — no mechanism in the repository counted them. Found by
executing the gate before and after the expansion fix and seeing its advisory
total sit unchanged at 4590 while the printed population halved. The three
variants are now in the allowlist; the total moves 4590 -> 6176 and nothing
falls through either counter.
THE FRONTIER WAS REPORTED AT NEARLY TWICE ITS SIZE. Measured, 1436 of the 3005
unjudged conformance pairs were one type compared against ITSELF at two
expansion depths — a declaration naming T against a body producing T's expanded
body (203 Node, 173 Outcome, 46 Witness, 43 Optional, 38 PipelineStep, long
tail). Resolving each side through lookup_type_for before comparing is a real
judgment step, not a name heuristic, and it can only remove a diagnostic since
both branches already treated unequal shapes as unjudged rather than as a
refusal. 3005 -> 1566. An inflated frontier is not a conservative error: it
buries the residue that genuinely cannot be decided under pairs never in doubt.
What remains is meaningful and independently rediscovers DESIGN's own open
threads — Nat vs Int (61), Hash vs ContentHash (29), brand aliases like
NonEmptyStr vs String (207), anonymous record literals (150+).
codex review 45533 finding 2 — every explicit-return diagnostic reported
body_typed.span, so a function with several early returns pointed them all at
one location. The collector now carries each return VALUE rather than only its
type, and each refusal is located at the return that caused it.
The two frontier rows for language_source_scaffold_index_test are deleted: they
were this same filesystem_read gap, and the cause I authored for them ("an
untyped lambda parameter") was a guess that was simply wrong. The occurrence
ratchet then fired in the FALLING direction and its message asserted a new call
had appeared — a diagnostic claiming a direction it had not measured. Reworded
to state both directions and to say which remedy each one implies.
Receipt figures re-derived, and one of them had never been reproducible: the
claimed 742 hand-written fns in cli_run.rs matches no command — 501 bare `fn`,
245 `pub fn`, never 742. Every figure now names the command that produces it:
`grep -cE '^(pub )?fn '` is 746 on main and 746 here (flat), the diff is 28
added / 0 removed, and zero added lines declare a fn.
Verified by execution: whole-tree compile-clean 0 blocking with 0 diagnostics
falling outside both counters; the #7479 repro still refuses with zero files
emitted while the `map` control still compiles clean; both CI-red sites now
green; two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
compiler_tests 30 passed / 1 failed, that one being
rust_btree_set_ord_eligibility_requires_nominal_carrier_shape, whose three
functions and test body are byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Stop keeping two copies of one receipt
review 45565 quoted the HAND-RUST receipt back as "742 -> 742, +18 lines" after
those figures had already been re-derived to 746/746 and 28 lines. Nothing was
stale in the sense of nobody updating it: the receipt existed in TWO carriers,
and I re-derived it in one.
The forked paragraph's own next sentence already named the carrier as the single
authority for this receipt, and then restated the numbers anyway — §3 doing
exactly what §3 says it does, inside a single paragraph. A receipt duplicated
across two carriers is worse than one kept in the wrong place: both read as
authoritative, they diverge silently, and a reviewer is as likely to cite the
stale copy as the live one. That is not hypothetical here; it is what happened.
So the plan carrier no longer repeats the figures. It states the claim the
receipt makes — the hand-Rust carrier census is flat, only arm count moved — and
points at the one place the numbers live, beside the coproduct whose extension
forces the arms, where each is stated with the exact command that reproduces it.
A reader checks by running those commands rather than by trusting either copy.
The paragraph says why it is written that way, so the copy does not grow back.
The projection was regenerated through main_wet on the generated-artifact gate,
which then re-runs clean; the doc is a projection and re-authoring it directly
is reverted by the heal.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Record why the seed reads Node storage directly, since the answer is not per-function
review 45570 asks that is_where_refinement_type and where_refinement_chain route
through a canonical query/fold surface, or carry a bounded disposition with
owner, lane and trigger. Measured, neither is available in the shape asked for,
and the reason is worth writing down where the next reader hits it.
There is no canonical surface reachable from here. fold_node and node_query live
in src/v2/std; no v1 seed module imports v2 at all; and v1 COMPILES v2, so
routing v1 inference through v2's fold inverts the bootstrap rather than tidying
it. DESIGN's fold_node line is scoped to the 7 v2 stages — a DRY example within
v2, not a rule binding the seed.
And the disposition is the seed's, not these functions'. They are 2 of 589
direct Node-storage reads in this file, 579 of which are on origin/main: the
seed IS the traversal, the stage that walks the tree so later stages need not.
Attaching a per-function trigger to 2 reads while 587 identical reads beside
them carry none would describe separable work that does not exist — a fabricated
bound, which is the same defect as a fabricated refusal pointed at a schedule.
The real trigger is the one the hand-Rust receipt already carries: the v1 seed
shrinks to zero at v2 self-host and these dissolve with it.
Worth noting that where_refinement_chain exists BECAUSE review 45410 asked for
exactly this consolidation — it is the single traversal authority that replaced
two independently-drifting walkers.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking, 6176 advisory, 0 diagnostics outside both
counters.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* State the return walker's disposition where it was asked, not only on its sibling
review 45580 raises the walker question again, this time against
collect_explicit_return_values. The DESIGN citation is the same one review 45570
made and I answered: node_query appears zero times in DESIGN, the single
fold_node line is scoped to the 7 v2 stages, fold_node/node_query are v2
substrate, no v1 seed module imports v2, and v1 COMPILES v2 — so routing seed
inference through v2's fold inverts the bootstrap rather than tidying it.
But one part of the finding is fair and is the reason it had to be found twice.
I recorded that reasoning on where_refinement_receiver_peel_note and left
explicit_return_conformance_note carrying only its lambda-coverage trigger, so
the note nearest the walker said nothing about the walker. A disposition stated
on one carrier and omitted from its sibling is not stated. It is now on both.
Measured, so the claim is checkable rather than asserted: self-recursive
`children |> flat_map` collection is the v1 seed's only traversal idiom — 16
such sites on origin/main across 04_emit_info, 04_sigs, 04_infer, 05_emit,
05_emit_rust, compile and complexity. There is no shared v1 walker to route
through because each collector recurses itself. This is the 17th instance of a
16-instance idiom, and its trigger is the one every sibling carries: the v1 seed
shrinks to zero at v2 self-host and they dissolve together.
Generalizing a shared collector for this one call site would ADD a 17th shape
rather than remove one, and attaching a per-function owner/lane/trigger to it
while 16 identical siblings carry none would describe separable work that does
not exist — the same fabricated bound I declined at review 45570.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Judge conformance with the structural relation, not a rendered shape string
codex review 45600 — the not-both-ground branch compared node_type_shape OUTPUT
and treated equality as proven conformance. That projection is lossy by design:
it renders every anonymous product as the literal text Product(<anon>) and every
named product as its OUTER NAME ONLY, discarding fields, variants and their
types. So two structurally different records compared EQUAL and were stamped
proven-conforming, and distinct definitions sharing an outer name did the same.
That is the exact fail-open this wall exists to delete, reintroduced while
removing a different one, and by the same mechanism as the 1.0/0.0 seam earlier
in this PR: a projection that LOOKS like evidence used where a proof was
required. A display projection belongs in a message; a judgment must consume the
structural relation. The finding is correct and the defect was mine — it arrived
with the expansion-depth fix two commits ago.
conformance_expanded_node now returns the resolved, brand-peeled NODE and the
branch calls node_type_compatible on it, which recurses into container elements
and compares canonical template names, so identity is established rather than
rendered. Its known imprecision is safe in exactly this position: it reports
mismatch for four classes of correct code, and a mismatch here yields the counted
unjudged advisory rather than a refusal, so a false negative costs a count and
never reds correct code. The wrong direction would have been to keep the string
because it was quieter.
The peel rides the SAME authority the method wall uses
(peel_where_refinement_base), one traversal with two consumers rather than a
second minted here, which also grounds the brand-alias class that dominated the
residue: 1566 -> 1024.
On review 45593, which asked that the unjudged branch refuse or be bounded by an
explicitly admitted frontier: I measured the frontier before answering, and a
roster is the wrong shape here — the residue is 398 DISTINCT declared/produced
pairs with 242 occurring exactly once, a long tail that grows with the corpus
rather than a small admitted set. Refusing it outright is also not available:
the classes are brand aliases, anonymous record literals, the Nat/Int fork and
unsubstituted generics, all of them CORRECT code, so refusal would red ~1000
sound declarations and fabricate refusals at scale. What was actually available
was to shrink it by judging more, which is what this commit does — and the
lossy-string defect 45600 found was sitting inside the previous attempt to do
exactly that.
Verified by execution: whole-tree compile-clean 0 blocking, 5634 advisory, 0
diagnostics outside both counters; conformance RED control refuses all four
shapes (scalar return, list element, data init, early return) each located;
#7479 still refuses with zero files emitted and the map control still compiles
clean; regen_stage0 --verify (regen_divergence_count=0); compiler_tests 30
passed / 1 failed, the pre-existing rust_btree_set_ord_eligibility failure whose
functions and test body are byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Record the proven conformance hole and the 🟡 seed-traversal frontier
Two reviews, and the first one is a finding I could not close.
review 45647 is CORRECT and I proved it by execution before answering: the
unjudged branch is not merely unmeasured, it lets a program that is simply WRONG
reach emission. `type R { x: Int }` `type S { y: String }`
`fn wrong_record() -> R { S { y: "a" } }` compiled EXIT 0 and EMITTED TWO FILES
while reporting the mismatch as a counted advisory. Two structurally unrelated
named records is not a representation gap; it is the conformance half of #7479.
I ATTEMPTED THE FIX AND IT IS NOT LANDED. Three successive narrowings of a
refuse-when-both-sides-are-named-structured rule, each measured against the whole
corpus: (1) structured and named -> 90 refusals of CORRECT code, dominated by the
two-representation optionality class; (2) narrowed to inhabited named records
with kernel scope names excluded -> 15; (3) additionally guarding the raw nodes
-> 27, by which point the population had shifted to a NEW class, produced sides
that are let-BINDING names rather than types. 90 -> 15 -> 27 is the finding: each
guard displaces the false-positive population instead of shrinking it. That is
the exemption-accumulation this wall refuses elsewhere, and shipping any of the
three would red correct code.
So the arm is reverted and the hole is recorded on the carrier with its executed
witness, the three measured attempts, the named blocking obstacle, and a
dissolution trigger. The obstacle is not vague: the produced-side node reaching
this branch is not reliably a TYPE — it can be a nominal reference, a kernel
encoding of cardinality or absence, an anonymous literal, or a let-binding
identity — so no predicate over its shape separates a real mismatch from a
representation gap until produced-side type identity is established upstream.
Dissolve-on: feature:conformance-produced-type-identity. My own note's line
applies to me here: unproven machinery that decides nothing is worse than a
declared row that admits what it cannot decide.
reviews 45570 / 45580 / 45666 — the walker. 45666's sharpest point is right and
I had leaned on the weak form: sibling count is PRECEDENT, and precedent is debt,
not permission. The justification is reachability, not popularity — fold_node and
node_query are v2 substrate, no v1 seed module imports v2, v1 COMPILES v2 so
routing seed inference through v2's fold inverts the bootstrap, and no shared v1
walker exists because every v1 collector recurses itself. The review also asked
for the repo's own declared-scaffold form rather than prose, which is a fair and
concrete ask: seed_node_traversal_frontier is now a 🟡 dissolve-on row covering
the CLASS (16 sibling sites on main, 579 direct field reads in 04_infer alone),
with the cost of closing now and the same trigger the hand-Rust receipt carries,
because it is the same seed and the same endpoint.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking, 5637 advisory, 1024 counted residue, 0
outside both counters; #7479 refuses with zero files emitted; conformance RED
control refuses all four shapes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Prove the permission is main's, not this path's
codex review 45695 holds that the PR "knowingly leaves a demonstrated wrong
program able to reach emission through the newly added conformance path" and
that the identity work must land before this path may permit emission. The hole
is real — I proved it last commit. The attribution is not, and it decides the
sequencing question, so I measured it instead of arguing it.
The identical program built against origin/main:
exit=0 files emitted=2 diagnostics=0
On this branch: the same 2 files, plus one counted advisory naming the mismatch.
The conformance path does not newly PERMIT that emission; main permits it
silently and this branch makes it visible and countable. Blocking here would
hold back the method-existence wall — which does refuse, and emits nothing — and
leave the live system strictly less protected than landing it.
A fourth fix attempt isolated the obstacle exactly rather than leaving it
inferred. Guarding on "both sides are Conj whose authored name resolves via
lookup_type_by_name to a record declaration" still refused 14 seed sites, and
every one had a LET-BINDING name on the produced side (module_emit_scope,
scope_after_expr, lookup_item, service_fallback_transport). lookup_type_by_name
resolves those because bindings and types inhabit ONE name environment, so the
guard cannot distinguish a type identity from a binding identity. That is the
recorded obstacle, now demonstrated: no predicate over the produced node's shape
or name can close this class, which is why four attempts moved the false-positive
population (90 -> 15 -> 27 -> 14) instead of shrinking it.
Attempt 4 is reverted like the other three. The row now carries the main
comparison alongside the witness, the four attempts and the trigger.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Fix list_append call labels that main's call-shape wall refuses
The floor failed on src/v2/test/claim/bash_program_fold_support.dag with eight
"call shape mismatch calling 'list_append': no parameter named 'xs'" refusals.
Not this lane's code: the file is byte-identical to origin/main and no commit
here touches it. It is main's own #7519 call-shape wall firing on a call site
that predates it — list_append is declared (left, right) in v2.std.algebra and
this file passed xs:/ys:, which the wall now correctly refuses and which was
silently accepted before it existed. Exactly the fail-open class #7519 closes.
It surfaced here rather than on #7519 because the two runs have different reach:
a PR-scoped compile-clean does not open test entrie…
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 1, 2026
…n, add the measurement-schema stage, split the acceptance door Adopts the operator spine verdict (2026-08-01, seventh pass) into the roadmap authority and the gap analysis: - ladder-measurement-schema precedes probes AND carrier (the receipt protocol both meet through; breaks the probes/carrier protocol cycle). - The three merged P0 slices recut at their actual grain, identities tombstoned: floor-call-shape-wall -> call-label-and-surplus-wall (accepted, #7519) + missing/duplicate + signature-resolution siblings; floor-method-existence-wall -> method-established-surface-wall (accepted, #7484) + receiver-normalization + zero-resolution siblings; floor-inhabitance-wall -> declared-conformance-ground-fragment (accepted, #7484) + grounding + general-wall siblings. - The Accepted door split mechanism/floor/extended (compiler-accepted-obligation-closure tombstoned): the audit form lands with the carrier; refusal never turns on over a known-open judgment (review 45545's substance preserved in the activation nodes). - Exemption removal re-grounded on argument-type-compatibility grounding + declared-conformance grounding (labels never gated it). - guarantee_ladder_edges rewritten wholesale; emitters parallel with the baseline; baseline defined as a two-revision execution. - Gap analysis sec 12 updated in place (Stage 0/1a/1c/2-amendment/4/6/6b); stale dissolution triggers repointed (doc_graph_roots, doc_reachability_witness_test); tombstone-note staleness fixed. - ROADMAP.md regenerated via main_wet; roadmap witness receipts 100 PASS (brief budgets, edge endpoints, acyclicity, identity registry with five tombstones); regen_stage0 --verify divergence 0. The branch additionally carries the ord-eligibility silent-red repair (childless gate on name-grain arms + incident note) and the clean regen of the generated stage0 files after the origin/main merge. Known pre-existing: the whole-tree cold census refuses 23 ambiguous-reference diagnostics in dag/test/claim/occurrence_binding_resolve_witness_test.dag (landed with #7508, byte-identical to origin/main; handed off to the occurrence lane). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 1, 2026
…ment-schema stage, acceptance-door split (#7553) * WIP: compiler correctness * Bind the guarantee-recovery analysis into the doc graph The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Reconcile the gap analysis against the independent review — three corrections adopted, receipts verified Adopted (all verified on main this pass): - Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not statically propagated: v2.std.refinement exists, NonEmptyList fixture + green cardinality_fold_propagation_test exist, and refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the carrier proves nothing). New Sec 4b: the operator independently re-directed this exact guarantee on 2026-07-04 (interface-summary-declared-use-arity.md Sec 3.1, "hard error in the language") — the intent is not lost; the lattice design pass (FLAG E) never started. - Failure history rewritten (Sec 2): the exemption dates to 2026-06-08 (a13fb57), pre-bankruptcy; correctness-dimensions.md marked type safety "Yes (blocking)" while return position was unchecked — so the ledger overstated, then the auditable contract was deleted. The pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a deliberate total semantics, not a priced-out wall. - Status vocabulary widened to the review's 11-state lattice; v2 terminal calibrated (validate_then_compile door + loop-bound wall are real; InferredTree is still not a proof boundary); application-arity row added (formal-driven walk, positional fallback for misspelled labels, ArityMismatch is constructor-arity); PatternLookupBlocked's silent [] arm confirmed (PatternDynamic does diagnose — review corrected there). - Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5 behaviors" is stale against v2.std.node's six (Match) — the guarantee authority lands as .dag rows, never hand-edited prose. - Sequencing reconciled to 7 stages: claims authority + expecting-red probe corpus together; zero-resolution method wall now, ambiguity wall census-first; cardinality vertical slice third. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Status header: two audit passes complete, open items typed Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Align the bind's dissolution trigger with the doc's own authority model (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * WIP: compiler correctness * Ladder follow-up: adopt the post-merge verdict (8 corrections) + the guarantee-ladder roadmap section Corrections, each verified against main before adoption: 1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque ... every proof-carrier is presently forgeable") was false as stated; corrected to an audited-status claim: sole_constructor is the candidate wall, completeness for generic carriers unverified. The earlier keyword-set inference is withdrawn in the Sec 10 ledger. 2. Subject grain: rung honesty is measured at a declared acceptance boundary; a class's rung is the MINIMUM across in-scope paths (the interpreter refuses the mislabeled call that order_typed_call_args reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1 carrier gains subject_grain/acceptance_boundary/compile_mode/ realization_target/covered_population. 3. Seed rungs demoted: return/data/generic, field-through-generics, exhaustiveness, cardinality, full ==-class, and L4 all to UnknownUnmeasured (compile admission proven is not runtime disposition proven); census marked specimen-denominated; unknown- method R0 scoped to the interpretation path. 4. Dissolution on climb amended in DESIGN 4b: production handling dissolves; the RED + positive controls REMAIN enrolled as the evidence the higher rung stays real. 5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows + witness-test fixture migrated); the guarantee-recovery row now carries BOTH anchors typed, not one typed + one in prose. Carrier note records that List admits [] — the exact cardinality gap the ladder tracks — with the doc-graph witnesses as the interim wall. 6. cardinality_fold_propagation_test relabeled everywhere as manual value-level specimens (length homomorphism over literals + runtime refine_byte); "not new design" softened to the accurate scope statement; the roadmap cardinality node re-briefed accordingly. 7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a generic dimension mechanism; extension-vs-redesign is an open audit question that roadmap pricing must carry. 8. Sec 1 "was not built" -> "never completed as an exhaustive acceptance contract"; Sec 11 queue updated (correctness-dimensions done; sole_constructor completeness audit added). Additions (operator direction): ROADMAP gains the "Guarantee ladder — climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes in ticket format with dependency edges (probe corpus gates the four floor walls; carrier gates cardinality slice, emitters, prevalence; exemption removal gates on the call-shape + inhabitance walls). The capability node is the sole_constructor completeness audit. State-vs- work split recorded on the carrier: rung STATE lives in the Stage-1 claims carrier and is emitted (ladder-census-emitters node); roadmap nodes track CLIMBS. Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap authority 35/35, model 9/9, focus 12/12. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give works its executing consumers (review 45336): nonempty wall, symbol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * De-inflate the three climb-node headlines (review 45349): work nodes name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Ladder nodes join the declared roadmap graph; binds nonempty by construction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Trim the three over-budget ladder briefs to the operator's 100-word ticket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Containment predicates consume doc_all_nodes, the one canonical walker (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Post-merge verdict follow-up: open-candidate honesty, anchored baseline, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Route the ambiguity wall and cardinality seam through the closure door (review 45545) The first edge set let compiler-accepted-obligation-closure land while floor-method-ambiguity-wall and cardinality-vertical-slice stayed open — the door would have certified "every required judgment established" over two required-open judgments (the grid marks the cardinality seam P0.2 minimum-R2 and ambiguity part of resolved identity; the verdict's spine routes ALL P0 obligations through the door). Both are now prerequisites of the closure; residual prevalence depends on the door alone. Authority 38/38, focus 12/12, page 28/28, drift 8/8; regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Reconcile the sec-7b behavior-count passage to past tense (review 45558) Sec 7b still described the 5-behaviors drift as current after this PR corrected the authority — the stale-claim problem the PR closes elsewhere. The passage now records the drift as found-and-corrected, keeps the specimen's evidentiary value (the denominator drifted silently in prose), and leaves the Match-promotion adjudication question with the queue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Remove probe demo scaffolding (net-zero vs main: files added by autocommit sweep mid-run, deleted after measurement) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Call-shape wall: refuse unknown argument labels and surplus positionals at the direct-call seam, mirroring the runtime contract The compile seam was silent on both classes call_function_inner refuses at runtime, and the emitter reordered mislabeled args positionally — two realizations of one program disagreeing silently. direct_call_shape_diags (v1.compiler.infer) closes both, blocking, exemption-free (a label has no representation gap). Census before landing refused 28 live rename fossils in 5 fns (to_string i->value, arm_body, is_import_slot_node, fold_list init->empty, path->path_opt), all relabeled to their declared authority; +3 fixed in the measured sig-unresolved blind spot. Probe pair pre/post, enrolled ct_call_shape_wall_witness_test RED/controls, regen fixed point divergence 0, whole-corpus compile-clean 0 blocking. Duplicate/missing stay unwalled with triggers (interpreter-first parity pair next). Roadmap node + census rows amended; ROADMAP regenerated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * Roster the call-shape witness blob in the scaffold index (review 45655) ct_call_shape_wall_witness_test joined compiler_tests_rust without its LanguageSourceScaffoldRow, so the exact-equality enrollment witness (compiler_tests_rust_blobs_are_all_rostered, 29 declared vs 28 rostered) would red on CI. Row added with the same hand-assertion scaffold trigger as its peers and enrolled in the roster; witness re-run green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Repair the silent-red ord-eligibility wall: name-grain arms admit only childless nodes d975e10 (2026-07-21) moved Symbol onto the name-only opaque-alias roster, dropping the shape check its enrolled negative control pins — Symbol<Float> became BTreeSet-eligible by name, and the RED sat invisible for ten days because the Rust unit suite left CI on 2026-07-11. Childless gate restores the shape constraint (zero corpus impact; regen fixed point holds); incident + dark-suite evidence gap filed as gap-analysis sixth-pass ledger + queue item 9 (operator decision, priced by this incident). Found by tidy-deer-730 during the 7484 main integration. Suite: 30 passed / 0 failed (was 1 failed). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Dedupe the call-shape witness aggregator entry after the main merge The merge auto-combined both sides' insertions of ct_call_shape_wall_witness_test into compiler_tests_source(); a duplicate generates the #[test] twice. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Spine reconciliation: recut the merged P0 slices at their actual grain, add the measurement-schema stage, split the acceptance door Adopts the operator spine verdict (2026-08-01, seventh pass) into the roadmap authority and the gap analysis: - ladder-measurement-schema precedes probes AND carrier (the receipt protocol both meet through; breaks the probes/carrier protocol cycle). - The three merged P0 slices recut at their actual grain, identities tombstoned: floor-call-shape-wall -> call-label-and-surplus-wall (accepted, #7519) + missing/duplicate + signature-resolution siblings; floor-method-existence-wall -> method-established-surface-wall (accepted, #7484) + receiver-normalization + zero-resolution siblings; floor-inhabitance-wall -> declared-conformance-ground-fragment (accepted, #7484) + grounding + general-wall siblings. - The Accepted door split mechanism/floor/extended (compiler-accepted-obligation-closure tombstoned): the audit form lands with the carrier; refusal never turns on over a known-open judgment (review 45545's substance preserved in the activation nodes). - Exemption removal re-grounded on argument-type-compatibility grounding + declared-conformance grounding (labels never gated it). - guarantee_ladder_edges rewritten wholesale; emitters parallel with the baseline; baseline defined as a two-revision execution. - Gap analysis sec 12 updated in place (Stage 0/1a/1c/2-amendment/4/6/6b); stale dissolution triggers repointed (doc_graph_roots, doc_reachability_witness_test); tombstone-note staleness fixed. - ROADMAP.md regenerated via main_wet; roadmap witness receipts 100 PASS (brief budgets, edge endpoints, acyclicity, identity registry with five tombstones); regen_stage0 --verify divergence 0. The branch additionally carries the ord-eligibility silent-red repair (childless gate on name-grain arms + incident note) and the clean regen of the generated stage0 files after the origin/main merge. Known pre-existing: the whole-tree cold census refuses 23 ambiguous-reference diagnostics in dag/test/claim/occurrence_binding_resolve_witness_test.dag (landed with #7508, byte-identical to origin/main; handed off to the occurrence lane). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Recut the extended activation as per-class admissions (review 45918) The first cut kept requires-all edges on one extended-activation node while its prose promised class-by-class widening — the graph would have deferred every admission behind the slowest climb, preserving the monolithic deferral the door split dissolves. Now: four per-class admission nodes (extended-admission-cardinality/-ambiguity/-v2-realization/-v2-translate, each <- floor-closure + its own climb, ready the day that climb lands) and accepted-extended-obligation-closure recut as the terminal roster-completeness certification, where requires-all honestly belongs. Same closure identity (no slug change, no tombstone); four fresh identities minted. Stage 6b + seventh-pass ledger + lane note updated; ROADMAP regenerated; graph/budget/identity witnesses 26 PASS. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Trim the ord name-grain note to its structural constraint (review 45929) The in-code note duplicated the incident narrative the gap analysis already records (sixth-pass ledger + queue item 9) — a parallel ledger realized into the emitted seed with no executable consumer. The carrier keeps only the constraint the code cannot show: why name-grain arms admit childless nodes only, the discriminating RED's symbol, and the shape-examining sibling path. regen_stage0 divergence 0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 1, 2026
…-schema) (#7572) * WIP: compiler correctness * Bind the guarantee-recovery analysis into the doc graph The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Reconcile the gap analysis against the independent review — three corrections adopted, receipts verified Adopted (all verified on main this pass): - Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not statically propagated: v2.std.refinement exists, NonEmptyList fixture + green cardinality_fold_propagation_test exist, and refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the carrier proves nothing). New Sec 4b: the operator independently re-directed this exact guarantee on 2026-07-04 (interface-summary-declared-use-arity.md Sec 3.1, "hard error in the language") — the intent is not lost; the lattice design pass (FLAG E) never started. - Failure history rewritten (Sec 2): the exemption dates to 2026-06-08 (a13fb57), pre-bankruptcy; correctness-dimensions.md marked type safety "Yes (blocking)" while return position was unchecked — so the ledger overstated, then the auditable contract was deleted. The pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a deliberate total semantics, not a priced-out wall. - Status vocabulary widened to the review's 11-state lattice; v2 terminal calibrated (validate_then_compile door + loop-bound wall are real; InferredTree is still not a proof boundary); application-arity row added (formal-driven walk, positional fallback for misspelled labels, ArityMismatch is constructor-arity); PatternLookupBlocked's silent [] arm confirmed (PatternDynamic does diagnose — review corrected there). - Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5 behaviors" is stale against v2.std.node's six (Match) — the guarantee authority lands as .dag rows, never hand-edited prose. - Sequencing reconciled to 7 stages: claims authority + expecting-red probe corpus together; zero-resolution method wall now, ambiguity wall census-first; cardinality vertical slice third. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Status header: two audit passes complete, open items typed Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Align the bind's dissolution trigger with the doc's own authority model (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * WIP: compiler correctness * Ladder follow-up: adopt the post-merge verdict (8 corrections) + the guarantee-ladder roadmap section Corrections, each verified against main before adoption: 1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque ... every proof-carrier is presently forgeable") was false as stated; corrected to an audited-status claim: sole_constructor is the candidate wall, completeness for generic carriers unverified. The earlier keyword-set inference is withdrawn in the Sec 10 ledger. 2. Subject grain: rung honesty is measured at a declared acceptance boundary; a class's rung is the MINIMUM across in-scope paths (the interpreter refuses the mislabeled call that order_typed_call_args reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1 carrier gains subject_grain/acceptance_boundary/compile_mode/ realization_target/covered_population. 3. Seed rungs demoted: return/data/generic, field-through-generics, exhaustiveness, cardinality, full ==-class, and L4 all to UnknownUnmeasured (compile admission proven is not runtime disposition proven); census marked specimen-denominated; unknown- method R0 scoped to the interpretation path. 4. Dissolution on climb amended in DESIGN 4b: production handling dissolves; the RED + positive controls REMAIN enrolled as the evidence the higher rung stays real. 5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows + witness-test fixture migrated); the guarantee-recovery row now carries BOTH anchors typed, not one typed + one in prose. Carrier note records that List admits [] — the exact cardinality gap the ladder tracks — with the doc-graph witnesses as the interim wall. 6. cardinality_fold_propagation_test relabeled everywhere as manual value-level specimens (length homomorphism over literals + runtime refine_byte); "not new design" softened to the accurate scope statement; the roadmap cardinality node re-briefed accordingly. 7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a generic dimension mechanism; extension-vs-redesign is an open audit question that roadmap pricing must carry. 8. Sec 1 "was not built" -> "never completed as an exhaustive acceptance contract"; Sec 11 queue updated (correctness-dimensions done; sole_constructor completeness audit added). Additions (operator direction): ROADMAP gains the "Guarantee ladder — climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes in ticket format with dependency edges (probe corpus gates the four floor walls; carrier gates cardinality slice, emitters, prevalence; exemption removal gates on the call-shape + inhabitance walls). The capability node is the sole_constructor completeness audit. State-vs- work split recorded on the carrier: rung STATE lives in the Stage-1 claims carrier and is emitted (ladder-census-emitters node); roadmap nodes track CLIMBS. Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap authority 35/35, model 9/9, focus 12/12. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give works its executing consumers (review 45336): nonempty wall, symbol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * De-inflate the three climb-node headlines (review 45349): work nodes name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Ladder nodes join the declared roadmap graph; binds nonempty by construction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Trim the three over-budget ladder briefs to the operator's 100-word ticket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Containment predicates consume doc_all_nodes, the one canonical walker (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Post-merge verdict follow-up: open-candidate honesty, anchored baseline, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Route the ambiguity wall and cardinality seam through the closure door (review 45545) The first edge set let compiler-accepted-obligation-closure land while floor-method-ambiguity-wall and cardinality-vertical-slice stayed open — the door would have certified "every required judgment established" over two required-open judgments (the grid marks the cardinality seam P0.2 minimum-R2 and ambiguity part of resolved identity; the verdict's spine routes ALL P0 obligations through the door). Both are now prerequisites of the closure; residual prevalence depends on the door alone. Authority 38/38, focus 12/12, page 28/28, drift 8/8; regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Reconcile the sec-7b behavior-count passage to past tense (review 45558) Sec 7b still described the 5-behaviors drift as current after this PR corrected the authority — the stale-claim problem the PR closes elsewhere. The passage now records the drift as found-and-corrected, keeps the specimen's evidentiary value (the denominator drifted silently in prose), and leaves the Match-promotion adjudication question with the queue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Remove probe demo scaffolding (net-zero vs main: files added by autocommit sweep mid-run, deleted after measurement) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Call-shape wall: refuse unknown argument labels and surplus positionals at the direct-call seam, mirroring the runtime contract The compile seam was silent on both classes call_function_inner refuses at runtime, and the emitter reordered mislabeled args positionally — two realizations of one program disagreeing silently. direct_call_shape_diags (v1.compiler.infer) closes both, blocking, exemption-free (a label has no representation gap). Census before landing refused 28 live rename fossils in 5 fns (to_string i->value, arm_body, is_import_slot_node, fold_list init->empty, path->path_opt), all relabeled to their declared authority; +3 fixed in the measured sig-unresolved blind spot. Probe pair pre/post, enrolled ct_call_shape_wall_witness_test RED/controls, regen fixed point divergence 0, whole-corpus compile-clean 0 blocking. Duplicate/missing stay unwalled with triggers (interpreter-first parity pair next). Roadmap node + census rows amended; ROADMAP regenerated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * Roster the call-shape witness blob in the scaffold index (review 45655) ct_call_shape_wall_witness_test joined compiler_tests_rust without its LanguageSourceScaffoldRow, so the exact-equality enrollment witness (compiler_tests_rust_blobs_are_all_rostered, 29 declared vs 28 rostered) would red on CI. Row added with the same hand-assertion scaffold trigger as its peers and enrolled in the roster; witness re-run green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Repair the silent-red ord-eligibility wall: name-grain arms admit only childless nodes d975e10 (2026-07-21) moved Symbol onto the name-only opaque-alias roster, dropping the shape check its enrolled negative control pins — Symbol<Float> became BTreeSet-eligible by name, and the RED sat invisible for ten days because the Rust unit suite left CI on 2026-07-11. Childless gate restores the shape constraint (zero corpus impact; regen fixed point holds); incident + dark-suite evidence gap filed as gap-analysis sixth-pass ledger + queue item 9 (operator decision, priced by this incident). Found by tidy-deer-730 during the 7484 main integration. Suite: 30 passed / 0 failed (was 1 failed). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Dedupe the call-shape witness aggregator entry after the main merge The merge auto-combined both sides' insertions of ct_call_shape_wall_witness_test into compiler_tests_source(); a duplicate generates the #[test] twice. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Spine reconciliation: recut the merged P0 slices at their actual grain, add the measurement-schema stage, split the acceptance door Adopts the operator spine verdict (2026-08-01, seventh pass) into the roadmap authority and the gap analysis: - ladder-measurement-schema precedes probes AND carrier (the receipt protocol both meet through; breaks the probes/carrier protocol cycle). - The three merged P0 slices recut at their actual grain, identities tombstoned: floor-call-shape-wall -> call-label-and-surplus-wall (accepted, #7519) + missing/duplicate + signature-resolution siblings; floor-method-existence-wall -> method-established-surface-wall (accepted, #7484) + receiver-normalization + zero-resolution siblings; floor-inhabitance-wall -> declared-conformance-ground-fragment (accepted, #7484) + grounding + general-wall siblings. - The Accepted door split mechanism/floor/extended (compiler-accepted-obligation-closure tombstoned): the audit form lands with the carrier; refusal never turns on over a known-open judgment (review 45545's substance preserved in the activation nodes). - Exemption removal re-grounded on argument-type-compatibility grounding + declared-conformance grounding (labels never gated it). - guarantee_ladder_edges rewritten wholesale; emitters parallel with the baseline; baseline defined as a two-revision execution. - Gap analysis sec 12 updated in place (Stage 0/1a/1c/2-amendment/4/6/6b); stale dissolution triggers repointed (doc_graph_roots, doc_reachability_witness_test); tombstone-note staleness fixed. - ROADMAP.md regenerated via main_wet; roadmap witness receipts 100 PASS (brief budgets, edge endpoints, acyclicity, identity registry with five tombstones); regen_stage0 --verify divergence 0. The branch additionally carries the ord-eligibility silent-red repair (childless gate on name-grain arms + incident note) and the clean regen of the generated stage0 files after the origin/main merge. Known pre-existing: the whole-tree cold census refuses 23 ambiguous-reference diagnostics in dag/test/claim/occurrence_binding_resolve_witness_test.dag (landed with #7508, byte-identical to origin/main; handed off to the occurrence lane). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Recut the extended activation as per-class admissions (review 45918) The first cut kept requires-all edges on one extended-activation node while its prose promised class-by-class widening — the graph would have deferred every admission behind the slowest climb, preserving the monolithic deferral the door split dissolves. Now: four per-class admission nodes (extended-admission-cardinality/-ambiguity/-v2-realization/-v2-translate, each <- floor-closure + its own climb, ready the day that climb lands) and accepted-extended-obligation-closure recut as the terminal roster-completeness certification, where requires-all honestly belongs. Same closure identity (no slug change, no tombstone); four fresh identities minted. Stage 6b + seventh-pass ledger + lane note updated; ROADMAP regenerated; graph/budget/identity witnesses 26 PASS. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Trim the ord name-grain note to its structural constraint (review 45929) The in-code note duplicated the incident narrative the gap analysis already records (sixth-pass ledger + queue item 9) — a parallel ledger realized into the emitted seed with no executable consumer. The carrier keeps only the constraint the code cannot show: why name-grain arms admit childless nodes only, the discriminating RED's symbol, and the shape-examining sibling path. regen_stage0 divergence 0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Spine A Stage 0: the guarantee measurement schema — evidence identifies its subject before anyone measures gunbc.guarantee_measurement carries the vocabulary probes and claims meet through, and nothing else (roadmap node ladder-measurement-schema; operator spine verdict 2026-08-01): GuaranteeClassId/PathId/ProbeId brands; GuaranteePath over four closed minimal axes (subject grain, acceptance boundary incl. the InferToEval/InferToTranslate phase boundaries the containment workstream consumes, compile mode, realization target with GuaranteeTargetName deferred-grounding brand); GuaranteeMeasurementReceipt with every field required (subject_revision x harness_revision x probe_set_digest, reusing std.types.CommitSha and std.content_hash); ProbeObservation as the raw outcome sum with ProbeNotRunnable structurally separated from verdicts (top-as-ignorance never readable as pass/fail); exactly-one path resolution and a receipt->path join that refuses unknown and duplicate. Registry mechanism without a registry population - no probe executes, no class rows, no disposition, no rung. An initial ObservedOutcome name collided with gunbc.output_policy's process-outcome type (whole-tree census caught the bare-reference break); renamed to ProbeObservation, census back to 0 blocking. Receipts: 8/8 synthetic-row witnesses green by execution (round-trip join, unknown-path refusal, duplicate-registry refusal never-first-pick, exactly-one resolution across four boundary variants, both uniqueness REDs, digest input-determinism incl. order sensitivity, verdict/ignorance separation); whole-tree compile 0 blocking; regen_divergence_count=0; generated artifacts zero drift. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Record the second-consumer re-grounding trigger for observed_is_verdict (review 46075) The predicate/walker dissolution rule triggers where a canonical fold already exists (nat_cata) or a substrate walk is extended; neither holds for a freshly declared domain sum whose only query this is. The note now records the named trigger: when the claims carrier lands as the sum's second consumer, a probe_observation fold becomes the canonical surface and observed_is_verdict re-expresses through it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Grant publication for the eight ungranted #7544 files (main-side gate breakage) The publication gate reds on current main itself: #7544 (heal-revalidation) merged after the P-B wall landed via #7560 but its CI raced the wall, so its eight new files carry no PublicFilePublishGrant rows and every PR merging current main inherits the failure. Rows added for all eight (mechanical placement declarations for files already public on main); cutover..HEAD Added/Copied/Renamed set now fully rostered, gate witnesses green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Grant publication for the three ungranted #7563 files (second main-side race) Same class as the #7544 fix one commit ago: #7563 merged on a pre-wall CI run, adding three SCM-kernel files with no grant rows. Roster now covers the full cutover..HEAD set including current main. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Thread GuaranteePathId through resolution and its refusal variants (review 46179) The resolver's key and both refusal-variant payloads carry the brand end-to-end; join_receipt_to_path no longer erases receipt.path to String. Measured the enforcement honestly: two executed controls show the checker accepting a bare String at a branded parameter and a branded record field, so the note records this as model-correctness and erasure-removal, with brand acceptance-enforcement handed to the probe corpus as its own class. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Merge origin/main; dedupe the roster union and grant the two #7550 lean files The alphabetized roster body on main already carried the 11 straggler paths, so #7580's tail block duplicated every one of them; the union keeps exactly one row per path, with this branch's two guarantee rows slotted alphabetically. Coverage against the cutover then caught a fourth race instance: #7550 merged two new files with no grant rows (dag/extdeps/languages/lean/overflow.dag and its witness), redding main's gate again - swept into the same roster here. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Observation counts are Nat, with the enforcement gap measured (review 46287) RefusedTyped.count and AcceptedCounted.count carry the cardinal type, and the fold's arm signatures follow. An executed control shows the checker still accepting a negative at the Nat field today, so the note records the swap as model-correctness with refusal owed to the numeric-refinement acceptance class, not claimed as a wall. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Orthogonalize the path axes instead of enumerating families (review 46308) InterpreterRun renames to RuntimeRun: run-level acceptance happens IN the path's realization, so which runtime is the realization axis's fact and an emitted-run path (the divergence probes' subject) is expressible rather than contradictory. The compile_mode axis deletes: every landed control derives its pipeline from its boundary, so the stored mode was a second representation whose only writable novelty was the contradiction; it returns as a stored axis with the first path measured under two pipelines at one boundary. Both review-named contradictions are now unwritable without a family coproduct, whose rows would restate the orthogonal axes per combination (the N-by-M shape DESIGN 2 folds into axes). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
4 of 6 tasks
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 2, 2026
Derive v2 InferToEval receipt observations from executed infer diagnostics instead of fabricating counts; add guarantee_probe_ids_unique enforcement. Reserve gunbc#7555 translate identities outside guarantee_probe_ids until that OPEN PR merges — slice-1 migration covers only #7484, #7519, #7485. Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 2, 2026
Derive v2 InferToEval receipt observations from executed infer diagnostics instead of fabricating counts; add guarantee_probe_ids_unique enforcement. Reserve gunbc#7555 translate identities outside guarantee_probe_ids until that OPEN PR merges — slice-1 migration covers only #7484, #7519, #7485. Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 2, 2026
Derive v2 InferToEval receipt observations from executed infer diagnostics instead of fabricating counts; add guarantee_probe_ids_unique enforcement. Reserve gunbc#7555 translate identities outside guarantee_probe_ids until that OPEN PR merges — slice-1 migration covers only #7484, #7519, #7485. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 2, 2026
…air, probe-adequacy mandate (#7643) * WIP: compiler correctness * Bind the guarantee-recovery analysis into the doc graph The analysis note landed as an orphan doc: gunbc.doc_graph_roots states that "an unbound doc is an orphan, loudly", and CI duly refused at be1a001 with doc_graph_has_no_orphan_docs returning false in both the dag/test/claim and src/v2/lens consumers. Registered as two HandAuthoredDocBind rows rather than one, because the analysis binds to two independent carriers and they dissolve on different triggers: - v1.compiler.infer module_skips_direct_call_arg_check — the one named violation of the dimension contract's "no escape hatch" clause (docs/thesis/correctness-dimensions.md), exempting v2.* and v1.compiler.* from direct-call argument checking. - v2.std.constraints solve_constraints — passes graph.root as source_facts, algebra AND the sole candidate, so the grounding proof reduces to well_formed(root) and is relabelled CanonicalGrounding. Green by execution, both directions: RED is the CI failure at be1a001; GREEN is all five witnesses in dag/test/claim/doc_reachability_witness_test.dag plus doc_graph_is_clean in src/v2/lens/doc_reachability_test.dag passing locally against the live docs/ tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Reconcile the gap analysis against the independent review — three corrections adopted, receipts verified Adopted (all verified on main this pass): - Cardinality reclassified UNEXPRESSIBLE -> RepresentableButForgeable, not statically propagated: v2.std.refinement exists, NonEmptyList fixture + green cardinality_fold_propagation_test exist, and refined_vacuous_stub_pack's Rejected arm returns Refined { base } (the carrier proves nothing). New Sec 4b: the operator independently re-directed this exact guarantee on 2026-07-04 (interface-summary-declared-use-arity.md Sec 3.1, "hard error in the language") — the intent is not lost; the lattice design pass (FLAG E) never started. - Failure history rewritten (Sec 2): the exemption dates to 2026-06-08 (a13fb57), pre-bankruptcy; correctness-dimensions.md marked type safety "Yes (blocking)" while return position was unchecked — so the ledger overstated, then the auditable contract was deleted. The pipeline_steps_empty_arm_note receipt is withdrawn: empty there is a deliberate total semantics, not a priced-out wall. - Status vocabulary widened to the review's 11-state lattice; v2 terminal calibrated (validate_then_compile door + loop-bound wall are real; InferredTree is still not a proof boundary); application-arity row added (formal-driven walk, positional fallback for misspelled labels, ArityMismatch is constructor-arity); PatternLookupBlocked's silent [] arm confirmed (PatternDynamic does diagnose — review corrected there). - Sec 7b: DESIGN.md is projected from gunbc.design_document, and its "5 behaviors" is stale against v2.std.node's six (Match) — the guarantee authority lands as .dag rows, never hand-edited prose. - Sequencing reconciled to 7 stages: claims authority + expecting-red probe corpus together; zero-resolution method wall now, ambiguity wall census-first; cardinality vertical slice third. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Status header: two audit passes complete, open items typed Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Align the bind's dissolution trigger with the doc's own authority model (review 45299) The first HandAuthoredDocBind trigger said "re-homed into DESIGN.md as its specification half" — wording that predates the reconciliation pass's Sec 7b finding that DESIGN.md is a projection of gunbc.design_document. As written, a direct DESIGN.md edit could have satisfied the trigger, which is exactly the Sec 3 parallel-representation failure Sec 7b names. Trigger now requires .dag claim rows projected via gunbc.design_document and states explicitly that a hand edit does not satisfy it. All five doc-reachability witnesses re-run green by execution after the edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 45305 (merge same-slug binds, fix stale block) + land the safety ladder as the organizing frame Review 45305, both findings verified correct and fixed: - doc_graph_roots: the two HandAuthoredDocBind rows shared (home, slug), which the carrier's own note defines as the symbolic identity — one doc had two independently removable authority rows. Merged to ONE row whose trigger anchors both carriers (module_skips_direct_call_arg_check, solve_constraints) and gates dissolution on BOTH conditions, with the merge provenance recorded on the carrier. (Observed, not fixed here: module-identity-storage-binding-design and accelerator-demo-roundtrip also carry same-slug duplicate rows — pre-existing, follow-up material.) - Sec 8b's example-0 block still said "unexpressible", contradicting the Sec 4 reclassification and mis-aiming the archetypal RED at inventing a carrier instead of sealing/propagating the one that exists. Rewritten: the RED exercises unforgeable construction + seam propagation, expected refusal at the 0..n -> 1..n seam. Operator direction, same pass: the safety ladder is now Sec 1b, the organizing frame — R3 structurally-impossible / R2 structural guarantee / R1 testable / R0 mitigatable / below-the-floor silent (forbidden, Sec 5). Three rules: floor absolute; climb to a STATED ceiling (mathematical / capability / price — the capability ceiling is unforgeable construction, blocked on reference-level visibility: the keyword set has no private/sealed/opaque); reported rung == measured rung, lens-checked for inflation and stalls. Includes the specimen table (the session's classes placed, cross-representation == as the exemplar full climb) and the non-goals roster (external reality, arbitrary predicates, budgets, optimality, self-governance, byte-identical self-emit — low ceilings BY DESIGN). Stage 1 claim rows gain current_rung / ceiling / next_rung_trigger. All five doc-reachability witnesses re-run green by execution after both file changes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * WIP: compiler correctness * Ladder follow-up: adopt the post-merge verdict (8 corrections) + the guarantee-ladder roadmap section Corrections, each verified against main before adoption: 1. sole_constructor EXISTS (SoleConstructorViolation, sealed-record specimen) — the DESIGN 4b capability claim ("no private/sealed/opaque ... every proof-carrier is presently forgeable") was false as stated; corrected to an audited-status claim: sole_constructor is the candidate wall, completeness for generic carriers unverified. The earlier keyword-set inference is withdrawn in the Sec 10 ledger. 2. Subject grain: rung honesty is measured at a declared acceptance boundary; a class's rung is the MINIMUM across in-scope paths (the interpreter refuses the mislabeled call that order_typed_call_args reorders for emission). DESIGN 4b meta-obligation 1 amended; Stage-1 carrier gains subject_grain/acceptance_boundary/compile_mode/ realization_target/covered_population. 3. Seed rungs demoted: return/data/generic, field-through-generics, exhaustiveness, cardinality, full ==-class, and L4 all to UnknownUnmeasured (compile admission proven is not runtime disposition proven); census marked specimen-denominated; unknown- method R0 scoped to the interpretation path. 4. Dissolution on climb amended in DESIGN 4b: production handling dissolves; the RED + positive controls REMAIN enrolled as the evidence the higher rung stays real. 5. HandAuthoredDocBind.work -> works: List<DeclarationRef> (40 rows + witness-test fixture migrated); the guarantee-recovery row now carries BOTH anchors typed, not one typed + one in prose. Carrier note records that List admits [] — the exact cardinality gap the ladder tracks — with the doc-graph witnesses as the interim wall. 6. cardinality_fold_propagation_test relabeled everywhere as manual value-level specimens (length homomorphism over literals + runtime refine_byte); "not new design" softened to the accurate scope statement; the roadmap cardinality node re-briefed accordingly. 7. Sec 8c recast: TypeBinding carries two bespoke coordinates, not a generic dimension mechanism; extension-vs-redesign is an open audit question that roadmap pricing must carry. 8. Sec 1 "was not built" -> "never completed as an exhaustive acceptance contract"; Sec 11 queue updated (correctness-dimensions done; sole_constructor completeness audit added). Additions (operator direction): ROADMAP gains the "Guarantee ladder — climb plan (DESIGN 4b)" section — 13 sized, unowned, dispatchable nodes in ticket format with dependency edges (probe corpus gates the four floor walls; carrier gates cardinality slice, emitters, prevalence; exemption removal gates on the call-shape + inhabitance walls). The capability node is the sole_constructor completeness audit. State-vs- work split recorded on the carrier: rung STATE lives in the Stage-1 claims carrier and is emitted (ladder-census-emitters node); roadmap nodes track CLIMBS. Verified by execution: main_wet regen (DESIGN.md + ROADMAP.md projections, never hand-edited); drift 4/4; doc-graph 5/5; roadmap authority 35/35, model 9/9, focus 12/12. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Give works its executing consumers (review 45336): nonempty wall, symbol fields, two-anchor pin, RED control review 45336 was correct: works had a typed carrier and zero readers — representation without a consumer is specification-without-execution (DESIGN 5 / E-10), the exact defect class the guarantee analysis documents, reproduced in its own fix. Consumers now executing in dag/test/claim/doc_reachability_witness_test: - doc_graph_binds_works_all_nonempty — an emptied works list reds - doc_graph_works_refs_carry_symbols — a ref stripped of module_path or decl_name reds - guarantee_recovery_bind_pins_both_anchors — deleting or renaming either of the two anchors (module_skips_direct_call_arg_check, solve_constraints) reds; row multiplicity pinned to one - doc_graph_works_empty_red_control — synthetic empty-works bind fails the predicate, proving the consumer discriminates Predicates live on the authority (gunbc.doc_graph_roots) so the witness consumes the carrier's own definition. Residue named on the carrier note: staleness against the live tree (a ref naming a decl that no longer exists) is NOT witnessed — v1.compiler.* is outside the witness compile pool, so ref-vs-tree resolution is exactly the feature:cited-symbol-resolution lens DESIGN 3 already names; the refs are symbolic citations and inherit that trigger. All 11 doc-reachability witnesses green by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * De-inflate the three climb-node headlines (review 45349): work nodes name the target rung; current rung defers to the census review 45349, third correct catch in this lane: the census demoted method existence (R0 interpretation-path-only), inhabitance (UnknownUnmeasured), and cardinality (UnknownUnmeasured) — and the roadmap nodes, authored before the demotion pass, kept "R0 -> R2" headlines, re-inflating the same claims the same day at the canonical authority. The section's own note says rung STATE lives in the claims carrier, never these nodes; the headlines now name only the TARGET rung and point at the census for current state, per DESIGN 4b's minimum-across-paths rule. ROADMAP.md regenerated via main_wet; roadmap authority witnesses 35/35; drift witnesses 4/4, by execution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Ladder nodes join the declared roadmap graph; binds nonempty by construction; rung state derived, never stored Executes the operator's 10-item merge bar on #7489 plus reviews 45356/45367 and tidy-deer-730's measured receipts: - guarantee_ladder_section() deleted; 16 nodes + 23 edges enter declared_roadmap_nodes()/declared_roadmap_edges() via guarantee_ladder_nodes()/ guarantee_ladder_edges(), owner "compiler-guarantee" (lane identity, unbound until closing contracts). Page visibility is the typed focus policy (lane added to roadmap_focus_selection). rendered⊆declared∪derived witnessed with a synthetic-ghost RED. - Graph corrections: probe corpus → carrier → baseline-prevalence → walls; prevalence split baseline/residual; new floor-generic-field-constraint-wall and floor-method-ambiguity-wall nodes; primitive-identity-join is a PREREQUISITE of the general method wall (measured: kernel algebra profiles vs interpreter dispatch fork, tidy-deer-730 on gunbc#7484); cardinality ← sole_constructor audit edge; capability node repointed off the parked visibility-grants doc. - Tickets de-stated: no current-rung transcription anywhere; carrier ticket rewritten to the four-carrier split (Requirement/Path/Measurement/derived Disposition, minimum across paths, no stored rung field) — reconciled across §12 Stage 1, DESIGN §4b tail, and the roadmap node (review 45367); five recovered vocabularies kept orthogonal. - HandAuthoredDocBind: primary_work + additional_works (zero-anchor bind unwritable); empty-works RED deleted with its validation, residue named; duplicate (home,slug) rows merged; bind-identity uniqueness witnessed with a synthetic-duplicate RED. - Census: method-existence subject-grain receipt (narrow kernel wall, gunbc#7484); parser silent-separator below-floor row; §11 items 6-8; §10 fourth-pass ledger. Witnesses: roadmap 37/37 (2 new), identity 9/9, focus 12/12, model 9/9, drift 8/8, doc-graph 11/11. ROADMAP.md/DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Trim the three over-budget ladder briefs to the operator's 100-word ticket law witness_ticket_brief_budget_holds_and_reds red on the CI floor: the carrier, method-existence, and cardinality briefs ran 169/128/111 words. The old section-local placement had escaped this law entirely (the exact ghost-universe defect the verdict named — the budget never saw those nodes); in the declared graph it applies. Briefs trimmed to 94/91/90 with every cut fact already carried in the gap analysis (sec 12 Stage 1b / Stage 2 amendment / the census), which each node links as its carrier. The budget itself is untouched — widening the declaration to satisfy the check is the DESIGN 5 tell, backwards. Page set 28/28, authority set green, regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Containment predicates consume doc_all_nodes, the one canonical walker (review 45412) document_rendered_nodes was a traversal fork beside roadmap_spawner's doc_all_nodes — same semantics, second walker. The predicates (whole-value ghost count + both RED probes) move INTO roadmap_spawner, the walker's module, because the spawner already imports roadmap_authority and the reverse import would cycle. The authority sheds the walker and its now-unused SectionElement imports; the containment note records both refused first cuts (identity-only membership, review 45406; the duplicate walker, review 45412) since each was this wall violating a law it enforces. Authority 38/38, spawner 16/16, page 28/28. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Post-merge verdict follow-up: open-candidate honesty, anchored baseline, FrontierAccepted, and the closure door Executes all six items of the operator's post-merge verdict on #7489, each verified against live state first (#7484 and #7485 confirmed OPEN; the anchor confirmed as the #7489 squash; Behavior confirmed six-membered): 1. Every "#7484 landed" claim replaced with open-candidate wording — main's disposition stated separately from candidate branch evidence (the ladder's rung-inflation rule applied to open-PR state; my transcription error). 2. Baseline prevalence anchored: anchor_commit 6c6e2dc (content-addressed, reproducible after in-flight merges; walls no longer race a live tree). 3. GuaranteeDisposition gains FrontierAccepted{diagnostic, accepted_boundary, evidence} — typed/located/counted but still Accepted; specimens MethodExistenceUndecided and GroundingNotDerived. 4. Graph: floor-parse-formation-wall + floor-record-construction-wall + compiler-accepted-obligation-closure added; v2-phase-carriers split into five staged nodes (self-grounding frontier → Translate refusal → inferred- tree completeness → per-kind derivation coverage → target realization gate) with the registry's FIRST TOMBSTONE (superseded_by the frontier node); method←join edge deleted per the zero-via-union nuance (join gates only the >1 wall and realization completeness); residual reroutes through the closure door. 5. DESIGN §4: closed vocabulary corrected to 6 connectives + 6 behaviors, matching v2.std.node.Behavior (the decidability denominator). 6. §1d provisional guarantee grid emitted as hand-authored interim, dissolve-on the carrier-emitted projection. Witnesses: authority 38/38, identity 9/9 (first tombstone passes the count-free tombstone claims), focus 12/12, model 9/9, page 28/28 (all 23 ladder briefs within the 100-word law), spawner 16/16, drift 8/8, doc 11/11. ROADMAP.md and DESIGN.md regenerated via main_wet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * chore: regenerate drifted generated artifacts (ci auto-heal) * Route the ambiguity wall and cardinality seam through the closure door (review 45545) The first edge set let compiler-accepted-obligation-closure land while floor-method-ambiguity-wall and cardinality-vertical-slice stayed open — the door would have certified "every required judgment established" over two required-open judgments (the grid marks the cardinality seam P0.2 minimum-R2 and ambiguity part of resolved identity; the verdict's spine routes ALL P0 obligations through the door). Both are now prerequisites of the closure; residual prevalence depends on the door alone. Authority 38/38, focus 12/12, page 28/28, drift 8/8; regen clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Reconcile the sec-7b behavior-count passage to past tense (review 45558) Sec 7b still described the 5-behaviors drift as current after this PR corrected the authority — the stale-claim problem the PR closes elsewhere. The passage now records the drift as found-and-corrected, keeps the specimen's evidentiary value (the denominator drifted silently in prose), and leaves the Match-promotion adjudication question with the queue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Remove probe demo scaffolding (net-zero vs main: files added by autocommit sweep mid-run, deleted after measurement) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: compiler correctness * Call-shape wall: refuse unknown argument labels and surplus positionals at the direct-call seam, mirroring the runtime contract The compile seam was silent on both classes call_function_inner refuses at runtime, and the emitter reordered mislabeled args positionally — two realizations of one program disagreeing silently. direct_call_shape_diags (v1.compiler.infer) closes both, blocking, exemption-free (a label has no representation gap). Census before landing refused 28 live rename fossils in 5 fns (to_string i->value, arm_body, is_import_slot_node, fold_list init->empty, path->path_opt), all relabeled to their declared authority; +3 fixed in the measured sig-unresolved blind spot. Probe pair pre/post, enrolled ct_call_shape_wall_witness_test RED/controls, regen fixed point divergence 0, whole-corpus compile-clean 0 blocking. Duplicate/missing stay unwalled with triggers (interpreter-first parity pair next). Roadmap node + census rows amended; ROADMAP regenerated. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * chore: regenerate drifted generated artifacts (ci auto-heal) * Roster the call-shape witness blob in the scaffold index (review 45655) ct_call_shape_wall_witness_test joined compiler_tests_rust without its LanguageSourceScaffoldRow, so the exact-equality enrollment witness (compiler_tests_rust_blobs_are_all_rostered, 29 declared vs 28 rostered) would red on CI. Row added with the same hand-assertion scaffold trigger as its peers and enrolled in the roster; witness re-run green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Repair the silent-red ord-eligibility wall: name-grain arms admit only childless nodes d975e10 (2026-07-21) moved Symbol onto the name-only opaque-alias roster, dropping the shape check its enrolled negative control pins — Symbol<Float> became BTreeSet-eligible by name, and the RED sat invisible for ten days because the Rust unit suite left CI on 2026-07-11. Childless gate restores the shape constraint (zero corpus impact; regen fixed point holds); incident + dark-suite evidence gap filed as gap-analysis sixth-pass ledger + queue item 9 (operator decision, priced by this incident). Found by tidy-deer-730 during the 7484 main integration. Suite: 30 passed / 0 failed (was 1 failed). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Dedupe the call-shape witness aggregator entry after the main merge The merge auto-combined both sides' insertions of ct_call_shape_wall_witness_test into compiler_tests_source(); a duplicate generates the #[test] twice. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Spine reconciliation: recut the merged P0 slices at their actual grain, add the measurement-schema stage, split the acceptance door Adopts the operator spine verdict (2026-08-01, seventh pass) into the roadmap authority and the gap analysis: - ladder-measurement-schema precedes probes AND carrier (the receipt protocol both meet through; breaks the probes/carrier protocol cycle). - The three merged P0 slices recut at their actual grain, identities tombstoned: floor-call-shape-wall -> call-label-and-surplus-wall (accepted, #7519) + missing/duplicate + signature-resolution siblings; floor-method-existence-wall -> method-established-surface-wall (accepted, #7484) + receiver-normalization + zero-resolution siblings; floor-inhabitance-wall -> declared-conformance-ground-fragment (accepted, #7484) + grounding + general-wall siblings. - The Accepted door split mechanism/floor/extended (compiler-accepted-obligation-closure tombstoned): the audit form lands with the carrier; refusal never turns on over a known-open judgment (review 45545's substance preserved in the activation nodes). - Exemption removal re-grounded on argument-type-compatibility grounding + declared-conformance grounding (labels never gated it). - guarantee_ladder_edges rewritten wholesale; emitters parallel with the baseline; baseline defined as a two-revision execution. - Gap analysis sec 12 updated in place (Stage 0/1a/1c/2-amendment/4/6/6b); stale dissolution triggers repointed (doc_graph_roots, doc_reachability_witness_test); tombstone-note staleness fixed. - ROADMAP.md regenerated via main_wet; roadmap witness receipts 100 PASS (brief budgets, edge endpoints, acyclicity, identity registry with five tombstones); regen_stage0 --verify divergence 0. The branch additionally carries the ord-eligibility silent-red repair (childless gate on name-grain arms + incident note) and the clean regen of the generated stage0 files after the origin/main merge. Known pre-existing: the whole-tree cold census refuses 23 ambiguous-reference diagnostics in dag/test/claim/occurrence_binding_resolve_witness_test.dag (landed with #7508, byte-identical to origin/main; handed off to the occurrence lane). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Recut the extended activation as per-class admissions (review 45918) The first cut kept requires-all edges on one extended-activation node while its prose promised class-by-class widening — the graph would have deferred every admission behind the slowest climb, preserving the monolithic deferral the door split dissolves. Now: four per-class admission nodes (extended-admission-cardinality/-ambiguity/-v2-realization/-v2-translate, each <- floor-closure + its own climb, ready the day that climb lands) and accepted-extended-obligation-closure recut as the terminal roster-completeness certification, where requires-all honestly belongs. Same closure identity (no slug change, no tombstone); four fresh identities minted. Stage 6b + seventh-pass ledger + lane note updated; ROADMAP regenerated; graph/budget/identity witnesses 26 PASS. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Trim the ord name-grain note to its structural constraint (review 45929) The in-code note duplicated the incident narrative the gap analysis already records (sixth-pass ledger + queue item 9) — a parallel ledger realized into the emitted seed with no executable consumer. The carrier keeps only the constraint the code cannot show: why name-grain arms admit childless nodes only, the discriminating RED's symbol, and the shape-examining sibling path. regen_stage0 divergence 0. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Spine A Stage 0: the guarantee measurement schema — evidence identifies its subject before anyone measures gunbc.guarantee_measurement carries the vocabulary probes and claims meet through, and nothing else (roadmap node ladder-measurement-schema; operator spine verdict 2026-08-01): GuaranteeClassId/PathId/ProbeId brands; GuaranteePath over four closed minimal axes (subject grain, acceptance boundary incl. the InferToEval/InferToTranslate phase boundaries the containment workstream consumes, compile mode, realization target with GuaranteeTargetName deferred-grounding brand); GuaranteeMeasurementReceipt with every field required (subject_revision x harness_revision x probe_set_digest, reusing std.types.CommitSha and std.content_hash); ProbeObservation as the raw outcome sum with ProbeNotRunnable structurally separated from verdicts (top-as-ignorance never readable as pass/fail); exactly-one path resolution and a receipt->path join that refuses unknown and duplicate. Registry mechanism without a registry population - no probe executes, no class rows, no disposition, no rung. An initial ObservedOutcome name collided with gunbc.output_policy's process-outcome type (whole-tree census caught the bare-reference break); renamed to ProbeObservation, census back to 0 blocking. Receipts: 8/8 synthetic-row witnesses green by execution (round-trip join, unknown-path refusal, duplicate-registry refusal never-first-pick, exactly-one resolution across four boundary variants, both uniqueness REDs, digest input-determinism incl. order sensitivity, verdict/ignorance separation); whole-tree compile 0 blocking; regen_divergence_count=0; generated artifacts zero drift. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Record the second-consumer re-grounding trigger for observed_is_verdict (review 46075) The predicate/walker dissolution rule triggers where a canonical fold already exists (nat_cata) or a substrate walk is extended; neither holds for a freshly declared domain sum whose only query this is. The note now records the named trigger: when the claims carrier lands as the sum's second consumer, a probe_observation fold becomes the canonical surface and observed_is_verdict re-expresses through it. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Grant publication for the eight ungranted #7544 files (main-side gate breakage) The publication gate reds on current main itself: #7544 (heal-revalidation) merged after the P-B wall landed via #7560 but its CI raced the wall, so its eight new files carry no PublicFilePublishGrant rows and every PR merging current main inherits the failure. Rows added for all eight (mechanical placement declarations for files already public on main); cutover..HEAD Added/Copied/Renamed set now fully rostered, gate witnesses green. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Grant publication for the three ungranted #7563 files (second main-side race) Same class as the #7544 fix one commit ago: #7563 merged on a pre-wall CI run, adding three SCM-kernel files with no grant rows. Roster now covers the full cutover..HEAD set including current main. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Thread GuaranteePathId through resolution and its refusal variants (review 46179) The resolver's key and both refusal-variant payloads carry the brand end-to-end; join_receipt_to_path no longer erases receipt.path to String. Measured the enforcement honestly: two executed controls show the checker accepting a bare String at a branded parameter and a branded record field, so the note records this as model-correctness and erasure-removal, with brand acceptance-enforcement handed to the probe corpus as its own class. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Merge origin/main; dedupe the roster union and grant the two #7550 lean files The alphabetized roster body on main already carried the 11 straggler paths, so #7580's tail block duplicated every one of them; the union keeps exactly one row per path, with this branch's two guarantee rows slotted alphabetically. Coverage against the cutover then caught a fourth race instance: #7550 merged two new files with no grant rows (dag/extdeps/languages/lean/overflow.dag and its witness), redding main's gate again - swept into the same roster here. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Observation counts are Nat, with the enforcement gap measured (review 46287) RefusedTyped.count and AcceptedCounted.count carry the cardinal type, and the fold's arm signatures follow. An executed control shows the checker still accepting a negative at the Nat field today, so the note records the swap as model-correctness with refusal owed to the numeric-refinement acceptance class, not claimed as a wall. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Orthogonalize the path axes instead of enumerating families (review 46308) InterpreterRun renames to RuntimeRun: run-level acceptance happens IN the path's realization, so which runtime is the realization axis's fact and an emitted-run path (the divergence probes' subject) is expressible rather than contradictory. The compile_mode axis deletes: every landed control derives its pipeline from its boundary, so the stored mode was a second representation whose only writable novelty was the contradiction; it returns as a stored axis with the first path measured under two pipelines at one boundary. Both review-named contradictions are now unwritable without a family coproduct, whose rows would restate the orthogonal axes per combination (the N-by-M shape DESIGN 2 folds into axes). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * Roadmap: schema acceptance receipt, axis-prose repair, probe-adequacy mandate Three post-merge obligations from the ladder-measurement-schema landing (gunbc#7572, merged 2026-08-01): - RoadmapAcceptanceReceipt for ladder-measurement-schema: executed red-control (duplicate_class_id_reds_uniqueness) + delivered handback (the schema module and its witness), criteria digest pinned over the corrected boundary text; the node leaves the active graph and the probe corpus promotes to lane top. - Axis-prose repair (snappy-eagle's prose-grep rule): the schema and carrier boundaries plus gap-analysis sec 12 no longer name the deleted compile_mode axis; each records the RuntimeRun re-read and the deletion's re-entry trigger instead (review 46308 on gunbc#7572). - Probe-adequacy mandate in guarantee-baseline-prevalence red_control: closure AND shape AND corpus-prevalence cross-check REQUIRED for every below-floor or silent-class row; a row without its adequacy receipt is unenrollable. ROADMAP.md regenerated via main_wet on the artifact gate; roadmap authority suite 39/39 by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Reconcile the schema node's acceptance bar to what Stage 0 owns (review 46861) The red_control claimed receipt-field unwritability - a wall that was never this node's to claim: corpus-wide construction enforcement is the floor-record-construction-wall class's bar, exactly as the module's receipt_identity_note states. The bar now says required-by-shape with enforcement explicitly delegated, the criteria digest re-pins over the honest text (74da4d8be7125c81, derived by execution), and the receipt stands on the executed duplicate-id control. Also removes a stray digest-probe test fn a background sweep had committed mid-measurement. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> * WIP: compiler correctness * Trim claims-carrier boundary under the 100-word ticket-brief budget; drop probe scaffolding The compile_mode de-reference added in this PR pushed the ladder-claims-carrier boundary to 101 words, redding witness_ticket_brief_budget_holds_and_reds (the enforcing witness for the boundary budget — CI batch 3). 'the landed ... row' reassurance prose becomes 'per gunbc.guarantee_measurement' (98 words); the single-authority pointer survives. ROADMAP.md regenerated. Also removes the transient probe_brief_violations diagnostics fn the autocommit sweeper captured (review 46970). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 2, 2026
Derive v2 InferToEval receipt observations from executed infer diagnostics instead of fabricating counts; add guarantee_probe_ids_unique enforcement. Reserve gunbc#7555 translate identities outside guarantee_probe_ids until that OPEN PR merges — slice-1 migration covers only #7484, #7519, #7485. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
added a commit
that referenced
this pull request
Aug 2, 2026
…guarantee_measurement identities (#7638) * WIP: ladder-probe-corpus slice 1: migrate landed wall controls onto gunbc.gua * Strengthen guarantee probe corpus with mutation controls and canonical ordering. Adds discriminating RED controls, probe_observation_fold routing witnesses, lexicographic probe roster fix, and v2 path identity joins so slice 1 receipts are keyed by schema identities without duplicating the dark-suite originals. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: ladder-probe-corpus slice 1: migrate landed wall controls onto gunbc.gua * Route green_control witness through observation_is_clean fold. Replaces hand-matching ProbeObservation arms in green_control_observation_is_accepted_clean with the corpus bridge helper (review 46857). Co-authored-by: Cursor <cursoragent@cursor.com> * Address review 46867: lex order, v2 wiring, revision params, dead code. Reorder probe roster to true lexicographic authority; delete unused census_has_any_rows; require subject/harness revisions on receipt builders (fixtures own placeholders); wire infer_self_grounding_wall_test to corpus identities with executing join witness; remove synthetic v2 path-join tests from dag witness. Co-authored-by: Cursor <cursoragent@cursor.com> * Return Optional counts from census class helpers. Replaces the 0-1 NotRunnable sentinel with Int? so unknown cannot masquerade as a cardinal count (review 46888 non-blocking nit). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: ladder-probe-corpus slice 1: migrate landed wall controls onto gunbc.gua * Address review 46918 and correct #7555 slice-1 scope. Derive v2 InferToEval receipt observations from executed infer diagnostics instead of fabricating counts; add guarantee_probe_ids_unique enforcement. Reserve gunbc#7555 translate identities outside guarantee_probe_ids until that OPEN PR merges — slice-1 migration covers only #7484, #7519, #7485. Co-authored-by: Cursor <cursoragent@cursor.com> * Connect v2 frontier green probe to executing receipt join. Adds wall_frontier_derived_green_receipt_joins_corpus_identity using the derived branch fixture (clean infer diagnostics) so v2_frontier_green_probe in guarantee_probe_ids has a real receipt consumer (review 46943). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: ladder-probe-corpus slice 1: migrate landed wall controls onto gunbc.gua * WIP: ladder-probe-corpus slice 1: migrate landed wall controls onto gunbc.gua * Bind guarantee probe receipts to canonical GuaranteeProbeRow rows. Review 46953: class, path, probe, and expectation now live in one registry row; receipt builders take the row instead of independently threaded ids. Co-authored-by: Cursor <cursoragent@cursor.com> * Import ReceiptPathUnknown and ReceiptPathDuplicate in probe corpus. review 46989: receipt_joins_v1_compile_path matches all three ReceiptJoin variants; namespace-only resolution requires explicit imports. Co-authored-by: Cursor <cursoragent@cursor.com> * Move string lex compare and Ordering elimination to std. review 47003: add ordering_fold/ordering_is_less on std.algebra.Ordering and string_lex_compare/string_is_lexicographically_before on std.string_type; guarantee_probe_corpus consumes those surfaces instead of local predicate/walker copies. Co-authored-by: Cursor <cursoragent@cursor.com> * Regen stage0 after std.algebra ordering_fold landing. Fixes regen_verify_gate_passes drift on std_algebra.rs. Co-authored-by: Cursor <cursoragent@cursor.com> * Enforce path-typed receipts and honest probe-set digests. review 47050: V1CompileProbeRow/V2InferEvalProbeRow fix path at construction; builders take executed_probe_ids for probe_set_digest; witnesses pass the single probe they actually run and add a digest honesty control. Co-authored-by: Cursor <cursoragent@cursor.com> * Route probe expectation checks through probe_expectation_fold. Addresses review 47205: dissolve the hand-match on ProbeExpectation in probe_row_observation_holds by adding ProbeExpectationFold alongside the type, mirroring probe_observation_fold in gunbc.guarantee_measurement. Co-authored-by: Cursor <cursoragent@cursor.com> * Derive guarantee probe receipt revisions from measured content. Addresses review 47213: replace all-zero/all-one placeholder CommitSha stamps with content-derived synthetic revisions — subject from compiled source or named infer fixture, harness from probe id under a stable tag. Adds discriminating witness that revisions vary with source/probe. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix parse error in subject_revision witness test. Leading-line `!=` after a newline is not a valid expression continuation in .dag; rewrite with let bindings (CI regen/heal parse failure). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: ladder-probe-corpus slice 1: migrate landed wall controls onto gunbc.gua * Strengthen guarantee receipt identity witnesses for review 47237. Harness revision now fingerprints scope-note content (not probe id alone), and a new witness proves alternate harness material changes the digest. Co-authored-by: Cursor <cursoragent@cursor.com> * Ground guarantee receipt revisions on MeasurementRevision coproduct. Add GitRevision | ContentFingerprint to Stage-0 schema so slice-1 witnesses mint honest ContentFingerprint identities instead of casting fnv digests to CommitSha; fix missing content_hash_combine_structural import. Co-authored-by: Cursor <cursoragent@cursor.com> * Remove stale CompileDiagnosticCensus inert-carrier roster row. gunbc.guarantee_probe_corpus now matches on CompileDiagnosticCensus in production code, so the carrier is live and the roster entry is stale. Co-authored-by: Cursor <cursoragent@cursor.com> * Keep #7555 path and class out of canonical probe registries. Slice 1 canonical guarantee_probe_paths and guarantee_probe_class_ids cover only landed controls; translate identities stay in reserved rosters until gunbc#7555 executing evidence lands. Co-authored-by: Cursor <cursoragent@cursor.com> * Ground guarantee receipt revisions on executed harness and fixtures. Fingerprint v1/v2 harness revisions from the executing spine plus registry ProbeExpectation; derive v2 subject revisions from Node content_hash; add explicit dark-suite disposition rows per gap-analysis sec 11 item 9. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: ladder-probe-corpus slice 1: migrate landed wall controls onto gunbc.gua * Import GuaranteeProbeId in infer self-grounding wall witness. Fixes unresolved bare GuaranteeProbeId reference in infer_wall_harness_revision. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix witness parse errors from line-leading != and + The dag parser rejects continuation lines that start with != or + inside match arms; bind harness revisions and fold penalties with let instead. Co-authored-by: Cursor <cursoragent@cursor.com> * Fail closed when probe id spans active and reserved registries resolve_canonical_probe_row now resolves over the combined active+reserved population so cross-roster duplicates return ProbeRowDuplicate instead of first-pick; witnesses assert canonical uniqueness and duplicate refusal. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: ladder-probe-corpus slice 1: migrate landed wall controls onto gunbc.gua * Bridge node content_hash to Fnv1a64Structural for subject revision v2.std.node.content_hash returns Hash (Primitive in v1 compile); route the node digest through structural_content_hash before tagging so compile-clean passes (guarantee_probe_corpus.dag:253 type mismatch). Co-authored-by: Cursor <cursoragent@cursor.com> * Remove speculative #7555 registry rows; widen v1 harness closure Delete reserved translate path/class/probe identities from slice 1 so #7555 lands its own authority with executing evidence (review 47312). Expand v1_compile_harness_source_paths to fingerprint the v1 compile pipeline stages compile_dag_diagnostic_census exercises, not schema only. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: ladder-probe-corpus slice 1: migrate landed wall controls onto gunbc.gua --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
2 tasks done
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 2, 2026
…l-shape wall. The direct-call shape wall (#7519) now refuses unknown labels and surplus positionals at compile time on every module including v2.*; the local-only interpreter witnesses were still asserting CallContractMismatch at runtime and panicking on the compile diagnostics instead. Split bad/good fixtures, assert blocking CallArgumentNameUnknown/CallPositionalSurplus diagnostics, and include #7648 pool fixes (std.occurrence_identity import, where-refinement advisory filter). Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 2, 2026
…l-shape wall (#7668) * Re-ground application-site contract witnesses to the compile-time call-shape wall. The direct-call shape wall (#7519) now refuses unknown labels and surplus positionals at compile time on every module including v2.*; the local-only interpreter witnesses were still asserting CallContractMismatch at runtime and panicking on the compile diagnostics instead. Split bad/good fixtures, assert blocking CallArgumentNameUnknown/CallPositionalSurplus diagnostics, and include #7648 pool fixes (std.occurrence_identity import, where-refinement advisory filter). Co-authored-by: Cursor <cursoragent@cursor.com> * Add HAND-RUST gate deferral receipt for call-contract witness helpers. Per review 47389: the compile-contract helpers are seed-retained local-only witnesses with an explicit ROADMAP dissolution trigger (ct_call_shape_wall_witness_test → guarantee_probe_corpus migration). Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 5, 2026
Enumerates which ExprCall/ExprMethodCall routes hit body_locals wall, #7519 sig wall, or remain uncovered (field-held fn via method syntax), with honest class rung at mitigatable minimum. Co-authored-by: Cursor <cursoragent@cursor.com>
2 tasks done
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 5, 2026
* WIP: Higher-order named application: refuse named args on function-value call * Refuse named arguments on function-value calls at compile time. Direct declaration calls keep named-argument binding; higher-order function-value applications require positional arguments only. Adds CallNamedArgOnFunctionValue blocking diagnostic, arity surplus check on the function-value path, and an executing witness covering all five operator controls including semantic RED for swapped positional args. Co-authored-by: Cursor <cursoragent@cursor.com> * Document callee-path coverage for function-value named-arg wall. Enumerates which ExprCall/ExprMethodCall routes hit body_locals wall, #7519 sig wall, or remain uncovered (field-held fn via method syntax), with honest class rung at mitigatable minimum. Co-authored-by: Cursor <cursoragent@cursor.com> * Land function-value witnesses in compiler_tests_rust.dag and add hole probe. Registers ct_function_value_named_application_controls_witness_test and ct_function_value_field_method_known_hole_probe_test in the authority (compiler_tests_rust.dag, language_source_scaffold_index) and regen chain. The hole probe executes path (5): field-held fn via ExprMethodCall with named actuals compiles clean today (tripwire for method-call label wall). Carrier note states mitigatable-minimum rung with path (5) as reason. Relabels keyed_row/keyed_roster/tokenize HO call sites to positional args so regen_stage0 self-compile stays green. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Higher-order named application: refuse named args on function-value call * Fix function-value transform call for main_wet regen. apply_emit_spelling_transform passes its transform parameter positionally; named actual on the body-local callee blocked heal_generated_artifacts during main_wet artifact generation. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Higher-order named application: refuse named args on function-value call * Fix hole-probe comment: coverage path (5), not (1). Aligns ct_function_value_field_method_known_hole_probe comment with function_value_named_application_wall_note path enumeration (review 48563). Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Higher-order named application: refuse named args on function-value call * Sync compiler_tests.rs hole-probe comment after regen (path 5). Completes emitted chain for review 48563; merge main + main_wet verified falsifier workflow drift already resolved on merged main. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Higher-order named application: refuse named args on function-value call --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
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.
Guarantee-lane climb (
floor-call-shape-wall, first slice — operator-directed 2026-07-31). The measured divergence was three-way:sub(a: 10, bb: 3)againstfn sub(a: Int, b: Int)compiled with zero diagnostics, the interpreter refused it at runtime (CallContractMismatchincall_function_inner), and the Rust emitter silently reordered it positionally — two realizations of one program disagreeing silently. The compile silence was the absorbing fallback indirect_call_arg_mismatch_diags: a param with no name-matched actual falls back to positional binding, so the label itself was never a checked fact.The wall
direct_call_shape_diags(v1.compiler.infer), hooked beside the existing type walk in thesig != nonebranch, mirrors exactly the two classes the runtime authority refuses — so the authorities agree instead of one refusing while the other absorbs:CallArgumentNameUnknown(blocking): a labeled actual naming no declared parameter — with the interpreter's deliberately-unused-parameter idiom mirrored (ctx:accepted against_ctxand_).CallPositionalSurplus(blocking): unlabeled actuals beyond the positional parameter list, using the same positional-capacity predicatecall_function_innercaches.Deliberately not under
module_skips_direct_call_arg_check: that exemption exists for type-representation gaps (brands, optionality forms, anonymous literals); a label has no representation — it is exact string membership against the declared list — so the wall runs over every module including the compiler's own sources.Deliberately not walled, each named with its trigger in
direct_call_shape_wall_note: duplicate labels and missing arguments (the interpreter itself does not refuse them today — an interpreter-first parity pair is the next slice), the method-pipe seam (the method wall's territory), and thesig == nonefallthrough (measured — below).Receipts, all by execution
compiled: 1 files emitted, 0 diagnostics; post-wall binary refuses both probes located —call shape mismatch calling 'sub': no parameter named 'bb' (declared: [a, b])/too many positional arguments: 3 supplied, 2 positional parameter(s) declared.to_string(i:)vs the renamedvalue(src/v1/compile.dag),arm_body(arm:)vsn,is_import_slot_node(p:)vsn, 17×fold_list(init:)vs this corpus's declaredempty(stage0_rust_source_lifecycle_scaffold.dag),floor_discovery_walk_failure_refusal_reason(path:)vspath_opt. All relabeled to the declared authority in this PR. Thefold_listrows are the sharpest: they never failed live because the interpreter groundsfold_listnatively (label-blind) while the user-fn path would refuse the same label — the program's meaning depended on which dispatch tier served the call.to_string(i:)sites indag_collect.dagnever reach the wall (callee resolves no sig at this seam); found by grep on the fossil's shape, fixed here; the class stays open with its trigger (resolution coverage).call_shape_wall_witness(authored incompiler_tests_rust.dag, generated intocompiler_tests.rs) — both REDs with blocking-classification asserts, and zero-diagnostic positive controls including the underscore idiom. Green:test compiler_tests::compiler_tests::call_shape_wall_witness ... ok.regen_stage0 --verify→regen_divergence_count=0; whole-corpus compile-clean (dag+src/v2, 1,635 resolved sources) → 0 blocking; the[src/v1, dag]regen closure dry (it reds loudly with the fossils present — that refusal-then-fix loop is recorded in the wall note).Ladder placement (honest grain)
The class "call argument labels a parameter that does not exist" moves from mitigatable (runtime refusal on one path, silent wrong output on the other) to structurally guaranteed at the direct-call seam — no
Acceptedprogram contains one. The emission path's silent reorder is retired forAcceptedprograms without touchingorder_typed_call_args(its positional arm remains the legitimate binding rule for unlabeled args; the state it could absorb is no longer writable). Census rows amended incompiler-guarantee-recovery-gap-analysis.md; roadmap nodefloor-call-shape-wallupdated with the landed slice; ROADMAP regenerated from its authority. Also: two total-match arms added in hand-seedcli_run.rs's diagnostic histogram (its own header mandates totality, no silent widening).🤖 Generated with Claude Code