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: Completed on the 14.10.2021, 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: 30th 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?
- aeternity will have even cooler contract language
- Less bugs in smart contracts, more reliable standard library
- 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.