Verificar formalmente un token ERC-20 Introducción En este capítulo, verificamos formalmente la implementación ERC-20 de Solmate, la cual incluye lo siguiente: Funciones estándar de cambio de estado: , , Funciones view estándar...

Restringir variables fantasma en invariantes En el capítulo anterior, vimos cómo las variables fantasma sin restricciones pueden generar falsos positivos. También aprendimos cómo se puede usar una sentencia para restringir eficazmente...

Restringiendo los valores fantasma en las reglas En el capítulo anterior, aprendimos cómo las variables fantasma permiten que la información fluya desde los hooks hacia las reglas. También aprendimos que: Al inicio de la verificación...

Uso de hooks de Sstore con mappings de almacenamiento Introducción En el capítulo “Introducción a Storage Hooks y Ghosts”, cubrimos los hooks de almacenamiento y los ghosts con variables de almacenamiento simples. Mostramos que...

Reglas parcialmente paramétricas para ERC-721 Introducción Este capítulo es la parte final (5/5) del recorrido por el código de la especificación CVL de ERC-721 de OpenZeppelin, la cual verifica formalmente lo siguiente...

Introducción a los Storage Hooks y Ghosts A menudo resulta necesario inspeccionar los cambios en ubicaciones de almacenamiento específicas para demostrar que una propiedad o invariante se cumple, especialmente cuando el almacenamiento no...

Verificando un Invariante Usando Ghost y Hook En cualquier implementación correcta de ERC20, la suma de todos los balances de las cuentas debe ser siempre igual al suministro total de tokens. Esta propiedad siempre debería mantenerse verdadera...

Reglas de Mint y Burn para ERC-721 Introducción ERC-721 es el estándar de Ethereum para tokens no fungibles, ampliamente utilizado para representar la propiedad digital. Como cualquier forma de propiedad, gira en torno a la oferta...

Overflow y Mathint En CVL, el tipo representa enteros no acotados, a diferencia de los tipos de tamaño fijo de Solidity como . Realiza operaciones aritméticas sin overflow ni underflow, lo que permite razonar basándose en...

Introducción a las propiedades de los métodos Introducción En el capítulo anterior, aprendimos sobre las reglas paramétricas, las cuales nos permiten verificar formalmente propiedades que se espera que se cumplan independientemente de qué...

Entendiendo el Spec File en Certora CVL En el último capítulo, vimos que para realizar la verificación formal utilizando Certora Prover, necesitamos proporcionar al Prover los siguientes elementos clave: Smart...

Introducción al Operador de Implicación El operador de implicación se utiliza frecuentemente como sustituto de la sentencia ya que es más limpio. Considere el siguiente ejemplo: una función que toma dos unsigned...