search

Zilliqa / scilla

Scilla - A Smart Contract Intermediate Level Language
https://scilla-lang.org
GNU General Public License v3.0
241 stars 78 forks source link

Constraint-based cash flow tracking #18

Open ilyasergey opened 6 years ago

ilyasergey commented 6 years ago
ilyasergey commented 5 years ago

The aim of this task is to leverage the cash-flow information to automatically check (on demand) most common invariants of contracts, such as “an amount of distributed money is always equal to the balance”. The balance is always positive etc.

The verifier will use the tags derived by CF and will compile the sequence of commands into constraint systems, relating the initial and the final state of a contract before/after the transitions, conjoined with the desired invariant. An off-the-shelf SMT solver will be used to determining whether the invariant still holds at the end. The analysis can take a number of default invariants, and also accept the custom invariants specified by the user in a decidable fragment of a logic.