Introducción

En el capítulo “Introducción a los hooks de almacenamiento y ghosts”, cubrimos los hooks de almacenamiento y los ghosts con variables de almacenamiento simples. Mostramos que los hooks hacen posible rastrear variables de almacenamiento que no son directamente accesibles a través de métodos públicos o externos. También demostramos que cuando ciertas cantidades no se almacenan explícitamente pero son requeridas para el razonamiento en las especificaciones, los hooks combinados con variables ghost pueden usarse para calcular y persistir esos valores.

Si estas variables hubieran sido públicas o accesibles externamente, sus valores podrían haberse leído fácilmente invocándolas directamente en CVL, lo que permitiría que cualquier cantidad derivada se calculara según fuera necesario.

Los mappings, sin embargo, son diferentes. No son enumerables: para acceder a un valor, uno ya debe conocer la clave, y no hay una forma incorporada de recuperar “todas las claves” o “todos los valores” de un mapping.

Esta limitación crea un gran desafío para la verificación: muchas propiedades importantes del contrato requieren razonar sobre todas las entradas de un mapping. Dado que no podemos enumerar o inspeccionar directamente todas las claves, necesitamos un mecanismo para realizar un seguimiento de los cambios en el mapping a medida que ocurren.

En este capítulo, extendemos el uso de los hooks Sstore más allá de los enteros, direcciones y booleanos, y los aplicamos a los mappings de almacenamiento, un patrón común en las especificaciones, ya que muchos contratos dependen en gran medida de los mappings.

Sintaxis del hook Sstore para mappings

Antes de continuar con las demostraciones de código, primero aprendamos la sintaxis / patrones de código de los hooks Sstore para mappings.

Hook Sstore — capturar los valores nuevo y antiguo

Aquí está la sintaxis del hook Sstore para capturar los valores nuevo y antiguo de un mapping de almacenamiento:

Copy
hook Sstore balances[KEY address user] uint256 newVal (uint256 oldVal) {
    // Implement hook logic for the balances mapping where:
		// - KEY is `user`
		// - old (previous) value is `oldVal`
		// - new (current) value is `newVal`
}

Siempre que se escribe un valor en un mapping, se pueden capturar tanto el valor antiguo como el nuevo.

Por ejemplo, para verificar que el balance de un usuario no aumenta en más de 10, calculamos la diferencia entre el balance antiguo y el nuevo y asignamos el resultado a la variable ghost g_balanceDelta:

Copy
ghost mathint g_balanceDelta;


hook Sstore balances[KEY address user] uint256 newVal (uint256 oldVal) {
    g_balanceDelta = newVal - oldVal;
}

El hook calcula el delta (newVal - oldVal) y lo almacena en la variable ghost g_balanceDelta, que representa cuánto cambia el balance de un usuario durante esa actualización de almacenamiento.

El valor g_balanceDelta puede usarse luego para verificar los límites de cambio. Por ejemplo:

Copy
rule deltaNotMoreThan10() {
    ...
    assert g_balanceDelta <= 10;
}

Hook Sstore — capturar solo el nuevo valor

Podemos elegir capturar solo el nuevo valor y omitir el valor antiguo, ya que este último es opcional:

Copy
hook Sstore balances[KEY address user] uint256 newVal {
	// implement hook logic
}

Esto se usa principalmente cuando el almacenamiento simplemente se está estableciendo y el delta (cambio) no se requiere en la lógica de verificación.

Por ejemplo, si queremos razonar que el balance de un usuario no excede 2000, solo necesitamos capturar newVal y asignarlo a una variable ghost:

Copy
ghost mathint g_balance;


hook Sstore balances[KEY address user] uint256 newVal {
	g_balance = newVal;
}

El valor g_balance puede usarse luego para verificar si un balance se mantiene dentro de los límites definidos. Por ejemplo:

Copy
rule balanceDoesNotExceed2000() {
	...
	assert g_balance <= 2000;
}

Es imposible rastrear todas las claves y valores en un mapping sin un hook Sstore

Para entender por qué los hooks son necesarios para verificar propiedades que involucran mappings, comencemos con un contrato simple, PointSystem, que hace lo siguiente:

• Añade puntos a un usuario específico e incrementa los puntos totales.
• Mantiene un registro por usuario en el mapping pointsOf[address].
• Rastre el total general en la variable totalPoints.

