T11b: durabilidad de spent (cura de F1)
T11 §B: el supuesto oculto de T10 (spent monótono en la fuente) se hace real con un write-ahead log. Un gasto se ackea SOLO tras persistirse; un crash pierde gastos no reconocidos, jamás uno reconocido. - durable::WriteAheadLog (committed solo crece; commit_spend persiste antes de devolver AckToken) + DurableSpent (wal durable + live volátil; recover reconstruye live desde el WAL ⟹ nunca por debajo del último ack). - try_restore_snapshot rechaza restaurar por debajo del WAL (adversario de rollback → doble gasto). Tests §G.1 (el crash MALO, no el benigno): el WAL sobrevive al crash y no olvida; el adversario que intenta revertir por debajo del compromiso durable es rechazado. Con dientes: proptest sobre secuencias de gastos+crashes (value nunca cae bajo el ack) y rollbacks (siempre rechazados). Combinado con el merge por max de T10, garantiza la monotonía que el certificado exige. 69 tests, clippy limpio. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
co-authored by
Claude Opus 4.8
parent
b4bd2e19b4
commit
f3f7c4fc1c
+177
@@ -0,0 +1,177 @@
|
||||
//! `durable` — que `spent` no pueda olvidar (T11b, F1 / §B).
|
||||
//!
|
||||
//! T10 asumía en silencio que `spent_i` es **monótono en la fuente**: un escritor
|
||||
//! nunca retrocede lo que ya cometió. Aquí ese supuesto se hace real con un
|
||||
//! **write-ahead log**: un gasto se reconoce al usuario (`ack`) **solo después**
|
||||
//! de persistirse. Un crash puede perder gastos *no reconocidos* (nunca
|
||||
//! prometidos), jamás uno reconocido.
|
||||
//!
|
||||
//! Modelo: el WAL es lo durable (sobrevive al crash); el `live` en memoria es
|
||||
//! volátil. `recover` reconstruye `live` desde el WAL ⟹ nunca por debajo del
|
||||
//! último ack. Cero coordinación: cada nodo fsyncea lo suyo. Combinado con el
|
||||
//! `merge` por máximo de T10, garantiza la monotonía que el certificado exige.
|
||||
|
||||
/// Prueba de que un gasto quedó comprometido de forma durable antes del ack.
|
||||
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
|
||||
pub struct AckToken {
|
||||
/// Total comprometido (durable) en el momento del ack.
|
||||
pub committed_total: i64,
|
||||
}
|
||||
|
||||
/// El log durable de gastos de una celda-dispositivo. Solo crece.
|
||||
#[derive(Debug, Clone, Default)]
|
||||
pub struct WriteAheadLog {
|
||||
committed: i64,
|
||||
}
|
||||
|
||||
impl WriteAheadLog {
|
||||
/// WAL vacío.
|
||||
pub fn new() -> Self {
|
||||
Self::default()
|
||||
}
|
||||
|
||||
/// Compromete un gasto (`amount ≥ 0`): **persiste primero** ("fsync") y solo
|
||||
/// entonces devuelve el `AckToken`. Monótono: `committed` solo crece.
|
||||
pub fn commit_spend(&mut self, amount: i64) -> AckToken {
|
||||
debug_assert!(amount >= 0, "los gastos son no negativos");
|
||||
self.committed += amount;
|
||||
AckToken {
|
||||
committed_total: self.committed,
|
||||
}
|
||||
}
|
||||
|
||||
/// Total comprometido y durable. Nunca retrocede.
|
||||
pub fn committed(&self) -> i64 {
|
||||
self.committed
|
||||
}
|
||||
}
|
||||
|
||||
/// El gasto de una celda-dispositivo, respaldado por un WAL durable.
|
||||
#[derive(Debug, Clone, Default)]
|
||||
pub struct DurableSpent {
|
||||
wal: WriteAheadLog,
|
||||
/// Valor en memoria (volátil): se pierde en un crash, se rehace desde el WAL.
|
||||
live: i64,
|
||||
}
|
||||
|
||||
impl DurableSpent {
|
||||
/// Celda de gasto durable en cero.
|
||||
pub fn new() -> Self {
|
||||
Self::default()
|
||||
}
|
||||
|
||||
/// Gasta `amount`: compromete al WAL (durable) y **luego** actualiza el valor
|
||||
/// vivo y ackea. No hay ack sin commit durable.
|
||||
pub fn spend(&mut self, amount: i64) -> AckToken {
|
||||
let ack = self.wal.commit_spend(amount);
|
||||
self.live = self.wal.committed();
|
||||
ack
|
||||
}
|
||||
|
||||
/// El gasto reconocido de la celda.
|
||||
pub fn value(&self) -> i64 {
|
||||
self.live
|
||||
}
|
||||
|
||||
/// Total durable (lo que el WAL garantiza).
|
||||
pub fn committed(&self) -> i64 {
|
||||
self.wal.committed()
|
||||
}
|
||||
|
||||
/// **Recuperación tras crash:** el estado en memoria se pierde; `live` se
|
||||
/// reconstruye desde el WAL. Resultado: `value() == committed() ≥ último ack`.
|
||||
/// Nunca re-gasta lo ya comprometido.
|
||||
pub fn recover(&mut self) {
|
||||
self.live = self.wal.committed();
|
||||
}
|
||||
|
||||
/// **Defensa contra el adversario (§G.1):** un intento de restaurar un
|
||||
/// snapshot *por debajo* del WAL (rollback → doble gasto) se **rechaza**.
|
||||
/// Solo se acepta un valor `≥ committed` (que no retrocede). Devuelve si se
|
||||
/// aceptó.
|
||||
pub fn try_restore_snapshot(&mut self, snapshot: i64) -> bool {
|
||||
if snapshot >= self.wal.committed() {
|
||||
self.live = snapshot;
|
||||
true
|
||||
} else {
|
||||
false // rollback por debajo del compromiso durable: RECHAZADO
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
#[cfg(test)]
|
||||
mod tests {
|
||||
use super::*;
|
||||
use proptest::prelude::*;
|
||||
|
||||
/// §G.1 — el WAL no olvida: se gasta y ackea, "crashea" (se pierde el estado
|
||||
/// en memoria), recupera desde el WAL, y el `spent` recuperado es ≥ el último
|
||||
/// ack. Nunca re-gasta lo ya comprometido.
|
||||
#[test]
|
||||
fn el_wal_sobrevive_al_crash() {
|
||||
let mut d = DurableSpent::new();
|
||||
d.spend(40);
|
||||
let ack = d.spend(30);
|
||||
assert_eq!(ack.committed_total, 70);
|
||||
|
||||
// "Crash": el valor en memoria se corrompe/pierde a un estado viejo...
|
||||
d.live = 40; // (simula memoria stale que olvidó los últimos 30)
|
||||
// ...pero la recuperación lo restaura desde el WAL durable.
|
||||
d.recover();
|
||||
assert_eq!(d.value(), 70, "recuperado ≥ último ack; no olvida");
|
||||
}
|
||||
|
||||
/// §G.1 (adversario) — restaurar un snapshot por debajo del WAL se rechaza;
|
||||
/// por encima (que no retrocede) se acepta.
|
||||
#[test]
|
||||
fn adversario_rollback_es_rechazado() {
|
||||
let mut d = DurableSpent::new();
|
||||
d.spend(70);
|
||||
assert!(!d.try_restore_snapshot(50), "50 < 70 comprometido: rollback rechazado");
|
||||
assert_eq!(d.value(), 70, "el rechazo no tocó el valor");
|
||||
assert!(d.try_restore_snapshot(80), "80 ≥ 70: no retrocede, aceptado");
|
||||
}
|
||||
|
||||
proptest! {
|
||||
/// §G.1 (con dientes) — sobre cualquier secuencia de gastos y crashes, el
|
||||
/// valor recuperado nunca cae por debajo del último ack comprometido.
|
||||
#[test]
|
||||
fn spent_nunca_cae_por_debajo_del_ack(
|
||||
ops in prop::collection::vec((any::<bool>(), 0i64..100), 0..40)
|
||||
) {
|
||||
let mut d = DurableSpent::new();
|
||||
for (crash, amount) in ops {
|
||||
if crash {
|
||||
// Se pierde memoria (a un estado arbitrario viejo) y se recupera.
|
||||
d.live = 0;
|
||||
d.recover();
|
||||
} else {
|
||||
d.spend(amount);
|
||||
}
|
||||
prop_assert!(d.value() >= d.committed(), "por debajo del WAL");
|
||||
prop_assert_eq!(d.value(), d.committed(), "value se ancla al WAL");
|
||||
}
|
||||
}
|
||||
|
||||
/// El adversario nunca logra revertir por debajo del compromiso durable.
|
||||
#[test]
|
||||
fn rollback_por_debajo_del_wal_siempre_rechazado(
|
||||
gastos in prop::collection::vec(0i64..50, 1..8),
|
||||
snapshot in -20i64..300,
|
||||
) {
|
||||
let mut d = DurableSpent::new();
|
||||
for g in gastos {
|
||||
d.spend(g);
|
||||
}
|
||||
let committed = d.committed();
|
||||
let aceptado = d.try_restore_snapshot(snapshot);
|
||||
if snapshot < committed {
|
||||
prop_assert!(!aceptado);
|
||||
prop_assert_eq!(d.value(), committed, "rechazo no retrocede");
|
||||
} else {
|
||||
prop_assert!(aceptado);
|
||||
prop_assert!(d.value() >= committed);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -13,6 +13,7 @@
|
||||
|
||||
pub mod cell;
|
||||
pub mod cohomology;
|
||||
pub mod durable;
|
||||
pub mod error;
|
||||
pub mod escrow;
|
||||
pub mod gf2;
|
||||
|
||||
Reference in New Issue
Block a user