Introducción

ERC-721 es el estándar de Ethereum para tokens no fungibles, ampliamente utilizado para representar propiedad digital. Como cualquier forma de propiedad, gira en torno a la creación de suministro, la eliminación de suministro y las transferencias de propiedad.

Este capítulo se centra en verificar formalmente las operaciones de mint y burn. Es la primera parte (1/5) del análisis de código de la especificación CVL de ERC-721 de OpenZeppelin.

A lo largo de sus especificaciones, OpenZeppelin utiliza un patrón que combina tres tipos de aserciones en una sola regla, categorizadas como:

1. Liveness — especifica las condiciones bajo las cuales la función no revierte.
2. Effect — especifica los cambios de estado que ocurrieron cuando la función no revirtió.
3. No side-effect — especifica que no ocurren cambios de estado no intencionados más allá de los de la aserción de Effect.

Exposición de las funciones internas _mint() y _burn() para verificación

_mint() y _burn() son funciones internas pensadas para que los desarrolladores hereden de ellas y construyan lógica personalizada para crear y destruir NFTs. En esta especificación, el contrato harness las hereda y expone como funciones externas, lo que permite al Prover invocar _mint() y _burn() durante la verificación.

Las siguientes son las implementaciones de OpenZeppelin de:

• _mint()
• _burn()
• el harness que las expone

Copy
// ERC721.sol

function _mint(address to, uint256 tokenId) internal {
    if (to == address(0)) {
        revert ERC721InvalidReceiver(address(0));
    }
    address previousOwner = _update(to, tokenId, address(0));
    if (previousOwner != address(0)) {
        revert ERC721InvalidSender(address(0));
    }
}
...

function _burn(uint256 tokenId) internal {
    address previousOwner = _update(address(0), tokenId, address(0));
    if (previousOwner == address(0)) {
        revert ERC721NonexistentToken(tokenId);
    }
}

Copy
// ERC721Harness.sol

function mint(address account, uint256 tokenId) external {
    _mint(account, tokenId);
}
...

function burn(uint256 tokenId) external {
    _burn(tokenId);
}

Verificar formalmente mint

La operación mint() crea un nuevo token y se lo asigna a un destinatario. Verificamos formalmente que:

• no revierte si y solo si el token no ha sido acuñado y el destinatario es válido
• si no revierte, tanto el suministro total como el balance del destinatario aumentan en uno
• el destinatario se convierte en el propietario
• no cambia el balance de ninguna otra cuenta ni la propiedad de ningún otro token

Aquí está la regla CVL que demuestra estas propiedades:

Copy
// ERC721.spec -- mint (explanation follows)