Copy
contract PointSystem {
    mapping (address => uint256) public pointsOf;
    uint256 public totalPoints;

    function addPoints(address _user, uint256 _amount) external {
        pointsOf[_user] += _amount;
        totalPoints += _amount;
    }
}

Ahora, verifiquemos la propiedad: “La suma de los puntos individuales de los usuarios es igual a los puntos totales.”

Sin usar un hook Sstore, un enfoque es trabajar con un número limitado de usuarios, por ejemplo, dos. Leemos sus balances directamente desde el mapping pointsOf, sumamos sus puntos y afirmamos que esta suma es igual a totalPoints.

La regla a continuación demuestra este enfoque, con totalPoints y todos los valores de pointsOf comenzando en cero:

Copy
rule sumOfUserPointsEqualsTotalPoints() {
    address account1; address account2; 
    uint256 amount1; uint256 amount2;   

    require account1 != account2;
    require pointsOf(account1) == 0 && pointsOf(account2) == 0; // points per user starts at zero
    require totalPoints() == 0; // total starts at zero

    addPoints(account1, amount1);
    addPoints(account2, amount2);

    assert to_mathint(totalPoints()) == pointsOf(account1) + pointsOf(account2);
}

En esta ejecución del Prover, vemos que la propiedad está verificada:

Ejecución del Prover: link

Al afirmar la igualdad usando solo dos usuarios (incluso si se añaden más manualmente declarando variables de cuenta adicionales), la propiedad se limita a ese subconjunto de cuentas. Esta no es la propiedad exacta que queremos verificar, ya que pueden existir muchos otros usuarios en el mapping cuyos puntos quedan excluidos de la comprobación.

Ahora, mejoremos la regla. Dejemos que totalPoints y los puntos de usuario (pointsOf[address]) comiencen en cualquier valor en lugar de cero eliminando las precondiciones require pointsOf(account1) == 0 && pointsOf(account2) == 0 y require totalPoints() == 0.

Luego registramos los valores de totalPoints y pointsOf[address] antes y después de la llamada al método addPoints(). Al hacerlo, nos permite calcular los deltas causados por la llamada y determinar cuánto ha cambiado cada variable.

Por último, afirmamos que los puntos totales (totalPointsAfter) son iguales a los puntos totales iniciales (totalPointsBefore) más la suma de los cambios en los puntos de account1 y account2. Este ajuste hace que la regla funcione independientemente del estado inicial:

Copy
rule sumOfUserPointsEqualsTotalPoints_modified() {
    address account1; address account2;
    uint256 amount1; uint256 amount2;

    require account1 != account2;

    // Capture the state BEFORE the method call
    mathint totalPointsBefore = totalPoints();
    mathint pointsOfAccount1Before = pointsOf(account1);
    mathint pointsOfAccount2Before = pointsOf(account2);

    // Method call
    addPoints(account1, amount1);
    addPoints(account2, amount2);

    // Capture the state AFTER the method call
    mathint totalPointsAfter = totalPoints();
    mathint pointsOfAccount1After = pointsOf(account1);
    mathint pointsOfAccount2After = pointsOf(account2);

    // Calculate how much each account's points changed
    mathint deltaPointsOfAccount1 = pointsOfAccount1After - pointsOfAccount1Before;
    mathint deltaPointsOfAccount2 = pointsOfAccount2After - pointsOfAccount2Before;

    // Assertion: The total points equal the initial total plus the changes in the points of account1 and account2
    assert totalPointsAfter == totalPointsBefore + deltaPointsOfAccount1 + deltaPointsOfAccount2;
}

Ejecución del Prover: link

Incluso con esta mejora en la regla, no representa con precisión la propiedad, ya que solo considera a dos usuarios específicos e ignora a todos los demás en el mapping. Solo demuestra que un subconjunto de usuarios es coherente con el total.

Rastrear todos los puntos de los usuarios es imposible sin un hook Sstore, incluso si el mapping es accesible externamente.

Uso del hook Sstore para enumerar los valores de un mapping de almacenamiento

Cada vez que el contrato escribe en pointsOf[address], el hook Sstore captura el nuevo valor y el valor antiguo, lo que le permite calcular el delta (cambio) y asignarlo a una variable ghost. En lugar de consultar el mapping directamente (desde el contrato) para todas las claves posibles, mantenemos un rastreador en forma de variable ghost que registra cada escritura en el almacenamiento a medida que ocurre.

Implementemos la lógica del hook Sstore. Como se mencionó, capturamos los valores antiguo y nuevo, calculamos el delta (cambio) y lo sumamos a una variable ghost para registrar los puntos totales. Declaramos esta variable ghost como g_sumOfUserPoints:

Copy
ghost mathint g_sumOfUserPoints;

hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
    g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}

Ahora que la suma de los puntos individuales de los usuarios es cuantificable en la variable ghost g_sumOfUserPoints, el siguiente paso es usarla en una regla o un invariante para comprobar que este rastreador siempre es igual a la variable de almacenamiento del contrato totalPoints.

Ghosts dentro de reglas e invariantes

Los ghosts pueden usarse tanto en reglas como en invariantes. En el siguiente ejemplo, verificamos que totalPoints (variable de almacenamiento) es igual a g_sumOfUserPoints (variable ghost), cuyo valor se rastrea y calcula en el hook Sstore.

Verificar que totalPoints() es igual a g_sumOfUserPoints como una regla

Aquí está la regla en forma paramétrica, donde f(e, args) permite al Prover verificar la regla contra todas las funciones del contrato con argumentos arbitrarios. Para la regla a continuación, requerimos que totalPoints y g_sumOfUserPoints comiencen en cero:

Copy
rule sumOfUserPointsEqualsTotalPoints(env e, method f, calldataarg args) {
    require totalPoints() == 0 && g_sumOfUserPoints == 0;

    f(e, args);
    assert totalPoints() == g_sumOfUserPoints;
}

Ejecución del Prover: link

Alternativamente, podemos permitir que totalPoints y g_sumOfUserPoints comiencen en cualquier valor, siempre y cuando comiencen en el mismo valor:

Copy
rule sumOfUserPointsEqualsTotalPoints_alt(env e, method f, calldataarg args) {
    require totalPoints() == g_sumOfUserPoints; // starts at any value, as long as they start at the same value
																						    
    f(e, args);
    assert totalPoints() == g_sumOfUserPoints;
}

Ejecución del Prover (verificado): link

Verificar que totalPoints() es igual a g_sumOfUserPoints como un invariante

Para verificar la misma propiedad de forma inductiva (caso base y paso de inducción), la escribimos como un invariante en CVL. El ghost se inicializa en cero, y aquí se aplica el mismo hook Sstore de la regla anterior:

Copy
ghost mathint g_sumOfUserPoints {
    init_state axiom g_sumOfUserPoints == 0;
}

hook Sstore pointsOf[KEY address account] uint256 newVal (uint256 oldVal) {
    g_sumOfUserPoints = g_sumOfUserPoints + newVal - oldVal;
}

invariant sumOfUserPointsEqualsTotalPoints_inv() 
    totalPoints() == g_sumOfUserPoints;

Ejecución del Prover (verificado): link

Al usar ghosts en un invariante en CVL, es necesario inicializarlos con un init_state axiom que establezca el valor inicial correcto; en este caso, cero para g_sumOfUserPoints.

Dado que los puntos de cada usuario comienzan en cero, la suma de todos los puntos de los usuarios (g_sumOfUserPoints) también comienza en cero. Esto importa porque, como parte del proceso de inducción, un invariante comprueba si la propiedad se cumple en el caso base (inmediatamente después del constructor).

Cuando verificamos esta propiedad como una regla anteriormente, probamos el caso en el que ambos comenzaban en cero y luego en un valor distinto de cero (pero igual). Como un invariante, solo probamos que ambos comiencen en cero.

La razón es que los invariantes deben comenzar a probarse inmediatamente después del constructor (el caso base), donde las variables de almacenamiento no inicializadas son cero por defecto. Esto significa que los invariantes solo pueden comenzar en valores distintos de cero si el constructor establece explícitamente esos valores. Las reglas, sin embargo, pueden asumir cualquier estado inicial arbitrario: puede ser cero o distinto de cero.

Resumen

• El uso de un hook Sstore es inevitable para los mappings al probar propiedades que involucran valores cambiantes. Resuelve el problema de la enumeración monitoreando las ranuras de almacenamiento y capturando los valores antiguo y nuevo para las claves del mapping.
• Sin un hook Sstore, las propiedades solo se pueden probar para un conjunto limitado de claves consultadas manualmente, en lugar de monitorear el almacenamiento directamente.
• En las reglas, los valores iniciales de las variables ghost están restringidos utilizando declaraciones require.
• En los invariantes, las variables ghost se inicializan utilizando el axioma init_state.

Este artículo forma parte de una serie sobre verificación formal utilizando el Certora Prover