Certora Prover Documentation
latest

Contents

  • Certora Technology White Paper
  • Certora User’s Guide
  • The Certora Verification Language
  • The Certora Prover
  • Gambit: Mutation Generator for Solidity
  • Old Documentation
    • Specification By Example
    • The Anatomy of a Specification
      • Overview
      • CVL Functions
      • Ghosts
      • Ghost Functions
      • Hooks
      • Definitions
      • Multicontract Hooks
      • A Complete Example
      • Syntax Update: Ghost Variables and Ghost Mappings
    • Advanced Subjects
    • Best Practices
    • Common Pitfalls
    • Assert splitting
    • Troubleshooting
Certora Prover Documentation
  • »
  • Old Documentation »
  • The Anatomy of a Specification
  • Edit on GitHub

The Anatomy of a Specification

  • Overview
  • CVL Functions
    • Syntax
    • Using a CVL Function
  • Ghosts
    • What are ghosts?
    • A Simple Bank Example
  • Ghost Functions
    • Uninterpreted Sorts
    • Uninterpreted Functions
    • Axioms for Uninterpreted Functions‌
    • Initial Axioms for Uninterpreted Functions
  • Hooks
    • Motivation
      • Program State
    • The Anatomy of a Hook
    • Hook Patterns
      • Sload and Sstore
      • Slot Patterns
    • Struct Patterns
      • Structs in Static Slots
      • Structs inside Mappings or Arrays
      • Manually Unpacking Structs
    • Putting it Together
    • The Body of a Hook
    • Two State Context
      • Havoc Assuming
    • A Hook that Modifies Ghost State
  • Definitions
    • Syntax
      • Basic Definitions
      • Advanced Definitions
        • Include an Application of Another Definition.
        • Reference Ghost Functions
  • Multicontract Hooks
  • A Complete Example
    • A Contract Implementing a Linked List
    • A Spec Using a Ghost to Compute Reachability
  • Syntax Update: Ghost Variables and Ghost Mappings
    • Variable-style declarations
    • Variable-style access
    • Mapping-style updates
Previous Next

© Copyright 2022, Certora, Inc. Revision 1076df8a.

Built with Sphinx using a theme provided by Read the Docs.
Read the Docs v: latest
Versions
latest
Downloads
On Read the Docs
Project Home
Builds