Introducción

Este capítulo continúa como la tercera parte (3/5) de nuestro recorrido por el código de la especificación CVL de ERC-721 de OpenZeppelin y se centra en las reglas de transferencia y aprobación de tokens, específicamente:

• transferFrom()
• approve()
• setApprovalForAll()
• zeroAddressBalanceRevert()

Estas reglas verifican las transferencias de propiedad, las aprobaciones por token, las aprobaciones de operadores para todos los tokens, y que consultar balanceOf(0) revierta.

Verificar formalmente transferFrom()

La función transferFrom() cambia la propiedad de un NFT a otra dirección. Asume que el NFT ya ha sido acuñado, y solo puede ser llamada por el propietario, una dirección aprobada para ese ID de token, o un operador aprobado para todos los tokens del propietario.

Aquí está la regla transferFrom que explicaremos sección por sección después del bloque de código:

Copy
rule transferFrom(env e, address from, address to, uint256 tokenId) {
	// preconditions
    require nonpayable(e);
    require authSanity(e);

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

    requireInvariant ownerHasBalance(tokenId);
    require balanceLimited(to);
    
    // pre-call state
    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);
		
	// method call
    transferFrom@withrevert(e, 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;
}

Precondiciones

Estas precondiciones especifican qué debe ser cierto antes de que el Prover ejecute transferFrom(). Explicamos cada línea del bloque de código a continuación:

Copy
require nonpayable(e);
require authSanity(e);
...
requireInvariant ownerHasBalance(tokenId);
require balanceLimited(to);

require nonpayable(e)

Esto requiere que transferFrom() sea llamada sin enviar ETH, ya que la función es non-payable. Se expresa como una definición:

Copy
definition nonpayable(env e) returns bool = e.msg.value == 0;

Define la condición e.msg.value == 0 como una expresión reutilizable llamada nonpayable(e), que verifica que la llamada no lleve ETH.

Aunque el estándar ERC-721 especifica transferFrom() como payable, OpenZeppelin la implementa como non-payable. En la práctica, no se espera que se envíe ETH junto con las transferencias de NFT, por lo que esto se ha convertido en una convención práctica. La regla de CVL impone e.msg.value == 0.

require authSanity(e)

Esto requiere que el llamador no sea la dirección cero. También se expresa como una definition:

Copy
definition authSanity(env e) returns bool = e.msg.sender != 0

Sin este requisito, el Prover trata a address(0) como un llamador válido, a pesar de que ninguna llamada real puede originarse desde address(0). La lógica de autorización del contrato nunca permite que address(0) sea un propietario, una dirección aprobada o un operador, por lo que cualquier violación de address(0) actuando como llamador son falsos positivos.

requireInvariant ownerHasBalance(tokenId)

Esta precondición requiere que el invariante ownerHasBalance(tokenId) (que garantiza que si un token existe, su propietario tiene un balance positivo) se cumpla al inicio de la regla. Obliga al Prover a comenzar en un estado donde cualquier token existente tenga un propietario válido (distinto de cero):

Copy
rule transferFrom(env e, address from, address to, uint256 tokenId) {
	// preconditions
	require nonpayable(e);
	require authSanity(e);
	...
	requireInvariant ownerHasBalance(tokenId); // invariant as a precondition
	require balanceLimited(to);
	...
}

Copy
// invariant as a precondition

invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
    ...

El invariante ownerHasBalance depende de otro invariante balanceOfConsistency a través de un bloque preserved, que verifica que balanceOf, _ownedByUser y los valores ghost _balances sean iguales:

Copy
invariant ownerHasBalance(uint256 tokenId)
    unsafeOwnerOf(tokenId) != 0 => balanceOf(ownerOf(tokenId)) > 0
    {
        preserved { // invariant as a preserved condition
            requireInvariant balanceOfConsistency(ownerOf(tokenId));  
        }
    }

Copy
// invariant as a preserved condition 

invariant balanceOfConsistency(address user)
    to_mathint(balanceOf(user)) == _ownedByUser[user] &&
    to_mathint(balanceOf(user)) == _balances[user];

Al usar el invariante ownerHasBalance(tokenId) como precondición, la regla transferFrom hereda la garantía de balanceOfConsistency:

Copy
rule transferFrom(env e, address from, address to, uint256 tokenId) {
	// preconditions
	require nonpayable(e);
	require authSanity(e);
	...
	requireInvariant ownerHasBalance(tokenId); // invariant as a precondition
	require balanceLimited(to);
	...
}

Si se elimina esta precondición, el Prover puede iniciar la regla en estados imposibles donde la propiedad y los balances no coinciden — por ejemplo, una dirección podría registrarse como la propietaria de un token mientras su balance es cero porque los valores ghost no se alinean con el almacenamiento. Esto conduce a falsos positivos en las violaciones.

require balanceLimited(to)

balanceLimited(to) limita el balance de la dirección receptora (to) para que se mantenga por debajo de max_uint256 tal como se expresa en la definición:

Copy
definition balanceLimited(address account) returns bool = balanceOf(account) < max_uint256;

El contrato incrementa los balances dentro de un bloque unchecked para mejorar la eficiencia del gas. Aunque el desbordamiento es prácticamente imposible, el Prover aún explora casos de desbordamiento porque transferFrom() llama a _update(), donde el incremento del balance ocurre dentro de un bloque unchecked:

Copy
// ERC721.sol

function transferFrom(address from, address to, uint256 tokenId) public virtual {
    ...
    address previousOwner = _update(to, tokenId, _msgSender());
    ..
}

Copy
/// ERC721.sol

function _update(address to, uint256 tokenId, address auth) internal virtual returns (address) {
    ...

    if (to != address(0)) {
        unchecked {
            _balances[to] += 1;
        }
    }
	  ...
}

El uso de require balanceLimited(to) descarta estados de desbordamiento prácticamente inalcanzables que harían que la regla fallara en escenarios poco realistas.

Estado antes de la llamada (Pre-call state)

Antes de invocar el método tra``nsferFrom(), registramos las variables de estado para compararlas con los valores posteriores a la llamada:

• balanceOfFromBefore es el balance del remitente (from) antes de la transferencia.
• balanceOfToBefore es el balance del receptor (to) antes de la transferencia.
• balanceOfOtherBefore es el balance de una cuenta no involucrada (otherAccount) antes de la transferencia.
• ownerBefore es el propietario del token que se va a transferir.
• otherOwnerBefore es el propietario de un token no involucrado.
• approvalBefore es la aprobación del token que se va a transferir.
• otherApprovalBefore es la aprobación de un token no involucrado.

Copy
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);

Note que leemos las aprobaciones usando unsafeGetApproved(), una función harness, en lugar del getApproved() del contrato. La versión harness expone el valor de aprobación incluso cuando el token no está acuñado o ha sido quemado (owner == address(0)) porque devuelve _getApproved(tokenId) sin verificar si el token existe o tiene un propietario. Por el contrario, getApproved() en el contrato real realiza una verificación de propiedad y revierte si el token no está acuñado o ha sido quemado:

Copy
// ERC721Harness.sol -- returns approval without checking token existence or ownership

function unsafeGetApproved(uint256 tokenId) external view returns (address) {
    return _getApproved(tokenId);
}

Copy
// ERC721.sol -- performs an ownership check and reverts if the token is unminted or burned

function getApproved(uint256 tokenId) public view virtual returns (address) {
    _requireOwned(tokenId); // reverts if `owner == address(0)`

    return _getApproved(tokenId);
}

Esto evita consultar el estado de aprobación de tokens no acuñados o quemados porque getApproved() revierte en esos casos. Sin embargo, la regla necesita comparar valores de aprobación a través de transiciones de estado que pasan por el estado de dirección cero:

• creación del token (de no acuñado a acuñado) — el propietario transita de address(0) a una dirección distinta de cero
• destrucción del token (de acuñado a no acuñado/quemado) — el propietario transita de una dirección distinta de cero de vuelta a address(0)

