diff --git a/dsl/extdeps/accounting/budget.dag b/dsl/extdeps/accounting/budget.dag
new file mode 100644
index 00000000000..a330f69ca8d
--- /dev/null
+++ b/dsl/extdeps/accounting/budget.dag
@@ -0,0 +1,77 @@
+module extdeps.accounting.budget
+
+import std.measure { Measure, measure_add, measure_le }
+import extdeps.external_authority { ExternalAuthority }
+import extdeps.uri { Uri, Https }
+
+data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority {
+  uri: Uri {
+    scheme: Https
+    locator: "en.wikipedia.org/wiki/Budget"
+  }
+}
+
+type BudgetingMethod = ZeroBased | Incremental | ActivityBased
+
+type Appropriation<Q, S> {
+  ceiling: Measure<Q, S, Nat>
+}
+
+type LineItem<Q, S> {
+  purpose: String
+  amount: Measure<Q, S, Nat>
+}
+
+type BudgetBalance = Surplus | Balanced | Deficit
+
+fn line_items_total<Q, S>(items: List<LineItem<Q, S>>) -> Measure<Q, S, Nat> {
+  fold(items, init: Measure { count: 0 }, f: (acc, it) => measure_add(a: acc, b: it.amount))
+}
+
+fn within_appropriation<Q, S>(appropriation: Appropriation<Q, S>, items: List<LineItem<Q, S>>) -> Bool {
+  measure_le(a: line_items_total(items: items), b: appropriation.ceiling)
+}
+
+fn budget_balance<Q, S>(appropriation: Appropriation<Q, S>, items: List<LineItem<Q, S>>) -> BudgetBalance {
+  let spent = line_items_total(items: items)
+  let ceiling = appropriation.ceiling
+  return if measure_le(a: spent, b: ceiling) {
+    if measure_le(a: ceiling, b: spent) { Balanced } else { Surplus }
+  } else {
+    Deficit
+  }
+}
+
+type AdmissionState<Q, S> {
+  appropriation: Appropriation<Q, S>
+  committed: List<LineItem<Q, S>>
+  used: Measure<Q, S, Nat>
+  refused: List<LineItem<Q, S>>
+}
+
+fn admit_line_item<Q, S>(st: AdmissionState<Q, S>, candidate: LineItem<Q, S>) -> AdmissionState<Q, S> {
+  let next_used = measure_add(a: st.used, b: candidate.amount)
+  return if measure_le(a: next_used, b: st.appropriation.ceiling) {
+    AdmissionState {
+      appropriation: st.appropriation,
+      committed: concat(st.committed, [candidate]),
+      used: next_used,
+      refused: st.refused
+    }
+  } else {
+    AdmissionState {
+      appropriation: st.appropriation,
+      committed: st.committed,
+      used: st.used,
+      refused: concat(st.refused, [candidate])
+    }
+  }
+}
+
+fn admit_all<Q, S>(appropriation: Appropriation<Q, S>, candidates: List<LineItem<Q, S>>) -> AdmissionState<Q, S> {
+  fold(
+    candidates,
+    init: AdmissionState { appropriation: appropriation, committed: [], used: Measure { count: 0 }, refused: [] },
+    f: admit_line_item
+  )
+}
diff --git a/dsl/product/budget_tree.dag b/dsl/product/budget_tree.dag
new file mode 100644
index 00000000000..3077def803f
--- /dev/null
+++ b/dsl/product/budget_tree.dag
@@ -0,0 +1,104 @@
+module product.budget_tree
+
+import std.measure { ByteSize, byte_size, measure_add, measure_le, Memory, One }
+import extdeps.accounting.budget {
+  Appropriation, LineItem, BudgetBalance, Surplus, Balanced, Deficit,
+  line_items_total, within_appropriation, budget_balance,
+  BudgetingMethod, ZeroBased,
+  AdmissionState, admit_all
+}
+
+type BudgetPriority = Guaranteed | Burstable | BestEffort
+
+type BudgetClaim {
+  item: LineItem<Memory, One>
+  priority: BudgetPriority
+}
+
+type BudgetNode {
+  name: String
+  appropriation: Appropriation<Memory, One>
+  claims: List<BudgetClaim>
+  children: List<BudgetNode>
+}
+
+data budget_tree_method: BudgetingMethod = ZeroBased
+
+fn claim_items(claims: List<BudgetClaim>) -> List<LineItem<Memory, One>> {
+  map(claims, c => c.item)
+}
+
+fn child_as_line_item(child: BudgetNode) -> LineItem<Memory, One> {
+  LineItem { purpose: child.name, amount: child.appropriation.ceiling }
+}
+
+fn node_commitments(node: BudgetNode) -> List<LineItem<Memory, One>> {
+  concat(claim_items(claims: node.claims), map(node.children, child_as_line_item))
+}
+
+fn node_balance(node: BudgetNode) -> BudgetBalance {
+  budget_balance(appropriation: node.appropriation, items: node_commitments(node: node))
+}
+
+fn node_conserves_local(node: BudgetNode) -> Bool {
+  within_appropriation(appropriation: node.appropriation, items: node_commitments(node: node))
+}
+
+fn node_conserves(node: BudgetNode) -> Bool {
+  node_conserves_local(node: node) && all(node.children, c => node_conserves(node: c))
+}
+
+fn admit_claims(node: BudgetNode) -> AdmissionState<Memory, One> {
+  admit_all(appropriation: node.appropriation, candidates: claim_items(claims: node.claims))
+}
+
+type Reconciliation =
+    AllSatisfied { realized: List<BudgetClaim> }
+  | Evicted { kept: List<BudgetClaim>, evicted: List<BudgetClaim> }
+  | GuaranteedShortfall { shortfall: ByteSize }
+
+fn claims_of_priority(claims: List<BudgetClaim>, p: BudgetPriority) -> List<BudgetClaim> {
+  filter(claims, c => c.priority == p)
+}
+
+fn ordered_by_priority(claims: List<BudgetClaim>) -> List<BudgetClaim> {
+  concat(
+    claims_of_priority(claims: claims, p: Guaranteed),
+    concat(
+      claims_of_priority(claims: claims, p: Burstable),
+      claims_of_priority(claims: claims, p: BestEffort)
+    )
+  )
+}
+
+type AdmitState {
+  used: ByteSize
+  kept: List<BudgetClaim>
+  evicted: List<BudgetClaim>
+}
+
+fn reconcile(node: BudgetNode, actual: ByteSize) -> Reconciliation {
+  let ordered = ordered_by_priority(claims: node.claims)
+  let final_state = fold(
+    ordered,
+    init: AdmitState { used: byte_size(count: 0), kept: [], evicted: [] },
+    f: (st, c) =>
+      if measure_le(a: measure_add(a: st.used, b: c.item.amount), b: actual) {
+        AdmitState {
+          used: measure_add(a: st.used, b: c.item.amount),
+          kept: concat(st.kept, [c]),
+          evicted: st.evicted
+        }
+      } else {
+        AdmitState { used: st.used, kept: st.kept, evicted: concat(st.evicted, [c]) }
+      }
+  )
+  let evicted_guaranteed = claims_of_priority(claims: final_state.evicted, p: Guaranteed)
+  return if evicted_guaranteed.length() > 0 {
+    GuaranteedShortfall { shortfall: line_items_total(items: claim_items(claims: evicted_guaranteed)) }
+  } else if final_state.evicted.length() > 0 {
+    Evicted { kept: final_state.kept, evicted: final_state.evicted }
+  } else {
+    AllSatisfied { realized: final_state.kept }
+  }
+}
diff --git a/dsl/std/measure.dag b/dsl/std/measure.dag
index 31fbbabf171..1b18f02b033 100644
--- a/dsl/std/measure.dag
+++ b/dsl/std/measure.dag
@@ -124,6 +124,14 @@ fn measure_scale_fraction_ceil<Q, S>(m: Measure<Q, S, Nat>, num: Nat, den: Nat)
   Measure { count: if den == 0 { m.count * num } else { ((m.count * num) + (den - 1)) / den } }
 }
 
