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
• Storage 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