Llamada a biblioteca en Starknet Una llamada a biblioteca ejecuta la lógica de una clase de contrato declarada en el contexto y almacenamiento del contrato que la invoca. Esto es similar a la de Solidity, pero utiliza class hashes...

Funciones Hash en Starknet. Solidity se basa en keccak-256 como su función hash principal para derivar identificadores deterministas a partir de datos arbitrarios, como el cálculo de selectores de funciones o el cálculo de almacenamiento...

Syscalls in Starknet In Solidity, low-level operations like reading/writing to storage, contract to contract calls, or sending messages are performed directly through inline assembly using Yul...

Uso de “requireInvariant" en reglas e invariantes Hasta ahora, hemos escrito una regla para verificar comportamientos específicos o un invariante para verificar propiedades que siempre deben cumplirse a lo largo del...

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...

Preserved Block y su rol en la verificación de invariantes Un invariante es una propiedad que siempre debe cumplirse después de que se despliega un smart contract y a lo largo de toda su ejecución. A primera vista,...

Introducción a los Invariantes en Certora Hasta ahora, nos hemos enfocado en verificar el comportamiento de métodos individuales o secuencias de métodos — asegurando que una llamada de función específica o un conjunto de llamadas,...

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...

Verificar formalmente WETH de Solady Introducción ETH, ampliamente utilizado en DeFi para swaps, provisión de liquidez, staking y colateral, necesita una versión compatible con ERC-20 para que los protocolos puedan interactuar con él a través de...

Invariantes para ERC-721 Introducción En capítulos anteriores, exploramos cómo funcionan los invariantes de CVL: propiedades que deben cumplirse a lo largo de toda la ejecución del contrato. Los invariantes pueden funcionar como precondiciones en...

Bucles en CVL: explosión de caminos y desenrollado de bucles Los bucles son una de las construcciones de programación más comunes, pero sigue siendo difícil razonar sobre ellos en la verificación formal. Mientras que un bucle en Solidity...

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...