Merge pull request #309 from aeternity/prepare_5.0.0

Preparing v5.0.0
2021-04-30 15:17:48 +02:00 · 2021-04-30 14:48:37 +02:00 · 2021-04-30 14:43:16 +02:00 · 2021-04-30 14:07:06 +02:00 · 2021-04-15 10:26:56 +02:00 · 2021-03-08 13:33:34 +01:00
62 changed files with 2387 additions and 755 deletions
@@ -8,6 +8,15 @@ executors:
    working_directory: ~/aesophia

 jobs:
+  verify_rebar_lock:
+    executor: aebuilder
+    steps:
+      - checkout
+      - run:
+          name: Ensure lock file is up-to-date
+          command: |
+            ./rebar3 upgrade
+            git diff --quiet -- rebar.lock || (echo "rebar.lock is not up-to-date" && exit 1)
  build:
    executor: aebuilder
    steps:
@@ -35,3 +44,10 @@ jobs:
            - _build/default/rebar3_20.3.8_plt
      - store_artifacts:
          path: _build/test/logs
+
+workflows:
+  version: 2
+  build_test:
+    jobs:
+      - build
+      - verify_rebar_lock
@@ -9,6 +9,97 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 ### Changed
 ### Removed

+## [5.0.0] 2021-04-30
+### Added
+- A new and improved [`String` standard library](https://github.com/aeternity/aesophia/blob/master/docs/sophia_stdlib.md#string)
+  has been added. Use it by `include "String.aes"`. It includes functions for
+  turning strings into lists of characters for detailed manipulation. For
+  example:
+  ```
+  include "String.aes"
+  contract C =
+    entrypoint filter_all_a(s: string) : string =
+      String.from_list(List.filter((c : char) => c != 'a', String.to_list(s)))
+  ```
+  will return a list with all `a`'s removed.
+
+  There are also convenience functions `split`, `concat`, `to_upper`,
+  `to_lower`, etc.
+
+  All String functions in FATEv2 operate on unicode code points.
+- Operations for pairing-based cryptography has been added the operations
+  are in the standard library [BLS12_381](https://github.com/aeternity/aesophia/blob/master/docs/sophia_stdlib.md#bls12_381).
+  With these operations it is possible to do Zero Knowledge-proofs, etc.
+  The operations are for the BLS12-381 curve (as the name suggests).
+- Calls to functions in other contracts (i.e. _remote calls_) can now be
+  [`protected`](https://github.com/aeternity/aesophia/blob/master/docs/sophia.md#protected-contract-calls).
+  If a contract call fails for any reason (for instance, the remote contract
+  crashes or runs out of gas, or the entrypoint doesn't exist or has the
+  wrong type) the parent call also fails. To make it possible to recover
+  from failures, contract calls takes a named argument `protected : bool`
+  (default `false`).
+
+  If `protected = true` the result of the contract call is wrapped in an
+  `option`, and `Some(value)` indicates a succesful execution and `None`
+  indicates that the contract call failed. Note: any gas consumed until
+  the failure is still charged, but all side effects in the remote
+  contract are rolled back on failure.
+- A new chain operation [`AENS.update`](https://github.com/aeternity/aesophia/blob/master/docs/sophia.md#aens-interface)
+  is supported.
+- New chain exploring operations `AENS.lookup` and `Oracle.expiry` to
+  look up an AENS record and the expiry of an Oracle respectively, are added.
+- Transaction introspection (`Auth.tx`) has been added. When a Generalized
+  account is authorized, the authorization function needs access to the
+  transaction (and the transaction hash) for the wrapped transaction. The
+  transaction and the transaction hash is available `Auth.tx`, it is only
+  available during authentication if invoked by a normal contract call
+  it returns `None`. Example:
+  ```
+  switch(Auth.tx)
+    None      => abort("Not in Auth context")
+    Some(tx0) =>
+      switch(tx0.tx)
+        Chain.SpendTx(_, amount, _)  => amount > 400
+        Chain.ContractCallTx(_, _)   => true
+        _                            => false
+  ```
+- A debug mode is a added to the compiler. Right now its only use is to
+  turn off hermetization.
+### Changed
+- The function `Chain.block_hash(height)` is now (in FATEv2) defined for
+  the current height - this used to be an error.
+- Standard library: Sort is optimized to do `mergesort` and a `contains`
+  function is added.
+- Improved type errors and explicit errors for some syntax errors (empty code
+  blocks, etc.).
+- Compiler optimization: The ACI is generated alongside bytecode. This means
+  that multiple compiler passes can be avoided.
+- Compiler optimization: Improved parsing (less stack used when transpiled).
+- A bug where constraints were handled out of order fixed.
+- Fixed calldata decoding for singleton records.
+- Improved the documentation w.r.t. signatures, especially stressing the fact that
+  the network ID is a part of what is signed.
+### Removed
+
+## [4.3.0]
+### Added
+- Added documentation (moved from `protocol`)
+- `Frac.aes` – library for rational numbers
+- Added some more meaningful error messages
+- Exported several parsing functionalities
+ - With option `keep_included` it is possible to see which files were included during the parse
+ - There is a function `run_parser` that be used to evaluate any parsing rule
+ - Exported parsers: `body`, `type` and `decl`
+### Changed
+- Performance improvements in the standard library
+- Fixed ACI encoder to handle `-` unary operator
+- Fixed including by absolute path
+- Fixed variant type printing in the ACI error messages
+- Fixed pretty printing of combined function clauses
+### Removed
+- `let` definitions are no longer supported in the toplevel of the contract
+- type declarations are no longer supported
+
 ## [4.2.0] - 2020-01-15
 ### Added
 - Allow separate entrypoint/function type signature and definition, and pattern
@@ -53,7 +144,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
  (de-)construct byte arrays.
 - `[a..b]` language construct, returning the list of numbers between
  `a` and `b` (inclusive). Returns the empty list if `a` > `b`.
- [Standard libraries] (https://github.com/aeternity/protocol/blob/master/contracts/sophia_stdlib.md)
+- [Standard libraries](https://github.com/aeternity/aesophia/blob/master/docs/sophia_stdlib.md)
 - Checks that `init` is not called from other functions.
 - FATE backend - the compiler is able to produce VM code for both `AEVM` and `FATE`. Many
  of the APIs now take `{backend, aevm | fate}` to decide wich backend to produce artifacts
@@ -192,10 +283,12 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Simplify calldata creation - instead of passing a compiled contract, simply
  pass a (stubbed) contract string.

-[Unreleased]: https://github.com/aeternity/aesophia/compare/v4.2.0...HEAD
-[4.2.0]: https://github.com/aeternity/aesophia/compare/v4.2.0...v4.1.0
-[4.1.0]: https://github.com/aeternity/aesophia/compare/v4.1.0...v4.0.0
-[4.0.0]: https://github.com/aeternity/aesophia/compare/v4.0.0...v3.2.0
+[Unreleased]: https://github.com/aeternity/aesophia/compare/v5.0.0...HEAD
+[5.0.0]: https://github.com/aeternity/aesophia/compare/v4.3.0...v5.0.0
+[4.3.0]: https://github.com/aeternity/aesophia/compare/v4.2.0...v4.3.0
+[4.2.0]: https://github.com/aeternity/aesophia/compare/v4.1.0...v4.2.0
+[4.1.0]: https://github.com/aeternity/aesophia/compare/v4.0.0...v4.1.0
+[4.0.0]: https://github.com/aeternity/aesophia/compare/v3.2.0...v4.0.0
 [3.2.0]: https://github.com/aeternity/aesophia/compare/v3.1.0...v3.2.0
 [3.1.0]: https://github.com/aeternity/aesophia/compare/v3.0.0...v3.1.0
 [3.0.0]: https://github.com/aeternity/aesophia/compare/v2.1.0...v3.0.0
@@ -1,12 +1,11 @@
 # aesophia

-This is the __sophia__ compiler for the æternity system which compiles contracts written in __sophia__ code to the æternity VM code.
-
-It is an OTP application written in Erlang and is by default included in
-[the æternity node](https://github.com/aeternity/epoch). However, it can
-also be included in other systems to compile contracts coded in sophia which
-can then be loaded into the æternity system.
+This is the __sophia__ compiler for the æternity system which compiles contracts written in __sophia__ to [FATE](https://github.com/aeternity/protocol/blob/master/contracts/fate.md) instructions.

+The compiler is currently being used three places
+ - [The command line compiler](https://github.com/aeternity/aesophia_cli)
+ - [The HTTP compiler](https://github.com/aeternity/aesophia_http)
+ - In [Aeternity node](https://github.com/aeternity/aeternity) tests

 ## Documentation

@@ -14,7 +13,6 @@ can then be loaded into the æternity system.
 * [Sophia Documentation](docs/sophia.md).
 * [Sophia Standard Library](docs/sophia_stdlib.md).

-
 ## Versioning

 `aesophia` has a version that is only loosely connected to the version of the
@@ -23,7 +21,6 @@ minor/patch version. The `aesophia` compiler version MUST be bumped whenever
 there is a change in how byte code is generated, but it MAY also be bumped upon
 API changes etc.

-
 ## Interface Modules

 The basic modules for interfacing the compiler:
@@ -6,6 +6,7 @@
 - [Language Features](#language-features)
    - [Contracts](#contracts)
        - [Calling other contracts](#calling-other-contracts)
+        - [Protected contract calls](#protected-contract-calls)
        - [Mutable state](#mutable-state)
            - [Stateful functions](#stateful-functions)
        - [Payable](#payable)
@@ -27,6 +28,7 @@
            - [Updating a value](#updating-a-value)
            - [Map implementation](#map-implementation)
        - [Strings](#strings)
+        - [Chars](#chars)
        - [Byte arrays](#byte-arrays)
        - [Cryptographic builins](#cryptographic-builins)
            - [AEVM note](#aevm-note)
@@ -35,6 +37,7 @@
            - [Example](#example)
            - [Sanity checks](#sanity-checks)
        - [AENS interface](#aens-interface)
+            - [Example](#example-1)
        - [Events](#events)
            - [Argument order](#argument-order)
        - [Compiler pragmas](#compiler-pragmas)
@@ -53,8 +56,8 @@
        - [Operators types](#operators-types)
        - [Operator precendences](#operator-precendences)
    - [Examples](#examples)
-    - [The lifetime of a contract](#the-lifetime-of-a-contract)
-        - [Killing a contract](#killing-a-contract)
+        - [Delegation signature](#delegation-signature)
+

 ## The Sophia Language
 An Æternity BlockChain Language
@@ -80,7 +83,7 @@ The main unit of code in Sophia is the *contract*.
 - A contract may define a type `state` encapsulating its local
  state. When creating a new contract the `init` entrypoint is executed and the
  state is initialized to its return value.
-  
+
 The language offers some primitive functions to interact with the blockchain and contracts.
 Please refer to the [Chain](sophia_stdlib.md#Chain), [Contract](sophia_stdlib.md#Contract)
 and the [Call](sophia_stdlib.md#Call) namespaces in the documentation.
@@ -138,6 +141,36 @@ without calling it you can write
    Chain.spend(v.address, amount)
 ```

+#### Protected contract calls
+
+If a contract call fails for any reason (for instance, the remote contract
+crashes or runs out of gas, or the entrypoint doesn't exist or has the wrong
+type) the parent call also fails. To make it possible to recover from failures,
+contract calls takes a named argument `protected : bool` (default `false`).
+
+The protected argument must be a literal boolean, and when set to `true`
+changes the type of the contract call, wrapping the result in an `option` type.
+If the call fails the result is `None`, otherwise it's `Some(r)` where `r` is
+the return value of the call.
+
+```sophia
+contract VotingType =
+  entrypoint : vote : string => unit
+
+contract Voter =
+  entrypoint tryVote(v : VotingType, alt : string) =
+    switch(v.vote(alt, protected = true) : option(unit))
+      None    => "Voting failed"
+      Some(_) => "Voting successful"
+```
+
+Any gas that was consumed by the contract call before the failure stays
+consumed, which means that in order to protect against the remote contract
+running out of gas it is necessary to set a gas limit using the `gas` argument.
+However, note that errors that would normally consume all the gas in the
+transaction still only uses up the gas spent running the contract.
+
+
 ### Mutable state

 Sophia does not have arbitrary mutable state, but only a limited form of
@@ -186,6 +219,7 @@ Without the `stateful` annotation the compiler does not allow the call to
  - `AENS.claim`
  - `AENS.transfer`
  - `AENS.revoke`
+  - `AENS.update`
 * Call a `stateful` function in the current contract
 * Call another contract with a non-zero `value` argument.

@@ -281,7 +315,7 @@ so even cyclic includes should be working without any special tinkering.

 ### Standard library

-Sophia offers [standard library](sophia_stdlib.md) which exposes some 
+Sophia offers [standard library](sophia_stdlib.md) which exposes some
 primitive operations and some higher level utilities. The builtin
 namespaces like `Chain`, `Contract`, `Map`
 are included by default and are supported internally by the compiler.
@@ -446,6 +480,13 @@ Example syntax:
 // yields [12,13,14,20,21,22,30,31,32]
 ```

+Lists can be constructed using the range syntax using special `..` operator:
+```
+[1..4] == [1,2,3,4]
+```
+The ranges are always ascending and have step equal to 1.
+
+
 Please refer to the [standard library](sophia_stdlib.md#List) for the predefined functionalities.

 ### Maps and records
@@ -533,7 +574,16 @@ Strings can be compared for equality (`==`, `!=`), used as keys in maps and
 records, and used in builtin functions `String.length`, `String.concat` and
 the hash functions described below.

-Please refer to the `Map` [library documentation](sophia_stdlib.md#String).
+Please refer to the `String` [library documentation](sophia_stdlib.md#String).
+
+### Chars
+
+There is a builtin type `char` (the underlying representation being an integer),
+mainly used to manipulate strings via `String.to_list`/`String.from_list`.
+
+Characters can also be introduced as character literals (`'x', '+', ...).
+
+Please refer to the `Char` [library documentation](sophia_stdlib.md#Char).

 ### Byte arrays

@@ -546,7 +596,7 @@ Please refer to the `Bytes` [library documentation](sophia_stdlib.md#Bytes).

 ### Cryptographic builins

-Libraries [Crypto](sophia_stdlib.md#Crypto) and [String](sophia_stdlib.md#String) provide functions to 
+Libraries [Crypto](sophia_stdlib.md#Crypto) and [String](sophia_stdlib.md#String) provide functions to
 hash objects, verify signatures etc. The `hash` is a type alias for `bytes(32)`.

 #### AEVM note
@@ -560,11 +610,10 @@ string`, `String.sha3(s)` and `Crypto.sha3(s)` will give different results on AE
 ### Authorization interface

 When a Generalized account is authorized, the authorization function needs
-access to the transaction hash for the wrapped transaction. (A `GAMetaTx`
-wrapping a transaction.) The transaction hash is available in the primitive
-`Auth.tx_hash`, it is *only* available during authentication if invoked by a
-normal contract call it returns `None`.
-
+access to the transaction and the transaction hash for the wrapped transaction. (A `GAMetaTx`
+wrapping a transaction.) The transaction and the transaction hash is available in the primitive
+`Auth.tx` and `Auth.tx_hash` respectively, they are *only* available during authentication if invoked by a
+normal contract call they return `None`.

 ### Oracle interface
 You can attach an oracle to the current contract and you can interact with oracles
@@ -582,7 +631,7 @@ Example for an oracle answering questions of type `string` with answers of type
 contract Oracles =

  stateful entrypoint registerOracle(acct : address,
-                                     sign : signature,   // Signed oracle address + contract address
+                                     sign : signature,   // Signed network id + oracle address + contract address
                                     qfee : int,
                                     ttl  : Chain.ttl) : oracle(string, int) =
     Oracle.register(acct, signature = sign, qfee, ttl)
@@ -603,13 +652,13 @@ contract Oracles =
    Oracle.extend(o, ttl)

  stateful entrypoint signExtendOracle(o    : oracle(string, int),
-                                     sign : signature,   // Signed oracle address + contract address
-                                     ttl  : Chain.ttl) : unit =
+                                       sign : signature,   // Signed network id + oracle address + contract address
+                                       ttl  : Chain.ttl) : unit =
    Oracle.extend(o, signature = sign, ttl)

  stateful entrypoint respond(o    : oracle(string, int),
                              q    : oracle_query(string, int),
-                              sign : signature,        // Signed oracle query id + contract address
+                              sign : signature,        // Signed network id + oracle query id + contract address
                              r    : int) =
    Oracle.respond(o, q, signature = sign, r)

@@ -630,7 +679,7 @@ contract Oracles =

 #### Sanity checks

-When an Oracle literal is passed to a contract, no deep checks are performed. 
+When an Oracle literal is passed to a contract, no deep checks are performed.
 For extra safety [Oracle.check](sophia_stdlib.md#check) and [Oracle.check_query](sophia_stdlib.md#check_query)
 functions are provided.

@@ -640,6 +689,46 @@ Contracts can interact with the
 [Aeternity Naming System](https://github.com/aeternity/protocol/blob/master/AENS.md).
 For this purpose the [AENS](sophia_stdlib.md#AENS) library was exposed.

+#### Example
+
+In this example we assume that the name `name` already exists, and is owned by
+an account with address `addr`. In order to allow a contract `ct` to handle
+`name` the account holder needs to create a
+[signature](#delegation-signature) `sig` of `addr | name.hash | ct.address`.
+
+Armed with this information we can for example write a function that extends
+the name if it expires within 1000 blocks:
+```
+  stateful entrypoint extend_if_necessary(addr : address, name : string, sig : signature) =
+    switch(AENS.lookup(name))
+      None => ()
+      Some(AENS.Name(_, FixedTTL(expiry), _)) =>
+        if(Chain.block_height + 1000 > expiry)
+          AENS.update(addr, name, Some(RelativeTTL(50000)), None, None, signature = sig)
+```
+
+And we can write functions that adds and removes keys from the pointers of the
+name:
+```
+  stateful entrypoint add_key(addr : address, name : string, key : string,
+                              pt : AENS.pointee, sig : signature) =
+    switch(AENS.lookup(name))
+      None => ()
+      Some(AENS.Name(_, _, ptrs)) =>
+        AENS.update(addr, name, None, None, Some(ptrs{[key] = pt}), signature = sig)
+
+  stateful entrypoint delete_key(addr : address, name : string,
+                                 key : string, sig : signature) =
+    switch(AENS.lookup(name))
+      None => ()
+      Some(AENS.Name(_, _, ptrs)) =>
+        let ptrs = Map.delete(key, ptrs)
+        AENS.update(addr, name, None, None, Some(ptrs), signature = sig)
+```
+
+*Note:* From the Iris hardfork more strict rules apply for AENS pointers, when
+a Sophia contract lookup or update (bad) legacy pointers, the bad keys are
+automatically removed so they will not appear in the pointers map.

 ### Events

@@ -653,7 +742,7 @@ To use events a contract must declare a datatype `event`, and events are then
 logged using the `Chain.event` function:

 ```
-  datatype event 
+  datatype event
    = Event1(int, int, string)
    | Event2(string, address)

@@ -825,15 +914,17 @@ In describing the syntax below, we use the following conventions:
 A Sophia file consists of a sequence of *declarations* in a layout block.

 ```c
-File ::= Block(Decl)
-Decl ::= ['payable'] 'contract' Con '=' Block(Decl)
+File ::= Block(TopDecl)
+
+TopDecl ::= ['payable'] 'contract' Con '=' Block(Decl)
       | 'namespace' Con '=' Block(Decl)
       | '@compiler' PragmaOp Version
       | 'include' String
-       | 'type'     Id ['(' TVar* ')'] ['=' TypeAlias]
+
+Decl ::= 'type'     Id ['(' TVar* ')'] '=' TypeAlias
       | 'record'   Id ['(' TVar* ')'] '=' RecordType
       | 'datatype' Id ['(' TVar* ')'] '=' DataType
-       | EModifier* ('entrypoint' | 'function') Block(FunDecl)
+       | (EModifier* 'entrypoint' | FModifier* 'function') Block(FunDecl)

 FunDecl ::= Id ':' Type                             // Type signature
          | Id Args [':' Type] '=' Block(Stmt)      // Definition
@@ -945,6 +1036,7 @@ Expr ::= '(' LamArgs ')' '=>' Block(Stmt)   // Anonymous function    (x) => x +
       | '[' Sep(Expr, ',') ']'             // List                  [1, 2, 3]
       | '[' Expr '|' Sep(Generator, ',') ']'
                                            // List comprehension    [k | x <- [1], if (f(x)), let k = x+1]
+       | '[' Expr '..' Expr ']'             // List range            [1..n]
       | '{' Sep(FieldUpdate, ',') '}'      // Record or map value   {x = 0, y = 1}, {[key] = val}
       | '(' Expr ')'                       // Parens                (1 + 2) * 3
       | Id | Con | QId | QCon              // Identifiers           x, None, Map.member, AELib.Token
@@ -1012,8 +1104,8 @@ contract FundMe =
                   deadline      : int,
                   goal          : int }

-  function spend(args : spend_args) =
-    raw_spend(args.recipient, args.amount)
+  stateful function spend(args : spend_args) =
+    Chain.spend(args.recipient, args.amount)

  entrypoint init(beneficiary, deadline, goal) : state =
    { contributions = {},
@@ -1052,7 +1144,6 @@ contract FundMe =
    require(state.total >= state.goal, "Project was not funded")
    spend({recipient = state.beneficiary,
           amount    = Contract.balance })
-    put(state{ beneficiary = #0 })

  stateful function withdraw_contributor() =
    if(state.total >= state.goal)
@@ -1062,3 +1153,11 @@ contract FundMe =
           amount    = state.contributions[to]})
    put(state{ contributions @ c = Map.delete(to, c) })
 ```
+
+### Delegation signature
+
+Some chain operations (`Oracle.<operation>` and `AENS.<operation>`) have an
+optional delegation signature. This is typically used when a user/accounts
+would like to allow a contract to act on it's behalf. The exact data to be
+signed varies for the different operations, but in all cases you should prepend
+the signature data with the `network_id` (`ae_mainnet` for the Aeternity mainnet, etc.).
@@ -0,0 +1,68 @@
+namespace BLS12_381 =
+  type fr    = MCL_BLS12_381.fr
+  type fp    = MCL_BLS12_381.fp
+  record fp2 = { x1 : fp, x2 : fp }
+  record g1  = { x : fp, y : fp, z : fp }
+  record g2  = { x : fp2, y : fp2, z : fp2 }
+  record gt  = { x1 : fp, x2 : fp, x3 : fp, x4 : fp, x5 : fp, x6 : fp,
+                 x7 : fp, x8 : fp, x9 : fp, x10 : fp, x11 : fp, x12 : fp }
+
+  function pairing_check(xs : list(g1), ys : list(g2)) =
+    switch((xs, ys))
+      ([], []) => true
+      (x :: xs, y :: ys) => pairing_check_(pairing(x, y), xs, ys)
+
+  function pairing_check_(acc : gt, xs : list(g1), ys : list(g2)) =
+    switch((xs, ys))
+      ([], []) => gt_is_one(acc)
+      (x :: xs, y :: ys) =>
+        pairing_check_(gt_mul(acc, pairing(x, y)), xs, ys)
+
+  function int_to_fr(x : int) = MCL_BLS12_381.int_to_fr(x)
+  function int_to_fp(x : int) = MCL_BLS12_381.int_to_fp(x)
+  function fr_to_int(x : fr)  = MCL_BLS12_381.fr_to_int(x)
+  function fp_to_int(x : fp)  = MCL_BLS12_381.fp_to_int(x)
+
+  function mk_g1(x : int, y : int, z : int) : g1 =
+    { x = int_to_fp(x), y = int_to_fp(y), z = int_to_fp(z) }
+
+  function mk_g2(x1 : int, x2 : int, y1 : int, y2 : int, z1 : int, z2 : int) : g2 =
+    { x = {x1 = int_to_fp(x1), x2 = int_to_fp(x2)},
+      y = {x1 = int_to_fp(y1), x2 = int_to_fp(y2)},
+      z = {x1 = int_to_fp(z1), x2 = int_to_fp(z2)} }
+
+  function pack_g1(t) = switch(t)
+                          (x, y, z) => {x = x, y = y, z = z} : g1
+  function pack_g2(t) = switch(t)
+                          ((x1, x2), (y1, y2), (z1, z2)) =>
+                            {x = {x1 = x1, x2 = x2}, y = {x1 = y1, x2 = y2}, z = {x1 = z1, x2 = z2}} : g2
+  function pack_gt(t) = switch(t)
+                          (x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) =>
+                            {x1 = x1, x2 = x2, x3 = x3, x4 = x4, x5 = x5, x6 = x6,
+                             x7 = x7, x8 = x8, x9 = x9, x10 = x10, x11 = x11, x12 = x12} : gt
+
+  function g1_neg(p : g1)         = pack_g1(MCL_BLS12_381.g1_neg((p.x, p.y, p.z)))
+  function g1_norm(p : g1)        = pack_g1(MCL_BLS12_381.g1_norm((p.x, p.y, p.z)))
+  function g1_valid(p : g1)       = MCL_BLS12_381.g1_valid((p.x, p.y, p.z))
+  function g1_is_zero(p : g1)     = MCL_BLS12_381.g1_is_zero((p.x, p.y, p.z))
+  function g1_add(p : g1, q : g1) = pack_g1(MCL_BLS12_381.g1_add((p.x, p.y, p.z), (q.x, q.y, q.z)))
+  function g1_mul(k : fr, p : g1) = pack_g1(MCL_BLS12_381.g1_mul(k, (p.x, p.y, p.z)))
+
+  function g2_neg(p : g2)         = pack_g2(MCL_BLS12_381.g2_neg(((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2))))
+  function g2_norm(p : g2)        = pack_g2(MCL_BLS12_381.g2_norm(((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2))))
+  function g2_valid(p : g2)       = MCL_BLS12_381.g2_valid(((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2)))
+  function g2_is_zero(p : g2)     = MCL_BLS12_381.g2_is_zero(((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2)))
+  function g2_add(p : g2, q : g2) = pack_g2(MCL_BLS12_381.g2_add(((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2)),
+                                                                 ((q.x.x1, q.x.x2), (q.y.x1, q.y.x2), (q.z.x1, q.z.x2))))
+  function g2_mul(k : fr, p : g2) = pack_g2(MCL_BLS12_381.g2_mul(k, ((p.x.x1, p.x.x2), (p.y.x1, p.y.x2), (p.z.x1, p.z.x2))))
+
+  function gt_inv(p : gt)              = pack_gt(MCL_BLS12_381.gt_inv((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12)))
+  function gt_add(p : gt, q : gt)      = pack_gt(MCL_BLS12_381.gt_add((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12),
+                                                                      (q.x1, q.x2, q.x3, q.x4, q.x5, q.x6, q.x7, q.x8, q.x9, q.x10, q.x11, q.x12)))
+  function gt_mul(p : gt, q : gt)      = pack_gt(MCL_BLS12_381.gt_mul((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12),
+                                                                      (q.x1, q.x2, q.x3, q.x4, q.x5, q.x6, q.x7, q.x8, q.x9, q.x10, q.x11, q.x12)))
+  function gt_pow(p : gt, k : fr)      = pack_gt(MCL_BLS12_381.gt_pow((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12), k))
+  function gt_is_one(p : gt)           = MCL_BLS12_381.gt_is_one((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12))
+  function pairing(p : g1, q : g2)     = pack_gt(MCL_BLS12_381.pairing((p.x, p.y, p.z), ((q.x.x1, q.x.x2), (q.y.x1, q.y.x2), (q.z.x1, q.z.x2))))
+  function miller_loop(p : g1, q : g2) = pack_gt(MCL_BLS12_381.miller_loop((p.x, p.y, p.z), ((q.x.x1, q.x.x2), (q.y.x1, q.y.x2), (q.z.x1, q.z.x2))))
+  function final_exp(p : gt)           = pack_gt(MCL_BLS12_381.final_exp((p.x1, p.x2, p.x3, p.x4, p.x5, p.x6, p.x7, p.x8, p.x9, p.x10, p.x11, p.x12)))
@@ -56,11 +56,14 @@ namespace Frac =
 /** Integer to rational division
 */
  function make_frac(n : int, d : int) : frac =
-    if (d == 0) abort("Division by zero")
+    if (d == 0) abort("Zero denominator")
    elif (n == 0) Zero
    elif ((n < 0) == (d < 0)) simplify(Pos(abs_int(n), abs_int(d)))
    else simplify(Neg(abs_int(n), abs_int(d)))

+  function one() : frac = Pos(1, 1)
+  function zero() : frac = Zero
+
  function eq(a : frac, b : frac) : bool =
    let (na, da) = to_pair(a)
    let (nb, db) = to_pair(b)
@@ -146,7 +149,10 @@ namespace Frac =

  function mul(a : frac, b : frac) : frac = make_frac(num(a) * num(b), den(a) * den(b))

-  function div(a : frac, b : frac) : frac = mul(a, inv(b))
+  function div(a : frac, b : frac) : frac = switch(b)
+    Neg(n, d) => mul(a, Neg(d, n))
+    Zero      => abort("Division by zero")
+    Pos(n, d) => mul(a, Pos(d, n))

 /** `b` to the power of `e`
 */
@@ -168,9 +174,10 @@ namespace Frac =
  function optimize(f : frac, loss : frac) : frac =
    require(geq(loss, Zero), "negative loss optimize")
    let s = sign(f)
-    mul(from_int(s), run_optimize(abs(f), loss))
-  private function run_optimize(f : frac, loss : frac) : frac =
-    let t = make_frac((num(f) + 1) / 2, (den(f) + 1)/2)
-    if(gt(abs(sub(t, f)), loss)) f
+    mul(from_int(s), run_optimize(abs(f), abs(f), loss))
+  private function run_optimize(orig : frac, f : frac, loss : frac) : frac =
+    let (n, d) = to_pair(f)
+    let t = make_frac((n+1)/2, (d+1)/2)
+    if(gt(abs(sub(t, orig)), loss)) f
    elif (eq(t, f)) f
-    else run_optimize(t, loss)
+    else run_optimize(orig, t, loss)
@@ -15,10 +15,24 @@ namespace List =
    _::t => Some(t)

  function last(l : list('a)) : option('a) = switch(l)
-    []  => None
-    [x] => Some(x)
+    []   => None
+    [x]  => Some(x)
    _::t => last(t)

+  function drop_last(l : list('a)) : option(list('a)) = switch(l)
+    [] => None
+    _  => Some(drop_last_unsafe(l))
+
+  function drop_last_unsafe(l : list('a)) : list('a) = switch(l)
+    [_]  => []
+    h::t => h::drop_last_unsafe(t)
+    []   => abort("drop_last_unsafe: list empty")
+
+
+  function contains(e : 'a, l : list('a)) = switch(l)
+    []   => false
+    h::t => h == e || contains(e, t)
+
 /** Finds first element of `l` fulfilling predicate `p` as `Some` or `None`
 * if no such element exists.
 */
@@ -28,14 +42,15 @@ namespace List =

 /** Returns list of all indices of elements from `l` that fulfill the predicate `p`.
 */
-  function find_indices(p : 'a => bool, l : list('a)) : list(int) = find_indices_(p, l, 0, [])
+  function find_indices(p : 'a => bool, l : list('a)) : list(int) = find_indices_(p, l, 0)
  private function find_indices_( p : 'a => bool
                                , l : list('a)
                                , n : int
-                                , acc : list(int)
                                ) : list(int) = switch(l)
-    []   => reverse(acc)
-    h::t => find_indices_(p, t, n+1, if(p(h)) n::acc else acc)
+    []   => []
+    h::t =>
+     let rest = find_indices_(p, t, n+1)
+     if(p(h)) n::rest else rest

  function nth(n : int, l : list('a)) : option('a) =
    switch(l)
@@ -64,44 +79,44 @@ namespace List =
 * `a` and `b` jumping by given `step`. Includes `a` and takes
 * `b` only if `(b - a) mod step == 0`. `step` should be bigger than 0.
 */
-  function from_to_step(a : int, b : int, s : int) : list(int) = from_to_step_(a, b, s, [])
-  private function from_to_step_(a, b, s, acc) =
-    if (a > b) reverse(acc) else from_to_step_(a + s, b, s, a :: acc)
+  function from_to_step(a : int, b : int, s : int) : list(int) =
+    from_to_step_(a, b - (b-a) mod s, s, [])
+  private function from_to_step_(a : int, b : int, s : int, acc : list(int)) : list(int) =
+    if(b < a) acc
+    else from_to_step_(a, b - s, s, b::acc)


 /** Unsafe. Replaces `n`th element of `l` with `e`. Crashes on over/underflow
 */
  function replace_at(n : int, e : 'a, l : list('a)) : list('a) =
-    if(n<0) abort("insert_at underflow") else replace_at_(n, e, l, [])
-  private function replace_at_(n : int, e : 'a, l : list('a), acc : list('a)) : list('a) =
+    if(n<0) abort("insert_at underflow") else replace_at_(n, e, l)
+  private function replace_at_(n : int, e : 'a, l : list('a)) : list('a) =
   switch(l)
     []   => abort("replace_at overflow")
-     h::t => if (n == 0) reverse(e::acc) ++ t
-             else replace_at_(n-1, e, t, h::acc)
+     h::t => if (n == 0) e::t
+             else h::replace_at_(n-1, e, t)

 /** Unsafe. Adds `e` to `l` to be its `n`th element. Crashes on over/underflow
 */
  function insert_at(n : int, e : 'a, l : list('a)) : list('a) =
-    if(n<0) abort("insert_at underflow") else insert_at_(n, e, l, [])
-  private function insert_at_(n : int, e : 'a, l : list('a), acc : list('a)) : list('a) =
-   if (n == 0) reverse(e::acc) ++ l
+    if(n<0) abort("insert_at underflow") else insert_at_(n, e, l)
+  private function insert_at_(n : int, e : 'a, l : list('a)) : list('a) =
+   if (n == 0) e::l
   else switch(l)
     []   => abort("insert_at overflow")
-     h::t => insert_at_(n-1, e, t, h::acc)
+     h::t => h::insert_at_(n-1, e, t)

 /** Assuming that cmp represents `<` comparison, inserts `x` before
 * the first element in the list `l` which is greater than it
 */
  function insert_by(cmp : (('a, 'a) => bool), x : 'a, l : list('a)) : list('a) =
-    insert_by_(cmp, x, l, [])
-  private function insert_by_(cmp : (('a, 'a) => bool), x : 'a, l : list('a), acc : list('a)) : list('a) =
    switch(l)
-      []   => reverse(x::acc)
+      []   => [x]
      h::t =>
        if(cmp(x, h)) // x < h
-          reverse(acc) ++ (x::l)
+          x::l
        else
-          insert_by_(cmp, x, t, h::acc)
+          h::insert_by(cmp, x, t)


  function foldr(cons : ('a, 'b) => 'b, nil : 'b, l : list('a)) : 'b = switch(l)
@@ -119,49 +134,52 @@ namespace List =
       f(e)
       foreach(l', f)

-  function reverse(l : list('a)) : list('a) = foldl((lst, el) => el :: lst, [], l)
+  function reverse(l : list('a)) : list('a) = reverse_(l, [])
+  private function reverse_(l : list('a), acc : list('a)) : list('a) = switch(l)
+    [] => acc
+    h::t => reverse_(t, h::acc)

-  function map(f : 'a => 'b, l : list('a)) : list('b) = map_(f, l, [])
-  private function map_(f : 'a => 'b, l : list('a), acc : list('b)) : list('b) = switch(l)
-    []   => reverse(acc)
-    h::t => map_(f, t, f(h)::acc)
+  function map(f : 'a => 'b, l : list('a)) : list('b) = switch(l)
+    [] => []
+    h::t => f(h)::map(f, t)

 /** Effectively composition of `map` and `flatten`
 */
  function flat_map(f : 'a => list('b), l : list('a)) : list('b) =
    ListInternal.flat_map(f, l)

-  function filter(p : 'a => bool, l : list('a)) : list('a) = filter_(p, l, [])
-  private function filter_(p : 'a => bool, l : list('a), acc : list('a)) : list('a) = switch(l)
-    []   => reverse(acc)
-    h::t => filter_(p, t, if(p(h)) h::acc else acc)
+  function filter(p : 'a => bool, l : list('a)) : list('a) = switch(l)
+    []   => []
+    h::t =>
+      let rest = filter(p, t)
+      if(p(h)) h::rest else rest

-/** Take `n` first elements
+/** Take up to `n` first elements
 */
  function take(n : int, l : list('a)) : list('a) =
-    if(n < 0) abort("Take negative number of elements") else take_(n, l, [])
-  private function take_(n : int, l : list('a), acc : list('a)) : list('a) =
-    if(n == 0) reverse(acc)
+    if(n < 0) abort("Take negative number of elements") else take_(n, l)
+  private function take_(n : int, l : list('a)) : list('a) =
+    if(n == 0) []
    else switch(l)
-      []   => reverse(acc)
-      h::t => take_(n-1, t, h::acc)
+      []   => []
+      h::t => h::take_(n-1, t)

-/** Drop `n` first elements
+/** Drop up to `n` first elements
 */
  function drop(n : int, l : list('a)) : list('a) =
-   if(n < 0) abort("Drop negative number of elements")
-   elif (n == 0) l
+   if(n < 0) abort("Drop negative number of elements") else drop_(n, l)
+  private function drop_(n : int, l : list('a)) : list('a) =
+   if (n == 0) l
   else switch(l)
      []   => []
-      h::t => drop(n-1, t)
+      h::t => drop_(n-1, t)

 /** Get the longest prefix of a list in which every element
 * matches predicate `p`
 */
-  function take_while(p : 'a => bool, l : list('a)) : list('a) = take_while_(p, l, [])
-  private function take_while_(p : 'a => bool, l : list('a), acc : list('a)) : list('a) = switch(l)
-    []   => reverse(acc)
-    h::t => if(p(h)) take_while_(p, t, h::acc) else reverse(acc)
+  function take_while(p : 'a => bool, l : list('a)) : list('a) = switch(l)
+    []   => []
+    h::t => if(p(h)) h::take_while(p, t) else []

 /** Drop elements from `l` until `p` holds
 */
@@ -172,18 +190,15 @@ namespace List =
 /** Splits list into two lists of elements that respectively
 * match and don't match predicate `p`
 */
-  function partition(p : 'a => bool, l : list('a)) : (list('a) * list('a)) = partition_(p, l, [], [])
-  private function partition_( p : 'a => bool
-                             , l : list('a)
-                             , acc_t : list('a)
-                             , acc_f : list('a)
-                             ) : (list('a) * list('a)) = switch(l)
-    []   => (reverse(acc_t), reverse(acc_f))
-    h::t => if(p(h)) partition_(p, t, h::acc_t, acc_f) else partition_(p, t, acc_t, h::acc_f)
+  function partition(p : 'a => bool, l : list('a)) : (list('a) * list('a)) = switch(l)
+    []   => ([], [])
+    h::t =>
+      let (l, r) = partition(p, t)
+      if(p(h)) (h::l, r) else (l, h::r)

-/** Flattens list of lists into a single list
- */
-  function flatten(ll : list(list('a))) : list('a) = foldr((l1, l2) => l1 ++ l2, [], ll)
+  function flatten(l : list(list('a))) : list('a) = switch(l)
+    []   => []
+    h::t => h ++ flatten(t)

  function all(p : 'a => bool, l : list('a)) : bool = switch(l)
    []   => true
@@ -199,49 +214,99 @@ namespace List =


 /** Zips two list by applying bimapping function on respective elements.
- * Drops longer tail.
+ * Drops the tail of the longer list.
 */
-  function zip_with(f : ('a, 'b) => 'c, l1 : list('a), l2 : list('b)) : list('c) = zip_with_(f, l1, l2, [])
-  private function zip_with_( f : ('a, 'b) => 'c
+  private function zip_with( f : ('a, 'b) => 'c
                            , l1 : list('a)
                            , l2 : list('b)
-                            , acc : list('c)
                            ) : list('c) = switch ((l1, l2))
-    (h1::t1, h2::t2) => zip_with_(f, t1, t2, f(h1, h2)::acc)
-    _ => reverse(acc)
+    (h1::t1, h2::t2) => f(h1, h2)::zip_with(f, t1, t2)
+    _ => []

-/** Zips two lists into list of pairs. Drops longer tail.
+/** Zips two lists into list of pairs.
+ * Drops the tail of the longer list.
 */
  function zip(l1 : list('a), l2 : list('b)) : list('a * 'b) = zip_with((a, b) => (a, b), l1, l2)

-  function unzip(l : list('a * 'b)) : list('a) * list('b) = unzip_(l, [], [])
-  private function unzip_( l     : list('a * 'b)
-                         , acc_l : list('a)
-                         , acc_r : list('b)
-                         ) : (list('a) * list('b)) = switch(l)
-    []               => (reverse(acc_l), reverse(acc_r))
-    (left, right)::t => unzip_(t, left::acc_l, right::acc_r)
+  function unzip(l : list('a * 'b)) : (list('a) * list('b)) = switch(l)
+    []          => ([], [])
+    (h1, h2)::t =>
+      let (t1, t2) = unzip(t)
+      (h1::t1, h2::t2)


-  // TODO: Improve?
-  function sort(lesser_cmp : ('a, 'a) => bool, l : list('a)) : list('a) = switch(l)
-    []   => []
-    h::t => switch (partition((x) => lesser_cmp(x, h), t))
-      (lesser, bigger) => sort(lesser_cmp, lesser) ++ h::sort(lesser_cmp, bigger)
+  /** Merges two sorted lists using `lt` comparator
+   */
+  function
+    merge : (('a, 'a) => bool, list('a), list('a)) => list('a)
+    merge(lt, x::xs, y::ys) =
+      if(lt(x, y)) x::merge(lt, xs, y::ys)
+      else y::merge(lt, x::xs, ys)
+    merge(_, [], ys) = ys
+    merge(_, xs, []) = xs
+
+
+  /** Mergesort inspired by
+   * https://hackage.haskell.org/package/base-4.14.1.0/docs/src/Data.OldList.html#sort
+   */
+  function
+    sort : (('a, 'a) => bool, list('a)) => list('a)
+    sort(_, []) = []
+    sort(lt, l) =
+      merge_all(lt, monotonic_subs(lt, l))
+
+  /** Splits list into compound increasing sublists
+   */
+  private function
+    monotonic_subs : (('a, 'a) => bool, list('a)) => list(list('a))
+    monotonic_subs(lt, x::y::rest) =
+      if(lt(y, x)) desc(lt, y, [x], rest)
+      else asc(lt, y, [x], rest)
+    monotonic_subs(_, l) = [l]
+
+  /** Extracts the longest descending prefix and proceeds with monotonic split
+   */
+  private function
+    desc : (('a, 'a) => bool, 'a, list('a), list('a)) => list(list('a))
+    desc(lt, x, acc, h::t) =
+      if(lt(x, h)) (x::acc) :: monotonic_subs(lt, h::t)
+      else desc(lt, h, x::acc, t)
+    desc(_, x, acc, []) = [x::acc]
+
+  /** Extracts the longest ascending prefix and proceeds with monotonic split
+   */
+  private function
+    asc : (('a, 'a) => bool, 'a, list('a), list('a)) => list(list('a))
+    asc(lt, x, acc, h::t) =
+      if(lt(h, x)) List.reverse(x::acc) :: monotonic_subs(lt, h::t)
+      else asc(lt, h, x::acc, t)
+    asc(_, x, acc, []) = [List.reverse(x::acc)]
+
+  /** Merges list of sorted lists
+   */
+  private function
+    merge_all : (('a, 'a) => bool, list(list('a))) => list('a)
+    merge_all(_, [part]) = part
+    merge_all(lt, parts) = merge_all(lt, merge_pairs(lt, parts))
+
+  /** Single round of `merge_all` – pairs of lists in a list of list
+   */
+  private function
+    merge_pairs : (('a, 'a) => bool, list(list('a))) => list(list('a))
+    merge_pairs(lt, x::y::rest) = merge(lt, x, y) :: merge_pairs(lt, rest)
+    merge_pairs(_, l) = l
+

 /** Puts `delim` between every two members of the list
 */
-  function intersperse(delim : 'a, l : list('a)) : list('a) = intersperse_(delim, l, [])
-  private function intersperse_(delim : 'a, l : list('a), acc : list('a)) : list('a) = switch(l)
-    []   => reverse(acc)
-    [e]  => reverse(e::acc)
-    h::t => intersperse_(delim, t, delim::h::acc)
-
+  function intersperse(delim : 'a, l : list('a)) : list('a) = switch(l)
+    []   => []
+    [e]  => [e]
+    h::t => h::delim::intersperse(delim, t)

 /** Effectively a zip with an infinite sequence of natural numbers
 */
-  function enumerate(l : list('a)) : list(int * 'a) = enumerate_(l, 0, [])
-  private function enumerate_(l : list('a), n : int, acc : list(int * 'a)) : list(int * 'a) = switch(l)
-    []   => reverse(acc)
-    h::t => enumerate_(t, n + 1, (n, h)::acc)
-
+  function enumerate(l : list('a)) : list(int * 'a) = enumerate_(l, 0)
+  private function enumerate_(l : list('a), n : int) : list(int * 'a) = switch(l)
+    []   => []
+    h::t => (n, h)::enumerate_(t, n + 1)
@@ -22,7 +22,11 @@ namespace Option =

 /** Assume it is `Some`
 */
-  function force(o : option('a)) : 'a = default(abort("Forced None value"), o)
+  function force(o : option('a)) : 'a = switch(o)
+    None    => abort("Forced None value")
+    Some(x) => x
+
+  function contains(e : 'a, o : option('a)) = o == Some(e)

  function on_elem(o : option('a), f : 'a => unit) : unit = match((), f, o)

@@ -65,20 +69,21 @@ namespace Option =
 /** Turns list of options into a list of elements that are under `Some`s.
 * Safe.
 */
-  function filter_options(l : list(option('a))) : list('a) = filter_options_(l, [])
-  private function filter_options_(l : list (option('a)), acc : list('a)) : list('a) = switch(l)
-    []         => List.reverse(acc)
-    None::t    => filter_options_(t, acc)
-    Some(x)::t => filter_options_(t, x::acc)
+  function filter_options(l : list(option('a))) : list('a) = switch(l)
+    []         => []
+    None::t    => filter_options(t)
+    Some(x)::t => x::filter_options(t)

 /** Just like `filter_options` but requires all elements to be `Some` and returns
 * None if any of them is not
 */
-  function seq_options(l : list (option('a))) : option (list('a)) = seq_options_(l, [])
-  private function seq_options_(l : list (option('a)), acc : list('a)) : option(list('a)) = switch(l)
-    []         => Some(List.reverse(acc))
-    None::t    => None
-    Some(x)::t => seq_options_(t, x::acc)
+  function seq_options(l : list (option('a))) : option (list('a)) = switch(l)
+    []         => Some([])
+    None::_    => None
+    Some(x)::t => switch(seq_options(t))
+      None => None
+      Some(st) => Some(x::st)
+

 /** Choose `Some` out of two if possible
 */
@@ -91,4 +96,3 @@ namespace Option =
    [] => None
    None::t    => choose_first(t)
    Some(x)::_ => Some(x)
-
@@ -0,0 +1,117 @@
+include "List.aes"
+namespace String =
+  // Computes the SHA3/Keccak hash of the string
+  function sha3(s : string) : hash    = StringInternal.sha3(s)
+  // Computes the SHA256 hash of the string.
+  function sha256(s : string) : hash  = StringInternal.sha256(s)
+  // Computes the Blake2B hash of the string.
+  function blake2b(s : string) : hash = StringInternal.blake2b(s)
+
+  // The length of a string - equivalent to List.lenght(to_list(s))
+  function length(s : string) : int = StringInternal.length(s)
+  // Concatenates `s1` and `s2`.
+  function concat(s1 : string, s2 : string) : string = StringInternal.concat(s1, s2)
+  // Concatenates a list of strings.
+  function
+    concats : (list(string)) => string
+    concats([])      = ""
+    concats(s :: ss) = List.foldl(StringInternal.concat, s, ss)
+
+  // Converts a `string` to a list of `char` - the code points are normalized, but
+  // composite characters are possibly converted to multiple `char`s.
+  function from_list(cs : list(char)) : string = StringInternal.from_list(cs)
+  // Converts a list of characters into a normalized UTF-8 string.
+  function to_list(s : string) : list(char) = StringInternal.to_list(s)
+
+  // Converts a string to lowercase.
+  function to_lower(s : string) = StringInternal.to_lower(s)
+  // Converts a string to uppercase.
+  function to_upper(s : string) = StringInternal.to_upper(s)
+
+  // Splits a string at (zero-based) index `ix`.
+  function split(i : int, s : string) : string * string =
+    let cs = StringInternal.to_list(s)
+    (StringInternal.from_list(List.take(i, cs)), StringInternal.from_list(List.drop(i, cs)))
+
+  // Returns the character/codepoint at (zero-based) index `ix`.
+  function at(ix : int, s : string) =
+    switch(List.drop(ix, StringInternal.to_list(s)))
+      []     => None
+      x :: _ => Some(x)
+
+  // Searches for `pat` in `str`, returning `Some(ix)` if `pat` is a substring
+  // of `str` starting at position `ix`, otherwise returns `None`.
+  function contains(str : string, substr : string) : option(int) =
+    if(substr == "") Some(0)
+    else
+      contains_(0, StringInternal.to_list(str), StringInternal.to_list(substr))
+
+  // Splits `s` into tokens, `pat` is the divider of tokens.
+  function tokens(s : string, pat : string) =
+    require(pat != "", "String.tokens: empty pattern")
+    tokens_(StringInternal.to_list(pat), StringInternal.to_list(s), [])
+
+  // Converts a decimal ("123", "-253") or a hexadecimal ("0xa2f", "-0xBBB") string
+  // into an integer. If the string doesn't contain a valid number `None` is returned.
+  function to_int(s : string) : option(int) =
+    let s = StringInternal.to_list(s)
+    switch(is_prefix(['-'], s))
+      None    => to_int_pos(s)
+      Some(s) => switch(to_int_pos(s))
+                   None => None
+                   Some(x) => Some(-x)
+
+  // Private helper functions below
+  private function to_int_pos(s : list(char)) =
+    switch(is_prefix(['0', 'x'], s))
+      None =>
+        to_int_(s, ch_to_int_10, 0, 10)
+      Some(s) =>
+        to_int_(s, ch_to_int_16, 0, 16)
+
+  private function
+    tokens_(_, [], acc) = [StringInternal.from_list(List.reverse(acc))]
+    tokens_(pat, str, acc) =
+      switch(is_prefix(pat, str))
+        Some(str') =>
+          StringInternal.from_list(List.reverse(acc)) :: tokens_(pat, str', [])
+        None =>
+          let c :: cs = str
+          tokens_(pat, cs, c :: acc)
+
+  private function
+    contains_(_, [], _) = None
+    contains_(ix, str, substr) =
+      switch(is_prefix(substr, str))
+        None =>
+          let _ :: str = str
+          contains_(ix + 1, str, substr)
+        Some(_) =>
+          Some(ix)
+
+  private function
+    is_prefix([], ys) = Some(ys)
+    is_prefix(_, [])  = None
+    is_prefix(x :: xs, y :: ys) =
+      if(x == y) is_prefix(xs, ys)
+      else       None
+
+  private function
+    to_int_([], _, x, _) = Some(x)
+    to_int_(i :: is, value, x, b) =
+      switch(value(i))
+        None => None
+        Some(i) => to_int_(is, value, x * b + i, b)
+
+  private function ch_to_int_10(c) =
+    let c = Char.to_int(c)
+    if(c >= 48 && c =< 57) Some(c - 48)
+    else None
+
+  private function ch_to_int_16(c) =
+    let c = Char.to_int(c)
+    if(c >= 48 && c =< 57)    Some(c - 48)
+    elif(c >= 65 && c =< 70)  Some(c - 55)
+    elif(c >= 97 && c =< 102) Some(c - 87)
+    else None
+
@@ -2,7 +2,7 @@

 {erl_opts, [debug_info]}.

-{deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {ref,"4f4d6d3"}}}
+{deps, [ {aebytecode, {git, "https://github.com/aeternity/aebytecode.git", {ref,"7f0d309"}}}
       , {getopt, "1.0.1"}
       , {eblake2, "1.0.0"}
       , {jsx, {git, "https://github.com/talentdeficit/jsx.git",
@@ -15,7 +15,7 @@
            {base_plt_apps, [erts, kernel, stdlib, crypto, mnesia]}
           ]}.

-{relx, [{release, {aesophia, "4.2.0"},
+{relx, [{release, {aesophia, "5.0.0"},
         [aesophia, aebytecode, getopt]},

        {dev_mode, true},
@@ -1,7 +1,7 @@
 {"1.1.0",
 [{<<"aebytecode">>,
  {git,"https://github.com/aeternity/aebytecode.git",
-       {ref,"4f4d6d30cd2c46b3830454d650a424d513f69134"}},
+       {ref,"7f0d3090d4dc6c4d5fca7645b0c21eb0e65ad208"}},
  0},
 {<<"aeserialization">>,
  {git,"https://github.com/aeternity/aeserialization.git",
@@ -14,6 +14,8 @@
        , contract_interface/2
        , contract_interface/3

+        , from_typed_ast/2
+
        , render_aci_json/1

        , json_encode_expr/1
@@ -23,6 +25,8 @@
 -type json()      :: jsx:json_term().
 -type json_text() :: binary().

+-export_type([aci_type/0]).
+
 %% External API
 -spec file(aci_type(), string()) -> {ok, json() | string()} | {error, term()}.
 file(Type, File) ->
@@ -65,18 +69,20 @@ do_contract_interface(Type, ContractString, Options) ->
    try
        Ast = aeso_compiler:parse(ContractString, Options),
        %% io:format("~p\n", [Ast]),
-        TypedAst = aeso_ast_infer_types:infer(Ast, [dont_unfold]),
+        {TypedAst, _} = aeso_ast_infer_types:infer(Ast, [dont_unfold | Options]),
        %% io:format("~p\n", [TypedAst]),
-        JArray = [ encode_contract(C) || C <- TypedAst ],
-
-        case Type of
-            json   -> {ok, JArray};
-            string -> do_render_aci_json(JArray)
-        end
+        from_typed_ast(Type, TypedAst)
    catch
        throw:{error, Errors} -> {error, Errors}
    end.

+from_typed_ast(Type, TypedAst) ->
+    JArray = [ encode_contract(C) || C <- TypedAst ],
+    case Type of
+        json   -> {ok, JArray};
+        string -> do_render_aci_json(JArray)
+    end.
+
 encode_contract(Contract = {contract, _, {con, _, Name}, _}) ->
    C0 = #{name => encode_name(Name)},

@@ -194,6 +200,8 @@ encode_expr({bytes, _, B})  ->
 encode_expr({Lit, _, L}) when Lit == oracle_pubkey; Lit == oracle_query_id;
                              Lit == contract_pubkey; Lit == account_pubkey ->
    aeser_api_encoder:encode(Lit, L);
+encode_expr({app, _, {'-', _}, [{int, _, N}]}) ->
+  encode_expr({int, [], -N});
 encode_expr({app, _, F, As}) ->
    Ef = encode_expr(F),
    Eas = encode_exprs(As),
@@ -12,7 +12,11 @@

 -module(aeso_ast_infer_types).

-export([infer/1, infer/2, unfold_types_in_type/3]).
+-export([ infer/1
+        , infer/2
+        , unfold_types_in_type/3
+        , pp_type/2
+        ]).

 -type utype() :: {fun_t, aeso_syntax:ann(), named_args_t(), [utype()], utype()}
               | {app_t, aeso_syntax:ann(), utype(), [utype()]}
@@ -20,6 +24,7 @@
               | aeso_syntax:id()  | aeso_syntax:qid()
               | aeso_syntax:con() | aeso_syntax:qcon()  %% contracts
               | aeso_syntax:tvar()
+               | {if_t, aeso_syntax:ann(), aeso_syntax:id(), utype(), utype()}  %% Can branch on named argument (protected)
               | uvar().

 -type uvar() :: {uvar, aeso_syntax:ann(), reference()}.
@@ -43,7 +48,14 @@
     name :: aeso_syntax:id(),
     type :: utype()}).

-type named_argument_constraint() :: #named_argument_constraint{}.
+-record(dependent_type_constraint,
+    { named_args_t     :: named_args_t()
+    , named_args       :: [aeso_syntax:arg_expr()]
+    , general_type     :: utype()
+    , specialized_type :: utype()
+    , context          :: term() }).
+
+-type named_argument_constraint() :: #named_argument_constraint{} | #dependent_type_constraint{}.

 -record(field_constraint,
    { record_t :: utype()
@@ -232,16 +244,21 @@ bind_fields([], Env) -> Env;
 bind_fields([{Id, Info} | Rest], Env) ->
    bind_fields(Rest, bind_field(Id, Info, Env)).

-%% Contract entrypoints take two named arguments (gas : int = Call.gas_left(), value : int = 0).
+%% Contract entrypoints take three named arguments
+%%  gas       : int  = Call.gas_left()
+%%  value     : int  = 0
+%%  protected : bool = false
 contract_call_type({fun_t, Ann, [], Args, Ret}) ->
    Id    = fun(X) -> {id, Ann, X} end,
    Int   = Id("int"),
    Typed = fun(E, T) -> {typed, Ann, E, T} end,
-    Named = fun(Name, Default) -> {named_arg_t, Ann, Id(Name), Int, Default} end,
+    Named = fun(Name, Default = {typed, _, _, T}) -> {named_arg_t, Ann, Id(Name), T, Default} end,
    {fun_t, Ann, [Named("gas",   Typed({app, Ann, Typed({qid, Ann, ["Call", "gas_left"]},
                                                        {fun_t, Ann, [], [], Int}),
                                        []}, Int)),
-                  Named("value", Typed({int, Ann, 0}, Int))], Args, Ret}.
+                  Named("value", Typed({int, Ann, 0}, Int)),
+                  Named("protected", Typed({bool, Ann, false}, Id("bool")))],
+     Args, {if_t, Ann, Id("protected"), {app_t, Ann, {id, Ann, "option"}, [Ret]}, Ret}}.

 -spec bind_contract(aeso_syntax:decl(), env()) -> env().
 bind_contract({contract, Ann, Id, Contents}, Env) ->
@@ -364,6 +381,7 @@ is_private(Ann) -> proplists:get_value(private, Ann, false).
 global_env() ->
    Ann     = [{origin, system}],
    Int     = {id, Ann, "int"},
+    Char    = {id, Ann, "char"},
    Bool    = {id, Ann, "bool"},
    String  = {id, Ann, "string"},
    Address = {id, Ann, "address"},
@@ -389,6 +407,24 @@ global_env() ->
    Signature = {named_arg_t, Ann, SignId, SignId, {typed, Ann, SignDef, SignId}},
    SignFun   = fun(Ts, T) -> {type_sig, [stateful|Ann], none, [Signature], Ts, T} end,
    TTL       = {qid, Ann, ["Chain", "ttl"]},
+    Pointee   = {qid, Ann, ["AENS", "pointee"]},
+    AENSName  = {qid, Ann, ["AENS", "name"]},
+    Fr        = {qid, Ann, ["MCL_BLS12_381", "fr"]},
+    Fp        = {qid, Ann, ["MCL_BLS12_381", "fp"]},
+    Fp2       = {tuple_t, Ann, [Fp, Fp]},
+    G1        = {tuple_t, Ann, [Fp, Fp, Fp]},
+    G2        = {tuple_t, Ann, [Fp2, Fp2, Fp2]},
+    GT        = {tuple_t, Ann, lists:duplicate(12, Fp)},
+    Tx        = {qid, Ann, ["Chain", "tx"]},
+    GAMetaTx  = {qid, Ann, ["Chain", "ga_meta_tx"]},
+    BaseTx    = {qid, Ann, ["Chain", "base_tx"]},
+    PayForTx  = {qid, Ann, ["Chain", "paying_for_tx"]},
+
+    FldT      = fun(Id, T) -> {field_t, Ann, {id, Ann, Id}, T} end,
+    TxFlds    = [{"paying_for", Option(PayForTx)}, {"ga_metas", List(GAMetaTx)},
+                 {"actor", Address}, {"fee", Int}, {"ttl", Int}, {"tx", BaseTx}],
+    TxType    = {record_t, [FldT(N, T) || {N, T} <- TxFlds ]},
+
    Fee       = Int,
    [A, Q, R, K, V] = lists:map(TVar, ["a", "q", "r", "k", "v"]),

@@ -426,8 +462,36 @@ global_env() ->
                     {"timestamp",    Int},
                     {"block_height", Int},
                     {"difficulty",   Int},
-                     {"gas_limit",    Int}])
-        , types = MkDefs([{"ttl", 0}]) },
+                     {"gas_limit",    Int},
+                     %% Tx constructors
+                     {"GAMetaTx",     Fun([Address, Int], GAMetaTx)},
+                     {"PayingForTx",  Fun([Address, Int], PayForTx)},
+                     {"SpendTx",      Fun([Address, Int, String], BaseTx)},
+                     {"OracleRegisterTx",       BaseTx},
+                     {"OracleQueryTx",          BaseTx},
+                     {"OracleResponseTx",       BaseTx},
+                     {"OracleExtendTx",         BaseTx},
+                     {"NamePreclaimTx",         BaseTx},
+                     {"NameClaimTx",            Fun([String], BaseTx)},
+                     {"NameUpdateTx",           Fun([Hash], BaseTx)},
+                     {"NameRevokeTx",           Fun([Hash], BaseTx)},
+                     {"NameTransferTx",         Fun([Address, Hash], BaseTx)},
+                     {"ChannelCreateTx",        Fun([Address], BaseTx)},
+                     {"ChannelDepositTx",       Fun([Address, Int], BaseTx)},
+                     {"ChannelWithdrawTx",      Fun([Address, Int], BaseTx)},
+                     {"ChannelForceProgressTx", Fun([Address], BaseTx)},
+                     {"ChannelCloseMutualTx",   Fun([Address], BaseTx)},
+                     {"ChannelCloseSoloTx",     Fun([Address], BaseTx)},
+                     {"ChannelSlashTx",         Fun([Address], BaseTx)},
+                     {"ChannelSettleTx",        Fun([Address], BaseTx)},
+                     {"ChannelSnapshotSoloTx",  Fun([Address], BaseTx)},
+                     {"ContractCreateTx",       Fun([Int], BaseTx)},
+                     {"ContractCallTx",         Fun([Address, Int], BaseTx)},
+                     {"GAAttachTx",             BaseTx}
+                    ])
+        , types = MkDefs([{"ttl", 0}, {"tx", {[], TxType}},
+                          {"base_tx", 0},
+                          {"paying_for_tx", 0}, {"ga_meta_tx", 0}]) },

    ContractScope = #scope
        { funs = MkDefs(
@@ -447,6 +511,7 @@ global_env() ->
    OracleScope = #scope
        { funs = MkDefs(
                    [{"register",     SignFun([Address, Fee, TTL], Oracle(Q, R))},
+                     {"expiry",       Fun([Oracle(Q, R)], Fee)},
                     {"query_fee",    Fun([Oracle(Q, R)], Fee)},
                     {"query",        StateFun([Oracle(Q, R), Q, Fee, TTL, TTL], Query(Q, R))},
                     {"get_question", Fun([Oracle(Q, R), Query(Q, R)], Q)},
@@ -462,7 +527,18 @@ global_env() ->
                      {"preclaim", SignFun([Address, Hash], Unit)},
                      {"claim",    SignFun([Address, String, Int, Int], Unit)},
                      {"transfer", SignFun([Address, Address, String], Unit)},
-                      {"revoke",   SignFun([Address, String], Unit)}]) },
+                      {"revoke",   SignFun([Address, String], Unit)},
+                      {"update",   SignFun([Address, String, Option(TTL), Option(Int), Option(Map(String, Pointee))], Unit)},
+                      {"lookup",   Fun([String], option_t(Ann, AENSName))},
+                      %% AENS pointee constructors
+                      {"AccountPt",  Fun1(Address, Pointee)},
+                      {"OraclePt",   Fun1(Address, Pointee)},
+                      {"ContractPt", Fun1(Address, Pointee)},
+                      {"ChannelPt",  Fun1(Address, Pointee)},
+                      %% Name object constructor
+                      {"Name",   Fun([Address, TTL, Map(String, Pointee)], AENSName)}
+                     ])
+        , types = MkDefs([{"pointee", 0}, {"name", 0}]) },

    MapScope = #scope
        { funs = MkDefs(
@@ -485,19 +561,65 @@ global_env() ->
                      {"sha256",   Fun1(A, Hash)},
                      {"blake2b",  Fun1(A, Hash)}]) },

+    %% Fancy BLS12-381 crypto operations
+    MCL_BLS12_381_Scope = #scope
+        { funs = MkDefs(
+                     [{"g1_neg",     Fun1(G1, G1)},
+                      {"g1_norm",    Fun1(G1, G1)},
+                      {"g1_valid",   Fun1(G1, Bool)},
+                      {"g1_is_zero", Fun1(G1, Bool)},
+                      {"g1_add",     Fun ([G1, G1], G1)},
+                      {"g1_mul",     Fun ([Fr, G1], G1)},
+
+                      {"g2_neg",     Fun1(G2, G2)},
+                      {"g2_norm",    Fun1(G2, G2)},
+                      {"g2_valid",   Fun1(G2, Bool)},
+                      {"g2_is_zero", Fun1(G2, Bool)},
+                      {"g2_add",     Fun ([G2, G2], G2)},
+                      {"g2_mul",     Fun ([Fr, G2], G2)},
+
+                      {"gt_inv",      Fun1(GT, GT)},
+                      {"gt_add",      Fun ([GT, GT], GT)},
+                      {"gt_mul",      Fun ([GT, GT], GT)},
+                      {"gt_pow",      Fun ([GT, Fr], GT)},
+                      {"gt_is_one",   Fun1(GT, Bool)},
+                      {"pairing",     Fun ([G1, G2], GT)},
+                      {"miller_loop", Fun ([G1, G2], GT)},
+                      {"final_exp",   Fun1(GT, GT)},
+
+                      {"int_to_fr", Fun1(Int, Fr)},
+                      {"int_to_fp", Fun1(Int, Fp)},
+                      {"fr_to_int", Fun1(Fr, Int)},
+                      {"fp_to_int", Fun1(Fp, Int)}
+                     ]),
+          types = MkDefs(
+                     [{"fr",  0}, {"fp",  0}]) },
+
    %% Authentication
    AuthScope = #scope
        { funs = MkDefs(
-                     [{"tx_hash", Option(Hash)}]) },
+                     [{"tx_hash", Option(Hash)},
+                      {"tx",      Option(Tx)}  ]) },

    %% Strings
    StringScope = #scope
        { funs = MkDefs(
-                     [{"length",  Fun1(String, Int)},
-                      {"concat",  Fun([String, String], String)},
-                      {"sha3",    Fun1(String, Hash)},
-                      {"sha256",  Fun1(String, Hash)},
-                      {"blake2b", Fun1(String, Hash)}]) },
+                     [{"length",    Fun1(String, Int)},
+                      {"concat",    Fun([String, String], String)},
+                      {"to_list",   Fun1(String, List(Char))},
+                      {"from_list", Fun1(List(Char), String)},
+                      {"to_upper",  Fun1(String, String)},
+                      {"to_lower",  Fun1(String, String)},
+                      {"sha3",      Fun1(String, Hash)},
+                      {"sha256",    Fun1(String, Hash)},
+                      {"blake2b",   Fun1(String, Hash)}
+                     ]) },
+
+    %% Chars
+    CharScope = #scope
+        { funs = MkDefs(
+                     [{"to_int",   Fun1(Char, Int)},
+                      {"from_int", Fun1(Int, Option(Char))}]) },

    %% Bits
    BitsScope = #scope
@@ -529,6 +651,7 @@ global_env() ->
                                          {"is_contract", Fun1(Address, Bool)},
                                          {"is_payable", Fun1(Address, Bool)}]) },

+
    #env{ scopes =
            #{ []           => TopScope
             , ["Chain"]    => ChainScope
@@ -539,27 +662,38 @@ global_env() ->
             , ["Map"]      => MapScope
             , ["Auth"]     => AuthScope
             , ["Crypto"]   => CryptoScope
-             , ["String"]   => StringScope
+             , ["MCL_BLS12_381"] => MCL_BLS12_381_Scope
+             , ["StringInternal"] => StringScope
+             , ["Char"]     => CharScope
             , ["Bits"]     => BitsScope
             , ["Bytes"]    => BytesScope
             , ["Int"]      => IntScope
             , ["Address"]  => AddressScope
-             } }.
+             }
+          , fields =
+             maps:from_list([{N, [#field_info{ ann = [], field_t = T, record_t = Tx, kind = record }]}
+                             || {N, T} <- TxFlds ])
+        }.
+

 option_t(As, T) -> {app_t, As, {id, As, "option"}, [T]}.
 map_t(As, K, V) -> {app_t, As, {id, As, "map"}, [K, V]}.

-spec infer(aeso_syntax:ast()) -> aeso_syntax:ast() | {env(), aeso_syntax:ast()}.
+-spec infer(aeso_syntax:ast()) -> {aeso_syntax:ast(), aeso_syntax:ast()} | {env(), aeso_syntax:ast(), aeso_syntax:ast()}.
 infer(Contracts) ->
    infer(Contracts, []).

-type option() :: return_env | dont_unfold | no_code | term().
+-type option() :: return_env | dont_unfold | no_code | debug_mode | term().

 -spec init_env(list(option())) -> env().
 init_env(_Options) -> global_env().

 -spec infer(aeso_syntax:ast(), list(option())) ->
-    aeso_syntax:ast() | {env(), aeso_syntax:ast()}.
+  {aeso_syntax:ast(), aeso_syntax:ast()} | {env(), aeso_syntax:ast(), aeso_syntax:ast()}.
+infer([], Options) ->
+    create_type_errors(),
+    type_error({no_decls, proplists:get_value(src_file, Options, no_file)}),
+    destroy_and_report_type_errors(init_env(Options));
 infer(Contracts, Options) ->
    ets_init(), %% Init the ETS table state
    try
@@ -568,15 +702,15 @@ infer(Contracts, Options) ->
        ets_new(type_vars, [set]),
        check_modifiers(Env, Contracts),
        {Env1, Decls} = infer1(Env, Contracts, [], Options),
-        {Env2, Decls2} =
+        {Env2, DeclsFolded, DeclsUnfolded} =
            case proplists:get_value(dont_unfold, Options, false) of
-                true  -> {Env1, Decls};
+                true  -> {Env1, Decls, Decls};
                false -> E = on_scopes(Env1, fun(Scope) -> unfold_record_types(Env1, Scope) end),
-                         {E, unfold_record_types(E, Decls)}
+                         {E, Decls, unfold_record_types(E, Decls)}
            end,
        case proplists:get_value(return_env, Options, false) of
-            false -> Decls2;
-            true  -> {Env2, Decls2}
+            false -> {DeclsFolded, DeclsUnfolded};
+            true  -> {Env2, DeclsFolded, DeclsUnfolded}
        end
    after
        clean_up_ets()
@@ -614,15 +748,23 @@ check_scope_name_clash(Env, Kind, Name) ->

 -spec infer_contract_top(env(), main_contract | contract | namespace, [aeso_syntax:decl()], list(option())) ->
    {env(), [aeso_syntax:decl()]}.
-infer_contract_top(Env, Kind, Defs0, _Options) ->
+infer_contract_top(Env, Kind, Defs0, Options) ->
+    create_type_errors(),
    Defs = desugar(Defs0),
-    infer_contract(Env, Kind, Defs).
+    destroy_and_report_type_errors(Env),
+    infer_contract(Env, Kind, Defs, Options).

 %% infer_contract takes a proplist mapping global names to types, and
 %% a list of definitions.
-spec infer_contract(env(), main_contract | contract | namespace, [aeso_syntax:decl()]) -> {env(), [aeso_syntax:decl()]}.
-infer_contract(Env0, What, Defs0) ->
-    Defs = process_blocks(Defs0),
+-spec infer_contract(env(), main_contract | contract | namespace, [aeso_syntax:decl()], list(option())) -> {env(), [aeso_syntax:decl()]}.
+infer_contract(Env0, What, Defs0, Options) ->
+    create_type_errors(),
+    Defs01 = process_blocks(Defs0),
+    Defs = case lists:member(debug_mode, Options) of
+               true  -> expose_internals(Defs01, What);
+               false -> Defs01
+           end,
+    destroy_and_report_type_errors(Env0),
    Env  = Env0#env{ what = What },
    Kind = fun({type_def, _, _, _, _})    -> type;
              ({letfun, _, _, _, _, _})   -> function;
@@ -669,20 +811,39 @@ process_blocks(Decls) ->
 -spec process_block(aeso_syntax:ann(), [aeso_syntax:decl()]) -> [aeso_syntax:decl()].
 process_block(_, []) -> [];
 process_block(_, [Decl]) -> [Decl];
-process_block(Ann, [Decl | Decls]) ->
+process_block(_Ann, [Decl | Decls]) ->
    IsThis = fun(Name) -> fun({letfun, _, {id, _, Name1}, _, _, _}) -> Name == Name1;
                             (_) -> false end end,
    case Decl of
        {fun_decl, Ann1, Id = {id, _, Name}, Type} ->
            {Clauses, Rest} = lists:splitwith(IsThis(Name), Decls),
-            [{fun_clauses, Ann1, Id, Type, Clauses} |
-             process_block(Ann, Rest)];
+            [type_error({mismatched_decl_in_funblock, Name, D1}) || D1 <- Rest],
+            [{fun_clauses, Ann1, Id, Type, Clauses}];
        {letfun, Ann1, Id = {id, _, Name}, _, _, _} ->
            {Clauses, Rest} = lists:splitwith(IsThis(Name), [Decl | Decls]),
-            [{fun_clauses, Ann1, Id, {id, [{origin, system} | Ann1], "_"}, Clauses} |
-             process_block(Ann, Rest)]
+            [type_error({mismatched_decl_in_funblock, Name, D1}) || D1 <- Rest],
+            [{fun_clauses, Ann1, Id, {id, [{origin, system} | Ann1], "_"}, Clauses}]
    end.

+%% Turns private stuff into public stuff
+expose_internals(Defs, What) ->
+    [ begin
+          Ann = element(2, Def),
+          NewAnn = case What of
+                       namespace -> [A ||A <- Ann, A /= {private, true}, A /= private];
+                       main_contract -> [{entrypoint, true}|Ann];  % minor duplication
+                       contract -> Ann
+                   end,
+          Def1 = setelement(2, Def, NewAnn),
+          case Def1 of  % fix inner clauses
+              {fun_clauses, Ans, Id, T, Clauses} ->
+                  {fun_clauses, Ans, Id, T, expose_internals(Clauses, What)};
+              _ -> Def1
+          end
+      end
+     || Def <- Defs
+    ].
+
 -spec check_typedefs(env(), [aeso_syntax:decl()]) -> {env(), [aeso_syntax:decl()]}.
 check_typedefs(Env = #env{ namespace = Ns }, Defs) ->
    create_type_errors(),
@@ -1246,7 +1407,7 @@ infer_expr(Env, {typed, As, Body, Type}) ->
    Type1 = check_type(Env, Type),
    {typed, _, NewBody, NewType} = check_expr(Env, Body, Type1),
    {typed, As, NewBody, NewType};
-infer_expr(Env, {app, Ann, Fun, Args0}) ->
+infer_expr(Env, {app, Ann, Fun, Args0} = App) ->
    NamedArgs  = [ Arg || Arg = {named_arg, _, _, _} <- Args0 ],
    Args       = Args0 -- NamedArgs,
    case aeso_syntax:get_ann(format, Ann) of
@@ -1261,8 +1422,16 @@ infer_expr(Env, {app, Ann, Fun, Args0}) ->
            NewFun={typed, _, _, FunType} = infer_expr(Env, Fun),
            NewArgs = [infer_expr(Env, A) || A <- Args],
            ArgTypes = [T || {typed, _, _, T} <- NewArgs],
+            GeneralResultType = fresh_uvar(Ann),
            ResultType = fresh_uvar(Ann),
-            unify(Env, FunType, {fun_t, [], NamedArgsVar, ArgTypes, ResultType}, {infer_app, Fun, Args, FunType, ArgTypes}),
+            When = {infer_app, Fun, NamedArgs1, Args, FunType, ArgTypes},
+            unify(Env, FunType, {fun_t, [], NamedArgsVar, ArgTypes, GeneralResultType}, When),
+            add_named_argument_constraint(
+              #dependent_type_constraint{ named_args_t = NamedArgsVar,
+                                          named_args   = NamedArgs1,
+                                          general_type = GeneralResultType,
+                                          specialized_type = ResultType,
+                                          context = {check_return, App} }),
            {typed, Ann, {app, Ann, NewFun, NamedArgs1 ++ NewArgs}, dereference(ResultType)}
    end;
 infer_expr(Env, {'if', Attrs, Cond, Then, Else}) ->
@@ -1421,7 +1590,7 @@ infer_op(Env, As, Op, Args, InferOp) ->
    TypedArgs = [infer_expr(Env, A) || A <- Args],
    ArgTypes = [T || {typed, _, _, T} <- TypedArgs],
    Inferred = {fun_t, _, _, OperandTypes, ResultType} = InferOp(Op),
-    unify(Env, ArgTypes, OperandTypes, {infer_app, Op, Args, Inferred, ArgTypes}),
+    unify(Env, ArgTypes, OperandTypes, {infer_app, Op, [], Args, Inferred, ArgTypes}),
    {typed, As, {app, As, Op, TypedArgs}, ResultType}.

 infer_pattern(Env, Pattern) ->
@@ -1522,6 +1691,15 @@ free_vars(L) when is_list(L) ->
    [V || Elem <- L,
          V <- free_vars(Elem)].

+next_count() ->
+    V = case get(counter) of
+            undefined ->
+                0;
+            X -> X
+        end,
+    put(counter, V + 1),
+    V.
+
 %% Clean up all the ets tables (in case of an exception)

 ets_tables() ->
@@ -1567,6 +1745,18 @@ ets_tab2list(Name) ->
    TabId = ets_tabid(Name),
    ets:tab2list(TabId).

+ets_insert_ordered(_, []) -> true;
+ets_insert_ordered(Name, [H|T]) ->
+    ets_insert_ordered(Name, H),
+    ets_insert_ordered(Name, T);
+ets_insert_ordered(Name, Object) ->
+    Count = next_count(),
+    TabId = ets_tabid(Name),
+    ets:insert(TabId, {Count, Object}).
+
+ets_tab2list_ordered(Name) ->
+    [E || {_, E} <- ets_tab2list(Name)].
+
 %% Options

 create_options(Options) ->
@@ -1592,27 +1782,27 @@ create_constraints() ->
    create_field_constraints().

 destroy_and_report_unsolved_constraints(Env) ->
+    solve_field_constraints(Env),
    solve_named_argument_constraints(Env),
    solve_bytes_constraints(Env),
-    solve_field_constraints(Env),
-    destroy_and_report_unsolved_field_constraints(Env),
    destroy_and_report_unsolved_bytes_constraints(Env),
-    destroy_and_report_unsolved_named_argument_constraints(Env).
+    destroy_and_report_unsolved_named_argument_constraints(Env),
+    destroy_and_report_unsolved_field_constraints(Env).

 %% -- Named argument constraints --

 create_named_argument_constraints() ->
-    ets_new(named_argument_constraints, [bag]).
+    ets_new(named_argument_constraints, [ordered_set]).

 destroy_named_argument_constraints() ->
    ets_delete(named_argument_constraints).

 get_named_argument_constraints() ->
-    ets_tab2list(named_argument_constraints).
+    ets_tab2list_ordered(named_argument_constraints).

 -spec add_named_argument_constraint(named_argument_constraint()) -> ok.
 add_named_argument_constraint(Constraint) ->
-    ets_insert(named_argument_constraints, Constraint),
+    ets_insert_ordered(named_argument_constraints, Constraint),
    ok.

 solve_named_argument_constraints(Env) ->
@@ -1637,8 +1827,43 @@ check_named_argument_constraint(Env,
            type_error({bad_named_argument, Args, Id}),
            false;
        [T] -> unify(Env, T, Type, {check_named_arg_constraint, C}), true
+    end;
+check_named_argument_constraint(Env,
+        #dependent_type_constraint{ named_args_t = NamedArgsT0,
+                                    named_args = NamedArgs,
+                                    general_type = GenType,
+                                    specialized_type = SpecType,
+                                    context = {check_return, App} }) ->
+    NamedArgsT = dereference(NamedArgsT0),
+    case dereference(NamedArgsT0) of
+        [_ | _] = NamedArgsT ->
+            GetVal = fun(Name, Default) ->
+                        hd([ Val || {named_arg, _, {id, _, N}, Val} <- NamedArgs, N == Name] ++
+                           [ Default ])
+                     end,
+            ArgEnv = maps:from_list([ {Name, GetVal(Name, Default)}
+                                      || {named_arg_t, _, {id, _, Name}, _, Default} <- NamedArgsT ]),
+            GenType1 = specialize_dependent_type(ArgEnv, GenType),
+            unify(Env, GenType1, SpecType, {check_expr, App, GenType1, SpecType}),
+            true;
+        _ -> unify(Env, GenType, SpecType, {check_expr, App, GenType, SpecType}), true
    end.

+specialize_dependent_type(Env, Type) ->
+    case dereference(Type) of
+        {if_t, _, {id, _, Arg}, Then, Else} ->
+            Val = maps:get(Arg, Env),
+            case Val of
+                {typed, _, {bool, _, true}, _}  -> Then;
+                {typed, _, {bool, _, false}, _} -> Else;
+                _ ->
+                    type_error({named_argument_must_be_literal_bool, Arg, Val}),
+                    fresh_uvar(aeso_syntax:get_ann(Val))
+            end;
+        _ -> Type   %% Currently no deep dependent types
+    end.
+
+
 destroy_and_report_unsolved_named_argument_constraints(Env) ->
    Unsolved = solve_named_argument_constraints(Env, get_named_argument_constraints()),
    [ type_error({unsolved_named_argument_constraint, C}) || C <- Unsolved ],
@@ -1651,14 +1876,14 @@ destroy_and_report_unsolved_named_argument_constraints(Env) ->
                         | {add_bytes, aeso_syntax:ann(), concat | split, utype(), utype(), utype()}.

 create_bytes_constraints() ->
-    ets_new(bytes_constraints, [bag]).
+    ets_new(bytes_constraints, [ordered_set]).

 get_bytes_constraints() ->
-    ets_tab2list(bytes_constraints).
+    ets_tab2list_ordered(bytes_constraints).

 -spec add_bytes_constraint(byte_constraint()) -> true.
 add_bytes_constraint(Constraint) ->
-    ets_insert(bytes_constraints, Constraint).
+    ets_insert_ordered(bytes_constraints, Constraint).

 solve_bytes_constraints(Env) ->
    [ solve_bytes_constraint(Env, C) || C <- get_bytes_constraints() ],
@@ -1712,18 +1937,18 @@ check_bytes_constraint(Env, {add_bytes, Ann, Fun, A0, B0, C0}) ->

 create_field_constraints() ->
    %% A relation from uvars to constraints
-    ets_new(field_constraints, [bag]).
+    ets_new(field_constraints, [ordered_set]).

 destroy_field_constraints() ->
    ets_delete(field_constraints).

 -spec constrain([field_constraint()]) -> true.
 constrain(FieldConstraints) ->
-    ets_insert(field_constraints, FieldConstraints).
+    ets_insert_ordered(field_constraints, FieldConstraints).

 -spec get_field_constraints() -> [field_constraint()].
 get_field_constraints() ->
-    ets_tab2list(field_constraints).
+    ets_tab2list_ordered(field_constraints).

 solve_field_constraints(Env) ->
    FieldCs =
@@ -1864,9 +2089,11 @@ destroy_and_report_unsolved_field_constraints(Env) ->
    {FieldCs, OtherCs} =
        lists:partition(fun(#field_constraint{}) -> true; (_) -> false end,
                        get_field_constraints()),
-    {CreateCs, ContractCs} =
+    {CreateCs, OtherCs1} =
        lists:partition(fun(#record_create_constraint{}) -> true; (_) -> false end,
                        OtherCs),
+    {ContractCs, []} =
+        lists:partition(fun(#is_contract_constraint{}) -> true; (_) -> false end, OtherCs1),
    Unknown  = solve_known_record_types(Env, FieldCs),
    if Unknown == [] -> ok;
       true ->
@@ -1940,7 +2167,8 @@ unfold_record_types(Env, T) ->
    unfold_types(Env, T, [unfold_record_types]).

 unfold_types(Env, {typed, Attr, E, Type}, Options) ->
-    {typed, Attr, unfold_types(Env, E, Options), unfold_types_in_type(Env, Type, Options)};
+    Options1 = [{ann, Attr} | lists:keydelete(ann, 1, Options)],
+    {typed, Attr, unfold_types(Env, E, Options), unfold_types_in_type(Env, Type, Options1)};
 unfold_types(Env, {arg, Attr, Id, Type}, Options) ->
    {arg, Attr, Id, unfold_types_in_type(Env, Type, Options)};
 unfold_types(Env, {type_sig, Ann, Constr, NamedArgs, Args, Ret}, Options) ->
@@ -1966,7 +2194,8 @@ unfold_types_in_type(Env, T) ->

 unfold_types_in_type(Env, {app_t, Ann, Id = {id, _, "map"}, Args = [KeyType0, _]}, Options) ->
    Args1 = [KeyType, _] = unfold_types_in_type(Env, Args, Options),
-    [ type_error({map_in_map_key, KeyType0}) || has_maps(KeyType) ],
+    Ann1 = proplists:get_value(ann, Options, aeso_syntax:get_ann(KeyType0)),
+    [ type_error({map_in_map_key, Ann1, KeyType0}) || has_maps(KeyType) ],
    {app_t, Ann, Id, Args1};
 unfold_types_in_type(Env, {app_t, Ann, Id, Args}, Options) when ?is_type_id(Id) ->
    UnfoldRecords  = proplists:get_value(unfold_record_types, Options, false),
@@ -2040,8 +2269,13 @@ subst_tvars1(_Env, X) ->
 unify(_, {id, _, "_"}, _, _When) -> true;
 unify(_, _, {id, _, "_"}, _When) -> true;
 unify(Env, A, B, When) ->
-    A1 = dereference(unfold_types_in_type(Env, A)),
-    B1 = dereference(unfold_types_in_type(Env, B)),
+    Options =
+        case When of    %% Improve source location for map_in_map_key errors
+            {check_expr, E, _, _} -> [{ann, aeso_syntax:get_ann(E)}];
+            _                     -> []
+        end,
+    A1 = dereference(unfold_types_in_type(Env, A, Options)),
+    B1 = dereference(unfold_types_in_type(Env, B, Options)),
    unify1(Env, A1, B1, When).

 unify1(_Env, {uvar, _, R}, {uvar, _, R}, _When) ->
@@ -2072,6 +2306,9 @@ unify1(_Env, {qcon, _, Name}, {qcon, _, Name}, _When) ->
    true;
 unify1(_Env, {bytes_t, _, Len}, {bytes_t, _, Len}, _When) ->
    true;
+unify1(Env, {if_t, _, {id, _, Id}, Then1, Else1}, {if_t, _, {id, _, Id}, Then2, Else2}, When) ->
+    unify(Env, Then1, Then2, When) andalso
+    unify(Env, Else1, Else2, When);
 unify1(Env, {fun_t, _, Named1, Args1, Result1}, {fun_t, _, Named2, Args2, Result2}, When)
    when length(Args1) == length(Args2) ->
    unify(Env, Named1, Named2, When) andalso
@@ -2133,6 +2370,8 @@ occurs_check1(R, {record_t, Fields}) ->
    occurs_check(R, Fields);
 occurs_check1(R, {field_t, _, _, T}) ->
    occurs_check(R, T);
+occurs_check1(R, {if_t, _, _, Then, Else}) ->
+    occurs_check(R, [Then, Else]);
 occurs_check1(R, [H | T]) ->
    occurs_check(R, H) orelse occurs_check(R, T);
 occurs_check1(_, []) -> false.
@@ -2262,6 +2501,30 @@ mk_t_err(Pos, Msg) ->
 mk_t_err(Pos, Msg, Ctxt) ->
    aeso_errors:new(type_error, Pos, lists:flatten(Msg), lists:flatten(Ctxt)).

+mk_error({no_decls, File}) ->
+    Pos = aeso_errors:pos(File, 0, 0),
+    mk_t_err(Pos, "Empty contract\n");
+mk_error({mismatched_decl_in_funblock, Name, Decl}) ->
+    Msg = io_lib:format("Mismatch in the function block. Expected implementation/type declaration of ~s function\n", [Name]),
+    mk_t_err(pos(Decl), Msg);
+mk_error({higher_kinded_typevar, T}) ->
+    Msg = io_lib:format("Type ~s is a higher kinded type variable\n"
+                        "(takes another type as an argument)\n", [pp(instantiate(T))]
+                       ),
+    mk_t_err(pos(T), Msg);
+mk_error({wrong_type_arguments, X, ArityGiven, ArityReal}) ->
+    Msg = io_lib:format("Arity for ~s doesn't match. Expected ~p, got ~p\n"
+                       , [pp(instantiate(X)), ArityReal, ArityGiven]
+                       ),
+    mk_t_err(pos(X), Msg);
+mk_error({unnamed_map_update_with_default, Upd}) ->
+    Msg = "Invalid map update with default\n",
+    mk_t_err(pos(Upd), Msg);
+mk_error({fundecl_must_have_funtype, _Ann, Id, Type}) ->
+    Msg = io_lib:format("~s at ~s was declared with an invalid type ~s.\n"
+                       "Entrypoints and functions must have functional types"
+                       , [pp(Id), pp_loc(Id), pp(instantiate(Type))]),
+    mk_t_err(pos(Id), Msg);
 mk_error({cannot_unify, A, B, When}) ->
    Msg = io_lib:format("Cannot unify ~s\n         and ~s\n",
                        [pp(instantiate(A)), pp(instantiate(B))]),
@@ -2344,14 +2607,6 @@ mk_error({indexed_type_must_be_word, Type, Type1}) ->
    Msg = io_lib:format("The indexed type ~s (at ~s) equals ~s which is not a word type\n",
                        [pp_type("", Type), pp_loc(Type), pp_type("", Type1)]),
    mk_t_err(pos(Type), Msg);
-mk_error({payload_type_must_be_string, Type, Type}) ->
-    Msg = io_lib:format("The payload type ~s (at ~s) should be string\n",
-                        [pp_type("", Type), pp_loc(Type)]),
-    mk_t_err(pos(Type), Msg);
-mk_error({payload_type_must_be_string, Type, Type1}) ->
-    Msg = io_lib:format("The payload type ~s (at ~s) equals ~s but it should be string\n",
-                        [pp_type("", Type), pp_loc(Type), pp_type("", Type1)]),
-    mk_t_err(pos(Type), Msg);
 mk_error({event_0_to_3_indexed_values, Constr}) ->
    Msg = io_lib:format("The event constructor ~s (at ~s) has too many indexed values (max 3)\n",
                        [name(Constr), pp_loc(Constr)]),
@@ -2395,13 +2650,21 @@ mk_error({include, _, {string, Pos, Name}}) ->
                        [binary_to_list(Name), pp_loc(Pos)]),
    mk_t_err(pos(Pos), Msg);
 mk_error({namespace, _Pos, {con, Pos, Name}, _Def}) ->
-    Msg = io_lib:format("Nested namespace not allowed\nNamespace '~s' at ~s not defined at top level.\n",
+    Msg = io_lib:format("Nested namespaces are not allowed\nNamespace '~s' at ~s not defined at top level.\n",
+                        [Name, pp_loc(Pos)]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({contract, _Pos, {con, Pos, Name}, _Def}) ->
+    Msg = io_lib:format("Nested contracts are not allowed\nContract '~s' at ~s not defined at top level.\n",
+                        [Name, pp_loc(Pos)]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({type_decl, _, {id, Pos, Name}, _}) ->
+    Msg = io_lib:format("Empty type declarations are not supported\nType ~s at ~s lacks a definition\n",
+                        [Name, pp_loc(Pos)]),
+    mk_t_err(pos(Pos), Msg);
+mk_error({letval, _Pos, {id, Pos, Name}, _Def}) ->
+    Msg = io_lib:format("Toplevel \"let\" definitions are not supported\nValue ~s at ~s could be replaced by 0-argument function\n",
                        [Name, pp_loc(Pos)]),
    mk_t_err(pos(Pos), Msg);
-mk_error({repeated_arg, Fun, Arg}) ->
-    Msg = io_lib:format("Repeated argument ~s to function ~s (at ~s).\n",
-                        [Arg, pp(Fun), pp_loc(Fun)]),
-    mk_t_err(pos(Fun), Msg);
 mk_error({stateful_not_allowed, Id, Fun}) ->
    Msg = io_lib:format("Cannot reference stateful function ~s (at ~s)\nin the definition of non-stateful function ~s.\n",
                        [pp(Id), pp_loc(Id), pp(Fun)]),
@@ -2476,10 +2739,10 @@ mk_error({new_tuple_syntax, Ann, Ts}) ->
    Msg = io_lib:format("Invalid type\n~s  (at ~s)\nThe syntax of tuple types changed in Sophia version 4.0. Did you mean\n~s\n",
                        [pp_type("  ", {args_t, Ann, Ts}), pp_loc(Ann), pp_type("  ", {tuple_t, Ann, Ts})]),
    mk_t_err(pos(Ann), Msg);
-mk_error({map_in_map_key, KeyType}) ->
+mk_error({map_in_map_key, Ann, KeyType}) ->
    Msg = io_lib:format("Invalid key type\n~s\n", [pp_type("  ", KeyType)]),
    Cxt = "Map keys cannot contain other maps.\n",
-    mk_t_err(pos(KeyType), Msg, Cxt);
+    mk_t_err(pos(Ann), Msg, Cxt);
 mk_error({cannot_call_init_function, Ann}) ->
    Msg = "The 'init' function is called exclusively by the create contract transaction\n"
          "and cannot be called from the contract code.\n",
@@ -2529,6 +2792,12 @@ mk_error({mixed_record_and_map, Expr}) ->
    Msg = io_lib:format("Mixed record fields and map keys in\n~s",
                        [pp_expr("  ", Expr)]),
    mk_t_err(pos(Expr), Msg);
+mk_error({named_argument_must_be_literal_bool, Name, Arg}) ->
+    Msg = io_lib:format("Invalid '~s' argument\n~s\nIt must be either 'true' or 'false'.", [Name, pp_expr("  ", instantiate(Arg))]),
+    mk_t_err(pos(Arg), Msg);
+mk_error({conflicting_updates_for_field, Upd, Key}) ->
+    Msg = io_lib:format("Conflicting updates for field '~s'\n", [Key]),
+    mk_t_err(pos(Upd), Msg);
 mk_error(Err) ->
    Msg = io_lib:format("Unknown error: ~p\n", [Err]),
    mk_t_err(pos(0, 0), Msg).
@@ -2547,7 +2816,7 @@ pp_when({check_typesig, Name, Inferred, Given}) ->
                   "  inferred type: ~s\n"
                   "  given type:    ~s\n",
         [Name, pp_loc(Given), pp(instantiate(Inferred)), pp(instantiate(Given))])};
-pp_when({infer_app, Fun, Args, Inferred0, ArgTypes0}) ->
+pp_when({infer_app, Fun, NamedArgs, Args, Inferred0, ArgTypes0}) ->
    Inferred = instantiate(Inferred0),
    ArgTypes = instantiate(ArgTypes0),
    {pos(Fun),
@@ -2556,6 +2825,7 @@ pp_when({infer_app, Fun, Args, Inferred0, ArgTypes0}) ->
                   "to arguments\n~s",
                   [pp_loc(Fun),
                    pp_typed("  ", Fun, Inferred),
+                    [ [pp_expr("  ", NamedArg), "\n"] || NamedArg <- NamedArgs ] ++
                    [ [pp_typed("  ", Arg, ArgT), "\n"]
                       || {Arg, ArgT} <- lists:zip(Args, ArgTypes) ] ])};
 pp_when({field_constraint, FieldType0, InferredType0, Fld}) ->
@@ -2632,6 +2902,12 @@ pp_when({list_comp, BindExpr, Inferred0, Expected0}) ->
     io_lib:format("when checking rvalue of list comprehension binding at ~s\n~s\n"
                   "against type \n~s\n",
                   [pp_loc(BindExpr), pp_typed("  ", BindExpr, Inferred), pp_type("  ", Expected)])};
+pp_when({check_named_arg_constraint, C}) ->
+    {id, _, Name} = Arg = C#named_argument_constraint.name,
+    [Type | _] = [ Type || {named_arg_t, _, {id, _, Name1}, Type, _} <- C#named_argument_constraint.args, Name1 == Name ],
+    Err = io_lib:format("when checking named argument\n~s\nagainst inferred type\n~s",
+                        [pp_typed("  ", Arg, Type), pp_type("  ", C#named_argument_constraint.type)]),
+    {pos(Arg), Err};
 pp_when(unknown) -> {pos(0,0), ""}.

 -spec pp_why_record(why_record()) -> {pos(), iolist()}.
@@ -2709,6 +2985,8 @@ pp({uvar, _, Ref}) ->
    ["?u" | integer_to_list(erlang:phash2(Ref, 16384)) ];
 pp({tvar, _, Name}) ->
    Name;
+pp({if_t, _, Id, Then, Else}) ->
+    ["if(", pp([Id, Then, Else]), ")"];
 pp({tuple_t, _, []}) ->
    "unit";
 pp({tuple_t, _, Cpts}) ->
@@ -2720,8 +2998,8 @@ pp({app_t, _, T, []}) ->
    pp(T);
 pp({app_t, _, Type, Args}) ->
    [pp(Type), "(", pp(Args), ")"];
-pp({named_arg_t, _, Name, Type, Default}) ->
-    [pp(Name), " : ", pp(Type), " = ", pp(Default)];
+pp({named_arg_t, _, Name, Type, _Default}) ->
+    [pp(Name), " : ", pp(Type)];
 pp({fun_t, _, Named = {uvar, _, _}, As, B}) ->
    ["(", pp(Named), " | ", pp(As), ") => ", pp(B)];
 pp({fun_t, _, Named, As, B}) when is_list(Named) ->
@@ -2751,7 +3029,7 @@ desugar_updates([Upd | Updates]) ->
    {More, Updates1}       = updates_key(Key, Updates),
    %% Check conflicts
    case length([ [] || [] <- [Rest | More] ]) of
-        N when N > 1 -> error({conflicting_updates_for_field, Upd, Key});
+        N when N > 1 -> type_error({conflicting_updates_for_field, Upd, Key});
        _ -> ok
    end,
    [MakeField(lists:append([Rest | More])) | desugar_updates(Updates1)].
@@ -36,7 +36,14 @@
              bits_intersection | bits_union | bits_difference |
              contract_to_address | address_to_contract | crypto_verify_sig | crypto_verify_sig_secp256k1 |
              crypto_sha3 | crypto_sha256 | crypto_blake2b |
-              crypto_ecverify_secp256k1 | crypto_ecrecover_secp256k1.
+              crypto_ecverify_secp256k1 | crypto_ecrecover_secp256k1 |
+              mcl_bls12_381_g1_neg | mcl_bls12_381_g1_norm | mcl_bls12_381_g1_valid |
+              mcl_bls12_381_g1_is_zero | mcl_bls12_381_g1_add | mcl_bls12_381_g1_mul |
+              mcl_bls12_381_g2_neg | mcl_bls12_381_g2_norm | mcl_bls12_381_g2_valid |
+              mcl_bls12_381_g2_is_zero | mcl_bls12_381_g2_add | mcl_bls12_381_g2_mul |
+              mcl_bls12_381_gt_inv | mcl_bls12_381_gt_add | mcl_bls12_381_gt_mul | mcl_bls12_381_gt_pow |
+              mcl_bls12_381_gt_is_one | mcl_bls12_381_pairing | mcl_bls12_381_miller_loop | mcl_bls12_381_final_exp |
+              mcl_bls12_381_int_to_fr | mcl_bls12_381_int_to_fp | mcl_bls12_381_fr_to_int | mcl_bls12_381_fp_to_int.

 -type flit() :: {int, integer()}
              | {string, binary()}
@@ -171,13 +178,43 @@ ast_to_fcode(Code, Options) ->

 -spec init_env([option()]) -> env().
 init_env(Options) ->
+    ChainTxArities = [3, 0, 0, 0, 0, 0, 1, 1, 1, 2, 1, 2, 2, 1, 1, 1, 1, 1, 1, 1, 2, 0],
    #{ type_env  => init_type_env(),
       fun_env   => #{},
       builtins  => builtins(),
       con_env   => #{["None"]        => #con_tag{ tag = 0, arities = [0, 1] },
                      ["Some"]        => #con_tag{ tag = 1, arities = [0, 1] },
                      ["RelativeTTL"] => #con_tag{ tag = 0, arities = [1, 1] },
-                      ["FixedTTL"]    => #con_tag{ tag = 1, arities = [1, 1] }
+                      ["FixedTTL"]    => #con_tag{ tag = 1, arities = [1, 1] },
+                      ["AENS", "AccountPt"]  => #con_tag{ tag = 0, arities = [1, 1, 1, 1] },
+                      ["AENS", "OraclePt"]   => #con_tag{ tag = 1, arities = [1, 1, 1, 1] },
+                      ["AENS", "ContractPt"] => #con_tag{ tag = 2, arities = [1, 1, 1, 1] },
+                      ["AENS", "ChannelPt"]  => #con_tag{ tag = 3, arities = [1, 1, 1, 1] },
+                      ["AENS", "Name"]       => #con_tag{ tag = 0, arities = [3] },
+                      ["Chain", "GAMetaTx"]               => #con_tag{ tag = 0, arities = [2] },
+                      ["Chain", "PayingForTx"]            => #con_tag{ tag = 0, arities = [2] },
+                      ["Chain", "SpendTx"]                => #con_tag{ tag = 0, arities = ChainTxArities },
+                      ["Chain", "OracleRegisterTx"]       => #con_tag{ tag = 1, arities = ChainTxArities },
+                      ["Chain", "OracleQueryTx"]          => #con_tag{ tag = 2, arities = ChainTxArities },
+                      ["Chain", "OracleResponseTx"]       => #con_tag{ tag = 3, arities = ChainTxArities },
+                      ["Chain", "OracleExtendTx"]         => #con_tag{ tag = 4, arities = ChainTxArities },
+                      ["Chain", "NamePreclaimTx"]         => #con_tag{ tag = 5, arities = ChainTxArities },
+                      ["Chain", "NameClaimTx"]            => #con_tag{ tag = 6, arities = ChainTxArities },
+                      ["Chain", "NameUpdateTx"]           => #con_tag{ tag = 7, arities = ChainTxArities },
+                      ["Chain", "NameRevokeTx"]           => #con_tag{ tag = 8, arities = ChainTxArities },
+                      ["Chain", "NameTransferTx"]         => #con_tag{ tag = 9, arities = ChainTxArities },
+                      ["Chain", "ChannelCreateTx"]        => #con_tag{ tag = 10, arities = ChainTxArities },
+                      ["Chain", "ChannelDepositTx"]       => #con_tag{ tag = 11, arities = ChainTxArities },
+                      ["Chain", "ChannelWithdrawTx"]      => #con_tag{ tag = 12, arities = ChainTxArities },
+                      ["Chain", "ChannelForceProgressTx"] => #con_tag{ tag = 13, arities = ChainTxArities },
+                      ["Chain", "ChannelCloseMutualTx"]   => #con_tag{ tag = 14, arities = ChainTxArities },
+                      ["Chain", "ChannelCloseSoloTx"]     => #con_tag{ tag = 15, arities = ChainTxArities },
+                      ["Chain", "ChannelSlashTx"]         => #con_tag{ tag = 16, arities = ChainTxArities },
+                      ["Chain", "ChannelSettleTx"]        => #con_tag{ tag = 17, arities = ChainTxArities },
+                      ["Chain", "ChannelSnapshotSoloTx"]  => #con_tag{ tag = 18, arities = ChainTxArities },
+                      ["Chain", "ContractCreateTx"]       => #con_tag{ tag = 19, arities = ChainTxArities },
+                      ["Chain", "ContractCallTx"]         => #con_tag{ tag = 20, arities = ChainTxArities },
+                      ["Chain", "GAAttachTx"]             => #con_tag{ tag = 21, arities = ChainTxArities }
                     },
       options   => Options,
       functions => #{} }.
@@ -194,18 +231,25 @@ builtins() ->
              {["Contract"], [{"address", none}, {"balance", none}, {"creator", none}]},
              {["Call"],     [{"origin", none}, {"caller", none}, {"value", none}, {"gas_price", none},
                              {"gas_left", 0}]},
-              {["Oracle"],   [{"register", 4}, {"query_fee", 1}, {"query", 5}, {"get_question", 2},
+              {["Oracle"],   [{"register", 4}, {"expiry", 1}, {"query_fee", 1}, {"query", 5}, {"get_question", 2},
                              {"respond", 4}, {"extend", 3}, {"get_answer", 2},
                              {"check", 1}, {"check_query", 2}]},
              {["AENS"],     [{"resolve", 2}, {"preclaim", 3}, {"claim", 5}, {"transfer", 4},
-                              {"revoke", 3}]},
+                              {"revoke", 3}, {"update", 6}, {"lookup", 1}]},
              {["Map"],      [{"from_list", 1}, {"to_list", 1}, {"lookup", 2},
                              {"lookup_default", 3}, {"delete", 2}, {"member", 2}, {"size", 1}]},
              {["Crypto"],   [{"verify_sig", 3}, {"verify_sig_secp256k1", 3},
                              {"ecverify_secp256k1", 3}, {"ecrecover_secp256k1", 2},
                              {"sha3", 1}, {"sha256", 1}, {"blake2b", 1}]},
-              {["Auth"],     [{"tx_hash", none}]},
-              {["String"],   [{"length", 1}, {"concat", 2}, {"sha3", 1}, {"sha256", 1}, {"blake2b", 1}]},
+              {["MCL_BLS12_381"], [{"g1_neg", 1}, {"g1_norm", 1}, {"g1_valid", 1}, {"g1_is_zero", 1}, {"g1_add", 2}, {"g1_mul", 2},
+                                   {"g2_neg", 1}, {"g2_norm", 1}, {"g2_valid", 1}, {"g2_is_zero", 1}, {"g2_add", 2}, {"g2_mul", 2},
+                                   {"gt_inv", 1}, {"gt_add", 2}, {"gt_mul", 2}, {"gt_pow", 2}, {"gt_is_one", 1},
+                                   {"pairing", 2}, {"miller_loop", 2}, {"final_exp", 1},
+                                   {"int_to_fr", 1}, {"int_to_fp", 1}, {"fr_to_int", 1}, {"fp_to_int", 1}]},
+              {["StringInternal"], [{"length", 1}, {"concat", 2}, {"to_list", 1}, {"from_list", 1},
+                                    {"sha3", 1}, {"sha256", 1}, {"blake2b", 1}, {"to_lower", 1}, {"to_upper", 1}]},
+              {["Char"],     [{"to_int", 1}, {"from_int", 1}]},
+              {["Auth"],     [{"tx_hash", none}, {"tx", none}]},
              {["Bits"],     [{"set", 2}, {"clear", 2}, {"test", 2}, {"sum", 1}, {"intersection", 2},
                              {"union", 2}, {"difference", 2}, {"none", none}, {"all", none}]},
              {["Bytes"],    [{"to_int", 1}, {"to_str", 1}, {"concat", 2}, {"split", 1}]},
@@ -224,20 +268,32 @@ state_layout(Env) -> maps:get(state_layout, Env, {reg, 1}).

 -spec init_type_env() -> type_env().
 init_type_env() ->
-    #{ ["int"]          => ?type(integer),
-       ["bool"]         => ?type(boolean),
-       ["bits"]         => ?type(bits),
-       ["char"]         => ?type(integer),
-       ["string"]       => ?type(string),
-       ["address"]      => ?type(address),
-       ["hash"]         => ?type(hash),
-       ["signature"]    => ?type(signature),
-       ["oracle"]       => ?type(Q, R, {oracle, Q, R}),
-       ["oracle_query"] => ?type(_, _, oracle_query),
-       ["list"]         => ?type(T, {list, T}),
-       ["map"]          => ?type(K, V, {map, K, V}),
-       ["option"]       => ?type(T, {variant, [[], [T]]}),
-       ["Chain", "ttl"] => ?type({variant, [[integer], [integer]]})
+    BaseTx = {variant, [[address, integer, string], [], [], [], [], [], [string],
+                        [hash], [hash], [address, hash], [address],
+                        [address, integer], [address, integer], [address],
+                        [address], [address], [address], [address], [address],
+                        [integer], [address, integer], []]},
+    #{ ["int"]             => ?type(integer),
+       ["bool"]            => ?type(boolean),
+       ["bits"]            => ?type(bits),
+       ["char"]            => ?type(integer),
+       ["string"]          => ?type(string),
+       ["address"]         => ?type(address),
+       ["hash"]            => ?type(hash),
+       ["signature"]       => ?type(signature),
+       ["oracle"]          => ?type(Q, R, {oracle, Q, R}),
+       ["oracle_query"]    => ?type(_, _, oracle_query),    %% TODO: not in Fate
+       ["list"]            => ?type(T, {list, T}),
+       ["map"]             => ?type(K, V, {map, K, V}),
+       ["option"]          => ?type(T, {variant, [[], [T]]}),
+       ["Chain", "ttl"]    => ?type({variant, [[integer], [integer]]}),
+       ["AENS", "pointee"] => ?type({variant, [[address], [address], [address], [address]]}),
+       ["AENS", "name"]    => ?type({variant, [[address, {variant, [[integer], [integer]]}, {map, string, {variant, [[address], [address], [address], [address]]}}]]}),
+       ["Chain", "ga_meta_tx"]    => ?type({variant, [[address, integer]]}),
+       ["Chain", "paying_for_tx"] => ?type({variant, [[address, integer]]}),
+       ["Chain", "base_tx"]       => ?type(BaseTx),
+       ["MCL_BLS12_381", "fr"]  => ?type({bytes, 32}),
+       ["MCL_BLS12_381", "fp"]  => ?type({bytes, 48})
     }.

 is_no_code(Env) ->
@@ -291,7 +347,6 @@ decls_to_fcode(Env, Decls) ->
                end, Env1, Decls).

 -spec decl_to_fcode(env(), aeso_syntax:decl()) -> env().
-decl_to_fcode(Env, {type_decl, _, _, _}) -> Env;
 decl_to_fcode(Env = #{context := {main_contract, _}}, {fun_decl, _, Id, _}) ->
    case is_no_code(Env) of
        false -> fcode_error({missing_definition, Id});
@@ -412,6 +467,8 @@ type_to_fcode(Env, Sub, {fun_t, _, Named, Args, Res}) ->
    FNamed = [type_to_fcode(Env, Sub, Arg) || {named_arg_t, _, _, Arg, _} <- Named],
    FArgs  = [type_to_fcode(Env, Sub, Arg) || Arg <- Args],
    {function, FNamed ++ FArgs, type_to_fcode(Env, Sub, Res)};
+type_to_fcode(Env, Sub, {if_t, _, _, _, Else}) ->
+    type_to_fcode(Env, Sub, Else);  %% Hacky: this is only for remote calls, in which case we want the unprotected type
 type_to_fcode(_Env, _Sub, Type) ->
    error({todo, Type}).

@@ -986,12 +1043,21 @@ stmts_to_fcode(Env, [Expr | Stmts]) ->

 op_builtins() ->
    [map_from_list, map_to_list, map_delete, map_member, map_size,
-     string_length, string_concat, string_sha3, string_sha256, string_blake2b,
+     stringinternal_length, stringinternal_concat, stringinternal_to_list, stringinternal_from_list,
+     stringinternal_sha3, stringinternal_sha256, stringinternal_blake2b,
+     char_to_int, char_from_int, stringinternal_to_lower, stringinternal_to_upper,
     bits_set, bits_clear, bits_test, bits_sum, bits_intersection, bits_union,
     bits_difference, int_to_str, address_to_str, crypto_verify_sig,
     address_to_contract,
     crypto_verify_sig_secp256k1, crypto_sha3, crypto_sha256, crypto_blake2b,
-     crypto_ecverify_secp256k1, crypto_ecrecover_secp256k1
+     crypto_ecverify_secp256k1, crypto_ecrecover_secp256k1,
+     mcl_bls12_381_g1_neg, mcl_bls12_381_g1_norm, mcl_bls12_381_g1_valid,
+     mcl_bls12_381_g1_is_zero, mcl_bls12_381_g1_add, mcl_bls12_381_g1_mul,
+     mcl_bls12_381_g2_neg, mcl_bls12_381_g2_norm, mcl_bls12_381_g2_valid,
+     mcl_bls12_381_g2_is_zero, mcl_bls12_381_g2_add, mcl_bls12_381_g2_mul,
+     mcl_bls12_381_gt_inv, mcl_bls12_381_gt_add, mcl_bls12_381_gt_mul, mcl_bls12_381_gt_pow,
+     mcl_bls12_381_gt_is_one, mcl_bls12_381_pairing, mcl_bls12_381_miller_loop, mcl_bls12_381_final_exp,
+     mcl_bls12_381_int_to_fr, mcl_bls12_381_int_to_fp, mcl_bls12_381_fr_to_int, mcl_bls12_381_fp_to_int
    ].

 set_state({reg, R}, Val) ->
@@ -1152,8 +1218,8 @@ lambda_lift_expr(Layout, UExpr) when element(1, UExpr) == def_u; element(1, UExp
 lambda_lift_expr(Layout, {remote_u, ArgsT, RetT, Ct, F}) ->
    FVs  = free_vars(Ct),
    Ct1  = lambda_lift_expr(Layout, Ct),
-    GasAndValueArgs = 2,
-    Xs   = [ lists:concat(["arg", I]) || I <- lists:seq(1, length(ArgsT) + GasAndValueArgs) ],
+    NamedArgCount = 3,
+    Xs   = [ lists:concat(["arg", I]) || I <- lists:seq(1, length(ArgsT) + NamedArgCount) ],
    Args = [{var, X} || X <- Xs],
    make_closure(FVs, Xs, {remote, ArgsT, RetT, Ct1, F, Args});
 lambda_lift_expr(Layout, Expr) ->
@@ -469,6 +469,7 @@ is_builtin_fun({qid, _, ["AENS", "preclaim"]}, _Icode)                       ->
 is_builtin_fun({qid, _, ["AENS", "claim"]}, _Icode)                          -> true;
 is_builtin_fun({qid, _, ["AENS", "transfer"]}, _Icode)                       -> true;
 is_builtin_fun({qid, _, ["AENS", "revoke"]}, _Icode)                         -> true;
+is_builtin_fun({qid, _, ["AENS", "update"]}, _Icode)                         -> true;
 is_builtin_fun({qid, _, ["Map", "lookup"]}, _Icode)                          -> true;
 is_builtin_fun({qid, _, ["Map", "lookup_default"]}, _Icode)                  -> true;
 is_builtin_fun({qid, _, ["Map", "member"]}, _Icode)                          -> true;
@@ -624,6 +625,12 @@ builtin_code(_, {qid, _, ["AENS", "revoke"]}, Args, _, _, Icode) ->
              [ast_body(Addr, Icode), ast_body(Name, Icode), ast_body(Sign, Icode)],
              [word, word, sign_t()], {tuple, []});

+builtin_code(_, {qid, _, ["AENS", "update"]}, Args, _, _, Icode) ->
+    {Sign, [Addr, Name, TTL, ClientTTL, Pointers]} = get_signature_arg(Args),
+    prim_call(?PRIM_CALL_AENS_UPDATE, #integer{value = 0},
+              [ast_body(Addr, Icode), ast_body(Name, Icode), ast_body(TTL, Icode), ast_body(ClientTTL, Icode), ast_body(Pointers, Icode), ast_body(Sign, Icode)],
+              [word, string, word, word, word, sign_t()], {tuple, []});
+
 %% -- Maps
 %% -- lookup functions
 builtin_code(_, {qid, _, ["Map", "lookup"]}, [Key, Map], _, _, Icode) ->
@@ -927,11 +934,16 @@ ast_typerep1({variant_t, Cons}, Icode) ->
    {variant, [ begin
                  {constr_t, _, _, Args} = Con,
                  [ ast_typerep1(Arg, Icode) || Arg <- Args ]
-                end || Con <- Cons ]}.
+                end || Con <- Cons ]};
+ast_typerep1({if_t, _, _, _, Else}, Icode) ->
+    ast_typerep1(Else, Icode). %% protected remote calls are not in AEVM

 ttl_t(Icode) ->
    ast_typerep({qid, [], ["Chain", "ttl"]}, Icode).

+%% pointee_t(Icode) ->
+%%     ast_typerep({qid, [], ["AENS", "pointee"]}, Icode).
+
 sign_t() -> bytes_t(64).
 bytes_t(Len) when Len =< 32 -> word;
 bytes_t(Len)                -> {tuple, lists:duplicate((31 + Len) div 32, word)}.
@@ -38,10 +38,13 @@
                | pp_assembler
                | pp_bytecode
                | no_code
+                | keep_included
+                | debug_mode
                | {backend, aevm | fate}
                | {include, {file_system, [string()]} |
                            {explicit_files, #{string() => binary()}}}
-                | {src_file, string()}.
+                | {src_file, string()}
+                | {aci, aeso_aci:aci_type()}.
 -type options() :: [option()].

 -export_type([ option/0
@@ -115,7 +118,8 @@ from_string(Backend, ContractString, Options) ->
    end.

 from_string1(aevm, ContractString, Options) ->
-    #{icode := Icode} = string_to_code(ContractString, Options),
+    #{ icode := Icode
+     , folded_typed_ast := FoldedTypedAst } = string_to_code(ContractString, Options),
    TypeInfo  = extract_type_info(Icode),
    Assembler = assemble(Icode, Options),
    pp_assembler(aevm, Assembler, Options),
@@ -123,47 +127,63 @@ from_string1(aevm, ContractString, Options) ->
    ByteCode = << << B:8 >> || B <- ByteCodeList >>,
    pp_bytecode(ByteCode, Options),
    {ok, Version} = version(),
-    {ok, #{byte_code => ByteCode,
-           compiler_version => Version,
-           contract_source => ContractString,
-           type_info => TypeInfo,
-           abi_version => aeb_aevm_abi:abi_version(),
-           payable => maps:get(payable, Icode)
-          }};
+    Res = #{byte_code => ByteCode,
+            compiler_version => Version,
+            contract_source => ContractString,
+            type_info => TypeInfo,
+            abi_version => aeb_aevm_abi:abi_version(),
+            payable => maps:get(payable, Icode)
+           },
+    {ok, maybe_generate_aci(Res, FoldedTypedAst, Options)};
 from_string1(fate, ContractString, Options) ->
-    #{fcode := FCode} = string_to_code(ContractString, Options),
+    #{ fcode := FCode
+     , folded_typed_ast := FoldedTypedAst } = string_to_code(ContractString, Options),
    FateCode = aeso_fcode_to_fate:compile(FCode, Options),
    pp_assembler(fate, FateCode, Options),
    ByteCode = aeb_fate_code:serialize(FateCode, []),
    {ok, Version} = version(),
-    {ok, #{byte_code => ByteCode,
-           compiler_version => Version,
-           contract_source => ContractString,
-           type_info => [],
-           fate_code => FateCode,
-           abi_version => aeb_fate_abi:abi_version(),
-           payable => maps:get(payable, FCode)
-          }}.
+    Res = #{byte_code => ByteCode,
+            compiler_version => Version,
+            contract_source => ContractString,
+            type_info => [],
+            fate_code => FateCode,
+            abi_version => aeb_fate_abi:abi_version(),
+            payable => maps:get(payable, FCode)
+           },
+    {ok, maybe_generate_aci(Res, FoldedTypedAst, Options)}.
+
+maybe_generate_aci(Result, FoldedTypedAst, Options) ->
+    case proplists:get_value(aci, Options) of
+        undefined ->
+            Result;
+        Type ->
+            {ok, Aci} = aeso_aci:from_typed_ast(Type, FoldedTypedAst),
+            maps:put(aci, Aci, Result)
+    end.

 -spec string_to_code(string(), options()) -> map().
 string_to_code(ContractString, Options) ->
    Ast = parse(ContractString, Options),
    pp_sophia_code(Ast, Options),
    pp_ast(Ast, Options),
-    {TypeEnv, TypedAst} = aeso_ast_infer_types:infer(Ast, [return_env | Options]),
-    pp_typed_ast(TypedAst, Options),
+    {TypeEnv, FoldedTypedAst, UnfoldedTypedAst} = aeso_ast_infer_types:infer(Ast, [return_env | Options]),
+    pp_typed_ast(UnfoldedTypedAst, Options),
    case proplists:get_value(backend, Options, aevm) of
        aevm ->
-            Icode = ast_to_icode(TypedAst, Options),
+            Icode = ast_to_icode(UnfoldedTypedAst, Options),
            pp_icode(Icode, Options),
-            #{ icode => Icode,
-               typed_ast => TypedAst,
-               type_env  => TypeEnv};
+            #{ icode => Icode
+             , unfolded_typed_ast => UnfoldedTypedAst
+             , folded_typed_ast => FoldedTypedAst
+             , type_env  => TypeEnv
+             , ast => Ast };
        fate ->
-            Fcode = aeso_ast_to_fcode:ast_to_fcode(TypedAst, Options),
-            #{ fcode => Fcode,
-               typed_ast => TypedAst,
-               type_env  => TypeEnv}
+            Fcode = aeso_ast_to_fcode:ast_to_fcode(UnfoldedTypedAst, Options),
+            #{ fcode => Fcode
+             , unfolded_typed_ast => UnfoldedTypedAst
+             , folded_typed_ast => FoldedTypedAst
+             , type_env  => TypeEnv
+             , ast => Ast }
    end.

 -define(CALL_NAME,   "__call").
@@ -198,9 +218,9 @@ check_call1(ContractString0, FunName, Args, Options) ->
        case proplists:get_value(backend, Options, aevm) of
            aevm ->
                %% First check the contract without the __call function
-                #{} = string_to_code(ContractString0, Options),
-                ContractString = insert_call_function(ContractString0, ?CALL_NAME, FunName, Args, Options),
-                #{typed_ast := TypedAst,
+                #{ast := Ast} = string_to_code(ContractString0, Options),
+                ContractString = insert_call_function(Ast, ContractString0, ?CALL_NAME, FunName, Args),
+                #{unfolded_typed_ast := TypedAst,
                  icode     := Icode} = string_to_code(ContractString, Options),
                {ok, {FunName, {fun_t, _, _, ArgTypes, RetType}}} = get_call_type(TypedAst),
                ArgVMTypes = [ aeso_ast_to_icode:ast_typerep(T, Icode) || T <- ArgTypes ],
@@ -220,13 +240,14 @@ check_call1(ContractString0, FunName, Args, Options) ->
                {ok, FunName, {ArgVMTypes, RetVMType1}, ArgTerms};
            fate ->
                %% First check the contract without the __call function
-                #{fcode := OrgFcode} = string_to_code(ContractString0, Options),
+                #{ fcode := OrgFcode
+                 , ast := Ast } = string_to_code(ContractString0, Options),
                FateCode = aeso_fcode_to_fate:compile(OrgFcode, []),
                %% collect all hashes and compute the first name without hash collision to
                SymbolHashes = maps:keys(aeb_fate_code:symbols(FateCode)),
                CallName = first_none_match(?CALL_NAME, SymbolHashes,
                                            lists:seq($1, $9) ++ lists:seq($A, $Z) ++ lists:seq($a, $z)),
-                ContractString = insert_call_function(ContractString0, CallName, FunName, Args, Options),
+                ContractString = insert_call_function(Ast, ContractString0, CallName, FunName, Args),
                #{fcode := Fcode} = string_to_code(ContractString, Options),
                CallArgs = arguments_of_body(CallName, FunName, Fcode),
                {ok, FunName, CallArgs}
@@ -252,9 +273,8 @@ first_none_match(CallName, Hashes, [Char|Chars]) ->
    end.

 %% Add the __call function to a contract.
-spec insert_call_function(string(), string(), string(), [string()], options()) -> string().
-insert_call_function(Code, Call, FunName, Args, Options) ->
-    Ast = parse(Code, Options),
+-spec insert_call_function(aeso_syntax:ast(), string(), string(), string(), [string()]) -> string().
+insert_call_function(Ast, Code, Call, FunName, Args) ->
    Ind = last_contract_indent(Ast),
    lists:flatten(
        [ Code,
@@ -310,7 +330,7 @@ to_sophia_value(ContractString, FunName, ok, Data, Options0) ->
    Options = [no_code | Options0],
    try
        Code = string_to_code(ContractString, Options),
-        #{ typed_ast := TypedAst, type_env  := TypeEnv} = Code,
+        #{ unfolded_typed_ast := TypedAst, type_env  := TypeEnv} = Code,
        {ok, _, Type0} = get_decode_type(FunName, TypedAst),
        Type   = aeso_ast_infer_types:unfold_types_in_type(TypeEnv, Type0, [unfold_record_types, unfold_variant_types]),

@@ -336,12 +356,12 @@ to_sophia_value(ContractString, FunName, ok, Data, Options0) ->
                try
                    {ok, aeso_vm_decode:from_fate(Type, aeb_fate_encoding:deserialize(Data))}
                catch throw:cannot_translate_to_sophia ->
-                        Type1 = prettypr:format(aeso_pretty:type(Type)),
+                        Type1 = prettypr:format(aeso_pretty:type(Type0)),
                        Msg = io_lib:format("Cannot translate FATE value ~p\n  of Sophia type ~s\n",
                                            [aeb_fate_encoding:deserialize(Data), Type1]),
                        {error, [aeso_errors:new(data_error, Msg)]};
                      _:_ ->
-                        Type1 = prettypr:format(aeso_pretty:type(Type)),
+                        Type1 = prettypr:format(aeso_pretty:type(Type0)),
                        Msg = io_lib:format("Failed to decode binary as type ~s\n", [Type1]),
                        {error, [aeso_errors:new(data_error, Msg)]}
               end
@@ -386,7 +406,7 @@ decode_calldata(ContractString, FunName, Calldata, Options0) ->
    Options = [no_code | Options0],
    try
        Code = string_to_code(ContractString, Options),
-        #{ typed_ast := TypedAst, type_env  := TypeEnv} = Code,
+        #{ unfolded_typed_ast := TypedAst, type_env  := TypeEnv} = Code,

        {ok, Args, _} = get_decode_type(FunName, TypedAst),
        GetType       = fun({typed, _, _, T}) -> T; (T) -> T end,
@@ -650,8 +670,9 @@ pp_fate_type(T) -> io_lib:format("~w", [T]).

 %% -------------------------------------------------------------------

+-spec sophia_type_to_typerep(string()) -> {error, bad_type} | {ok, aeb_aevm_data:type()}.
 sophia_type_to_typerep(String) ->
-    {ok, Ast} = aeso_parser:type(String),
+    Ast = aeso_parser:run_parser(aeso_parser:type(), String),
    try aeso_ast_to_icode:ast_typerep(Ast) of
        Type -> {ok, Type}
    catch _:_ -> {error, bad_type}
@@ -302,18 +302,27 @@ to_scode1(Env, {funcall, Fun, Args}) ->
 to_scode1(Env, {builtin, B, Args}) ->
    builtin_to_scode(Env, B, Args);

-to_scode1(Env, {remote, ArgsT, RetT, Ct, Fun, [Gas, Value | Args]}) ->
+to_scode1(Env, {remote, ArgsT, RetT, Ct, Fun, [Gas, Value, Protected | Args]}) ->
    Lbl = make_function_id(Fun),
    {ArgTypes, RetType0} = typesig_to_scode([{"_", T} || T <- ArgsT], RetT),
    ArgType = ?i(aeb_fate_data:make_typerep({tuple, ArgTypes})),
    RetType = ?i(aeb_fate_data:make_typerep(RetType0)),
-    case Gas of
-        {builtin, call_gas_left, _} ->
-            Call = aeb_fate_ops:call_r(?a, Lbl, ArgType, RetType, ?a),
-            call_to_scode(Env, Call, [Ct, Value | Args]);
+    case Protected of
+        {lit, {bool, false}} ->
+            case Gas of
+                {builtin, call_gas_left, _} ->
+                    Call = aeb_fate_ops:call_r(?a, Lbl, ArgType, RetType, ?a),
+                    call_to_scode(Env, Call, [Ct, Value | Args]);
+                _ ->
+                    Call = aeb_fate_ops:call_gr(?a, Lbl, ArgType, RetType, ?a, ?a),
+                    call_to_scode(Env, Call, [Ct, Value, Gas | Args])
+            end;
+        {lit, {bool, true}} ->
+            Call = aeb_fate_ops:call_pgr(?a, Lbl, ArgType, RetType, ?a, ?a, ?i(true)),
+            call_to_scode(Env, Call, [Ct, Value, Gas | Args]);
        _ ->
-            Call = aeb_fate_ops:call_gr(?a, Lbl, ArgType, RetType, ?a, ?a),
-            call_to_scode(Env, Call, [Ct, Value, Gas | Args])
+            Call = aeb_fate_ops:call_pgr(?a, Lbl, ArgType, RetType, ?a, ?a, ?a),
+            call_to_scode(Env, Call, [Ct, Value, Gas, Protected | Args])
    end;

 to_scode1(_Env, {get_state, Reg}) ->
@@ -498,6 +507,8 @@ builtin_to_scode(_Env, call_gas_left, []) ->
    [aeb_fate_ops:gas(?a)];
 builtin_to_scode(Env, oracle_register, [_Sign,_Account,_QFee,_TTL,_QType,_RType] = Args) ->
    call_to_scode(Env, aeb_fate_ops:oracle_register(?a, ?a, ?a, ?a, ?a, ?a, ?a), Args);
+builtin_to_scode(Env, oracle_expiry, [_Oracle] = Args) ->
+    call_to_scode(Env, aeb_fate_ops:oracle_expiry(?a, ?a), Args);
 builtin_to_scode(Env, oracle_query_fee, [_Oracle] = Args) ->
    call_to_scode(Env, aeb_fate_ops:oracle_query_fee(?a, ?a), Args);
 builtin_to_scode(Env, oracle_query, [_Oracle, _Question, _QFee, _QTTL, _RTTL, _QType, _RType] = Args) ->
@@ -536,8 +547,15 @@ builtin_to_scode(Env, aens_transfer, [_Sign, _From, _To, _Name] = Args) ->
 builtin_to_scode(Env, aens_revoke, [_Sign, _Account, _Name] = Args) ->
    call_to_scode(Env, [aeb_fate_ops:aens_revoke(?a, ?a, ?a),
                        tuple(0)], Args);
+builtin_to_scode(Env, aens_update, [_Sign, _Account, _NameString, _TTL, _ClientTTL, _Pointers] = Args) ->
+    call_to_scode(Env, [aeb_fate_ops:aens_update(?a, ?a, ?a, ?a, ?a, ?a),
+                        tuple(0)], Args);
+builtin_to_scode(Env, aens_lookup, [_Name] = Args) ->
+    call_to_scode(Env, aeb_fate_ops:aens_lookup(?a, ?a), Args);
 builtin_to_scode(_Env, auth_tx_hash, []) ->
-    [aeb_fate_ops:auth_tx_hash(?a)].
+    [aeb_fate_ops:auth_tx_hash(?a)];
+builtin_to_scode(_Env, auth_tx, []) ->
+    [aeb_fate_ops:auth_tx(?a)].

 %% -- Operators --

@@ -564,8 +582,14 @@ op_to_scode(map_to_list)       -> aeb_fate_ops:map_to_list(?a, ?a);
 op_to_scode(map_delete)        -> aeb_fate_ops:map_delete(?a, ?a, ?a);
 op_to_scode(map_member)        -> aeb_fate_ops:map_member(?a, ?a, ?a);
 op_to_scode(map_size)          -> aeb_fate_ops:map_size_(?a, ?a);
-op_to_scode(string_length)     -> aeb_fate_ops:str_length(?a, ?a);
-op_to_scode(string_concat)     -> aeb_fate_ops:str_join(?a, ?a, ?a);
+op_to_scode(stringinternal_length)    -> aeb_fate_ops:str_length(?a, ?a);
+op_to_scode(stringinternal_concat)    -> aeb_fate_ops:str_join(?a, ?a, ?a);
+op_to_scode(stringinternal_to_list)   -> aeb_fate_ops:str_to_list(?a, ?a);
+op_to_scode(stringinternal_from_list) -> aeb_fate_ops:str_from_list(?a, ?a);
+op_to_scode(stringinternal_to_lower)  -> aeb_fate_ops:str_to_lower(?a, ?a);
+op_to_scode(stringinternal_to_upper)  -> aeb_fate_ops:str_to_upper(?a, ?a);
+op_to_scode(char_to_int)       -> aeb_fate_ops:char_to_int(?a, ?a);
+op_to_scode(char_from_int)     -> aeb_fate_ops:char_from_int(?a, ?a);
 op_to_scode(bits_set)          -> aeb_fate_ops:bits_set(?a, ?a, ?a);
 op_to_scode(bits_clear)        -> aeb_fate_ops:bits_clear(?a, ?a, ?a);
 op_to_scode(bits_test)         -> aeb_fate_ops:bits_test(?a, ?a, ?a);
@@ -584,9 +608,33 @@ op_to_scode(crypto_ecrecover_secp256k1)  -> aeb_fate_ops:ecrecover_secp256k1(?a,
 op_to_scode(crypto_sha3)                 -> aeb_fate_ops:sha3(?a, ?a);
 op_to_scode(crypto_sha256)               -> aeb_fate_ops:sha256(?a, ?a);
 op_to_scode(crypto_blake2b)              -> aeb_fate_ops:blake2b(?a, ?a);
-op_to_scode(string_sha3)                 -> aeb_fate_ops:sha3(?a, ?a);
-op_to_scode(string_sha256)               -> aeb_fate_ops:sha256(?a, ?a);
-op_to_scode(string_blake2b)              -> aeb_fate_ops:blake2b(?a, ?a).
+op_to_scode(stringinternal_sha3)         -> aeb_fate_ops:sha3(?a, ?a);
+op_to_scode(stringinternal_sha256)       -> aeb_fate_ops:sha256(?a, ?a);
+op_to_scode(stringinternal_blake2b)      -> aeb_fate_ops:blake2b(?a, ?a);
+op_to_scode(mcl_bls12_381_g1_neg)        -> aeb_fate_ops:bls12_381_g1_neg(?a, ?a);
+op_to_scode(mcl_bls12_381_g1_norm)       -> aeb_fate_ops:bls12_381_g1_norm(?a, ?a);
+op_to_scode(mcl_bls12_381_g1_valid)      -> aeb_fate_ops:bls12_381_g1_valid(?a, ?a);
+op_to_scode(mcl_bls12_381_g1_is_zero)    -> aeb_fate_ops:bls12_381_g1_is_zero(?a, ?a);
+op_to_scode(mcl_bls12_381_g1_add)        -> aeb_fate_ops:bls12_381_g1_add(?a, ?a, ?a);
+op_to_scode(mcl_bls12_381_g1_mul)        -> aeb_fate_ops:bls12_381_g1_mul(?a, ?a, ?a);
+op_to_scode(mcl_bls12_381_g2_neg)        -> aeb_fate_ops:bls12_381_g2_neg(?a, ?a);
+op_to_scode(mcl_bls12_381_g2_norm)       -> aeb_fate_ops:bls12_381_g2_norm(?a, ?a);
+op_to_scode(mcl_bls12_381_g2_valid)      -> aeb_fate_ops:bls12_381_g2_valid(?a, ?a);
+op_to_scode(mcl_bls12_381_g2_is_zero)    -> aeb_fate_ops:bls12_381_g2_is_zero(?a, ?a);
+op_to_scode(mcl_bls12_381_g2_add)        -> aeb_fate_ops:bls12_381_g2_add(?a, ?a, ?a);
+op_to_scode(mcl_bls12_381_g2_mul)        -> aeb_fate_ops:bls12_381_g2_mul(?a, ?a, ?a);
+op_to_scode(mcl_bls12_381_gt_inv)        -> aeb_fate_ops:bls12_381_gt_inv(?a, ?a);
+op_to_scode(mcl_bls12_381_gt_add)        -> aeb_fate_ops:bls12_381_gt_add(?a, ?a, ?a);
+op_to_scode(mcl_bls12_381_gt_mul)        -> aeb_fate_ops:bls12_381_gt_mul(?a, ?a, ?a);
+op_to_scode(mcl_bls12_381_gt_pow)        -> aeb_fate_ops:bls12_381_gt_pow(?a, ?a, ?a);
+op_to_scode(mcl_bls12_381_gt_is_one)     -> aeb_fate_ops:bls12_381_gt_is_one(?a, ?a);
+op_to_scode(mcl_bls12_381_pairing)       -> aeb_fate_ops:bls12_381_pairing(?a, ?a, ?a);
+op_to_scode(mcl_bls12_381_miller_loop)   -> aeb_fate_ops:bls12_381_miller_loop(?a, ?a, ?a);
+op_to_scode(mcl_bls12_381_final_exp)     -> aeb_fate_ops:bls12_381_final_exp(?a, ?a);
+op_to_scode(mcl_bls12_381_int_to_fr)     -> aeb_fate_ops:bls12_381_int_to_fr(?a, ?a);
+op_to_scode(mcl_bls12_381_int_to_fp)     -> aeb_fate_ops:bls12_381_int_to_fp(?a, ?a);
+op_to_scode(mcl_bls12_381_fr_to_int)     -> aeb_fate_ops:bls12_381_fr_to_int(?a, ?a);
+op_to_scode(mcl_bls12_381_fp_to_int)     -> aeb_fate_ops:bls12_381_fp_to_int(?a, ?a).

 %% PUSH and STORE ?a are the same, so we use STORE to make optimizations
 %% easier, and specialize to PUSH (which is cheaper) at the end.
@@ -734,6 +782,7 @@ attributes(I) ->
        {'CALL', A}                           -> Impure(?a, [A]);
        {'CALL_R', A, _, B, C, D}             -> Impure(?a, [A, B, C, D]);
        {'CALL_GR', A, _, B, C, D, E}         -> Impure(?a, [A, B, C, D, E]);
+        {'CALL_PGR', A, _, B, C, D, E, F}     -> Impure(?a, [A, B, C, D, E, F]);
        {'CALL_T', A}                         -> Impure(pc, [A]);
        {'CALL_VALUE', A}                     -> Pure(A, []);
        {'JUMP', _}                           -> Impure(pc, []);
@@ -815,6 +864,7 @@ attributes(I) ->
        {'CONTRACT_TO_ADDRESS', A, B}         -> Pure(A, [B]);
        {'ADDRESS_TO_CONTRACT', A, B}         -> Pure(A, [B]);
        {'AUTH_TX_HASH', A}                   -> Pure(A, []);
+        {'AUTH_TX', A}                        -> Pure(A, []);
        {'BYTES_TO_INT', A, B}                -> Pure(A, [B]);
        {'BYTES_TO_STR', A, B}                -> Pure(A, [B]);
        {'BYTES_CONCAT', A, B, C}             -> Pure(A, [B, C]);
@@ -853,12 +903,44 @@ attributes(I) ->
        {'ORACLE_GET_ANSWER', A, B, C, D, E}  -> Pure(A, [B, C, D, E]);
        {'ORACLE_GET_QUESTION', A, B, C, D, E}-> Pure(A, [B, C, D, E]);
        {'ORACLE_QUERY_FEE', A, B}            -> Pure(A, [B]);
-        {'AENS_RESOLVE', A, B, C, D}          -> Pure(A, [B, C, D]);
+        {'ORACLE_EXPIRY', A, B}               -> Impure(A, [B]);
+        {'AENS_RESOLVE', A, B, C, D}          -> Impure(A, [B, C, D]);
        {'AENS_PRECLAIM', A, B, C}            -> Impure(none, [A, B, C]);
        {'AENS_CLAIM', A, B, C, D, E}         -> Impure(none, [A, B, C, D, E]);
-        'AENS_UPDATE'                         -> Impure(none, []);%% TODO
+        {'AENS_UPDATE', A, B, C, D, E, F}     -> Impure(none, [A, B, C, D, E, F]);
        {'AENS_TRANSFER', A, B, C, D}         -> Impure(none, [A, B, C, D]);
        {'AENS_REVOKE', A, B, C}              -> Impure(none, [A, B, C]);
+        {'AENS_LOOKUP', A, B}                 -> Impure(A, [B]);
+        {'BLS12_381_G1_NEG', A, B}            -> Pure(A, [B]);
+        {'BLS12_381_G1_NORM', A, B}           -> Pure(A, [B]);
+        {'BLS12_381_G1_VALID', A, B}          -> Pure(A, [B]);
+        {'BLS12_381_G1_IS_ZERO', A, B}        -> Pure(A, [B]);
+        {'BLS12_381_G1_ADD', A, B, C}         -> Pure(A, [B, C]);
+        {'BLS12_381_G1_MUL', A, B, C}         -> Pure(A, [B, C]);
+        {'BLS12_381_G2_NEG', A, B}            -> Pure(A, [B]);
+        {'BLS12_381_G2_NORM', A, B}           -> Pure(A, [B]);
+        {'BLS12_381_G2_VALID', A, B}          -> Pure(A, [B]);
+        {'BLS12_381_G2_IS_ZERO', A, B}        -> Pure(A, [B]);
+        {'BLS12_381_G2_ADD', A, B, C}         -> Pure(A, [B, C]);
+        {'BLS12_381_G2_MUL', A, B, C}         -> Pure(A, [B, C]);
+        {'BLS12_381_GT_INV', A, B}            -> Pure(A, [B]);
+        {'BLS12_381_GT_ADD', A, B, C}         -> Pure(A, [B, C]);
+        {'BLS12_381_GT_MUL', A, B, C}         -> Pure(A, [B, C]);
+        {'BLS12_381_GT_POW', A, B, C}         -> Pure(A, [B, C]);
+        {'BLS12_381_GT_IS_ONE', A, B}         -> Pure(A, [B]);
+        {'BLS12_381_PAIRING', A, B, C}        -> Pure(A, [B, C]);
+        {'BLS12_381_MILLER_LOOP', A, B, C}    -> Pure(A, [B, C]);
+        {'BLS12_381_FINAL_EXP', A, B}         -> Pure(A, [B]);
+        {'BLS12_381_INT_TO_FR', A, B}         -> Pure(A, [B]);
+        {'BLS12_381_INT_TO_FP', A, B}         -> Pure(A, [B]);
+        {'BLS12_381_FR_TO_INT', A, B}         -> Pure(A, [B]);
+        {'BLS12_381_FP_TO_INT', A, B}         -> Pure(A, [B]);
+        {'STR_TO_LIST', A, B}                 -> Pure(A, [B]);
+        {'STR_FROM_LIST', A, B}               -> Pure(A, [B]);
+        {'STR_TO_UPPER', A, B}                -> Pure(A, [B]);
+        {'STR_TO_LOWER', A, B}                -> Pure(A, [B]);
+        {'CHAR_TO_INT', A, B}                 -> Pure(A, [B]);
+        {'CHAR_FROM_INT', A, B}               -> Pure(A, [B]);
        {'ABORT', A}                          -> Impure(pc, A);
        {'EXIT', A}                           -> Impure(pc, A);
        'NOP'                                 -> Pure(none, [])
@@ -1611,6 +1693,7 @@ split_calls(Ref, [], Acc, Blocks) ->
 split_calls(Ref, [I | Code], Acc, Blocks) when element(1, I) == 'CALL';
                                               element(1, I) == 'CALL_R';
                                               element(1, I) == 'CALL_GR';
+                                               element(1, I) == 'CALL_PGR';
                                               element(1, I) == 'jumpif' ->
    split_calls(make_ref(), Code, [], [{Ref, lists:reverse([I | Acc])} | Blocks]);
 split_calls(Ref, [{'ABORT', _} = I | _Code], Acc, Blocks) ->
@@ -73,28 +73,33 @@ new(Options) ->

 builtin_types() ->
    Word = fun([]) -> word end,
-    #{ "bool"         => Word
-     , "int"          => Word
-     , "char"         => Word
-     , "bits"         => Word
-     , "string"       => fun([]) -> string end
-     , "address"      => Word
-     , "hash"         => Word
-     , "unit"         => fun([]) -> {tuple, []} end
-     , "signature"    => fun([]) -> {tuple, [word, word]} end
-     , "oracle"       => fun([_, _]) -> word end
-     , "oracle_query" => fun([_, _]) -> word end
-     , "list"         => fun([A]) -> {list, A} end
-     , "option"       => fun([A]) -> {variant, [[], [A]]} end
-     , "map"          => fun([K, V]) -> map_typerep(K, V) end
-     , ["Chain", "ttl"] => fun([]) -> {variant, [[word], [word]]} end
+    #{ "bool"              => Word
+     , "int"               => Word
+     , "char"              => Word
+     , "bits"              => Word
+     , "string"            => fun([]) -> string end
+     , "address"           => Word
+     , "hash"              => Word
+     , "unit"              => fun([]) -> {tuple, []} end
+     , "signature"         => fun([]) -> {tuple, [word, word]} end
+     , "oracle"            => fun([_, _]) -> word end
+     , "oracle_query"      => fun([_, _]) -> word end
+     , "list"              => fun([A]) -> {list, A} end
+     , "option"            => fun([A]) -> {variant, [[], [A]]} end
+     , "map"               => fun([K, V]) -> map_typerep(K, V) end
+     , ["Chain", "ttl"]    => fun([]) -> {variant, [[word], [word]]} end
+     , ["AENS", "pointee"] => fun([]) -> {variant, [[word], [word], [word]]} end
     }.

 builtin_constructors() ->
-    #{ ["RelativeTTL"] => 0
-     , ["FixedTTL"]    => 1
-     , ["None"]        => 0
-     , ["Some"]        => 1 }.
+    #{ ["RelativeTTL"]     => 0
+     , ["FixedTTL"]        => 1
+     , ["None"]            => 0
+     , ["Some"]            => 1
+     , ["AccountPointee"]  => 0
+     , ["OraclePointee"]   => 1
+     , ["ContractPointee"] => 2
+     }.

 map_typerep(K, V) ->
    {map, K, V}.
@@ -146,4 +151,3 @@ get_constructor_tag(Name, #{constructors := Constructors}) ->
        undefined -> error({undefined_constructor, Name});
        Tag       -> Tag
    end.
-
@@ -74,25 +74,31 @@
                    %%   first argument. I.e. no backtracking to the second argument if the first
                    %%   fails.

+trampoline({bounce, Cont}) when is_function(Cont, 0) ->
+    trampoline(Cont());
+trampoline(Res) ->
+    Res.
+-define(BOUNCE(X), {bounce, fun() -> X end}).
+
 %% Apply a parser to its continuation. This compiles a parser to its low-level representation.
 -spec apply_p(parser(A), fun((A) -> parser1(B))) -> parser1(B).
 apply_p(?lazy(F), K)           -> apply_p(F(), K);
 apply_p(?fail(Err), _)         -> {fail, Err};
-apply_p(?choice([P | Ps]), K)  -> lists:foldl(fun(Q, R) -> choice1(apply_p(Q, K), R) end,
-                                             apply_p(P, K), Ps);
+apply_p(?choice([P | Ps]), K)  -> lists:foldl(fun(Q, R) -> choice1(trampoline(apply_p(Q, K)), R) end,
+                                              trampoline(apply_p(P, K)), Ps);
 apply_p(?bind(P, F), K)        -> apply_p(P, fun(X) -> apply_p(F(X), K) end);
 apply_p(?right(P, Q), K)       -> apply_p(P, fun(_) -> apply_p(Q, K) end);
 apply_p(?left(P, Q), K)        -> apply_p(P, fun(X) -> apply_p(Q, fun(_) -> K(X) end) end);
 apply_p(?map(F, P), K)         -> apply_p(P, fun(X) -> K(F(X)) end);
 apply_p(?layout, K)            -> {layout, K, {fail, {expected, layout_block}}};
 apply_p(?tok(Atom), K)         -> {tok_bind, #{Atom => K}};
-apply_p(?return(X), K)         -> K(X);
+apply_p(?return(X), K)         -> ?BOUNCE(K(X));
 apply_p([P | Q], K)            -> apply_p(P, fun(H) -> apply_p(Q, fun(T) -> K([H | T]) end) end);
 apply_p(T, K) when is_tuple(T) -> apply_p(tuple_to_list(T), fun(Xs) -> K(list_to_tuple(Xs)) end);
 apply_p(M, K) when is_map(M) ->
    {Keys, Ps} = lists:unzip(maps:to_list(M)),
    apply_p(Ps, fun(Vals) -> K(maps:from_list(lists:zip(Keys, Vals))) end);
-apply_p(X, K) -> K(X).
+apply_p(X, K) -> ?BOUNCE(K(X)).

 %% -- Primitive combinators --------------------------------------------------

@@ -160,7 +166,7 @@ layout() -> ?layout.
 %% @doc Parse a sequence of tokens using a parser. Fails if the parse is ambiguous.
 -spec parse(parser(A), tokens()) -> {ok, A} | {error, term()}.
 parse(P, S) ->
-  case parse1(apply_p(P, fun(X) -> {return_plus, X, {fail, no_error}} end), S) of
+  case parse1(trampoline(apply_p(P, fun(X) -> {return_plus, X, {fail, no_error}} end)), S) of
    {[], {Pos, Err}} -> {error, {add_current_file(Pos), parse_error, flatten_error(Err)}};
    {[A], _}         -> {ok, A};
    {As, _}          -> {error, {{1, 1}, ambiguous_parse, As}}
@@ -241,7 +247,7 @@ col(T)  when is_tuple(T) -> element(2, pos(T)).

 %% If both parsers want the next token we grab it and merge the continuations.
 choice1({tok_bind, Map1}, {tok_bind, Map2}) ->
-    {tok_bind, merge_with(fun(F, G) -> fun(T) -> choice1(F(T), G(T)) end end, Map1, Map2)};
+    {tok_bind, merge_with(fun(F, G) -> fun(T) -> choice1(trampoline(F(T)), trampoline(G(T))) end end, Map1, Map2)};

 %% If both parsers fail we combine the error messages. If only one fails we discard it.
 choice1({fail, E1}, {fail, E2})             -> {fail, add_error(E1, E2)};
@@ -255,7 +261,7 @@ choice1(P, {return_plus, X, Q})             -> {return_plus, X, choice1(P, Q)};
 %% If both sides want a layout block we combine them. If only one side wants a layout block we
 %% will commit to a layout block is there is one.
 choice1({layout, F, P}, {layout, G, Q})     ->
-    {layout, fun(N) -> choice1(F(N), G(N)) end, choice1(P, Q)};
+    {layout, fun(N) -> choice1(trampoline(F(N)), trampoline(G(N))) end, choice1(P, Q)};
 choice1({layout, F, P}, Q)                  -> {layout, F, choice1(P, Q)};
 choice1(P, {layout, G, Q})                  -> {layout, G, choice1(P, Q)}.

@@ -278,6 +284,8 @@ parse1(P, S) ->
 %% The main work horse. Returns a list of possible parses and an error message in case parsing
 %% fails.
 -spec parse1(parser1(A), #ts{}, [A], term()) -> {[A], error()}.
+parse1({bounce, F}, Ts, Acc, Err) ->
+    parse1(F(), Ts, Acc, Err);
 parse1({tok_bind, Map}, Ts, Acc, Err) ->
    case next_token(Ts) of
        {T, Ts1} ->
@@ -3,20 +3,33 @@
 %%% Description :
 %%% Created     : 1 Mar 2018 by Ulf Norell
 -module(aeso_parser).
+-compile({no_auto_import,[map_get/2]}).

 -export([string/1,
         string/2,
         string/3,
+         auto_imports/1,
         hash_include/2,
-         type/1]).
+         decl/0,
+         type/0,
+         body/0,
+         maybe_block/1,
+         run_parser/2,
+         run_parser/3]).

 -include("aeso_parse_lib.hrl").
 -import(aeso_parse_lib, [current_file/0, set_current_file/1]).

-type parse_result() :: aeso_syntax:ast() | none().
+-type parse_result() :: aeso_syntax:ast() | {aeso_syntax:ast(), sets:set(include_hash())} | none().

 -type include_hash() :: {string(), binary()}.

+
+escape_errors({ok, Ok}) ->
+    Ok;
+escape_errors({error, Err}) ->
+    parse_error(Err).
+
 -spec string(string()) -> parse_result().
 string(String) ->
    string(String, sets:new(), []).
@@ -30,21 +43,17 @@ string(String, Opts) ->

 -spec string(string(), sets:set(include_hash()), aeso_compiler:options()) -> parse_result().
 string(String, Included, Opts) ->
-    case parse_and_scan(file(), String, Opts) of
-        {ok, AST} ->
-            case expand_includes(AST, Included, Opts) of
-                {ok, AST1}   -> AST1;
-                {error, Err} -> parse_error(Err)
-            end;
-        {error, Err} ->
-            parse_error(Err)
+    AST = run_parser(file(), String, Opts),
+    case expand_includes(AST, Included, Opts) of
+        {ok, AST1}   -> AST1;
+        {error, Err} -> parse_error(Err)
    end.

-type(String) ->
-    case parse_and_scan(type(), String, []) of
-        {ok, AST}    -> {ok, AST};
-        {error, Err} -> {error, [mk_error(Err)]}
-    end.
+
+run_parser(P, Inp) ->
+    escape_errors(parse_and_scan(P, Inp, [])).
+run_parser(P, Inp, Opts) ->
+    escape_errors(parse_and_scan(P, Inp, Opts)).

 parse_and_scan(P, S, Opts) ->
    set_current_file(proplists:get_value(src_file, Opts, no_file)),
@@ -102,7 +111,7 @@ decl() ->

      %% Function declarations
    , ?RULE(modifiers(), fun_or_entry(), maybe_block(fundef_or_decl()), fun_block(_1, _2, _3))
-    , ?RULE(keyword('let'), valdef(),set_pos(get_pos(_1), _2))
+    , ?RULE(keyword('let'), valdef(), set_pos(get_pos(_1), _2))
    ])).

 fun_block(Mods, Kind, [Decl]) ->
@@ -596,8 +605,13 @@ expand_includes(AST, Included, Opts) ->
             || File <- lists:usort(auto_imports(AST)) ] ++ AST,
    expand_includes(AST1, Included, [], Opts).

-expand_includes([], _Included, Acc, _Opts) ->
-    {ok, lists:reverse(Acc)};
+expand_includes([], Included, Acc, Opts) ->
+    case lists:member(keep_included, Opts) of
+        false ->
+            {ok, lists:reverse(Acc)};
+        true ->
+            {ok, {lists:reverse(Acc), Included}}
+    end;
 expand_includes([{include, Ann, {string, _SAnn, File}} | AST], Included, Acc, Opts) ->
    case get_include_code(File, Ann, Opts) of
        {ok, Code} ->
@@ -656,8 +670,14 @@ stdlib_options() ->

 get_include_code(File, Ann, Opts) ->
    case {read_file(File, Opts), read_file(File, stdlib_options())} of
-        {{ok, _}, {ok,_ }} ->
-            fail(ann_pos(Ann), "Illegal redefinition of standard library " ++ File);
+        {{ok, Bin}, {ok, _}} ->
+            case filename:basename(File) == File of
+                true -> { error
+                        , fail( ann_pos(Ann)
+                              , "Illegal redefinition of standard library " ++ binary_to_list(File))};
+                %% If a path is provided then the stdlib takes lower priority
+                false -> {ok, binary_to_list(Bin)}
+            end;
        {_, {ok, Bin}} ->
            {ok, binary_to_list(Bin)};
        {{ok, Bin}, _} ->
@@ -145,8 +145,12 @@ decl(D, Options) ->
    with_options(Options, fun() -> decl(D) end).

 -spec decl(aeso_syntax:decl()) -> doc().
-decl({contract, _, C, Ds}) ->
-    block(follow(text("contract"), hsep(name(C), text("="))), decls(Ds));
+decl({contract, Attrs, C, Ds}) ->
+    Mod = fun({Mod, true}) when Mod == payable ->
+                  text(atom_to_list(Mod));
+             (_) -> empty() end,
+    block(follow( hsep(lists:map(Mod, Attrs) ++ [text("contract")])
+                , hsep(name(C), text("="))), decls(Ds));
 decl({namespace, _, C, Ds}) ->
    block(follow(text("namespace"), hsep(name(C), text("="))), decls(Ds));
 decl({pragma, _, Pragma}) -> pragma(Pragma);
@@ -155,13 +159,16 @@ decl({type_def, _, T, Vars, Def}) ->
    Kind = element(1, Def),
    equals(typedecl(Kind, T, Vars), typedef(Def));
 decl({fun_decl, Ann, F, T}) ->
+    Mod = fun({Mod, true}) when Mod == private; Mod == stateful; Mod == payable ->
+                  text(atom_to_list(Mod));
+             (_) -> empty() end,
    Fun = case aeso_syntax:get_ann(entrypoint, Ann, false) of
            true  -> text("entrypoint");
            false -> text("function")
          end,
-    hsep(Fun, typed(name(F), T));
+    hsep(lists:map(Mod, Ann) ++ [Fun, typed(name(F), T)]);
 decl(D = {letfun, Attrs, _, _, _, _}) ->
-    Mod = fun({Mod, true}) when Mod == private; Mod == stateful ->
+    Mod = fun({Mod, true}) when Mod == private; Mod == stateful; Mod == payable ->
                            text(atom_to_list(Mod));
             (_) -> empty() end,
    Fun = case aeso_syntax:get_ann(entrypoint, Attrs, false) of
@@ -257,6 +264,8 @@ type({args_t, _, Args}) ->
 type({bytes_t, _, any}) -> text("bytes(_)");
 type({bytes_t, _, Len}) ->
    text(lists:concat(["bytes(", Len, ")"]));
+type({if_t, _, Id, Then, Else}) ->
+    beside(text("if"), args_type([Id, Then, Else]));
 type({named_arg_t, _, Name, Type, _Default}) ->
    %% Drop the default value
    %% follow(hsep(typed(name(Name), Type), text("=")), expr(Default));
@@ -283,12 +292,9 @@ tuple_type(Factors) ->
      , text(")")
      ]).

-spec arg_expr(aeso_syntax:arg_expr()) -> doc().
-arg_expr({named_arg, _, Name, E}) ->
-    follow(hsep(expr(Name), text("=")), expr(E));
-arg_expr(E) -> expr(E).
-
-spec expr_p(integer(), aeso_syntax:expr()) -> doc().
+-spec expr_p(integer(), aeso_syntax:arg_expr()) -> doc().
+expr_p(P, {named_arg, _, Name, E}) ->
+    paren(P > 100, follow(hsep(expr(Name), text("=")), expr(E)));
 expr_p(P, {lam, _, Args, E}) ->
    paren(P > 100, follow(hsep(args(Args), text("=>")), expr_p(100, E)));
 expr_p(P, If = {'if', Ann, Cond, Then, Else}) ->
@@ -364,13 +370,19 @@ expr_p(_, {Type, _, Bin})
         Type == oracle_query_id ->
    text(binary_to_list(aeser_api_encoder:encode(Type, Bin)));
 expr_p(_, {string, _, <<>>}) -> text("\"\"");
-expr_p(_, {string, _, S}) -> term(binary_to_list(S));
+expr_p(_, {string, _, S}) ->
+    text(io_lib:format("\"~s\"", [binary_to_list(S)]));
 expr_p(_, {char, _, C}) ->
    case C of
        $' -> text("'\\''");
        $" -> text("'\"'");
-        _  -> S = lists:flatten(io_lib:format("~p", [[C]])),
-              text("'" ++ tl(lists:droplast(S)) ++ "'")
+        _ when C < 16#80 ->
+            S = lists:flatten(io_lib:format("~p", [[C]])),
+            text("'" ++ tl(lists:droplast(S)) ++ "'");
+        _  ->
+            S = lists:flatten(
+                  io_lib:format("'~ts'", [list_to_binary(aeso_scan:utf8_encode([C]))])),
+            text(S)
    end;
 %% -- Names
 expr_p(_, E = {id, _, _})   -> name(E);
@@ -442,7 +454,7 @@ prefix(P, Op, A) ->
 app(P, F, Args) ->
    paren(P > 900,
    beside(expr_p(900, F),
-           tuple(lists:map(fun arg_expr/1, Args)))).
+           tuple(lists:map(fun expr/1, Args)))).

 field({field, _, LV, E}) ->
    follow(hsep(lvalue(LV), text("=")), expr(E));
@@ -486,6 +498,3 @@ get_elifs(If = {'if', Ann, Cond, Then, Else}, Elifs) ->
    end;
 get_elifs(Else, Elifs) -> {lists:reverse(Elifs), {else, Else}}.

-fmt(Fmt, Args) -> text(lists:flatten(io_lib:format(Fmt, Args))).
-term(X) -> fmt("~p", [X]).
-
@@ -7,7 +7,7 @@
 %%%-------------------------------------------------------------------
 -module(aeso_scan).

-export([scan/1]).
+-export([scan/1, utf8_encode/1]).

 -import(aeso_scan_lib, [token/1, token/2, symbol/0, skip/0,
                        override/2, push/2, pop/1]).
@@ -28,7 +28,13 @@ lexer() ->
    QID      = ["(", CON, "\\.)+", ID],
    QCON     = ["(", CON, "\\.)+", CON],
    OP       = "[=!<>+\\-*/:&|?~@^]+",
-    CHAR     = "'([^'\\\\]|(\\\\.))'",
+    %% Five cases for a character
+    %%  * 1 7-bit ascii, not \ or '
+    %%  * 2-4 8-bit values (UTF8)
+    %%  * \ followed by a known modifier [aernrtv]
+    %%  * \xhh
+    %%  * \x{hhh...}
+    CHAR     = "'(([\\x00-\\x26\\x28-\\x5b\\x5d-\\x7f])|([\\x00-\\xff][\\x80-\\xff]{1,3})|(\\\\[befnrtv'\\\\])|(\\\\x[0-9a-fA-F]{2,2})|(\\\\x\\{[0-9a-fA-F]*\\}))'",
    STRING   = "\"([^\"\\\\]|(\\\\.))*\"",

    CommentStart = {"/\\*", push(comment, skip())},
@@ -77,34 +83,34 @@ scan(String) ->
 %% -- Helpers ----------------------------------------------------------------

 parse_string([$" | Chars]) ->
-    unescape(Chars).
+    unicode:characters_to_nfc_binary(unescape(Chars)).

-parse_char([$', $\\, Code, $']) ->
-    case Code of
-        $'  -> $';
-        $\\ -> $\\;
-        $b  -> $\b;
-        $e  -> $\e;
-        $f  -> $\f;
-        $n  -> $\n;
-        $r  -> $\r;
-        $t  -> $\t;
-        $v  -> $\v;
-        _   -> {error, "Bad control sequence: \\" ++ [Code]}
-    end;
-parse_char([$', C, $']) -> C.
+parse_char([$' | Chars]) ->
+    case unicode:characters_to_nfc_list(unescape($', Chars, [])) of
+        [Char] -> Char;
+        _Bad   -> {error, "Bad character literal: '" ++ Chars}
+    end.

-unescape(Str) -> unescape(Str, []).
+utf8_encode(Cs) ->
+    binary_to_list(unicode:characters_to_binary(Cs)).

-unescape([$"], Acc) ->
+unescape(Str) -> unescape($", Str, []).
+
+unescape(Delim, [Delim], Acc) ->
    list_to_binary(lists:reverse(Acc));
-unescape([$\\, $x, D1, D2 | Chars ], Acc) ->
+unescape(Delim, [$\\, $x, ${ | Chars ], Acc) ->
+    {Ds, [_ | Cs]} = lists:splitwith(fun($}) -> false ; (_) -> true end, Chars),
+    C = list_to_integer(Ds, 16),
+    Utf8Cs = binary_to_list(unicode:characters_to_binary([C])),
+    unescape(Delim, Cs, [Utf8Cs | Acc]);
+unescape(Delim, [$\\, $x, D1, D2 | Chars ], Acc) ->
    C = list_to_integer([D1, D2], 16),
-    unescape(Chars, [C | Acc]);
-unescape([$\\, Code | Chars], Acc) ->
-    Ok = fun(C) -> unescape(Chars, [C | Acc]) end,
+    Utf8Cs = binary_to_list(unicode:characters_to_binary([C])),
+    unescape(Delim, Chars, [Utf8Cs | Acc]);
+unescape(Delim, [$\\, Code | Chars], Acc) ->
+    Ok = fun(C) -> unescape(Delim, Chars, [C | Acc]) end,
    case Code of
-        $"  -> Ok($");
+        Delim -> Ok(Delim);
        $\\ -> Ok($\\);
        $b  -> Ok($\b);
        $e  -> Ok($\e);
@@ -115,8 +121,8 @@ unescape([$\\, Code | Chars], Acc) ->
        $v  -> Ok($\v);
        _   -> error("Bad control sequence: \\" ++ [Code])  %% TODO
    end;
-unescape([C | Chars], Acc) ->
-    unescape(Chars, [C | Acc]).
+unescape(Delim, [C | Chars], Acc) ->
+    unescape(Delim, Chars, [C | Acc]).

 strip_underscores(S) ->
    lists:filter(fun(C) -> C /= $_ end, S).
@@ -37,20 +37,26 @@
 -type decl() :: {contract, ann(), con(), [decl()]}
              | {namespace, ann(), con(), [decl()]}
              | {pragma, ann(), pragma()}
-              | {type_decl, ann(), id(), [tvar()]}
+              | {type_decl, ann(), id(), [tvar()]} % Only for error msgs
              | {type_def, ann(), id(), [tvar()], typedef()}
-              | {fun_decl, ann(), id(), type()}
-              | {fun_clauses, ann(), id(), type(), [letbind()]}
+              | {fun_clauses, ann(), id(), type(), [letfun() | fundecl()]}
              | {block, ann(), [decl()]}
-              | letbind().
+              | fundecl()
+              | letfun()
+              | letval(). % Only for error msgs

 -type compiler_version() :: [non_neg_integer()].

 -type pragma() :: {compiler, '==' | '<' | '>' | '=<' | '>=', compiler_version()}.

+
+-type letval()  :: {letval, ann(), pat(), expr()}.
+-type letfun()  :: {letfun, ann(), id(), [pat()], type(), expr()}.
+-type fundecl() :: {fun_decl, ann(), id(), type()}.
+
 -type letbind()
-    :: {letval, ann(), pat(), expr()}
-     | {letfun, ann(), id(), [pat()], type(), expr()}.
+    :: letfun()
+     | letval().

 -type arg() :: {arg, ann(), id(), type()}.

@@ -45,7 +45,6 @@ fold(Alg = #alg{zero = Zero, plus = Plus, scoped = Scoped}, Fun, K, X) ->
            %% decl()
            {contract, _, _, Ds}     -> Decl(Ds);
            {namespace, _, _, Ds}    -> Decl(Ds);
-            {type_decl, _, I, _}     -> BindType(I);
            {type_def, _, I, _, D}   -> Plus(BindType(I), Decl(D));
            {fun_decl, _, _, T}      -> Type(T);
            {letval, _, P, E}        -> Scoped(BindExpr(P), Expr(E));
@@ -95,6 +95,8 @@ from_fate({tuple_t, _, Types}, ?FATE_TUPLE(Val))
        when length(Types) == tuple_size(Val) ->
    {tuple, [], [from_fate(Type, X)
                 || {Type, X} <- lists:zip(Types, tuple_to_list(Val))]};
+from_fate({record_t, [{field_t, _, FName, FType}]}, Val) ->
+    {record, [], [{field, [], [{proj, [], FName}], from_fate(FType, Val)}]};
 from_fate({record_t, Fields}, ?FATE_TUPLE(Val))
        when length(Fields) == tuple_size(Val) ->
    {record, [], [ {field, [], [{proj, [], FName}], from_fate(FType, X)}
@@ -1,6 +1,6 @@
 {application, aesophia,
 [{description, "Contract Language for aeternity"},
-  {vsn, "4.2.0"},
+  {vsn, "5.0.0"},
  {registered, []},
  {applications,
   [kernel,
@@ -11,7 +11,10 @@ test_contract(N) ->
    {Contract,MapACI,DecACI} = test_cases(N),
    {ok,JSON} = aeso_aci:contract_interface(json, Contract),
    ?assertEqual([MapACI], JSON),
-    ?assertEqual({ok, DecACI}, aeso_aci:render_aci_json(JSON)).
+    ?assertEqual({ok, DecACI}, aeso_aci:render_aci_json(JSON)),
+    %% Check if the compiler provides correct aci
+    {ok,#{aci := JSON2}} = aeso_compiler:from_string(Contract, [{aci, json}]),
+    ?assertEqual(JSON, JSON2).

 test_cases(1) ->
    Contract = <<"payable contract C =\n"
@@ -80,11 +83,11 @@ test_cases(3) ->
    DecACI = <<"contract C =\n"
               "  type state = unit\n"
               "  datatype event = SingleEventDefined\n"
-	       "  datatype bert('a) = Bin('a)\n"
-	       "  entrypoint a : (C.bert(string)) => int\n">>,
+               "  datatype bert('a) = Bin('a)\n"
+               "  entrypoint a : (C.bert(string)) => int\n">>,
    {Contract,MapACI,DecACI}.

-%% Rounttrip
+%% Roundtrip
 aci_test_() ->
    [{"Testing ACI generation for " ++ ContractName,
      fun() -> aci_test_contract(ContractName) end}
@@ -94,8 +97,13 @@ all_contracts() -> aeso_compiler_tests:compilable_contracts().

 aci_test_contract(Name) ->
    String = aeso_test_utils:read_contract(Name),
-    Opts   = [{include, {file_system, [aeso_test_utils:contract_path()]}}],
+    Opts   = case lists:member(Name, aeso_compiler_tests:debug_mode_contracts()) of
+                 true  -> [debug_mode];
+                 false -> []
+             end ++ [{include, {file_system, [aeso_test_utils:contract_path()]}}],
    {ok, JSON} = aeso_aci:contract_interface(json, String, Opts),
+    {ok, #{aci := JSON1}} = aeso_compiler:from_string(String, [{aci, json}, {backend, fate} | Opts]),
+    ?assertEqual(JSON, JSON1),

    io:format("JSON:\n~p\n", [JSON]),
    {ok, ContractStub} = aeso_aci:render_aci_json(JSON),
@@ -122,4 +130,3 @@ check_stub(Stub, Options) ->
        _ = [ io:format("~s\n", [aeso_errors:pp(E)]) || E <- Errs ],
        error({parse_errors, Errs})
    end.
-
@@ -113,6 +113,7 @@ compilable_contracts() ->
     {"funargs", "traffic_light", ["Pantone(12)"]},
     {"funargs", "tuples", ["()"]},
     %% TODO {"funargs", "due", ["FixedTTL(1020)"]},
+     {"funargs", "singleton_rec", ["{x = 1000}"]},
     {"variant_types", "init", []},
     {"basic_auth", "init", []},
     {"address_literals", "init", []},
@@ -142,4 +143,4 @@ compilable_contracts() ->
 not_yet_compilable(fate) ->
    [];
 not_yet_compilable(aevm) ->
-    [].
+    ["funargs", "strings"].
@@ -39,7 +39,7 @@ simple_compile_test_() ->
                   error(ErrBin)
           end
       end} || ContractName <- compilable_contracts(), Backend <- [aevm, fate],
-               not lists:member(ContractName, not_yet_compilable(Backend))] ++
+               not lists:member(ContractName, not_compilable_on(Backend))] ++
    [ {"Test file not found error",
       fun() ->
           {error, Errors} = aeso_compiler:file("does_not_exist.aes"),
@@ -110,7 +110,15 @@ compile(Backend, Name) ->

 compile(Backend, Name, Options) ->
    String = aeso_test_utils:read_contract(Name),
-    case aeso_compiler:from_string(String, [{src_file, Name ++ ".aes"}, {backend, Backend} | Options]) of
+    Options1 =
+        case lists:member(Name, debug_mode_contracts()) of
+            true  -> [debug_mode];
+            false -> []
+        end ++
+        [ {src_file, Name ++ ".aes"}, {backend, Backend}
+        , {include, {file_system, [aeso_test_utils:contract_path()]}}
+        ] ++ Options,
+    case aeso_compiler:from_string(String, Options1) of
        {ok, Map}                                        -> Map;
        {error, ErrorString} when is_binary(ErrorString) -> ErrorString;
        {error, Errors}                                  -> Errors
@@ -146,6 +154,7 @@ compilable_contracts() ->
     "events",
     "include",
     "basic_auth",
+     "basic_auth_tx",
     "bitcoin_auth",
     "address_literals",
     "bytes_equality",
@@ -154,6 +163,7 @@ compilable_contracts() ->
     "bytes_to_x",
     "bytes_concat",
     "aens",
+     "aens_update",
     "tuple_match",
     "cyclic_include",
     "stdlib_include",
@@ -163,13 +173,26 @@ compilable_contracts() ->
     "payable",
     "unapplied_builtins",
     "underscore_number_literals",
+     "pairing_crypto",
     "qualified_constructor",
     "let_patterns",
-     "lhs_matching"
+     "lhs_matching",
+     "more_strings",
+     "protected_call",
+     "hermetization_turnoff"
    ].

-not_yet_compilable(fate) -> [];
-not_yet_compilable(aevm) -> [].
+not_compilable_on(fate) -> [];
+not_compilable_on(aevm) ->
+    [ "stdlib_include", "manual_stdlib_include", "pairing_crypto"
+    , "aens_update", "basic_auth_tx", "more_strings"
+    , "unapplied_builtins", "bytes_to_x", "state_handling", "protected_call"
+    , "hermetization_turnoff"
+
+    ].
+
+debug_mode_contracts() ->
+    ["hermetization_turnoff"].

 %% Contracts that should produce type errors

@@ -371,15 +394,19 @@ failing_contracts() ->
        [<<?Pos(12, 42)
           "Cannot unify int\n"
           "         and string\n"
-           "when checking the record projection at line 12, column 42\n"
-           "  r.foo : (gas : int, value : int) => Remote.themap\n"
+           "when checking the type of the expression at line 12, column 42\n"
+           "  r.foo() : map(int, string)\n"
           "against the expected type\n"
-           "  (gas : int, value : int) => map(string, int)">>])
-    , ?TYPE_ERROR(bad_include_and_ns,
-        [<<?Pos(2, 11)
-           "Include of 'included.aes' at line 2, column 11\nnot allowed, include only allowed at top level.">>,
-         <<?Pos(3, 13)
-           "Nested namespace not allowed\nNamespace 'Foo' at line 3, column 13 not defined at top level.">>])
+           "  map(string, int)">>])
+    , ?TYPE_ERROR(not_toplevel_include,
+                  [<<?Pos(2, 11)
+                     "Include of 'included.aes' at line 2, column 11\nnot allowed, include only allowed at top level.">>])
+    , ?TYPE_ERROR(not_toplevel_namespace,
+                  [<<?Pos(2, 13)
+                     "Nested namespaces are not allowed\nNamespace 'Foo' at line 2, column 13 not defined at top level.">>])
+    , ?TYPE_ERROR(not_toplevel_contract,
+        [<<?Pos(2, 12)
+           "Nested contracts are not allowed\nContract 'Con' at line 2, column 12 not defined at top level.">>])
    , ?TYPE_ERROR(bad_address_literals,
        [<<?Pos(11, 5)
           "Cannot unify address\n"
@@ -535,11 +562,15 @@ failing_contracts() ->
         "Cannot unify int\n         and string\nwhen checking the type of the pattern at line 2, column 53\n  x : int\nagainst the expected type\n  string">>
      ])
    , ?TYPE_ERROR(map_as_map_key,
-       [<<?Pos(5, 25)
+       [<<?Pos(5, 47)
         "Invalid key type\n"
         "  map(int, int)\n"
         "Map keys cannot contain other maps.">>,
-        <<?Pos(6, 25)
+        <<?Pos(6, 31)
+         "Invalid key type\n"
+         "  list(map(int, int))\n"
+         "Map keys cannot contain other maps.">>,
+        <<?Pos(6, 31)
         "Invalid key type\n"
         "  lm\n"
         "Map keys cannot contain other maps.">>])
@@ -612,6 +643,44 @@ failing_contracts() ->
         [<<?Pos(5, 28)
            "Invalid call to contract entrypoint 'Foo.foo'.\n"
            "It must be called as 'c.foo' for some c : Foo.">>])
+    , ?TYPE_ERROR(toplevel_let,
+                  [<<?Pos(2, 7)
+                     "Toplevel \"let\" definitions are not supported\n"
+                     "Value this_is_illegal at line 2, column 7 could be replaced by 0-argument function">>])
+    , ?TYPE_ERROR(empty_typedecl,
+                  [<<?Pos(2, 8)
+                     "Empty type declarations are not supported\n"
+                     "Type t at line 2, column 8 lacks a definition">>])
+    , ?TYPE_ERROR(higher_kinded_type,
+                  [<<?Pos(2, 35)
+                     "Type 'm is a higher kinded type variable\n"
+                     "(takes another type as an argument)">>])
+    , ?TYPE_ERROR(bad_arity,
+                  [<<?Pos(3, 20)
+                     "Arity for id doesn't match. Expected 1, got 0">>,
+                   <<?Pos(3, 25)
+                     "Cannot unify int\n"
+                     "         and id\n"
+                     "when checking the type of the expression at line 3, column 25\n"
+                     "  123 : int\n"
+                     "against the expected type\n"
+                     "  id">>,
+                   <<?Pos(4, 20)
+                     "Arity for id doesn't match. Expected 1, got 2">>,
+                   <<?Pos(4, 35)
+                     "Cannot unify int\n"
+                     "         and id(int, int)\n"
+                     "when checking the type of the expression at line 4, column 35\n"
+                     "  123 : int\n"
+                     "against the expected type\n"
+                     "  id(int, int)">>])
+    , ?TYPE_ERROR(bad_unnamed_map_update_default,
+                  [<<?Pos(4, 17)
+                     "Invalid map update with default">>])
+    , ?TYPE_ERROR(non_functional_entrypoint,
+                  [<<?Pos(2, 14)
+                     "f at line 2, column 14 was declared with an invalid type int.\n"
+                     "Entrypoints and functions must have functional types">>])
    , ?TYPE_ERROR(bad_records,
        [<<?Pos(3, 16)
           "Mixed record fields and map keys in\n"
@@ -623,6 +692,22 @@ failing_contracts() ->
           "Empty record/map update\n"
           "  r {}">>
        ])
+    , ?TYPE_ERROR(bad_protected_call,
+        [<<?Pos(6, 22)
+           "Invalid 'protected' argument\n"
+           "  (0 : int) == (1 : int) : bool\n"
+           "It must be either 'true' or 'false'.">>
+        ])
+    , ?TYPE_ERROR(bad_function_block,
+                  [<<?Pos(4, 5)
+                     "Mismatch in the function block. Expected implementation/type declaration of g function">>,
+                   <<?Pos(5, 5)
+                     "Mismatch in the function block. Expected implementation/type declaration of g function">>
+                  ])
+    , ?TYPE_ERROR(just_an_empty_file,
+                  [<<?Pos(0, 0)
+                     "Empty contract">>
+                  ])
    , ?TYPE_ERROR(bad_number_of_args,
                  [<<?Pos(3, 39)
                     "Cannot unify () => unit\n"
@@ -645,6 +730,9 @@ failing_contracts() ->
                     "  g : (int, string) => 'c\nto arguments\n"
                     "  \"Litwo, ojczyzno moja\" : string">>
                  ])
+    , ?TYPE_ERROR(bad_state,
+                  [<<?Pos(4, 16)
+                     "Conflicting updates for field 'foo'">>])
    ].

 -define(Path(File), "code_errors/" ??File).
@@ -798,6 +886,11 @@ validate(Contract1, Contract2) ->
    ByteCode = #{ fate_code := FCode } = compile(fate, Contract1),
    FCode1   = aeb_fate_code:serialize(aeb_fate_code:strip_init_function(FCode)),
    Source   = aeso_test_utils:read_contract(Contract2),
-    aeso_compiler:validate_byte_code(ByteCode#{ byte_code := FCode1 }, Source,
-                                     [{backend, fate}, {include, {file_system, [aeso_test_utils:contract_path()]}}]).
+    aeso_compiler:validate_byte_code(
+      ByteCode#{ byte_code := FCode1 }, Source,
+      case lists:member(Contract2, debug_mode_contracts()) of
+          true  -> [debug_mode];
+          false -> []
+      end ++
+      [{backend, fate}, {include, {file_system, [aeso_test_utils:contract_path()]}}]).

@@ -63,7 +63,8 @@ simple_contracts_test_() ->
     %% Parse tests of example contracts
     [ {lists:concat(["Parse the ", Contract, " contract."]),
        fun() -> roundtrip_contract(Contract) end}
-        || Contract <- [counter, voting, all_syntax, '05_greeter', aeproof, multi_sig, simple_storage, fundme, dutch_auction] ]
+        || Contract <- [counter, voting, all_syntax, '05_greeter', aeproof,
+                        multi_sig, simple_storage, fundme, dutch_auction, utf8] ]
    }.

 parse_contract(Name) ->
@@ -85,7 +86,7 @@ parse_expr(Text) ->
 round_trip(Text) ->
    Contract  = parse_string(Text),
    Text1     = prettypr:format(aeso_pretty:decls(strip_stdlib(Contract))),
-    Contract1 = parse_string(Text1),
+    Contract1 = parse_string(aeso_scan:utf8_encode(Text1)),
    NoSrcLoc  = remove_line_numbers(Contract),
    NoSrcLoc1 = remove_line_numbers(Contract1),
    ?assertMatch(NoSrcLoc, diff(NoSrcLoc, NoSrcLoc1)).
@@ -58,8 +58,7 @@ contract Greeter =

    let state = { greeting = "Hello" }

-    let setGreeting =
-        (greeting: string) =>
+    function setGreeting(greeting: string) =
            state{ greeting = greeting }


@@ -33,7 +33,22 @@ contract AENSTest =
                                sign : signature) : unit =
    AENS.claim(addr, name, salt, name_fee, signature = sign)

-  // TODO: update() -- how to handle pointers?
+
+  stateful entrypoint update(owner      : address,
+                             name       : string,
+                             ttl        : option(Chain.ttl),
+                             client_ttl : option(int),
+                             pointers   : option(map(string, AENS.pointee))) : unit =
+    AENS.update(owner, name, ttl, client_ttl, pointers)
+
+  stateful entrypoint signedUpdate(owner      : address,
+                                   name       : string,
+                                   ttl        : option(Chain.ttl),
+                                   client_ttl : option(int),
+                                   pointers   : option(map(string, AENS.pointee)),
+                                   sign       : signature) : unit =
+    AENS.update(owner, name, ttl, client_ttl, pointers, signature = sign)
+

  stateful entrypoint transfer(owner     : address,
                             new_owner : address,
@@ -0,0 +1,17 @@
+contract AENSUpdate =
+  stateful entrypoint update_name(owner : address, name : string) =
+    let p1 : AENS.pointee = AENS.AccountPt(Call.caller)
+    let p2 : AENS.pointee = AENS.OraclePt(Call.caller)
+    let p3 : AENS.pointee = AENS.ContractPt(Call.caller)
+    let p4 : AENS.pointee = AENS.ChannelPt(Call.caller)
+    AENS.update(owner, name, None, None,
+                Some({ ["account_pubkey"] = p1, ["oracle_pubkey"] = p2,
+                       ["contract_pubkey"] = p3, ["misc"] = p4 }))
+
+  entrypoint get_ttl(name : string) =
+    switch(AENS.lookup(name))
+     Some(AENS.Name(_, FixedTTL(ttl), _)) => ttl
+
+  entrypoint expiry(o : oracle(int, int)) : int =
+    Oracle.expiry(o)
+
@@ -1,44 +1,82 @@
 // Try to cover all syntactic constructs.
+@compiler > 0
+@compiler =< 10.1.1.1.1.1.2.3.4

-contract AllSyntaxType =
-  type typeDecl /* bla */
-  type paramTypeDecl('a, 'b)

+namespace Ns =
+  datatype d('a) = D | S(int) | M('a, list('a), int)
+  private function fff() = 123
+
+  stateful entrypoint
+    f (1, x) = (_) => x
+
+payable contract AllSyntaxType =
  /** Multi-
    * line
    * comment
    */
-  function foo : _
+  stateful function foo : _
+  entrypoint bar : int => (int * 'a)
+

 contract AllSyntax =

-  type typeDecl = int
-  type paramTypeDecl('a, 'b) = (('a, 'b) => 'b) => list('a) => 'b => 'b
+  datatype mickiewicz = Adam | Mickiewicz
+  record goethe('a, 'b) = {
+    johann : int,
+    wolfgang : 'a,
+    von : 'a * 'b * int,
+    goethe : unit
+    }
+  type dante = Ns.d(int)
+  type shakespeare('a) = goethe('a, 'a)

-  record nestedRecord = { x : int }
-  record recordType = { z : nestedRecord, y : int }
-  datatype variantType('a) = None | Some('a)
+  type state = shakespeare(int)

-  let valWithType : map(int, int) => option(int) = (m) => Map.get(m, 42)
-  let valNoType =
-        if(valWithType(Map.empty) == None)
-          print(42 mod 10 * 5 / 3)
+  entrypoint init() = {
+    johann = 1000,
+    wolfgang = -10,

-  function funWithType(x : int, y) : int * list(int) = (x, 0 :: [y] ++ [])
-  function funNoType() =
-    let foo = (x, y : bool) =>
-                if (! (y && x =< 0x0b || true)) [x]
-                else [11..20]
-    let setY(r : recordType) : unit = r{ y = 5 }
-    let setX(r : recordType, x : int) : recordType = r { z.x = x }  // nested record update
-    let getY(r) = switch(r) {y = y} => y
-    switch (funWithType(1, -2))
-      (x, [y, z]) => bar({x = z, y = -y + - -z * (-1)})
-      (x, y :: _) => ()
+/* TODO: This does not compile because of bug in the parser tester.
+    von = (2 + 2, 0, List.sum([x | k <- [1,2,3]
+                                 , let l = k + 1
+                                 , if(l < 10)
+                                 , let f(x) = x + 100
+                                 , Adam <- [Adam, Mickiewicz]
+                                 , let x = f(l)
+                                 ])),
+*/
+    von = (2 + 2, 0, List.sum([1,2,3,4])),
+    goethe = () }

-  let hash : address = #01ab0fff11
-  let b = false
-  let qcon = Mod.Con
-  let str = "blabla\nfoo"
-  let chr = '"'
+  function f() =
+     let kp = "nietzsche"
+     // let p = "Пушкин" // TODO: this also doesn't do right round_trip...
+     let k(x : bytes(8)) : bytes(8) = Bytes.to_int(#fedcba9876543210)

+     let f : () => address = () => ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt
+     if(Bits.test(Bits.all, 10))
+       abort("ohno")
+     if(true && false)
+       require(true, "ohyes")
+     elif(false || 2 == 2)
+       ()
+     else
+       ()
+     if(true) f(1,2)((1,2))
+     else switch(1::[1,2,3])
+       [] => 1
+       a::b => 123
+       1::2::3 => 123123
+       [2,3,4] => 1
+       _ => 13
+       1::[2] => 2138
+     put(state{johann = 1})
+     
+     let m = {["foo"] = 19, /*hey wanna talk about inlined comments?*/ ["bar"] = 42}
+     let n = {}
+     m{ ["x" = 0] @ z = z + state.johann }
+
+     let sh : shakespeare(shakespeare(int)) =
+       {wolfgang = state}
+     sh{wolfgang.wolfgang = sh.wolfgang} // comment
@@ -0,0 +1,4 @@
+contract C =
+  type id('a) = 'a
+  entrypoint f() : id = 123
+  entrypoint g() : id(int, int) = 123
@@ -0,0 +1,5 @@
+contract C =
+  function
+    g(1) = 2
+    f(2) = 3
+    h(1) = 123
@@ -0,0 +1,6 @@
+contract Remote =
+  entrypoint id : int => int
+
+contract ProtectedCall =
+  entrypoint bad(r : Remote) =
+    r.id(protected = 0 == 1, 18)
@@ -0,0 +1,5 @@
+contract C =
+  record state = { foo : int }
+  entrypoint init(i : int) =
+    state{ foo = i,
+           foo = 42 }
@@ -0,0 +1,5 @@
+contract C =
+  entrypoint f() =
+    let z = 123
+    {}{ [1 = 0] = z + 1 }
+    2
@@ -0,0 +1,74 @@
+// namespace Chain =
+//   record tx = { paying_for : option(Chain.paying_for_tx)
+//               , ga_metas : list(Chain.ga_meta_tx)
+//               , actor : address
+//               , fee   : int
+//               , ttl   : int
+//               , tx    : Chain.base_tx }
+
+//   datatype ga_meta_tx = GAMetaTx(address, int)
+//   datatype paying_for_tx = PayingForTx(address, int)
+//   datatype base_tx = SpendTx(address, int, string)
+//                    | OracleRegisterTx | OracleQueryTx | OracleResponseTx | OracleExtendTx
+//                    | NamePreclaimTx | NameClaimTx(hash) | NameUpdateTx(string)
+//                    | NameRevokeTx(hash) | NameTransferTx(address, string)
+//                    | ChannelCreateTx(address) | ChannelDepositTx(address, int) | ChannelWithdrawTx(address, int) |
+//                    | ChannelForceProgressTx(address) | ChannelCloseMutualTx(address) | ChannelCloseSoloTx(address)
+//                    | ChannelSlashTx(address) | ChannelSettleTx(address) | ChannelSnapshotSoloTx(address)
+//                    | ContractCreateTx(int) | ContractCallTx(address, int)
+//                    | GAAttachTx
+
+
+// Contract replicating "normal" Aeternity authentication
+contract BasicAuthTx =
+  record state = { nonce : int, owner : address }
+  datatype foo = Bar | Baz()
+
+  entrypoint init() = { nonce = 1, owner = Call.caller }
+
+  stateful entrypoint authorize(n : int, s : signature) : bool =
+    require(n >= state.nonce, "Nonce too low")
+    require(n =< state.nonce, "Nonce too high")
+    put(state{ nonce = n + 1 })
+    switch(Auth.tx_hash)
+      None          => abort("Not in Auth context")
+      Some(tx_hash) =>
+        let Some(tx0) = Auth.tx
+        let x : option(Chain.paying_for_tx) = tx0.paying_for
+        let x : list(Chain.ga_meta_tx) = tx0.ga_metas
+        let x : int = tx0.fee + tx0.ttl
+        let x : address = tx0.actor
+        let x : Chain.tx = { tx = Chain.NamePreclaimTx, paying_for = None, ga_metas = [],
+                             fee = 123, ttl = 0, actor = Call.caller }
+        switch(tx0.tx)
+          Chain.SpendTx(receiver, amount, payload) => verify(tx_hash, n, s)
+          Chain.OracleRegisterTx                   => false
+          Chain.OracleQueryTx                      => false
+          Chain.OracleResponseTx                   => false
+          Chain.OracleExtendTx                     => false
+          Chain.NamePreclaimTx                     => false
+          Chain.NameClaimTx(name)                  => false
+          Chain.NameUpdateTx(name)                 => false
+          Chain.NameRevokeTx(name)                 => false
+          Chain.NameTransferTx(to, name)           => false
+          Chain.ChannelCreateTx(other_party)       => false
+          Chain.ChannelDepositTx(channel, amount)  => false
+          Chain.ChannelWithdrawTx(channel, amount) => false
+          Chain.ChannelForceProgressTx(channel)    => false
+          Chain.ChannelCloseMutualTx(channel)      => false
+          Chain.ChannelCloseSoloTx(channel)        => false
+          Chain.ChannelSlashTx(channel)            => false
+          Chain.ChannelSettleTx(channel)           => false
+          Chain.ChannelSnapshotSoloTx(channel)     => false
+          Chain.ContractCreateTx(amount)           => false
+          Chain.ContractCallTx(ct_address, amount) => false
+          Chain.GAAttachTx                         => false
+
+  function verify(tx_hash, n, s) =
+    Crypto.verify_sig(to_sign(tx_hash, n), state.owner, s)
+
+  entrypoint to_sign(h : hash, n : int) =
+    Crypto.blake2b((h, n))
+
+  entrypoint weird_string() : string =
+    "\x19Weird String\x42\nMore\n"
@@ -1,4 +1,4 @@
-
+include "String.aes"
 contract BytesToX =

  entrypoint to_int(b : bytes(42)) : int = Bytes.to_int(b)
@@ -17,7 +17,7 @@ contract ChannelOnChainContractOracle =
      bets     = {}
      }

-  public stateful function place_bet(answer: string) = 
+  public stateful function place_bet(answer: string) =
    switch(Map.lookup(answer, state.bets))
      None =>
        put(state{ bets = state.bets{[answer] = Call.caller}})
@@ -25,6 +25,9 @@ contract ChannelOnChainContractOracle =
      Some(_value) =>
        "bet_already_taken"

+  public function expiry() =
+    Oracle.expiry(state.oracle)
+
  public function query_fee() =
    Oracle.query_fee(state.oracle)

@@ -35,7 +38,7 @@ contract ChannelOnChainContractOracle =
    switch(Oracle.get_answer(state.oracle, q))
      None         =>
        "no response"
-      Some(result) => 
+      Some(result) =>
        if(state.question == Oracle.get_question(state.oracle, q))
            switch(Map.lookup(result, state.bets))
              None         =>
@@ -0,0 +1,3 @@
+contract C =
+  type t
+  entrypoint f() = 123
@@ -1,4 +1,4 @@
-
+include "String.aes"
 contract FunctionArguments =

  entrypoint sum(n : int, m: int) =
@@ -45,3 +45,8 @@ contract FunctionArguments =

  entrypoint due(t : Chain.ttl) =
     true
+
+  record singleton_r = { x : int }
+
+  entrypoint singleton_rec(r : singleton_r) =
+    r.x
@@ -0,0 +1,11 @@
+namespace M =
+  function mf() = mg()
+  function mg() = mf()
+
+namespace N =
+  function nf() = ng() + M.mf() + M.mg()
+  private function ng() = nf() + M.mf() + M.mg()
+
+contract C =
+  entrypoint f() = N.ng() + N.nf() + g()
+  function g() = N.ng() + N.nf() + f()
@@ -0,0 +1,3 @@
+contract IWantToBelieve =
+  type stateT('s, 'm, 'a) = 's => 'm('a * 's)
+  entrypoint s() = 123
@@ -0,0 +1,14 @@
+include "String.aes"
+contract StringX =
+  entrypoint test() =
+    let s1 = "a string"
+    let s2 = "another string"
+    let s  = String.concat(s1, s2)
+    String.sha256(s)
+    String.length(s1)
+    String.from_list(String.to_list(s))
+    String.split(4, s1)
+    String.at(2, s2)
+    String.tokens(s, ",")
+    String.to_upper(s1)
+    String.to_lower(s2)
@@ -15,7 +15,7 @@ contract MultiSig =
      | OwnerRemoved (address)          // of { .removedOwner : Address }
      | ReqChanged   (int)             // of { .newReq : int }

-    let maxOwners : int = 250
+    function maxOwners() : int = 250

    record state = { nRequired    : int
                 , nOwners      : int
@@ -68,7 +68,7 @@ contract MultiSig =
      switch(check_pending(callhash()))
        CheckFail(state') => { state = state' }
        CheckOk(state') =>
-            if(state.nOwners >= maxOwners) () /* TODO */
+            if(state.nOwners >= maxOwners()) () /* TODO */
            else
              let nOwners' = state'.nOwners + 1
              { state = state' { owners    = Map.insert(nOwners', newOwner, state'.owners)
@@ -0,0 +1,5 @@
+contract C1 =
+  entrypoint f : int
+
+contract C =
+  entrypoint f() = 123
@@ -0,0 +1,6 @@
+namespace BadNs =
+  contract Con =
+    entrypoint e : () => int
+
+contract Con =
+  entrypoint foo() = 43
@@ -0,0 +1,5 @@
+namespace BadNs =
+  include "included.aes"
+
+contract Con =
+  entrypoint foo() = 43
@@ -1,5 +1,4 @@
-contract Bad =
-  include "included.aes"
+contract BadCon =
  namespace Foo =
    function foo() = 42

@@ -0,0 +1,30 @@
+include "BLS12_381.aes"
+
+contract GrothVerify =
+  type fr = BLS12_381.fr
+  type g1 = BLS12_381.g1
+  type g2 = BLS12_381.g2
+
+  record proof = { a : g1, b : g2, c : g1 }
+  record verify_key = { a : g1, b : g2, c : g2, d : g2, ic : list(g1) }
+
+  record state = { vk : verify_key }
+
+  entrypoint init(vk0 : verify_key) = {vk = vk0}
+
+  entrypoint verify_proof(p : proof, input : list(fr)) =
+    let vk = state.vk
+    let vk_x = calc_vk_x(vk.ic, input)
+
+    BLS12_381.pairing_check([BLS12_381.g1_neg(p.a), vk.a, vk_x, p.c],
+                            [p.b, vk.b, vk.c, vk.d])
+
+  function calc_vk_x(ics : list(g1), xs : list(fr)) =
+    switch(ics)
+      (ic :: ics) => calc_vk_x_(ic, ics, xs)
+
+  function calc_vk_x_(vk_x : g1, ics : list(g1), xs : list(fr)) =
+    switch((ics, xs))
+      ([], []) => vk_x
+      (ic :: ics, x :: xs) => calc_vk_x_(BLS12_381.g1_add(vk_x, BLS12_381.g1_mul(x, ic)), ics, xs)
+
@@ -0,0 +1,14 @@
+contract Remote =
+  entrypoint id : int => int
+
+contract ProtectedCall =
+
+  function higher_order(r : Remote) =
+    r.id
+
+  entrypoint test_ok(r : Remote) =
+    let f = higher_order(r)
+    let Some(n) = r.id(protected = true, 10)
+    let Some(m) = f(protected = true, 5)
+    n + m + r.id(protected = false, 100) + f(1)
+
@@ -1,3 +1,4 @@
+include "String.aes"
 contract Remote =
  record rstate = { i : int, s : string, m : map(int, int) }

@@ -1,3 +1,4 @@
+include "String.aes"
 contract Strings =
    entrypoint str_len(s) = String.length(s)
    entrypoint str_concat(s1, s2) = String.concat(s1, s2)
@@ -0,0 +1,3 @@
+contract C =
+  let this_is_illegal = 2/0
+  entrypoint this_is_legal() = 2/0
@@ -7,6 +7,7 @@
 //    AENS.transfer
 //    AENS.revoke
 //    Oracle.extend
+include "String.aes"
 contract UnappliedBuiltins =
  entrypoint main() = ()
  type o = oracle(int, int)
@@ -21,6 +22,7 @@ contract UnappliedBuiltins =
  function b_abort()                     = abort
  function b_require()                   = require
  function oracle_query_fee()            = Oracle.query_fee
+  function oracle_expiry()               = Oracle.expiry
  stateful function oracle_query()       = Oracle.query        : (o, _, _, _, _) => _
  function oracle_get_question()         = Oracle.get_question : (o, _) => _
  function oracle_get_answer()           = Oracle.get_answer   : (o, _) => _
@@ -0,0 +1,21 @@
+contract UTF8 =
+  entrypoint f1() : char = '1'
+  entrypoint f2() : char = '+'
+  entrypoint f3() : char = 'd'
+  entrypoint f4() : char = 'X'
+  entrypoint f5() : char = 'å'
+  entrypoint f6() : char = 'Ä'
+  entrypoint f7() : char = 'æ'
+  entrypoint f8() : char = 'ë'
+  entrypoint f9() : char = 'ẻ'
+  entrypoint f10() : char = '\x27'
+  entrypoint f11() : char = '\x{2200}'
+  entrypoint f12() : char = '💩'
+  entrypoint f13() : char = '\n'
+
+
+
+  // entrypoint f13() : char = 'e̊'
+  // entrypoint f14() : char = '\Ì'
+
+  // '💩' vs. map('a,'b)
@@ -1,16 +1,3 @@
-
-/* Contract type */
-contract VotingType =
-  type state
-  function init            : list(string) => state
-
-  function giveRightToVote : address => unit
-  function delegate        : address => unit
-  function vote            : int => unit
-  function winnerName      : unit => string
-  function currentTally    : unit => list(string * int)
-
-/* Contract implementation */
 contract Voting =

  // Types
Author	SHA1	Message	Date
Hans Svensson	6858329faa	Merge pull request #309 from aeternity/prepare_5.0.0 Preparing v5.0.0	2021-04-30 15:17:48 +02:00
Hans Svensson	c2a3e333c7	Preparing v5.0.0	2021-04-30 14:48:37 +02:00
Hans Svensson	4787830861	Merge pull request #308 from aeternity/merge_lima_to_master Merge lima to master	2021-04-30 14:43:16 +02:00
Hans Svensson	a0111066e7	Merge branch 'lima' into merge_lima_to_master	2021-04-30 14:07:06 +02:00
Hans Svensson	2311d19602	Merge pull request #291 from aeternity/GH-3282-aens_pointers_cleanup Add note about legacy (Lima) AENS pointers in update/lookup	2021-04-15 10:26:56 +02:00
Radosław Rowicki	3b2ce63fa7	Merge pull request #300 from aeternity/erlps-lima Trampoline in parser	2021-03-08 13:33:34 +01:00
radrow	8b4a1aaf0d	Trampoline	2021-03-08 12:45:21 +01:00
Radosław Rowicki	c6e7db2381	Merge pull request #299 from aeternity/fix-ets Fix constraints ordering	2021-03-05 10:42:16 +01:00
radrow	4e60d019ca	Fix constraints ordering	2021-02-23 11:05:02 +01:00
Radosław Rowicki	b8002029cf	Merge pull request #294 from aeternity/mergesort Upgrade sorting function	2021-02-23 08:58:36 +01:00
radrow	1a14602f36	Upgrade sorting function	2021-02-09 14:18:42 +01:00
Hans Svensson	e2ef95d6fd	Merge pull request #293 from aeternity/GH-292-desugar_error Properly handle type errors during desugar	2021-02-05 11:14:47 +01:00
Hans Svensson	22aaeceba8	Properly handle type errors during desugar	2021-01-25 21:28:10 +01:00
Hans Svensson	2a78189f31	Add note about legacy (Lima) AENS pointers in update/lookup	2021-01-07 12:14:04 +01:00
Radosław Rowicki	f1d95484a5	Merge pull request #288 from aeternity/expose-interface-fix-lima Fix interface exposure (lima)	2020-10-21 14:01:21 +02:00
Radosław Rowicki	4504fb8dcf	Merge pull request #286 from aeternity/expose-interface-fix Fix interface exposure (master)	2020-10-21 14:00:48 +02:00
radrow	7e65f26211	Fix interface exposure	2020-10-21 12:42:42 +02:00
radrow	8798e0b2c9	Fix interface exposure	2020-10-21 12:40:13 +02:00
Radosław Rowicki	1dfc349065	Merge pull request #285 from aeternity/lima-master-merge Lima master merge	2020-10-15 19:50:48 +02:00
radrow	1266d9ea99	Fix one test2	2020-10-13 10:42:38 +02:00
radrow	bbb049cb2e	Merge branch 'lima' into lima-master-merge	2020-10-13 10:33:30 +02:00
radrow	787551b8bc	Fix one test	2020-10-13 10:29:14 +02:00
radrow	ac673602b9	Merge branch 'lima' into master	2020-10-13 10:22:05 +02:00
Radosław Rowicki	0b83422189	Merge pull request #284 from aeternity/hermetization-turnoff Debug mode to turn off hermetization	2020-10-12 13:17:40 +02:00
radrow	1a5017ce2b	Debug mode turns off hermetization Added tests and fixed bugs	2020-10-09 18:41:30 +02:00
Hans Svensson	079b3a45c9	Merge pull request #283 from aeternity/GH-3002-blockhash_at_current_height Document Chain.block_hash at current height	2020-10-08 10:48:41 +02:00
Hans Svensson	c0d9759e60	Whitespace fixes	2020-10-07 16:53:24 +02:00
Hans Svensson	b7b242bc66	Document the (changed) behavior of Chain.block_hash	2020-10-07 16:53:10 +02:00
Grzegorz Uriasz	25fa365c29	Merge pull request #280 from aeternity/optionally_generate_aci Provide the ACI along with the bytecode	2020-09-10 10:05:51 +02:00
Grzegorz Uriasz	bb728db51b	Provide the ACI along with the bytecode	2020-09-09 18:39:02 +02:00
Grzegorz Uriasz	1fee306daa	Merge pull request #279 from aeternity/optimize_calldata_generation Improve call data encoding times by 35%	2020-09-09 15:50:36 +02:00
Grzegorz Uriasz	c4eaf2249a	Don't regenerate the AST	2020-09-09 15:33:34 +02:00
Hans Svensson	6c23fd0d41	Merge pull request #278 from aeternity/contains-fun Added `contains` functions in List and Option. Fixed one type error	2020-08-27 11:25:38 +02:00
radrow	3d73e52d48	Fix tests	2020-08-26 15:56:21 +02:00
radrow	89b3ec3d17	minor optimization	2020-08-26 12:10:24 +02:00
radrow	7e32ef57c2	Added `contains` functions in List and Option. Fixed one type error catch	2020-08-26 11:56:18 +02:00
Hans Svensson	ed5447e430	Merge pull request #273 from aeternity/GH272-singleton_record_calldata_decode Fix singleton record calldata decode + test	2020-08-11 07:58:36 +02:00
Hans Svensson	db4de5d926	Fix singleton record calldata decode + test	2020-08-10 16:37:09 +02:00
Radosław Rowicki	6b60fde2df	Merge pull request #267 from aeternity/option-fix Fixed `force` function	2020-06-18 15:05:55 +02:00
Radosław Rowicki	dd8eea0d55	Merge pull request #261 from aeternity/fixes Ban empty contracts, ban function blocks with mismatched declarations	2020-06-07 18:01:03 +02:00
Radosław Rowicki	eb71abc665	Fixed `force` function	2020-06-06 14:36:46 +02:00
Hans Svensson	eff1ad4688	Merge pull request #265 from aeternity/improve_docs Make the network id an explicit part of the signature material	2020-06-05 13:00:42 +02:00
Hans Svensson	cb2588fae2	Make the network id an explicit part of the signature material	2020-05-29 08:47:01 +02:00
Hans Svensson	08261a319b	Merge pull request #264 from aeternity/update_readme Make README less outdated	2020-05-29 08:45:23 +02:00
Hans Svensson	f21717a9c0	Make README less outdated	2020-05-29 08:35:19 +02:00
Hans Svensson	9753f90034	Merge pull request #262 from aeternity/fix_types Fix AENS types + whitespace	2020-05-27 08:10:18 +02:00
Hans Svensson	8f240a7ddf	Fix AENS types + whitespace	2020-05-27 08:06:06 +02:00
radrow	54e43764ca	Ban empty contracts, ban function blocks with mismatched declarations	2020-05-15 19:09:08 +02:00
Hans Svensson	05b87fe200	Merge pull request #259 from kryptokrauts/master fix param description for AENS interface	2020-05-07 16:07:10 +02:00
Marco Walz	cc07e3a638	fix param description for AENS interface	2020-05-05 11:21:27 +02:00
Radosław Rowicki	ea5850cf93	Merge pull request #256 from radrow/master Merge lima – 4.3.0	2020-04-30 13:52:50 +02:00
radrow	d2dcb9e249	Add AENS example, readd delegation signature chapter, fix links	2020-04-30 00:02:26 +02:00
radrow	adb3cf5406	Update documentation to master	2020-04-29 15:27:40 +02:00
radrow	ad78f440d9	Merge lima	2020-04-02 15:32:26 +02:00
Radosław Rowicki	962ddf5303	Version push – 4.3.0 (#255 ) * Version push – 4.3.0 . * Fixed ordering of diffs in CHANGELOG	2020-04-02 15:10:53 +02:00
Radosław Rowicki	85b151aa65	Prepare 4.3.0 (#254 )	2020-04-02 13:59:22 +02:00
Radosław Rowicki	93341dc13b	Prepared for REPL usage (#218 ) * Prepared for REPL usage Exposed expr parsing ets init in constant Exposing and fixing exposed expr This will be squashed either Expose letdef Error handling exposed autoimport remove unnecessary changes Fix types Parser update Expose body parser remove map_get warning make dialyzer happy * Formatting Co-Authored-By: Hans Svensson <hanssv@gmail.com> Co-authored-by: Hans Svensson <hanssv@gmail.com>	2020-04-02 12:29:14 +02:00
Radosław Rowicki	98036eff65	Update TOC in sophia.md (#245 )	2020-04-01 13:11:02 +02:00
Radosław Rowicki	dc977f7354	Fixed example (#249 )	2020-03-31 13:14:13 +02:00
Radosław Rowicki	4f554acee6	Fix error messages for some illegal constructions, fix absolute path includes (#251 ) * Updated tests, banned type decls and toplevel letvals * Properly ban nested contracts * Fix including by path * Fix error message test * Fix prettpr attr display. Make dialyzer happy * More tests * Fixed type printing * Updated docs	2020-03-30 14:52:16 +02:00
Radosław Rowicki	48b52cb501	Enchanted Frac library a bit (#253 )	2020-03-29 17:14:01 +02:00
Ulf Norell	515838e2f9	Handle negative numbers in aci (#247 ) * Handle negative numbers in aci Fixes aeternity/aesophia_http#59 * Updated CHANGELOG Updated CHANGELOG1 Co-authored-by: radrow <radrowicki@gmail.com>	2020-03-23 18:11:00 +01:00
Ulf Norell	42cd47d1b3	Merge pull request #241 from aeternity/GH-203-protected-calls Add support for protected contract calls	2020-03-02 16:15:05 +01:00
Ulf Norell	93d2086ddf	aebytecode commit	2020-03-02 12:08:41 +01:00
Ulf Norell	9487b79f42	Fix dialyzer complaints	2020-03-02 12:08:41 +01:00
Ulf Norell	e64ac9396a	Test cases for protected calls	2020-03-02 12:08:41 +01:00
Ulf Norell	4a812b6f3b	Error message tweaks	2020-03-02 11:35:55 +01:00
Ulf Norell	fe2d93ea8a	Compile protected calls to CALL_PGR	2020-03-02 11:35:55 +01:00
Ulf Norell	ecbc15db1b	Add 'protected' named argument to remote calls If protected = true, the return type is wrapped in an option() which comes back None if the remote call fails for any reason.	2020-03-02 08:51:33 +01:00
Hans Svensson	d0caee24d9	Merge pull request #240 from aeternity/GH-176-additional_documentation Add some comments to String.aes	2020-02-28 11:16:38 +01:00
Hans Svensson	57eb77f2f8	Add some comments to String.aes	2020-02-28 11:07:02 +01:00
Hans Svensson	53ed60b498	Merge pull request #238 from aeternity/GH-176-more_string_functions Change Char.to_lower/upper into String.to_lower/upper	2020-02-26 20:01:10 +01:00
Hans Svensson	e49738c90c	New aebytecode reference	2020-02-26 18:23:12 +01:00
Hans Svensson	a38a365181	Change Char.to_lower/upper into String.to_lower/upper	2020-02-26 14:15:49 +01:00
Hans Svensson	0dddac3d86	Merge pull request #236 from aeternity/GH-176-more_string_functions Gh 176 more string functions	2020-02-25 09:49:00 +01:00
Hans Svensson	3da694e798	New aebytecode commit hash	2020-02-25 09:02:18 +01:00
Hans Svensson	e98edd4eef	Handle UTF-8 in character literals Also handle `\x{hhh..}` in strings... Character literals has to be a single character, not composite. + tests (and the corresponding fix to the char literal pretty printer)	2020-02-24 15:35:54 +01:00
Hans Svensson	2bad76314f	More efficient implementations in String.aes	2020-02-24 15:34:23 +01:00
Hans Svensson	b9acf24dca	Make String.aes a stdlib + add more string functions This means moving the FATE operations to StringInternal and adding to/from_list (and Char.to/from_int + Char.to_upper/lower).	2020-02-21 09:45:11 +01:00
Hans Svensson	6682b24156	Merge pull request #223 from aeternity/GH-202-Auth_tx_introspection Gh 202 auth tx introspection	2020-02-11 15:48:46 +01:00
Hans Svensson	b31be6227d	Update aebytecode reference	2020-02-11 14:20:41 +01:00
Hans Svensson	bbc8555331	Auth.tx implementation and types The arities field of the Chain.base_tx constructor is 22 integers long... This isn't very pretty but that is the design we've chosen.	2020-02-11 10:00:46 +01:00
Radosław Rowicki	13bc821211	Optimize stdlib (#215 )	2020-02-07 19:51:12 +01:00
Hans Svensson	34c10e1518	Merge pull request #214 from aeternity/GH-188-AENS_lookup Add AENS.lookup and Oracle.expiry	2020-02-03 14:37:55 +01:00
Hans Svensson	bb79e7dd89	Update aebytecode reference	2020-02-03 14:26:13 +01:00
Hans Svensson	c3426f0e65	Add AENS.lookup Also move Pointee-constructors inside AENS namespace.	2020-02-03 12:52:00 +01:00
Hans Svensson	db01e237c1	Add Oracle.expiry	2020-02-03 12:24:27 +01:00
Hans Svensson	760d2841d1	From Iris (with AENS.update) AENS.resolve is not Pure	2020-02-03 12:22:34 +01:00
Hans Svensson	43013ec920	Merge pull request #213 from aeternity/merge_lima_to_master Merge lima to master	2020-01-15 15:54:41 +01:00
Hans Svensson	d821de6381	Merge 'origin/lima' into 'origin/master'	2020-01-15 15:03:11 +01:00
Hans Svensson	282f743925	Merge pull request #209 from aeternity/merge_lima_to_master Merge lima to master	2019-12-19 15:34:26 +01:00
Hans Svensson	cf1072140e	Merge 'origin/lima' into merge_lima_to_master	2019-12-19 15:09:48 +01:00
Hans Svensson	75797686ad	Merge pull request #187 from aeternity/GH-2850-add_fancy_crypto_bls12_381 Add BLS12-381 operations (to FATE)	2019-11-29 15:27:38 +01:00
Tino Breddin	ed9384c2af	Merge pull request #185 from aeternity/tb-rebar-lock-check Add CI check to verify rebar.lock	2019-11-27 17:28:31 +01:00
Hans Svensson	1c24a700dc	Add BLS12-381 operations (to FATE)	2019-11-27 10:57:24 +01:00
Hans Svensson	f2e9fbcc51	Merge pull request #186 from aeternity/merge_lima Merge lima into master	2019-11-27 10:50:29 +01:00
Hans Svensson	2d49426fe0	Merge 'origin/lima' into master	2019-11-27 10:46:18 +01:00
Tino Breddin	f5df2c1a5f	Add CI workflow	2019-11-26 17:27:26 +01:00
Tino Breddin	04445e4dee	Add CI check to verify rebar.lock	2019-11-26 17:24:02 +01:00
Ulf Norell	eec70f03a5	Merge pull request #183 from aeternity/lima Merge lima into master	2019-11-25 13:16:17 +01:00
skkw	c2c8e297ae	Merge pull request #178 from aeternity/PT-158904718-aens-update-sophia changed type of client ttl to int option	2019-11-18 18:39:54 +01:00
skkw	5c5d3c60ef	changed type of client ttl to int option	2019-11-18 16:25:47 +01:00
Ulf Norell	2a3274ba25	Merge pull request #175 from aeternity/GH-174-encode-decode-bits Handle encoding/decoding bits	2019-11-18 12:12:45 +01:00
Ulf Norell	13b7bde44b	Prefix format annotation for negative numbers	2019-11-18 11:55:04 +01:00
Ulf Norell	baf527b5fa	Handle encoding/decoding bits Fixes GH-174	2019-11-18 11:35:08 +01:00
skkw	422baa5b65	Merge pull request #155 from aeternity/PT-158904718-aens-update-sophia support for AENS.update call	2019-11-12 14:49:42 +01:00
skkw	126e04ae42	support for AENS.update call	2019-11-12 14:27:46 +01:00