En el capítulo anterior, aprendimos cómo las variables fantasma permiten que la información fluya desde los hooks hacia las reglas. También aprendimos que:
- Al inicio de la ejecución de verificación, el Prover elige valores arbitrarios (havoced) para las variables fantasma.
- Las variables fantasma se tratan como una extensión del almacenamiento del contrato. Si una transacción se revierte durante la ejecución simbólica, el Prover también revierte cualquier actualización ghost de esa ruta, manteniéndolas consistentes con el estado de almacenamiento del contrato.
El segundo caso no suele ser una preocupación, ya que revertir valores ghost durante las transacciones refleja el comportamiento normal del almacenamiento. Sin embargo, el primer caso puede conducir a resultados de verificación incorrectos o engañosos.
En este capítulo, demostraremos cómo este problema puede afectar la verificación y explicaremos cómo solucionarlo estableciendo consistencia entre las variables fantasma y el estado del contrato utilizando la declaración require.
Entendiendo el Peligro de los Ghosts no Restringidos
Para ver cómo una variable fantasma no restringida puede afectar la verificación, repasemos el contrato Counter utilizado en capítulos anteriores.
//SPDX-License-Identifier: MIT
pragma solidity 0.8.24;
contract Counter {
uint256 public count;
function increment() external {
count++;
}
}
Considere la especificación a continuación, que tiene como objetivo verificar que cada llamada a la función increment() aumente correctamente la variable count. Asegura que el cambio total en count coincida con el número de veces que se invocó la función, tal como lo rastrea la variable fantasma countIncrementCall.
methods {
function increment() external envfree;
function count() external returns (uint) envfree;
}
// Ghost variable to track how many times the `count` variable is updated
ghost mathint countIncrementCall;
// Hook triggered before `count` is updated via SSTORE
hook Sstore count uint256 updatedValue (uint256 prevValue) {
// Increment the ghost each time `count` is about to be modified
countIncrementCall = countIncrementCall + 1;
}
/*
*Rule to verify that count increases by exactly the number of times increment()
is called
*/
rule checkCounterIncrements() {
// Capture the value of `count` before any updates
mathint precallCountValue = count();
// Perform three increment operations
increment();
increment();
increment();
// Capture the value of `count` after updates
mathint postCallCountValue = count();
// Assert that `count` increased by the same amount as tracked by the ghost
assert postCallCountValue == precallCountValue + countIncrementCall;
}
La especificación anterior hace lo siguiente:
- Declaramos una variable fantasma,
countIncrementCall, de tipomathintpara que actúe como nuestro contador independiente. - Usamos un hook
Sstoreque observa la variablecount. Cada vez que el contrato escribe un nuevo valor encount, este hook se activa e incrementa el ghostcountIncrementCall. - La regla
checkCounterIncrementsestablece un escenario de prueba. Lee el valor inicial decount, llama aincrement()tres veces y luego lee el valor final. - Finalmente, afirma que el conteo final debe ser igual al conteo inicial más el número de incrementos rastreados por nuestro ghost. Dado que llamamos a
increment()tres veces,countIncrementCalldebería ser 3, por lo que se espera que la aserción se cumpla.
A primera vista, esta especificación parece lógicamente sólida. Sin embargo, cuando se ejecuta a través del Certora Prover, falla al verificar la regla checkCounterIncrements, como se muestra en la salida ilustrada a continuación:
Para entender por qué falla la aserción, analicemos la traza de llamadas (call trace) proporcionada por el Prover.
Por Qué Falló la Verificación
Nuestro análisis de la traza de llamadas revela que la regla no falló debido a un defecto en la lógica, sino porque la variable fantasma countIncrementCall comenzó con un valor elegido de manera adversarial por el Prover, en este caso -0x2 (o -2). Es importante destacar que este valor no se eligió por error. En cambio, fue asignado intencionalmente a través de un proceso sistemático conocido como havocing.
El havocing es el mecanismo mediante el cual el Prover asigna valores iniciales arbitrarios (no restringidos) a variables de estado o fantasma. “Arbitrario” aquí significa que la variable es libre de tomar cualquier valor dentro del rango de su tipo. Al hacerlo, el Prover puede examinar sistemáticamente casos extremos y escenarios límite que podrían causar un fallo de verificación. Esta técnica hace que el proceso de verificación sea exhaustivo, permitiendo al Prover razonar sobre todos los estados posibles que el contrato podría alcanzar.
En este caso en particular, la variable de almacenamiento count comenzó en 0xA (10 en decimal), mientras que countIncrementCall comenzó en -2. Después de llamar a increment() tres veces, count alcanzó 0xD (13 en decimal), y la variable fantasma aumentó de -2 a 1. Sin embargo, la aserción esperaba:
postCallCountValue == precallCountValue + countIncrementCall;
lo cual, sustituyendo los valores reales, se convirtió en:
13 == 10 + 1
Esto es claramente falso, por lo tanto, la verificación falló.
La “Lección” a Recordar
Este fallo destaca un concepto importante sobre cómo opera el Prover. Durante la verificación, el Prover no asume ningún valor inicial predeterminado o definido por el constructor ni para el almacenamiento del contrato ni para las variables fantasma. En su lugar, les aplica havoc — asignando valores simbólicos arbitrarios dentro de su rango permitido. Este comportamiento permite al Prover razonar sobre todos los estados iniciales posibles del contrato, asegurando que las propiedades se mantengan universalmente, no solo para configuraciones iniciales específicas.
Si bien este enfoque hace que la verificación sea exhaustiva, también puede introducir condiciones iniciales poco realistas. Si una regla depende de una relación significativa entre el almacenamiento del contrato y una variable fantasma, el havocing puede romper esa relación al iniciarlas desde valores no relacionados. Por ejemplo, un ghost que represente el número de llamadas a increment() podría comenzar con -2 o 5, a pesar de que aún no ha ocurrido ninguna llamada a la función increment().
Cuando eso sucede, la regla podría fallar — no porque su lógica sea defectuosa, sino porque la verificación comenzó desde un estado que nunca podría existir en la práctica. Estos fallos son falsos positivos: resaltan un desajuste entre la inicialización simbólica y la intención semántica en lugar de un problema real en el contrato.
Cuál es la “Solución”
La clave para evitar estos falsos fallos es asegurar que la relación inicial entre una variable fantasma y el almacenamiento del contrato sea lógicamente correcta antes de que comience la verificación. Esto no significa fijar sus valores exactos, sino más bien restringirlos para que comiencen en un estado que tenga sentido.
Por ejemplo, en nuestra regla, la variable fantasma countIncrementCall está destinada a representar el número de veces que se ha invocado increment(). Al inicio de la regla, antes de que ocurra cualquier llamada, este número debe ser cero. La variable count del contrato podría comenzar en cualquier valor — 0, 10 o 100 — pero el ghost siempre debería comenzar en 0, ya que aún no han ocurrido incrementos.
Para imponer tal consistencia lógica, usamos la declaración require en CVL. En CVL, una declaración require actúa como una precondición lógica, indicando al Prover que explore todos los comportamientos posibles solo desde estados iniciales que satisfagan esa relación especificada. Al agregar una restricción simple como:
require countIncrementCall == 0;
Filtramos efectivamente configuraciones sin sentido donde el valor inicial del ghost contradice su significado previsto.
Con esta restricción en su lugar, el Prover sigue realizando una exploración adversarial, pero lo hace comenzando desde estados semánticamente válidos. Esto asegura que cualquier fallo de verificación que ocurra después de aplicar la restricción corresponda a un problema real en la regla o en la lógica del contrato — no a un efecto secundario de la inicialización arbitraria.
Restringiendo los Ghosts con la Declaración require
Como se discutió anteriormente, en nuestro caso, la variable fantasma countIncrementCall está destinada a representar el número de veces que se ha llamado a la función increment(). Al inicio de la ejecución de la regla, aún no ha ocurrido ninguna de estas llamadas — lo que significa que el valor inicial correcto para este ghost debería ser cero.
Podemos codificar esta restricción directamente en nuestra regla simplemente agregando require countIncrementCall == 0; al principio de la regla.
// Rule to verify that `increment()` increases `count` by exactly the number of times it's called
rule checkCounterIncrements() {
//Add the require statement to constrain the ghost
require countIncrementCall == 0;
// Capture the value of `count` before any updates
mathint precallCountValue = count();
// Perform three increment operations
increment();
increment();
increment();
// Capture the value of `count` after updates
mathint postCallCountValue = count();
// Assert that `count` increased by the same amount as tracked by the ghost
assert postCallCountValue == precallCountValue + countIncrementCall;
}
Al incluir esta precondición, aseguramos que el Prover inicie la ejecución de la regla en un estado lógicamente significativo, donde el almacenamiento del contrato y la semántica del ghost están alineados. El Prover todavía realiza una exploración simbólica y adversarial completa, pero ahora evita explorar estados imposibles, como que la variable fantasma countIncrementCall comience en -2 o 5.
Cuando se vuelve a ejecutar la verificación, tanto count como countIncrementCall comienzan en estados lógicamente consistentes. Sus valores pueden diferir — por ejemplo, count podría comenzar en 10 y countIncrementCall en 0 — sin embargo, su relación sigue siendo sólida.
A partir de aquí, cada llamada a increment() actualiza tanto el almacenamiento del contrato como el ghost en perfecta sincronía. Después de tres llamadas, count aumenta en tres, y countIncrementCall también registra tres actualizaciones. Como resultado, la aserción
assert postCallCountValue == precallCountValue + countIncrementCall;
se mantiene en todas las rutas de ejecución válidas, confirmando que la regla ahora se verifica con éxito.
Esto demuestra cómo una sola línea require countIncrementCall == 0 puede eliminar falsos fallos de verificación al anclar el análisis del Prover a un punto de partida lógicamente sólido. No limita el alcance de la verificación; en cambio, asegura que el espacio de exploración sea semánticamente válido y que cualquier fallo de la regla refleje un problema lógico genuino en lugar de un artefacto de inicialización arbitrario.
Sin embargo, hay una suposición importante en esta especificación que merece una reflexión más profunda.
Aquí, el ghost countIncrementCall se incrementa con las escrituras en la ranura de almacenamiento de count, lo cual funciona porque count actualmente solo se modifica dentro de increment(). Pero, ¿qué pasaría si otra función —digamos, reset() o setCount()— también modificara count? El ghost aún se incrementaría, aunque no se haya llamado a increment().
Esto resalta una importante consideración de diseño: la elección de a qué aplicarle un hook determina qué es lo que realmente rastrea el ghost. En este caso, estamos rastreando escrituras en el almacenamiento (storage writes), no llamadas a funciones. Para contratos simples, estos pueden ser equivalentes, pero a medida que los contratos se vuelven más complejos, esa equivalencia puede romperse. Exploraremos estrategias alternativas de hooks que abordan esta limitación en un capítulo posterior.
Conclusión
Las variables fantasma no restringidas pueden llevar al Prover a explorar estados poco realistas, lo que resulta en fallos de verificación engañosos. Al restringir sus valores iniciales utilizando una declaración require, podemos asegurarnos de que los ghosts comiencen en un estado que se alinee lógicamente con el almacenamiento del contrato. Este pequeño pero crucial paso mantiene la verificación tanto exhaustiva como semánticamente válida, permitiendo al Prover informar solo sobre problemas lógicos genuinos.
Este artículo es parte de una serie sobre verificación formal usando el Certora Prover