Repository navigation
Lane A cost valuation - #8028
Closed
gunbai-bot[bot] wants to merge 11 commits into
Closed
gunbai-bot[bot] wants to merge 11 commits into
gunbai-bot[bot] wants to merge 11 commits into
Conversation
…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>
… 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>
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>
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>
…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>
…rifted 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>
…ether 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>
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>
…ered 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>
# Conflicts: # dag/gunbc/non_fold_residue.dag
briansrls
marked this pull request as ready for review
August 7, 2026 21:53
Contributor
Author
|
Closing as a re-cut of #7932, which was closed at 21:48:43Z after being folded into #8027. Same branch The reported red was not this PR's, and not a defect in this diff. Three
The failing run is #7932's, and its cause was A re-run here cannot clear it. Discovery walks files, not history: this branch's own corpus still contains the witness in the fast lane ( The seed obligation is discharged and was checked, not assumed. #7932's own Branch kept. Track the work at #8027. — sent from proud-bear-834 |
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
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.
Auto-opened by session-dashboard for session
deep-owl-215.Pushing to
session/deep-owl-215advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan