Los bucles son una de las estructuras de programación más comunes, pero siguen siendo difíciles de razonar en la verificación formal. Aunque un bucle en Solidity o en cualquier otro lenguaje de programación parece simple —simplemente repite una acción hasta que se cumple una condición— su verificación se vuelve exponencialmente compleja. Un motor de verificación formal, como el Certora Prover, debe razonar sobre todas las cantidades posibles de iteraciones de un bucle, lo que lleva a lo que se conoce como el problema de explosión de rutas (path explosion): el aumento exponencial de las posibles rutas de ejecución que el Prover debe explorar a medida que aumenta el número de iteraciones del bucle o las ramificaciones condicionales.
Para gestionar esta complejidad, el Certora Prover y otras herramientas de verificación formal utilizan una técnica llamada desenrollo acotado de bucles (bounded loop unrolling). Esta técnica limita cuántas veces se explora simbólicamente un bucle durante la verificación, permitiendo al Prover evitar un espacio de búsqueda que de otro modo sería inviable causado por iteraciones de bucle desconocidas y no acotadas.
En este capítulo, vamos a:
- Explicar por qué los bucles son difíciles de verificar y cómo surge el problema de explosión de rutas.
- Mostrar cómo el Prover mitiga este problema utilizando el desenrollo acotado de bucles.
- Introducir dos banderas de configuración,
--loop_itery--optimistic_loop, que controlan cómo se exploran los bucles. - Discutir las fortalezas y limitaciones de estos enfoques, y por qué no pueden proporcionar una prueba completa y sólida para bucles desconocidos y no acotados.
Por qué los bucles son difíciles de verificar
Para entender por qué los bucles son difíciles de verificar, considera el siguiente contrato de Solidity que hace un seguimiento del número más grande añadido a un arreglo collection:
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract MaxInCollection {
uint256[] collection;
uint256 public maxInCollection = 0;
function addToCollection(uint256 x) public {
if (x > maxInCollection) {
maxInCollection = x;
}
collection.push(x);
}
function returnMax() public view returns (uint256) {
uint256 maxTmp = 0;
for (uint256 i = 0; i < collection.length; i++) {
if (collection[i] > maxTmp) {
maxTmp = collection[i];
}
}
return maxTmp;
}
}
En el contrato anterior, la función addToCollection() añade un nuevo elemento al arreglo collection. También actualiza la variable de estado maxInCollection cada vez que el nuevo elemento excede el máximo actual. El contrato también incluye returnMax(), que itera a través del arreglo para calcular y devolver el valor máximo.
La propiedad central (invariante) que este contrato debería mantener es simple: maxInCollection debería ser siempre igual al valor devuelto por returnMax().
Vamos a verificar esto formalmente expresándolo como un invariante en CVL:
methods {
function maxInCollection() external returns(uint256) envfree;
function returnMax() external returns(uint256) envfree;
}
invariant maxEqReturnMax()
maxInCollection() == returnMax();
A primera vista, esta afirmación parece válida y esperamos que el Prover la verifique con éxito. Sin embargo, cuando la ejecutamos a través del Certora Prover, la verificación falla, como se muestra a continuación:
Después de ver el resultado de la verificación, podrías estar confundido: si ambas funciones son lógicamente equivalentes en lo que devuelven, ¿por qué el Prover sigue fallando en establecer esa equivalencia?
La respuesta reside en la diferencia fundamental entre cómo la EVM ejecuta un programa y cómo el Prover razona sobre él: la EVM ejecuta una ruta específica con entradas concretas, mientras que el Prover explora todas las rutas posibles con entradas simbólicas.
Para entender esta diferencia, primero examinemos qué sucede durante la ejecución del contrato y luego contrastémoslo con cómo el Prover razona simbólicamente.
Un programa sigue una ruta concreta
Cuando ejecutamos este contrato en la práctica con entradas concretas (valores específicos y reales), el programa sigue una única ruta concreta determinada por estas entradas y la secuencia de llamadas a funciones.
Por ejemplo:
- Supongamos que llamamos a
addToCollection(7),addToCollection(5), yaddToCollection(9)en ese orden. - El arreglo
collectionse convierte en[7, 5, 9], ymaxInCollectionse actualiza a 9. - Cuando más tarde llamamos a
returnMax(), la función itera sobre el arreglo tres veces y calcula el valor máximo 9. - Por lo tanto, tanto
maxInCollectioncomoreturnMax()devuelven el mismo resultado, confirmando que el valor máximo se rastrea correctamente.
Así que en la ejecución concreta, el programa sigue una ruta única y determinista definida por las entradas dadas y el contenido del arreglo, y ambas funciones devuelven el mismo valor.
El Prover razona sobre todas las entradas a la vez
El Certora Prover es un motor de ejecución simbólica, lo que significa que no prueba el programa con una entrada a la vez. En cambio, razona sobre todas las ejecuciones posibles simultáneamente.
Para lograr esto, el Prover simula simbólicamente el comportamiento del programa paso a paso, razonando sobre restricciones lógicas en lugar de valores concretos.
Así es como el Prover aborda el invariante maxEqReturnMax(), paso a paso:
- Comprobación del estado inicial (Caso base): El primer paso es comprobar si el invariante se cumple inmediatamente después de que el constructor del contrato termine de ejecutarse.
- En este estado, el arreglo
collectionestá vacío, por lo quecollection.lengthes0. - La variable de estado
maxInCollectionse inicializa en0. - Luego, el Prover ejecuta simbólicamente la función
returnMax(). InicializamaxTmpen 0 y se encuentra con el bucle:
- En este estado, el arreglo
for (uint256 i = 0; i < collection.length; i++)
Dado que collection.length es 0 en el estado inicial, el cuerpo del bucle nunca se ejecuta, y la función simplemente devuelve maxTmp, que sigue siendo 0.
Como resultado, el invariante se cumple en el estado inicial, lo que significa que el caso base se verifica con éxito, como se muestra a continuación:
-
El paso inductivo: Después de confirmar que el invariante se cumple en el estado inicial, el Prover pasa a la siguiente fase: el paso inductivo. Este paso consiste en asegurar que el invariante continúe cumpliéndose después de cualquier cambio de estado en el contrato.
En términos simples, el Prover comprueba lo siguiente:
“Si el invariante se cumple en el estado actual S, entonces también debe cumplirse en el siguiente estado S′ que resulta de cualquier llamada de función válida.”
Para razonar sobre esto, el Prover sigue conceptualmente tres etapas:
a. Suposición antes de la llamada (Before the Call Assumption): El Prover comienza considerando un estado válido arbitrario
Sen el que el invariante ya se cumple. Esto forma la hipótesis inductiva, un paso estándar en el razonamiento inductivo. El Prover no necesita conocer el contenido real del arreglocollectiono el valor demaxInCollection; asume —como parte del propio método de prueba— que en este estadoS, la propiedadmaxInCollection() == returnMax()es verdadera.b. Ejecución simbólica: A continuación, el Prover simula una llamada de función que podría cambiar el estado del contrato. En nuestro caso, elige
addToCollection(). Crucialmente, no elige un valor específico como5o10como entrada paraaddToCollection(). En su lugar, utiliza una variable simbólica, x, que representa cualquier valor posible deuint256que la función podría recibir.Luego, el Prover ejecuta simbólicamente el cuerpo de
addToCollection(x):-
Ve la declaración
if:if (x > maxInCollection). Dado que tantoxcomomaxInCollectionson simbólicos, el Prover se ramifica, considerando ambas posibilidades:Caso 1:
x > maxInCollection. El nuevo estadoS'tendrámaxInCollectionactualizado ax.Caso 2:
x <= maxInCollection. El nuevo estadoS'tendrámaxInCollectionsin cambios.
En ambos casos, ejecuta simbólicamente
collection.push(x). Esto significa que el arreglocollectionen el estadoS'es ahora elcollectiondel estadoSmás el nuevo elementox, ycollection.lengthha aumentado en 1.El Prover tiene ahora una descripción simbólica completa del nuevo estado,
S', en términos del estado anteriorSy de la entrada simbólicax.c. Verificación después de la llamada (After Call Verification): En el paso final, el Prover debe demostrar ahora que el invariante se cumple en el nuevo estado
S'. Se pregunta: ¿EsmaxInCollection()(en el estado S’) ==returnMax()(en el estado S’)?Para completar este paso, el Prover analiza ambos lados de esta ecuación:
-
LHS (
maxInCollection()): Esto es directo. El Prover conoce simbólicamente el nuevo valor demaxInCollection(es el valor antiguo ox). -
RHS (
returnMax()): A continuación, ejecutará simbólicamente la funciónreturnMax(). Este es el punto en el que la verificación se vuelve un desafío, porquereturnMax()contiene un bucle:
-
for (uint256 i = 0; i < collection.length; i++) {...}
¿Por qué el bucle es un problema?
Cuando el Prover alcanza la función returnMax(), necesita ejecutar simbólicamente el bucle:
for (uint256 i = 0; i < collection.length; i++) {...}
En una ejecución concreta, el bucle se ejecuta una cantidad específica de veces, una vez por cada elemento en el arreglo.
Pero para el Certora Prover, la longitud del arreglo es simbólica, por lo que el número de iteraciones es desconocido.
Este es el punto crítico: el Prover debe considerar todas las longitudes de arreglo posibles a la vez, desde un arreglo vacío hasta el tamaño máximo representable. Solo eso ya crea un enorme espacio de búsqueda.
Dentro del bucle, hay otra condicional:
if (collection[i] > maxTmp)
Para entradas simbólicas, esta condición puede ser true o false en cada iteración.
Por lo que cada iteración duplica el número de rutas simbólicas que el Prover debe considerar.
Si la longitud del arreglo es n, el Prover se enfrenta aproximadamente a 2ⁿ rutas.
Por ejemplo:
- 2 elementos ⇒ 4 rutas (2²)
- 3 elementos ⇒ 8 rutas (2³)
- 10 elementos ⇒ 1024 rutas (2¹⁰)
- Para una longitud simbólica (no acotada) → es efectivamente inmanejable
Este crecimiento exponencial es lo que hace que sea prácticamente inviable para el Prover explorar todas las rutas en un tiempo o con recursos razonables.
El enfoque del Prover para abordar el problema de explosión de rutas
Como se mencionó anteriormente, el Certora Prover utiliza el desenrollo acotado de bucles para manejar este problema. La técnica limita cuántas veces se explora un bucle durante la verificación, con el límite predeterminado establecido en una iteración. Una vez que se alcanza este límite, el Prover deja de explorar más allá porque cada iteración adicional duplica el número de rutas simbólicas que debe analizar. Como resultado, las rutas restantes quedan sin demostrar.
En la verificación formal, demostrar un invariante requiere mostrar que se cumple para cada transición de estado posible, incluyendo todas las iteraciones de cualquier bucle. Si queda incluso una posible ruta sin revisar, el paso inductivo de la prueba queda incompleto. Es por eso que el Prover marca el invariante maxEqReturnMax() como fallido:
Es muy importante entender que cualquier cálculo con un número no acotado de pasos es difícil de razonar simbólicamente para el Prover. Y esta dificultad no se limita a los bucles for/while en tu código de Solidity. El mismo problema aparece incluso en lugares donde no hay ningún bucle explícito visible. Examinemos un ejemplo concreto de tales bucles ocultos: los strings de Solidity.
El string de Solidity: El caso clásico de los bucles ocultos
Para entender cómo los strings provocan errores del tipo “unwinding condition in a loop”, considera el siguiente contrato inteligente que almacena un string en la variable de estado txt y permite que cualquiera lo actualice a través de setTxt():
// SPDX-License-Identifier: MIT
pragma solidity 0.8.25;
contract Example {
string public txt;
function setTxt(string memory _txt) external {
txt = _txt;
}
}
Ahora, considera la siguiente especificación que intenta demostrar que el string almacenado siempre es igual a la entrada:
methods{
function setTxt(string) external envfree;
function txt() external returns(string) envfree;
}
rule storedStringShouldEqualToInput() {
string _txt;
//call
setTxt(_txt);
//assertions
assert _txt == txt();
}
Si ejecutas el Prover con esta especificación, la regla falla:
Y verás el conocido error “Unwinding condition in a loop”, al igual que en el ejemplo anterior que involucraba un bucle explícito.
Podrías estar preguntándote por qué aparece este error cuando el código no contiene ningún bucle explícito.
La razón es simple: un bucle oculto.
En Solidity, un string no es un valor único, sino un arreglo dinámico de bytes. Sin embargo, debido a la arquitectura de palabras de 256 bits de la EVM, cuando trabajas con arreglos dinámicos, el compilador y la EVM los manejan copiando fragmentos de 32 bytes a la vez.
Esta copia repetida, basada en palabras, es el bucle oculto que el Prover encuentra en el bytecode compilado.
En nuestra especificación, se desencadenan cuatro bucles ocultos durante el manejo del string:
-
Copia de
calldataamemory(La entrada)- Qué sucede: Cuando llamas a
setTxt(_txt), el string de entrada llega a un área de almacenamiento temporal de solo lectura llamadacalldata. Para usar o procesar realmente ese string dentro de la función, la EVM primero debe moverlo al espacio de trabajo de la función, llamadomemory. - El bucle: Esta transferencia se realiza en bloques de 32 bytes a la vez. La EVM entra en bucle hasta que todo el string se ha movido de
calldataamemory.
- Qué sucede: Cuando llamas a
-
Copia de
memoryastorage(La asignación)- Qué sucede: La asignación
txt = _txt;guarda el string de forma permanente. Mueve los datos del espacio de trabajo temporal enmemoryalstoragedel contrato, que es donde reside el estado de tu contrato en la blockchain. - El bucle: Dado que esta es una escritura permanente, la EVM ejecuta un bucle para copiar el string palabra por palabra (32 bytes a la vez) en las ranuras de almacenamiento designadas del contrato. Este es el punto principal de falla para la verificación.
- Qué sucede: La asignación
-
Copia de
storagede vuelta amemory(La lectura)- Qué sucede: Cuando llamas al getter público
txt(), el contrato tiene que recuperar los datos del string almacenado. Carga el string desde su ubicación permanente enstoragede vuelta a la memoria temporalmemorypara que pueda ser devuelto. - El bucle: Se ejecuta otro bucle interno más, leyendo las palabras de 32 bytes del string desde el almacenamiento una por una.
- Qué sucede: Cuando llamas al getter público
-
Comparación de strings (La aserción)
- Qué sucede: En tu aserción,
assert _txt == txt();, el Prover debe comprobar si los dos strings simbólicos son iguales. - El bucle: La única forma de comprobar la igualdad de dos arreglos dinámicos es compararlos palabra por palabra desde el principio hasta el final, lo cual es la definición de un bucle oculto final.
- Qué sucede: En tu aserción,
Para una ejecución concreta (ejecutar el código con una entrada específica, como el string "Hello"), este bucle oculto es simple. La longitud del string es un número conocido y fijo, por lo que el bucle se ejecuta una cantidad definida de veces. Todo es predecible.
Sin embargo, para un motor de ejecución simbólica como el Certora Prover, la entrada _txt no es un string fijo. Es un valor simbólico, lo que significa que representa todos los strings posibles a la vez, desde un string vacío hasta uno de tamaño máximo.
Ahora el Prover se ve obligado a razonar sobre una familia de ejecuciones no acotada. Tiene que comprobar si la propiedad se cumple, sin importar la longitud del string o los bytes que contenga. Esto crea dos grandes problemas:
Problema 1: Tamaño de bucle desconocido (La búsqueda no acotada)
El primer desafío surge porque la longitud del string es simbólica (desconocida). Esto significa que el contador del bucle que controla el proceso de copiado de 32 bytes también es simbólico.
- Para un string específico, el bucle se ejecuta un número determinado de veces (por ejemplo, exactamente 3 veces).
- Para el Prover, el bucle podría ejecutarse cualquier cantidad de veces (por ejemplo, 0, 1, 10 o 100 veces).
Por lo tanto, el Prover debe comprobar no solo una ruta de ejecución, sino toda una familia de rutas, una correspondiente a cada longitud posible que podría tener el string. Aunque esto por sí solo crea un enorme espacio de búsqueda técnicamente no acotado, este problema empeora exponencialmente debido al segundo problema: las ramificaciones dentro del bucle.
Problema 2: Ramificación exponencial (El efecto de duplicación)
El número total de rutas explota porque el bucle oculto frecuentemente encuentra comprobaciones condicionales (como comparar la palabra actual de 32 bytes). Dado que el Prover no conoce el contenido del string simbólico, no puede determinar el resultado de la comprobación.
Para garantizar la corrección, el Prover debe explorar ambas posibilidades simultáneamente. Esto fuerza a que la ruta de ejecución se bifurque, requiriendo que el Prover explore las consecuencias de que la condición sea true y que la condición sea false. Esta exploración efectivamente duplica el número de rutas de ejecución con cada iteración del bucle.
Por ejemplo:
- Si el bucle oculto se ejecuta solo 3 veces, y hay una comprobación condicional en cada iteración, el Prover debe analizar
2 x 2 x 2 = 8rutas separadas. - Si el string simbólico es lo suficientemente largo como para desencadenar 10 iteraciones del bucle, el Prover tiene que analizar
2^10 = 1.024rutas.
Esta combinación de longitud no acotada y ramificación exponencial es lo que crea el problema de explosión de rutas, haciendo que el proceso de verificación sea rápidamente imposible a nivel computacional.
El Prover se ve abrumado por el enorme y rápido crecimiento del número de posibles rutas de ejecución y se ve obligado a dejar de explorar el bucle después de un número fijo de iteraciones mediante el desenrollo acotado de bucles.
Debido a que el Prover no puede comprobar todas las rutas posibles (es decir, no puede desenrollar completamente el bucle para todas las longitudes simbólicas), la prueba se considera incompleta. Por lo tanto, no puede demostrar que la propiedad se cumple para todos los strings posibles, que es la razón por la que la regla storedStringShouldEqualToInput() falla al verificarse con éxito.
Revisitando la “Causa”
Podemos ver que el Prover falló al verificar ambas reglas: maxEqReturnMax() y storedStringShouldEqualToInput(), no porque las propiedades sean falsas, sino porque el Prover no puede terminar de razonar sobre ellas.
- En el caso de
maxEqReturnMax(), el bucle dentro dereturnMax()puede, en principio, ejecutarse hasta2²⁵⁶−1veces —una vez por cada elemento posible en el arreglo. Si denotamos la longitud del arreglo comon, el Prover debe intentar desenrollar el bucle para cada valor posible den, lo cual es inviable computacionalmente. - En el caso de
storedStringShouldEqualToInput(), el bucle oculto dentro detxt = _txtpuede ejecutarse una vez por cada 32 bytes en el string. Dado que la longitud de la entrada es simbólica, el Prover debe considerar todas las longitudes de string posibles, lo que de nuevo conduce a una exploración no acotada.
En ambos casos, la causa raíz es la misma: el Prover no puede explorar simbólicamente un número no acotado de iteraciones de un bucle.
Esto nos deja con una pregunta: ¿qué opciones tenemos para manejar estos casos?
La “Solución”: Banderas de configuración
El Certora Prover proporciona dos opciones de configuración para ayudar a lidiar con los bucles. Aunque estas no proporcionan pruebas completas de corrección, son herramientas útiles para controlar el comportamiento del Prover.
1. Aumentar el límite de desenrollo con loop_iter
La primera y más directa opción es indicarle al Prover que desenrolle el bucle más veces usando la bandera --loop_iter. Esto puede hacerse desde la terminal o a través del archivo de configuración.
Desde la terminal:
certoraRun confs/<your-config-file>.conf --loop_iter <N>
O dentro de un archivo de configuración:
{
"files": [
"contracts/<YourContract>.sol:<ContractName>"
],
"verify": "<ContractName>:specs/<your-spec-file>.spec",
"loop_iter": "<N>"
}
En el comando de la terminal y en los ejemplos del archivo de configuración anteriores, <N> especifica el número máximo de iteraciones del bucle que el Prover explorará antes de detenerse**.**
Uso de la bandera loop_iter en nuestra regla
Para entender cómo funciona la bandera --loop_iter en la práctica, apliquemos esto a nuestro ejemplo de string y ejecutemos el Prover con el siguiente comando:
certoraRun confs/example.conf --loop_iter 3
Cuando ejecutamos el Prover con el comando anterior, esto es lo que va a suceder en la práctica:
- El Prover ahora desenrollará hasta 3 iteraciones del bucle oculto (el bucle de copiado de bytes dentro de
txt = _txt). - Dado que cada iteración copia una palabra de 32 bytes, esto significa que el Prover puede verificar con éxito la propiedad para strings de hasta 96 bytes (3 × 32 = 96) de longitud.
- Sin embargo, para strings de más de 96 bytes, el Prover alcanza su límite de desenrollo. En ese punto, esas rutas quedan sin demostrar.
- Como resultado, la regla
storedStringShouldEqualToInput()seguirá fallando en el caso general, ya que el Prover no puede probar la corrección para todas las longitudes de string.
El resultado será el mismo sin importar cuánto aumentes el límite: cualquier --loop_iter finito solo prueba la propiedad para strings de hasta ese número de palabras de 32 bytes. Los strings más grandes quedan sin demostrar, y aumentar el límite ralentiza rápidamente el Prover.
2. Omitir más allá del límite con optimistic_loop
La segunda opción adopta un enfoque muy diferente. En lugar de aumentar el límite, se le puede decir al Prover que asuma que todo más allá del límite funciona bien. Eso es lo que hace --optimistic_loop.
Desde la terminal:
certoraRun confs/<your-config-file>.conf --optimistic_loop
O dentro de un archivo de configuración:
{
"files": [
"contracts/<YourContract>.sol:<ContractName>"
],
"verify": "<ContractName>:specs/<your-spec-file>.spec",
"optimistic_loop": true
}
Normalmente, cuando el Prover alcanza el límite de su bucle y ve que el bucle podría continuar, marca esa ruta como sin demostrar.
Con --optimistic_loop, el Prover cambia de estrategia:
- Para las iteraciones dentro del límite, se comporta de forma normal y comprueba cada caso.
- Para las iteraciones más allá del límite, asume que la propiedad se seguirá cumpliendo sin explorar realmente esas rutas.
Uso de la bandera optimistic_loop en nuestra regla
Para entender cómo funciona la bandera --optimistic_loop en la práctica, apliquemos esto a nuestro ejemplo de string y ejecutemos el Prover con el siguiente comando:
certoraRun confs/example.conf --optimistic_loop
Cuando ejecutamos el Prover con el comando anterior, esto es lo que va a suceder en la práctica:
- El Prover todavía explora el bucle por un pequeño número de iteraciones (su límite de desenrollo predeterminado).
- Una vez que alcanza ese límite, en lugar de reportar un error de “unwinding condition in a loop”, asume que la propiedad se sigue cumpliendo para todos los casos restantes.
- Como resultado, la regla
storedStringShouldEqualToInput()pasa ahora la verificación, a pesar de que las longitudes de string mayores nunca se comprobaron completamente.
Este enfoque se llama “optimista” porque el Prover esencialmente espera que lo que vio en las primeras iteraciones siga siendo cierto para todas las futuras.
Podemos ver que con --loop_iter, el Prover explora solo hasta el límite (3 iteraciones en nuestro ejemplo). Cualquier cosa más larga queda sin demostrar, por lo que la verificación falla. Sin embargo, con --optimistic_loop, el Prover toma un atajo: asume que si la propiedad se cumple dentro del límite explorado, también se cumple más allá de él. Esto elimina el fallo de desenrollo y hace que la regla pase.
Aunque estas banderas son útiles para la depuración y la gestión de la verificación, ninguna proporciona una prueba completa y sólida para bucles desconocidos y no acotados.
--loop_iteres incompleta.--optimistic_loopes no sólida (hace suposiciones).
Resumen
En este capítulo, vimos por qué los bucles, tanto explícitos como ocultos, plantean un desafío tan grande en la verificación formal. En ambas situaciones, el Prover no puede explorar simbólicamente un número desconocido y no acotado de iteraciones. Para avanzar, se apoya en dos banderas de configuración: --loop_iter y --optimistic_loop
La bandera --loop_iter aumenta el número de iteraciones exploradas, pero esto solo demuestra la corrección para entradas pequeñas y, por lo tanto, sigue siendo incompleta. La bandera --optimistic_loop permite al Prover omitir más allá del límite asumiendo la corrección, pero esa suposición puede ser incorrecta, lo que lo hace no sólido.
Estas alternativas son útiles para depurar, realizar comprobaciones rápidas o detectar errores superficiales. Sin embargo, no pueden proporcionar una prueba completa cuando se trata de bucles no acotados.
Este artículo forma parte de una serie sobre verificación formal usando Certora Prover