De ahí la necesidad de unsafeGetApproved(), para que la regla pueda leer los valores de aprobación incluso cuando el token se encuentra en el estado de propietario con dirección cero.

Ahora que el estado previo a la llamada está registrado, ejecutamos transferFrom() y razonamos sobre los valores posteriores a la llamada en las aserciones que siguen.

Llamada de transferencia

La llamada transferFrom() con @withrevert instruye al Prover a explorar tanto las rutas que revierten como las que no revierten. La condición !lastReverted captura si la llamada no revirtió y almacena esto como success:

Copy
transferFrom@withrevert(e, from, to, tokenId);
bool success = !lastReverted;

Aserciones — liveness, effect, y no side effect

Liveness:

Una transferencia no revierte si y solo si (<=>) se cumple todo lo siguiente:

• from == ownerBefore

  La dirección from (desde la cual se está transfiriendo el token) debe ser el propietario anterior del token.

• from != 0

  La dirección from no debe ser la dirección cero.

• to != 0

  La dirección to (receptor) no debe ser la dirección cero.

• (operator == from || operator == approvalBefore || isApprovedForAll(ownerBefore, operator))

  El operador (llamador) debe tener autorización a través de al menos una de las siguientes:

  • operator == from — el propietario transfiere su propio token
  • operator == approvalBefore — el operador tiene aprobación específica para este token (vía approve())
  • isApprovedForAll(ownerBefore, operator) — el operador tiene aprobación general para todos los tokens del propietario (vía setApprovalForAll())

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

Effect:

Si la transferencia no revierte, se aplican los siguientes cambios de estado:

• to_mathint(balanceOf(from)) == balanceOfFromBefore - assert_uint256(from != to ? 1 : 0)

  El balance del remitente disminuye en 1, excepto en una autotransferencia (from == to) donde permanece sin cambios.

• to_mathint(balanceOf(to)) == balanceOfToBefore + assert_uint256(from != to ? 1 : 0)

  El balance del receptor aumenta en 1, excepto en una autotransferencia (from == to) donde permanece sin cambios.

• unsafeOwnerOf(tokenId) == to

  La dirección receptora (to) se convierte en el nuevo propietario de tokenId.

• unsafeGetApproved(tokenId) == 0

  La aprobación para tokenId se borra.

Copy
// 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:

Después de afirmar los cambios de estado previstos (effect), también verificamos que no ocurran efectos no deseados en los balances, la propiedad o las aprobaciones:

• En el balance

  balanceOf(otherAccount) != balanceOfOtherBefore => (otherAccount == from || otherAccount == to)

  Si el balance de cualquier cuenta cambia, implica (=>) que la cuenta es o bien el remitente o el receptor. Ninguna otra cuenta no involucrada tuvo su balance modificado.

• En la propiedad

  unsafeOwnerOf(otherTokenId) != otherOwnerBefore => otherTokenId == tokenId

  Si la propiedad de cualquier token cambia, implica (=>) que el token fue el que se transfirió. Ningún otro token no involucrado tuvo un cambio en su propiedad.

• En la aprobación

  unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId

  Si la aprobación de cualquier token cambia, implica (=>) que el token fue el que se transfirió. Ningún otro token no involucrado tuvo su aprobación modificada.

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

Aquí están las especificaciones completas para la regla transferFrom:

Copy
methods {
    function balanceOf(address) external returns (uint256) envfree;
    function ownerOf(uint256) external returns (address) 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;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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];

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: transferFrom behavior and side effects                                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferFrom(env e, address from, address to, uint256 tokenId) {
    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);

    transferFrom@withrevert(e, 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;
}

Aquí está la ejecución del Prover.

Ahora que hemos verificado transferFrom``(), podemos pasar a los mecanismos de aprobación que autorizan estas transferencias.

