tawasuyu/hifas

1//! `durable` — que `spent` no pueda olvidar (T11b, F1 / §B).
2//!
3//! T10 asumía en silencio que `spent_i` es **monótono en la fuente**: un escritor
4//! nunca retrocede lo que ya cometió. Aquí ese supuesto se hace real con un
5//! **write-ahead log**: un gasto se reconoce al usuario (`ack`) **solo después**
6//! de persistirse. Un crash puede perder gastos *no reconocidos* (nunca
7//! prometidos), jamás uno reconocido.
8//!
9//! Modelo: el WAL es lo durable (sobrevive al crash); el `live` en memoria es
10//! volátil. `recover` reconstruye `live` desde el WAL ⟹ nunca por debajo del
11//! último ack. Cero coordinación: cada nodo fsyncea lo suyo. Combinado con el
12//! `merge` por máximo de T10, garantiza la monotonía que el certificado exige.
13
14/// Prueba de que un gasto quedó comprometido de forma durable antes del ack.
15#[derive(Debug, Clone, Copy, PartialEq, Eq)]
16pub struct AckToken {
17    /// Total comprometido (durable) en el momento del ack.
18    pub committed_total: i64,
19}
20
21/// El log durable de gastos de una celda-dispositivo. Solo crece.
22#[derive(Debug, Clone, Default)]
23pub struct WriteAheadLog {
24    committed: i64,
25}
26
27impl WriteAheadLog {
28    /// WAL vacío.
29    pub fn new() -> Self {
30        Self::default()
31    }
32
33    /// Compromete un gasto (`amount ≥ 0`): **persiste primero** ("fsync") y solo
34    /// entonces devuelve el `AckToken`. Monótono: `committed` solo crece.
35    pub fn commit_spend(&mut self, amount: i64) -> AckToken {
36        debug_assert!(amount >= 0, "los gastos son no negativos");
37        self.committed += amount;
38        AckToken {
39            committed_total: self.committed,
40        }
41    }
42
43    /// Total comprometido y durable. Nunca retrocede.
44    pub fn committed(&self) -> i64 {
45        self.committed
46    }
47}
48
49/// El gasto de una celda-dispositivo, respaldado por un WAL durable.
50#[derive(Debug, Clone, Default)]
51pub struct DurableSpent {
52    wal: WriteAheadLog,
53    /// Valor en memoria (volátil): se pierde en un crash, se rehace desde el WAL.
54    live: i64,
55}
56
57impl DurableSpent {
58    /// Celda de gasto durable en cero.
59    pub fn new() -> Self {
60        Self::default()
61    }
62
63    /// Gasta `amount`: compromete al WAL (durable) y **luego** actualiza el valor
64    /// vivo y ackea. No hay ack sin commit durable.
65    pub fn spend(&mut self, amount: i64) -> AckToken {
66        let ack = self.wal.commit_spend(amount);
67        self.live = self.wal.committed();
68        ack
69    }
70
71    /// El gasto reconocido de la celda.
72    pub fn value(&self) -> i64 {
73        self.live
74    }
75
76    /// Total durable (lo que el WAL garantiza).
77    pub fn committed(&self) -> i64 {
78        self.wal.committed()
79    }
80
81    /// **Recuperación tras crash:** el estado en memoria se pierde; `live` se
82    /// reconstruye desde el WAL. Resultado: `value() == committed() ≥ último ack`.
83    /// Nunca re-gasta lo ya comprometido.
84    pub fn recover(&mut self) {
85        self.live = self.wal.committed();
86    }
87
88    /// **Defensa contra el adversario (§G.1):** un intento de restaurar un
89    /// snapshot *por debajo* del WAL (rollback → doble gasto) se **rechaza**.
90    /// Solo se acepta un valor `≥ committed` (que no retrocede). Devuelve si se
91    /// aceptó.
92    pub fn try_restore_snapshot(&mut self, snapshot: i64) -> bool {
93        if snapshot >= self.wal.committed() {
94            self.live = snapshot;
95            true
96        } else {
97            false // rollback por debajo del compromiso durable: RECHAZADO
98        }
99    }
100}
101
102#[cfg(test)]
103mod tests {
104    use super::*;
105    use proptest::prelude::*;
106
107    /// §G.1 — el WAL no olvida: se gasta y ackea, "crashea" (se pierde el estado
108    /// en memoria), recupera desde el WAL, y el `spent` recuperado es ≥ el último
109    /// ack. Nunca re-gasta lo ya comprometido.
110    #[test]
111    fn el_wal_sobrevive_al_crash() {
112        let mut d = DurableSpent::new();
113        d.spend(40);
114        let ack = d.spend(30);
115        assert_eq!(ack.committed_total, 70);
116
117        // "Crash": el valor en memoria se corrompe/pierde a un estado viejo...
118        d.live = 40; // (simula memoria stale que olvidó los últimos 30)
119        // ...pero la recuperación lo restaura desde el WAL durable.
120        d.recover();
121        assert_eq!(d.value(), 70, "recuperado ≥ último ack; no olvida");
122    }
123
124    /// §G.1 (adversario) — restaurar un snapshot por debajo del WAL se rechaza;
125    /// por encima (que no retrocede) se acepta.
126    #[test]
127    fn adversario_rollback_es_rechazado() {
128        let mut d = DurableSpent::new();
129        d.spend(70);
130        assert!(!d.try_restore_snapshot(50), "50 < 70 comprometido: rollback rechazado");
131        assert_eq!(d.value(), 70, "el rechazo no tocó el valor");
132        assert!(d.try_restore_snapshot(80), "80 ≥ 70: no retrocede, aceptado");
133    }
134
135    /// §G.4 — valor REAL del recurso tras un crash + rollback, con y sin la capa
136    /// de durabilidad. `real` es un tally independiente de lo que de verdad se
137    /// desembolsó; el certificado exige `real ≥ piso`.
138    ///
139    /// Escenario: celda con presupuesto 50 (cuenta 50, piso 0). Se gasta 50
140    /// (agota la celda), un crash revierte el estado en memoria a 0 (rollback
141    /// CRUDO, bypass del WAL), y se re-gasta.
142    fn valor_real_tras_rollback(con_durabilidad: bool) -> i64 {
143        let (initial, budget) = (50i64, 50i64);
144        // `real` = oráculo INDEPENDIENTE del desembolso FÍSICO al usuario (efecto
145        // externo e irreversible). Se incrementa en el punto de entrega (el ack,
146        // justo tras `spend`), UNA vez por retiro efectivamente entregado. Nunca
147        // lee la contabilidad interna del sistema (`cell.value()`/`committed()`):
148        // cuenta eventos de entrega, no lo que el sistema cree que gastó. Ahí vive
149        // la diferencia detección/prevención — mide el dinero que salió al mundo.
150        let mut real = 0;
151        let mut cell = DurableSpent::new();
152
153        // El guard usa la contabilidad del sistema para DECIDIR si entregar; si esa
154        // contabilidad se corrompe (rollback), se entrega de más y `real` lo atrapa.
155        if budget - cell.value() >= 50 {
156            cell.spend(50); // commit durable → ack → 50 entregados al usuario
157            real += 50; // ← desembolso físico (externo), no la variable `spent`
158        }
159        // Crash + rollback crudo: la memoria vuelve a un estado viejo (spent = 0).
160        cell.live = 0;
161        if con_durabilidad {
162            cell.recover(); // la durabilidad restaura spent = 50 desde el WAL
163        }
164        // Re-gasto, guardado por el `spent` visible en este momento.
165        if budget - cell.value() >= 50 {
166            cell.spend(50);
167            real += 50; // ← segunda entrega física si el guard dejó pasar (doble gasto)
168        }
169        initial - real
170    }
171
172    /// §G.4 (verde) — con durabilidad, el rollback se atrapa (recover restaura el
173    /// WAL), el re-gasto se bloquea, y el certificado aguanta: valor real ≥ 0.
174    #[test]
175    fn g4_con_durabilidad_el_certificado_queda_verde() {
176        let v = valor_real_tras_rollback(true);
177        println!("§G.4 CON durabilidad: valor real = {v}  (>= 0 ⟹ VERDE)");
178        assert!(v >= 0, "con durabilidad no hay doble gasto");
179    }
180
181    /// §G.4 (el diente) — SIN durabilidad, el rollback no atrapado provoca doble
182    /// gasto: valor real = -50 < 0. El invariante se rompe de verdad.
183    #[test]
184    fn g4_sin_durabilidad_el_rollback_sobregira() {
185        let v = valor_real_tras_rollback(false);
186        println!("§G.4 SIN durabilidad: valor real = {v}  (< 0 ⟹ certificado ROJO)");
187        assert!(v < 0, "el rollback no atrapado DEBE sobregirar");
188    }
189
190    /// §G.4 (literal) — la aserción del certificado dinámico, ejecutada sobre el
191    /// rollback no atrapado, **falla ruidosamente**. Esto prueba que la capa de
192    /// durabilidad (§G.1) tiene dientes: sin ella, el certificado se pone rojo.
193    #[test]
194    #[should_panic(expected = "certificado en ROJO")]
195    fn g4_el_certificado_se_pone_rojo_bajo_rollback() {
196        let v = valor_real_tras_rollback(false);
197        assert!(v >= 0, "certificado en ROJO: valor real {v} < piso 0 por doble gasto");
198    }
199
200    proptest! {
201        /// §G.1 (con dientes) — sobre cualquier secuencia de gastos y crashes, el
202        /// valor recuperado nunca cae por debajo del último ack comprometido.
203        #[test]
204        fn spent_nunca_cae_por_debajo_del_ack(
205            ops in prop::collection::vec((any::<bool>(), 0i64..100), 0..40)
206        ) {
207            let mut d = DurableSpent::new();
208            for (crash, amount) in ops {
209                if crash {
210                    // Se pierde memoria (a un estado arbitrario viejo) y se recupera.
211                    d.live = 0;
212                    d.recover();
213                } else {
214                    d.spend(amount);
215                }
216                prop_assert!(d.value() >= d.committed(), "por debajo del WAL");
217                prop_assert_eq!(d.value(), d.committed(), "value se ancla al WAL");
218            }
219        }
220
221        /// El adversario nunca logra revertir por debajo del compromiso durable.
222        #[test]
223        fn rollback_por_debajo_del_wal_siempre_rechazado(
224            gastos in prop::collection::vec(0i64..50, 1..8),
225            snapshot in -20i64..300,
226        ) {
227            let mut d = DurableSpent::new();
228            for g in gastos {
229                d.spend(g);
230            }
231            let committed = d.committed();
232            let aceptado = d.try_restore_snapshot(snapshot);
233            if snapshot < committed {
234                prop_assert!(!aceptado);
235                prop_assert_eq!(d.value(), committed, "rechazo no retrocede");
236            } else {
237                prop_assert!(aceptado);
238                prop_assert!(d.value() >= committed);
239            }
240        }
241    }
242}