[Active] Logic Qualified Data Types for Sophia – master thesis

As some of you may already know, I am working on my master thesis right now. I have decided to combine my education with my work and passion to compiler construction — therefore my research is focused here at aeternity, on our brilliant Sophia language. My plan is to enrich its amazing type system with an advanced feature of simplified version of dependent types called LiQuiD types.

Application Status

Status: Approved on the 21.04.2021
Last updated: 15.04.2021
Submitted by Radosław Rowicki, [email protected] on the 13.04.2021
Team: @radrow
Approved Budget (in h): –
Used Budget (in h): –
Planned Delivery: 1st of September

Specify the funding category

Research, Education, Open Source

Application Title

Logic Qualified Data Types for Sophia

Applicant

Radosław Rowicki – core developer with 2 year experience at aeternity. Focused on Sophia and FATE.

Value 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 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.

The project is going to be the base of my master thesis in computer science at the University of Warsaw. The currently declared title is Formal Verification of Smart Contracts, but I will probably specialize it to something more concrete.

Example of usage:

contract C =
  entrypoint withdraw(x : int) =
    Chain.spend(Call.caller, x)

should result in error:

Refined type error at line 3, column 5:
  Could not solve promise `0 =< x` in context:
    x : int

Refined type error at line 3, column 5:
  Could not solve promise `x =< Contract.balance` in context:
    x : int

This, however, will pass:

contract C =
  entrypoint withdraw(x : int) =
    require(x > 0, "non-positive amount!")
    if(x > Contract.balance) Chain.spend(Contract.balance)
    else Chain.spend(x)

The trick is that Chain.spend will have type {value : int | 0 =< value && value =< Contract.balance} instead of just boring int. This will limit the space spanned by int datatype only to these integers that fit in the valid range. The system will automatically infer and solve the constraints to be met in a path-sensitive way – meaning that it will take into account if expressions and require statements.

Definition of Terms

  • liquid type – logically qualified data type. A type that carries additional logical assertions on the contained values.

Status Quo

The work on this has been started. Explaining the details is fairly technical, but I am close to having some minimal viable product that will handle some simple Sophia expressions. The progress can be tracked on my fork of the Sophia compiler.

Required Work

  • Implement new types and syntax in the Sophia language
  • Implement path sensitive constraint generation
  • Implement constraint solver
  • Integrate nicely with the compiler (readable error messages included)
  • Extend the checker to handle more complex Sophia features

Estimate

This project can be made as complex as one wishes, but I need to stick to my university deadline which should be somewhere around end of August, which gives approximately 4 months.

Known Limitations

  • Sophia supports some non-standard constructions known from basic ML lanugages, like records, contracts, named arguments, etc. While this is not something that makes the task much harder, it still needs to be addressed properly which makes it longer to finish.
  • The proposed system may be sometimes hard to convince that the code is correct (i.e. the solver complains on some things that seem “obvious”). Also, the readability of error messages may be something non-trivial.

Outlook

What happens after this project is completed?

  1. aeternity will have even cooler contract language
  2. Less bugs in smart contracts, more reliable standard library
  3. PR value – afaik this will be the first scientific paper that refers aeternity as a subject of research.

Do you plan to populate your project?

Definitely. There is nothing more satisfying than seeing people making cool use of your creations.

Publishment

Technically, since it is a master thesis, the University of Warsaw will have the rights to its text. Although I am sure it won’t be a problem to publish it anyway. In case it is not true, I am happy to write separate articles about the results and show the use cases.

Maintainance

I declare to provide maintenance of the project on request for at least one year after delivery.

10 Likes

how do u defend your thesis? by proving your added feature is working?

3 Likes

It is done as a presentation in front of the commission. I will talk about my research, techniques and results - including showoff of the program. After that I will need to answer some questions related (directly or not) to my subject. All of these things count to my final grade.

7 Likes

Dear @radrow,
Your Application has been approved by the ACF Board. Thank you very much for improving Sophia!

3 Likes

congrats! Incase you have problem similar as mine : https://www.youtube.com/watch?v=arj7oStGLkU

2 Likes