Titulación DCC

Los tipos refinados (liquid types) extienden los sistemas de tipos tradicionales con anotaciones lógicas, permitiendo verificar automáticamente que un programa cumple garantías de corrección en tiempo de compilación.

Liquid Fixpoint es el motor que sirve de base a implementaciones de esta idea, tales como Flux y LiquidHaskell. Su función es tomar condiciones de verificación, expresadas como Horn clauses (implicaciones lógicas entre predicados), y determinar su satisfacibilidad mediante el uso de un solver SMT (como Z3). Fue escrito hace más de una década, y desde entonces se ha acumulado conocimiento sobre cómo construir este tipo de solvers de forma más eficiente. Además, sigue atado al toolchain de GHC, lo que genera fricción para integrarlo a proyectos más nuevos (e.j., no se puede linkear estáticamente). 

Este proyecto propone construir un solver de Horn clauses en Rust funcionalmente equivalente a Liquid Fixpoint, aprovechando ese conocimiento acumulado para mejorar su diseño, y buscando dos beneficios: mejor rendimiento y menor overhead de runtime respecto a Haskell, y una integración directa con herramientas del ecosistema Rust como Flux. El trabajo incluye una evaluación empírica: correr la implementación contra la batería de tests existente de Liquid Fixpoint para verificar equivalencia funcional, y realizar benchmarks de desempeño (tiempo de ejecución, uso de memoria) comparando ambas implementaciones en casos de prueba representativos.