rule mint(env e, address to, uint256 tokenId) {
	// preconditions
	require nonpayable(e);
	// requireInvariant notMintedUnset(tokenId);

    uint256 otherTokenId;
    address otherAccount;

    require balanceLimited(to);
    
	// pre-call state
    mathint supplyBefore         = _supply;
    uint256 balanceOfToBefore    = balanceOf(to);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
		
	// method call
    mint@withrevert(e, 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;
}

Discutiremos las secciones de la regla anterior de la siguiente manera:

• Precondiciones
• Estado previo a la llamada
• Llamada a mint
• Aserciones
  • liveness
  • effect
  • no side-effect

Precondiciones

Una precondición es una restricción en una regla que especifica lo que debe ser verdadero antes de que el Prover ejecute el método mint(). Puede o no mantenerse “después” de la llamada, dependiendo de los cambios de estado causados por el método.

Las siguientes son las precondiciones para la regla mint:

Copy
require nonpayable(e);
// requireInvariant notMintedUnset(tokenId); // intentionally commented out
...

require balanceLimited(to);

Nota: Para simplificar la discusión, la precondición invariante notMintedUnset(tokenId) está comentada, ya que la regla mint se verifica exitosamente sin ella. Cubriremos los invariantes CVL del código base de ERC-721 en el próximo capítulo.

• require nonpayable(e)

  Esto requiere que la llamada se realice sin enviar ningún ETH porque mint() es non-payable. nonpayable(e) se expresa como una definition que devuelve true si e.msg.value == 0 y false en caso contrario:

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

  Encapsula la lógica para comprobar que una llamada no lleva ETH al vincular la condición e.msg.value == 0 a una expresión reutilizable llamada nonpayable(e). Esta definición nos permite hacer referencia a la condición a lo largo de toda la especificación, en lugar de escribir e.msg.value == 0 repetidamente cada vez que invocamos una función non-payable.

  Nota: definition es un tema amplio en CVL. Para más información, consulta la documentación de Certora. En esta serie, las definiciones se utilizan de manera directa como expresiones reutilizables para mejorar la legibilidad del código.

• require balanceLimited(to)

  Esto requiere que el balance del destinatario sea menor que max_uint256. También se expresa como una definition que devuelve true si balanceOf(account) < max_uint256:

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

  La implementación de ERC-721 de OpenZeppelin incrementa intencionalmente los balances dentro de un bloque unchecked para optimizar el gas. El desbordamiento (overflow) es teóricamente posible pero prácticamente imposible, ya que alcanzar max_uint256 requeriría acuñar más NFTs de los que realista y físicamente podrían existir. Por lo tanto, la precondición require balanceLimited(to) es razonable.

  Sin la precondición balanceLimited(to), el Prover considerará los casos de desbordamiento, ya que mint() llama a la función _update(), donde el incremento del balance ocurre dentro de un bloque unchecked:

  Copy
  // ERC721.sol
  
  function _mint(address to, uint256 tokenId) internal {
      ...
      address previousOwner = _update(to, tokenId, address(0));
      ...
  }
  

  Copy
  /// ERC721.sol
  
  function _update(address to, uint256 tokenId, address auth) internal virtual returns (address) {
      ...
  
      if (to != address(0)) {
          unchecked {
              _balances[to] += 1;
          }
      }
  	  ...
  }
  

Registrar el estado previo a la llamada — suministro total, balances y propiedad antes de la llamada a mint

Los siguientes estados se registran antes de invocar la función mint(). Estos valores luego se comparan con los valores posteriores a la llamada en la sección de aserciones:

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

• mathint supplyBefore = _supply

  Esto registra el suministro total antes de la llamada a mint, para compararlo con el suministro posterior a la acuñación (post-mint) y confirmar que ha aumentado en 1.

  _supply es una variable ghost que rastrea el suministro total y se actualiza a través de un hook Sstore a medida que se añaden nuevos balances y se restan los antiguos.

  La variable ghost _supply está declarada como un mathint, por lo tanto, supplyBefore también debe ser un mathint. Si supplyBefore se declarara como uint256, el Prover reportaría un error de tipo. Este error surge porque mathint representa un entero matemático no delimitado, mientras que uint256 representa un entero delimitado. Asignar un valor mathint a un uint256 asumiría que el valor cabe dentro de 256 bits, lo cual el Prover no puede asumir de forma segura.

  Aquí está la implementación del hook Sstore que actualiza la variable ghost _supply:

  Copy
  ghost mathint _supply {
      init_state axiom _supply == 0;
  }
  
  hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) {
      _supply = _supply - oldValue + newValue;
  }
  

• uint256 balanceOfToBefore = balanceOf(to)

  Esto registra el balance del destinatario antes de la llamada a mint, para compararlo con el balance post-mint y confirmar que también ha aumentado en 1.

• uint256 balanceOfOtherBefore = balanceOf(otherAccount)

  Esto registra el balance de cualquier otra cuenta antes de la llamada a mint, para compararlo con el balance post-mint y confirmar que no ha cambiado, y por lo tanto no hay efectos secundarios.

• address ownerBefore = unsafeOwnerOf(tokenId)

  Esto registra al propietario del token antes de la llamada a mint. Para que el mint tenga éxito, este valor debe ser cero, lo cual es una de las condiciones de liveness (ownerBefore == 0 y to != 0).

  unsafeOwnerOf() es una función harness que expone la propiedad incluso para tokens sin un propietario válido. Devuelve la dirección cero para tokens no acuñados, a diferencia de ownerOf(), que revertiría en esos casos. Esto permite a la regla comparar la propiedad antes y después de la acuñación, ya que esas transiciones de propiedad implican el paso de la dirección cero (estado no acuñado) a una dirección de propietario válida.

• address otherOwnerBefore = unsafeOwnerOf(otherTokenId)

  Esto registra al propietario de un token arbitrario (distinto al que se está acuñando) antes de la llamada a mint para que podamos confirmar que no ha cambiado post-mint, y por lo tanto no hay efectos secundarios.

Llamada a mint

La etiqueta @withrevert permite al Prover explorar tanto las rutas que revierten como las que no. La condición !lastReverted captura si la llamada no revirtió y almacena esto como success:

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

Aserciones — liveness, effect y no side effect

Como se mencionó anteriormente, el patrón de reglas utilizado a lo largo de la especificación combina liveness, effect y no side-effect en una sola regla. Aquí está el bloque de código que posteriormente explicaremos en detalle:

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

Liveness:

La aserción a continuación establece que _mint() no revierte si y solo si el token no ha sido acuñado (ownerBefore == 0) y el destinatario es válido (to != 0):

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

Utilizamos el patrón de revert y disyunción en los dos capítulos anteriores. Si fuéramos a convertir la aserción anterior a ese patrón, se convertiría en:

_mint() revierte si y solo si el token ya está acuñado (ownerBefore != 0) o el destinatario no es válido (to == 0).

Copy
// reverts
assert !success <=> (
    ownerBefore != 0 ||
    to == 0
);

Mientras que el patrón de “éxito + conjunción” (liveness) enumera todas las condiciones bajo las cuales la función tiene éxito, el patrón de “revert + disyunción” enumera todas las condiciones bajo las cuales revierte. Son lógicamente equivalentes.

Effect:

Si la función mint() no revierte, entonces los cambios de estado resultantes son:

• el suministro total aumenta exactamente en uno (_supply == supplyBefore + 1)
• el balance del destinatario aumenta exactamente en uno (balanceOf(to) == balanceOfToBefore + 1)
• el token ahora es propiedad del destinatario (unsafeOwnerOf(tokenId) == to)

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

No side effect:

Las siguientes aserciones comprueban que la función mint() no causa efectos secundarios no intencionados:

• assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == to

  Esto comprueba que solo cambie el balance del destinatario previsto, sin afectar a todas las demás cuentas. Si el balance de una cuenta cambia después de la llamada a mint, entonces esa cuenta es el destinatario (to). Si el balance de una cuenta no cambia, entonces esa cuenta no es el destinatario y, por lo tanto, no se ve afectada por la llamada a mint.

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

  Esto comprueba que solo cambie el propietario del token acuñado, sin afectar a todos los demás tokens. Si el propietario de un token cambia después de la llamada a mint, entonces ese token es el token acuñado. Si el propietario de un token no cambia, entonces ese token no es el token acuñado y, por lo tanto, su propiedad no se ve afectada por la llamada a mint.

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

Ahora, aquí está la especificación completa, que incluye la regla mint, las definiciones, los ghosts y los hooks:

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

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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: mint behavior and side effects                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule mint(env e, address to, uint256 tokenId) {
    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);

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

Aquí está la ejecución del Prover.

Verificar formalmente burn

La operación burn realiza los cambios de estado opuestos a mint.

Al acuñar (minting), los cambios de estado son:

• _supply aumenta en 1
• balanceOf(to) aumenta en 1
• ownerOf(tokenId) cambia del valor anterior address(0) a una dirección distinta de cero

Al quemar (burning), ocurre lo contrario:

• _supply disminuye en 1
• balanceOf(from) disminuye en 1
• ownerOf(tokenId) cambia de su dirección anterior distinta de cero de vuelta a address(0)

A diferencia de mint, donde los tokens son recién creados sin aprobaciones existentes, las operaciones burn deben eliminar cualquier aprobación existente como parte de la limpieza del token.

Teniendo en mente estos comportamientos, verificamos formalmente que:

• no revierte si y solo si el token existe (es decir, el propietario no es address(0))
• si la llamada tiene éxito, el suministro total disminuye en uno y el balance del propietario anterior disminuye en uno
• el propietario se establece en address(0), lo que significa que el token no tiene propietario
• la aprobación del token se borra
• no cambian los balances de otras cuentas, la propiedad de otros tokens ni las aprobaciones

Aquí está la regla CVL que demuestra estas propiedades:

Copy
// ERC721.spec -- burn (explanation follows) 

rule burn(env e, uint256 tokenId) {
	// preconditions
    require nonpayable(e);

    address from = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;
    address otherAccount;

    // requireInvariant ownerHasBalance(tokenId);
    
    // pre-call state
    mathint supplyBefore         = _supply;
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);
		
	// method call
    burn@withrevert(e, tokenId);
    bool success = !lastReverted;

    // liveness
    assert success <=> (
        ownerBefore != 0
    );

    // effect
    assert success => (
        unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
        unsafeOwnerOf(tokenId)      == 0 &&
        unsafeGetApproved(tokenId)  == 0
    );

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

Precondiciones

Al igual que la regla mint, esta regla es non-payable. Por lo tanto, require nonpayable(e) es necesario:

Copy
require nonpayable(e);
...

Registrar el estado previo a la llamada — suministro total, balances, propiedad y aprobación antes de la llamada a burn

Todos los estados previos a la llamada registrados en la regla mint también aparecen en la regla burn, excepto por los siguientes:

