Grant Final Report 0135
App Title
Logic Qualified Data Types for Sophia
App description and link to the grant application
Sophia is a novel language in the world of smart contract languages. It offers static and strong type system with powerful inference algorithm, so despite being strict on the rules, the syntax is clearly readable and convenient to use. My purpose is to extend its awesomeness even further by enhancing it with liquid types 4 which will allow more precise control over the processed data and apply assertions not only to the domains of the variables, but also to their values.
The extension will allow the compiler to perform additional reasoning on the data flow by disallowing constructions that would normally result in runtime errors – like negative spends or out-of-bounds list queries.
Requirements
- Implement a base for liquid type inference algorithm for Sophia
- Extend Sophia syntax to interact with liquid types
- Provide some test cases
- Write report about application of liquid types for smart contract development on the aeternity blockchain
- Provide examples of usage
- Propose further development and describe limitations
Summary of the Development with time report
The whole work took as expected around 530 hours of work including development, thesis writeup and research around the related theory.
A working proof of concept is provided. The implementation is capable of performing verification of smart contracts as shown in the chapter “Outcome” of the document. Please refer to the related pull request to the aesophia repo for the details on the implementation.
Challenges
Adapt the existing state of the art solutions for liquid types to the Sophia language
Solution: handling mutable state of the blockchain is done via the purification algorithm which strips most of the blockchain abstractions from the code. The rest follows the algortihm of the Patrick Rondon which was introduced in his PhD dissertation. Pattern matching approach has been additionally done by me and on top of path sensitivity offers dead code elimination and pattern exhaustion prevention.
Find a way to write liquid type inference for Sophia in a performant way
Solution: There are several solutions proposed in the “Discussion” chapter. For example, incremental solving and context sensitive can drastically improve the performance of the iterative weakening.
Analyze application and value of liquid types in verification of smart contracts
Solution: Please refer to the “Outcome” sections for examples analysis of the value. In short, liquid types can prevent a great range of stupid bugs in smart contracts if utilised properly.
Make the system as user friendly as possible by providing a comfortable syntax and meaningful error messages
Solution: Syntax is as natural as it could have been and follows the conventions. There is a tiny quirk in qualifications of lists’ lengths, but it does not limit any functionality (just looks a little bit odd). Error messages explain the situation clearly by providing assumptions and expected results.
Mutually dependent product types and higher-arity functions
Workaround: Normal products don’t support mutual dependencies, but the document describes how to fix it. Linear dependencies of functions’ domains can be solved by applying a so-called currying technique for higher-arity functions (what Sophia supports).
Documentation
I think the thesis’ write up serves as a decent documentation:
thesis.pdf (977.0 KB)
The link to the most recent version: GitHub - radrow/masters-thesis: Liquid types for verification of smart contracts --- my master's thesis in computer science
Contact details
Please be welcome to reach out to me via aeternity forum, github, email or wire chat 