aeternity / aesophia Goto Github PK

Stand alone compiler for the Sophia smart contract language

Home Page: https://docs.aeternity.com/aesophia

License: ISC License

Erlang 99.11% Reason 0.83% Python 0.02% HTML 0.03%

aesophia's Introduction

aesophia

This is the sophia compiler for the æternity system which compiles contracts written in sophia to FATE instructions.

The compiler is currently being used three places

Documentation

Additionally you can check out the contracts section of the æternity blockchain specification.

Versioning

Versioning should follow the semantic versioning guidelines. Id est, given a version number MAJOR.MINOR.PATCH, increment the:

MAJOR version when you make incompatible API changes
MINOR version when you add functionality in a backwards compatible manner
PATCH version when you make backwards compatible bug fixes

Interface Modules

The basic modules for interfacing the compiler:

aesophia's People

Contributors

Stargazers

Watchers

Forkers

radrow danielaivanova opt9 aekiti mrfrey14 jdgcs kchenpengfei aherranz kryptokrauts evmbro nikita-fuchs ioolkos callbay davidalphafox marc0olo devindirt fabiankrol vitaljeevanjot davidyuk

aesophia's Issues

Undecidable type inference crashes compilation

Compiling following code

contract Bum =
  stateful entrypoint bum() =
    Oracle.register(Contract.address, 12345, RelativeTTL(1000))
    ()

leads to internal compiler error ({badmatch,undefined}), however

contract Bum =
  stateful entrypoint bum() =
    Oracle.register(Contract.address, 12345, RelativeTTL(1000)) : oracle(int, int)
    ()

works flawlessly.

The type infer cannot deduce return type of Oracle.register... because it is polymorphic and does not depend on the context. This causes oracle type to be specified by an unbound typevar which makes compiler mad. Inferred return type of Oracle.register is exactly

{app_t,
         [{origin,system}],
         {id,[{origin,system}],"oracle"},
         [{tvar,[{file,"xd"},{line,3},{col,5}],"'a"},
          {tvar,[{file,"xd"},{line,3},{col,5}],"'b"}]}}

We should detect such situations and raise type errors.

Bug copyright (c) @hanssv

Function blocks accept clauses with different names

I don't think it should be legal. Also, makes my REPL unhappy.

contract C =
  entrypoint
    f() = 123
    g() = 123

Recursive datatypes

Pattern matching in function heads

From the Sophia discussion at the Sofia workshop.

Typechecker does not warn about enforced monomorphism of local definitions

Following code does not typecheck:

  entrypoint tttt() =
    let f(x : 'a) : 'a = x
    if(f(true)) f(1) else f(2)

because local functions are not allowed to be polymorphic and 'a get implicitly assigned to bool which causes f(1) to be badly typed. This behavior is very misleading, because the actual type of f (bool => bool) does not match explicitly given type signature.
We should detect such situations and rise meaningful errors.

Add comparable typevar constraints

Currently all types can be combined with == and =<-like relation operators. While this works cool on ints, strings and possibly some other types, it seems to be completely useless for custom ADTs and functions. In my opinion the expression ((x, y) => x) == ((x, y) => y) shouldn't typecheck, as it may lead to hard to find bugs.
Another example: FixedTTL(x) > FixedTTL(y) works as expected comparing x > y, but if we accidentally compare FixedTTL and RelativeTTL the first one will be always greater, no matter of the arguments.

To solve this issue I propose adding qualification to typevars (similar to typeclasses, but restricted only to Ord and Eq):

// Most general type is spelled 'a. It cannot be compared and unified with generalized non-comparable typevar.
function id(x : 'a) : 'a = x

// Types that can be compared using `==` operator would have double tick before the tvar name
function neq(x : ''a, y : ''a) : bool = !(x == y)

// Types forming a linear order would require triple tick (or something else, this is starting to look ugly)
function lt(x : '''a, y : '''a) : bool = x < y
// ''a unifies with '''a
function spec_eq(x : '''a, y : '''a) : bool = x == y

The new syntax opens another way of dealing with it:

function 
  lt : 'a is ord, ('a, 'a) => bool
  lt(x, y) = x < y

I think this is the place where we could accept operator overloading. Although in situations where == can be derived automatically it is usually the best and the only solution, the < like operators can be more tricky so we could let the users define the comparison by themselves. Of course not stateful nor payable.

Lambda types forget stateful constraint

Consider the following contract:

contract Bum =
  type state = (int * (int => unit))
  entrypoint init() = (0, (x) => ())

  stateful entrypoint setX(x : int) = switch(state)
    (_, f) => put((x, f))

  entrypoint getX() = switch(state)
    (x, _) => x

  stateful entrypoint hack() = switch(state)
    (s, f) => put((s, (x) => setX(x)))

  entrypoint bum(x : int) = switch(state)
    (_, f) => f(x)

If the user calls hack they can start to freely modify the state from non-stateful entrypoint bum:

AESO> :dep bum.aes as bum
bum : Bum was successfully deployed
AESO> bum.getX()
0
AESO> bum.hack()
()
AESO> bum.bum(2137)
()
AESO> bum.getX()   
2137

^{^{This bug is sponsored by Sophia REPL}}

Contract inheritance

From the Sophia discussion at the Sofia workshop.

Function modifiers

From the Sophia discussion at the Sofia workshop.

Solidity lets you create modifiers that can wrap function bodies in arbitrary code.

"using namespace"

When you are heavily using some namespace it becomes very annoying to mention its name every time. Also, one could make aliases for namespaces:

include "List.aes"
include "Option.aes"
contract Con =
  using List
  using Option as O
  entrypoint f(x) = O.concat_option(sum(x)) // `sum` originally in `List`

The naming collisions would throw type errors and ask for qualification.

Currying support

Sometimes curried functions are more useful than >1 arity ones, because they play very naturally with partial application. Example of syntax/usage:

function map(f : ('a) => 'b)(l : list('a)) : list('b) = switch(l)
  []   => []
  h::t => f(h)::map(f)(t)

function map_deep(f : ('a) => 'b)(l : list(list('a))) : list(list('b)) =
  map(map(f))(l)

CLI: Standard library files not reachable in escript

~/Quviq/Aeternity/aesophia_cli [git:*master]: cat /tmp/foo.aes 
include "List.aes"
contract C =

  entrypoint foo(f : int => bool, l : list(int)) =
    List.map(f, l)
~/Quviq/Aeternity/aesophia_cli [git:*master]: ./aesophia_cli /tmp/foo.aes 
Parse error in '/tmp/foo.aes' at line 1, col 1:
Couldn't find include file 'List.aes'

There are actually two problems

The aesophis/priv/stdlib/* is not included in the escript aesophia_cli
You can't access the files in an escript as if they are in the file system

Encode/decode bits

Currently you cannot encode calldata or decode results containingbits values.

Validating on-chain code

It's important to be able to verify that an on-chain contract is the result of compiling some particular source code with a particular compiler version. Since the init function is not present in the on-chain code this isn't as simple as running the compiler and comparing the byte code.

We should provide some functionality in the compiler to make this easier. Suggestion:

Input byte code and source code and return yes / no-because

Pattern guards

Sometimes it is nice to be able to provide some assertions on patterns, for instance:

function f(l) = switch(l)
  k::_ | k < 0 => k
  _::t         => f(t)
  []           => 0

Expressions in the guard must not be stateful

FATE debugger

From the Sophia discussion at the Sofia workshop.

Map garbarge collection bug

Reference counting for store maps is too conservative for nested map updates in some cases, leading to maps being copied instead of updated inplace. Example:

@compiler >= 4
payable contract MultiMap =

  record state = 
    { my_map          : map(string, map(int, custom)) }

  record custom = 
    { sender        : address
    , received_at   : int }

  entrypoint init () : state = { my_map = {} }
    
  entrypoint my_map() : map(string, map(int, custom)) = state.my_map
  
  entrypoint size(key: string) : int = Map.size(state.my_map[key = {}])

  payable stateful entrypoint set (key: string) : unit =
    put(state{ my_map[key = {}][size(key)] = new_custom() })
    
  stateful function new_custom() : custom =
    { sender        = Call.caller,
      received_at   = Chain.timestamp }

Adding two keys makes the outer map big enough to be given store handling and successive sets to one of the keys then requires linear gas instead of constant, since the inner map is copied instead of updated inplace.

Work-around: avoid nested maps.

Allow shadowing of inherited functions

@hanssv asked here if we want to allow overriding of inherited functions and whether there are some use cases for that. Solidity supports shadowing, which allows to extend logic of super critical functions without touching their code.
To the outside world, especially if the contract follows a standard, the function with the extended logic remains the one to be called, there is no other.

Example (pseudocode)

contract basicToken {


    function transfer(amount, recipient) returns (bool) {
     *critical code here*
    }

}

contract myFancyToken is basicToken{


function transfer (amount, recipient) {
    doSomething();
    bool result = super.transfer(amount, recipient); // executing basicToken's transfer() logic and evaluating output!

    if (!result) damnItFailed();
        else
    doSomethingFancy();
}

only myFancyToken's implementation of transfer() is accessible from the outside and gets called by default from every ERC20-able wallet/software/whatever, and the additional code of the dapp's smart contract utilizing this token gets executed automatically with every transfer.

If you need any "real" examples from production cases, drop a line :)

Bug in named arguments

Typechecking following code throws badarg on ++ operator, because named arg in i(2) turns out to be uvar instead of actual named argument list.

contract Id =
  entrypoint id : ('x) => 'x

contract Bum =
  entrypoint bum() = 
    let i = ct_2gPXZnZdKU716QBUFKaT4VdBZituK93KLvHJB3n4EnbrHHw4Ay : Id
    i.id(2) + i(2)

Create contracts from other contracts

From the Sophia discussion at the Sofia workshop.

Transaction introspection in Auth context

Allow access to the signed transaction within the authentication context:

switch(Auth.tx)
  Spend(from, to, amount, payload) => ...
  AENSTransfer(from, to, name) => ...
  ...

Contract declarations under namespace

The following contract glitches out throwing unknown_error:

namespace N =                                                               
  contract C =                                                              
    entrypoint f : () => int
contract C =
  entrypoint f(c : N.C) = c.f()

Properly deprecate AEVM backend

New features are only added to FATE compiler back-end - this asymmetry makes it hard to maintain the tests etc. From Iris on-wards the chain will only accept new FATE contracts so we should deprecate AEVM.

Data deconstruction in let

From the Sophia discussion at the Sofia workshop.

For instance,

  let x :: xs = ys
  let (x, y) = pt
  let Some(x) = Map.lookup(k, m)

New VM-function to lookup the owner of a name - AENS.get_owner(name : string) : option(address)

This method can also be used to check if name exists or not.

"using namespace" qualification

Depends on #233

Extension of the above. This really helps finding "where the heck is (...) defined". Speaking of the possibility to include only specific parts of the namespace.

contract Con =
  using List hiding [flat_map, map]
  using Option for [flat_map, map2, map]

type declarations are not working

Type declarations are not working. The following contract fails to compile with unknown_error (it's a type_error):

contract N =                                  
  type d                                       
                                               
contract C =                                 
  entrypoint f() = 123

Builtin types for date and time

From the Sophia discussion at the Sofia Workshop.

FundMe Contract - sophia.md

type_error: Unbound variable raw_spend at line 13, column 5
At: Line 13, column 5

The error above was found when deploying the crowd-funding contract

More functions on strings

Some suggestions

  String.split(i : int, s : string) : string * string
  String.to_list(s : string) : list(char)
  String.from_list(cs : list(char)) : string
  String.at(s : string, i : int) : char

cc @thepiwo @radrow

Partial operator application

In Haskell and Scala one can partially apply an operator. It is very useful with higher order functions:

function inc_all(l : list(int)) : list(int) = map((_+1), l)
function negate_all(l : list(int)) : list(int) = map((0-_), l)

Compiler crashes on empty file

As I remember there is an attempt to handle this situation, but it seems to fail

New VM-function to lookup the TTL of a name - AENS.expire_by(name : string) : option(int)

To be able to handle name extensions in a contract it might be interesting to look up the current expiry (block height).

Improve docs on signatures

Some AENS and Oracle functions takes a named argument - the signature. There is a caveat, the signature material has to be prefixed with the network id. This is mentioned in the general node documentation on signatures, but who looks there :-)

Remember both master and lima!

Release 4.1.0

Add operator lambdas

Ability to treat an operator in parentheses like a casual function, just like in Haskell and OCaml;

function sum(l : list(int)) : int = foldl((+), 0, l)
function plus(x, y) = (+)(x, y) // ugly but shows the idea

Reverse application operator |>

This idea was wandering around for several months. Speaking of the |> operator like in Elixir, Elm and F#. This is super cool and useful:

function enterprise_pipeline(int x) : stuff = x
  |> IntegerDivider.divide_int().by(3)
  |> Int.to_str
  |> StringAnalyzer.analyze("casual")
  |> StringAnalyzerResultProcesserFactory.make_factory
  |> StringAnalyzerResultProcesserFactory.produce_stuff

Support for rational numbers

Rational numbers are essential to clearly represent ratios and proportions, which appear commonly in lots of models and computations. Sophia does not support any kind of numbers other than integrals and I think it could be changed.

How does it look now

While developing some kind of basic bonding curve contract I had to specify reserve_ratio. This is the very first place I really faced lack of fractions – I was forced to define max_reserve_ratio, and set reserve ratio as "the value that divided by max_reserve_ratio will produce actual reserve ratio". This leads to quite ridiculous consequences, because then in Bancor formula I need to take something to the power of that ratio, which requires defining more and more operations on these implicit rationals and pushes all this work to the user. Take a look at this solidity code taken from https://github.com/relevant-community/contracts/blob/bondingCurves/contracts/BancorFormula.sol :

    /**
        General Description:
            Determine a value of precision.
            Calculate an integer approximation of (_baseN / _baseD) ^ (_expN / _expD) * 2 ^ precision.
            Return the result along with the precision used.

        Detailed Description:
            Instead of calculating "base ^ exp", we calculate "e ^ (ln(base) * exp)".
            The value of "ln(base)" is represented with an integer slightly smaller than "ln(base) * 2 ^ precision".
            The larger "precision" is, the more accurately this value represents the real value.
            However, the larger "precision" is, the more bits are required in order to store this value.
            And the exponentiation function, which takes "x" and calculates "e ^ x", is limited to a maximum exponent (maximum value of "x").
            This maximum exponent depends on the "precision" used, and it is given by "maxExpArray[precision] >> (MAX_PRECISION - precision)".
            Hence we need to determine the highest precision which can be used for the given input, before calling the exponentiation function.
            This allows us to compute "base ^ exp" with maximum accuracy and without exceeding 256 bits in any of the intermediate computations.
    */
    function power(uint256 _baseN, uint256 _baseD, uint32 _expN, uint32 _expD) internal constant returns (uint256, uint8) {
        uint256 lnBaseTimesExp = ln(_baseN, _baseD) * _expN / _expD;
        uint8 precision = findPositionInMaxExpArray(lnBaseTimesExp);
        return (fixedExp(lnBaseTimesExp >> (MAX_PRECISION - precision), precision), precision);
    }

Note all these workarounds. The programmer needs to pass nominators and denominators separately to define actually very principal operations. This leads to a lot of unneeded bloat of code and creates a lot of opportunities to introduce bugs.

How do I see it

For a start, handling rationals may be done by a library. Rational number is literally a pair of integers. We may call it either Frac, Ratio, Fractional or Rational. It is important to point to the user that they are not system floats. However, the language may actually help us here – taking an idea from OCaml we may include new operators: (+.) : frac -> frac -> frac, (-.), (/.), (*.), because just like in OCaml we have only Hindley-Milner typesystem that won't allow more fancy polymorphism that would allow use of traditional +-like operators. Sample usage:

let a = frac(1, 6)  //  1/6
let b = a *. Int.to_frac(3)  // 1/2 – fractions should be kept in simplified version
let c = b.nom + b.den  // 1 + 2 = 3 – nom and den should be exposed to let users define their own stuff easier

Some operations will preserve rational body and there is nothing to bother here. There is however some problem with functions that may exit rationals, like sqrt, or exponentiation in general as their results can have infinite numerical representation and they will need to be approximated. On the other hand we are not introducing new issue – Sophia programmers still need to deal with it. There is no way to bypass it, but we may make this a bit nicer.

From my point of view it would be very handy to have approximation tools in some library that would perform it for user, but that is a different talk.

What would I expect / naming propositions

Contruction:

// Build fractional from nominator and denominator
frac : int -> int -> frac
// Conversion from int
Frac.from_int / Int.to_frac : int -> frac

Rounding:

Frac.round : frac -> int
Frac.floor : frac -> int
Frac.ceil : frac -> int

Operations:

Frac.add / (+.) : frac -> frac -> frac
Frac.sub / (-.) : frac -> frac -> frac
Frac.div / (/.) : frac -> frac -> frac
Frac.mul / (*.) : frac -> frac -> frac
// negation
Frac.neg : frac -> frac
// invertion
Frac.inv : frac -> frac

Beside that we can later provide some functions that approximate operations on real numbers, like

Frac.exp : frac -> frac -> frac -> frac
Frac.exp(base, exponent, maximum_error)

Constant definitions are accepted by the parser but not by the typechecker

The following contract causes the typechecker to throw an unknown_error:

contract C =
  let x = 2138
  entrypoint f() =123

Prepare Lima release - v4.0.0

This includes

check documentation
update changelog #164
tag aesophia
update aesophia_http aeternity/aesophia_http#48
update aesophia_cli aeternity/aesophia_cli#25
tag aesophia_http and aesophia_cli

Compiler crashes instead of giving an error message

When constructing an empty record:

contract Test = 
    record state = {}

    public entrypoint init() =
        state{}

the compiler crashes with the following stack trace:

{badmatch,[]} [{aeso_parser,record_or_map,1, [{file,"/app/_build/default/lib/aesophia/src/aeso_parser.erl"}, {line,364}]}, {aeso_parser,record_update,3, [{file,"/app/_build/default/lib/aesophia/src/aeso_parser.erl"}, {line,332}]}, {aeso_parser,elim,2, [{file,"/app/_build/default/lib/aesophia/src/aeso_parser.erl"}, {line,327}]}, {aeso_parse_lib,'-apply_p/2-fun-5-',3, [{file,"/app/_build/default/lib/aesophia/src/aeso_parse_lib.erl"}, {line,86}]}, {aeso_parse_lib,apply_p,2, [{file,"/app/_build/default/lib/aesophia/src/aeso_parse_lib.erl"}, {line,82}]}, {aeso_parse_lib,parse1,4, [{file,"/app/_build/default/lib/aesophia/src/aeso_parse_lib.erl"}, {line,300}]}, {aeso_parse_lib,parse,2, [{file,"/app/_build/default/lib/aesophia/src/aeso_parse_lib.erl"}, {line,163}]}, {aeso_parser,string,3, [{file,"/app/_build/default/lib/aesophia/src/aeso_parser.erl"}, {line,33}]}]
At: Line 0, column 0

The compiler should report an relevant error message instead of hard crashing.

Runtime validation of contracts

Checking at runtime that a given contract indeed implements the expected interface.

Release version 4.2.0

aesophia, aesophia_cli and aesophia_http

More functions on binaries

From the Sophia discussion at the Sofia Workshop.

Matching on individual bytes?

"assign" pattern

Like in Erlang or Haskell, ability to assign a variable to a pattern while matching

function f(x) = switch(x)
  h1::(t = h2::_) => (h1 + h2)::t  // same as `h1::h2::k => (h1 + h2)::h2::k`
  _ => x

Parameterised contracts

To make contract inheritance (#198) more useful it might be nice to support parameterised contracts:

contract Parent(type t, x : t) =
  ...
contract Main is Parent(int, 0) =
  ...

Builtin modifiers for token amounts

From the Sophia discussion at the Sofia workshop.

Crash when printing error message

Given the contract-stub:

contract HashTimeLock =
  datatype status = INVALID | ACTIVE | REFUNDED | WITHDRAWN | EXPIRED
  record lock_contract = {input_amount : int, output_amount : int, expiration : int, hash_lock : hash, status: status, sender : address, receiver : address, output_network : string, output_address : string}
  entrypoint new_contract(l : lock_contract) : lock_contract = l

The following call-result decoding fails:

./aesophia_cli /tmp/foo.aes -b fate --call_result cb_q58BgUFsUQgA37pD+/b+7SyBTPjsmp5mKp47Akx0c4yLS635b4gbwW1nTsf/wG+IG8FtZ07H/8BvhgFxEO8ARp8BgYcZ2AhdUzRj15KZWrT0vIXnJEq1gEZLA1zDge3Qam24r4UAAAAAAAE/nwCgBwwURA4zMENRZdpeBEtaqcNdLL4wyRwyFFVJN19SUmSfAKBrs4jtfFRU9fsXJtVRgxnm+6MvasbSWpfv9LbvZBN72A1BRVPRYWtfNDcxZFlVclE4RUF0bXp3dUtEdzRWQkdRZG5FY1A1WUY1NjNXRzR5UjlXdmZwNXRScCV612Q= --call_result_fun new_contract 
escript: exception error: no function clause matching 
                 aeso_pretty:type({variant_t,
                                   [{constr_t,
                                     [{file,no_file},{line,2},{col,21}],
                                     {con,
                                      [{file,no_file},{line,2},{col,21}],
                                      "INVALID"},
                                     []},
                                    {constr_t,
                                     [{file,no_file},{line,2},{col,31}],
                                     {con,
                                      [{file,no_file},{line,2},{col,31}],
                                      "ACTIVE"},
                                     []},
                                    {constr_t,
                                     [{file,no_file},{line,2},{col,40}],
                                     {con,
                                      [{file,no_file},{line,2},{col,40}],
                                      "REFUNDED"},
                                     []},
                                    {constr_t,
                                     [{file,no_file},{line,2},{col,51}],
                                     {con,
                                      [{file,no_file},{line,2},{col,51}],
                                      "WITHDRAWN"},
                                     []},
                                    {constr_t,
                                     [{file,no_file},{line,2},{col,63}],
                                     {con,
                                      [{file,no_file},{line,2},{col,63}],
                                      "EXPIRED"},
                                     []}]}) (/Users/hans/Quviq/Aeternity/aesophia_cli/_checkouts/aesophia/src/aeso_pretty.erl, line 245)
  in function  aeso_pretty:typed/2 (/Users/hans/Quviq/Aeternity/aesophia_cli/_checkouts/aesophia/src/aeso_pretty.erl, line 131)
  in call from lists:map/2 (lists.erl, line 1239)
  in call from lists:map/2 (lists.erl, line 1239)
  in call from aeso_pretty:typedef/1 (/Users/hans/Quviq/Aeternity/aesophia_cli/_checkouts/aesophia/src/aeso_pretty.erl, line 228)
  in call from aeso_compiler:to_sophia_value/5 (/Users/hans/Quviq/Aeternity/aesophia_cli/_checkouts/aesophia/src/aeso_compiler.erl, line 339)
  in call from aesophia_cli:decode_call_res/5 (/Users/hans/Quviq/Aeternity/aesophia_cli/src/aesophia_cli.erl, line 269)
  in call from aesophia_cli:main/1 (/Users/hans/Quviq/Aeternity/aesophia_cli/src/aesophia_cli.erl, line 62)

The problem comes from trying to print an error message for a variant-type that case is missing since aeso_pretty:type isn't normally called directly, but in to_sophia_value it is.

Cannot include by absolute path

The following contract fails with case_clause (assuming file exists):

include "/tmp/Jebudu.aes"
contract C =
  entrypoint f() = 123

"no arguments" displayed as empty string

AESO> function g(x) = x + 1
AESO> g() 
Error:
1:1:Cannot unify int
         and 
when checking the application at line 1, column 1 of
  g : (int) => int
to arguments

Speaking of the

1:1:Cannot unify int
         and

part. This is highly dangerous for the aesthetics

aeternity / aesophia Goto Github PK

aesophia's Introduction

aesophia

Documentation

Versioning

Interface Modules

aesophia's People

Contributors

Stargazers

Watchers

Forkers

aesophia's Issues

How does it look now

How do I see it

What would I expect / naming propositions

Recommend Projects

Recommend Topics

Recommend Org