En CVL, el tipo mathint representa enteros sin límite, a diferencia de los tipos de tamaño fijo de Solidity como uint256. Realiza operaciones aritméticas sin overflow ni underflow, lo que permite razonar basándose en matemáticas puras. Por lo tanto, expone situaciones de overflow o underflow que de otro modo podrían pasar desapercibidas en bloques unchecked o en inline assembly.

En este capítulo, aprenderás:

• Qué es mathint y por qué es el tipo predeterminado
• Cómo realizar conversiones (cast) de mathint a uint256 y los peligros de hacerlo
• Cómo podemos comparar código en assembly optimizado con la fórmula “prevista” y ver si las suposiciones se mantienen

Bloque Unchecked

En Solidity, un bloque unchecked desactiva las comprobaciones de overflow/underflow. Por lo tanto, en CVL, debemos razonar usando mathint para exponer estas situaciones de overflow/underflow.

Para demostrarlo, considera la función average() que acepta dos enteros sin signo (unsigned integers) y calcula su promedio:

Copy
/// Solidity

function average(uint256 x, uint256 y) external pure returns (uint256) {
    unchecked {
        return (x + y) / 2;
    }
}

Vamos a verificar formalmente si la función devuelve correctamente el promedio de dos enteros sin signo escribiendo la siguiente regla (rule):

Copy
/// CVL

rule average_overflow() {
    uint256 x;
    uint256 y;

    
mathint returnVal = average(x, y);

    assert returnVal == (x + y) / 2;
}

Esta regla falla, lo que indica que ocurrió un overflow durante la evaluación de x + y. Explicaremos el motivo a continuación.

La aritmética de CVL se evalúa como mathint por defecto

El overflow fue detectado porque el lado derecho de la aserción de CVL (x + y) / 2 adoptó por defecto el tipo mathint. Certora define mathint como: “… un tipo que puede representar un entero de cualquier tamaño; las operaciones con mathint nunca pueden sufrir overflow o underflow.” - fuente

Para ver cómo se detectó el overflow, repasemos un cálculo rápido en ambos lados de la aserción:

Copy
// assert `left-hand side` == `right-hand-side`
assert returnVal == (x + y) / 2;

Usemos los mismos valores que utilizó el Prover (2^256 - 3 y 3, como se muestra en la imagen) para calcular el promedio y entender por qué falló la regla.

Dado que el lado derecho (x + y) / 2 se evalúa como mathint por defecto, calcula correctamente el promedio como 2^255:

• x + y = 2^256 (con x = 2^256 - 3 e y = 0x3)
• 2^256 / 2 = 2^255

El lado izquierdo, que es el valor de retorno (returnVal) de la función average() invocada en Solidity, se evaluó como 0:

• x + y = 0 (con x = 2^256 - 3 e y = 0x3) debido al overflow
• 0 / 2 = 0

Mientras que el lado derecho calculó correctamente el promedio gracias al tipo sin límite mathint, el lado izquierdo returnVal (el valor de retorno de la función de Solidity) sufrió un overflow y reinició su ciclo a cero (wrap around) durante la ejecución de x + y. Esto llevó a una discrepancia en los cálculos. Por lo tanto, 0 != 2^255, resultando en una falla en la comprobación de igualdad.

Como la aritmética de CVL asume mathint por defecto, es más seguro escribir especificaciones porque elimina la posibilidad de convertir accidentalmente las operaciones aritméticas a un tipo con límite. Sin embargo, no nos impide hacer una conversión (cast) a uint256, lo cual puede ser peligroso, como veremos en la siguiente sección.

Convertir (Downcasting) mathint a uint256 Puede Ocultar Peligrosamente Problemas de Overflow/Underflow

require_uint256 es una función incorporada de CVL que convierte un mathint sin límite a un uint256 con límite. Según Certora:

“… la conversión de require ignorará los contraejemplos en los que el valor convertido esté fuera de rango.” - fuente

Para demostrarlo, revisaremos la regla anterior y la reescribiremos para que las operaciones de CVL utilicen “deliberadamente” uint256 a través de require_uint256. Por consiguiente, se ignorarán violaciones importantes de la regla.

Esta es la regla de CVL:

Copy
/// CVL

rule average_overflowIgnored() {
    uint256 x;
    uint256 y;

    mathint returnVal = average(x, y);
    
    uint256 numerator = require_uint256(x + y);
    uint256 expectedVal = r
equire_uint256(numerator / 2);


    assert returnVal == expectedVal;
}

En la regla anterior, el lado derecho de la aserción (expectedVal) se restringió al rango de uint256 usando require_uint256, lo que intrínsecamente excluye cualquier entrada que pudiera causar un overflow.

Como resultado, expectedVal siempre es igual a returnVal, lo que hace que la regla se cumpla mientras ignora silenciosamente el overflow:

Ejecución del Prover: enlace

Inline Assembly

Otra fuente de overflow/underflow es el inline assembly. Aunque permite un código eficiente en gas, pasa por alto las comprobaciones de seguridad de Solidity, incluidas las de overflows y underflows.

