First, we will write "basic" properties for each of the following entrypoint functions, where basic properties specify the storage update and the sequence of operations to follow. These basic properties will be written based on our understanding of the LIGO code, but they will be verified against the Michelson code using our K Michelson semantics. Thus, verifying these basic properties will essentially prove the correctness of the LIGO-to-Michelson compilation.
add_liquidity()
remove_liquidity()
xtz_to_token()
token_to_xtz()
token_to_token()
(and more ...)
Then, we will write contract invariant properties that are needed to prove certain desired properties over arbitrary sequences of entrypoint functions, including inter-contract function calls. Examples of such desired properties include (but not limited to):
It is not possible to produce a profit by merely executing add_liquidity() immediately followed by remove_liquidity() (e.g., by exploiting rounding errors).
Similarly, it is not possible to make a profit by executing xtz_to_token() immediately followed by token_to_xtz() or vice versa.
The effect of token_to_token() is equivalent to executing token_to_xtz() followed by xtz_to_token().
(and more ...)
In the first week, we will review the code to identify such properties (for both basic properties and contract invariant properties), and will communicate the Dexter team to make sure that the properties capture their intention of the code. Then, we will verify that the properties are satisfied by the Michelson code, so that we do not need to trust the LIGO-to-Michelson compiler for the validity of our verification result. We will immediately report any concerns or issues, if any, that are found during the verification process. More properties could be additionally identified as we make a progress. We will identify and verify as many properties as time allows.
First, we will write "basic" properties for each of the following entrypoint functions, where basic properties specify the storage update and the sequence of operations to follow. These basic properties will be written based on our understanding of the LIGO code, but they will be verified against the Michelson code using our K Michelson semantics. Thus, verifying these basic properties will essentially prove the correctness of the LIGO-to-Michelson compilation.
Then, we will write contract invariant properties that are needed to prove certain desired properties over arbitrary sequences of entrypoint functions, including inter-contract function calls. Examples of such desired properties include (but not limited to):
In the first week, we will review the code to identify such properties (for both basic properties and contract invariant properties), and will communicate the Dexter team to make sure that the properties capture their intention of the code. Then, we will verify that the properties are satisfied by the Michelson code, so that we do not need to trust the LIGO-to-Michelson compiler for the validity of our verification result. We will immediately report any concerns or issues, if any, that are found during the verification process. More properties could be additionally identified as we make a progress. We will identify and verify as many properties as time allows.