Introducción

Este capítulo es la cuarta parte (4/5) de nuestro análisis de código de la especificación CVL de ERC-721 de OpenZeppelin y se centra en verificar formalmente las operaciones de acuñación segura (safe mint) y transferencia segura (safe transfer), específicamente:

• _safeMint() y _safeMint(bytes)
• safeTransferFrom() y safeTransferFrom(bytes)

La función _safeMint() extiende _mint() con una comprobación adicional: si el destinatario es un contrato, verifica que el contrato pueda manejar tokens ERC-721. Esto evita que los NFTs se queden atascados en contratos que carecen de la lógica de transferencia.

El ERC-721 en OpenZeppelin tiene dos versiones de safeMint: una que toma un parámetro de datos bytes, y otra que no. La versión más simple (sin bytes) llama a la versión con bytes, pasando una cadena vacía como parámetro data:

Copy
// ERC721.sol

function _safeMint(address to, uint256 tokenId) internal {
    _safeMint(to, tokenId, "");
}

function _safeMint(address to, uint256 tokenId, bytes memory data) internal virtual {
    _mint(to, tokenId);
    ERC721Utils.checkOnERC721Received(_msgSender(), address(0), to, tokenId, data);
}

Nota: La biblioteca ERC721Utils se puede encontrar aquí.

Ambas versiones acuñan un NFT a la dirección to, y luego llaman a la función hook onERC721Received() en el destinatario si este es un contrato. La versión con el parámetro bytes reenvía adicionalmente data al hook onERC721Received del contrato receptor, lo que permite al destinatario personalizar su comportamiento en función de los datos proporcionados. Por ejemplo, un contrato de juego puede acuñar un NFT directamente en el contrato de inventario de un jugador e incluir data que especifique el tipo de artículo, la rareza o los atributos iniciales para desencadenar eventos del juego.

Ambas versiones revierten (revert) y deshacen la acuñación si:

• el destinatario no implementa onERC721Received(),
• el callback revierte, o
• el callback devuelve un valor distinto al selector esperado 0x150b7a02.

No es posible verificar formalmente _safeMint() sin resolver su llamada externa al contrato destinatario.

Cuando se invoca _safeMint() en una regla, llama a checkOnERC721Received(), que a su vez realiza una llamada externa a onERC721Received() en el contrato destinatario. El Prover no puede determinar qué hará onERC721Received(), por lo que trata la llamada como no resuelta. Las llamadas externas no resueltas hacen que el Prover asuma cambios arbitrarios en el almacenamiento, lo que significa que las variables de almacenamiento (storage variables) y las variables fantasma (ghost variables) en las afirmaciones (assertions) posteriores a la llamada toman valores no deterministas, haciendo que las afirmaciones carezcan de sentido.

Para resolver la llamada externa, se añade un contrato receptor simulado (mock) cuya función onERC721Received devuelve 0x150b7a02 (el valor de this.onERC721Received.selector).

Copy
// ERC721ReceiverHarness.sol -- this is a mock contract

import "contracts/interfaces/IERC721Receiver.sol";

contract ERC721ReceiverHarness is IERC721Receiver {
    function onERC721Received(address, address, uint256, bytes calldata) external pure returns (bytes4) {
        return this.onERC721Received.selector; // always returns 0x150b7a02
    }
}

No verificamos el contrato receptor externo porque su implementación está fuera de nuestro control. En su lugar, la llamada a onERC721Received se despacha a un contrato receptor simulado que siempre devuelve el selector esperado 0x150b7a02. Esto significa que la especificación no prueba los casos en los que el callback revierte o devuelve un valor incorrecto.

Sin embargo, esto no significa que _safeMint() no revertiría si ocurre un fallo en el callback en una ejecución real. La afirmación de vitalidad (liveness assertion) asegura que la función se comporte correctamente en tales casos revirtiendo.

La afirmación de vitalidad no inspecciona el valor de retorno del callback en sí; comprueba si la llamada en su conjunto tuvo éxito o revirtió. Como se discutió en el capítulo “Mint and Burn”, la acuñación no revierte (!lastReverted) si y solo si ownerBefore == address(0) y to != address(0):

