Warning

This page was created from a pull request (#74).

The Certora Verification Language

The Certora Verification Language (often abbreviated CVL) is the language used to write specifications for smart contracts. This chapter describes the syntax and semantics of CVL Specifications.

• Specification Files
• Syntactic conventions

Common Syntactic Elements

• Basic Syntax
  • Comments
  • Identifiers
  • Literals
• Types
  • Syntax
  • Solidity Types
    • Array access
    • User-defined types
  • Additional CVL types
    • The mathint type
    • The env type
    • The method and calldataarg types
    • The storage type
    • Uninterpreted sorts
  • Conversions between CVL and Solidity types
• Mathematical Operations
  • Mathematical operations
  • Maximum values
  • Implicit casting
  • Explicit casting
• Expressions
  • Syntax
  • Basic operations
  • String interpolation
  • Extended logical operations
  • Accessing fields and arrays
  • Contracts, method signatures and their properties
  • Special variables and fields
  • Calling contract functions
    • Type restrictions
  • Comparing storage
• Statements
  • Syntax
  • Variable declarations
  • assert and require
  • satisfy statements
  • requireInvariant statements
  • Solidity-like statements
  • Function calls
  • havoc statements

Specification File Contents

• Pragmas
  • Syntax
• Import and Use Statements
  • Syntax
• Using statements
  • Syntax
• The Methods Block
  • Syntax
  • Methods entry patterns
    • Exact entries
    • Wildcard entries
    • Location annotations
    • Visibility modifiers
  • envfree annotations
  • optional annotations
  • Summaries
    • Summary application
    • Summary types
• Events
  • Syntax
• Rules
  • Syntax
  • Overview
  • Parametric rules
  • Filters
  • Multiple assertions
  • Rule descriptions
  • How rules are verified
• Built-in Rules
  • Syntax
  • Bad loop detection — msgValueInLoopRule
  • Delegate call detection — hasDelegateCalls
  • Basic setup checks — sanity
    • How sanity is checked
  • Thorough complexity checks — deepSanity
    • How deepSanity is checked
• Functions
  • Syntax
• Invariants
  • Syntax
  • Overview
  • Assumptions made while checking invariants
  • Preserved blocks
  • Filters
  • Writing an invariant as a rule
  • Invariants and induction
• Uninterpreted Sorts
  • Syntax
• Ghosts
  • Syntax
  • Declaring ghost variables
  • Using ghost variables
  • Initial state axioms
  • Ghost functions
• Definitions
  • Syntax
• Hooks
  • Syntax
• EVM (Ethereum Virtual Machine) Opcode Hooks
  • Background
  • Hooking on opcodes
  • Missing instructions
  • Known inter-dependencies and common pitfalls

CVL Version 2

• Changes introduced in CVL 2
  • Superficial syntax changes
    • function and ; required for methods block entries
    • Required ; in more places
    • Method literals require sig:
    • Use of contract name instead of using variable
    • Rules must start with rule
  • Changes to methods block entries
    • Most Solidity types allowed as arguments
    • Required internal or external annotation
    • optional methods block entries
    • Required calldata, memory, or storage annotations for reference types
    • Summaries only apply to one contract by default
    • Requirements on returns
  • Changes to integer types
    • Mathematical operations return mathint
    • Comparisons require identical types
    • Implicit and explicit casting
    • Casting enums to integer types
    • Modulo operator % returns negative values for negative inputs
    • Support for bytes1…bytes32
    • Changes for bitwise operations
  • Changes to the fallback function
  • Removed features
    • Methods entries for sighashes
    • invoke, sinvoke, and call
    • static_assert and static_require
    • invoke_fallback and certorafallback()
    • invoke_whole
    • Havocing local variables
    • Destructuring syntax for struct returns
    • bytes[] and string[]
    • pragma
    • events
  • Changes to the Command Line Interface (CLI)
    • Flags Renaming
    • Prover Args
    • Solidity Compiler Args
    • Enhanced server support
• Migration guide
  • Step 0: Install CVL 2
  • Step 1: Skim CVL 2 changes
  • Step 2: Run the migration script
  • Step 3: Fix type errors
    • Syntax errors introduced by the migration script
    • Type errors in arithmetic and casts
    • using statements
    • Problems with certorafallback or invoke_fallback
  • Step 4: Review your methods blocks
    • internal and external methods
    • Receiver contracts
  • Step 5: Profit!