Introducción
En capítulos anteriores, exploramos cómo funcionan las invariantes de CVL: propiedades que deben mantenerse durante toda la ejecución del contrato. Las invariantes pueden funcionar como precondiciones en reglas y condiciones preserved en otras invariantes, lo que permite que la verificación se base en garantías ya probadas y elimina el riesgo de suposiciones defectuosas. Las invariantes también se comprueban automáticamente en todas las funciones que cambian el estado.
Este capítulo continúa como la parte (2/5) del análisis del código de la especificación CVL del ERC-721 de OpenZeppelin y se centra en las propiedades invariantes. Verifica las siguientes cinco invariantes de ERC-721:
-
balanceOfConsistencyEl balance de un usuario y el recuento de su propiedad siempre son iguales.
-
ownerHasBalanceLos propietarios de tokens siempre tienen balances positivos.
-
ownedTotalIsSumOfBalancesEl recuento total de tokens en propiedad es igual a la suma de todos los balances de los usuarios.
-
notMintedUnsetLos tokens no acuñados (unminted) no tienen configurada ninguna dirección aprobada.
-
zeroAddressHasNoApprovedOperatorLos tokens no acuñados no tienen operadores aprobados.
Estas invariantes garantizan que los balances reflejen con precisión la propiedad y que las aprobaciones sigan siendo consistentes con el estado de la propiedad.
La invariante balanceOfConsistency
En ERC-721, hay tres formas de determinar el balance de tokens de una cuenta:
- llamando a la función pública
balanceOf(address) - leyendo del mapeo
_balances - leyendo del mapeo de almacenamiento
_ownersy contando cuántos tokens posee la dirección
Estas tres cantidades deben ser iguales porque cada una representa el mismo hecho subyacente: cuántos tokens posee el usuario. Cualquier discrepancia indicaría una contabilidad inconsistente entre los balances y el seguimiento de la propiedad.
En la invariante balanceOfConsistency, estas cantidades corresponden a balanceOf(user), _balances[user] y _ownedByUser[user], y cada una representa el balance de tokens del usuario:
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user]
...
Cómo se deriva cada representación del balance
Para verificar esta invariante, la especificación captura cada una de estas representaciones. A continuación se explica cómo se deriva cada una.
balanceOf(user) — función de vista pública del balance de un usuario
balanceOf(user) es una función de vista pública que podemos invocar directamente en CVL para recuperar el balance del usuario. Esta función devuelve el valor almacenado en la variable de mapeo de almacenamiento _balances.
_balances[user] — balances de tokens reflejados desde el almacenamiento
_balances[user] es una variable ghost que lee y refleja la variable de mapeo de almacenamiento privado _balances a través de un hook Sload.
Se inicializa a cero para todas las direcciones utilizando un axioma init_state con un cuantificador forall, el cual establece que cada dirección comienza con un balance cero en el estado inicial, coincidiendo con el estado de almacenamiento predeterminado del contrato:
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
...
Sin esta inicialización, el Prover asume valores iniciales arbitrarios (caso base) para los balances, lo que puede llevar a una contabilidad incorrecta desde el estado inicial. Esto invalida la lógica de seguimiento y da como resultado violaciones de falsos positivos durante la verificación.
Después de la inicialización, la especificación debe reflejar las lecturas de almacenamiento en el estado ghost utilizando un hook Sload. El hook Sload lee los valores del slot de almacenamiento real de _balances y sincroniza esos valores con la variable ghost (el ghost y la variable de almacenamiento comparten el mismo nombre pero no entran en conflicto):
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sload uint256 value _balances[KEY address user] {
require _balances[user] == to_mathint(value);
}
La sincronización ocurre cuando el valor de almacenamiento devuelto por el hook Sload se restringe mediante require para que sea igual a la variable ghost. Esta sincronización es necesaria porque las variables ghost no se actualizan automáticamente en las lecturas de almacenamiento.
_ownedByUser[user] — recuento de propiedad de tokens derivado del almacenamiento
_ownedByUser[user] es una variable ghost que representa el recuento de todos los tokenIds para los cuales ownerOf(tokenId) == user:
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
...
En otras palabras, si listamos todos los tokens y contamos cuántos posee user, obtenemos _ownedByUser[user]. No queremos un escenario en el que balanceOf(user) informe 2, pero el recuento real de propiedad sea 3 (por ejemplo, si ownerOf(token1) == user, ownerOf(token2) == user y ownerOf(token3) == user).
La variable ghost _ownedByUser[user] almacena cuántos tokens posee un usuario a través del hook Sstore. El hook se ejecuta cada vez que el contrato escribe un nuevo valor en el mapeo de almacenamiento privado del contrato _owners[tokenId], y observa tanto oldOwner como newOwner para determinar cómo ha cambiado la propiedad.
Al comparar estos dos valores, podemos clasificar la actualización como una acuñación (mint), quema (burn) o transferencia (transfer):
- Mint:
oldOwner == address(0)ynewOwner != address(0) - Burn:
oldOwner != address(0)ynewOwner == address(0) - Transfer: tanto
oldOwnercomonewOwnerson direcciones distintas de cero
El hook actualiza el mapeo ghost _ownedByUser para reflejar estos cambios de propiedad:
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
// _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
Nota: Comentamos intencionalmente la línea _ownedTotal = ... porque no es necesaria en este momento. No estamos rastreando el número total de tokens en propiedad; solo estamos rastreando los tokens que posee cada usuario individual.
La primera línea en el hook Sstore para _owners maneja el incremento de tokens, lo que significa que ocurre un mint y un transfer:
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
- Si
newOwner != 0, se suma 1 al recuento de tokens denewOwner. Esto se aplica a:- Mint: cuando se crea un token y se asigna a un usuario (
address(0)anewOwner) - Transfer: cuando un token pasa de un usuario a otro (
oldOwneranewOwner)
- Mint: cuando se crea un token y se asigna a un usuario (
- Si
newOwner == 0, esto indica un burn, por lo que ningúnnewOwnerrecibe el token. La expresión ternaria se evalúa como 0, por lo que no se produce ninguna suma. Sin embargo, esa pérdida de token (burn) aún debe contabilizarse, y eso lo maneja la segunda línea.
La segunda línea en el hook Sstore para _owners maneja el decremento de tokens, lo que significa que ocurre un burn y un transfer (también):
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
- Si
oldOwner != 0, el propietario anterior (distinto de cero) tenía el token y ahora lo pierde, por lo que restamos 1. Esto se aplica tanto a las operaciones de transfer como de burn. - Si
oldOwner == 0, esto indica un mint, donde el token es recién creado sin propietario anterior. El ternario se evalúa como 0, por lo que no ocurre ninguna resta. En su lugar, el recuento de propiedad se contabiliza en la primera línea — la que maneja los incrementos de tokens.
Ahora que hemos analizado la expresión de la invariante y cómo se derivan las tres representaciones del balance de tokens de un usuario, queda una pieza final para completar la especificación: el manejo de devoluciones de llamada (callbacks) externas de las operaciones de acuñación segura (safe mint) y transferencia segura (safe transfer).
Las invariantes invocan automáticamente todas las funciones que cambian el estado durante la verificación, lo que significa que el Prover llama a safeMint() y safeTransferFrom(), las cuales desencadenan callbacks externos a onERC721Received() en el contrato del destinatario. Necesitamos configurar cómo el Prover maneja esta llamada externa. De lo contrario, estas llamadas externas son tratadas como no resueltas por el Prover, lo que causa havoc (caos/estado arbitrario) en las variables ghost y el almacenamiento, y lleva a violaciones de falsos positivos en la propiedad invariante.
DISPATCHER — resolviendo el callback de onERC721Received
Para resolver este callback, la especificación despacha (dispatches) la llamada onERC721Received() a un contrato receptor simulado (mock) que devuelve el selector bytes4 0x150b7a02 para indicar soporte de ERC-721. Para implementar el despacho (dispatch), necesitamos:
- crear un contrato receptor ERC721 simple (mock),
- incluirlo en la scene de verificación,
- añadir una instrucción de despacho (dispatch) en el bloque
methods.
El contrato receptor simulado (mock) de ERC721:
Aquí está el contrato receptor, implementado como un harness que devuelve el selector bytes4 0x150b7a02:
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.20;
import "contracts/interfaces/IERC721Receiver.sol";
contract ERC721ReceiverHarness is IERC721Receiver {
function onERC721Received(address, address, uint256, bytes calldata) external pure returns (bytes4) {
return this.onERC721Received.selector;
}
}
Nota: Importar IERC721Receiver sirve como una verificación de interfaz, confirmando que el contrato cumple con la especificación esperada del receptor ERC721.
Añadir el contrato receptor simulado a la scene:
A continuación, incluimos ERC721ReceiverHarness.sol en la scene añadiéndolo al archivo de configuración .conf:
// .conf
{
"files": [
"certora/harness/ERC721Harness.sol",
"certora/harness/ERC721ReceiverHarness.sol",
],
...
}
Llegados a este punto, el receptor simulado forma parte de la scene de verificación y está disponible como un objetivo de despacho (dispatch target).
Añadir la instrucción DISPATCH:
Luego, en el bloque methods de la especificación CVL, añadimos la instrucción de despacho:
// .spec
methods {
function balanceOf(address) external returns (uint256) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
La línea de despacho: function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true) instruye al Prover a enrutar las llamadas a onERC721Received() a todos los contratos en la scene de verificación (_ es un comodín) que implementen onERC721Received() y probar su implementación frente a la invariante balanceOfConsistency. Dado que solo tenemos un contrato que implementa onERC721Received, que es el receptor simulado, ese es el único contrato que el Prover probará.
Con DISPATCHER(true), solo los contratos en la scene se seleccionan para el despacho, y el Prover prueba cada implementación coincidente para determinar si alguna puede causar una violación.
El contrato receptor simulado utilizado aquí es intencionalmente mínimo. Implementa solo la función onERC721Received() y devuelve el selector requerido 0x150b7a02. No contiene lógica que cambie el estado ni afecte el almacenamiento del contrato que llama. Como resultado, el callback no puede introducir ninguna violación de invariantes.
Incluso si el receptor simulado hace que safeMint() o safeTransferFrom() (incluyendo sus variantes de bytes) se reviertan — por ejemplo, devolviendo un valor de callback incorrecto — las invariantes no se ven afectadas porque las reversiones (reverts) no causan ningún cambio de estado. Sin embargo, este no es el caso cuando verificamos formalmente las funciones de safe mint y safe transfer en un capítulo posterior, donde los callbacks que revierten causan fallos en las aserciones.
En esta especificación de invariante CVL, la función de DISPATCHER es simplemente resolver la llamada externa. Sin él, safeMint() y safeTransferFrom() — incluyendo sus variantes — invocan llamadas externas no resueltas, lo que causa caos (havoc) y conduce a fallos de falsos positivos en las invariantes.
La especificación completa y la ejecución del Prover para la invariante balanceOfConsistency
Aquí está la especificación CVL completa para la invariante balanceOfConsistency, que incluye el bloque methods, las declaraciones de variables ghost y las implementaciones de los hooks:
methods {
function balanceOf(address) external returns (uint256) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
// _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sload uint256 value _balances[KEY address user] {
require _balances[user] == to_mathint(value);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user];
// {
// preserved {
// require balanceLimited(user);
// }
// }
Nota: El bloque preserved está comentado intencionalmente porque la invariante se verifica con éxito sin él, lo que significa que no es estrictamente necesario.
Aquí está la ejecución verificada del Prover.
La invariante ownerHasBalance — los propietarios de tokens tienen balances positivos
Esta invariante establece que si un tokenId existe (el propietario es distinto de cero), entonces el balance de ese propietario debe ser mayor que cero:
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
...
Esta invariante se utiliza como precondición en capítulos posteriores al verificar transferencias, donde el remitente debería tener un balance positivo. Podríamos integrar de forma rígida (hardcode) unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 directamente en la regla, pero demostrarlo como una invariante proporciona garantías de seguridad más sólidas.
Aquí se necesita un bloque preserved para requerir balanceOfConsistency(ownerOf(tokenId)) antes de que se ejecute ownerHasBalance. Esto le dice al Prover: “Antes de comprobar si el propietario tiene balance, confirma primero que balanceOf coincide con el recuento de propiedad rastreado por los ghosts”. Evita que el Prover entre en estados inconsistentes en los que existe un propietario pero parece tener un balance cero debido a havoc.
Aquí está la invariante de CVL:
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
{
preserved {
requireInvariant balanceOfConsistency(ownerOf(tokenId));
// require balanceLimited(ownerOf(tokenId));
}
}
La especificación completa y la ejecución del Prover para la invariante ownerHasBalance
Aquí está la especificación CVL completa para la invariante ownerHasBalance, que incluye el bloque methods, las variables ghost, los hooks y la invariante preserved balanceOfConsistency:
methods {
function ownerOf(uint256) external returns (address) envfree;
function balanceOf(address) external returns (uint256) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
// _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sload uint256 value _balances[KEY address user] {
require _balances[user] == to_mathint(value);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user];
// {
// preserved {
// require balanceLimited(user);
// }
// }
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover v8.3.1
{
preserved {
requireInvariant balanceOfConsistency(ownerOf(tokenId));
// require balanceLimited(ownerOf(tokenId));
}
}
Nota: La expresión original de la invariante era balanceOf(ownerOf(tokenId)) > 0__, pero se actualizó a unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 para verificarse con la versión 8.3.1 del Prover.
Aquí está la ejecución del Prover.
La invariante ownedTotalIsSumOfBalances — el total de tokens en propiedad es igual a la suma de todos los balances
En esta especificación de invariante, se derivan el número total de tokens en propiedad y el suministro total (total supply) porque el estándar principal ERC-721 no expone ninguna noción de suministro total; solo ERC-721 Enumerable define totalSupply(). Dado que esta invariante no puede verificarse directamente frente a una función estándar, estos valores se reconstruyen utilizando variables ghost (_ownedTotal y _supply) y hooks.
_ownedTotal cuenta cuántos tokens existen actualmente observando los cambios de propiedad a través del hook Sstore en la variable de almacenamiento _owners. _supply es la suma de todos los balances de los usuarios, también rastreada como un ghost.
Con estos dos valores reconstruidos y rastreados como ghosts, la invariante verifica que _ownedTotal sea igual a _supply. Esto asegura una contabilidad de balances consistente. Si los tokens en propiedad superan el suministro, los balances están subcontados (los tokens existen pero no se reflejan en los balances). Si el suministro supera los tokens en propiedad, los balances están sobrecontados (los balances reclaman más tokens de los que realmente existen).
Por lo tanto, esta igualdad garantiza que cada token en propiedad se cuente exactamente una vez en los totales de los balances:
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: number of owned tokens is the sum of all balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownedTotalIsSumOfBalances()
_ownedTotal == _supply
{
// preserved blocks will be shown later
}
Tanto _supply como _ownedTotal son variables de mapeo ghost utilizadas para rastrear el suministro total de tokens a través de hooks Sstore, pero desde diferentes perspectivas:
-
_supplyrastrea el suministro total restando el balance antiguo y sumando el balance nuevo cada vez que hay una escritura de almacenamiento en_balances:hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) { _supply = _supply - oldValue + newValue; }Al observar los balances a nivel de almacenamiento, se deriva
_supply, y el efecto sobre_supplydepende del tipo de operación:- Cuando se acuña (mint) un token a un usuario y el balance cambia de
oldValue = 2anewValue = 3,_supplyse calcula como_supply = _supply - 2 + 3, lo que da como resultado un aumento neto de 1. - Cuando se quema (burn) un token del propietario y el balance cambia de
oldValue = 3anewValue = 2,_supplyse calcula como_supply = _supply - 3 + 2, lo que da como resultado una disminución neta de 1. - Cuando un usuario transfiere un token a otro usuario, el balance del remitente disminuye en 1 mientras que el balance del destinatario aumenta en 1. La disminución del remitente compensa el aumento del destinatario, por lo que
_supplypermanece sin cambios.
- Cuando se acuña (mint) un token a un usuario y el balance cambia de
-
_ownedTotalrastrea el número de tokens en propiedad a través de un hookSstorerestando 1 cuando se borra la propiedad y sumando 1 cuando un token se asigna a una dirección distinta de cero:hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) { ... _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0); }Vamos a simular esto en base a los cambios de propiedad, pero primero, reorganicemos el código para mayor claridad:
_ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);-
Si tanto
oldOwnercomonewOwnerson direcciones distintas de cero, entonces ocurre una transferencia (transfer):newOwneres distinto de cero, por lo que la expresión ternaria se evalúa como1, y se suma1.oldOwneres distinto de cero, por lo que la expresión ternaria se evalúa como1, y se resta1.
El efecto neto es que no hay cambios en
_ownedTotal, ya que se suma1y se resta1. Por principio, una operación de transferencia no afecta el recuento total de propiedad. -
Si
oldOwneres cero ynewOwneres distinto de cero, entonces ocurre una acuñación (mint):newOwneres distinto de cero, por lo que la expresión ternaria se evalúa como1, y se suma1.oldOwneres cero, por lo que la expresión ternaria se evalúa como0, y se resta0.
El efecto neto es
+1, porque se suma1y no se resta nada. Por principio, una operación de acuñación suma al recuento total de propiedad. -
Si
oldOwneres distinto de cero ynewOwneres cero, entonces ocurre una quema (burn):newOwneres cero, por lo que la expresión ternaria se evalúa como0, y se suma0.oldOwneres distinto de cero, por lo que la expresión ternaria se evalúa como1, y se resta1.
El efecto neto es
-1, porque no se suma nada y se resta1. Por principio, una operación de quema reduce el recuento total de propiedad.
-
Cláusulas Preserved:
La invariante incluye cláusulas preserved. Lo siguiente resume cada una de ellas:
-
Para mint:
mint(),safeMint(),safeMint(``bytes``)-
require balanceLimited(to)El balance del destinatario debe permanecer por debajo de
max_uint256para evitar que el Prover explore caminos de desbordamiento (overflow) poco realistas.
-
-
Para burn:
burn()-
requireInvariant ownerHasBalance(tokenId)El token debe tener un propietario con un balance positivo antes de ser quemado.
-
-
Para transfer:
transferFrom(),safeTransferFrom(),safeTransferFrom(``bytes``)-
require balanceLimited(to)El balance del destinatario debe mantenerse por debajo de
max_uint256. -
requireInvariant ownerHasBalance(tokenId)El token debe provenir de un propietario válido con un balance distinto de cero.
-
Aquí está la invariante que incluye las cláusulas preserved:
invariant ownedTotalIsSumOfBalances()
_ownedTotal == _supply
{
preserved mint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
}
preserved burn(uint256 tokenId) with (env e) {
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(ownerOf(tokenId));
}
preserved transferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
}
Nota: La invariante ownedTotalIsSumOfBalances se verifica con éxito incluso sin requireInvariant balanceOfConsistency__. Con fines de discusión, lo comentamos para que el lector pueda ver qué condiciones preserved se requieren estrictamente para verificar la invariante. Esto no significa que sea inútil; como ya está probada, se puede asumir que siempre se cumple. Por lo tanto, se puede reinstaurar de forma segura. Agregarla como condición preserved generalmente acorta los tiempos de ejecución del Prover.
La especificación completa y la ejecución del Prover para la invariante ownedTotalIsSumOfBalances
Aquí está la especificación CVL completa para la invariante ownedTotalIsSumOfBalances, que incluye el bloque methods, las variables ghost, los hooks y las invariantes preserved ownerHasBalance y balanceOfConsistency:
methods {
function ownerOf(uint256) external returns (address) envfree;
function balanceOf(address) external returns (uint256) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
ghost mathint _ownedTotal {
init_state axiom _ownedTotal == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
_ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mathint _supply {
init_state axiom _supply == 0;
}
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
_supply = _supply - oldValue + newValue;
}
hook Sload uint256 value _balances[KEY address user] {
require _balances[user] == to_mathint(value);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user];
// {
// preserved {
// require balanceLimited(user);
// }
// }
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
{
preserved {
requireInvariant balanceOfConsistency(ownerOf(tokenId));
// require balanceLimited(ownerOf(tokenId));
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: number of owned tokens is the sum of all balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownedTotalIsSumOfBalances()
_ownedTotal == _supply
{
preserved mint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
}
preserved burn(uint256 tokenId) with (env e) {
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(ownerOf(tokenId));
}
preserved transferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
}
Ejecución del Prover: enlace
La invariante notMintedUnset — los tokens no acuñados no tienen aprobaciones
Si un token no está acuñado (es decir, no tiene propietario), entonces tampoco debe tener ninguna dirección aprobada:
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;
unsafeOwnerOf() y unsafeGetApproved() son funciones de vista de harness que devuelven la dirección cero en lugar de revertir cuando un tokenId no está acuñado. En contraste, las funciones estándar ownerOf() y getApproved() revierten para tokens no acuñados y, por lo tanto, nunca devuelven estos valores de dirección cero.
Usar ownerOf() y getApproved() crearía un problema para la evaluación de invariantes. Las invariantes deben ser expresiones booleanas que se evalúen como true o false, pero cuando el Prover evalúa una invariante que llama a ownerOf(tokenId) o getApproved(tokenId) en un tokenId no acuñado, la llamada a la función se revierte. Un revert no es ni true ni false, lo que impide que la expresión invariante se evalúe como un valor booleano. Aunque las reglas pueden usar @withrevert e inspeccionar la bandera lastReverted para manejar llamadas que revierten, las invariantes son expresiones booleanas puras y no soportan dicha lógica de control de flujo.
Al usar las funciones de harness unsafeOwnerOf() y unsafeGetApproved() que devuelven la dirección cero en lugar de revertir, el Prover puede evaluar la expresión de la invariante a un valor booleano para todos los valores de tokenId, incluyendo los tokens no acuñados.
Esta invariante es importante porque si de alguna manera se establece una aprobación para un tokenId que no existe, y ese tokenId se acuña más tarde a una dirección diferente, la dirección aprobada previamente aún conservaría los derechos de transferencia. Esto podría permitir transferencias no autorizadas inmediatamente después de la acuñación. La invariante garantiza que todos los tokens comiencen con el estado predeterminado: sin propietario, sin aprobación.
La especificación completa y la ejecución del Prover para la invariante notMintedUnset
methods {
function unsafeGetApproved(uint256) external returns (address) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;
Ejecución del Prover: enlace
La invariante zeroAddressHasNoApprovedOperator — los tokens no acuñados no tienen un operador aprobado
isApprovedForAll es una función pública que verifica si un operador (una dirección) está autorizado para administrar todos los tokens propiedad de una cuenta en particular. Esta invariante establece que ninguna dirección debe ser aprobada nunca como operador para address(0). Dado que address(0) es el propietario implícito de los tokens no acuñados, esto evita que cualquier operador sea preautorizado para administrar tokens antes de que sean acuñados.
Por lo tanto, la función de vista isApprovedForAll(0, a) siempre debe devolver false:
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
!isApprovedForAll(0, a)
{
preserved with (env e) {
require nonzerosender(e);
}
}
Sin embargo, esto se cumple solo bajo la condición preserved de que el llamador (msg.sender) no sea la dirección cero (require nonzerosender(e)) según la definición:
definition nonzerosender(env e) returns bool = e.msg.sender != 0;
Esta suposición tiene sentido porque address(0) no tiene clave privada, por lo que nadie puede iniciar transacciones desde esta dirección, lo que hace imposible llamar a ninguna función en la realidad. Sin embargo, dado que la función setApprovalForAll() no evita explícitamente que la dirección cero la llame, el Prover explorará esta posibilidad, lo que puede llevar a violaciones de falsos positivos, donde el Prover informa de una violación que no puede ocurrir en la práctica.
Con la condición preserved asegurando que msg.sender sea distinto de cero, esta invariante garantiza que address(0) nunca puede tener operadores aprobados. Por lo tanto, los tokens no acuñados no pueden tener un operador.
La especificación completa y la ejecución del Prover para la invariante zeroAddressHasNoApprovedOperator
Ahora aquí está la especificación completa de la invariante zeroAddressHasNoApprovedOperator, que incluye el bloque methods y la definition:
methods {
function isApprovedForAll(address,address) external returns (bool) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition nonzerosender(env e) returns bool = e.msg.sender != 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
!isApprovedForAll(0, a)
{
preserved with (env e) {
require nonzerosender(e);
}
}
Ejecución del Prover: enlace
Especificación CVL Consolidada Para Todas Las Invariantes
Ahora que hemos discutido cada invariante de forma independiente, podemos consolidarlas en una sola especificación:
methods {
function balanceOf(address) external returns (uint256) envfree;
function ownerOf(uint256) external returns (address) envfree;
function isApprovedForAll(address,address) external returns (bool) envfree;
function unsafeOwnerOf(uint256) external returns (address) envfree;
function unsafeGetApproved(uint256) external returns (address) envfree;
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
definition nonzerosender(env e) returns bool = e.msg.sender != 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: ownership count │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mathint _ownedTotal {
init_state axiom _ownedTotal == 0;
}
ghost mapping(address => mathint) _ownedByUser {
init_state axiom forall address a. _ownedByUser[a] == 0;
}
hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) {
_ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0);
_ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0);
_ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
ghost mathint _supply {
init_state axiom _supply == 0;
}
ghost mapping(address => mathint) _balances {
init_state axiom forall address a. _balances[a] == 0;
}
hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
_supply = _supply - oldValue + newValue;
}
hook Sload uint256 value _balances[KEY address user] {
require _balances[user] == to_mathint(value);
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: balanceOf is the number of tokens owned │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant balanceOfConsistency(address user)
to_mathint(balanceOf(user)) == _ownedByUser[user] &&
to_mathint(balanceOf(user)) == _balances[user];
// {
// preserved {
// require balanceLimited(user);
// }
// }
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: owner of a token must have some balance │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownerHasBalance(uint256 tokenId)
unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0 // fixed for Prover V8
{
preserved {
requireInvariant balanceOfConsistency(ownerOf(tokenId));
// require balanceLimited(ownerOf(tokenId));
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: number of owned tokens is the sum of all balances │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant ownedTotalIsSumOfBalances()
_ownedTotal == _supply
{
preserved mint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
}
preserved safeMint(address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
}
preserved burn(uint256 tokenId) with (env e) {
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(ownerOf(tokenId));
}
preserved transferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
preserved safeTransferFrom(address from, address to, uint256 tokenId, bytes data) with (env e) {
require balanceLimited(to);
requireInvariant ownerHasBalance(tokenId);
// requireInvariant balanceOfConsistency(from);
// requireInvariant balanceOfConsistency(to);
}
}
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: tokens that do not exist are not owned and not approved │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant notMintedUnset(uint256 tokenId)
unsafeOwnerOf(tokenId) == 0 => unsafeGetApproved(tokenId) == 0;
/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Invariant: address(0) has no authorized operator │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
invariant zeroAddressHasNoApprovedOperator(address a)
!isApprovedForAll(0, a)
{
preserved with (env e) {
require nonzerosender(e);
}
}
Aquí está la ejecución del Prover.
Este artículo es parte de una serie sobre verificación formal usando el Certora Prover