Recuerde que transferFrom() tiene éxito solo cuando el llamador tiene la autorización adecuada: como el propietario del token, como una dirección aprobada para ese token, o como un operador aprobado para todos los tokens del propietario. Las siguientes dos reglas verifican las funciones que otorgan estos permisos: approve() para la autorización por token y setApprovalForAll() para la autorización a nivel de operador.

Verificar formalmente approve()

La función de contrato approve() otorga a una dirección el permiso para transferir un token específico. Tiene éxito solo si el token existe y el llamador es el propietario o un operador (tiene aprobación general).

Aquí está la regla que verifica este comportamiento:

Copy
rule approve(env e, address spender, uint256 tokenId) {
	// preconditions
    require nonpayable(e);
    require authSanity(e);
		
	// pre-call state
    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
		
	// method call
    approve@withrevert(e, spender, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

Precondiciones

A estas alturas, ya sabemos que nonpayable(e) requiere que la llamada se envíe sin Ether, y authSanity(e) requiere que msg.sender no sea la dirección cero:

Copy
require nonpayable(e);
require authSanity(e);

Llamada de approve

Como un patrón común en las especificaciones de reglas ERC-721 de OpenZeppelin, el método approve se llama con @withrevert, y el resultado de !lastReverted se almacena en la variable success para razonar sobre el caso en el que la llamada tiene éxito:

Copy
approve@withrevert(e, spender, tokenId);
bool success = !lastReverted;

Aserciones — liveness, effect, y no side effect

Liveness:

Esto significa que la llamada a la función no revierte “si y solo si” se cumplen las siguientes condiciones:

• owner != 0

  El propietario del token no debe ser la dirección cero. Esto evita aprobar un token que no existe o fue quemado.

• (owner == caller || isApprovedForAll(owner, caller))

  Esta es una verificación de autorización donde el caller debe ser o bien:

  • El owner del token, o
  • Ser un operador aprobado mediante isApprovedForAll(owner, caller) (devuelve verdadero)

Copy
// liveness
assert success <=> (
    owner != 0 &&
    (owner == caller || isApprovedForAll(owner, caller))
);

Effect:

• assert success => unsafeGetApproved(tokenId) == spender

  Si la llamada tuvo éxito (success == true), entonces la dirección aprobada para tokenId ahora debe ser igual a spender.

Copy
// effect
assert success => unsafeGetApproved(tokenId) == spender;

No side effect:

• assert unsafeGetApproved(otherTokenId) != otherApprovalBefore => otherTokenId == tokenId

  Si la dirección aprobada para otherTokenId cambia, entonces otherTokenId debe ser el mismo que tokenId. Significa que solo tokenId (el objetivo previsto) tiene su aprobación actualizada y ningún otro token (otherTokenId) se ve afectado accidentalmente.

Copy
// no side effect
assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;

Aquí está la especificación completa para la regla approve:

Copy
methods {
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;
}

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

definition nonpayable(env e) returns bool = e.msg.value == 0;
definition authSanity(env e) returns bool = e.msg.sender != 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: approve behavior and side effects                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approve(env e, address spender, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    approve@withrevert(e, spender, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

Aquí está la ejecución del Prover.

Verificar formalmente setApprovalForAll()

La función setApprovalForAll() autoriza a una dirección a administrar todos los tokens propiedad del llamador. Aquí está la regla:

Copy
rule setApprovalForAll(env e, address operator, bool approved) {
	// preconditions
    require nonpayable(e);
		
	// pre-call state
    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

En este punto, ya estamos familiarizados con el patrón de precondiciones, los estados previos y posteriores a la llamada, y la llamada al método, así que nos saltaremos eso y pasaremos directamente a las aserciones.

Aserciones — liveness, effect, y no side effect

Liveness:

• assert success <=> operator != 0

  La llamada tiene éxito si y solo si el operador no es la dirección cero. ERC-721 prohíbe aprobar a la dirección cero como operador, por lo que esta aserción requiere que la llamada falle cuando operator == 0:

Copy
// liveness
assert success <=> operator != 0;

Effect:

• assert success => isApprovedForAll(owner, operator) == approved

  Si la llamada tuvo éxito, el estado de aprobación del par (owner, operator) debe coincidir con el valor booleano approved. Significa que el valor de aprobación (verdadero o falso) se estableció correctamente.

  Copy
  // effect
  assert success => isApprovedForAll(owner, operator) == approved;
  

No side effect:

• Si el estado de aprobación de cualquier (otherOwner, otherOperator) cambia, esas direcciones deben coincidir con el llamador (owner) y el operador designado (operator). Cualquier cambio en una entrada de aprobación diferente hace que esta aserción falle.

Copy
// no side effect
assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
    otherOwner    == owner &&
    otherOperator == operator
);

Aquí está la especificación completa de CVL para la regla setApprovalForAll:

Copy
methods {
    function unsafeOwnerOf(uint256) external returns (address) envfree;
    function unsafeGetApproved(uint256) external returns (address) envfree;
    function isApprovedForAll(address,address) external returns (bool) envfree;
}

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

definition nonpayable(env e) returns bool = e.msg.value == 0;
definition authSanity(env e) returns bool = e.msg.sender != 0;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: setApprovalForAll behavior and side effects                                                                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule setApprovalForAll(env e, address operator, bool approved) {
    require nonpayable(e);

    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

Aquí está la ejecución del Prover.

Verificar formalmente que balanceOf(0) revierte

La siguiente regla verifica que la función balanceOf siempre revierte cuando se consulta la dirección cero.

A continuación se muestra la implementación de balanceOf en el contrato. Revierte si owner == address(0):

Copy
function balanceOf(address owner) public view virtual returns (uint256) {
    if (owner == address(0)) {
        revert ERC721InvalidOwner(address(0));

    }
    return _balances[owner];
}

Aquí está la regla que verifica este comportamiento:

Copy
methods {
    function balanceOf(address) external returns (uint256) envfree;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: balance of address(0) is 0                                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule zeroAddressBalanceRevert() {
    balanceOf@withrevert(0);
    assert lastReverted;
}

Aquí está la ejecución del Prover:

Especificación completa para transferencia y aprobación

Aquí está la especificación completa y la ejecución del Prover.

Copy
methods {
    function balanceOf(address) external returns (uint256) envfree;
    function ownerOf(uint256) external returns (address) 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;

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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);
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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];

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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));
        }
    }

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: transferFrom behavior and side effects                                                                        │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule transferFrom(env e, address from, address to, uint256 tokenId) {
    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);

    transferFrom@withrevert(e, 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;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: approve behavior and side effects                                                                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule approve(env e, address spender, uint256 tokenId) {
    require nonpayable(e);
    require authSanity(e);

    address caller = e.msg.sender;
    address owner = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;

    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

    approve@withrevert(e, spender, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        owner != 0 &&
        (owner == caller || isApprovedForAll(owner, caller))
    );

    // effect
    assert success => unsafeGetApproved(tokenId) == spender;

    // no side effect
    assert unsafeGetApproved(otherTokenId) != otherApprovalBefore  => otherTokenId == tokenId;
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: setApprovalForAll behavior and side effects                                                                   │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule setApprovalForAll(env e, address operator, bool approved) {
    require nonpayable(e);

    address owner = e.msg.sender;
    address otherOwner;
    address otherOperator;

    bool otherIsApprovedForAllBefore = isApprovedForAll(otherOwner, otherOperator);

    setApprovalForAll@withrevert(e, operator, approved);
    bool success = !lastReverted;

    // liveness
    assert success <=> operator != 0;

    // effect
    assert success => isApprovedForAll(owner, operator) == approved;

    // no side effect
    assert isApprovedForAll(otherOwner, otherOperator) != otherIsApprovedForAllBefore => (
        otherOwner    == owner &&
        otherOperator == operator
    );
}

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ Rule: balance of address(0) is 0                                                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/
rule zeroAddressBalanceRevert() {
    balanceOf@withrevert(0);
    assert lastReverted;
}

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