Liquid types proof of concept #825

2021-08-02T19:55:34+09:00

zxq9 commented

2021-08-02 19:55:34 +09:00

(Migrated from gitlab.com)

Created by: radrow

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

Relevant paper: http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf
Forum thread: https://forum.aeternity.com/t/active-logic-qualified-data-types-for-sophia-master-thesis/

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.

*Created by: radrow* # 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 * Relevant paper: http://goto.ucsd.edu/~rjhala/liquid/liquid_types.pdf * Forum thread: https://forum.aeternity.com/t/active-logic-qualified-data-types-for-sophia-master-thesis/ 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: ```ocaml 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.

Pull request closed

This pull request cannot be reopened because the branch was deleted.

Sign in to join this conversation.

1 Participants

Notifications

Due Date

No due date set.

Dependencies

No dependencies set.

Reference: QPQ-AG/sophia#825