What does dispatcher(true) mean?

deposit(uint256) returns(uint256)  => DISPATCHER(true)

what does dispatcher(true) mean here?
Tutorials → lesson 09 → SymbolicPoolDemo → highLevel.spec


1 Like

@datapunk what you see here is a function summarization.
there are several predefined summarization commands that allow to the user to instruct the prover how a call to a function from within the contract will behave.
For example in the line you wrote, the user specified that when deposit is being called, instead of executing the lines of the code, you do whatever dispatcher tells you to do.

dispatcher is a summarization that has to do with multi occurrence of the same function signature. When multi contracts are being used, meaning that multiple contracts are being specified in the verification context, a dispatcher(true) tells to the prover - “when deposit() is being called, go and look for all functions with this signature and invoke them as well, i.e. check them”.

you can read more on summarization in this page of the documentation:

The is also the very powerful option of summarizing contract methods with ghosts, and CVL functions. The idea is the same. You implement a ghost/function, meaning the way things should work when you call the specific method, and summarize the function as to say “when calling method X from the contract, do Y instead”.

summarizations are necessary in almost all projects, and are very powerful. They usually used to model methods that the prover is having hard time with to reduce runtime, etc.
With that said, it’s also something that needs to be handled carefully to avoid assumptions that doesn’t have any ground. We always have to be sure that our summarization does not make us under-approximate the state.