[Certora] Specify that augustus call can't approve

[QGarchery]

So we could keep this as an issue for later, where we would want to specify that the augustus registry prevents from calling token with those functions. In the meantime, another option is to remove ParaswapAdapter from the parametric contracts

Originally posted by @QGarchery in #238 (comment)

[QGarchery]

There may be a trick to do this, where it doesn't require to summarize the augustus call (which is difficult to do, how would you hook on a very general call like that ?). It would instead summarize the call to isValidAugustus(augustus) to specify that augustus is not a token. A dirty way to do this is to summarize this call to dispatch augustus to a general contract, that can delegatecall anything, except that the implied selector shouldn't be approve
I wonder if there is a better way to do this

[gd-colin]

Unfortunately, the trick you suggested doesn't seem to work. Look at this run.

[QGarchery]

It seems to be related to a different "bug", in the sense that the callee of the augustus.call(...) is unresolved. Which is weird because it correctly does augustus == MockAugustus

[gd-colin]

Certora is investigating a bug but Quentin's idea should work once the bug is fixed.