Para demostrarlo, considera la función flawedCeilDiv(), que implementa la división de techo (ceiling division) usando inline assembly. Refleja la fórmula matemática (n + d - 1) / d, la cual redondea hacia arriba el resultado de la división entera cuando hay un residuo distinto de cero. Por ejemplo, 6 / 3 se evalúa como 2 porque la división es exacta, mientras que 5 / 2 se evalúa como 3 debido a que el residuo fuerza el redondeo hacia arriba.

A continuación se muestra la implementación de la función:

Copy
/// Solidity

function flawedCeilDiv(uint256 n, uint256 d) external pure returns (uint256 z) {
    assembly { 
        z := div(sub(add(n, d), 1), d) 
    }
}

Así es como funciona el código en assembly:

• add(n, d) → calcula n + d
• sub(..., 1) → resta 1 → n + d - 1
• div(..., d) → realiza la división

Ahora vamos a verificar formalmente si la fórmula (n + d - 1) / d es equivalente al comportamiento previsto de la función flawedCeilDiv():

Copy
/// CVL

rule flawedCeilDiv_overflow() {
    uint256 n;
    uint256 d;

    require d != 0;
    
    mathint returnVal = flawedCeilDiv(n, d);
    mathint expectedVal = (n + d - 1) / d;

    assert returnVal == expectedVal;   
}

Nota: La precondición require d != 0 excluye los errores de división por cero con fines de demostración, ya que nuestro enfoque aquí está en detectar el comportamiento de overflow, no la división por cero.

Como se esperaba, hay una violación debido a un overflow cuando se está evaluando n + d:

Queremos comprobar específicamente si flawedCeilDiv() se comporta de forma equivalente a (n + d - 1) / d, pero también descubrimos inesperadamente que se produce un overflow. Esto resalta por qué las operaciones aritméticas de CVL asumen mathint por defecto.

Enfatizando que el Downcasting de mathint Puede Ocultar Overflows/Underflows

Para reforzar por qué debe evitarse el downcasting de las operaciones aritméticas de CVL a uint256, restringimos intencionalmente expectedVal (un mathint por defecto) al rango de uint256:

Copy
/// CVL

rule flawedCeilDiv_overflowIgnored() {
    uint256 n;
    uint256 d;

    require d != 0;
    mathint returnVal = flawedCeilDiv(n, d);

    uint256 numerator = require_uint256(n + d - 1);         
    uint256 expectedVal = require_uint256(numerator / d);  
                               
    assert returnVal == expectedVal;
}

Como resultado, los contraejemplos más allá del rango de uint256 se ignoran; por lo tanto, la regla se cumple, ocultando el comportamiento de overflow:

Ejecución del Prover: enlace

Verificando el Comportamiento Sin Overflow de unsafeDivUp

Sustituyamos la función de Solidity flawedCeilDiv() por una alternativa que no sufra overflow. Una de esas implementaciones es la función unsafeDivUp() de Solmate, que se muestra a continuación:

Copy
/// Solidity

function unsafeDivUp(uint256 x, uint256 y) external pure returns (uint256 z) {
    /// @solidity memory-safe-assembly
    assembly {
        // Add 1 to x * y if x % y > 0. Note this will
        // return 0 instead of reverting if y is zero.
        z := add(gt(mod(x, y), 0), div(x, y))
    }
}

Nota: Cambiamos la visibilidad de la función a external para evitar el uso de un harness, lo cual queda fuera del alcance de este artículo.

Ahora vamos a verificar formalmente si (n + d - 1) / d es igual al comportamiento previsto de unsafeDivUp():

Copy
/// CVL

rule unsafeDivUp_noOverflow() {
    uint256 n;
    uint256 d;

    require d != 0;
    mathint result = unsafeDivUp(n, d);        
    
    mathint expected = (n + d - 1) / d;
    assert result == expected;
}

Como podemos ver, la función se mantiene bajo el supuesto de que se comporta de forma equivalente a (n + d - 1) / d. Dado que las operaciones en CVL adoptan naturalmente mathint por defecto, podemos observar que no ocurre ningún overflow (incluso sin pensar activamente en ello).

Ejecución del Prover: enlace

Nota: La precondición require d != 0 excluye la división por cero, ya que esta regla se centra únicamente en verificar el comportamiento libre de overflow.

Como nota final, Certora proporciona la siguiente directriz práctica:

“La regla general es que debes usar mathint siempre que sea posible; solo usa los tipos uint o int para los datos que se pasarán como entrada a las funciones del contrato.” - fuente

Resumen

• mathint es un tipo sin límite en CVL que modela la aritmética sin overflow ni underflow.
• La aritmética en CVL asume mathint por defecto, lo que hace que las especificaciones sean más seguras al evitar conversiones (casting) accidentales a tipos con límite.
• require_uint256 restringe un tipo mathint al rango de uint256, ignorando por tanto los valores más allá de max_uint256. Por lo tanto, puede ocultar overflows.
• Usa mathint siempre que sea posible, y usa uint o int para los argumentos de las funciones de los contratos.

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