Hi, I encountered a warning when trying to run my spec against Spartan Protocol.
Syntax warning in spec file: using a function pointer for a function with overloadings (SpartaProtocolPool.constructor(), SpartaProtocolPool.constructor(address,address)), returning the first overloading
Is it something to do with the settings? Is it an undesired behavior (which it looks like to me)?
Refs
I also gathered some possibly related issues in the reply below.
I got
UNRESOLVED Auto summary
havoc type: only the return value
use decision: default
in the summary of a call for an invariant in a job. It shows up in all clickable function result though.
I’m not sure about the cause either. This did show up in some of my failure cases before. Is it possibly related to the overloading issue?
Ref
Last, I got “Unwinding condition in a loop” in the report of a job simulating a call name() and symbol().
This is quite confusing to me because there is no loop in Spartan.sol nor ERC20.sol.
NOTE: adding the flag --optimistic_loop can make it disappear.
Ref:
I’ll start from the bottom up:
Re the unwinding condition in a loop - name() and symbol() are getters of string types. strings are being handled internally with loops (because they are of dynamic size) which make necessitate careful handling.
Since here the name and the symbol aren’t interesting for any rules, you can either filter them out with the filtered feature, or you can use the optimistic_loop to make them pass.
Re the call resolution warnings - warnings are not errors. This table is giving the user information on how the prover handled some vertex points in the formal verification. Take for example the first row of the table:
SpartanProtocol invoked add_liquidity function which, in turn, called balanceOf of a specific ERC20 token. Since the the function balanceOf does not exist in SpartanProtocol, and you never linked the ERC20.sol as part of your verification context, then the prover doesn’t know what this function does. The prover then tell you that it decided to resolve this by using the default behavior which is havocing. Havocing basically means that no prior info (assignments, restrictions, etc.) is being kept on the variable, so that now the variable can take any value within its type restriction. The prover is telling you that because you may have expected it to return a deterministic value based on an actual invocation of balanceOf.
Havocing was chosen as the default behavior since it will never under-approximate. It allows the variable to take any value which at the very least be an accurate description of reality, or in most cases a massive over-approximation.
Re the function pointer error - im not sure what triggered it, i will need some more info to understand. To get a more elaborative error message. On your list of jobs go to the run that failed and click on the clipboard on the right (right next to the abort job button). Send this link so we can go through the text.
In general note that your report links are lacking anonymous key, so nobody can open them besides you (or anyone else who has your key).
Thanks a lot for the detailed and clear answers!
- Re the unwinding condition in a loop -
name()andsymbol()are getters of string types. strings are being handled internally with loops (because they are of dynamic size) which make necessitate careful handling.
Since here the name and the symbol aren’t interesting for any rules, you can either filter them out with the filtered feature, or you can use the optimistic_loop to make them pass.
By the filtered feature, do you mean filtered {}? Example. Is there more information about the keyword? I tried to search for its usage in the documents but I didn’t find it.
SpartanProtocol invoked
add_liquidityfunction which, in turn, calledbalanceOfof a specific ERC20 token. Since the the functionbalanceOfdoes not exist in SpartanProtocol, and you never linked theERC20.solas part of your verification context, then the prover doesn’t know what this function does.
By linking ERC20.sol, could you direct me how to do it? I tried the following command but it seems not helpful.
certoraRun SpartaProtocolPool.sol ERC20.sol --verify SpartaProtocolPool:Spartan.spec
I saw the option --link but I’m not sure if it can be used here.
- Re the function pointer error - im not sure what triggered it, i will need some more info to understand. To get a more elaborative error message. On your list of jobs go to the run that failed and click on the clipboard on the right (right next to the abort job button). Send this link so we can go through the text.
An example is this dump. The first two lines:
Syntax warning in spec file: using a function pointer for a function with overloadings (SpartaProtocolPool.constructor(), SpartaProtocolPool.constructor(address,address)), returning the first overloading
Syntax warning in spec file: using a function pointer for a function with overloadings (SpartaProtocolPool.constructor(), SpartaProtocolPool.constructor(address,address)), returning the first overloading
Much appreciated. 
By the filtered feature, do you mean
filtered {}? Example. Is there more information about the keyword? I tried to search for its usage in the documents but I didn’t find it.
Yes this is exactly what im talking about. unfortunately we don’t have documentation on that at the moment. we are working on moving our docs to readthedocs, improve it and add many examples. You can find it here
The filtered is pretty straight forward. It will filter out/in function you specify on the specific rule. for example if i write f.selector != isView, then view function will not be processed when running a rule. this is useful mainly to reduce run-time complexity - for example if we want to check that a function doesn’t change a var state, we can filter out view function since they cannot change state. You’ll have to use examples to learn the syntax at the moment. if you need more examples/help ask for it and we’ll find and explain the syntax more thoroughly.
By linking
ERC20.sol, could you direct me how to do it? I tried the following command but it seems not helpful.
multi-contract is an important functionality as many contracts communicate with other contracts. You will find some explanations here and here. In some cases you may also need to use linking which (unsurprisingly) links an instance of another contract that appear in the contract you are verifying. You can read about it in the docs here, but here’s an example anyway:
contract Aux{
unit a;
uint b
uint c;
function foo(uint g) public returns (bool){
...
}
}
contract Use_Aux{
Aux q;
uint r;
bool s;
function bar(){
s = q.foo(r)
...
}
}
In the example above, if you try to verify contract Use_Aux, then q, the instance of Aux is unknown to the prover. you will have to link it, meaning you will have to tell the prover the instance q is of type Aux, you can find it in Aux.sol.
An example is this dump. The first two lines:
Syntax warning in spec file: using a function pointer for a function with overloadings (SpartaProtocolPool.constructor(), SpartaProtocolPool.constructor(address,address)), returning the first overloading
Syntax warning in spec file: using a function pointer for a function with overloadings (SpartaProtocolPool.constructor(), SpartaProtocolPool.constructor(address,address)), returning the first overloading
There’s a difference between a warning and an error.
A syntax warning basically notify you that things are not fully defined and so the prover, behind the scenes, complete what ever it needed to run.
While a syntax error will hard stop the run due to ambiguity and unclear intentions.
In the case that you point out, it seems like the a constructor is defined as taking 2 args, but the spec seems to know only a constructor that takes no args. Im not sure why that is happening, it can occur due to wrong craft of harness file that inherits from the parent contract, or maybe wrong declaration of methods (though constructors are no usually declared).
In any case that warning tells you that something automatic happened, which may or may not be what you intended so you need to pay attention to it.