Mantener las invariantes: el contrato que hace correcto al unsafe

Un núcleo unsafe no es correcto en abstracto: es correcto bajo unas suposiciones. ptr::read es seguro si esos bytes están inicializados; get_unchecked(i) lo es si i cae en rango. Esas suposiciones —el puntero no es nulo, len <= cap, los primeros len elementos están vivos— son las invariantes del tipo, y tu trabajo como autor de la abstracción es sostenerlas en todo momento en que el control esté fuera de tus métodos. Sostenerlas tiene tres frentes obligatorios: el constructor las establece, cada método las preserva, y Drop las honra. Y hay un cuarto, traicionero, que casi todos olvidan: un pánico a mitad de una mutación no puede dejar el objeto en un estado que luego provoque UB.

La invariante como proposición

Una invariante es una afirmación sobre el estado interno que debe ser cierta siempre que el control salga de tus métodos: entre una llamada y la siguiente, un observador externo jamás debe poder atrapar al objeto en un estado que viole esa afirmación. Construyamos una pila de capacidad fija sobre memoria sin inicializar para verlo en carne viva:

use std::mem::MaybeUninit;

pub struct Pila<T> {
    datos: Box<[MaybeUninit<T>]>, // capacidad = datos.len()
    len: usize,
}

Sus invariantes, escritas como un contrato con uno mismo:

• len <= datos.len() (nunca desbordamos la capacidad).
• Las posiciones datos[0..len] están inicializadas; datos[len..] no.

Todo el unsafe de este tipo será correcto si y solo si esas dos frases se mantienen. La disciplina consiste en no dejarlas caer en ningún camino.

Establecer y preservar

El constructor establece la invariante partiendo de un estado trivialmente válido: capacidad reservada, cero elementos vivos.

impl<T> Pila<T> {
    pub fn con_capacidad(cap: usize) -> Self {
        let datos = (0..cap).map(|_| MaybeUninit::uninit()).collect();
        Pila { datos, len: 0 } // len = 0: el rango inicializado esta vacio, cierto
    }
}

Cada método debe preservar la invariante: si es cierta al entrar, ha de ser cierta al salir. Y aquí aparece la sutileza del orden. En push escribimos el valor antes de incrementar len; en pop decrementamos len antes de leer el valor:

impl<T> Pila<T> {
    pub fn push(&mut self, v: T) -> Result<(), T> {
        if self.len == self.datos.len() {
            return Err(v); // preserva la invariante rechazando el desbordamiento
        }
        self.datos[self.len].write(v);
        self.len += 1; // solo tras escribir: len nunca cuenta un hueco sin inicializar
        Ok(())
    }

    pub fn pop(&mut self) -> Option<T> {
        if self.len == 0 {
            return None;
        }
        self.len -= 1; // primero: el elemento deja de estar "vivo" para la invariante
        // SAFETY: datos[len] estaba inicializado y ya nadie mas lo leera
        Some(unsafe { self.datos[self.len].assume_init_read() })
    }
}

El orden no es estética: es corrección. Si en push incrementáramos len antes de escribir, existiría un instante en que la invariante “los primeros len están inicializados” sería falsa, con un hueco de basura contando como vivo. Y si algo entre medias fallara, ese estado corrupto sobreviviría.

El camino que todos olvidan: el pánico

Por eso pop decrementa len antes de mover el valor hacia fuera: en el momento en que ese elemento sale de la pila, deja de contar como inicializado, y aunque el propio dato entrara en pánico al ser movido —imposible aquí, pero razónalo en general—, Drop ya no lo tocaría. El principio se generaliza: si vas a extraer o reescribir varios elementos, ajusta primero el contador y opera después, de modo que ningún estado intermedio observable viole la invariante.

Honrar la invariante en Drop

Drop es el tercer camino, y depende por completo de que la invariante sea cierta al entrar. Debe destruir exactamente los elementos inicializados —los primeros len— y ni uno más, o incurrirá en doble liberación:

impl<T> Drop for Pila<T> {
    fn drop(&mut self) {
        for hueco in &mut self.datos[..self.len] {
            // SAFETY: datos[0..len] estan inicializados (invariante) y se
            // destruyen una sola vez, porque len marca justo esa frontera
            unsafe { hueco.assume_init_drop(); }
        }
    }
}

Fíjate en la simbiosis: Drop puede confiar ciegamente en len porque cada método lo mantuvo honesto. La invariante es un contrato transitivo. Y el peligro simétrico está en mover un valor fuera de memoria cruda sin ajustar el contador: si assume_init_read copia un T hacia fuera pero len sigue contándolo, Drop lo destruirá una segunda vez. Por eso mover-fuera y decrementar son un solo acto indivisible.

flowchart TD
C[Constructor establece la invariante] --> M[Metodos la preservan en cada camino]
M --> M
M --> P[Un panico desenrolla y dispara Drop]
P --> D[Drop honra la invariante y destruye solo lo vivo]
M --> D
style C fill:#a6e3a1,color:#11111b
style P fill:#f38ba8,color:#11111b
style D fill:#cba6f7,color:#11111b