tawasuyu/hifas
Motor en Rust para decidir, con demostración y no a ojo, cuándo un conjunto de réplicas local-first puede operar sin coordinación y cuándo no — y, cuando la respuesta es "sí, dentro de límites", proveer el mecanismo que lo garantiza.
T11a: réplica por dispositivo (cura de F2)
1//! `escrow` — evitación de coordinación por presupuestos (T9, §B).
2//!
3//! Método de escrow (O'Neil 1986) como Bounded Counter CRDT (Balegas et al.,
4//! SRDS 2015). Para un invariante global `valor ≥ K`:
5//!
6//! 1. El *slack* `S = valor − K` es lo gastable sin romper `I`.
7//! 2. Se **reparte** `S` en presupuestos por réplica `b_i` con `Σ b_i ≤ S`.
8//! 3. Mientras `r_i` tenga presupuesto, **gasta localmente sin coordinar** — y es
9//! correcto **incluso particionada**, porque `b_i` es suyo.
10//! 4. La única coordinación es el **rebalanceo edge-local** al agotar `b_i` (T9b).
11//!
12//! **El certificado.** Si `spent_i ≤ b_i` en cada réplica, entonces
13//! `valor = inicial − Σ spent_i ≥ inicial − Σ b_i ≥ inicial − S = K`, para **toda
14//! ejecución, orden y partición**. No se descubre tarde: se garantiza por
15//! construcción. Eso es evitación real, no la detección reactiva de T8 (§A).
16//!
17//! **Honestidad (§B):** escrow no vence a CALM; *transforma* la operación
18//! ("retirar sin límite" → "retirar dentro de presupuesto") para que sea
19//! I-confluente, al costo de un rebalanceo ocasional.
20
21use crate::invariant::GlobalInvariant;
22
23/// El resultado de intentar gastar localmente.
24#[derive(Debug, Clone, Copy, PartialEq, Eq)]
25pub enum SpendResult {
26 /// Dentro de presupuesto: gasto local, **cero coordinación**.
27 Local,
28 /// Presupuesto agotado: hace falta rebalanceo edge-local (T9b).
29 NeedsRebalance {
30 /// Cuánto falta para cubrir el gasto pedido.
31 deficit: i64,
32 },
33}
34
35/// El presupuesto repartido: la 0-cocadena `b` sobre las réplicas.
36#[derive(Debug, Clone, PartialEq, Eq)]
37pub struct Budget {
38 /// Presupuesto restante por réplica.
39 pub per_replica: Vec<i64>,
40}
41
42impl Budget {
43 /// Presupuesto a partir de un reparto explícito.
44 pub fn new(per_replica: Vec<i64>) -> Self {
45 Self { per_replica }
46 }
47
48 /// Reparte el `slack` en `n` presupuestos proporcionales a `weights`, con
49 /// división entera para garantizar `Σ b_i ≤ slack` (reparto siempre válido).
50 pub fn split(inv: &GlobalInvariant, weights: &[u64]) -> Self {
51 let s = inv.slack().max(0) as u128;
52 let total: u128 = weights.iter().map(|&w| w as u128).sum();
53 let per_replica = if total == 0 {
54 vec![0; weights.len()]
55 } else {
56 // ⌊w_i · S / total⌋ ⟹ la suma nunca excede S.
57 weights.iter().map(|&w| ((w as u128 * s) / total) as i64).collect()
58 };
59 Self { per_replica }
60 }
61
62 /// El certificado del reparto (§B): `Σ b_i ≤ slack` y todo `b_i ≥ 0`.
63 pub fn is_valid_split(&self, inv: &GlobalInvariant) -> bool {
64 self.per_replica.iter().all(|&b| b >= 0)
65 && self.per_replica.iter().sum::<i64>() <= inv.slack()
66 }
67
68 /// Presupuesto restante de la réplica `r`.
69 pub fn remaining(&self, r: usize) -> i64 {
70 self.per_replica[r]
71 }
72
73 /// Gasto local de `amount` (≥ 0) en la réplica `r`. Si cabe, descuenta y
74 /// devuelve `Local`; si no, **no gasta** y devuelve `NeedsRebalance` con el
75 /// déficit. Nunca declara "libre global" a ciegas.
76 pub fn try_spend(&mut self, r: usize, amount: i64) -> SpendResult {
77 debug_assert!(amount >= 0, "los gastos son no negativos");
78 if amount <= self.per_replica[r] {
79 self.per_replica[r] -= amount;
80 SpendResult::Local
81 } else {
82 SpendResult::NeedsRebalance {
83 deficit: amount - self.per_replica[r],
84 }
85 }
86 }
87
88 /// El valor del recurso implicado por unos gastos `spent_i` (para el
89 /// certificado): `inicial − Σ spent_i`.
90 pub fn value_after(inv: &GlobalInvariant, spent: &[i64]) -> i64 {
91 inv.initial - spent.iter().sum::<i64>()
92 }
93}
94
95/// **Presupuesto con procedencia** (T10, §C.1 — la vía Balegas): todo es monótono
96/// creciente, así que la fusión es un CRDT y **no hay carreras**. Sustituye al
97/// `Budget` mutable de T9 (`b_i` leído-y-escrito), que era seguro solo en
98/// snapshots congelados y secuenciales.
99///
100/// El presupuesto disponible es una **función derivada** de dos historiales que
101/// solo crecen: `granted[from][to]` (derechos cedidos) y `spent[i]` (gasto).
102///
103/// **El teorema (§C):** `Σ avail = Σ b0 − Σ spent`, invariante bajo cualquier
104/// entrelazado, porque cada `granted[j][i]` entra `+` en `i` y `−` en `j` y se
105/// cancela. Imposible fabricar presupuesto por fusión; imposible perderlo por un
106/// crash a medio propagar (un `grant` vive entero en `granted[from][to]`: al
107/// re-fusionar, o llegó completo o no llegó).
108#[derive(Debug, Clone, PartialEq, Eq)]
109pub struct EscrowState {
110 /// Reparto inicial (constante); `Σ b0 ≤ slack`.
111 pub b0: Vec<i64>,
112 /// `granted[from][to]`: derechos transferidos, solo crece. Fila `from`
113 /// escrita solo por la réplica `from` (single-writer ⟹ sin conflicto).
114 pub granted: Vec<Vec<i64>>,
115 /// `spent[i]`: gasto de la réplica `i`, solo crece.
116 pub spent: Vec<i64>,
117}
118
119impl EscrowState {
120 /// Estado inicial a partir de un reparto `b0` (sin transferencias ni gasto).
121 pub fn new(b0: Vec<i64>) -> Self {
122 let n = b0.len();
123 Self {
124 b0,
125 granted: vec![vec![0; n]; n],
126 spent: vec![0; n],
127 }
128 }
129
130 /// Número de réplicas.
131 pub fn replicas(&self) -> usize {
132 self.b0.len()
133 }
134
135 /// Presupuesto disponible de `i` = inicial + recibido − cedido − gastado.
136 pub fn avail(&self, i: usize) -> i64 {
137 let recibido: i64 = (0..self.replicas()).map(|j| self.granted[j][i]).sum();
138 let cedido: i64 = self.granted[i].iter().sum();
139 self.b0[i] + recibido - cedido - self.spent[i]
140 }
141
142 /// Presupuesto total disponible. Por el teorema de §C es exactamente
143 /// `Σ b0 − Σ spent` — los `granted` se cancelan y **no cambian el total**.
144 pub fn total_avail(&self) -> i64 {
145 self.b0.iter().sum::<i64>() - self.spent.iter().sum::<i64>()
146 }
147
148 /// La otra vía de calcular el total (sumando cada `avail`), que DEBE coincidir
149 /// con `total_avail`: la prueba de la cancelación de `granted`.
150 pub fn sum_avail(&self) -> i64 {
151 (0..self.replicas()).map(|i| self.avail(i)).sum()
152 }
153
154 /// La réplica `from` cede `amount` (≥0) a `to`. Guardado por su `avail` local
155 /// (single-writer): nunca cede más de lo que tiene ⟹ imposible fabricar en el
156 /// origen. Devuelve `false` si no le alcanza.
157 pub fn grant(&mut self, from: usize, to: usize, amount: i64) -> bool {
158 debug_assert!(amount >= 0);
159 if amount <= self.avail(from) {
160 self.granted[from][to] += amount;
161 true
162 } else {
163 false
164 }
165 }
166
167 /// La réplica `i` gasta `amount` (≥0) si le queda `avail`. Monótono.
168 pub fn spend(&mut self, i: usize, amount: i64) -> bool {
169 debug_assert!(amount >= 0);
170 if amount <= self.avail(i) {
171 self.spent[i] += amount;
172 true
173 } else {
174 false
175 }
176 }
177
178 /// **Fusión CRDT**: máximo componente a componente en `granted` y `spent`
179 /// (los historiales solo crecen). Conmutativa, asociativa, idempotente. No
180 /// puede subir `total_avail`: `Σ spent` solo crece ⟹ el total solo baja.
181 pub fn merge(&mut self, other: &EscrowState) {
182 debug_assert_eq!(self.b0, other.b0, "mismo reparto inicial");
183 let n = self.replicas();
184 for i in 0..n {
185 self.spent[i] = self.spent[i].max(other.spent[i]);
186 for j in 0..n {
187 self.granted[i][j] = self.granted[i][j].max(other.granted[i][j]);
188 }
189 }
190 }
191}
192
193/// Una **identidad** como **conjunto de celdas-dispositivo** (T11a, §C, cura de
194/// F2). No se modela la identidad como una réplica: un usuario es un conjunto de
195/// dispositivos, cada uno una réplica del esquema de T10 con su propia celda de
196/// presupuesto y su propio `spent`. Así la disciplina single-writer se cumple a
197/// nivel de **celda-dispositivo**, no de identidad: dos dispositivos gastan sin
198/// serializar, sin carrera, sin fencing (F2 es un no-problema por diseño).
199///
200/// El invariante (el recurso, p.ej. saldo ≥ 0) es de la identidad; su
201/// disponibilidad y su certificado se computan sobre SUS dispositivos.
202#[derive(Debug, Clone)]
203pub struct Identity {
204 /// Índices de las celdas-dispositivo de esta identidad en el `EscrowState`.
205 pub devices: Vec<usize>,
206 /// El invariante del recurso de esta identidad.
207 pub inv: GlobalInvariant,
208}
209
210impl Identity {
211 /// Crea una identidad con sus dispositivos y su invariante.
212 pub fn new(devices: Vec<usize>, inv: GlobalInvariant) -> Self {
213 Self { devices, inv }
214 }
215
216 /// Presupuesto disponible de la identidad = Σ del `avail` de sus dispositivos.
217 /// Los `grant` **entre** dispositivos de la identidad se cancelan ⟹ solo lo
218 /// mueven `b0` y `spent`: `total_avail = Σ b0[d] − Σ spent[d]`.
219 pub fn total_avail(&self, state: &EscrowState) -> i64 {
220 self.devices.iter().map(|&d| state.avail(d)).sum()
221 }
222
223 /// Valor del recurso de la identidad: `inicial − Σ spent[d]` sobre sus celdas.
224 pub fn value(&self, state: &EscrowState) -> i64 {
225 let gastado: i64 = self.devices.iter().map(|&d| state.spent[d]).sum();
226 self.inv.initial - gastado
227 }
228
229 /// ¿Se preserva el invariante de la identidad?
230 pub fn invariant_holds(&self, state: &EscrowState) -> bool {
231 self.inv.holds(self.value(state))
232 }
233}
234
235#[cfg(test)]
236mod tests {
237 use super::*;
238 use crate::verdict::Verdict;
239 use proptest::prelude::*;
240
241 /// El caso 60/60 de T8, ahora bien tratado (§F): con presupuestos [50,50]
242 /// (reparto válido de S=100), una réplica **particionada** que intenta retirar
243 /// 60 recibe `NeedsRebalance`, NO `Local`. Muere el falso-verde del detector.
244 #[test]
245 fn t9_particionado_60_es_bloqueado_no_libre() {
246 let inv = GlobalInvariant::new(100, 0); // saldo ≥ 0, slack 100
247 let mut budget = Budget::new(vec![50, 50]);
248 assert!(budget.is_valid_split(&inv));
249
250 // La réplica 0, aislada, intenta retirar 60 (> su presupuesto de 50).
251 let res = budget.try_spend(0, 60);
252 assert_eq!(res, SpendResult::NeedsRebalance { deficit: 10 });
253 // El veredicto de escrow NO es "libre": pide rebalanceo (localizado).
254 assert!(matches!(Verdict::via_escrow(0, &res), Verdict::NeedsCoordination { .. }));
255 // Y no gastó: el presupuesto sigue intacto (el gasto queda pendiente).
256 assert_eq!(budget.remaining(0), 50);
257 }
258
259 /// Gasto dentro de presupuesto: local y descuenta.
260 #[test]
261 fn gasto_dentro_de_presupuesto_es_local() {
262 let mut budget = Budget::new(vec![50, 50]);
263 assert_eq!(budget.try_spend(0, 30), SpendResult::Local);
264 assert_eq!(budget.remaining(0), 20);
265 assert!(matches!(Verdict::via_escrow(0, &SpendResult::Local), Verdict::RunsFree));
266 }
267
268 fn split_valido(inv: &GlobalInvariant, raw: &[u64]) -> Budget {
269 let b = Budget::split(inv, raw);
270 assert!(b.is_valid_split(inv), "split debe ser válido por construcción");
271 b
272 }
273
274 proptest! {
275 /// **EL CERTIFICADO (§F, el corazón de T9a).** Para todo reparto válido y
276 /// TODA combinación de gastos dentro de presupuesto —incluidas particiones
277 /// arbitrarias y todas las réplicas gastando su máximo a la vez— el
278 /// invariante global `valor ≥ K` se preserva. Se cuantifica sobre todos
279 /// los estados alcanzables, no sobre un merge concreto.
280 #[test]
281 fn certificado_valor_nunca_baja_del_piso(
282 initial in 0i64..500,
283 floor in -100i64..100,
284 pesos in prop::collection::vec(0u64..50, 1..6),
285 gasto_raw in prop::collection::vec(0u64..600, 1..6),
286 ) {
287 prop_assume!(initial >= floor); // slack ≥ 0
288 let inv = GlobalInvariant::new(initial, floor);
289 let budget = split_valido(&inv, &pesos);
290
291 // Gastos arbitrarios pero acotados por el presupuesto de cada réplica.
292 let spent: Vec<i64> = budget
293 .per_replica
294 .iter()
295 .zip(gasto_raw.iter().chain(std::iter::repeat(&0)))
296 .map(|(&b, &g)| (g as i64).min(b)) // spent_i ≤ b_i
297 .collect();
298
299 // El certificado: valor = inicial − Σ spent ≥ floor. Para cualquier
300 // subconjunto que sincronice (partición) el valor es aún mayor.
301 let valor = Budget::value_after(&inv, &spent);
302 prop_assert!(inv.holds(valor), "valor {} < piso {}", valor, inv.floor);
303 }
304 }
305
306 // ---- T10a: presupuesto con procedencia (EscrowState) ----
307
308 /// **El modo de fallo de §B, PREVENIDO en el origen.** `B` tiene 30. Cede 20 a
309 /// `A`; el segundo intento de ceder 20 a `C` **falla** (solo le quedan 10),
310 /// porque `grant` está guardado por el `avail` local. Nada de fabricar 20 por
311 /// una lectura-y-escritura descuidada. `Σ avail` se conserva en 30.
312 #[test]
313 fn grant_guardado_previene_la_fabricacion() {
314 let mut s = EscrowState::new(vec![0, 30, 0]);
315 assert!(s.grant(1, 0, 20), "B cede 20 a A");
316 assert!(!s.grant(1, 2, 20), "B ya no puede ceder otros 20 (solo le quedan 10)");
317 assert!(s.grant(1, 2, 10), "pero sí los 10 restantes");
318 assert_eq!(s.avail(0), 20);
319 assert_eq!(s.avail(1), 0);
320 assert_eq!(s.avail(2), 10);
321 assert_eq!(s.total_avail(), 30, "Σ avail conservado: cero fabricación");
322 }
323
324 /// Crash a mitad de transferencia: un `grant` aplicado en una copia y no
325 /// propagado, al re-fusionar tarde da el mismo estado. Ni fabrica ni pierde.
326 #[test]
327 fn crash_a_mitad_de_transferencia_es_seguro() {
328 let base = EscrowState::new(vec![30, 0]);
329 // Copia 1: B0 concede 20 a la réplica 1 (el "grant en tránsito").
330 let mut c1 = base.clone();
331 assert!(c1.grant(0, 1, 20));
332 // Copia 2 (crashea sin ver el grant): fusiona el resto tal cual.
333 let mut c2 = base.clone();
334 c2.merge(&base);
335 // El grant llega tarde: c2 re-fusiona con c1.
336 c2.merge(&c1);
337 assert_eq!(c2, c1, "el grant llega entero o no llega; nunca a medias");
338 assert_eq!(c2.total_avail(), 30);
339 }
340
341 /// **§G.2 — réplica por dispositivo (F2).** Una identidad con dos
342 /// dispositivos (celdas `[50,50]`, cuenta 100). Ambos gastan concurrentemente
343 /// SU celda sin serializar; el gasto de uno **no toca** el `avail` del otro;
344 /// el `total_avail` de la identidad es `Σ celdas − Σ spent`, invariante.
345 #[test]
346 fn t11a_dos_dispositivos_gastan_sin_pisarse() {
347 let inv = GlobalInvariant::new(100, 0);
348 let id = Identity::new(vec![0, 1], inv);
349 let mut state = EscrowState::new(vec![50, 50]);
350
351 assert!(state.spend(0, 40));
352 assert!(state.spend(1, 30));
353 assert_eq!(state.avail(1), 20, "el gasto de 0 no tocó el avail de 1");
354 assert_eq!(id.total_avail(&state), 30, "Σ celdas − Σ spent = 100 − 70");
355 assert!(id.invariant_holds(&state));
356
357 // Cada celda tiene un único escritor lógico: 0 no puede gastar la de 1.
358 assert!(!state.spend(0, 20), "0 ya solo tiene 10 en su propia celda");
359 }
360
361 /// Rebalanceo **entre dispositivos** de una identidad = un `grant`, que
362 /// conserva el `total_avail` (T10a) — el rebalanceo edge-local de T10b.
363 #[test]
364 fn t11a_rebalanceo_entre_dispositivos_conserva() {
365 let inv = GlobalInvariant::new(100, 0);
366 let id = Identity::new(vec![0, 1], inv);
367 let mut state = EscrowState::new(vec![0, 50]);
368 let antes = id.total_avail(&state);
369
370 assert!(state.grant(1, 0, 20), "el dispositivo 1 cede 20 al 0 (seco)");
371 assert_eq!(state.avail(0), 20);
372 assert_eq!(state.avail(1), 30);
373 assert_eq!(id.total_avail(&state), antes, "el rebalanceo conserva");
374 }
375
376 /// Identidades disjuntas no se pisan (F2): la disponibilidad de una identidad
377 /// depende **solo** de sus dispositivos; la actividad de otra no la afecta.
378 #[test]
379 fn t11a_identidades_disjuntas_aisladas() {
380 let inv = GlobalInvariant::new(100, 0);
381 let a = Identity::new(vec![0, 1], inv);
382 let b = Identity::new(vec![2, 3], inv);
383 let mut state = EscrowState::new(vec![50, 50, 50, 50]);
384
385 // Toda la actividad ocurre en la identidad B.
386 assert!(state.spend(2, 40));
387 assert!(state.grant(3, 2, 10));
388
389 assert_eq!(a.total_avail(&state), 100, "A intacta");
390 assert!(a.invariant_holds(&state));
391 assert!(b.invariant_holds(&state));
392 }
393
394 fn escrow_st() -> impl Strategy<Value = EscrowState> {
395 (1usize..=4).prop_flat_map(|n| {
396 let b0 = prop::collection::vec(0i64..50, n);
397 let granted = prop::collection::vec(prop::collection::vec(0i64..30, n), n);
398 let spent = prop::collection::vec(0i64..30, n);
399 (b0, granted, spent).prop_map(|(b0, granted, spent)| EscrowState { b0, granted, spent })
400 })
401 }
402
403 /// Dos estados con el mismo reparto inicial (para poder fusionarlos).
404 fn par_de_escrow() -> impl Strategy<Value = (EscrowState, EscrowState)> {
405 escrow_st().prop_flat_map(|a| {
406 let n = a.replicas();
407 let granted = prop::collection::vec(prop::collection::vec(0i64..30, n), n);
408 let spent = prop::collection::vec(0i64..30, n);
409 let b0 = a.b0.clone();
410 (Just(a), (granted, spent)).prop_map(move |(a, (g, s))| {
411 let b = EscrowState { b0: b0.clone(), granted: g, spent: s };
412 (a, b)
413 })
414 })
415 }
416
417 /// Fusiona todas las copias en una vista global (el estado "verdadero").
418 fn merge_all(copies: &[EscrowState], b0: &[i64]) -> EscrowState {
419 let mut g = EscrowState::new(b0.to_vec());
420 for c in copies {
421 g.merge(c);
422 }
423 g
424 }
425
426 /// Escenario dinámico: invariante, reparto por pesos, y una secuencia de
427 /// eventos `(op, x, y, monto)` a interpretar como spend/grant/merge.
428 #[allow(clippy::type_complexity)]
429 fn escenario() -> impl Strategy<Value = (GlobalInvariant, Vec<u64>, Vec<(u8, usize, usize, i64)>)> {
430 (2usize..=4, 0i64..200, -50i64..50).prop_flat_map(|(n, slack, floor)| {
431 let inv = GlobalInvariant::new(floor + slack, floor);
432 let pesos = prop::collection::vec(0u64..20, n);
433 let evento = (0u8..3, 0..n, 0..n, 0i64..80);
434 let eventos = prop::collection::vec(evento, 0..40);
435 (Just(inv), pesos, eventos)
436 })
437 }
438
439 proptest! {
440 /// **§F.5 — EL CERTIFICADO DINÁMICO (el teorema de T10).** Entrelaza gastos,
441 /// transferencias (`grant`) concurrentes, crashes (grants sin propagar) y
442 /// particiones (merges en orden arbitrario) sobre copias por réplica. En
443 /// **todo momento** `valor = inicial − Σ spent ≥ K`, y el presupuesto total
444 /// nunca se fabrica (`total_avail ≥ 0`). Subsume el certificado estático de
445 /// T9: ya no vale solo para snapshots congelados, sino bajo concurrencia.
446 #[test]
447 fn certificado_dinamico(( inv, pesos, eventos) in escenario()) {
448 let n = pesos.len();
449 // Reparto válido: Σ b0 ≤ slack (mismo split proporcional de T9a).
450 let b0 = Budget::split(&inv, &pesos).per_replica;
451 // Una copia local por réplica (vistas divergibles bajo partición).
452 let mut copies = vec![EscrowState::new(b0.clone()); n];
453
454 for (op, x, y, amount) in eventos {
455 let i = x % n;
456 let j = y % n;
457 match op % 3 {
458 // Gasto local, guardado por el avail local (single-writer índice i).
459 0 => { copies[i].spend(i, amount); }
460 // Transferencia: la réplica i cede desde SU fila, guardada.
461 1 => { copies[i].grant(i, j, amount); }
462 // Sincronización: i fusiona la copia de j (orden arbitrario = partición/crash).
463 _ => { let otra = copies[j].clone(); copies[i].merge(&otra); }
464 }
465
466 // El teorema, tras cada evento: la vista global no fabrica ni sobregira.
467 let global = merge_all(&copies, &b0);
468 prop_assert!(global.total_avail() >= 0, "presupuesto fabricado: total_avail < 0");
469 let valor = inv.initial - global.spent.iter().sum::<i64>();
470 prop_assert!(inv.holds(valor), "valor {} < piso {}", valor, inv.floor);
471 }
472 }
473
474 /// **§F.1 — el total no se puede fabricar.** `Σ avail` (sumando cada réplica)
475 /// SIEMPRE es igual a `Σ b0 − Σ spent`: los `granted` se cancelan, pase lo
476 /// que pase con las transferencias. Este es el teorema que mata el §B.
477 #[test]
478 fn total_avail_es_invariante_a_los_granted(s in escrow_st()) {
479 prop_assert_eq!(s.sum_avail(), s.total_avail());
480 prop_assert_eq!(s.total_avail(), s.b0.iter().sum::<i64>() - s.spent.iter().sum::<i64>());
481 }
482
483 /// **§F.2 — `merge` es un CRDT:** conmutativo e idempotente.
484 #[test]
485 fn merge_conmutativo_e_idempotente((a, b) in par_de_escrow()) {
486 let mut ab = a.clone(); ab.merge(&b);
487 let mut ba = b.clone(); ba.merge(&a);
488 prop_assert_eq!(&ab, &ba, "merge conmutativo");
489 let mut abb = ab.clone(); abb.merge(&b);
490 prop_assert_eq!(&abb, &ab, "merge idempotente");
491 }
492
493 /// **§F.1 (fusión) — `merge` nunca sube el total.** `Σ spent` solo crece por
494 /// max ⟹ `total_avail` solo puede bajar. Imposible fabricar por fusión.
495 #[test]
496 fn merge_nunca_fabrica_presupuesto((a, b) in par_de_escrow()) {
497 let mut m = a.clone(); m.merge(&b);
498 prop_assert!(m.total_avail() <= a.total_avail());
499 prop_assert!(m.total_avail() <= b.total_avail());
500 }
501 }
502}