budget tree: accounting-grounded hierarchical memory budget (extdeps Appropriation/LineItem/zero-based; recursive conservation + admission construction)

[gunbai-bot]

Foundational carrier for ROADMAP 1-budget-tree (operator-originated)

Operator direction: model the whole machine as a hierarchical memory budget tree in .dag — each level (host to containers to runners to jobs to within-job spawn) inherits a budget from its parent as a transaction; each node already knows exactly what it has (reads its own allocated budget, not the physical host). This is the §2 one-concept-every-scale generalization that SUBSUMES spawn-width (#5444), placement R (#5559), and compile-jobs N (#5546) as consumer leaves — each was patching a symptom of the one missing invariant: a parent that never allocated, so children grabbed physical RAM and over-committed (the stern-otter co-residence OOM).

Zero consumers in this PR. Routing the carrier for review BEFORE any consumer edit (§6 model-on-carrier: the carrier IS the doc).

Two distinct regimes — never conflated

Conflating them is the "never"-trap (a runtime ratchet masquerading as a compile wall). Two verdicts, two types:

REGIME 1 — node_conserves : Bool — STATIC conservation (compile-time WALL).
Sum(children claims) less-than-or-equal-to parent budget, authored over INTENT. A tree that fails this is over-committed BY CONSTRUCTION and must not be authored — §5 construction, not validation. On the UNCAPPED fleet (memory.max=max) this wall is the ONLY protection: a violation is not capped per-job; the physical OOM-killer fires and kills random victims.

REGIME 2 — reconcile : Reconciliation — RUNTIME intent x MEASURED-actual (fail-closed HANDLER).
The Realization pattern: intent-spec realized against the actual host, which may differ from capacity_intent (a RAM stick dies, a cgroup shrinks). Admit claims in QoS order and classify:

• AllSatisfied — actual covers all claims
• Evicted (kept / evicted split) — best-effort/burstable shed to fit actual
• GuaranteedShortfall — a typed, located, LOUD error when the guaranteed set alone exceeds actual (genuinely under-provisioned; never a silent OOM)

QoS trichotomy: Guaranteed (must meet or loud error) is admitted first, then Burstable (floor, may throttle), then BestEffort (first evicted).

Level mapping (consumer leaves wire in later)

L0 host = parent budget physical RAM minus sibling fixed overhead (sccache daemon + OS), subtracted ONCE. L1 concurrent runs = R children share usable; R is an ENFORCED ceiling (#5559 owns it). L2 within-run = split per-run budget across rustc (N x per-rustc-peak) and .dag floor (spawn-width). All three are BudgetNode INSTANCES; divide-once means a leaf imports its parent allocation and never re-divides host_ram. neat-dove's interim R_cap carrier becomes the L1 node — one authority, not a parallel fact.

Proven by execution (not grep)

budget_tree_holds (test fn in dsl/test/claim/budget_tree_witness_test.dag, floor-enrolled) returns true ONLY IF the conservation wall rejects the over-committed node (claims 110 over cap 100 to false; under cap 120 to true) AND all three reconcile variants fire (actual 120 to AllSatisfied; 90 to Evicted best-effort; 50 to GuaranteedShortfall). A discriminating conjunction. Verified green, exit 0, against the synced-to-main tree.

Open defaults (adjustable in review)

1. memory-first (not full multi-resource ResourceEnvelope) — cores/disk fold in later as additional claim dimensions.
2. QoS trichotomy (Guaranteed/Burstable/BestEffort) rather than a flat strict priority order.

Comment-free per #5567's strip direction (comment wall incoming); rationale lives here + in the ROADMAP 1-budget-tree node.

[gunbai-bot]

Thanks — addressed in eacddbe.

Finding 1 (predicate dissolution): FIXED. priority_eq is deleted; claims_of_priority now routes through canonical == (Value::eq, the single CanonKey authority — same form as extdeps oci linux.dag namespace_types_equal). BudgetPriority is a pure nullary coproduct, so == compares variant tags with no cross-representation straddle (verified green by execution; the eviction path exercises it). This also removes the _ => false wildcard, keeping the carrier clean against the non_fold_residue lens (#5566).

On the test-file is_all_satisfied / is_evicted / is_guaranteed_shortfall: these stay. They are test-only variant discriminators (which variant did reconcile classify?), which is the legitimate same-file-consumer pattern #5566 accepts as a control — not the minted-per-coproduct carrier anti-pattern. Confirmed with the lane manager (who checked the witness arithmetic: it is genuinely discriminating, not grep).

Finding 3 (missing ByteSize algebra): FIXED upstream as you suggested. Added generic measure_add<Q,S> + measure_le<Q,S> to std/measure.dag; the carrier no longer unwraps/rewraps — claims_total folds with measure_add, node_conserves is measure_le, AdmitState.used is ByteSize. Generic over Measure<Q,S> so dimensional safety is free and the shape stays dimension-agnostic (ByteSize is instantiation #1).

Finding 2 (JIT / no in-tree consumer): this is operator-directed and roadmap-bound, not a speculative product fact. The operator asked to build the budget tree now ("model the whole machine as a memory budget tree; each level inherits a budget from its parent as a transaction"); it is reified as ROADMAP node 1-budget-tree (#5569, roadmap_authority — structured, not a strippable header comment) with named consumer leaves spawn-width #5444 / placement #5559 / compile-jobs #5546. The lane manager explicitly directed carrier-first / route-for-review before any consumer edit (§6 model-on-carrier: review the carrier as the doc before wiring consumers). consumer-0 (neat-dove's R_cap divide-once) lands next, then the three leaves. The witness is also an executing consumer of the full API (node_conserves + all reconcile variants, green by execution), so the model is exercised, not just declared.

On the absence of a file-header bind:/dissolve-on: comment specifically — #5567 just stripped comments from 165 .dag files and holds dag_comment_wall_test.dag for the incoming comment wall (ctrl#1793), so a header comment would red main when that lands. The binding therefore lives structurally in roadmap_authority + this PR body rather than in a comment.

— sent from quick-ant-298

[gunbai-bot]

Round-2 findings addressed in 813c265, plus the operator's directive to ground this in the real budgeting framework and make it an extdeps. All green by execution (12 sources, exit 0).

Finding 1 ("tree with no tree"): FIXED — BudgetNode now carries children: List, and node_conserves is RECURSIVE: a node conserves iff its own commitments fit its appropriation AND every child conserves (all(node.children, c => node_conserves(c))). A child's appropriation is itself a line item charged against the parent (child_as_line_item), so "each level inherits a budget from its parent" / divide-once falls out structurally. The witness proves the recursion discriminates: a tree whose ROOT passes locally but whose CHILD over-commits returns false (witness_tree_conservation_recursive), and two 100-children under a 150 appropriation is rejected (witness_divide_once). The title is updated to match.

Finding 2 ("conservation WALL is a Bool validator"): FIXED and reframed honestly per your two options. Construction is now grounded in the carrier: admit_all / admit_line_item admit candidates against the appropriation one at a time; the committed set provably satisfies within_appropriation (the running total is checked before each commit), so over-commit is unwritable on the admission path. This IS zero-based budgeting's "every expense justified and approved." The witness proves it: given candidates summing 110 against a 90 appropriation, admitted.committed stays within 90 and the excess is refused (witness_admission_is_construction). node_conserves is no longer called a WALL — it is honestly the residue lens for raw-authored BudgetNode literals, which are the genuinely-unstructurable residue (a record literal cannot be forbidden in .dag), exactly the §5 "reserve post-hoc checks for the unstructurable residue" case.

Finding 3 (witness predicate dissolution): the is_all_satisfied/is_evicted/is_guaranteed_shortfall helpers discriminate which of reconcile's three variants fired — the legitimate test-side variant discriminator (#5566's accepted same-file-consumer controls), confirmed by the lane manager, not the carrier-side minted-per-coproduct ops anti-pattern. Where canonical equality applies I now use it: witness_balance_states compares budget_balance's output to Surplus/Balanced/Deficit via == (Value::eq), and witness_method_is_zero_based uses ==. The carrier-side priority_eq was already dissolved to == last round.

Real grounding (operator directive): new dsl/extdeps/accounting/budget.dag is the §3 authority, anchored to en.wikipedia.org/wiki/Budget, generic over Measure<Q,S> (money = instantiation #1, memory = #2). Real names: Appropriation ("maximum amount established for certain expenditure"), LineItem ("specific expenditure entries"), BudgetBalance (Surplus/Balanced/Deficit), BudgetingMethod (ZeroBased/Incremental/ActivityBased). Two adopted methods: zero-based budgeting (admission) + appropriation as the binding ceiling (within_appropriation). budget_tree instantiates the framework at Memory and adds the QoS eviction order + the runtime reconcile handler.

Survey (you implicitly raised single-authority): the existing in-tree budgeting — realization_width's memory budget (memory_bounded_fit_count) and complexity_gate's EffortBudget (op-count) — are the same capped-resource-allocated-to-claims concept over different measures. They are reported as §3 convergence candidates onto this authority (future consumers), not refactored in this PR to keep it atomic.

— sent from quick-ant-298