Prover Approximations

In order to check programs in an acceptable amount of time, the Prover simplifies the code being verified. This section describes the mechanisms for simplification.

Warning

The approximations described in this section may be underapproximations, meaning that they can cause real bugs to be overlooked by the Prover.

• Loop Unrolling
• Method Summarization
  • Overview
  • How Summarization Helps Solvers
  • Syntax
  • Example: Summarization for a complex function
  • Important Considerations
  • Summary
• Harnessing
  • Example:
    • unit test internal functions
    • define complex functionally (view/pure)
• Modeling of Hashing in the Certora Prover
  • Introduction
  • Modeling the Keccak function (bounded case)
    • Examples (Imprecision of Modeling)
    • Modeling does not account for individual values of the Keccak function
    • Modeling does not account for ordering
    • Constants in code vs hashes
  • Hashing of unbounded data
    • Examples for Unbounded Hashing
  • Background: The Solidity Storage Model
  • Conclusion
• Quantifier Grounding
  • How grounding works
  • Limitations on grounding
    • Alternating Quantifiers
    • Recursion
    • Variables must be arguments
    • Double Polarity