Grant report Logic Qualified Data Types for Sophia

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

  1. Implement a base for liquid type inference algorithm for Sophia
  2. Extend Sophia syntax to interact with liquid types
  3. Provide some test cases
  4. Write report about application of liquid types for smart contract development on the aeternity blockchain
  5. Provide examples of usage
  6. 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: https://github.com/radrow/masters-thesis

Contact details

Please be welcome to reach out to me via aeternity forum, github, email or wire chat :slight_smile:

5 Likes