Soteria Rust es una herramienta de ejecución simbólica escrita en OCaml que verifica programas Rust recorriendo cada camino de ejecución para detectar comportamiento indefinido y errores de aliasing. Durante un benchmark rutinario, los desarrolladores observaron que un bucle sencillo que incrementa una variable N veces crecía en tiempo de forma cuadrática respecto a N, algo incompatible con un incremento lineal. Tras perfilar el código, descubrieron que el 87 % del tiempo (2,62 de 3,02 segundos para N=1000) se concentraba en la implementación de Tree Borrows, el modelo de aliasing más avanzado de Rust para código inseguro.
Tree Borrows modela cada referencia como un nodo dentro de un árbol cuyo estado evoluciona en una máquina de cinco estados. Cada acceso a memoria obliga a actualizar todos los nodos del árbol, de modo que un crecimiento descontrolado del árbol dispara el coste. La causa concreta resultó no ser la variable incrementada, sino el objeto Range del bucle for: sin optimizaciones —imprescindibles porque estas pueden ocultar comportamiento indefinido—, cada llamada a Iterator::next añade nueve nodos al árbol y realiza diez accesos, generando un patrón cuadrático de 45N² accesos a nodos.
La solución consistió en delegar al recolector de basura de OCaml la liberación de los nodos del árbol de Tree Borrows, aprovechando que el lenguaje ya cuenta con un GC maduro. Con apenas unas 40 líneas de código, el equipo pasó de tiempo cuadrático a lineal y obtuvo aceleraciones de hasta 10×. La entrada detalla el diagnóstico, las matemáticas del crecimiento del árbol y la filosofía de la corrección, e ilustra por qué Soteria no puede activar optimizaciones del compilador sin perder su capacidad de detectar errores.