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
• Harnessing
  • Harnessing by extension
  • Harnessing by munging
• Modeling of Hashing in the 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
  • Hashing of Unbounded Data
    • Examples for Unbounded Hashing
  • Background: The Solidity Storage Model
  • Conclusion