En cualquier implementación correcta de ERC20, la suma de todos los saldos de las cuentas debe ser siempre igual al suministro total de tokens. Esta propiedad siempre debe mantenerse verdadera durante cualquier cambio de estado. Si una llamada, ya sea directa o como parte de una secuencia de llamadas, viola este invariante, señala una falla fundamental en la lógica y el diseño del contrato.
En este capítulo, aprovecharemos lo que hemos aprendido sobre las variables ghost y los hooks de los capítulos anteriores para verificar formalmente este invariante crítico.
Añadiendo Smart Contracts Para Verificación
Para este tutorial, usaremos el contrato ERC20 de la biblioteca Solmate, desarrollado por Transmission11. Para incluir este contrato en su proyecto, cree un nuevo archivo llamado ERC20.sol dentro del subdirectorio contracts del directorio de su proyecto Certora. Luego, copie el código de la implementación ERC20 de Solmate y péguelo en ese archivo.
// SPDX-License-Identifier: AGPL-3.0-only
pragma solidity 0.8.25;
/// @notice Modern and gas efficient ERC20 + EIP-2612 implementation.
/// @author Solmate (https://github.com/transmissions11/solmate/blob/main/src/tokens/ERC20.sol)
/// @author Modified from Uniswap (https://github.com/Uniswap/uniswap-v2-core/blob/master/contracts/UniswapV2ERC20.sol)
/// @dev Do not manually set balances without updating totalSupply, as the sum of all user balances must not exceed it.
contract ERC20 {
/*//////////////////////////////////////////////////////////////
EVENTS
//////////////////////////////////////////////////////////////*/
event Transfer(address indexed from, address indexed to, uint256 amount);
event Approval(address indexed owner, address indexed spender, uint256 amount);
/*//////////////////////////////////////////////////////////////
METADATA STORAGE
//////////////////////////////////////////////////////////////*/
string public name;
string public symbol;
uint8 public immutable decimals;
/*//////////////////////////////////////////////////////////////
ERC20 STORAGE
//////////////////////////////////////////////////////////////*/
uint256 public totalSupply;
mapping(address => uint256) public balanceOf;
mapping(address => mapping(address => uint256)) public allowance;
/*//////////////////////////////////////////////////////////////
EIP-2612 STORAGE
//////////////////////////////////////////////////////////////*/
uint256 internal immutable INITIAL_CHAIN_ID;
bytes32 internal immutable INITIAL_DOMAIN_SEPARATOR;
mapping(address => uint256) public nonces;
/*//////////////////////////////////////////////////////////////
CONSTRUCTOR
//////////////////////////////////////////////////////////////*/
constructor(
string memory _name,
string memory _symbol,
uint8 _decimals
) {
name = _name;
symbol = _symbol;
decimals = _decimals;
INITIAL_CHAIN_ID = block.chainid;
INITIAL_DOMAIN_SEPARATOR = computeDomainSeparator();
}
/*//////////////////////////////////////////////////////////////
ERC20 LOGIC
//////////////////////////////////////////////////////////////*/
function approve(address spender, uint256 amount) public virtual returns (bool) {
allowance[msg.sender][spender] = amount;
emit Approval(msg.sender, spender, amount);
return true;
}
function transfer(address to, uint256 amount) public virtual returns (bool) {
balanceOf[msg.sender] -= amount;
// Cannot overflow because the sum of all user
// balances can't exceed the max uint256 value.
unchecked {
balanceOf[to] += amount;
}
emit Transfer(msg.sender, to, amount);
return true;
}
function transferFrom(
address from,
address to,
uint256 amount
) public virtual returns (bool) {
uint256 allowed = allowance[from][msg.sender]; // Saves gas for limited approvals.
if (allowed != type(uint256).max) allowance[from][msg.sender] = allowed - amount;
balanceOf[from] -= amount;
// Cannot overflow because the sum of all user
// balances can't exceed the max uint256 value.
unchecked {
balanceOf[to] += amount;
}
emit Transfer(from, to, amount);
return true;
}
/*//////////////////////////////////////////////////////////////
EIP-2612 LOGIC
//////////////////////////////////////////////////////////////*/
function permit(
address owner,
address spender,
uint256 value,
uint256 deadline,
uint8 v,
bytes32 r,
bytes32 s
) public virtual {
require(deadline >= block.timestamp, "PERMIT_DEADLINE_EXPIRED");
// Unchecked because the only math done is incrementing
// the owner's nonce which cannot realistically overflow.
unchecked {
address recoveredAddress = ecrecover(
keccak256(
abi.encodePacked(
"\x19\x01",
DOMAIN_SEPARATOR(),
keccak256(
abi.encode(
keccak256(
"Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)"
),
owner,
spender,
value,
nonces[owner]++,
deadline
)
)
)
),
v,
r,
s
);
require(recoveredAddress != address(0) && recoveredAddress == owner, "INVALID_SIGNER");
allowance[recoveredAddress][spender] = value;
}
emit Approval(owner, spender, value);
}
function DOMAIN_SEPARATOR() public view virtual returns (bytes32) {
return block.chainid == INITIAL_CHAIN_ID ? INITIAL_DOMAIN_SEPARATOR : computeDomainSeparator();
}
function computeDomainSeparator() internal view virtual returns (bytes32) {
return
keccak256(
abi.encode(
keccak256("EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)"),
keccak256(bytes(name)),
keccak256("1"),
block.chainid,
address(this)
)
);
}
/*//////////////////////////////////////////////////////////////
INTERNAL MINT/BURN LOGIC
//////////////////////////////////////////////////////////////*/
function _mint(address to, uint256 amount) internal virtual {
totalSupply += amount;
// Cannot overflow because the sum of all user
// balances can't exceed the max uint256 value.
unchecked {
balanceOf[to] += amount;
}
emit Transfer(address(0), to, amount);
}
function _burn(address from, uint256 amount) internal virtual {
balanceOf[from] -= amount;
// Cannot underflow because a user's balance
// will never be larger than the total supply.
unchecked {
totalSupply -= amount;
}
emit Transfer(from, address(0), amount);
}
}
Entendiendo el Desafío
Para expresar nuestro invariante como una expresión CVL, necesitamos dos valores:
- El suministro total de tokens
- La suma de todos los saldos de las cuentas
Nuestro contrato tiene una variable de estado pública llamada totalSupply que realiza un seguimiento del suministro total de tokens en cualquier estado y cuyo valor se puede leer utilizando la función getter llamada totalSupply(). Sin embargo, el desafío principal es que el contrato no proporciona ninguna forma integrada de obtener la suma total de todos los saldos.
La “Solución”
Para obtener la suma de todos los saldos de las cuentas, crearemos una variable ghost llamada sumOfBalances cuyo valor inicial se establecerá en 0 utilizando el axioma init_state. El ghost sumOfBalances se actualizará a través de un store hook cada vez que haya una operación de escritura en el mapping balanceOf.
Como sabemos, el store hook puede darnos acceso tanto al valor antiguo como al nuevo del saldo que se está actualizando. Usamos estos valores para calcular el cambio y actualizar nuestro ghost en consecuencia:
sumOfBalances = sumOfBalances - oldValue + newValue;
Por ejemplo, si el saldo de un usuario se incrementa de 100 a 150, nuestro hook resta 100 y suma 150 a sumOfBalances, aumentando correctamente el total en 50. Al aplicar este cálculo de delta para cada actualización de saldo, nuestro ghost sumOfBalances rastreará los cambios en el estado del contrato, reflejando la suma de todos los saldos.
Una vez que tenemos ambos valores disponibles para el Prover (el totalSupply real del contrato y nuestro ghost sumOfBalances mantenido con precisión), podemos declarar formalmente el invariante usando el bloque invariant en CVL para afirmar que el suministro total es siempre igual a la suma de todos los saldos de las cuentas.
Escribiendo la Especificación Completa Paso a Paso
Pongamos ahora en práctica todo lo que hemos discutido y escribamos una especificación completa que verifique si la suma de todos los saldos coincide con el suministro total de tokens, siguiendo los pasos a continuación:
- Dentro del directorio de su proyecto Certora, navegue hasta el subdirectorio
specsy cree un nuevo archivo llamadoerc20.spec. - Dentro de
erc20.spec, defina una variable ghost llamadasumOfBalances.
ghost mathint sumOfBalances;
- A continuación, usamos el axioma
init_statepara establecer el valor inicial desumOfBalancesen0en el caso base del invariante**.**
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
Este axioma restringe la variable ghost solo en el caso base del invariante, estableciendo un estado consistente posterior al constructor. Sin esta línea base, el Prover podría asumir valores iniciales arbitrarios para el ghost, haciendo que la preservación del invariante pierda sentido.
- Defina un store hook que rastree los cambios en el mapping
balanceOfy actualice nuestra variable ghostsumOfBalancesen consecuencia.
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount) {
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
- Ahora que tenemos ambos valores —el
totalSupply()del contrato y nuestro ghostsumOfBalances— podemos definir el invariante principal como se muestra a continuación:
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount) {
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
invariant totalSupplyEqSumOfBalances()
to_mathint(totalSupply()) == sumOfBalances;
- Finalmente, agregue un bloque de methods que incluirá la firma de la función de
totalSupply().
methods {
function totalSupply() external returns(uint256) envfree;
}
ghost mathint sumOfBalances {
init_state axiom sumOfBalances == 0;
}
hook Sstore balanceOf[KEY address account ] uint256 newAmount (uint256 oldAmount) {
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
invariant totalSupplyEqSumOfBalances()
to_mathint(totalSupply()) == sumOfBalances;
- Navegue hasta el subdirectorio
confsy cree un nuevo archivo llamadoerc20.conf.
{
"files": [
"contracts/ERC20.sol:ERC20"
],
"verify": "ERC20:specs/erc20.spec",
"msg": "Testing erc20 functionality"
}
Ejecutando la Verificación
Una vez que haya ejecutado todos los pasos anteriores, envíe el código para su verificación ejecutando el comando certoraRun confs/erc20.conf en su terminal.
Abra el resultado de la verificación proporcionado por el Prover en cualquier navegador web de su elección para ver un resultado similar a la imagen a continuación:
En nuestro resultado de la verificación, podemos ver que la comprobación del invariante falló en ambos lugares: después de la llamada al constructor y durante la ejecución de los métodos.
Cuando hacemos clic en la violación “induction base: After the constructor”, el Prover recomienda agregar la clave optimistic_loop a su configuración y establecer su valor en true, o alternativamente incrementar loop_iter a un valor mayor a 1.
Por ahora, sigamos la recomendación del Prover actualizando el archivo de configuración con la clave optimistic_loop establecida en true. Exploraremos este problema con mayor profundidad en un capítulo posterior titulado “¿Cómo los Strings Conducen a Bucles?”
{
"files": [
"contracts/ERC20.sol:ERC20"
],
"verify": "ERC20:specs/erc20.spec",
"optimistic_loop": true,
"msg": "Testing erc20 functionality"
}
Una vez hecho esto, vuelva a ejecutar el Prover ejecutando el comando certoraRun confs/erc20.conf en la terminal. En nuestro nuevo resultado de verificación, podemos ver que nuestro invariante pasa con éxito durante la ejecución del constructor pero falla durante la ejecución de los métodos, específicamente para las funciones transfer() y transferFrom().
Para entender la causa de la violación, haga clic en el call trace de la función transfer() o transferFrom(). En nuestro caso, analizaremos el call trace de la función transfer().
Para ver el call trace completo, haga clic en el botón “Expand” disponible en la esquina superior derecha del panel Call Trace.
En el call trace, podemos ver que los saldos iniciales de las cuentas individuales 0x7 y 0x8200 están establecidos en 2^256 − 4 y 0xf000000000000000000000000000000000000000000000000000000000000000, respectivamente. En forma decimal, estos corresponden a 115792089237316195423570985008687907853269984665640564039457584007913129639932 y 108890810646419256008710686707116392212123736112785533035372916772359555072000.
Ambos de estos valores son asignados por el Prover a través de havocing y caen dentro del rango numérico de 0 a 2^{256} - 1. Sin embargo, en cualquier contrato ERC20 correctamente implementado, el saldo de ninguna cuenta individual debería exceder jamás la suma total de todos los saldos. En este escenario, ambas cuentas comienzan con saldos que son enormemente mayores que el suministro total (0xa) y sumOfBalances, creando un estado inicial imposible que nunca podría existir en un despliegue real.
El Prover hace esto porque no entiende intrínsecamente la lógica de negocio de un token ERC20; simplemente trata el almacenamiento como datos en bruto. A menos que se restrinja explícitamente, asume que cualquier valor uint256 es un punto de partida válido.
Para evitar esto, necesitamos decirle específicamente al Prover que los saldos iniciales de las cuentas individuales no deben ser mayores que el sumOfBalances. Para hacerlo, usaremos la declaración require proporcionada por CVL para restringir los valores que el Prover debe considerar.
Restringiendo los Saldos Iniciales usando la Declaración require
En nuestro archivo erc20.spec, agregue el código que se muestra a continuación a nuestro store hook para limitar el alcance de los valores que se pueden asignar al saldo de cualquier cuenta. Una vez hecho esto, vuelva a ejecutar el Prover para ver el resultado de la verificación.
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
require oldAmount <= sumOfBalances; //add this line
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
En el nuevo resultado, notará que el Prover ya no encuentra ninguna violación.
Nuestro invariante totalSupplyEqSumOfBalances pasó la verificación porque, después de agregar la línea require oldAmount <= sumOfBalances; en el store hook, el Prover solo explorará rutas de ejecución donde esta condición se mantenga verdadera. Esto descarta efectivamente los contraejemplos que dependen de que un solo saldo sea mayor que la suma total (por ejemplo, el saldo del remitente o del receptor en un transfer), asegurando que el Prover se enfoque en escenarios donde los saldos individuales permanecen dentro de los límites lógicos del suministro total. Como resultado, la verificación tiene éxito, confirmando que el invariante se preserva bajo todas las transiciones permitidas.
Un Enfoque Alternativo: El Load Hook
Si bien agregar una restricción al hook Sstore funciona, existe otro enfoque donde agregamos la restricción sobre los saldos individuales dentro de un Load Hook.
Para implementar este enfoque, siga los pasos a continuación:
- Defina un load hook en el mapping
balanceOfque intercepte cada lectura abalanceOf.
hook Sload uint256 balance balanceOf[KEY address addr] {}
- Introduzca una restricción dentro de este hook usando
require sumOfBalances >= to_mathint(balance);.
hook Sload uint256 balance balanceOf[KEY address addr] {
require sumOfBalances >= to_mathint(balance);
}
- Elimine la restricción del hook
Sstorepara que dependamos únicamente de la lógica del load hook.
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
require oldAmount <= sumOfBalances; //remove this line
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
Así es como debería verse la especificación actualizada después de los cambios sugeridos anteriormente:
methods {
function totalSupply() external returns(uint256) envfree;
}
ghost mathint sumOfBalances {
// Constraining pre-constructor ghost value through axiom
init_state axiom sumOfBalances == 0;
}
// Added a load hook on balanceOf mapping
hook Sload uint256 balance balanceOf[KEY address addr] {
// Introduce a constraint
require sumOfBalances >= to_mathint(balance);
}
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
// Delta Update
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
invariant totalSupplyEqSumOfBalances()
to_mathint(totalSupply()) == sumOfBalances;
Si vuelve a ejecutar la verificación con este cambio (eliminando el require del hook Sstore y manteniéndolo solo en el hook Sload), el invariante totalSupplyEqSumOfBalances seguirá pasando.
Esto funciona porque el load hook filtra explícitamente cualquier estado donde el saldo de una cuenta individual sea mayor que la suma total de todos los saldos. Si el Prover intenta construir un contraejemplo usando un estado inicial tan imposible, eventualmente leerá ese saldo mientras evalúa la lógica del contrato. En el momento en que ocurre esta lectura, la declaración require dentro del load hook verifica si ese saldo es consistente con nuestra variable ghost. Dado que el saldo es irrealmente grande, la condición falla, y el Prover se ve obligado a descartar esa ruta de ejecución por completo.
Sstore vs. Sload: ¿Dónde Colocar las Restricciones?
Ambas versiones “funcionan” porque excluyen los estados imposibles que violarían nuestro invariante, pero el enfoque del load hook proporciona una salvaguarda más confiable y completa. Analicemos por qué:
Lo Que el Store Hook Realmente Garantiza
Cuando ponemos la restricción en el store hook:
hook Sstore balanceOf[KEY address account] uint256 newAmount (uint256 oldAmount) {
require oldAmount <= sumOfBalances;
sumOfBalances = sumOfBalances - oldAmount + newAmount;
}
En el código anterior, le estamos diciendo efectivamente al Prover: “Cada vez que escribas en balanceOf[account], asegúrate de que el valor anterior (oldAmount) no fuera mayor que sumOfBalances”
Esto crea un punto ciego:
- Si el Prover nunca escribe en cierto espacio de
balanceOf[addr], entonces este hook nunca se activa para esa dirección. - Esto significa que el Prover todavía es libre de comenzar desde un valor inicial extraño (a través de havoc), como
balanceOf[addr] = 2^{256} - 1, incluso sisumOfBalances = 10. - Mientras el contrato no intente escribir en ese espacio, el
requireenSstorenunca se verifica, y se permite que el estado imposible persista durante las lecturas y el razonamiento lógico.
En resumen, el store hook solo dice: “Si alguna vez tocas este espacio escribiendo en él, entonces el valor anterior debe ser razonable.” No dice: “Todos los saldos son siempre razonables cada vez que los miras.”
Lo Que el Load Hook Garantiza en su Lugar
Ahora, observe la versión del load hook:
hook Sload uint256 balance balanceOf[KEY address addr] {
require sumOfBalances >= to_mathint(balance);
}
Esto se ejecuta cada vez que el Prover lee un saldo de balanceOf. Aquí, le estamos diciendo al Prover: “Cada vez que leas un saldo, ese saldo debe ser menor o igual a sumOfBalances”
Esto tiene dos efectos importantes:
- El Prover no puede usar un saldo imposible en ningún cálculo. Si intenta asumir que
balanceOf[addr]es mayor quesumOfBalancesy luego lo lee, elrequireen el load hook falla, y esa ruta de ejecución se descarta inmediatamente. - Esto se aplica incluso si nunca se escribió en el espacio. El Prover podría hacer havoc a
balanceOf[addr]a algún valor arbitrario al principio, pero en el momento en que lee ese valor, el load hook lo verifica. Si el valor es imposible, toda esa ruta se desecha.
El load hook actúa como un control de cordura global: “Cualquier saldo que mires debe tener sentido con respecto al ghost sumOfBalances”
Es por esto que, cuando nos preocupamos por mantener sumOfBalances alineado con los saldos reales y evitar estados imposibles de ERC20, el enfoque del load hook suele ser la mejor opción.
Conclusión
En este capítulo, verificamos el invariante fundamental de ERC20: Suministro Total = Suma de Todos los Saldos.
Logramos esto usando una variable ghost para rastrear la suma agregada y hooks para sincronizar ese ghost con el almacenamiento del contrato. De manera crucial, demostramos por qué colocar restricciones en un hook Sload es a menudo más seguro que en un hook Sstore. Al vigilar los valores cada vez que se leen, cerramos efectivamente el “punto ciego” donde el Prover podría, de otro modo, asumir estados iniciales imposibles.
Estas técnicas le permiten probar reglas de negocio de alto nivel sobre almacenamiento de bajo nivel, asegurando que su verificación se centre únicamente en comportamientos válidos y realistas del contrato.
Este artículo es parte de una serie sobre verificación formal usando el Certora Prover