• uint256 balanceOfFromBefore = balanceOf(from)

  En lugar de registrar el estado previo a la llamada del receptor del mint (balanceOf(to)), la regla burn registra el balance del propietario (balanceOf(from)) para verificar que, al final de la llamada a burn, el balance disminuye en 1.

• address otherApprovalBefore = unsafeGetApproved(otherTokenId)

  La aprobación es necesaria en la función burn; por lo tanto, registra la aprobación de otro token arbitrario para verificar que permanece sin cambios.

Llamada a burn

Como en reglas anteriores, la llamada utiliza la etiqueta @withrevert. El booleano success captura si la llamada no revirtió (!lastReverted), lo cual se utiliza para verificar los cambios esperados entre los estados previos y posteriores a la llamada:

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

Aserciones — liveness, effect**, y no side effect**

Todos los valores recuperados aquí son estados posteriores a la llamada comparados con estados previos a la llamada:

Copy
// liveness
assert success <=> (
    ownerBefore != 0
);

// effect
assert success => (
    unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
    to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
    unsafeOwnerOf(tokenId)      == 0 &&
    unsafeGetApproved(tokenId)  == 0
);

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

Liveness:

Afirma que la llamada a burn no revierte si y solo si el tokenId a quemar tiene un propietario.

Effect:

Si la llamada a burn no revierte, significa que todos los siguientes cambios de estado deben haber ocurrido:

• unsafeOwnerOf(tokenId) != 0 => (_supply == supplyBefore - 1)

  Si el token está acuñado (tiene un propietario distinto de cero), entonces el suministro disminuye en exactamente 1. Esto significa que la disminución en el suministro solo se comprueba cuando hay al menos un token acuñado.

• to_mathint(balanceOf(from)) == balanceOfFromBefore - 1

  El balance de la dirección from (el propietario del token) ha disminuido en 1.

• unsafeOwnerOf(tokenId) == 0

  La propiedad del token ha sido borrada, por lo que unsafeOwnerOf(tokenId) devuelve 0.

• unsafeGetApproved(tokenId) == 0

  Cualquier aprobación existente para el token ha sido eliminada, por lo que unsafeGetApproved(tokenId) devuelve 0.

No side effect:

• assert balanceOf(otherAccount) != balanceOfOtherBefore => otherAccount == from

  Esto comprueba que solo cambie el balance del propietario pre-burn (antes de la quema), sin afectar a todas las demás cuentas. Si el balance de una cuenta cambia después de la llamada a burn, entonces esa cuenta es el propietario antes del burn.

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

  Esto comprueba que solo cambie la propiedad del token quemado, sin afectar a todos los demás tokens. Si el propietario de un token cambia después de la llamada a burn, entonces ese token es el token quemado.

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

  Esto comprueba que solo se borre la aprobación del token quemado, sin afectar las aprobaciones de todos los demás tokens. Si la aprobación para un token cambia después de la llamada a burn, entonces ese token es el token quemado.

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

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

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

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

/*
┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│ 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: burn behavior and side effects                                                                                │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
*/

rule burn(env e, uint256 tokenId) {
    require nonpayable(e);

    address from = unsafeOwnerOf(tokenId);
    uint256 otherTokenId;
    address otherAccount;

    // requireInvariant ownerHasBalance(tokenId);

    mathint supplyBefore         = _supply;
    uint256 balanceOfFromBefore  = balanceOf(from);
    uint256 balanceOfOtherBefore = balanceOf(otherAccount);
    address ownerBefore          = unsafeOwnerOf(tokenId);
    address otherOwnerBefore     = unsafeOwnerOf(otherTokenId);
    address otherApprovalBefore  = unsafeGetApproved(otherTokenId);

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

    // liveness
    assert success <=> (
        ownerBefore != 0
    );

    // effect
    assert success => (
        unsafeOwnerOf(tokenId)      != 0 => (_supply == supplyBefore - 1) && // modified for the Prover v8.3.1
        to_mathint(balanceOf(from)) == balanceOfFromBefore - 1 &&
        unsafeOwnerOf(tokenId)      == 0 &&
        unsafeGetApproved(tokenId)  == 0
    );

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

Nota: La línea requireInvariant ownerHasBalance(tokenId) está comentada porque el Prover 8.3.1 reporta violaciones de este invariante, por lo que no puede aplicarse en esta especificación. Esto llevó a ajustar la aserción de “effect” de _supply == supplyBefore - 1 a unsafeOwnerOf(tokenId) != 0 => (_supply == supplyBefore - 1). Todos los invariantes, incluyendo ownerHasBalance(tokenId), se discutirán en el próximo capítulo.

Aquí está la ejecución del Prover para la regla burn.

Especificaciones completas para mint y burn

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

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