Repository navigation
C0(c): split lens_contract_complexity's RatchetForever permanence claim into two distinct contract subjects - #7841
Merged
Merged
Conversation
The partition witness failed to typecheck because a line-broken == was parsed as a new statement; keep the exhaustiveness check on one line. Add explicit ConstructionJustification imports to v2.lens.complexity. Co-authored-by: Cursor <cursoragent@cursor.com>
The C0(c) split introduced structural-equality matches over the new claim coproducts; enroll them in non_fold_residue_frontier so the always-on corpus-read gate does not red on an unrostered site. Co-authored-by: Cursor <cursoragent@cursor.com>
The 2026-08-04 falsifier-build/falsifier job split left falsifier_cold_control_steps_follow_floor_in_job_order calling falsifier_job_steps() without a job_id; use falsifier_floor_job_steps() so the cold-control steps resolve from the floor job. Co-authored-by: Cursor <cursoragent@cursor.com>
Keep #7841 scoped to the C0(c) contract split only. The two job_id witness failures are main-red and expected on this PR. Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 6, 2026
…I fixed (review 49289)
Review 49289 caught three more instances of exactly the defect this PR exists
to remove, and it was right: I corrected one occurrence and did not sweep for
the class -- the same shortcut I would send back on someone else's diff.
Fixed, all verified against main rather than recalled:
section 7 C0(c) bullet still called the split "the next implementation
slice" while the C0 summary said DELIVERED
section 9 operator ruling same, so a reader of section 9 could still treat
C0(c) as open
section 2 table still listed a single lens_contract_complexity row
carrying RatchetForever. That row does not exist on
main. Replaced with the two rows that do --
derived_kernel (WallAfterGrounding) and optimality
(RatchetForever, the genuinely undecidable residue)
Two the review did not name, found by sweeping for the class instead of the
reported lines:
section 4 asserted in the present tense that lens_contract_complexity
carries RatchetForever. Marked RESOLVED by #7841 and kept as the
argument the split rests on, rather than deleted -- the reasoning
is why the split has the shape it has
section 8 a discriminating control named the deleted contract. Re-pointed
at both split rows, where the mode/consumer disagreement is
actually checkable
status blockquote said one carrier "currently" declares it permanent
Remaining bare mentions at lines 119, 143 and 147 are deliberate historical
references ("the mixed row", "as written then") describing the pre-split state
in explicitly past tense, not live claims about the tree.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 6, 2026
…sfiable condition (review 49307) Third catch of the same class, and this one was more than a stale name -- the retirement criteria were unsatisfiable as written. Clause 1 required that "lens_contract_complexity's boundary class distinguishes the genuinely undecidable residue from the decidable capability". That is precisely what #7841 delivered, so the clause is SATISFIED and now says so, naming the two rows that replaced the mixed one. Clause 2 required that "lens_contract_complexity has a live consumer witness and has flipped off AuditOnly". Read onto the split, that can never be true. lens_contract_complexity_optimality is RatchetForever and stays permanently AuditOnly by the plan's own section 7 C0(c) ruling -- so a retirement condition demanding it flip would make this doc unretirable BY CONSTRUCTION. Re-scoped to lens_contract_complexity_derived_kernel, which is the half that can legitimately flip, and the clause now states explicitly why optimality is excluded so nobody re-adds it later. That second half is the part worth noticing: a dissolution trigger that cannot fire is a scaffold with no exit, which is the failure DESIGN section 6 asks a named trigger to prevent. The stale name would have been cosmetic; the unsatisfiable condition was not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 6, 2026
…nstead Reviews caught this plan stale in four separate places, each claim true when written and false a day later. The common shape was a merge-event assertion -- "DELIVERED ON MERGE of #7841", "both rows are on main" -- which rots without anyone touching it, because nothing in the tree can decide it. Replace the class, not the four lines. Every delivery claim now names the carrier SYMBOL a reader can resolve (DESIGN section 3, cite-the-symbol), so it is decidable by grep rather than by remembering which PR merged when. Verified: all seven cited symbols resolve; zero PR numbers and zero merge-event phrases remain in the carrier. Also fixes a real dangling reference the C0(c) split created: the census note in gunbc.v1_complexity_capability_census cited lens_contract_complexity, a row that no longer exists. Re-pointed at lens_contract_complexity_derived_kernel, which is the one a consumer surface would actually move -- optimality is AuditOnly permanently.
briansrls
pushed a commit
that referenced
this pull request
Aug 6, 2026
…an still reads OPEN (#7900) * WIP: cost analysis * The signed accent selects a class; it does not re-author its colour (#7895) signed_accent_render was a second StarlightRender literal carrying fields byte-identical to g_render twelve lines above it in the same file — hue 45, sat 26, light 87, name "g-starlight" — so one decided colour was authored twice and held in agreement by nobody. Row 4 signed a CLASS, and a selection is a reference, so signed_accent_render is now g_render. The failure this closes is not hypothetical: retuning the G projection against the cited chromaticity would have moved g_render and left the SIGNED row behind, and the site would have kept painting a colour the signature no longer described while every witness stayed green. witness_signed_accent_is_g_and_live repeated witness_g_class_is_the_live_night_ figure's three field comparisons verbatim — the same expression twice once the rows are one value — so it collapses to the part that is still falsifiable: which class the signature selects. Renamed witness_signed_accent_selects_the_g_class. ONE FORK REMAINS AND IS NOT PAPERED OVER: gunbc.design.theme warm_starlight carries the same three numbers a third time under its own name, and witness_g_class_is_the_live_night_figure holds it in agreement with this projection by comparison rather than derivation — validation standing where construction was available (DESIGN §5). accent_signed_note now records that, and names the open question it waits on: whether the site-independent register library may take its accent from a site-layer projection, or whether night_theme is a site instance that should be assembled at the site layer. Not decided unilaterally — design.theme has two consumers (the site and the srv1 roadmap dashboard). Green by execution: the four affected witnesses PASS (selection, live-night figure, no-green in source and projection, study page emits). RED control verified by execution — re-pointing signed_accent_render at k_render FAILs witness_signed_accent_selects_the_g_class. The collapse is value-identical by construction (the literals were byte-identical), so no emission can change. Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> * Execute the name-key precondition C0(b2)'s join was assuming classification_matches_fact joins a roster row to a DeclFact on BARE NAME, while DeclFact carries qualified_name and kind and could key exactly. That is sound only while every top-level declaration of v1.compiler.complexity has a distinct name, and nothing in the carrier makes that true -- it is a property of the subject module, not a wall this carrier erects. Measured over src/v1/complexity.dag: 201 top-level declarations (171 fn, 26 type, 4 data, 0 let), zero duplicate names. So the join is correct today. But a measurement of the current tree is not an oracle (DESIGN section 5), so the precondition is now EXECUTED rather than assumed. The gap this closes is real and none of the four existing totality witnesses covers it: a duplicate name in the DERIVED population still classifies, still matches a roster row, and leaves no stale row, so one roster row can silently answer for two declarations while every count agrees. roster_names_distinct does not cover it either -- it constrains the AUTHORED side only, and the duplicate here would be on the derived side. Added population_names_distinct beside the existing roster_names_distinct, reusing name_already_seen rather than minting a second distinctness fold. Green by execution, all three run through claim_batch against the real tree: PASS w_population_decl_names_are_distinct (live population) PASS w_distinctness_fold_reds_on_a_planted_duplicate (discriminating RED) PASS w_distinctness_fold_accepts_a_distinct_control (positive control) The RED matters: a distinctness fold that cannot fail proves nothing, so a planted same-name pair must come back false or the live green is empty. Dissolve-on is named on the carrier: the roster carrying exact DeclFact identity (qualified_name, or name plus kind) makes the join exact by construction and retires the precondition. That is a 201-row re-authoring and is deliberately not bundled here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Sweep the stale-status class across the whole plan, not the one line I fixed (review 49289) Review 49289 caught three more instances of exactly the defect this PR exists to remove, and it was right: I corrected one occurrence and did not sweep for the class -- the same shortcut I would send back on someone else's diff. Fixed, all verified against main rather than recalled: section 7 C0(c) bullet still called the split "the next implementation slice" while the C0 summary said DELIVERED section 9 operator ruling same, so a reader of section 9 could still treat C0(c) as open section 2 table still listed a single lens_contract_complexity row carrying RatchetForever. That row does not exist on main. Replaced with the two rows that do -- derived_kernel (WallAfterGrounding) and optimality (RatchetForever, the genuinely undecidable residue) Two the review did not name, found by sweeping for the class instead of the reported lines: section 4 asserted in the present tense that lens_contract_complexity carries RatchetForever. Marked RESOLVED by #7841 and kept as the argument the split rests on, rather than deleted -- the reasoning is why the split has the shape it has section 8 a discriminating control named the deleted contract. Re-pointed at both split rows, where the mode/consumer disagreement is actually checkable status blockquote said one carrier "currently" declares it permanent Remaining bare mentions at lines 119, 143 and 147 are deliberate historical references ("the mixed row", "as written then") describing the pre-split state in explicitly past tense, not live claims about the tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix the dissolution trigger: it named a deleted row and set an unsatisfiable condition (review 49307) Third catch of the same class, and this one was more than a stale name -- the retirement criteria were unsatisfiable as written. Clause 1 required that "lens_contract_complexity's boundary class distinguishes the genuinely undecidable residue from the decidable capability". That is precisely what #7841 delivered, so the clause is SATISFIED and now says so, naming the two rows that replaced the mixed one. Clause 2 required that "lens_contract_complexity has a live consumer witness and has flipped off AuditOnly". Read onto the split, that can never be true. lens_contract_complexity_optimality is RatchetForever and stays permanently AuditOnly by the plan's own section 7 C0(c) ruling -- so a retirement condition demanding it flip would make this doc unretirable BY CONSTRUCTION. Re-scoped to lens_contract_complexity_derived_kernel, which is the half that can legitimately flip, and the clause now states explicitly why optimality is excluded so nobody re-adds it later. That second half is the part worth noticing: a dissolution trigger that cannot fire is a scaffold with no exit, which is the failure DESIGN section 6 asks a named trigger to prevent. The stale name would have been cosmetic; the unsatisfiable condition was not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: cost analysis * Remove merge-event status prose from the plan; cite carrier symbols instead Reviews caught this plan stale in four separate places, each claim true when written and false a day later. The common shape was a merge-event assertion -- "DELIVERED ON MERGE of #7841", "both rows are on main" -- which rots without anyone touching it, because nothing in the tree can decide it. Replace the class, not the four lines. Every delivery claim now names the carrier SYMBOL a reader can resolve (DESIGN section 3, cite-the-symbol), so it is decidable by grep rather than by remembering which PR merged when. Verified: all seven cited symbols resolve; zero PR numbers and zero merge-event phrases remain in the carrier. Also fixes a real dangling reference the C0(c) split created: the census note in gunbc.v1_complexity_capability_census cited lens_contract_complexity, a row that no longer exists. Re-pointed at lens_contract_complexity_derived_kernel, which is the one a consumer surface would actually move -- optimality is AuditOnly permanently. * chore: regenerate drifted generated artifacts (ci auto-heal) * WIP: cost analysis * Stop the witness-admission row scan slicing UTF-8 prose mid-character The floor worker died exit 101 with no terminal receipt on witness_admission_entry_function_keys_from_source: WINDOW is a 400-BYTE budget applied to UTF-8 prose via after.len().min(WINDOW), so whenever byte 400 lands inside a multi-byte char the slice panics and takes the whole run down. The row that exposed it simply happened to put an em dash across that offset. Every other slice in that function takes its offset from find/split_once, which return char boundaries; this fixed offset was the only unguarded one. It now walks down to the nearest boundary, so an over-long row is truncated rather than fatal. Note the comment directly above already recorded an earlier panic in this same function, so the failure mode has form. Fixing the string instead of the scanner was the tempting move and it is the unmarked workaround DESIGN section 5 forbids: it would leave the defect armed for the next author who writes prose with an em dash in it. So the em dash stays in the row, and the scanner is what changed. PROVEN DISCRIMINATING BY EXECUTION, both directions: - unfixed: panics "byte index 400 is not a char boundary; it is inside em dash (bytes 398..401)" -- the production failure reproduced exactly - fixed: passes The fixture puts entry: and function: FIRST, mirroring real rows, because the scanner deliberately panics when entry: falls outside the window and that refusal is correct behaviour rather than the bug under test -- an earlier draft of this fixture tripped that arm and would have tested the wrong thing. The prose is a run of em dashes shifted by 0/1/2 ASCII bytes, covering every residue class mod 3, so at least one iteration is GUARANTEED to put the window edge strictly inside a character. The test deliberately does not model where the scanner sets search_from; pinning that offset would make the fixture fail for the wrong reason the moment the scanner moves. --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 8, 2026
…ries #8010's witness retirement) (#8027) * WIP: cost analysis * Execute the name-key precondition C0(b2)'s join was assuming classification_matches_fact joins a roster row to a DeclFact on BARE NAME, while DeclFact carries qualified_name and kind and could key exactly. That is sound only while every top-level declaration of v1.compiler.complexity has a distinct name, and nothing in the carrier makes that true -- it is a property of the subject module, not a wall this carrier erects. Measured over src/v1/complexity.dag: 201 top-level declarations (171 fn, 26 type, 4 data, 0 let), zero duplicate names. So the join is correct today. But a measurement of the current tree is not an oracle (DESIGN section 5), so the precondition is now EXECUTED rather than assumed. The gap this closes is real and none of the four existing totality witnesses covers it: a duplicate name in the DERIVED population still classifies, still matches a roster row, and leaves no stale row, so one roster row can silently answer for two declarations while every count agrees. roster_names_distinct does not cover it either -- it constrains the AUTHORED side only, and the duplicate here would be on the derived side. Added population_names_distinct beside the existing roster_names_distinct, reusing name_already_seen rather than minting a second distinctness fold. Green by execution, all three run through claim_batch against the real tree: PASS w_population_decl_names_are_distinct (live population) PASS w_distinctness_fold_reds_on_a_planted_duplicate (discriminating RED) PASS w_distinctness_fold_accepts_a_distinct_control (positive control) The RED matters: a distinctness fold that cannot fail proves nothing, so a planted same-name pair must come back false or the live green is empty. Dissolve-on is named on the carrier: the roster carrying exact DeclFact identity (qualified_name, or name plus kind) makes the join exact by construction and retires the precondition. That is a 201-row re-authoring and is deliberately not bundled here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Sweep the stale-status class across the whole plan, not the one line I fixed (review 49289) Review 49289 caught three more instances of exactly the defect this PR exists to remove, and it was right: I corrected one occurrence and did not sweep for the class -- the same shortcut I would send back on someone else's diff. Fixed, all verified against main rather than recalled: section 7 C0(c) bullet still called the split "the next implementation slice" while the C0 summary said DELIVERED section 9 operator ruling same, so a reader of section 9 could still treat C0(c) as open section 2 table still listed a single lens_contract_complexity row carrying RatchetForever. That row does not exist on main. Replaced with the two rows that do -- derived_kernel (WallAfterGrounding) and optimality (RatchetForever, the genuinely undecidable residue) Two the review did not name, found by sweeping for the class instead of the reported lines: section 4 asserted in the present tense that lens_contract_complexity carries RatchetForever. Marked RESOLVED by #7841 and kept as the argument the split rests on, rather than deleted -- the reasoning is why the split has the shape it has section 8 a discriminating control named the deleted contract. Re-pointed at both split rows, where the mode/consumer disagreement is actually checkable status blockquote said one carrier "currently" declares it permanent Remaining bare mentions at lines 119, 143 and 147 are deliberate historical references ("the mixed row", "as written then") describing the pre-split state in explicitly past tense, not live claims about the tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix the dissolution trigger: it named a deleted row and set an unsatisfiable condition (review 49307) Third catch of the same class, and this one was more than a stale name -- the retirement criteria were unsatisfiable as written. Clause 1 required that "lens_contract_complexity's boundary class distinguishes the genuinely undecidable residue from the decidable capability". That is precisely what #7841 delivered, so the clause is SATISFIED and now says so, naming the two rows that replaced the mixed one. Clause 2 required that "lens_contract_complexity has a live consumer witness and has flipped off AuditOnly". Read onto the split, that can never be true. lens_contract_complexity_optimality is RatchetForever and stays permanently AuditOnly by the plan's own section 7 C0(c) ruling -- so a retirement condition demanding it flip would make this doc unretirable BY CONSTRUCTION. Re-scoped to lens_contract_complexity_derived_kernel, which is the half that can legitimately flip, and the clause now states explicitly why optimality is excluded so nobody re-adds it later. That second half is the part worth noticing: a dissolution trigger that cannot fire is a scaffold with no exit, which is the failure DESIGN section 6 asks a named trigger to prevent. The stale name would have been cosmetic; the unsatisfiable condition was not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: cost analysis * Remove merge-event status prose from the plan; cite carrier symbols instead Reviews caught this plan stale in four separate places, each claim true when written and false a day later. The common shape was a merge-event assertion -- "DELIVERED ON MERGE of #7841", "both rows are on main" -- which rots without anyone touching it, because nothing in the tree can decide it. Replace the class, not the four lines. Every delivery claim now names the carrier SYMBOL a reader can resolve (DESIGN section 3, cite-the-symbol), so it is decidable by grep rather than by remembering which PR merged when. Verified: all seven cited symbols resolve; zero PR numbers and zero merge-event phrases remain in the carrier. Also fixes a real dangling reference the C0(c) split created: the census note in gunbc.v1_complexity_capability_census cited lens_contract_complexity, a row that no longer exists. Re-pointed at lens_contract_complexity_derived_kernel, which is the one a consumer surface would actually move -- optimality is AuditOnly permanently. * chore: regenerate drifted generated artifacts (ci auto-heal) * WIP: cost analysis * Stop the witness-admission row scan slicing UTF-8 prose mid-character The floor worker died exit 101 with no terminal receipt on witness_admission_entry_function_keys_from_source: WINDOW is a 400-BYTE budget applied to UTF-8 prose via after.len().min(WINDOW), so whenever byte 400 lands inside a multi-byte char the slice panics and takes the whole run down. The row that exposed it simply happened to put an em dash across that offset. Every other slice in that function takes its offset from find/split_once, which return char boundaries; this fixed offset was the only unguarded one. It now walks down to the nearest boundary, so an over-long row is truncated rather than fatal. Note the comment directly above already recorded an earlier panic in this same function, so the failure mode has form. Fixing the string instead of the scanner was the tempting move and it is the unmarked workaround DESIGN section 5 forbids: it would leave the defect armed for the next author who writes prose with an em dash in it. So the em dash stays in the row, and the scanner is what changed. PROVEN DISCRIMINATING BY EXECUTION, both directions: - unfixed: panics "byte index 400 is not a char boundary; it is inside em dash (bytes 398..401)" -- the production failure reproduced exactly - fixed: passes The fixture puts entry: and function: FIRST, mirroring real rows, because the scanner deliberately panics when entry: falls outside the window and that refusal is correct behaviour rather than the bug under test -- an earlier draft of this fixture tripped that arm and would have tested the wrong thing. The prose is a run of em dashes shifted by 0/1/2 ASCII bytes, covering every residue class mod 3, so at least one iteration is GUARANTEED to put the window edge strictly inside a character. The test deliberately does not model where the scanner sets search_from; pinning that offset would make the fixture fail for the wrong reason the moment the scanner moves. * Lane A C1: evaluate CostExpr at concrete SizeVariable bindings, with the CostSum binder lexically scoped The subject is semantic work, not hardware time: a CostExpr plus concrete bindings yields exact, unresolved, or refused modelled work. No duration, rate, or calibration constant enters this module. The load-bearing part is binder handling. v2.lens.cost.expr normalize_cost_expr_to_symbolic matches CostSum with the binder discarded, so a binder-dependent body projects a SymbolicCost naming a variable that is bound inside the sum - the magnitude may survive, the variable identity does not. This evaluator does not inherit that: env_bind prepends and lookup_bindings answers the head-most match, so a binder shadows an outer binding of the same identity for the extent of its body and only for that extent, with removal on exit structural rather than an unbind step. Proven by execution against a binder-discarding mutation: pinning the binder to Zero reds binder_dependent_body_is_summed_not_treated_as_invariant and binder_shadowing_is_scoped_and_removed_on_exit while leaving the invariant-body and zero-iteration witnesses green - which is the exact signature of the defect, and is why the existing C1 fixture (same variable for binder and bound) cannot see it. A second mutation answering zero for an unbound variable reds both missing-binding witnesses while zero_iterations_produce_exact_zero stays green: that pairing is what keeps a zero in a cost report unambiguous between nothing to do and nothing modelled. Carriers: v2.lens.cost.valuation CostEvaluation, CostValuationBinding, evaluate_cost_expr, evaluate_cost_expr_partially; std.algebra FreeSemigroup with v2.std.algebra non_empty_singleton / non_empty_append. The nonempty arms are carried by std.algebra FreeSemigroup - the free semigroup over T exactly as FreeMonoid is the free monoid over T, one algebraic axis at two identities. Its head field is the construction wall: an UnresolvedCost naming no free variable and a refusal carrying no cause have no representation, rather than being validated against. It is deliberately not the Refined<List<T>> spelling of the manual fixture, whose refinement predicate concedes the empty state is writable, and the NonEmptyList alias is withheld until that fixture retires so one name never resolves to two declarations. NonEmptyDiagnostics, FiniteSet, NonEmptySymbolChain and NonEmptyGrammarChoiceAmbiguityRows are the same shape monomorphised and dissolve onto it at their own already-declared triggers; that corpus-wide de-fork is not carried here. Stated gaps rather than silent ones: BoundedCost is declared-not-produced because its seed is a ceiling-valued binding, which is the sibling discrete-cost note's envelope scope; CostLog refuses its magnitude through the expression authority's own vocabulary until a cited integer-logarithm authority exists on std.nat. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 49620 and the parent lane review: interval arithmetic, claim totality, quadratic accumulation, and a false citation Bounded-upper CostSum answered an EXACT value. combine_evaluation of ExactCost 3 and ExactCost 7 under nat_max reaches combine_known with both endpoints at 3, so bounded_or_exact collapses to ExactCost 7 — an exactness claim manufactured from an inexact input, sitting exactly where the envelope lane plugs its seed in. Replaced with evaluation_interval, which pairs the LOWER of one evaluation with the UPPER of a different one; an inverted interval refuses with InvertedCostInterval rather than being normalised by swapping the endpoints. Witnessed at its own seam because the arm has no producer yet; restoring the max spelling reds three of the four new witnesses. The PR body claim that the envelope lane adds a seed and no arithmetic was therefore false and is retracted. The Tier1 claim conjunction ran three of thirteen witnesses while its label asserted the refusal and scoping behaviour the other ten established, so CI could go green with the label false. every_valuation_witness_holds now enumerates every test fn in the file. Refusal accumulation was quadratic and reachable today: non_empty_append is linear in its left argument, so a body refusing under upper = u built u causes left-nested — and CostEffect refuses unconditionally in this slice. The causes were also IDENTICAL, because the body expression is fixed and only the binder value changes, so this amplified one deficit u times rather than counting u deficits. evaluate_summation now stops evaluating the body once the accumulator has settled; the soundness argument (a refusal here is a property of the body expression, not the binder's value) and its dissolve-on are on the carrier, and the new one-cause witness reds when the skip is removed. The FreeSemigroup grounding note carried a false citation, in the note arguing for single authority. Of the four carriers it named as each already carrying a migrate_when_nonempty_list_refinement_promoted trigger, grep says only two do, and a fifth instance was omitted. Corrected to five carriers, two triggered. Both surviving triggers are RETARGETED onto FreeSemigroup: they named the event as promoting the manual refinement to std, and this change decided that promotion is not the mechanism, so they would have been left waiting on an event that cannot occur as spelled. Also: the partial evaluation mode is stated as not being an escape from a refusal (swapping entry points to silence one is the author-side absorbing fallback); the order note now says causes accumulate WITHIN an arm and the dominated side's payload is dropped ACROSS arms; and the projection-path binder discard in normalize_cost_expr_to_symbolic is named as tracked debt with its trigger and the reason the existing fixture cannot see it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Trigger the pull_request ci workflow, which never fired for this branch Zero GitHub Actions runs were created for either pushed SHA over roughly an hour, while sibling branches got ci runs throughout that window; the run was not awaiting approval either. main protection requires the ci check, so an empty synchronize is the only way to get one. Two approvals on the previous head are re-earned rather than assumed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Recut to the exact core; fix the log arm reporting the wrong cause Operator ruling: scope to complete exact valuation. Kept — exact valuation at a complete binding set, CostSum binder scoping and shadowing, duplicate refusal, effect refusal, log refusal, and the earned-zero versus fabricated-zero distinction. Held on session/deep-owl-215-partial-bounded-hold — partial evaluation and bounded evaluation, sequenced rather than rejected, with both constraints that ride with them recorded on the carrier so they cannot be quietly undone: complete and partial stay TWO ENTRY POINTS over one fold, and the unresolved state must carry the residual CostExpr, not just free-variable names. CostEvaluation is two states here because at the exact core there are exactly two honest answers: the work is this number, or here is why it cannot be. Declaring an arm with no producer is rung inflation — and the bounded arm in particular was carried through an earlier revision while its arithmetic silently collapsed a two-endpoint envelope to its own ceiling. The log arm reported the wrong cause. It matched CostLog { base: _, .. }, ignored the base entirely, and answered UngroundedLogArgument for every non-refusing case — so base 0 read as an ARGUMENT problem, and a fully grounded argument was called UNGROUNDED, while v2.lens.cost.expr's normalizer right beside it already checked the base against its own InvalidLogBase. Two paths disagreeing about one fact. Now three distinct causes for three unrelated failures: an invalid base refuses through the expression authority's InvalidLogBase (cited, not re-minted), an unbound argument refuses as MissingSizeBinding like any other unbound size, and a valid base with an exact argument refuses as IntegerLogarithmUnavailable, which names the real gap and is countable against it. Restoring the base-ignoring arm reds both invalid-base witnesses; the base-zero and grounded-argument pair is the discriminating one, since the old arm gave both the same cause. All 16 witnesses green by execution, all 16 enrolled in the claim conjunction. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Enroll the claim conjunction as a test fn: it was the one orphan the naming-hygiene gate found The enroll-or-refuse pre-plan walk refused v2.test.lens_cost.valuation every_valuation_witness_holds as a plain fn unreachable from every test fn and test data — silent de-enrollment. It is the single root of the run: the ci job's failure was FloorUpstreamAlreadyRed with build=success and heal=success, which adds no verdict of its own. Note the remedy that does NOT work, since it is the obvious one: the claim data already referenced the helper by name — that is what it exists for — and a plain `data` does not count as reachability for this gate. Promotion to `test fn` is what satisfies it. Worth naming the shape rather than just fixing it: the conjunction was factored out to close review 49620's finding that the claim enumerated three of thirteen witnesses, and the helper that fixed a specification-without-execution defect was itself not executed by anything the gate recognises. Same class, one level out. The totality note now says so, so the next reader sees why the enrollment is deliberate rather than incidental. 17 witnesses green by execution; the local pre-plan walk that produced the CI refusal now completes clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Regenerate the stage0 seed: adding FreeSemigroup to a std authority drifted the self-host fixed-point regen_verify_gate_passes returned false because src/v1/stage0/src/std_algebra.rs did not contain the FreeSemigroup the emitter now produces from dag/std/algebra.dag. Adding a type to a std authority without regenerating the committed emitter output is exactly what the fixed-point gate exists to catch. Regenerated with regen_stage0 rather than hand-edited — the file is emitter output, and a hand-added struct would pass the diff while making the seed diverge from its authority. The diff is 7 lines, additive, only the struct. Order mattered: regenerate, rebuild the seed binaries from the regenerated sources, then verify with those binaries — regen_divergence_count=0, and 17 witnesses green against the rebuilt seed. The ci job's failure was again FloorUpstreamAlreadyRed with build and heal green, so regen was the only real signal. Note on the emitted shape, since it is visible in the diff: FreeSemigroup carries a _phantom: PhantomData<T> beside an already-inhabited T. That is the emitter's established convention for generic structs here, not something this type triggered — 25 of 39 structs in this one file carry it, including Magma<T> and the FieldOfFractions<R> pair DESIGN names as correctly grounded. There are zero construction sites for it in emitted Rust, so it imposes nothing on call sites. Whether the convention is a defect is a corpus-wide emitter question, not this PR's. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Zero is a two-sided annihilator: fix CostMul and symbolic_product together CostMul routed both sides through the generic refusal-dominates combiner, so CostMul of zero and CostEffect refused while the symbolic authority answered zero for the same expression — two paths disagreeing about one CostExpr, and the exact evaluator was the wrong one: a zero multiplicity means the body is never executed, so refusing because an unexecuted factor lacks an effect model is the did-no-work versus could-not-model conflation the earned-zero controls exist to prevent. Fixing only that would have traded one divergence for a narrower one, because the reference was itself ASYMMETRIC: symbolic_product matched a's arms first, including UnknownCost, and only then inspected b — so zero times unknown absorbed while unknown times ZERO returned unknown. Multiplication is commutative, so an operand order that changes the answer is a defect, not a style. Both paths are fixed in one motion and now agree in both orders. The annihilator lives in a multiplication-specific function and beats refusal-dominance, which governs every other combination here. That ordering is load-bearing and the carrier says so: checking refusals first reads like tightening a fail-closed path and would silently restore the defect, with only the two zero-times-effect witnesses reding. Controls, both directions on both properties, because an asymmetry defect cannot be caught by an asymmetric test: zero times unknown and unknown times zero both absorb; one times unknown and unknown times one both stay unknown; zero times CostEffect and CostEffect times zero are both ExactCost zero; one times CostEffect still refuses. Mutations discriminate — reverting multiply_evaluations reds both zero-order witnesses while one-times-effect still refuses; restoring the old arm order reds only the right-operand case. 24 witnesses green. The Blocking cost-wall baseline was re-run because this touches an authority feeding it: loop_iteration_floor (incl. its independent linear-times-zero control), disj_alternative_floor, bounded_summation (incl. existing_cost_lens_kernel_unchanged), atom_zero, expr_refusal and copied_port_derivation — 19 witnesses, all green. Witness accounting corrected: the claim label and note now say every LEAF witness, which the aggregating conjunction obviously cannot include itself in. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Qualify the one bare nat_max the second Nat authority made ambiguous Adding v2.std.nat.nat_max (the Peano Nat, needed by evaluate_size_expr's SizeMax and evaluate_cost_expr_in_env's CostMax) gave the name two declarations. test.claim.realization_schedule_critical_path is the single module whose import closure carries both authorities, so its bare call site stopped resolving and reddened the compile-clean gate. Qualified as std.nat.nat_max, matching the std.nat.nat_compare already qualified on the line above it inside the same witness. The four other bare nat_max call sites were checked by scoped compile rather than assumed safe -- dag/std/realization_width, dag/std/realization_measurement, dag/gunbc/econ/free_tier_serving and dag/gunbc/econ/scm_serving_model each compile with zero errors, so their closures do not carry both authorities and they need no qualification. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the two hygiene gates: exhaustive arms where possible, one rostered residue The floor reported three reds. Two roots, one of them not mine. NON-FOLD RESIDUE. Three wildcard arms landed with the exact evaluator. Two were avoidable and are now gone rather than declared: combine_evaluation and evaluate_summation match over CostEvaluation, which has exactly two variants, so `_ =>` became `ExactCost { value: .. } =>`. DESIGN section 5 puts construction above declaring a residue, and it buys what a roster row cannot -- a third CostEvaluation variant would now make both matches non-exhaustive and compile-clean would refuse, instead of the new variant being swept into a wildcard silently. multiply_evaluations is rostered, not "fixed". Its arms discriminate a nested VALUE (an ExactCost carrying Zero) rather than a variant, so enumerating would write the residual combine_evaluation call twice, underneath the arm order that multiply_evaluations_zero_note declares load-bearing. Duplicating that expression to satisfy a counter would make the function more fragile. Its reason says so, rather than reusing the generic nfr_reason_mint_era its neighbours carry. INERT CARRIER. Not from this change. Probing inert_carrier_names_live returned eleven live names against twelve rostered; the extra is ProcMeminfo, whose consumer landed in #7891 -- already an ancestor of this branch -- while the roster row stayed. origin/main carries both files byte-identically, so this witness is red on main too. The row is deleted here because it blocks merge and deletion is exactly what its own dissolve trigger prescribes; reported upstream so another lane does not duplicate it. Also records, in symbolic_product_zero_absorption_note, that the symmetry the annihilator fix established is CLASSIFICATION and not provenance: unknown times unknown still returns the left operand's diagnostic. That is pre-existing and module-wide (symbolic_sequential drops the same way), and closing it means widening UnknownCost to carry several diagnostics, which is its own change with its own witnesses. Green by execution: non_fold_residue_clean_holds, non_fold_residue_no_unrostered_or_stale, inert_carrier_no_unrostered_or_stale, and every_valuation_witness_holds over all 23 leaf witnesses -- the last because the exhaustive-arm edits rewrote live evaluation paths, not just roster data. Seed receipt reports unrostered=0 stale=0 live=149. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Roster #7965's two carriers and handle #7909's two git mock cases Both failing witnesses on this PR are MAIN-SIDE DEBT landed today, not this branch's. Neither constituent introduced them and neither of main's own runs executed the witnesses that catch them. inert_carrier_no_unrostered_or_stale. TerminatingOneShotFrontier and WitnessPurpose (dag/std/witness_purpose.dag, #7965) are a taxonomy landed ahead of its consumer: nothing outside their own module and their own test file references them, which is precisely the seed's inert predicate (declared once, referenced by a test, zero non-test references outside the declaration block). They get roster rows in the established shape, carrying the shared dissolve trigger -- a live consumer reads the carrier and the stale-roster check then forces the row's deletion. git_mock_consumer_is_total_holds. #7909 added git.Inspect.WorkingTreeStatus and git.Inspect.IgnoredFiles to git_published_mock_corpus without arms in materialize_git_mock, so both fell to mock_unhandled_rejection and totality failed. main publishes 20 cases against 18 arms; this adds the two arms. HOW THE OWNER WAS ESTABLISHED, because my first attribution was wrong. I found seven type carriers new versus main and inferred they were the inert ones -- true premise, unsupported conclusion, since none of the seven can satisfy the predicate (five are referenced by no test file at all; the other two are consumed in non-test fn signatures). The primitive is not directly invocable (no unique runtime declaration identity) and a second-worktree run is invalid because the corpus scan anchors to the compile-time-baked workspace root. So the rule was read out of the seed and reimplemented, and THE REPLICA IS VALIDATED AGAINST THE EXECUTED ORACLE: on this head it reproduces 13 inert against 11 rostered, exactly the unrostered=2 stale=0 the real run measured. Run over three trees it gives main 2 unrostered + 1 stale, pr-7932 clean, this branch main's 2 with main's stale already fixed -- so this branch was strictly better than main before this commit. GREEN BY EXECUTION, with the discriminating red on the real consumer: inert_carrier_no_unrostered_or_stale FAILED on this head before this commit and PASSES after; git_mock_consumer_is_total_holds likewise, alongside both omission RED controls (git_mock_omitted_member_is_red_holds, git_mock_omitted_show_tree_is_red_holds) still passing, so the added arms did not disarm the controls. No regen: neither module projects to a stage0 seed file and no seed .rs references the roster units, verified against a positive control (dag/std/algebra.dag does project, to std_algebra.rs). 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> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.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.
Summary
C0(c) splits the mixed
lens_contract_complexitypermanence claim into two distinct contract subjects, as ruled in the v2 complexity capability parity program:lens_contract_complexity_derived_kernel(ComplexityDerivedKernel) — decidable capability (asymptotic projection, bounded work/span, summation, output size, peak space, bounded-input evaluation, acyclic summaries, descent-grounded SCCs) carriesWallAfterGrounding { dissolves_to: SingleAuthority }(dissolves when Parity C2ComplexitySummarylands onv2.lens.cost).lens_contract_complexity_optimality(ComplexityOptimality) — genuinely undecidable residue (global optimality, complete rewrite discovery, unrestricted semantic complexity equivalence) honestly keepsRatchetForever, permanentAuditOnly.The old single
Complexity/lens_contract_complexityrow is removed rather than flipped in place. Scope authority lives inv2.lens.enforcement.complexity_contract_subjectwith typed claim rosters; a witness proves the two subjects are disjoint and jointly exhaust the legacy mixed row.Test plan
complexity_contract_subject_partition_witness_test.dag(4 witnesses: partition holds, derived↔optimality subject RED controls, duplicate-roster RED)lens_registry.sg_claims_test— both newLensIdV0rows resolve with singleton bound countsenforcement_live_witness_test/enforcement_inventory_witness_test— updated unbound-contract enumerations