Copy
bool success = !lastReverted;
assert success <=> (ownerBefore == 0 && to != 0);

Cuando el callback del receptor causa un revert, el lado derecho (ownerBefore == 0 && to != 0) sigue cumpliéndose porque estos valores se capturaron antes de la llamada. Sin embargo, success es falso, lo que viola la afirmación bicondicional. El Prover detecta esta contradicción y reporta una violación. Por lo tanto, no se requiere ninguna afirmación adicional para comprobar explícitamente el valor de retorno del callback.

El mismo principio discutido anteriormente con safe mint también se aplica a las transferencias seguras de tokens.

El safeTransferFrom también tiene dos versiones: una que toma un parámetro de datos bytes, y otra que no:

Copy
// ERC721.sol

function safeTransferFrom(address from, address to, uint256 tokenId) public {
    safeTransferFrom(from, to, tokenId, "");
}

function safeTransferFrom(address from, address to, uint256 tokenId, bytes memory data) public virtual {
    transferFrom(from, to, tokenId);
    ERC721Utils.checkOnERC721Received(_msgSender(), from, to, tokenId, data);
}

En la versión con el parámetro bytes, data se reenvía al hook onERC721Received del contrato receptor para que el destinatario pueda procesar datos adicionales durante la transferencia. Si el destinatario es un contrato que no implementa onERC721Received o devuelve una respuesta no válida, toda la transacción se revierte.

Tanto safeMint() como safeTransferFrom() siguen el mismo patrón de llamada externa, por lo que la especificación utiliza el mismo contrato receptor simulado al verificar estas funciones.

Verificar formalmente safe mint

Dado que _safeMint() y _safeMint(bytes) son funciones internas, OpenZeppelin las expone a través de funciones de arnés (harness functions) que el Prover puede invocar:

Copy
// ERC721Harness.sol

function safeMint(address to, uint256 tokenId) external {
    _safeMint(to, tokenId);
}

function safeMint(address to, uint256 tokenId, bytes memory data) external {
    _safeMint(to, tokenId, data);
}

La regla safeMint a continuación utiliza method f, la llamada de función arbitraria, de la misma manera que lo hacen las reglas paramétricas. En las reglas paramétricas típicas, tanto la función como los argumentos son arbitrarios (f(e, args)). Aquí, el bloque filtered restringe method f únicamente a las dos variantes de safeMint, y los argumentos to y tokenId se declaran explícitamente en lugar de usar args. Esta declaración explícita permite a la regla aplicar precondiciones que restringen estos argumentos, lo cual no se puede hacer directamente dentro de la construcción calldataarg args. Esto significa que la función es arbitraria dentro de un conjunto permitido, mientras que los argumentos están controlados, lo que difiere de un patrón paramétrico completo.

Aquí está la regla, que analizaremos a continuación:

Copy
// ERC721.spec -- safeMint

rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeMint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256,bytes).selector
} {
    require nonpayable(e);
    // requireInvariant notMintedUnset(tokenId);

    uint256 otherTokenId;
    address otherAccount;

    require balanceLimited(to);

    mathint supplyBefore         = _supply;
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);

    helperMintWithRevert@withrevert(e, f, to, tokenId);
    bool success = !lastReverted;

    assert success <=> (
        ownerBefore == 0 &&
        to != 0
    );

    // effect
    assert success => (
        _supply                   == supplyBefore + 1 &&
        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
        unsafeOwnerOf(tokenId)    == to
    );

    // no side effect
    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
}

Filtrar method f a las variantes de safeMint

El parámetro method f le dice al Prover que pruebe funciones arbitrarias, pero la cláusula filtered limita las pruebas únicamente a las dos versiones de safeMint:

Copy
rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeMint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256,bytes).selector
} {
	...
    helperMintWithRevert@withrevert(e, f, to, tokenId);
	...
}

Para manejar ambas variantes dentro de una sola regla, utilizamos una función auxiliar helperMintWithRevert que enruta la llamada a la versión adecuada según el selector de la función:

Copy
function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
    if (f.selector == sig:safeMint(address,uint256).selector) {
        safeMint(e, to, tokenId);
    } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
        bytes params;
        require params.length < 0xffff;
        safeMint(e, to, tokenId, params);
    } else {
        require false;
    }
}