+fn measure_add<Q, S>(a: Measure<Q, S, Nat>, b: Measure<Q, S, Nat>) -> Measure<Q, S, Nat> {
+  Measure { count: a.count + b.count }
+}
+
+fn measure_le<Q, S>(a: Measure<Q, S, Nat>, b: Measure<Q, S, Nat>) -> Bool {
+  a.count <= b.count
+}
+
 fn time_measure<S>(count: Nat) -> Measure<Time, S, Nat> {
   Measure { count: count }
 }
diff --git a/dsl/test/claim/budget_tree_witness_test.dag b/dsl/test/claim/budget_tree_witness_test.dag
new file mode 100644
index 00000000000..bb69970db9c
--- /dev/null
+++ b/dsl/test/claim/budget_tree_witness_test.dag
@@ -0,0 +1,110 @@
+module test.claim.budget_tree_witness
+
+import std.logic { Bool }
+import std.measure { byte_size, Memory, One }
+import extdeps.accounting.budget {
+  Appropriation, LineItem, BudgetBalance, Surplus, Balanced, Deficit,
+  BudgetingMethod, ZeroBased, within_appropriation, admit_all, AdmissionState
+}
+import product.budget_tree {
+  BudgetNode, BudgetClaim, BudgetPriority, Guaranteed, BestEffort,
+  Reconciliation, AllSatisfied, Evicted, GuaranteedShortfall,
+  node_conserves, node_conserves_local, node_balance, reconcile,
+  claim_items, budget_tree_method
+}
+
+fn claim(name: String, amount: Nat, p: BudgetPriority) -> BudgetClaim {
+  BudgetClaim { item: LineItem { purpose: name, amount: byte_size(count: amount) }, priority: p }
+}
+
+fn appr(n: Nat) -> Appropriation<Memory, One> {
+  Appropriation { ceiling: byte_size(count: n) }
+}
+
+fn sample_claims() -> List<BudgetClaim> {
+  [
+    claim(name: "g1", amount: 40, p: Guaranteed),
+    claim(name: "g2", amount: 40, p: Guaranteed),
+    claim(name: "b1", amount: 30, p: BestEffort)
+  ]
+}
+
+fn leaf_node(cap: Nat) -> BudgetNode {
+  BudgetNode { name: "host", appropriation: appr(n: cap), claims: sample_claims(), children: [] }
+}
+
+fn child_node(cap: Nat) -> BudgetNode {
+  BudgetNode { name: "c", appropriation: appr(n: cap), claims: sample_claims(), children: [] }
+}
+
+fn root_with(child: BudgetNode) -> BudgetNode {
+  BudgetNode { name: "root", appropriation: appr(n: 200), claims: [], children: [child] }
+}
+
+fn is_all_satisfied(r: Reconciliation) -> Bool {
+  match r { AllSatisfied { realized: x } => true  _ => false }
+}
+
+fn is_evicted(r: Reconciliation) -> Bool {
+  match r { Evicted { kept: k, evicted: e } => true  _ => false }
+}
+
+fn is_guaranteed_shortfall(r: Reconciliation) -> Bool {
+  match r { GuaranteedShortfall { shortfall: s } => true  _ => false }
+}
+
+fn witness_conservation_residue_lens() -> Bool {
+  node_conserves_local(node: leaf_node(cap: 120)) && !node_conserves_local(node: leaf_node(cap: 100))
+}
+
+fn witness_tree_conservation_recursive() -> Bool {
+  node_conserves(node: root_with(child: child_node(cap: 120)))
+    && !node_conserves(node: root_with(child: child_node(cap: 100)))
+}
+
+fn witness_divide_once() -> Bool {
+  let two_children = [child_node(cap: 100), child_node(cap: 100)]
+  let tight = BudgetNode { name: "r", appropriation: appr(n: 150), claims: [], children: two_children }
+  let roomy = BudgetNode { name: "r", appropriation: appr(n: 250), claims: [], children: two_children }
+  return !node_conserves_local(node: tight) && node_conserves_local(node: roomy)
+}
+
+fn witness_admission_is_construction() -> Bool {
+  let admitted = admit_all(appropriation: appr(n: 90), candidates: claim_items(claims: sample_claims()))
+  return within_appropriation(appropriation: appr(n: 90), items: admitted.committed)
+    && admitted.refused.length() > 0
+}
+
+fn witness_balance_states() -> Bool {
+  (node_balance(node: leaf_node(cap: 200)) == Surplus)
+    && (node_balance(node: leaf_node(cap: 110)) == Balanced)
+    && (node_balance(node: leaf_node(cap: 100)) == Deficit)
+}
+
+fn witness_reconcile_all_satisfied() -> Bool {
+  is_all_satisfied(r: reconcile(node: leaf_node(cap: 120), actual: byte_size(count: 120)))
+}
+
+fn witness_reconcile_evicts_best_effort() -> Bool {
+  is_evicted(r: reconcile(node: leaf_node(cap: 120), actual: byte_size(count: 90)))
+}
+
+fn witness_reconcile_guaranteed_shortfall() -> Bool {
+  is_guaranteed_shortfall(r: reconcile(node: leaf_node(cap: 120), actual: byte_size(count: 50)))
+}
+
+fn witness_method_is_zero_based() -> Bool {
+  budget_tree_method == ZeroBased
+}
+
+test fn budget_tree_holds() -> Bool {
+  witness_conservation_residue_lens()
+    && witness_tree_conservation_recursive()
+    && witness_divide_once()
+    && witness_admission_is_construction()
+    && witness_balance_states()
+    && witness_reconcile_all_satisfied()
+    && witness_reconcile_evicts_best_effort()
+    && witness_reconcile_guaranteed_shortfall()
+    && witness_method_is_zero_based()
+}