//! `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");
    }

    /// §G.4 — valor REAL del recurso tras un crash + rollback, con y sin la capa
    /// de durabilidad. `real` es un tally independiente de lo que de verdad se
    /// desembolsó; el certificado exige `real ≥ piso`.
    ///
    /// Escenario: celda con presupuesto 50 (cuenta 50, piso 0). Se gasta 50
    /// (agota la celda), un crash revierte el estado en memoria a 0 (rollback
    /// CRUDO, bypass del WAL), y se re-gasta.
    fn valor_real_tras_rollback(con_durabilidad: bool) -> i64 {
        let (initial, budget) = (50i64, 50i64);
        // `real` = oráculo INDEPENDIENTE del desembolso FÍSICO al usuario (efecto
        // externo e irreversible). Se incrementa en el punto de entrega (el ack,
        // justo tras `spend`), UNA vez por retiro efectivamente entregado. Nunca
        // lee la contabilidad interna del sistema (`cell.value()`/`committed()`):
        // cuenta eventos de entrega, no lo que el sistema cree que gastó. Ahí vive
        // la diferencia detección/prevención — mide el dinero que salió al mundo.
        let mut real = 0;
        let mut cell = DurableSpent::new();

        // El guard usa la contabilidad del sistema para DECIDIR si entregar; si esa
        // contabilidad se corrompe (rollback), se entrega de más y `real` lo atrapa.
        if budget - cell.value() >= 50 {
            cell.spend(50); // commit durable → ack → 50 entregados al usuario
            real += 50; // ← desembolso físico (externo), no la variable `spent`
        }
        // Crash + rollback crudo: la memoria vuelve a un estado viejo (spent = 0).
        cell.live = 0;
        if con_durabilidad {
            cell.recover(); // la durabilidad restaura spent = 50 desde el WAL
        }
        // Re-gasto, guardado por el `spent` visible en este momento.
        if budget - cell.value() >= 50 {
            cell.spend(50);
            real += 50; // ← segunda entrega física si el guard dejó pasar (doble gasto)
        }
        initial - real
    }

    /// §G.4 (verde) — con durabilidad, el rollback se atrapa (recover restaura el
    /// WAL), el re-gasto se bloquea, y el certificado aguanta: valor real ≥ 0.
    #[test]
    fn g4_con_durabilidad_el_certificado_queda_verde() {
        let v = valor_real_tras_rollback(true);
        println!("§G.4 CON durabilidad: valor real = {v}  (>= 0 ⟹ VERDE)");
        assert!(v >= 0, "con durabilidad no hay doble gasto");
    }

    /// §G.4 (el diente) — SIN durabilidad, el rollback no atrapado provoca doble
    /// gasto: valor real = -50 < 0. El invariante se rompe de verdad.
    #[test]
    fn g4_sin_durabilidad_el_rollback_sobregira() {
        let v = valor_real_tras_rollback(false);
        println!("§G.4 SIN durabilidad: valor real = {v}  (< 0 ⟹ certificado ROJO)");
        assert!(v < 0, "el rollback no atrapado DEBE sobregirar");
    }

    /// §G.4 (literal) — la aserción del certificado dinámico, ejecutada sobre el
    /// rollback no atrapado, **falla ruidosamente**. Esto prueba que la capa de
    /// durabilidad (§G.1) tiene dientes: sin ella, el certificado se pone rojo.
    #[test]
    #[should_panic(expected = "certificado en ROJO")]
    fn g4_el_certificado_se_pone_rojo_bajo_rollback() {
        let v = valor_real_tras_rollback(false);
        assert!(v >= 0, "certificado en ROJO: valor real {v} < piso 0 por doble gasto");
    }

    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);
            }
        }
    }
}