This PR provides a proof of concept implementation of refinement types in Sophia. While this work is not production-ready, it can serve as an advanced starting point and inspiration for how such types could be added to the existing Sophia type system. The project has been written as a part of my research for my master's thesis at the University of Warsaw. The document is still work in progress and will be shared after it is defended.
For a reference what are liquid types and what is their value please refer to the
The work on this contribution and research is a subject of the 0135 ACF grant "Logic Qualified Data Types for Sophia".
Requirements
Erlang (of course) and a SMT solver that speaks SMT-lib language. I was using Z3 by Microsoft Research and I highly recommend it.
What is there
The project covers most of the Sophia expressions including but not limited to
arithmetics
lists
custom datatypes
functions (higher-order included)
tuples
addresses
pattern matching
Moreover, the following are featured
some functions in List.aes stdlib
dead code prevention
unsafe control flow prevention (like switch exhaustion)
recursion
polymorphism
Furthermore, it is able to infer judgements about the state and track it along imperative control flows. The contract's balance is being tracked as well and it is being entirely statically verified that there are no negative spends and every spend can be afforded at time. This however does not apply to balances of other contracts, but once maps are added it can be easily supported with some simple preprocessing (i.e. adding balance map to the contract state).
There is some simple testing suite with examples of contracts utilizing the liquid types. The introduced syntax allows users to define custom liquid types and put manual assertions on the data.
What is to be done
In order to make this project eligible to face users, the following should be addressed:
[ ] Full syntax, data and types coverage. At this point there is lack of support for some record projection constructions, maps, byte arrays, bit fields, some operators and builtin functions, list comprehensions and stdlib.
[ ] State management needs some tricky fixups when someone abuses lambdas (I had a lot of pain working with this, 80% of which was caused by a hole in Sophia #217 )
[ ] Interactions with other contracts are not supported at all
[ ] All of the "future work" sections in the thesis (will be published in about a month)
[ ] Mutually recursive dependencies in tuples and higher-arity functions
[ ] General performance is not satisfying
Also, I was too lazy to write SMT library as a proper gen_statem and I run it as a bare recurring process. It works fine tho, it's just ugly.
Cool stuff
Just to give some view why it is cool and choco. Let us consider the following spend-split contract which distributes spends among addresses equally:
include "List.aes"
contract SpendSplit =
payable stateful entrypoint split(targets : list(address)) =
let value_per_person = Call.value / List.length(targets)
spend_to_all(value_per_person, targets)
stateful function
spend_to_all : (int, list(address)) => unit
spend_to_all(_, []) = ()
spend_to_all(value, addr::rest) =
Chain.spend(addr, value)
spend_to_all(value, rest)
Looks fine, yeah? No. Try it in the refiner and you will see that
Could not prove the promise at spend_split.aes 13:7:
value =< $init_balance && value >= 0
from the assumption
true
Could not prove the promise at spend_split.aes 13:7
arising from an application of "C.spend_to_all" to its 2nd argument:
$balance_38 >= 0
from the assumption
true
Could not prove the promise at spend_split 6:39
arising from an application of "(/)" to its right argument:
n_105 != 0
from the assumption
true
(messages are slightly redacted for readability). Indeed, there are two latent issues:
division by zero is list is empty
no check if contract can afford the spend (note this is important since the spend_to_all function could be potentially called under different conditions. Atm the use-case of functions are not considered, but technically could be, though).
The contract needs a fixup then:
contract SpendSplit =
payable stateful entrypoint split(targets : list(address)) =
require(targets != [], "NO_TARGETS")
let value_per_person = Call.value / List.length(targets)
spend_to_all(value_per_person, targets)
stateful function
spend_to_all : ( {v : int | v >= 0 && v =< Contract.balance / l}
, {l : list(address)}
) => unit
spend_to_all(_, []) = ()
spend_to_all(value, addr::rest) =
Chain.spend(addr, value)
spend_to_all(value, rest)
(This example uses some work in progress features and might not run at the current state of refinement. There are workarounds for that though).
This and other examples will be discussed in more details in my thesis.
Liquid types
This PR provides a proof of concept implementation of refinement types in Sophia. While this work is not production-ready, it can serve as an advanced starting point and inspiration for how such types could be added to the existing Sophia type system. The project has been written as a part of my research for my master's thesis at the University of Warsaw. The document is still work in progress and will be shared after it is defended.
For a reference what are liquid types and what is their value please refer to the
The work on this contribution and research is a subject of the 0135 ACF grant "Logic Qualified Data Types for Sophia".
Requirements
Erlang (of course) and a SMT solver that speaks SMT-lib language. I was using Z3 by Microsoft Research and I highly recommend it.
What is there
The project covers most of the Sophia expressions including but not limited to
Moreover, the following are featured
List.aesstdlibswitchexhaustion)Furthermore, it is able to infer judgements about the
stateand track it along imperative control flows. The contract's balance is being tracked as well and it is being entirely statically verified that there are no negative spends and every spend can be afforded at time. This however does not apply to balances of other contracts, but once maps are added it can be easily supported with some simple preprocessing (i.e. adding balance map to the contract state).There is some simple testing suite with examples of contracts utilizing the liquid types. The introduced syntax allows users to define custom liquid types and put manual assertions on the data.
What is to be done
In order to make this project eligible to face users, the following should be addressed:
Also, I was too lazy to write SMT library as a proper
gen_statemand I run it as a bare recurring process. It works fine tho, it's just ugly.Cool stuff
Just to give some view why it is cool and choco. Let us consider the following spend-split contract which distributes spends among addresses equally:
Looks fine, yeah? No. Try it in the refiner and you will see that
(messages are slightly redacted for readability). Indeed, there are two latent issues:
spend_to_allfunction could be potentially called under different conditions. Atm the use-case of functions are not considered, but technically could be, though).The contract needs a fixup then:
(This example uses some work in progress features and might not run at the current state of refinement. There are workarounds for that though).
This and other examples will be discussed in more details in my thesis.