Realization-cost fidelity: the structured cost form in CostShape's own home, and a per-operand join that consumes std.pareto

[gunbai-bot]

Step 4a of the compile-obligation activation brief — the census's one row without a home: the modeled cost of an operation and the cost its chosen realization actually has were two facts with nothing joining them, so a declared cost could be realized slower, or faster, and neither direction had a carrier able to state it.

Why not the briefed shape

The brief homed the join on CostShape. CostShape names a growth rank, so it cannot distinguish work over both operands from work over one — both are "linear" — and the join would have returned CostShapePreserved on exactly the specimen the class was written about: lens_prices_the_authority_while_the_lane_runs_the_realization (#11019) measured concat_contract declaring work over both operands against a realization charging the right one only, which makes a cost model reading the contract convict the correct construction. A wall whose RED is unauthorable for its own motivating case is DESIGN §4b's decoration.

What landed instead (operator ruling: extend the home, don't mint a second vocabulary)

• dag/std/algebra.dag gains the structured form beside CostShape: CostFactor over a named operand (constant / logarithmic / linear / linearithmic), CostTerm as a product of factors, StructuredCost as a sum of terms. CostShape stays, now as the projection of that expression (structured_cost_to_shape) for the sites that only need a rank. One home, two readings.
• The projection is partial and says so: a cost linear in two operands has no CostShape image, and the absent arm is the vocabulary gap stated out loud rather than a rounded rank presented as the operation's shape.
• dag/std/realization_cost_fidelity.dag joins modeled to realized per operand, and consumes std.pareto (axis_comparison_int, dominance_of_comparisons) instead of restating dominance — DESIGN §3d, "growing a second decision algebra beside Pareto is the fork this law exists to prevent". It therefore inherits Pareto's separation of Incomparable from DominanceUndecided, which is precisely the distinction a cost report must not lose.
• An operand named by only one side is not a missing axis: its rank on the other side is 0, which is the true statement that the cost does not grow in it. That is what makes "declares work in both operands, realizes work in one" come out as a difference.

Five arms where the brief asked for four — both additions stated

• RealizationDivergesByOperand — a proven trade-off (cheaper in one operand, dearer in another) is a finding, not an absence; collapsing it into Unknown would report "nothing to see" about two established facts (§5 absorbing fallback).
• ModeledCostNotStructured — the counted migration frontier for contracts not yet restated in the structured form. Omitting those rows would shrink the denominator by exactly the unmigrated population.
• RealizationCostUnknown stays reachable only from a missing realization fact, never as the answer to a comparison.

Evidence, by execution

claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/realization_cost_fidelity_witness_test.dag — 8 green, led by the specimen:

• concat_model_over_prices_the_left_operand — modeled over both operands vs realized over the right one → RealizationFasterThanModeled (the model over-prices the left operand)
• the_rank_only_reading_cannot_see_the_concat_divergence — the discriminator kept in the corpus rather than in this description: read as a rank, the two costs are indistinguishable. That is the reading the briefed join would have produced, and it is the argument for why the structured form had to land first.
• plus slower / preserved / per-operand-trade-off, and the counting split across measured, unmeasured, and unmigrated so a single count cannot flatten three states into one green.

Not carried, declared rather than implied

The row population. Asserting a realized cost for a primitive without measuring the emitted compiler would be the fabricated fact this authority exists to catch, so rows land with the measurement (step 4c). The contracts' migration to the structured form is the trigger that retires ModeledCostNotStructured.

dag/std is a closure source, so this needs its own head-bound closure receipt and queues behind #11004.

🤖 Generated with Claude Code

https://claude.ai/code/session_01RPVTQBSK9E8j3UDQGPZN1f

[gunbai-bot]

Conformance note, now that DESIGN §3b carries a decision/selection domain (#11010, landed after this branch was cut): that row's home authorities include std.pareto::DominanceVerdict, and this change inhabits it rather than forking it. The per-operand comparison builds AxisComparison values and hands them to std.pareto dominance_of_comparisons; it declares no dominance vocabulary of its own, no second axis-orientation rule, and no evidence-gap arm beside Pareto's. CostFidelity's five arms are a projection of the verdict Pareto returns — Dominates/Dominated/Equivalent/Incomparable map one-to-one onto faster/slower/preserved/diverges-by-operand — plus two arms Pareto has no opinion about: a missing realization fact, and a model not yet restated in the structured form.

Stating it here because the domain's whole point is that the answer is three-valued and the middle value has to be said out loud: this is conforms, not a stated divergence.

Worth one more line on what that inheritance bought, since it is the part I would otherwise have had to argue for: Pareto's separation of Incomparable from DominanceUndecided is exactly the distinction a cost report must not lose. A realization cheaper in one operand and dearer in another is a proven trade-off — two established facts — and reporting it as "undecided" or folding it into RealizationCostUnknown would be the §5 absorbing fallback, reading as "measured, nothing to report" while meaning "measured, and the two disagree". Consuming the existing algebra made that come out right by construction rather than by my remembering to write it.

— sent from calm-crane-722

[gunbai-bot]

Both findings in review 63523 verified and fixed in 7a6de6b17c9. The first one is the better catch of the two and I want to say why.

1. The projection rounded — inside the function whose own annotation forbids rounding. rank 1 is logarithmic in the operand, CostShape has no logarithmic spelling, and shape_for_single_operand_rank answered ShapeConstant for it: a cost that grows, reported as one that does not. Three lines above it the comment says a rounded rank presented as the operation's shape is "the fabricated answer this whole authority exists to prevent". I wrote the rule and then broke it in the implementation of the rule — which is exactly the shape this module is about, one level up. It answers absent now, like every other cost CostShape cannot say.

Two witnesses keep it executed rather than asserted: logarithmic_cost_has_no_shape_and_does_not_round_to_constant (must not project) and linear_and_sorting_single_operand_costs_still_project (so the absent arm is a statement about the vocabulary, not a projection that gave up).

2. The frontier was in the PR body, not in the diff — which §3c names as a tell in so many words ("consumption described in the PR body but absent from the diff"). Correct, and the fix is in the module rather than here:

• Consumer: the compile-obligation census's realization-cost-fidelity row — the row the census reports as having no home — joined per (primitive, target) through realization_cost_fidelity_rows, with count_cost_fidelity_findings / count_cost_fidelity_unmeasured / count_cost_model_unmigrated as its three reported populations.
• Route: the census entry point folds std.primitive_identity's modeled costs against RealizationCostFact rows measured from the emitted compiler.
• Trigger, a capability rather than an artifact: the emitted compiler being measurable per primitive, so a realized cost is an observation rather than an assertion. ModeledCostNotStructured gets its own smaller trigger — migrating std.primitives contract costs into StructuredCost.

The module also records why there are deliberately no RealizationCostFact rows yet: hand-authoring one would make the model and the realization agree by construction, which is the precise failure this join exists to make impossible. And it states what a green run means today — the arms are proven against authored costs, and the population this will judge does not exist yet.

On std.primitive_identity:303 still carrying cost: CostShape and src/v1/complexity.dag still reading it: that is intended and is the un-migrated side of the same frontier. CostShape remains the rank projection for sites that only need a rank; rewiring those consumers is the contract migration named as the second trigger, not a hunk this PR should carry.

— sent from calm-crane-722

[gunbai-bot]

Both findings verified and fixed in 934671fd3b4. The first one is the same defect as last round, one level deeper, and your framing of it is what made the repair obvious.

1. The rank arithmetic collided, and a collision has no refusal door. You are right that this is not hypothetical — CostTerm.factors is unconstrained, so {Log{n}, Log{n}} is representable today, and it scored 2, identical to a single Linear{n}. Consequences exactly as you traced them: structured_cost_to_shape projected log²n as ShapeLinearScan, and cost_fidelity_of(modeled: log²n, realized: n) answered CostShapePreserved. A real divergence reported as preserved, by the module built to make that impossible. The observation that the _ => none arm proves refusal was available while a collided rank offers no such door is the sharpest part of the finding: the bug is not the wrong number, it is that a collapsed encoding cannot refuse.

So growth stops being an ordinal. A cost in an operand is n^degree · (log n)^logs — two numbers — carried as OperandGrowth { degree, logs }, multiplied within a term (a term is a product, so the exponents add, separately) and maxed across terms under a lexicographic order, which is the true order of those functions: n beats (log n)^k for every k. The projection follows: CostShape can say exactly constant, linear and linearithmic in one operand; logarithmic, quadratic and log-squared each answer absent rather than rounding.

The axis comparison moves from axis_comparison_int to axis_comparison(goal, value_order:). std.pareto still owns dominance — supplying the ordering of a growth rate is this authority's own job, and the pair is what made an Int comparison the wrong shape.

2. Target equality minted a second naming scheme. Correct, and it is the §3 violation in miniature: three arms the type already names, given string names so they could be compared. realization_target_eq is a structural match now, which also fails in the right direction — a fourth target stops the match compiling, whereas a slug table would silently answer "not equal" for the arm someone forgot to add.

Three new controls, thirteen green: log_squared_and_linear_do_not_collide (must be RealizationSlowerThanModeled), log_squared_has_no_shape, quadratic_in_one_operand_has_no_shape.

Worth saying plainly: two rounds in a row, the defect was in an arm my own witnesses did not exercise, in a module whose subject is fabricated cost answers. The controls are now written from the vocabulary's combinations rather than from the cases I happened to think of.

— sent from calm-crane-722

[gunbai-bot]

review 63577 found a real §3 fork and I took the deeper of its two proposed repairs. Fixed in b8f889da7a3.

The finding, restated so the record is clear: CostShape is not a pure growth vocabulary. ShapeIterateBody means "once per element × whatever the caller's body costs", and it is the cost std.primitive_identity carries today for fold_list and index_by (:759,764). StructuredCost had no factor for that, so on migration those primitives could only be written LinearInOperand, and shape_for_operand_growth would project them back as ShapeLinearScan — a different arm of the same authority, silently. ShapeIterateBody had no preimage, ShapeLinearScan had two. Both halves of your citation land: two names answering one question and disagreeing, and the rounding the annotation two lines above forbids.

Why the modelling fix rather than "refuse the linear case too": refusing linear would leave ShapeIterateBody permanently unreachable and the projection nearly vacuous (constant and linearithmic only), and it would treat a real fact — that a caller-supplied body runs per element — as noise. So:

• CostFactor gains CallerBodyPerElementIn { operand }; OperandGrowth gains a bodies count.
• The body is deliberately not an exponent. It multiplies work without changing growth in the operand, so it counts separately and the order stays over (degree, logs).
• An axis whose growths agree and whose bodies differ is therefore UndecidedOnEvidence — std.pareto's own word — because the body may be O(1). Calling it Same hides a real difference; calling it worse invents one.
• That lands as a sixth arm, RealizationCostBodyDependent, not folded into RealizationCostUnknown, which stays reachable only from a missing fact. This is the part your finding forced and I want to name it: without the new arm, an undecided-on-evidence comparison would have reported "not measured" about something that was measured.
• The projection is now total with exactly one preimage per arm: (0,0,0) constant, (1,0,1) iterate-body, (1,0,0) linear-scan, (1,1,0) sort-body.

Three new controls, sixteen green: iterate_body_and_linear_scan_project_to_different_arms (the two that used to collide), a_per_element_body_difference_is_undecided_not_preserved, a_body_does_not_outrank_a_real_growth_difference.

This is the third round on this module where the defect sat in a combination the vocabulary admitted and no witness constructed — the pattern is filed as two receipts on check_subject_narrower_than_its_declared_claim in #11031, and this round is the same shape found from the other end: not a combination of my factors, but an arm of the vocabulary I was projecting into that nothing could reach.

— sent from calm-crane-722

[gunbai-bot]

Both findings verified and fixed in b90cdb7d2ae. Both are arms I introduced and did not enumerate, which is now the fourth round of that on this module.

1. The body count was dropped by a growth-dominated term. Traced exactly as you describe: operand_growth_max returned the winning term's OperandGrowth whole and consulted bodies only on an Equal tie, so modeled [n·n] against realized [n·n, body(n)] both collapsed to (2,0,0), operand_axis_comparison answered Same, and cost_fidelity_of answered CostShapePreserved — for a realization that runs a caller-supplied body per element where the model runs none. Authorable today, as you note, since the witness already authors multi-term costs.

The repair is the argument you make: a cost is a sum, so growth in an operand comes from the largest term, but a body is a fact about the cost, not about the winning term. Growth comes from the ordering; bodies is maxed independently — exactly as degree and logs are carried separately rather than summed. That the defect lived in the function written to keep those facts apart is the part worth recording.

2. RealizationCostBodyDependent was counted in no reported population. Correct, and it is the quieter half of the same defect. The arm exists so a measured-but-undecided comparison is not read as preserved; being invisible in all three counts the declared consumer reports defeats it just as completely. It is not a finding (nothing is established about which side is worse), not unmeasured (both costs are known), not unmigrated (both are structured) — so it gets its own population, count_cost_body_dependent, and the module's consumer statement now names four populations.

Two new controls, eighteen green: a_body_in_a_losing_term_is_not_dropped, and the_undecided_arm_appears_in_a_reported_population — the second asserts all four counts on one ledger at once, so the type cannot gain an arm again without the accounting being revisited in the same breath.

One thing this round taught that the previous three did not, and I would rather write it down than repeat it: adding an arm to a coproduct is not finished when the arm is reachable — it is finished when every fold over that type has been revisited. The match arms fail loudly when a variant is added; the counting folds accept the new arm and silently exclude it from every population. Those are the folds that need looking at, and they are the ones that look fine.

— sent from calm-crane-722

[gunbai-bot]

Investigated. This one is mine and real — not the toolchain deleter and not the D1/G parse family — but it is not fixable on this head today, and I am not pushing because this PR is held under the D-train no-push rule.

The failure: required-ci: generated-artifact population=stage0-mirrors FAIL generated surface drift: std_algebra.rs, with first_generation_equal=false. src/v1/stage0/src/std_algebra.rs is the generated stage0 mirror of dag/std/algebra.dag, this PR edits that authority, and the mirror was never regenerated with it. regen-fixed-point fixed_point_equal=true, so generation is stable — the candidate simply differs from what is committed, which is exactly what that population exists to catch.

For the record on the other job: the $HOME differs from euid-obtained home directory lines in this run are rustup's notice and appear on green jobs too, so they are not the deleter signature; cargo/bin/cargo exists=no at phase=start on srv1-14 is the pre-isolation reading, not a mid-job disappearance. Nothing here needs a rerun.

Why the fix waits, and what it will be. The head that failed (b90cdb7) predates the rebuild that review 63628 required: CostFactor / CostTerm / StructuredCost are deleted from std.algebra and the structured form now lives in std.induction CostBound. That changes which mirrors drift — std_algebra.rs moves back toward its baseline and std_induction.rs becomes the one carrying new surface — so regenerating against this head would produce an artifact for content that is already superseded locally.

So the regeneration belongs to the un-hold step, against the rebuilt content, in one push: remerge main, regenerate the stage0 mirrors from the merged authorities, push once. Worth noting the mirror regen needs a cgroup-bound host (the producer-driven regen panics HostBudgetUnreadable where no cgroup binds it), so it is a srv1/srv2 run rather than something I can produce from this session's container.

The general point this raises for the queue, since I am not the only lane touching dag/std: editing a .dag authority that has a stage0 mirror creates a second obligation in the same change, and nothing in the local witness path says so — claim_batch was green on this content throughout. The floor is the only thing that knows.

— sent from calm-crane-722

[gunbai-bot]

Fixed in d5da126745e, and both findings in review 63797 were reproduced by execution before I touched anything:

cost_fidelity_of(modeled: cost_linear("n"), realized: cost_sqrt("n"))  ->  RealizationFasterThanModeled
cost_fidelity_of(ForeverBound, ConstantBound)                         ->  CostShapePreserved

√n reported as cheaper than n; unbounded work reported as preserving a constant. Your diagnosis of the cause is exact: ParamGrowth carries representable, the projection consults it, and param_growth_order compares only (degree, logs) — so an unrepresentable growth was ordered as (0,0). The module's own annotation says a reader reporting constant or linear for such a bound "would be fabricating"; the join did it three lines of indirection away.

ForeverBound needed a second look and changed the shape of the fix. It names no parameters at all, so the axis list was empty, and an empty axis list is Equivalent in std.pareto. "No axes" and "no difference" are not the same fact — which is why orderability had to become a property of the whole bound (cost_bound_is_orderable) rather than a per-parameter flag: a bound with no parameters has no per-parameter flag to carry.

CostGrowthNotOrderable is its own arm, not overloaded onto RealizationCostBodyDependent, exactly as you asked. They are different ignorances with different repairs: body-dependent means both costs are known and their order turns on an unmodelled body; not-orderable means this reading cannot place a bound on the lattice at all. Folding them together would send a reader to model a body cost when the real gap is a fractional exponent.

The arm is counted (count_cost_not_orderable, a fifth reported population) and every existing fold over CostFidelity was revisited — this module shipped a reachable arm that no count reported two rounds ago, and that is the rule that came out of it.

Five new controls, twenty-four green. One of them is there for a reason worth naming: two_constants_still_compare_as_preserved, so the gate is about orderability rather than about having no parameters. Without it I would have no evidence I hadn't simply broken the constant case while fixing ForeverBound.

Separately, for whoever reads this next: the stage0-mirrors drift on the prior head is std_induction.rs (the rebuild moved the surface out of std.algebra), and heal-generated-artifacts went green beside it without regenerating it — heal does not cover stage0 mirrors, so that regeneration is a separate step against this head.

— sent from calm-crane-722

[gunbai-bot]

Review 63818, both findings verified against the head they were raised on and both fixed in b376035.

Finding 1 — ParamGrowth.representable is an in-band sum. Correct, and the diagnosis of the causal chain is correct too: param_growth_order compared (degree, logs) while the flag sat unused, which is exactly how sqrt(n) came to order cheaper than n and ForeverBound came to compare equal to a constant. The gate I added last round catches both after the illegal comparison is written — validation standing where construction was available (DESIGN §5).

Declared as the coproduct:

type GrowthRank { degree: Int, logs: Int, bodies: Int }
type ParamGrowth = OrderableGrowth { rank: GrowthRank } | GrowthNotOrderable
fn param_growth_order(a: GrowthRank, b: GrowthRank) -> Ordering

The order takes a rank, not a growth, so a caller holding an unplaceable growth has nothing to pass it — the comparison is unwritable rather than refused. It found a live caller on its first run: the existing witness the_rank_only_reading_cannot_see_the_concat_divergence was handing two ParamGrowth values straight into param_growth_order, and the module refused it by type. The flag had been sitting beside that call the whole time.

atomic_cost_is_orderable is now derived from the growth arm instead of re-spelling the exponent match beside it. cost_bound_is_orderable stays and the annotation now says why it is not the parallel gate you flagged: a bound with no parameters yields no per-parameter growth at all, and ForeverBound is exactly that shape, so no axis exists to carry the refusal. That residue is what it covers. std.realization_cost_fidelity follows — the axis comparison is AxisComparison? and the fold absorbs into CostGrowthNotOrderable rather than rendering an unplaceable axis as UndecidedOnEvidence, which is a different ignorance with a different repair.

Finding 2 — the census row asserts NoHomeExists after this PR authors the join. Correct; the payload was false at that head. nearest now points at std.realization_cost_fidelity cost_fidelity_of, and the reason and trigger state what is actually still missing rather than what has landed: the join exists but has no observer — nothing in the corpus reads a cost bound off an emitted realization, so it can never be given its realized operand, and the home remains wherever a target realization is selected. Kept as NoHomeExists rather than promoted to HomeAuthority for that reason.

Five new controls on the arms (a_fractional_exponent_growth_has_no_rank, an_unbounded_growth_has_no_rank, a_linear_growth_has_a_rank, an_unorderable_factor_absorbs_the_whole_bound, an_unorderable_growth_projects_to_no_shape); 29 witnesses green. Per DESIGN §4b(4) the two original fabrication controls stay enrolled even though the ordering that produced them is now unwritable.

The remaining red on this PR is the std_induction.rs stage0 mirror, which is being regenerated off-session at this head.

— sent from calm-crane-722

[gunbai-bot]

Review 63838, both findings, fixed in a5087bd (on top of the regenerated std_induction.rs mirror).

Finding 1 — the body count is dropped whenever growth differs. Correct, and the reachable case you name is the one that matters most, because I had enrolled the wrong answer as a green witness. a_body_does_not_outrank_a_real_growth_difference asserted RealizationSlowerThanModeled for n × body(n) against n log n — a witness that encoded my reasoning instead of testing it, so it could only ever confirm what I already believed. With a body of O(n²) the modeled side is n³ and the realization is far faster. The mirror direction you identify is the more dangerous one, because the wrong answer flatters the realization.

The repair is one rule replacing two rather than a new arm beside the old one:

the axis is decided exactly when the body delta agrees with the growth delta or is zero, and is UndecidedOnEvidence when they oppose.

That subsumes the equal-growth case — growths equal with bodies differing is opposition at a growth delta of zero — so rank_axis_comparison got smaller, not larger. param_growth_order still ranks on (degree, logs) alone, which stays right: an unbounded body has no position on that lattice. What follows from that is not "ignore it" but "consult it beside the order", which is what the annotation now says.

Three controls, and they discriminate against each other by construction:

• an_opposing_body_and_growth_delta_is_body_dependent — the flipped one, red under the old rule (which answered Slower)
• an_opposing_body_does_not_make_a_realization_faster — your mirror case, red under the old rule (which answered Faster)
• an_agreeing_body_and_growth_delta_stays_decided — red if the repair over-corrects into a blanket UndecidedOnEvidence

Passing all three is only possible under the intended rule. 31 witnesses green.

Finding 2 — the stale arm count in the annotation. Correct, and deleted rather than corrected. §4c says an annotation must not restate what the declaration structurally says, and a count of arms is exactly that restatement — which is why it could drift. The paragraph now points at the declaration instead of counting it.

The remaining CI red at the previous head was the std_induction.rs stage0 mirror; that is regenerated and in this head.

— sent from calm-crane-722

[gunbai-bot]

srv2 closure receipt for #11026 at head a5087bd (overlay on main 44a0467; instrument closure_pr.sh, pinned producer claim_executor_pinned built from the overlay, route --v2-native-route --source-root dag --source-root src/v2).

Regressed files vs the main baseline (closure_main.sh at 199aee7; 29 refusals): none. Stage shifts: none.

• Emitted closure: 172 files, digest a4c50c9b823b… (changed from main's c17ed878…, as expected: dag/std/induction.dag and dag/std/realization_cost_fidelity.dag are closure members). Emitted binary sha256 d374b5c07e19be0d.
• Closure root 167 modules; native fold EXIT=0, _terminal: complete, wall 316 s, rss 1.24 GB.
• After-set: 29 file refusals (28 parse_g0_tokens_remain, 1 normalize_reason_post_normalize_not_well_formed on src/v2/std/runtime.dag), joined by path against the baseline's 29: 0 new, 0 cleared.

Receipt-neutral by execution; the regenerated std_induction.rs mirror (15be6be) is on this head. Nothing blocks landing on the closure side.

[gunbai-bot]

srv2 closure receipt at head 3bb39e8 (overlay of this PR's diff on main f583087, pinned producer, native fold over the 167-module closure of src/v2/compiler/00_compile.dag):

• after-set: 14 rows, identical to the main baseline at f583087 (13 parse_g0_tokens_remain + 1 normalize on src/v2/std/runtime.dag). Regressed: none. Fixed: none.
• closure manifest: 167 modules, identical to main (no new closure-member import).

Instrument: closure_pr.sh 11026 on srv2 (p-11026/refusals_after.txt, p-11026/manifest.txt).

— sent from eager-raven-113