Checker refuses a non-Bool match guard (PositionMatchGuard); Int guards counted as expected red - #12829
Closed
gunbai-bot[bot] wants to merge 5 commits into
Closed
Checker refuses a non-Bool match guard (PositionMatchGuard); Int guards counted as expected red#12829gunbai-bot[bot] wants to merge 5 commits into
gunbai-bot[bot] wants to merge 5 commits into
Conversation
…12779) #12420 gave the caret a lowered form, so `a + ^s` stopped refusing and reify_operand_refusal's two refusal claims went false on main. The specimen is now `a + g(p: { })` (statement_spine_headless). Discrimination re-measured: main minus #12725's fold change reds both claims; main greens all four. Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
* Meaning splits from storage, and the new module imports the nature it uses The contract/persistence split lands first because the engine imports std.judgment_contract for DemandIdentity and demand_identity_canonical, so the lower authority has to exist before the engine group can qualify on its own. judgment_contract declares JudgmentContract.demand_nature: DemandNature and did not import it. std.materialization_ladder is that type's single authority and does not import this module, so the edge is acyclic and the repair is to consume it rather than restate it. The defect survived the originating lane because that lane never compiled this module as its own entry closure; compiled as one at the integration base it is a hard diagnostic. All five encoding and decoding bodies -- length_prefixed_encode, length_prefixed_decode, demand_identity_canonical, demand_identity_decode, string_from_code_points -- are byte-identical to the versions they moved from, so the canonical identity format is preserved by construction rather than by inspection. Nat crossings, checked at the boundary rather than by spelling: count and length are builtin methods typed through v1.compiler.infer_method's registry from the algebra templates, every one of which declares return_type std.nat.Nat, so the v2.std.algebra.length wrapper returning Int is not on this path. Eight sites cross into to_string, into a comparison against a parse_int result, and into take and skip which declare Int. The front end accepts all eight at the integration base, so no widening is authored: a cast nobody needs would lose the nonnegativity the contract carries. Compiled at base 4039815 -- judgment_contract exit=0, 0 blocking errors; materialization_provider exit=0, 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The generic engine lands on the contract it imports, without its native claim demand_engine imports std.judgment_contract for DemandIdentity and demand_identity_canonical, so it follows the contract split rather than leading it. Carried with its direct claims only. native_demand_schedule_test is held back deliberately. Compiled as its own entry closure at the integration base it refuses on twelve names it expects from v2.compiler.compile -- NativeDemandPlan, NativeDemandValue, the four native_demand_* identity and plan functions, the three NativeCost arms, native_demand_cost_class and the two observation functions. Those names arrive with the production consumer, so the claim belongs to that group; landing it here would have put a red in the tree with no authority able to green it. The Nat question is answered differently here than in the contract group and the difference is the evidence. All five sites call length as a FREE function -- length(xs: e.entries) -- which resolves to v2.std.algebra length returning Int, not the builtin method whose algebra template declares std.nat.Nat. So the refinement does not reach this module's arithmetic, established from the call form and the declarer rather than from the name. Compiled at base 4039815: demand_engine exit=0, demand_engine_test exit=0, 0 blocking errors each. Direct claims executed, 15 requested and 15 reported, exit=0, no absent results. The negative paths are inside that population rather than beside it: a refused prerequisite blocks its dependent, a fresh effect is never attached, a cycle is reported as a cycle, a missing edge is reported, and no seat leaves a demand ready. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The clock gets an emitted body, and its signature stops admitting what it denied Three authorities, one capability. v1.compiler.infer_method declares the observed_monotonic_nanos signature, extdeps.languages.rust.emit bridges it into the emitted registry, and v1.compiler.runtime_rust carries the body as its own rt_realization_measurement fragment rather than lines inside an unrelated block. The signature repair is a seed defect independent of the demand program. The row read `params: []` while every call site passed a label and the interpreter accepted it, so the interpreter admitted an argument its own signature denied and no emitted body could have been written against the declaration. The label is never identity material and is never hashed; it exists so pure-call memoization cannot collapse two readings around one subject into one, which would report every measured span as zero. trace_mark beside it already declared its label, so this row now matches the shape its neighbour had. Why the body had to exist: a modeled operation, an interpreter implementation and an emitted-runtime realization are three capabilities, and the builtin was registered for the interpreter only. A fold reading the clock therefore typechecked, ran under `gunbc run`, and panicked in the emitted binary -- which is where the native route actually executes. std.primitive_identity rosters five derived surfaces and a runtime body surface is not among them, which is how a registry row with no body passed every rostered check. Excluded from this group deliberately: the 05_emit_rust.dag hunk in the originating commit is entirely the emitted_closure_crate_name and seed_host_crate_name consolidation, with nothing clock-related in it. That naming work is handled through #12358 and is not replayed here. Compiled at base 4039815, each as its own entry closure: 04_method exit=0, runtime_rust exit=0, rust/emit exit=0, 0 blocking errors each. The emitted realization is NOT yet qualified by this commit. The built binary renders runtime text from the stage0 mirror, not from this .dag, so the specimen that proves the emitted clock executes requires the regenerated mirror and a rebuilt binary. That is the next step, and it is a precondition of the production consumer rather than of this carry. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Install the regenerated mirrors for the three clock authorities Regenerated rather than carried: the originating lane's mirror commit is a generated projection, and installing its bytes would have shipped a mirror produced by a different authority set than the one integrated here. The affected output population is DERIVED and it is three, not the four the assessment listed as candidates. required-regen planned 161, executed 161 and adjudicated 161, and reported drift in exactly extdeps_languages_rust_emit.rs, v1_compiler_infer_method.rs and v1_compiler_runtime_rust.rs -- one per carried authority. v1_compiler_emit_rust.rs is absent from that set because the 05_emit_rust.dag naming hunk was excluded, which is the difference between a candidate list and a roster. Each mirror carries its authority's change and nothing else: the emitted runtime registry gains the observed_monotonic_nanos bridge row, the builtin signature's empty params becomes the declared label, and the runtime source gains rt_realization_measurement. declared_divergent=1 [main.rs] is pre-existing and is not from this change. This makes the emitted realization exist in a binary for the first time; that binary's specimen is the next step and no claim about the emitted clock is made by this commit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The fallback stops discarding the missing-row cause, and the fatal stays put Carried from the originating lane because #12355 was CLOSED WITHOUT MERGE, so this is neither a dependency already in the tree nor a delivered fix to preserve. It is independent of demand scheduling and lands as its own change rather than inside the production-consumer group. A missing grammar row is not a shape error and this arm reported it as one. The row match produces a precise translate_grammar_relation_row_not_found when the target's grammar renders no row for a relation; the fallback discarded it and then refused from translate_type_expression_project, so a target missing a row for a MODULE MEMBER surfaced as translate_arrow_body_not_a_type_expression -- a cause about the node's shape rather than the target's coverage. DESIGN section 5 requires a failure arm to refuse with a located typed cause, not substitute a different one, and the substitution mis-located real work. THE FATAL IS DELIBERATELY UNCHANGED. translate_arrow_body_not_a_type_expression is the discriminating red of a rostered class at rung 1, closure_emit_renders_an_arrow_without_its_body, asserted BY NAME in v2.test.emit.closure_emit_arrow_body_refusal and pinned by //gunbc/instruments:v2-native-cli. Promoting the row cause to fatal would have retired that evidence while looking like a diagnostic improvement. The row cause is therefore appended FIRST and the shape cause LAST, because diagnostics_fatal selects the last diagnostic -- so the fatal is byte-for-byte the cause it was, and the only change is that the row cause is carried as context instead of dropped. Merged rather than applied: main moved this file +167/-20 since the originating merge base and the conflict was positional. Main's side added translate_module_not_a_type_expression_diagnostic and translate_first_module_body_optional, which translate_type_expression_tree now CALLS, so both sides are load-bearing and both are kept. Nothing of main's was dropped to make room for the carried comment. Compiled at base 4039815 as its own entry closure: exit=0, 0 blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The route switches: the engine schedules and the rendered main stops doing it The production cut. 00_compile.dag carries the demand consumer and its observation folds, 05_emit_rust.dag switches the rendered main onto native_demand_schedule_universe, and native_demand_schedule_test joins its authority at last. WHERE THE CUT ACTUALLY IS, because the file sizes read the other way round. 00_compile.dag is +1047/-0 and nothing was deleted from it, which looks exactly like a handler landing beside the implementation it was supposed to displace. It is not: the route lives in the emitter's rendered-main TEXT, where native_demand_schedule_universe is called from two string literals, and 05_emit_rust.dag is +86/-97 -- a net deletion, the displaced scheduler and its observation leaving the rendered main. A reader checking only the consumer module would conclude the opposite, so the arithmetic is stated here. Carried from three emitter commits and NOT a fourth. The naming consolidation in 1de2805 is excluded, so `let crate_name = if has_pipeline { "v1_compiler" } else { "v1_compiled" }` stands byte-for-byte as main has it and nothing of #12358's subject is replayed. Main's own changes to 00_compile are preserved rather than overwritten: the gunbc.native_frontier_ratchet import, and main's move of list_append and list_snoc_item from v2.std.algebra to std.algebra. Compiled at base 4039815, each as its own entry closure: 00_compile exit=0, native_demand_schedule_test exit=0, 05_emit_rust exit=0, 0 blocking errors each. Claims executed, 14 requested and 14 reported, exit=0, no absent results. The negative paths are inside that population: a reversed elapsed reading is invalid rather than zero, an invalid or unclassified reading makes the observation INCOMPLETE rather than silently totalling, a blocked demand contributes no transition, a kind outside the contracts is counted rather than dropped, and rendering the receipt moves no total. What this commit does NOT establish: the emitted route. 05_emit_rust.dag changed, so v1_compiler_emit_rust.rs is now stale and the binary still renders the old main. Regenerating that mirror and requalifying against the production consumer is the next step. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Install the regenerated emitter mirror so the binary renders the switched main One mirror, derived rather than listed. required-regen planned 161, executed 161 and adjudicated 161, and reported drift in exactly v1_compiler_emit_rust.rs -- the single authority the production cut changed. The three mirrors installed for the clock group came back clean, which is the evidence that they installed correctly rather than merely that nothing complained. The mirror now renders native_demand_schedule_universe, so a binary built from this tree emits a main that schedules through the engine. Before this commit the switched route existed only in .dag and every built binary still rendered the displaced scheduler. declared_divergent=1 [main.rs] is pre-existing and not from this change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * A dead clock passed every check, so progress becomes its own refused fact THE HOLE, stated as measured rather than as a worry. elapsed_observation admits finish == start as ElapsedObserved { nanos: 0 }, so a realization whose body returns a constant zero leaves every transition CLASSIFIED and VALIDLY OBSERVED: unclassified is 0, invalid_elapsed is 0, classified equals the transition count, and native_demand_observation_complete answers TRUE over totals that are entirely zero. The emitted-body membership phase cannot see it either -- that check establishes a bridge HAS a body, never that the body measures anything. Two different predicates, one shared blind spot. Three of the four distinctions already held and are unchanged: a reversed reading is ElapsedObservationInvalid rather than zero, invalid_elapsed is counted SEPARATELY from unclassified, and both already break completeness. The missing one was progress. native_demand_observation_progressed asks progress AT THE RUN, not per transition. One fast transition may honestly observe a zero span on a coarse clock, so a per-transition rule would refuse real work; a run that executed transitions and accumulated no span at all is a clock that is not running. An empty run is vacuously progressed, so the predicate reports no defect where there was no work. DELIBERATELY NOT FOLDED INTO completeness. Completeness answers whether every admitted transition reached a cost class; progress answers whether the realization underneath produced a measurement. Fusing them would make one counter answer two questions and would silently change what every existing consumer of `complete` asserts. The rendered main CONSUMES it fail-closed: a run whose clock never advanced refuses with a located cause naming the transition count, rather than reporting its zeros as an observation. Reporting them would be a fabricated measurement presented as a reading, which DESIGN section 5 forbids outright. So the predicate has a production consumer and is not a declaration only witnesses read. THE READINGS IN THE CLAIMS ARE SUPPLIED, NOT CLOCKED. The subject is the observation fold, so reading the real clock would assert something about the host's timer instead -- and could not author the constant-zero case at all, since a working clock refuses to produce it. Supplying them is also what bounds the control: there is no timer to wait on, so a broken clock cannot hang its own test. Compiled at base 4039815: 00_compile exit=0, native_demand_schedule_test exit=0, 05_emit_rust exit=0, 0 blocking errors each. Claims executed, 18 requested and 18 reported, exit=0, no absent results. The four added controls discriminate in both directions: the dead-clock case would fail if progress were always true (it asserts complete AND not progressed over the same run), and the positive control would fail if progress were always false. NOT established by this commit: the refusal in a binary. 05_emit_rust.dag changed, so v1_compiler_emit_rust.rs is stale again and every built binary still renders a main without the refusal. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Install the regenerated mirror so the dead-clock refusal exists in a binary One mirror again, derived not listed: required-regen planned 161, executed 161, adjudicated 161, drift in exactly v1_compiler_emit_rust.rs -- the single authority the progress control changed. The four previously installed mirrors came back clean. The mirror now carries native_demand_observation_progressed, so a binary built from this tree renders a main that refuses a run whose clock never advanced. Before this commit the refusal existed only in .dag and every built binary would have reported the zeros. declared_divergent=1 [main.rs] is pre-existing and not from this change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * judgment_contract imports the skip it uses, which the required floor refused REQUIRED-FLOOR REFUSAL cause=UnimportedBareProvider on dag/std/judgment_contract.dag#skip, provider src/v2/std/algebra.dag: the file declares imports, so its bare channel is off and `skip` is never pulled for it. Same class as the DemandNature repair in 3e0a494 and it hid for the same reason: my entry-closure compile passed, because `skip` RESOLVES. The unimported-bare-provider gate is a separate wall from resolution, and only the required floor runs it -- so compiling the module as its own closure could not have caught this, and did not. Only `skip` is flagged of the six bare names the carried decoder uses, and the distinction is checked rather than assumed: skip is declared as fn skip<T> in v2.std.algebra with no builtin registry row, so it is a genuine provider reference. take and fold resolve as algebra METHOD TEMPLATES, count and length through the builtin registry, and join is a free primitive. Importing those would be the concat mistake from earlier in this lane, where naming a free primitive in an import broke resolve across every consumer. The import names the same function that already resolved: fn skip<T>(xs: FreeMonoid<T>, n: Int) against `cs |> skip(n: hash_at + 1)`, where the pipe supplies xs and n is an Int. Verified: judgment_contract compiles exit=0 with 0 blocking errors, and the 48 contract claims re-run 48 requested / 48 reported / 48 PASS, exit=0 -- so the import is a hygiene repair and not a behaviour change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address both review findings: the scheduler's cost is a row, and a failed module counts once P1 -- THE SCHEDULER'S OWN WORK WAS UNATTRIBUTED, AND THAT IS A CORRECTNESS DEFECT. `schedule_plan_started` opened, covered only native_demand_tested_tree_input, and CLOSED BEFORE native_demand_schedule_universe ran -- so plan construction, ready-queue selection, binding lookup, settlement, readiness recomputation and row collection all fell into the parent residual. The partition's tolerance arm is a fixed 50ms, so a large enough selected universe makes an otherwise VALID adjudication exit NativeDriverCostRemainderExceedsTolerance: a fail-closed refusal fired by correct input, which is the wrong direction of wrong. The repair uses the mechanism already built for it. std.compiler_entry gains ExclusiveDemandScheduling, and because the driver's match over that key is exhaustive WITH NO WILDCARD, adding the row FORCED the driver to say what measures it -- which is the reason that match was written without a wildcard. demand_scheduling_nanos = span(whole scheduling call) - (engine's prepare nanos + engine's eval nanos) TWO THINGS DELIBERATE HERE. Adding the span to ExclusivePrepare was the one-line edit and it would DOUBLE-COUNT: the engine already reports its own prepare nanos and the driver already adds them, so that would trip the OVER-attribution arm instead of the tolerance one. And the subtraction SATURATES -- these are unsigned, the engine's attributed sum can exceed the enclosing wall span when the two clocks disagree at the margin, and a plain subtraction would wrap to an enormous positive and report it as scheduler cost. P2 -- A MODULE THAT FAILED AT RESOLVE WAS COUNTED TWICE. Its resolve transition carries the decided rows as its VALUE and is a real preparation refusal; the dependent infer demand is then admitted and settles DemandRefused WITHOUT a value -- it never executed, so there is nothing it refused -- and the blanket arm counted it again. prepare_refused reported 2 for one failing module where the module-level count before the engine was 1. NativePreparationStanding gains PreparationUnrun for that case, with its own prepare_unrun total exported and serialized beside prepare_refused. It gets a counter rather than folding into NotApplicable because "admitted and never executed" is worth reading: a population where it is large is one mostly blocked behind earlier failures, and nothing else in the receipt would show that. THE LIMIT, STATED RATHER THAN IMPLIED. This reads the settled state and not a cause, so a demand that genuinely refused on its OWN execution without producing rows also lands in Unrun. The engine already distinguishes DemandRefused from DemandBlocked { cause } (v2.std.demand_engine), and settling such a dependent as Blocked is the sharper repair -- that belongs to the engine's settlement, not to this rollup, and until it lands the number is visible here rather than hidden inside the refusal count. THE ROW KEY'S OWN CONSEQUENCE, HANDLED. std.compiler_entry's header records that its roster is a hand-authored list whose hole is caught by a witness, and that the witness only catches it while every key carries a DISTINCT NON-ZERO fixture value. Adding a variant therefore broke nine matches in test.claim.native_driver_cost_partition_witness (correctly -- they are over the key TYPE), and the new row gets a distinct non-zero in the sum fixture with the asserted sum and the reconciling parent both moved by the same delta, so the residual under test is unchanged. It also gets the discriminating probe that file keeps per added row: every other row well inside the parent, the total pushed past it through this one, so the probe fails exactly when this row is dropped from the fold. Green: 14/14 in the partition witness, including the new probe. gunbc rebuilt clean; 00_compile and 05_emit_rust compile with no blocking errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Index the engine's adjacency, and measure the locality claim instead of asserting it THE COST SHAPE IS NO LONGER AN UNVERIFIED NOTE. It is two numbers from a control, and they say half the law holds and half does not. WHAT THE LAW CLAIMS: "a completion re-evaluates its DIRECT dependents" -- settling a demand with one dependent among N unrelated ones costs one derivation, not N. The module's own header admitted the check could not see the other half, in its own words: the counter "counts DERIVATIONS, not entries visited", and "locating the dependents is a scan of the relation list". So a whole-population scan and a targeted update reached identical states AND identical counts, and the existing claim passed either way. WHAT IS FIXED: relations are now indexed by direction. demand_engine_relate -- the single site a relation enters -- maintains dependents_of and prerequisites_of, and the two readers consult the index instead of filtering the whole relation population. After this, no reader walks the relation list at all; `.relations` survives only as the authority it always was, plus a length in one fuel bound. These are NOT a second authority. Nothing writes the index that does not write the list in the same call, no reader asks the index a question the list would answer differently, and there is no second writer to drift from. What it removes is a scan, not a fact. WHAT IS NOT FIXED, MEASURED AND ENROLLED: settle still walks the entire entry population TWICE -- once to update the settled entry, once to recompute its dependents' readiness. The new control settles a one-dependent demand in a 5-demand graph and in a 45-demand graph and reports: derivations identical the relation scan is gone entries_walked 10 vs 90 the population walk is not The claim asserts what the engine does TODAY, so it is green by execution and inverts the moment the store becomes keyed. Writing it as the desired property would have landed a red and specified the same thing. WHAT REMAINS IS MECHANICAL AND NAMED. With a persistent LIST, updating one entry is inherently a walk, so locality requires entries keyed by identity plus a separate order list for the whole-population passes the law does NOT claim are local -- seal, reevaluate and the ready-queue build. Nine internal sites and one external length(). AND THE CONSEQUENCE FOR LANDING, STATED PLAINLY: until that control inverts, the production cut is not landable. Its central claim is that a completion costs its out-degree and not the graph, and at the entries grain the implementation does not hold that. The fallback of splitting the cut and landing only the engine/contract/clock foundations is now a live option, since the defect is quantified rather than suspected. I stopped short of the store swap deliberately. It is nine sites in a load-bearing module at the end of a long session, and rushing exactly this kind of edit is what silently deleted a Node-typed argument earlier today. The measurement is committed so the next pass starts from a number. Green: 16/16 demand engine claims including the new control; 22/22 native demand schedule; 14/14 cost partition. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Keyed entry store: a completion now costs its out-degree, measured THE LOCALITY CLAIM HOLDS AT THE ENTRIES GRAIN. The control that was enrolled as the defect now asserts the property and passes: settling a demand with ONE dependent costs the same in a 5-demand graph and in a 45-demand graph, on both counters. before derivations 1 vs 1 entries_walked 10 vs 90 after derivations 1 vs 1 entries_walked 2 vs 2 WHAT CHANGED. `entries` is keyed by identity and `entry_order` carries the insertion order separately, so settlement is a lookup and an insert instead of a rewrite of the population. demand_engine_settle now touches the settled entry and, through the keyed reverse-adjacency index, exactly its direct dependents -- which is the entire content of the law it claims. THE WHOLE-POPULATION PASSES THAT REMAIN ARE THE ONES THE LAW DOES NOT CLAIM ARE LOCAL: seal validates every demand once, reevaluate recomputes every readiness. Both now route through one named helper, demand_engine_entries_mapped, so a THIRD such pass cannot appear inside a function that is supposed to be local without a reader seeing the name. A GENERIC EROSION THIS HIT, AND IT IS THE SAME ONE AS THE FIELD-PROJECTION LANE'S. map_lookup answers Optional<V> over the map's own value generic, and a value destructured straight out of it does not carry DemandEntry<V> through a FIELD READ -- eight errors, all "no field 'identity' on type 'V'". Naming a typed parameter restores it, so every entry rewrite goes through demand_entry_with_state, demand_entry_produced or demand_entry_attached rather than reading fields off a lookup result inline. STILL OUTSTANDING IN THIS FILE, and it is the other half of the cost gate: demand_engine_next rebuilds the ready queue by filtering AND sorting the whole population on every admission, and demand_engine_in_flight filters it again. Keyed entries do not touch that. The next pass maintains the ready set incrementally in canonical order so admitting an already-ready demand is a head read, with its own counter -- because counting only readiness derivations is what hid the entry scans in the first place. Green: 16/16 demand engine claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The keyed store's invariants, and the locality claim held at the grain it proves THREE INVARIANTS MADE EXECUTABLE, because splitting a store from its order buys locality and owes agreement. Two representations of one population can disagree, and a keyed store with a stale order list would answer settlement correctly while every whole-population pass -- seal, reevaluate, receipts -- silently skipped or double-counted a demand. the order resolves entirely in the keyed store no pass reads a dropped key the order names each demand once seal cannot derive one demand twice settlement leaves the order unchanged a completion changes STATE, not membership The third is the value-level shadow of settlement being local: the population a demand belongs to is not a function of what settled. THE FIFTH INVARIANT IS ABSENT AND ITS ABSENCE IS DECLARED. "No operational function traverses entry_order" is a property of the SOURCE, not of any value a claim can read -- the traversals live in demand_engine_entries_mapped and demand_engine_all_entries, and nothing in .dag can see that a third has not appeared elsewhere. Calling the shadow structural would be rung inflation (DESIGN section 4b(1)), so it is recorded as diligence at the same grain as std.compiler_entry's hand-authored row roster, with the same next-rung trigger: a lens over this module's own call graph. AND A PRECISION CORRECTION TO MY OWN CLAIM, which I had overstated. What the counter establishes is that settlement visits the settled entry and its direct dependents and NOTHING ELSE -- the semantic full-population scan is gone. It does NOT establish constant-time operations: a keyed persistent map may carry population-dependent internal cost such as tree depth, and an ordered ready set may carry logarithmic insertion. "Costs its out-degree, not the graph" is sound as a statement about GRAPH WORK; "O(out-degree) wall time" claims more than this evidence supports, and the carrier's header now says so rather than leaving the stronger reading available. Green: 19/19 demand engine claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The ready order and in-flight count are maintained, not rederived per admission THE OTHER HALF OF THE COST GATE. demand_engine_next answered one question -- which identity is canonically first -- by filtering every entry and SORTING the survivors, on every admission, and demand_engine_in_flight filtered the population again beside it. Neither cost a readiness derivation, so both were invisible to the only counter the engine had: exactly the way the entry scans hid. demand_engine_ready_queue returns the maintained order demand_engine_in_flight returns the maintained count demand_engine_next reads the head MAINTENANCE IS LOCAL, AT THE ONE SITE STATE CHANGES. Settlement syncs the settled identity's membership from its new state and then its DIRECT dependents' -- the fold is over the out-degree, so the unrelated population is not consulted here either. The order is keyed on the demand identity and never on arrival, because two runs of one closure must admit in one order and an order depending on which prerequisite settled last would make the completion receipt unreproducible. Seal and reevaluate rebuild both facts from the states they just decided, through one named republish function so a local function cannot reach for a full rebuild by accident. A FINDING ABOUT THE SCAN THAT WAS THERE: demand_engine_in_flight filtered every entry for DemandRunning, and NOTHING IN THIS CORPUS SETS THAT STATE. No producer transitions a demand to running, so that walk computed a constant zero on every admission. It is still derived from state rather than hardcoded -- returning 0 with a comment would be correct today and a fail-open the moment a producer appears, admitting past the seat count because the count was a literal -- so the delta is taken where state changes and tracks a producer that does not exist yet. A COUNTER I WROTE AND DELETED. I first added ready_inspected to make the admission claim observable, then found demand_engine_next returns an admission and not an engine, so no caller could ever read it: a field nothing writes, which is the dangling declaration DESIGN section 3c forbids. The admission cost claim is structural instead -- one inspection of a maintained head, by construction -- and what the counter was a proxy for is asserted directly and is the sharper property: THE MAINTAINED ORDER EQUALS WHAT A FULL REBUILD WOULD PRODUCE, across a seal and three settlements including a refusal, in a 45-demand graph. Drift there would admit a stale identity or skip a ready one while every count looked fine. FIVE STRUCTURAL REDS BESIDE IT: in-flight standing is population-independent and zero; the canonical head survives an unrelated completion; a settled demand leaves the order; a refused prerequisite never admits its dependent; a duplicated dependency cannot duplicate a ready identity. Green: 25/25 demand engine claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * DemandRunning is a declared frontier, and the in-flight delta gets a control that can fail THE REVIEW IS RIGHT AND THE CATCH IS SHARP: DemandRunning is a variant NOTHING IN THIS CORPUS PRODUCES, which is the same unconsumed declaration (DESIGN section 3c) as the inspection counter deleted from this module one commit ago. It got a quiet pass because it sits inside a coproduct rather than standing alone as a field. AND MY CONTROL WAS WORSE THAN USELESS THERE. "The in-flight count is population-independent and zero" cannot fail if the running path breaks, because no producer reaches that path -- so it looked like a guard over the in-flight delta while guarding nothing. A check that cannot go red is a decoration (DESIGN section 4b), and this one was positioned to be cited as coverage. THE FRONTIER IS NOW DECLARED WITH ITS PRODUCER AND TRIGGER, not merely noted. The seat vocabulary is real and consumed -- demand_lease_admits asks the caller's offer whether an admitted demand obtains a lease -- but admission does not RECORD that a demand went in flight, because demand_engine_next answers a DemandAdmission and not an engine, so nothing it wrote could reach a caller. The producer is therefore the admission path returning the engine it changed, which is the SAME structural gap that made the inspection counter unreadable: one missing return, two dangling declarations. Trigger: multi-seat realization -- with one seat the driver executes immediately after admission and no demand is ever observably in flight. AND THE DELTA NOW HAS A ROW THAT DISCRIMINATES. DemandRunning cannot be reached by RUNNING the engine, but it can be SUPPLIED -- demand_engine_settle takes any state, which is the boundary this claim sits at (DESIGN section 3's witness rule). Entering running raises the count, entering it twice does not double-count, and leaving it for a settled state lowers it again. PROVEN DISCRIMINATING BY MUTATION, because a passing claim establishes nothing until it can fail: with demand_in_flight_delta stubbed to return 0, the population row still PASSES and only the new row goes RED. That is the exact split the review predicted. A third row beside it: a running demand is not in the ready order, so a seat held is not also a seat offered. Green: 27/27 demand engine claims. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Gate item 4: engine, schedule and partition controls green at this head demand engine 27/27 native schedule 22/22 cost partition 14/14 TWO MERGE CONSEQUENCES FIXED, neither caused by this lane's changes and both found only by running the sets at THIS head rather than trusting the earlier greens. Main tightened the unimported-bare-provider rule, so dag/test/claim/native_driver_cost_partition_- witness now needs `import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly }` -- it declares imports, so its bare channel is off and the pair no longer resolves through the census. The file had passed 14/14 before the merge on exactly the same content. And fixing the import made its DEBT ROW stale, which the rule then refused in the other direction: the roster carried (file, SubstrateInputsOnly) as ActiveDebt, and a pair the file no longer needs must be retired rather than left owed. Its standing moves ActiveDebt -> Retired { cause: ImportsFixed }, which is the one transition that roster admits, and the cause is true: the imports were fixed in this change. Worth recording that the rule caught BOTH directions. A missing import refused at the file, and a discharged debt left in place refused as RosterStale -- so neither the fix nor its bookkeeping could be half-done silently. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Drop the translate fallback, reach the mirror fixed point, census the moved authorities THE TRANSLATE FALLBACK IS REMOVED, and the deciding fact is one I did not have when I argued to keep it: this exact repair already had its own PR, #12355. It was HELD because none of its tests observed the preserved diagnostic chain; its author then tried to construct a discriminating red, found the double-failure arm UNREACHABLE on that base, and recommended closing rather than landing unwitnessed defensive code. #12355 closed unmerged. So it was never a 36-line judgment call. The qualitative test is whether the changed arm has a reachable consumer and a mutation-sensitive control, and it demonstrably has neither -- which is the same standard this session has been applying to everything else: a check that cannot go red is a decoration. I argued to retain code I WROTE on a size argument, which is the bias worth recording beside the revert. It is a v2 module, so no seed mirror had to be re-derived and no "translate-removed-but-mirror-stale" head was possible. Restore it only when current main supplies a concrete double-failure specimen whose complete diagnostic chain changes when the repair is removed. THE MIRROR FIXED POINT IS REACHED AND VERIFIED, not assumed. Pass one drifted exactly one mirror -- v1_compiler_emit_rust.rs, from the P1 redo -- which was installed and rebuilt. Pass two reports first_generation_equal=true and exits 0, and both mirrors were hashed before it ran and verified byte-identical after. That is the boundary stated as "the second pass writes zero bytes", checked rather than inferred from an exit code. THE MOVED-AUTHORITY CENSUS, because line counts show the DIRECTION of an extraction and not semantic uniqueness. "materialization_provider shrank and judgment_contract is absent on main" establishes that declarations moved; it does not establish that each now has one home. Measured: 31 authorities declared in judgment_contract each has EXACTLY ONE declaration corpus-wide (dag, src/v1, src/v2) NONE is also declared in materialization_provider the provider CONSUMES them through import std.judgment_contract So the survivorship row reads: moved authorities have one declaration each; the persistence provider consumes them and no longer defines them. And the conclusion is narrowed to what the evidence supports -- no supersession or duplicate authority was found in the retained demand-engine groups; generated mirrors are re-derived; the unrelated translate fallback was removed -- rather than the broader "nothing is duplicated" that asked line totals to prove semantic uniqueness. Green at the fixed-point head: 27/27 demand engine, 22/22 native schedule, 14/14 cost partition. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Cover the new row key in the Rust test targets, which no --bin build compiles THE GENERATED LANE FAILED ON A TEST TARGET I NEVER COMPILED. Adding ExclusiveDemandScheduling to the row key left two non-exhaustive matches in src/v1/tests/src/native_driver_cost_refusal_test.rs: error[E0004]: non-exhaustive patterns: NativeDriverExclusiveRowKey::ExclusiveDemandScheduling not covered I HAVE A NOTE ABOUT EXACTLY THIS AND STILL DID NOT RUN THE COMMAND. `cargo build --bin gunbc` does not compile src/v1/tests, so every local build I ran was blind to it. CLAUDE.md names the command that is not: `cargo clippy --all-targets -- -D warnings` is "the only command that compiles the integration-test and example targets, so a red there is invisible to every other step". The pre-push hook runs cargo fmt, not clippy, so nothing local objected either. WHAT THE EXHAUSTIVE MATCH DID RIGHT. This is the same construction that forced the driver to measure the row: a match over the key TYPE with no wildcard refuses to compile until its author decides what the new row means there. It caught the test targets too -- it just caught them in CI because that is the only place they were built. The row key's own header in std.compiler_entry says a wildcard would answer zero for a span nobody wired up; the same reasoning is why these two fixtures had to say 0 explicitly rather than inherit it. Verified with the CI command this time, not a --bin build: cargo clippy --all-targets -D warnings finishes clean. ALSO CONFIRMED FROM THAT RUN: floor PASSED at 43m9s, so the monotone-roster merge was the right repair, and the regen phases report first_generation_equal=true and fixed_point_equal=true in CI -- the mirror fixed point I verified locally by hashing holds on the runner as well. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Count the population through entry_order, not the keyed store The emitted closure refused to compile where the interpreter had accepted the same source: error[E0308]: length(run.engine.clone().entries.clone()) expected Rc<im::Vector<_>>, found Rc<im::HashMap<Rc<DemandIdentity>, Rc<DemandEntry<..>>>> `entries` is keyed by identity now and `entry_order` is the population's enumeration, so three sites counting the store as a list were wrong: native_demand_run_demand_count in 00_compile, and two assertions in the engine's own claim file. All three typechecked in .dag -- FreeMonoid is loose enough interpreted -- and only the emit route caught them, which is the rostered class accepted_source_emits_uncompilable_target. Worth recording that the interpreted claims could NOT have caught this: 27/27 passed over the same source. emit-build is a non-required detector lane and its own log says a red there is a real finding, most likely the author's. It was. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Install the regenerated mirrors for the merged emitter authorities The merge took main's side for two GENERATED mirrors so the tree would build, and the regen then re-derived both from the merged .dag. This commits that re-derivation: without it the branch carries main's mirrors against this lane's emitter source, which is exactly the drift the generated lane refuses. Caught by reading git status before claiming the push was complete -- the candidates had been installed into the worktree and rebuilt against, but never committed, so the head pushed a moment ago carried main's mirrors. Verified after: regen pass two reports first_generation_equal=true and rewrites no mirror, with every hash checked. Co-Authored-By: Claude Opus 5 (1M context) <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>
…12407) * v2: coercion admits a refinement-to-declared-carrier cast as Widened A cast from a refinement to its DECLARED carrier (x as Int from x: Pos, type Pos = Int where positive) is admitted as Widened: the declaration's carrier edge composed with the existing exact-structural find_witness. No preservation rule is added (ruling: neat-boar-16). - v2.compiler.infer refinement_declaration: reference -> declaration {path, carrier, where_clause} by the reference's own path down the containment spine; one reader for this cast and the literal-into- refinement producer (shape agreed with quick-crab-850 / deep-bee-18). - v2.std.coercion coercion_cast_crossing takes source_declared_carrier and stays tree-free; a non-carrier target refuses with the original operand mismatch. One step only: Pos2 = Pos where .. widens to Pos, not Int. - body lowering lowers a where-refined head as a type (it rode as the raw parse sequence nothing resolved), so the carrier is resolved and an undeclared carrier now refuses unbound. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * infer: RefinementDeclaration drops unconsumed path; where_clause named as a declared frontier (review 71764) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * body_cast_node: 15b/15c supply values at coercion's interface; drop the over-budget assembly rows Floor refused three new witnesses over the 72300 eval-step new-witness budget (no claim failed). The refusal logic lives in v2.std.coercion, so 15b/15c now supply the reference, declared carrier and target there (2652 / 2015 steps); row 15 stays the inhabitance claim on the production route. The undeclared-carrier assembly row is dropped: row 15 is the lowering change's discriminating red (an unlowered head cannot widen). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2 resolve: ResolvedTree carries the SymbolIndex resolution consulted; cut every consumer root-first Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * pick_ingested: the arrow extractor returns the arrow Node (my retype over-reached) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * infer: drop the unused tree parameter from infer_bind_annotation_check (review 71857) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * infer: thread symbol_index through the gather step call the carrier merge brought in Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * infer: drop the unused tree parameter from infer_transform_cast_optional (review 71891) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * infer: thread ResolvedTree whole as 'resolved'; parameter scope search frozen as a declared frontier (neat-boar-16 ruling) Every infer function that took tree: Node (plus the separate symbol_index) now takes resolved: ResolvedTree and reads resolved.root / resolved.symbol_index. infer_parameter_scope_search stays FROZEN (no new callers or arms): a frame-bound parameter reference reaches infer as a bare canonical_atom with no path, so the index cannot key it; the trigger is on the carrier comment. infer_branch_operand_resolved_type no longer passes its operand as a fake tree: it states the literal-else-facts result that call always produced. Row 16 (positive(x: Int) beside f(x: Pos)) is the ruling's required control. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Merge origin/main (#12379 landed); #12379's new hand-built infer inputs use the named no-declarations constructor Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * plain_type_decl_lowering (new from main): its assembly helpers carry ResolvedTree and walk .root Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * Merge origin/main; body_let_annotation (#12540's new rows) carries ResolvedTree Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * v2: lower the where-refined head as a type so resolve binds it; ResolvedTree.resolved_declarations (neat-boar-16 ruling) The head reached resolve as an unlowered dag_surface_qualified_name shell, which resolve preserves unchanged as module metadata, so a declaration's carrier was never resolved. It is now lowered through the one type-expression lowering; resolve binds it; an undeclared carrier refuses unbound. ResolvedTree gains resolved_declarations, the same module fold over the resolved root, alongside symbol_index (the index resolution consulted). The other declaration-body type positions are a declared frontier (gunbc.recurring_failure_mode declaration_body_type_shell_preserved_unresolved). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * resolve: ResolvedTree comment states symbol_index's consumers once (no later stage reads it; #12407 reads resolved_declarations) (review 72652) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> * body_cast_node: the Pos2 one-step row reads the resolved carrier only; infer's admission is row 15's subject (over the new-witness budget) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…); Int guards counted as expected red on the relation v1.compiler.infer judges every match-arm guard as a PositionMatchGuard obligation of declared_type_inhabitance, declared Bool, so a String guard now refuses DeclaredTypeNotInhabited at acceptance. An Int/Float guard is still admitted by the shared relation (declared_realizes_as_kernel_numeric admits a kernel numeric at any KernelMinted declared type); its two rows are enrolled expected red, and that relation repair is routed to the typing lane. Stage0 mirror regenerated to a fixed point. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Superseded by #12841 (clever-lynx-801). #12841 builds the same guard obligation in both ExprMatch arm-inference passes, as — sent from bright-owl-402 |
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 30, 2026
…guard reds from #12829, one shared control; name the two-check fork Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.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.
Follow-up to #12814, requested by manager jolly-boar-500 (option A of the escalation). Stacked on #12814; the base will retarget to
mainonce that PR lands.What changed
v1.compiler.infer): every match-arm guard is now judged as a newPositionMatchGuardobligation of the one inhabitance relation (declared_type_inhabitance), with Bool as the declared type.match_guard_obligation_diagsand is called from both arm-inference passes ofExprMatch.v1_compiler_infer.rswas regenerated viaclaim_executor --required-regen. The second pass reports rc=0, so the mirror is at a fixed point.MatchGuardNotBoolrefusal from Seed interpreter honours match-arm guards (interpreter/emitter divergence) #12814 stays as the runtime catch.Evidence
Remote
claim_batch --wetruns oftest.claim.match_guard_bool_inhabitance_witness_testwith the regenerated seed:a_string_guard_is_refused_at_acceptance(x if (s))DeclaredTypeNotInhabited)DeclaredTypeNotInhabited @ match guard, blocking)a_bool_guard_is_admitted(control)an_int_literal_guard_is_refused_at_acceptance(x if 5)an_int_valued_guard_is_refused_at_acceptance(x if x + 1)Unchanged:
declared_type_inhabitance_direct_call_witness_testis unchanged. Its one FAIL,w_a_branded_product_refinement_at_an_unrelated_product_formal_still_refuses, is already enrolled in the expected-red roster on main.Residue: Int and Float guards (not a declared drop; the rung was never higher)
declared_realizes_as_kernel_numericadmits an Int or Float produced value at any declared type whose provenance realizes natively, andprovenance_realizes_nativelyanswers true for everyKernelMintedtype, including Bool and String. So the gap is in the shared relation, not the guard wiring, and it reaches every wired position.v2.workflow.floor_expected_redfloor_expected_red_chunk_int_guard_admitted_by_the_relation. They pass, and leave the roster as regression controls, once the relation requires the declared side to realize as a numeric.Row
gunbc.recurring_failure_mode.interpreter_ignores_match_arm_guardsnow records:x if s =>parsess => 1as a lambda, so a single-binding guard must be parenthesised;DeclaredTypeNotInhabitedisGateBlocking;Cost note
The two Int expected-red rows measured about 5 s CPU each in these runs, against 183 ms for the String row. If the floor's cost gate objects, the cause is
compile_dag_diagnostic_censuson those fixtures, not the check itself.🤖 Generated with Claude Code