La función auxiliar permite a la regla probar tanto safeMint() como safeMint(bytes) dentro de una única regla utilizando method f, de modo que no hay necesidad de escribir reglas separadas para cada variante. Enruta la llamada basándose en el selector de la función y dirige la ejecución a la rama if/else correspondiente.

Expliquemos cada condición:

• f.selector == sig:safeMint(address,uint256).selector

  Si la llamada al método arbitrario es safeMint(address,uint256) de dos parámetros, entonces la función auxiliar de CVL invoca safeMint(e, to, tokenId).

• f.selector == sig:safeMint(address,uint256,bytes).selector

  Si la llamada al método arbitrario es safeMint(address, uint256, bytes) de tres parámetros, la función auxiliar de CVL invoca safeMint(e, to, tokenId, params), donde params está restringido a menos de 0xffff ($2^{16} - 1$ o 65,535 bytes) mediante require params.length < 0xffff.

  Dado que bytes es un array de tamaño dinámico, require params.length < 0xffff es un límite de verificación práctico: lo suficientemente grande para cubrir casos de uso realistas para el parámetro data de safeMint, pero lo suficientemente pequeño para evitar que el Prover explore entradas irrealmente grandes.

• else { require false; }

  Esta rama se incluye solo como comodín (catch-all), pero es inalcanzable en esta regla porque la cláusula filtered ya restringe method f a las dos variantes de safeMint. El Prover no puede suministrar ningún otro selector de función, por lo que el bloque else cubre solo un caso teórico que no puede ocurrir bajo la regla filtrada.

Nota: En la especificación original de OpenZeppelin, este auxiliar helperMintWithRevert también contenía una rama para mint(address,uint256)__, pero ese caso ya está excluido por la cláusula filtered en la regla. Dado que la regla solo permite safeMint() y safeMint(bytes)__, eliminamos la rama no utilizada por claridad. Como referencia, aquí está el código original de helperMintWithRevert__.

Despachar onERC721Received al receptor simulado

El DISPATCHER se añade en el bloque methods para instruir al Prover a despachar la llamada a cualquier contrato (denotado por el comodín _) en la escena de verificación que implemente el método especificado (onERC721Received):

Copy
function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);

Dado que solo el receptor simulado implementa este método, el callback siempre se despacha a él. Si varios contratos hubieran implementado onERC721Received, el Prover despacharía a cada uno de ellos y exploraría todas las rutas de verificación.

Sin esto, el Prover trata la llamada a onERC721Received como no resuelta. Como resultado, el Prover produce contraejemplos que violan las afirmaciones debido a la llamada externa no resuelta en las reglas safeMint y safeTransferFrom.

Dispatchee — contrato receptor simulado

Un dispatchee es un contrato en la escena que es el objetivo de la llamada de despacho. La escena debe contener al menos un contrato que implemente onERC721Received. El siguiente contrato proporciona un dispatchee mínimo para este propósito:

Copy
contract ERC721ReceiverHarness is IERC721Receiver {
    function onERC721Received(address, address, uint256, bytes calldata) external pure returns (bytes4) {
        return this.onERC721Received.selector;
    }
}

Esta es una implementación mínima de la interfaz IERC721Receiver. Acepta cualquier token ERC721 entrante y devuelve el selector esperado (0x150b7a02) para señalar una transferencia exitosa. Aunque no ejecuta lógica adicional, le da al Prover un dispatchee válido para onERC721Received.

Especificación completa — safeMint

Las afirmaciones son idénticas a las de la regla mint del capítulo “Mint and Burn”, donde se explican en detalle las comprobaciones de vitalidad (liveness), efecto y ausencia de efectos secundarios (no side-effect). Por este motivo, no repetimos esta discusión aquí y remitimos a los lectores a ese capítulo para una mayor explicación.

A continuación se muestra la especificación CVL completa para safeMint:

Copy
methods {
    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 nonpayable(env e) returns bool = e.msg.value == 0;
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helpers                                                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

function helperMintWithRevert(env e, method f, address to, uint256 tokenId) {
    if (f.selector == sig:safeMint(address,uint256).selector) {
        // safeMint@withrevert(e, to, tokenId);
        safeMint(e, to, tokenId);
    } else if (f.selector == sig:safeMint(address,uint256,bytes).selector) {
        bytes params;
        require params.length < 0xffff;
        // safeMint@withrevert(e, to, tokenId, params);
        safeMint(e, to, tokenId, params);
    } else {
        require false;
    }
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all balances                                                                                  │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

ghost mathint _supply {
    init_state axiom _supply == 0;
}

hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
    _supply = _supply - oldValue + newValue;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: safeMint behavior and side effects                                                                            │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule safeMint(env e, method f, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeMint(address,uint256).selector ||
    f.selector == sig:safeMint(address,uint256,bytes).selector
} {
    require nonpayable(e);
    // requireInvariant notMintedUnset(tokenId);

    uint256 otherTokenId;
    address otherAccount;

    require balanceLimited(to);

    mathint supplyBefore         = _supply;
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);

    helperMintWithRevert@withrevert(e, f, to, tokenId);
    bool success = !lastReverted;
    
		// liveness
    assert success <=> (
        ownerBefore == 0 &&
        to != 0
    );

    // effect
    assert success => (
        _supply                   == supplyBefore + 1 &&
        to_mathint(balanceOf(to)) == balanceOfToBefore + 1 &&
        unsafeOwnerOf(tokenId)    == to
    );

    // no side effect
    assert balanceOf(otherAccount)     != balanceOfOtherBefore => otherAccount == to;
    assert unsafeOwnerOf(otherTokenId) != otherOwnerBefore     => otherTokenId == tokenId;
}

Nota: Una nueva característica del Prover introducida en la versión 8.1.0 permite a las funciones CVL usar @withRevert__. Esto cambia la sintaxis dentro de la función: en lugar de colocar @withRevert en cada invocación de método, ahora se aplica en la función CVL. Actualizamos la sintaxis para que funcione con la última versión del Prover.

Aquí está la ejecución del Prover: enlace

Verificar formalmente safe transferFrom

La función del contrato safeTransferFrom() extiende transferFrom() con la comprobación de seguridad onERC721Received. Por lo tanto, las precondiciones, el estado previo a la llamada y las afirmaciones de la regla safeTransferFrom son idénticas a las de la regla transferFrom del capítulo anterior, pero sigue el mismo patrón de ejecución de método que safeMint:

• utiliza method f con filtrado para probar ambas variantes,
• enruta la ejecución a través de una función auxiliar de CVL, y
• despacha onERC721Received() al receptor simulado.

Aquí está la regla. Al igual que con safeMint, nos centramos en cómo se utilizan el filtrado de métodos, el enrutamiento de funciones auxiliares y el manejo de callbacks externos para verificar ambas variantes de safeTransferFrom:

Copy
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
    f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
} {
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);

    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    helperTransferWithRevert@withrevert(e, f, from, to, tokenId);
    bool success = !lastReverted;

    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1: 0) &&
        to_mathint(balanceOf(to))   == balanceOfToBefore   + assert_uint256(from != to ? 1: 0) &&
        unsafeOwnerOf(tokenId)      == to &&
        unsafeGetApproved(tokenId)  == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

Filtrar method f a las variantes de safeTransferFrom

La regla safeTransferFrom restringe la ejecución a dos métodos (a través de method f), a saber:

• safeTransferFrom(address, address, uint256)
• safeTransferFrom(address, address, uint256, bytes)

Luego pasa la llamada a la función CVL helperTransferWithRevert() como se muestra a continuación:

Copy
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
    f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
} {
	...
    
    helperTransferWithRevert@withrevert(e, f, from, to, tokenId);
    bool success = !lastReverted;

    ...
}

Tenemos una lógica condicional separada para safeTransferFrom(): una para la variante con el parámetro bytes y otra sin él.

Para la variante con bytes, restringimos la longitud del parámetro bytes para que sea menor que 0xffff para mantener el array dentro de un límite práctico y limitar el espacio de exploración. Aparte de esta restricción, ambas variantes de safeTransferFrom() siguen la misma lógica y utilizan la misma estructura de regla:

Copy
function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
    if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
        safeTransferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
        bytes params;
        require params.length < 0xffff; 
        safeTransferFrom(e, from, to, tokenId, params);
    } else {
        calldataarg args;
        f(e, args);
    }
}

Nota: Al igual que la regla safeMint__, la rama condicional f.selector == sig:transferFrom(address,address,uint256).selector se eliminó de esta función CVL porque es innecesaria. La regla ya filtra todas las funciones excepto safeTransferFrom() y safeTransferFrom(bytes)__. Como referencia, aquí está el código original de _helperTransferWithRevert__: _enlace

Despachar el callback onERC721Received

En la sección de safeMint, configuramos el receptor simulado y la configuración DISPATCHER(true) para que el Prover pueda modelar el callback externo onERC721Received.

Aquí se requiere la misma configuración porque tanto safeMint como safeTransferFrom desencadenan una llamada externa a un receptor ERC-721. Sin esta configuración de despacho, el Prover trataría el callback como una llamada externa no resuelta, lo que causa estragos y hace que las afirmaciones posteriores a la llamada carezcan de sentido.

Especificación completa — safeTransferFrom

Las afirmaciones son idénticas a las de la regla transferFrom del capítulo anterior, “Transfer and Approval”, donde se explican en detalle las comprobaciones de vitalidad, efecto y ausencia de efectos secundarios.

A continuación se muestra la especificación CVL completa para safeTransferFrom:

Copy
methods {
    function balanceOf(address) external returns (uint256) envfree;
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;
    function _.onERC721Received(address,address,uint256,bytes) external => DISPATCHER(true);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Definitions                                                                                                         │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

definition nonpayable(env e) returns bool = e.msg.value == 0;
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;
definition authSanity(env e) returns bool = e.msg.sender != 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Helpers                                                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

function helperTransferWithRevert(env e, method f, address from, address to, uint256 tokenId) {
    if (f.selector == sig:safeTransferFrom(address,address,uint256).selector) {
        // safeTransferFrom@withrevert(e, from, to, tokenId);
        safeTransferFrom(e, from, to, tokenId);
    } else if (f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector) {
        bytes params;
        require params.length < 0xffff; 
        // safeTransferFrom@withrevert(e, from, to, tokenId, params);
        safeTransferFrom(e, from, to, tokenId, params);
    } else {
        calldataarg args;
        f@withrevert(e, args);
    }
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Ghost & hooks: sum of all 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);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: safeTransferFrom behavior and side effects                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule safeTransferFrom(env e, method f, address from, address to, uint256 tokenId) filtered { f ->
    f.selector == sig:safeTransferFrom(address,address,uint256).selector ||
    f.selector == sig:safeTransferFrom(address,address,uint256,bytes).selector
} {
    require nonpayable(e);
    require authSanity(e);

    address operator = e.msg.sender;
    uint256 otherTokenId;
    address otherAccount;

    // requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);

    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address approvalBefore       = unsafeGetApproved(tokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    helperTransferWithRevert@withrevert(e, f, from, to, tokenId);
    bool success = !lastReverted;
    
    // liveness
    assert success <=> (
        from == ownerBefore &&
        from != 0 &&
        to   != 0 &&
        (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))
    );

    // effect
    assert success => (
        to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1: 0) &&
        to_mathint(balanceOf(to))   == balanceOfToBefore   + assert_uint256(from != to ? 1: 0) &&
        unsafeOwnerOf(tokenId)      == to &&
        unsafeGetApproved(tokenId)  == 0
    );

    // no side effect
    assert balanceOf(otherAccount)         != balanceOfOtherBefore => (otherAccount == from || otherAccount == to);
    assert unsafeOwnerOf(otherTokenId)     != otherOwnerBefore     => otherTokenId == tokenId;
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

Nota: Una nueva característica del Prover introducida en la versión 8.1.0 permite a las funciones CVL usar @withRevert__. Esto cambia la sintaxis dentro de la función: en lugar de colocar @withRevert en cada invocación de método, ahora se aplica en la función CVL. Actualizamos la sintaxis para que funcione con la última versión del Prover.

Aquí está la ejecución del Prover.

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