diff --git a/docs/aevm_01_abi.md b/docs/aevm_01_abi.md
new file mode 100644
index 0000000..dcc6700
--- /dev/null
+++ b/docs/aevm_01_abi.md
@@ -0,0 +1,229 @@
+## The Sophia\_AEVM\_01 ABI
+
+### Byte code
+
+The byte code contains meta data about the original sophia source
+code.
+
+#### Meta data
+The byte code contains meta data for the contract.
+- source_code_hash - a Blake2b hash of the source code string of the contract
+- type_info - see Type information below
+- byte_code - the actual byte code
+
+The layout of the encoding can be found
+[here](https://github.com/aeternity/protocol/blob/master/serializations.md#sophia-byte-code).
+The encoding is tagged with the compiler version.
+
+#### Type information
+The type information of each function is encoded in the meta data. The function
+hash depends both on the function name and the type signature of the function.
+The function hash is also the identifier of a function when calling a contract.
+In this way, the function prototype in the calling function gets some level of
+type verification.
+
+The type information contains:
+- fun_hash - A Blake2b hash of the function name and the function types
+- fun_name - The function name as a string
+- arg_type - The vm encoded typerep of the argument (as a tuple) of the function
+- out_type - The vm encoded typerep of the return type of the function
+
+### Memory layout
+
+Sophia values are 256-bit words. In case of unboxed types (`int`,
+`address`, and `bool`) this is simply the value. For boxed types
+such as tuples and (non-empty) lists, the word is a pointer into the heap
+(memory).
+
+More precisely
+
+- Unboxed types are represented as a single big endian 256-bit (32 bytes) word.
+ Booleans are represented as 0 for `false` and 1 for `true`. The empty list is
+ represented as an unboxed -1. In memory maps are represented by an unboxed
+ unique identifier. The contents of the map is stored separately in the VM
+ state.
+
+- Boxed types are represented as a 256-bit pointer to a contiguous sequence of
+ words, called a *heap object*, on the heap.
+
+ | Value/Type | Heap object
+ | --- | ---
+ | Tuple | The value of each component in left-to-right order.
+ | String | The length (number of bytes), followed by as many words as required to store the character data, padded on the right with 0.
+
+ The following types are represented in terms of other types:
+
+
+ Type | Representation |
+ Non-empty list | A pair of the head and the tail. |
+ Record | A tuple of the field values. |
+ Data type |
+ A tuple where the first component is a constructor
+ tag (starting with 0 for the first constructor), and the following
+ components are the constructor arguments. For instance, for
+ datatype zeroOrTwo = Zero | Two(int, int)
+ Zero is encoded as a singleton tuple (0) and
+ Two(a, b) as the triple (1, a, b).
+ |
+ Signature | A pair of two 256-bit words. |
+ Option types | datatype option('a) = None | Some('a). |
+ ttl | datatype ttl = RelativeTTL(int) | FixedTTL(int) |
+ Type representations |
+
+ When types need to be encoded as data, they are represented as the following datatype
+
+
+ datatype typerep = Word // any unboxed type
+ | String
+ | List(typerep)
+ | Tuple(list(typerep))
+ | Datatype(list(list(typerep)))
+ | TypeRep
+ | Map(typerep, typerep)
+
+ The argument to the Datatype constructor is the list of type
+ representations of the constructor arguments.
+ |
+
+
+### Encoding Sophia values as binaries
+
+When communicating Sophia values between a contract and the outside world they
+are encoded as a binary containing a heap whose first word is the encoded value
+(except in the case of maps, see below). For example, the value `("main", (1, 2, 3))`
+can be encoded as
+```
+Word 0 1 2 3 4 5 6 7
+Addr 0x00 0x20 0x40 0x60 0x80 0xA0 0xC0 0xE0
+Value 0x20 0x60 0xA0 4 "main" 1 2 3
+```
+where `"main"` is the 32 byte word obtained by right padding the string
+`"main"` with zeroes.
+
+Note that the order of the heap objects on the heap is unspecified. Another
+valid encoding of the same value is
+```
+Word 0 1 2 3 4 5 6 7
+Addr 0x00 0x20 0x40 0x60 0x80 0xA0 0xC0 0xE0
+Value 0x60 4 "main" 0x20 0xA0 1 2 3
+```
+
+A canonical binary representation is obtained by storing heap objects in
+depth-first left-to-right order (as in the first example). This is the
+representation used in map keys.
+
+#### Binary encoding of Sophia maps
+
+In memory, maps are represented by their unique identifier, but in binary
+encodings the identifier is replaced by a boxed representation with a heap
+object of the shape
+```
+ MapSize (N)
+ KeySize1
+ +----------+
+ | Key1 |
+ +----------+
+ ValSize1
+ +----------+
+ | Val1 |
+ +----------+
+ ...
+ KeySizeN
+ +----------+
+ | KeyN |
+ +----------+
+ ValSizeN
+ +----------+
+ | ValN |
+ +----------+
+```
+The keys and values are encoded as standalone binaries, so the addresses in
+`KeyI` (say) are relative only to the `KeyI` binary.
+
+### Initialization
+
+When a Sophia contract is called the calldata should be a pair of a function
+hash and a tuple of arguments, encoded as a binary as described above
+The value should be a pair of a function hash and a tuple of arguments
+For instance, to call the function `foo` (assuming the function
+hash 12345) with arguments `1` and `"bar"`, the calldata should be
+(the binary encoding of)
+```
+ (12345, (1, "bar"))
+```
+Before the contract starts executing the first word of the encoded calldata
+(i.e. the calldata value) is pushed on the stack and the rest of the calldata
+heap is written to memory. The result is that the Sophia contract starts with
+the value of the calldata on top of the stack.
+
+If the contract state has been initialized it is stored on the heap and a
+pointer to it is written to address 0. If the contract state has not been
+initialized, for instance, when running the `init` function, 0 is written to
+address 0. Note that address 0 contains a *pointer* to the value of the state,
+not the value itself.
+
+The compiler is responsible for generating the appropriate dispatch code,
+looking at the calldata and calling the correct function.
+
+### Return
+
+When returning from a contract call (using the `RETURN` instruction) the
+type information from the meta data is used to encode the return value.
+The VM reads the return value from the heap and returns it to the caller,
+and reads the updated contract state using the state pointer at address 0.
+A contract can write 0 to the state pointer to indicate that the state
+did not change.
+
+### Storing the contract state
+
+The contract state is stored in the *store* as a binary heap whose first word
+is the value (with maps stored as their identifiers) under key `0x00`.
+The type of the state is stored as an encoded type representation under key
+`0x01` (***subject to change: contract state type to be stored in contract
+metadata***). The list of maps in the contract state is stored under key `0x02`
+as a sequence of 256-bit map identifiers. For each map there are mappings
+(where `[X]` denotes a single 256-bit word):
+```
+ [MapId] => [RealId] [RefCount] [Size] Types
+ [RealId] Key => Val
+```
+`Types` is the binary encoding of the tuple `(KeyType, ValType)` of type
+representations for the key and value types of the map. `Key` and `Val` are
+stand-alone heap encodings with map identifiers for maps (although for keys
+there are no maps). The `RealId` field is an indirection to allow in-place
+updates of maps and the `RefCount` field is used to track the number of
+occurrences of a map in other maps for the purpose of garbage collection.
+
+The `init` function of a contract should return a pair of the state type
+representation and the initial state, which are written to the store by the VM.
+Note that the Sophia code for `init` only returns the initial state value--the
+compiler is responsible for adding the type representation.
+
+### Remote contract calls
+
+The `CALL` instruction for calling another contract works differently for
+Sophia contracts than in the EVM. It expects on the stack (top to bottom):
+- `Gas` - the amount of gas to allocate to the call
+- `Address` - the address of the contract to call (or 0 for primops)
+- `Amount` - the amount of tokens to transfer with the call
+- `Calldata` - the calldata value (pair of function hash and arguments)
+- `TypeHash` - the function hash of primops that have dynamic types
+ (e.g., oracles). Otherwise unused.
+- `_` - unused (offset to write return value in the EVM)
+- `_` - unused (return value size in the EVM)
+
+The calldata is read from the heap guided by the calldata type and passed to
+the called contract. Before the call is made gas is charged for the size of the
+expanded calldata (e.g. maps have to be made explicit when passed between
+contracts). When the call returns the return value is pushed on top of the
+stack, and potential heap objects for the return value written to the top of
+the heap. The return type from the contracts meta data is used when writing it
+ to the heap. Since maps are handled outside the heap, the caller explicitly
+pays gas for handling maps in the return value.
+
+### Delegation signature
+Some chain operations (`Oracle.` and `AENS.`) has 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.).
diff --git a/docs/sophia.md b/docs/sophia.md
new file mode 100644
index 0000000..b05cbc0
--- /dev/null
+++ b/docs/sophia.md
@@ -0,0 +1,1006 @@
+[back](./contracts.md)
+## The Sophia Language
+An Æternity BlockChain Language
+
+The Sophia is a language in the ML family. It is strongly typed and has
+restricted mutable state.
+
+Sophia is customized for smart contracts, which can be published
+to a blockchain (the Æternity BlockChain). Thus some features of conventional
+languages, such as floating point arithmetic, are not present in Sophia, and
+some blockchain specific primitives, constructions and types have been added.
+## Language Features
+### Contracts
+
+The main unit of code in Sophia is the *contract*.
+
+- A contract implementation, or simply a contract, is the code for a
+ smart contract and consists of a list of types, entrypoints and local
+ functions. Only the entrypoints can be called from outside the contract.
+- A contract instance is an entity living on the block chain (or in a state
+ channel). Each instance has an address that can be used to call its
+ entrypoints, either from another contract or in a call transaction.
+- 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 primive 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.
+
+#### Calling other contracts
+
+To call a function in another contract you need the address to an instance of
+the contract. The type of the address must be a contract type, which consists
+of a number of type definitions and entrypoint declarations. For instance,
+
+```javascript
+// A contract type
+contract VotingType =
+ entrypoint vote : string => unit
+```
+
+Now given contract address of type `VotingType` you can call the `vote`
+entrypoint of that contract:
+
+```javascript
+contract VoteTwice =
+ entrypoint voteTwice(v : VotingType, alt : string) =
+ v.vote(alt)
+ v.vote(alt)
+```
+
+Contract calls take two optional named arguments `gas : int` and `value : int`
+that lets you set a gas limit and provide tokens to a contract call. If omitted
+the defaults are no gas limit and no tokens. Suppose there is a fee for voting:
+
+```javascript
+ entrypoint voteTwice(v : VotingType, fee : int, alt : string) =
+ v.vote(value = fee, alt)
+ v.vote(value = fee, alt)
+```
+
+Named arguments can be given in any order.
+
+Note that reentrant calls are not permitted. In other words, when calling
+another contract it cannot call you back (directly or indirectly).
+
+To construct a value of a contract type you can give a contract address literal
+(for instance `ct_2gPXZnZdKU716QBUFKaT4VdBZituK93KLvHJB3n4EnbrHHw4Ay`), or
+convert an account address to a contract address using `Address.to_contract`.
+Note that if the contract does not exist, or it doesn't have the entrypoint, or
+the type of the entrypoint does not match the stated contract type, the call
+fails.
+
+To recover the underlying `address` of a contract instance there is a field
+`address : address`. For instance, to send tokens to the voting contract (given that it is payable)
+without calling it you can write
+
+```javascript
+ entrypoint pay(v : VotingType, amount : int) =
+ Chain.spend(v.address, amount)
+```
+
+### Mutable state
+
+Sophia does not have arbitrary mutable state, but only a limited form of
+state associated with each contract instance.
+
+- Each contract defines a type `state` encapsulating its mutable state.
+ The type `state` defaults to the `unit`.
+- The initial state of a contract is computed by the contract's `init`
+ function. The `init` function is *pure* and returns the initial state as its
+ return value.
+ If the type `state` is `unit`, the `init` function defaults to returning the value `()`.
+ At contract creation time, the `init` function is executed and
+ its result is stored as the contract state.
+- The value of the state is accessible from inside the contract
+ through an implicitly bound variable `state`.
+- State updates are performed by calling a function `put : state => unit`.
+- Aside from the `put` function (and similar functions for transactions
+ and events), the language is purely functional.
+- Functions modifying the state need to be annotated with the `stateful` keyword (see below).
+
+To make it convenient to update parts of a deeply nested state Sophia
+provides special syntax for map/record updates.
+
+#### Stateful functions
+
+Top-level functions and entrypoints must be annotated with the
+`stateful` keyword to be allowed to affect the state of the running contract.
+For instance,
+
+```javascript
+ stateful entrypoint set_state(s : state) =
+ put(s)
+```
+
+Without the `stateful` annotation the compiler does not allow the call to
+`put`. A `stateful` annotation is required to
+
+* Use a stateful primitive function. These are
+ - `put`
+ - `Chain.spend`
+ - `Oracle.register`
+ - `Oracle.query`
+ - `Oracle.respond`
+ - `Oracle.extend`
+ - `AENS.preclaim`
+ - `AENS.claim`
+ - `AENS.transfer`
+ - `AENS.revoke`
+* Call a `stateful` function in the current contract
+* Call another contract with a non-zero `value` argument.
+
+A `stateful` annotation *is not* required to
+
+* Read the contract state.
+* Issue an event using the `event` function.
+* Call another contract with `value = 0`, even if the called function is stateful.
+
+### Payable
+
+#### Payable contracts
+
+A concrete contract is by default *not* payable. Any attempt at spending to such
+a contract (either a `Chain.spend` or a normal spend transaction) will fail. If a
+contract shall be able to receive funds in this way it has to be declared `payable`:
+
+```javascript
+// A payable contract
+payable contract ExampleContract =
+ stateful entrypoint do_stuff() = ...
+```
+
+If in doubt, it is possible to check if an address is payable using
+`Address.is_payable(addr)`.
+
+#### Payable entrypoints
+
+A contract entrypoint is by default *not* payable. Any call to such a function
+(either a [Remote call](#calling-other-contracts) or a contract call transaction)
+that has a non-zero `value` will fail. Contract entrypoints that should be called
+with a non-zero value should be declared `payable`.
+
+```javascript
+payable stateful entrypoint buy(to : address) =
+ if(Call.value > 42)
+ transfer_item(to)
+ else
+ abort("Value too low")
+```
+
+Note: In the Aeternity VM (AEVM) contracts and entrypoints were by default
+payable until the Lima release.
+
+### Namespaces
+
+Code can be split into libraries using the `namespace` construct. Namespaces
+can appear at the top-level and can contain type and function definitions, but
+not entrypoints. Outside the namespace you can refer to the (non-private) names
+by qualifying them with the namespace (`Namespace.name`).
+For example,
+
+```
+namespace Library =
+ type number = int
+ function inc(x : number) : number = x + 1
+
+contract MyContract =
+ entrypoint plus2(x) : Library.number =
+ Library.inc(Library.inc(x))
+```
+
+Functions in namespaces have access to the same environment (including the
+`Chain`, `Call`, and `Contract`, builtin namespaces) as function in a contract,
+with the exception of `state`, `put` and `Chain.event` since these are
+dependent on the specific state and event types of the contract.
+
+### Splitting code over multiple files
+
+Code from another file can be included in a contract using an `include`
+statement. These must appear at the top-level (outside the main contract). The
+included file can contain one or more namespaces and abstract contracts. For
+example, if the file `library.aes` contains
+
+```
+namespace Library =
+ function inc(x) = x + 1
+```
+
+you can use it from another file using an `include`:
+
+```
+include "library.aes"
+contract MyContract =
+ entrypoint plus2(x) = Library.inc(Library.inc(x))
+```
+
+This behaves as if the contents of `library.aes` was textually inserted into
+the file, except that error messages will refer to the original source
+locations. The language will try to include each file at most one time automatically,
+so even cyclic includes should be working without any special tinkering.
+
+### Types
+Sophia has the following types:
+
+| Type | Description | Example | |
+| ---------- | ------------------------------- | -------: | |
+| int | A 2-complement integer | ```-1``` | |
+| address | Aeternity address, 32 bytes | ```Call.origin``` | |
+| bool | A Boolean | ```true``` | |
+| bits | A bit field | ```Bits.none``` | |
+| bytes(n) | A byte array with `n` bytes | ```#fedcba9876543210``` | |
+| string | An array of bytes | ```"Foo"``` | |
+| list | A homogeneous immutable singly linked list. | ```[1, 2, 3]``` | |
+| ('a, 'b) => 'c | A function. Parentheses can be skipped if there is only one argument | ```(x : int, y : int) => x + y``` | |
+| tuple | An ordered heterogeneous array | ```(42, "Foo", true)``` | |
+| record | An immutable key value store with fixed key names and typed values | ``` record balance = { owner: address, value: int } ``` | |
+| map | An immutable key value store with dynamic mapping of keys of one type to values of one type | ```type accounts = map(string, address)``` | |
+| option('a) | An optional value either None or Some('a) | ```Some(42)``` | |
+| state | A user defined type holding the contract state | ```record state = { owner: address, magic_key: bytes(4) }``` | |
+| event | An append only list of blockchain events (or log entries) | ```datatype event = EventX(indexed int, string)``` | |
+| hash | A 32-byte hash - equivalent to `bytes(32)` | | |
+| signature | A signature - equivalent to `bytes(64)` | | |
+| Chain.ttl | Time-to-live (fixed height or relative to current block) | ```FixedTTL(1050)``` ```RelativeTTL(50)``` | |
+| oracle('a, 'b) | And oracle answering questions of type 'a with answers of type 'b | ```Oracle.register(acct, qfee, ttl)``` | |
+| oracle_query('a, 'b) | A specific oracle query | ```Oracle.query(o, q, qfee, qttl, rttl)``` | |
+| contract | A user defined, typed, contract address | ```function call_remote(r : RemoteContract) = r.fun()``` | |
+
+### Literals
+| Type | Constant/Literal example(s) |
+| ---------- | ------------------------------- |
+| int | `-1`, `2425`, `4598275923475723498573485768` |
+| address | `ak_2gx9MEFxKvY9vMG5YnqnXWv1hCsX7rgnfvBLJS4aQurustR1rt` |
+| bool | `true`, `false` |
+| bits | `Bits.none`, `Bits.all` |
+| bytes(8) | `#fedcba9876543210` |
+| string | `"This is a string"` |
+| list | `[1, 2, 3]`, `[(true, 24), (false, 19), (false, -42)]` |
+| tuple | `(42, "Foo", true)` |
+| record | `{ owner = Call.origin, value = 100000000 }` |
+| map | `{["foo"] = 19, ["bar"] = 42}`, `{}` |
+| option(int) | `Some(42)`, `None` |
+| state | `state{ owner = Call.origin, magic_key = #a298105f }` |
+| event | `EventX(0, "Hello")` |
+| hash | `#000102030405060708090a0b0c0d0e0f000102030405060708090a0b0c0d0e0f` |
+| signature | `#000102030405060708090a0b0c0d0e0f000102030405060708090a0b0c0d0e0f000102030405060708090a0b0c0d0e0f000102030405060708090a0b0c0d0e0f` |
+| Chain.ttl | `FixedTTL(1050)`, `RelativeTTL(50)` |
+| oracle('a, 'b) | `ok_2YNyxd6TRJPNrTcEDCe9ra59SVUdp9FR9qWC5msKZWYD9bP9z5` |
+| oracle_query('a, 'b) | `oq_2oRvyowJuJnEkxy58Ckkw77XfWJrmRgmGaLzhdqb67SKEL1gPY` |
+| contract | `ct_Ez6MyeTMm17YnTnDdHTSrzMEBKmy7Uz2sXu347bTDPgVH2ifJ` |
+
+### Arithmetic
+
+Sophia integers (`int`) are represented by 256-bit (AEVM) or arbitrary-sized (FATE) signed words and supports the following
+arithmetic operations:
+- addition (`x + y`)
+- subtraction (`x - y`)
+- multiplication (`x * y`)
+- division (`x / y`), truncated towards zero
+- remainder (`x mod y`), satisfying `y * (x / y) + x mod y == x` for non-zero `y`
+- exponentiation (`x ^ y`)
+
+All operations are *safe* with respect to overflow and underflow. On AEVM they behave as the corresponding
+operations on arbitrary-size integers and fail with `arithmetic_error` if the
+result cannot be represented by a 256-bit signed word. For example, `2 ^ 255`
+fails rather than wrapping around to -2²⁵⁵.
+
+The division and modulo operations also throw an arithmetic error if the
+second argument is zero.
+
+### Bit fields
+
+Sophia integers do not support bit arithmetic. Instead there is a separate
+type `bits`. See the standard library [documentation](sophia_stdlib.md#Bits).
+
+On the AEVM a bit field is represented by a 256-bit word and reading or writing
+a bit outside the 0..255 range fails with an `arithmetic_error`. On FATE a bit
+field can be of arbitrary size (but it is still represented by the
+corresponding integer, so setting very high bits can be expensive).
+
+### Type aliases
+
+Type aliases can be introduced with the `type` keyword and can be
+parameterized. For instance
+
+```
+type number = int
+type string_map('a) = map(string, 'a)
+```
+
+A type alias and its definition can be used interchangeably. Sophia does not support
+higher-kinded types, meaning that following type alias is invalid: `type wrap('f, 'a) = 'f('a)`
+
+### Algebraic data types
+
+Sophia supports algebraic data types (variant types) and pattern matching. Data
+types are declared by giving a list of constructors with
+their respective arguments. For instance,
+
+```
+datatype one_or_both('a, 'b) = Left('a) | Right('b) | Both('a, 'b)
+```
+
+Elements of data types can be pattern matched against, using the `switch` construct:
+
+```
+function get_left(x : one_or_both('a, 'b)) : option('a) =
+ switch(x)
+ Left(x) => Some(x)
+ Right(_) => None
+ Both(x, _) => Some(x)
+```
+
+or directly in the left-hand side:
+```
+function
+ get_left : one_or_both('a, 'b) => option('a)
+ get_left(Left(x)) = Some(x)
+ get_left(Right(_)) = None
+ get_left(Both(x, _)) = Some(x)
+```
+
+*NOTE: Data types cannot currently be recursive.*
+
+### Lists
+
+A Sophia list is a dynamically sized, homogenous, immutable, singly
+linked list. A list is constructed with the syntax `[1, 2, 3]`. The
+elements of a list can be any of datatype but they must have the same
+type. The type of lists with elements of type `'e` is written
+`list('e)`. For example we can have the following lists:
+
+```
+[1, 33, 2, 666] : list(int)
+[(1, "aaa"), (10, "jjj"), (666, "the beast")] : list(int * string)
+[{[1] = "aaa", [10] = "jjj"}, {[5] = "eee", [666] = "the beast"}] : list(map(int, string))
+```
+
+New elements can be prepended to the front of a list with the `::`
+operator. So `42 :: [1, 2, 3]` returns the list `[42, 1, 2, 3]`. The
+concatenation operator `++` appends its second argument to its first
+and returns the resulting list. So concatenating two lists
+`[1, 22, 33] ++ [10, 18, 55]` returns the list `[1, 22, 33, 10, 18, 55]`.
+
+Sophia supports list comprehensions known from languages like Python, Haskell or Erlang.
+Example syntax:
+```
+[x + y | x <- [1,2,3,4,5], let k = x*x, if (k > 5), y <- [k, k+1, k+2]]
+// yields [12,13,14,20,21,22,30,31,32]
+```
+
+Please refer to the [standard library](sophia_stdlib.md#List) for the predefined functionalities.
+
+### Maps and records
+
+A Sophia record type is given by a fixed set of fields with associated,
+possibly different, types. For instance
+```
+ record account = { name : string,
+ balance : int,
+ history : list(transaction) }
+```
+
+Maps, on the other hand, can contain an arbitrary number of key-value bindings,
+but of a fixed type. The type of maps with keys of type `'k` and values of type
+`'v` is written `map('k, 'v)`. The key type can be any type that does not
+contain a map or a function type.
+
+Please refer to the [standard library](sophia_stdlib.md#Map) for the predefined functionalities.
+
+#### Constructing maps and records
+
+A value of record type is constructed by giving a value for each of the fields.
+For the example above,
+```
+ function new_account(name) =
+ {name = name, balance = 0, history = []}
+```
+Maps are constructed similarly, with keys enclosed in square brackets
+```
+ function example_map() : map(string, int) =
+ {["key1"] = 1, ["key2"] = 2}
+```
+The empty map is written `{}`.
+
+#### Accessing values
+
+Record fields access is written `r.f` and map lookup `m[k]`. For instance,
+```
+ function get_balance(a : address, accounts : map(address, account)) =
+ accounts[a].balance
+```
+Looking up a non-existing key in a map results in contract execution failing. A
+default value to return for non-existing keys can be provided using the syntax
+`m[k = default]`. See also `Map.member` and `Map.lookup` below.
+
+#### Updating a value
+
+Record field updates are written `r{f = v}`. This creates a new record value
+which is the same as `r`, but with the value of the field `f` replaced by `v`.
+Similarly, `m{[k] = v}` constructs a map with the same values as `m` except
+that `k` maps to `v`. It makes no difference if `m` has a mapping for `k` or
+not.
+
+It is possible to give a name to the old value of a field or mapping in an
+update: instead of `acc{ balance = acc.balance + 100 }` it is possible to write
+`acc{ balance @ b = b + 100 }`, binding `b` to `acc.balance`. When giving a
+name to a map value (`m{ [k] @ x = v }`), the corresponding key must be present
+in the map or execution fails, but a default value can be provided:
+`m{ [k = default] @ x = v }`. In this case `x` is bound to `default` if
+`k` is not in the map.
+
+Updates can be nested:
+```
+function clear_history(a : address, accounts : map(address, account)) : map(address, account) =
+ accounts{ [a].history = [] }
+```
+This is equivalent to `accounts{ [a] @ acc = acc{ history = [] } }` and thus
+requires `a` to be present in the accounts map. To have `clear_history` create
+an account if `a` is not in the map you can write (given a function `empty_account`):
+```
+ accounts{ [a = empty_account()].history = [] }
+```
+
+#### Map implementation
+
+Internally in the VM maps are implemented as hash maps and support fast lookup
+and update. Large maps can be stored in the contract state and the size of the
+map does not contribute to the gas costs of a contract call reading or updating
+it.
+
+### Strings
+
+There is a builtin type `string`, which can be seen as an array of bytes.
+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).
+
+### Byte arrays
+
+Byte arrays are fixed size arrays of 8-bit integers. They are described in hexadecimal system,
+for example the literal `#cafe` means a two-element array of bytes `ca` (202) and `fe` (254)
+and thus is a value of type `bytes(2)`.
+
+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
+hash objects, verify signatures etc. The `hash` is a type alias for `bytes(32)`.
+
+#### AEVM note
+The hash functions in `String` hash strings interpreted as byte arrays, and
+the `Crypto` hash functions accept an element of any (first-order) type. The
+result is the hash of the binary encoding of the argument as [described
+below](#encoding-sophia-values-as-binaries). Note that this means that for `s :
+string`, `String.sha3(s)` and `Crypto.sha3(s)` will give different results on AEVM.
+
+
+### 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`.
+
+
+#### Oracle interface
+You can attach an oracle to the current contract and you can interact with oracles
+through the Oracle interface.
+
+For a full description of how Oracle works see
+[Oracles](https://github.com/aeternity/protocol/blob/master/oracles/oracles.md#oracles).
+For a functionality documentation refer to the [standard library](sophia_stdlib.md#Oracle).
+
+
+##### Example
+
+Example for an oracle answering questions of type `string` with answers of type `int`:
+```
+contract Oracles =
+
+ stateful entrypoint registerOracle(acct : address,
+ sign : signature, // Signed oracle address + contract address
+ qfee : int,
+ ttl : Chain.ttl) : oracle(string, int) =
+ Oracle.register(acct, signature = sign, qfee, ttl)
+
+ entrypoint queryFee(o : oracle(string, int)) : int =
+ Oracle.query_fee(o)
+
+ payable stateful entrypoint createQuery(o : oracle_query(string, int),
+ q : string,
+ qfee : int,
+ qttl : Chain.ttl,
+ rttl : int) : oracle_query(string, int) =
+ require(qfee =< Call.value, "insufficient value for qfee")
+ Oracle.query(o, q, qfee, qttl, RelativeTTL(rttl))
+
+ stateful entrypoint extendOracle(o : oracle(string, int),
+ ttl : Chain.ttl) : unit =
+ Oracle.extend(o, ttl)
+
+ stateful entrypoint signExtendOracle(o : oracle(string, int),
+ sign : signature, // Signed 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
+ r : int) =
+ Oracle.respond(o, q, signature = sign, r)
+
+ entrypoint getQuestion(o : oracle(string, int),
+ q : oracle_query(string, int)) : string =
+ Oracle.get_question(o, q)
+
+ entrypoint hasAnswer(o : oracle(string, int),
+ q : oracle_query(string, int)) =
+ switch(Oracle.get_answer(o, q))
+ None => false
+ Some(_) => true
+
+ entrypoint getAnswer(o : oracle(string, int),
+ q : oracle_query(string, int)) : option(int) =
+ Oracle.get_answer(o, q)
+```
+
+##### Sanity checks
+
+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.
+
+### AENS interface
+
+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.
+
+
+#### Events
+
+Sophia contracts log structured messages to an event log in the resulting
+blockchain transaction. The event log is quite similar to [Events in
+Solidity](https://solidity.readthedocs.io/en/v0.4.24/contracts.html#events). To
+use events a contract must declare a datatype `event`, and events are then
+logged using the `Chain.event` function:
+
+```
+ datatype event =
+ Event1(int, int, string)
+ | Event2(string, address)
+
+ Chain.event(e : event) : unit
+```
+
+The event can have 0-3 *indexed* fields, and an optional *payload* field. A
+field is indexed if it fits in a 32-byte word, i.e.
+- `bool`
+- `int`
+- `bits`
+- `address`
+- `oracle(_, _)`
+- `oracle_query(_, _)`
+- contract types
+- `bytes(n)` for `n` ≤ 32, in particular `hash`
+
+The payload field must be either a string or a byte array of more than 32 bytes.
+The fields can appear in any order.
+
+*NOTE:* Indexing is not part of the core aeternity node.
+
+Events are further discussed in [Sophia explained -
+Events](./sophia_explained.md#events).
+
+Events are emitted by using the `Chain.event` function. The following function
+will emit one Event of each kind in the example.
+
+```
+ entrypoint emit_events() : () =
+ Chain.event(TheFirstEvent(42))
+ Chain.event(AnotherEvent(Contract.address, "This is not indexed"))
+```
+
+### Compiler pragmas
+
+To enforce that a contract is only compiled with specific versions of the
+Sophia compiler, you can give one or more `@compiler` pragmas at the
+top-level (typically at the beginning) of a file. For instance, to enforce that
+a contract is compiled with version 4.3 of the compiler you write
+
+```
+@compiler >= 4.3
+@compiler < 4.4
+```
+
+Valid operators in compiler pragmas are `<`, `=<`, `==`, `>=`, and `>`. Version
+numbers are given as a sequence of non-negative integers separated by dots.
+Trailing zeros are ignored, so `4.0.0 == 4`. If a constraint is violated an
+error is reported and compilation fails.
+
+### Exceptions
+
+Contracts can fail with an (uncatchable) exception using the built-in function
+
+```
+abort(reason : string) : 'a
+```
+
+Calling abort causes the top-level call transaction to return an error result
+containing the `reason` string. Only the gas used up to and including the abort
+call is charged. This is different from termination due to a crash which
+consumes all available gas.
+
+For convenience the following function is also built-in:
+
+```
+function require(b : bool, err : string) =
+ if(!b) abort(err)
+```
+
+## Syntax
+
+### Lexical syntax
+
+#### Comments
+
+Single line comments start with `//` and block comments are enclosed in `/*`
+and `*/` and can be nested.
+
+#### Keywords
+
+```
+contract elif else entrypoint false function if import include let mod namespace
+private payable stateful switch true type record datatype
+```
+
+#### Tokens
+
+- `Id = [a-z_][A-Za-z0-9_']*` identifiers start with a lower case letter.
+- `Con = [A-Z][A-Za-z0-9_']*` constructors start with an upper case letter.
+- `QId = (Con\.)+Id` qualified identifiers (e.g. `Map.member`)
+- `QCon = (Con\.)+Con` qualified constructor
+- `TVar = 'Id` type variable (e.g `'a`, `'b`)
+- `Int = [0-9]+(_[0-9]+)*|0x[0-9A-Fa-f]+(_[0-9A-Fa-f]+)*` integer literal with optional `_` separators
+- `Bytes = #[0-9A-Fa-f]+(_[0-9A-Fa-f]+)*` byte array literal with optional `_` separators
+- `String` string literal enclosed in `"` with escape character `\`
+- `Char` character literal enclosed in `'` with escape character `\`
+- `AccountAddress` base58-encoded 32 byte account pubkey with `ak_` prefix
+- `ContractAddress` base58-encoded 32 byte contract address with `ct_` prefix
+- `OracleAddress` base58-encoded 32 byte oracle address with `ok_` prefix
+- `OracleQueryId` base58-encoded 32 byte oracle query id with `oq_` prefix
+
+Valid string escape codes are
+
+| Escape | ASCII | |
+|---------------|-------------|---|
+| `\b` | 8 | |
+| `\t` | 9 | |
+| `\n` | 10 | |
+| `\v` | 11 | |
+| `\f` | 12 | |
+| `\r` | 13 | |
+| `\e` | 27 | |
+| `\xHexDigits` | *HexDigits* | |
+| | | |
+-------------------
+
+See the [identifier encoding scheme](/node/api/api_encoding.md) for the
+details on the base58 literals.
+
+### Layout blocks
+
+Sophia uses Python-style layout rules to group declarations and statements. A
+layout block with more than one element must start on a separate line and be
+indented more than the currently enclosing layout block. Blocks with a single
+element can be written on the same line as the previous token.
+
+Each element of the block must share the same indentation and no part of an
+element may be indented less than the indentation of the block. For instance
+
+```
+contract Layout =
+ function foo() = 0 // no layout
+ function bar() = // layout block starts on next line
+ let x = foo() // indented more than 2 spaces
+ x
+ + 1 // the '+' is indented more than the 'x'
+```
+
+### Notation
+
+In describing the syntax below, we use the following conventions:
+- Upper-case identifiers denote non-terminals (like `Expr`) or terminals with
+ some associated value (like `Id`).
+- Keywords and symbols are enclosed in single quotes: `'let'` or `'='`.
+- Choices are separated by vertical bars: `|`.
+- Optional elements are enclosed in `[` square brackets `]`.
+- `(` Parentheses `)` are used for grouping.
+- Zero or more repetitions are denoted by a postfix `*`, and one or more
+ repetitions by a `+`.
+- `Block(X)` denotes a layout block of `X`s.
+- `Sep(X, S)` is short for `[X (S X)*]`, i.e. a possibly empty sequence of `X`s
+ separated by `S`s.
+- `Sep1(X, S)` is short for `X (S X)*`, i.e. same as `Sep`, but must not be empty.
+
+
+### Declarations
+
+A Sophia file consists of a sequence of *declarations* in a layout block.
+
+```c
+File ::= Block(Decl)
+Decl ::= ['payable'] 'contract' Con '=' Block(Decl)
+ | 'namespace' Con '=' Block(Decl)
+ | '@compiler' PragmaOp Version
+ | 'include' String
+ | 'type' Id ['(' TVar* ')'] ['=' TypeAlias]
+ | 'record' Id ['(' TVar* ')'] '=' RecordType
+ | 'datatype' Id ['(' TVar* ')'] '=' DataType
+ | EModifier* ('entrypoint' | 'function') Block(FunDecl)
+
+FunDecl ::= Id ':' Type // Type signature
+ | Id Args [':' Type] '=' Block(Stmt) // Definition
+
+PragmaOp ::= '<' | '=<' | '==' | '>=' | '>'
+Version ::= Sep1(Int, '.')
+
+EModifier ::= 'payable' | 'stateful'
+FModifier ::= 'stateful' | 'private'
+
+Args ::= '(' Sep(Pattern, ',') ')'
+```
+
+Contract declarations must appear at the top-level.
+
+For example,
+```
+contract Test =
+ type t = int
+ entrypoint add (x : t, y : t) = x + y
+```
+
+There are three forms of type declarations: type aliases (declared with the
+`type` keyword), record type definitions (`record`) and data type definitions
+(`datatype`):
+
+```c
+TypeAlias ::= Type
+RecordType ::= '{' Sep(FieldType, ',') '}'
+DataType ::= Sep1(ConDecl, '|')
+
+FieldType ::= Id ':' Type
+ConDecl ::= Con ['(' Sep1(Type, ',') ')']
+```
+
+For example,
+```
+record point('a) = {x : 'a, y : 'a}
+datatype shape('a) = Circle(point('a), 'a) | Rect(point('a), point('a))
+type int_shape = shape(int)
+```
+
+### Types
+
+```c
+Type ::= Domain '=>' Type // Function type
+ | Type '(' Sep(Type, ',') ')' // Type application
+ | '(' Type ')' // Parens
+ | 'unit' | Sep(Type, '*') // Tuples
+ | Id | QId | TVar
+
+Domain ::= Type // Single argument
+ | '(' Sep(Type, ',') ')' // Multiple arguments
+```
+
+The function type arrow associates to the right.
+
+Example,
+```
+'a => list('a) => (int * list('a))
+```
+
+### Statements
+
+Function bodies are blocks of *statements*, where a statement is one of the following
+
+```c
+Stmt ::= 'switch' '(' Expr ')' Block(Case)
+ | 'if' '(' Expr ')' Block(Stmt)
+ | 'elif' '(' Expr ')' Block(Stmt)
+ | 'else' Block(Stmt)
+ | 'let' LetDef
+ | Expr
+
+LetDef ::= Id Args [':' Type] '=' Block(Stmt) // Function definition
+ | Pattern '=' Block(Stmt) // Value definition
+
+Case ::= Pattern '=>' Block(Stmt)
+Pattern ::= Expr
+```
+
+`if` statements can be followed by zero or more `elif` statements and an optional final `else` statement. For example,
+
+```
+let x : int = 4
+switch(f(x))
+ None => 0
+ Some(y) =>
+ if(y > 10)
+ "too big"
+ elif(y < 3)
+ "too small"
+ else
+ "just right"
+```
+
+### Expressions
+
+```c
+Expr ::= '(' LamArgs ')' '=>' Block(Stmt) // Anonymous function (x) => x + 1
+ | 'if' '(' Expr ')' Expr 'else' Expr // If expression if(x < y) y else x
+ | Expr ':' Type // Type annotation 5 : int
+ | Expr BinOp Expr // Binary operator x + y
+ | UnOp Expr // Unary operator ! b
+ | Expr '(' Sep(Expr, ',') ')' // Application f(x, y)
+ | Expr '.' Id // Projection state.x
+ | Expr '[' Expr ']' // Map lookup map[key]
+ | Expr '{' Sep(FieldUpdate, ',') '}' // Record or map update r{ fld[key].x = y }
+ | '[' Sep(Expr, ',') ']' // List [1, 2, 3]
+ | '[' Expr '|' Sep(Generator, ',') ']'
+ // List comprehension [k | x <- [1], if (f(x)), let k = x+1]
+ | '{' 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
+ | Int | Bytes | String | Char // Literals 123, 0xff, #00abc123, "foo", '%'
+ | AccountAddress | ContractAddress // Chain identifiers
+ | OracleAddress | OracleQueryId // Chain identifiers
+
+Generator ::= Pattern '<-' Expr // Generator
+ | 'if' '(' Expr ')' // Guard
+ | LetDef // Definition
+
+LamArgs ::= '(' Sep(LamArg, ',') ')'
+LamArg ::= Id [':' Type]
+
+FieldUpdate ::= Path '=' Expr
+Path ::= Id // Record field
+ | '[' Expr ']' // Map key
+ | Path '.' Id // Nested record field
+ | Path '[' Expr ']' // Nested map key
+
+BinOp ::= '||' | '&&' | '<' | '>' | '=<' | '>=' | '==' | '!='
+ | '::' | '++' | '+' | '-' | '*' | '/' | 'mod' | '^'
+UnOp ::= '-' | '!'
+```
+
+### Operators types
+
+| Operators | Type
+| --- | ---
+| `-` `+` `*` `/` `mod` `^` | arithmetic operators
+| `!` `&&` `\|\|` | logical operators
+| `==` `!=` `<` `>` `=<` `>=` | comparison operators
+| `::` `++` | list operators
+
+### Operator precendences
+
+In order of highest to lowest precedence.
+
+| Operators | Associativity
+| --- | ---
+| `!` | right
+| `^` | left
+| `*` `/` `mod` | left
+| `-` (unary) | right
+| `+` `-` | left
+| `::` `++` | right
+| `<` `>` `=<` `>=` `==` `!=` | none
+| `&&` | right
+| `\|\|` | right
+
+## Examples
+
+```
+/*
+ * A simple crowd-funding example
+ */
+contract FundMe =
+
+ record spend_args = { recipient : address,
+ amount : int }
+
+ record state = { contributions : map(address, int),
+ total : int,
+ beneficiary : address,
+ deadline : int,
+ goal : int }
+
+ function spend(args : spend_args) =
+ raw_spend(args.recipient, args.amount)
+
+ entrypoint init(beneficiary, deadline, goal) : state =
+ { contributions = {},
+ beneficiary = beneficiary,
+ deadline = deadline,
+ total = 0,
+ goal = goal }
+
+ function is_contributor(addr) =
+ Map.member(addr, state.contributions)
+
+ stateful entrypoint contribute() =
+ if(Chain.block_height >= state.deadline)
+ spend({ recipient = Call.caller, amount = Call.value }) // Refund money
+ false
+ else
+ let amount =
+ switch(Map.lookup(Call.caller, state.contributions))
+ None => Call.value
+ Some(n) => n + Call.value
+ put(state{ contributions[Call.caller] = amount,
+ total @ tot = tot + Call.value })
+ true
+
+ stateful entrypoint withdraw() =
+ if(Chain.block_height < state.deadline)
+ abort("Cannot withdraw before deadline")
+ if(Call.caller == state.beneficiary)
+ withdraw_beneficiary()
+ elif(is_contributor(Call.caller))
+ withdraw_contributor()
+ else
+ abort("Not a contributor or beneficiary")
+
+ stateful function withdraw_beneficiary() =
+ 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)
+ abort("Project was funded")
+ let to = Call.caller
+ spend({recipient = to,
+ amount = state.contributions[to]})
+ put(state{ contributions @ c = Map.delete(to, c) })
+```
+
+## The lifetime of a contract
+
+### Killing a contract
+
+There is no selfdestruct instruction in the aevm as in the Ethereum
+Virtual Machine instead there is a disable transaction which the
+creator of a contract can issue. When a contract is disabled no new
+contract can call the old contract.
+
+When a contract is posted to the chain all references to other
+contracts are checked and a reference counter in each contract is
+increased. You can only post a contract to the chain if all the
+contracts referred to are enabled.
+
+When a contract is disabled all other contracts it refer to get their
+reference count decreased.
+
+If a contract is disabled and its reference count is zero a miner can
+choose to garbage collect the contract.
+
+The reference count of a contract is handled as the account balance
+and kept in the state tree of the miner and the merkle hash is
+included in the state hash in each block just as with balances.
+
+The transaction for creating a contract has an extra fee called
+deposit which has to be an even number. The disable transaction is
+free but the miner and the creator get half of the deposit fee each at
+contract disable thus encouraging creators to disable their contracts
+and miners to pick disable transactions.
diff --git a/docs/sophia_stdlib.md b/docs/sophia_stdlib.md
new file mode 100644
index 0000000..d2d3107
--- /dev/null
+++ b/docs/sophia_stdlib.md
@@ -0,0 +1,1613 @@
+
+
+# Standard library
+
+Sophia language offers standard library that consists of following namespaces:
+
+
+- [Bits](##Bits)
+- [String](##String)
+- [Bytes](##Bytes)
+- [Int](##Int)
+- [Map](##Map)
+- [Address](##Address)
+- [Crypto](##Crypto)
+- [Auth](##Auth)
+- [Oracle](##Oracle)
+- [AENS](##AENS)
+- [Contract](##Contract)
+- [Call](##Call)
+- [Chain](##Chain)
+- [List](##List)
+- [Option](##Option)
+- [Func](##Func)
+- [Pair](##Pair)
+- [Triple](##Triple)
+- [BLS12_381](##BLS12_381)
+
+# Builtin namespaces
+
+They are available without any explicit includes.
+
+## Bits
+
+### none
+```
+Bits.none : bits
+```
+
+A bit field with all bits cleared
+
+
+### all
+```
+Bits.all : bits
+```
+
+A bit field with all bits set
+
+
+### set
+```
+Bits.set(b : bits, i : int) : bits
+```
+
+Set bit i
+
+
+### clear
+```
+Bits.clear(b : bits, i : int) : bits
+```
+
+Clear bit i
+
+
+### test
+```
+Bits.test(b : bits, i : int) : bool
+```
+
+Check if bit i is set
+
+
+### sum
+```
+Bits.sum(b : bits) : int
+```
+
+Count the number of set bits
+
+
+### union
+```
+Bits.union(a : bits, b : bits) : bits
+```
+
+Bitwise disjunction
+
+
+### intersection
+```
+Bits.intersection(a : bits, b : bits) : bits
+```
+
+Bitwise conjunction
+
+
+### difference
+```
+Bits.difference(a : bits, b : bits) : bits
+```
+
+Each bit is true if and only if it was 1 in `a` and 0 in `b`
+
+
+## String
+
+### length
+```
+String.length(s : string) : int
+```
+
+Returns the length of a string
+
+
+### concat
+```
+String.concat(s1 : string, s2 : string) : string
+```
+
+Concatenates two strings
+
+
+### sha3
+```
+String.sha3(s : string) : hash
+```
+
+Calculates SHA3 sum of a string.
+
+
+### sha256
+```
+String.sha256(s : string) : hash
+```
+
+Calculates SHA256 sum of a string
+
+
+### blake2b
+```
+String.blake2b(s : string) : hash
+```
+
+Calculates blake2b of a string
+
+
+## Bytes
+
+### to_int
+```
+Bytes.to_int(b : bytes(n)) : int
+```
+
+Interprets the byte array as a big endian integer
+
+
+### to_str
+```
+Bytes.to_str(b : bytes(n)) : string
+```
+
+Returns the hexadecimal representation of the byte array
+
+
+### concat
+```
+Bytes.concat : (a : bytes(m), b : bytes(n)) => bytes(m + n)
+```
+
+Concatenates two byte arrays
+
+
+### split
+```
+Bytes.split(a : bytes(m + n)) : bytes(m) * bytes(n)
+```
+
+Splits a byte array at given index
+
+
+## Int
+
+### to_str
+```
+Int.to_str : int => string
+```
+
+Casts integer to string using decimal representation
+
+
+## Map
+
+### lookup
+`Map.lookup(k : 'k, m : map('k, 'v)) : option('v)`
+
+Returns the value under a key in given map as `Some` or `None`
+if the key is not present
+
+
+### lookup_default
+`Map.lookup_default(k : 'k, m : map('k, 'v), v : 'v) : 'v`
+
+Returns the value under a key in given map or the
+default value `v` if the key is not present
+
+
+### member
+`Map.member(k : 'k, m : map('k, 'v)) : bool`
+
+Checks if the key is present in the map
+
+
+### delete
+`Map.delete(k : 'k, m : map('k, 'v)) : map('k, 'v)`
+
+Removes the key from the map
+
+
+### size
+`Map.size(m : map('k, 'v)) : int`
+
+Returns the number of elements in the map
+
+
+### to_list
+`Map.to_list(m : map('k, 'v)) : list('k * 'v)`
+
+Returns a list containing pairs of keys and their respective elements.
+
+
+### from_list
+`Map.from_list(m : list('k * 'v)) : map('k, 'v)`
+
+Turns a list of pairs of form `(key, value)` into a map
+
+
+
+## Address
+
+### to_str
+```
+Address.to_str(a : address) : string
+```
+
+Base58 encoded string
+
+
+### is_contract
+```
+Address.is_contract(a : address) : bool
+```
+
+Is the address a contract
+
+
+### is_oracle
+```
+Address.is_oracle(a : address) : bool
+```
+
+Is the address a registered oracle
+
+
+### is_payable
+```
+Address.is_payable(a : address) : bool
+```
+
+Can the address be spent to
+
+
+### to_contract
+```
+Address.to_contract(a : address) : C
+```
+
+Cast address to contract type C (where `C` is a contract)
+
+
+## Crypto
+
+### sha3
+```
+Crypto.sha3(x : 'a) : hash
+```
+
+Hash any object to SHA3
+
+
+### sha256
+```
+Crypto.sha256(x : 'a) : hash
+```
+
+Hash any object to SHA256
+
+
+### blake2b
+```
+Crypto.blake2b(x : 'a) : hash
+```
+
+Hash any object to blake2b
+
+
+### verify_sig
+```
+Crypto.verify_sig(msg : hash, pubkey : address, sig : signature) : bool
+```
+
+Checks if the signature of `msg` was made using private key corresponding to
+the `pubkey`
+
+### ecverify_secp256k1
+```
+Crypto.ecverify_secp256k1(msg : hash, addr : bytes(20), sig : bytes(65)) : bool
+```
+
+Verifies a signature for a msg against an Ethereum style address
+
+
+### ecrecover_secp256k1
+```
+Crypto.ecrecover_secp256k1(msg : hash, sig : bytes(65)) : option(bytes(20))
+```
+
+Recovers the Ethereum style address from a msg hash and respective signature
+
+
+### verify_sig_secp256k1
+```
+Crypto.verify_sig_secp256k1(msg : hash, pubkey : bytes(64), sig : bytes(64)) : bool
+```
+
+
+
+## Auth
+
+### tx_hash
+```
+Auth.tx_hash : option(hash)
+```
+
+Gets the transaction hash during authentication.
+
+## Oracle
+
+### register
+```
+Oracle.register(, acct : address, qfee : int, ttl : Chain.ttl) : oracle('a, 'b)
+```
+
+Registers new oracle answering questions of type `'a` with answers of type `'b`.
+
+* The `acct` is the address of the oracle to register (can be the same as the contract).
+* `signature` is a signature proving that the contract is allowed to register the account -
+ the account address + the contract address (concatenated as byte arrays) is
+ signed with the
+ private key of the account, proving you have the private key of the oracle to be. If the
+ address is the same as the contract `sign` is ignored and can be left out entirely.
+* The `qfee` is the minimum query fee to be paid by a user when asking a question of the oracle.
+* The `ttl` is the Time To Live for the oracle, either relative to the current
+ height (`RelativeTTL(delta)`) or a fixed height (`FixedTTL(height)`).
+* The type `'a` is the type of the question to ask.
+* The type `'b` is the type of the oracle answers.
+
+Examples:
+```
+ Oracle.register(addr0, 25, RelativeTTL(400))
+ Oracle.register(addr1, 25, RelativeTTL(500), signature = sign1)
+```
+
+
+### get_question
+```
+Oracle.get_question(o : oracle('a, 'b), q : oracle_query('a, 'b)) : 'a
+```
+
+Checks what was the question of query `q` on oracle `o`
+
+
+### respond
+```
+Oracle.respond(, o : oracle('a, 'b), q : oracle_query('a, 'b), 'b) : unit
+```
+
+Responds to the question `q` on `o`.
+Unless the contract address is the same as the oracle address the `signature`
+(which is an optional, named argument)
+needs to be provided. Proving that we have the private key of the oracle by
+signing the oracle query id + contract address
+
+
+### extend
+```
+Oracle.extend(, o : oracle('a, 'b), ttl : Chain.ttl) : unit
+```
+
+Extends TTL of an oracle.
+* `singature` is a named argument and thus optional. Must be the same as for `Oracle.register`
+* `o` is the oracle being extended
+* `ttl` must be `RelativeTTL`. The time to live of `o` will be extended by this value.
+
+### query_fee
+```
+Oracle.query_fee(o : oracle('a, 'b)) : int
+```
+
+Returns the query fee of the oracle
+
+
+### query
+```
+Oracle.query(o : oracle('a, 'b), q : 'a, qfee : int, qttl : Chain.ttl, rttl : Chain.ttl) : oracle_query('a, 'b)
+```
+
+Asks the oracle a question.
+* The `qfee` is the query fee debited to the contract account (`Contract.address`).
+* The `qttl` controls the last height at which the oracle can submit a response
+ and can be either fixed or relative.
+* The `rttl` must be relative and controls how long an answer is kept on the chain.
+The call fails if the oracle could expire before an answer.
+
+
+### get_answer
+```
+Oracle.get_answer(o : oracle('a, 'b), q : oracle_query('a, 'b)) : option('b)
+```
+
+Checks what is the optional query answer
+
+
+### check
+```
+Oracle.check(o : oracle('a, 'b)) : bool
+```
+
+Returns `true` iff the oracle `o` exists and has correct type
+
+
+### check_query
+```
+Oracle.check_query(o : oracle('a, 'b), q : oracle_query('a, 'b)) : bool
+```
+
+It returns `true` iff the oracle query exist and has the expected type.
+
+
+## AENS
+
+The following functionalities are available for interacting with the Aeternity
+Naming System (AENS).
+If `owner` is equal to `Contract.address` the signature `signature` is
+ignored, and can be left out since it is a named argument. Otherwise we need
+a signature to prove that we are allowed to do AENS operations on behalf of
+`owner`
+
+### resolve
+```
+AENS.resolve(name : string, key : string) : option('a)
+```
+
+Name resolution. Here `name` should be a registered name and `key` one of the attributes
+associated with this name (for instance `"account_pubkey"`). The return type
+(`'a`) must be resolved at compile time to an atomic type and the value is
+type checked against this type at run time.
+
+
+### preclaim
+```
+AENS.preclaim(owner : address, commitment_hash : hash, ) : unit
+```
+
+The signature should be over `owner address` + `Contract.address`
+(concatenated as byte arrays).
+
+
+### claim
+```
+AENS.claim(owner : address, name : string, salt : int, name_fee : int, ) : unit
+```
+
+The signature should be over `owner address` + `name_hash` + `Contract.address`
+using the private key of the `owner` account for signing.
+
+
+### transfer
+```
+AENS.transfer(owner : address, new_owner : address, name_hash : hash, ) : unit
+```
+
+Transfers name to the new owner.
+
+The signature should be over `owner address` + `name_hash` + `Contract.address`
+using the private key of the `owner` account for signing.
+
+
+### revoke
+```
+AENS.revoke(owner : address, name_hash : hash, ) : unit
+```
+
+Revokes the name to extend the ownership time.
+
+The signature should be over `owner address` + `name_hash` + `Contract.address`
+using the private key of the `owner` account for signing.
+
+
+## Contract
+
+Values related to the current contract
+
+### creator
+```
+Contract.creator : address
+```
+
+Address of the entity that signed the contract creation transaction
+
+
+### address
+```
+Contract.address : address
+```
+
+Address of the contract account
+
+
+### balance
+```
+Contract.balance : int
+```
+
+Amount of coins in the contract account
+
+
+## Call
+
+Values related to the call to the current contract
+
+### origin
+```
+Call.origin : address
+```
+
+The address of the account that signed the call transaction that led to this call.
+
+
+### caller
+```
+Call.caller : address
+```
+
+The address of the entity (possibly another contract) calling the contract.
+
+### value
+```
+Call.value : int
+```
+
+The amount of coins transferred to the contract in the call.
+
+
+### gas
+```
+Call.gas_price : int
+```
+
+The gas price of the current call.
+
+
+### gas
+```
+Call.gas_left() : int
+```
+
+The amount of gas left for the current call.
+
+
+## Chain
+
+Values and functions related to the chain itself and other entities that live on it.
+
+### balance
+```
+Chain.balance(a : address) : int
+```
+
+The balance of account `a`.
+
+
+### block_hash
+```
+Chain.block_hash(h : int) : option(bytes(32))
+```
+
+The hash of the block at height `h`.
+
+
+### block_height
+```
+Chain.block_height : int"
+```
+
+The height of the current block (i.e. the block in which the current call will be included).
+
+
+### coinbase
+```
+Chain.coinbase : address
+```
+
+The address of the account that mined the current block.
+
+
+### timestamp
+```
+Chain.timestamp : int
+```
+
+The timestamp of the current block.
+
+
+### difficulty
+```
+Chain.difficulty : int
+```
+
+The difficulty of the current block.
+
+
+### gas
+```
+Chain.gas_limit : int
+```
+
+The gas limit of the current block.
+
+
+# Includable namespaces
+
+These need to be explicitly included (with `.aes` suffix)
+
+## List
+
+This module contains common operations on lists like constructing, querying, traversing etc.
+
+### is_empty
+```
+List.is_empty(l : list('a)) : bool
+```
+
+Returns `true` iff the list is equal to `[]`.
+
+
+### first
+```
+List.first(l : list('a)) : option('a)
+```
+
+Returns `Some` of the first element of a list or `None` if the list is empty.
+
+
+### tail
+```
+List.tail(l : list('a)) : option(list('a))
+```
+
+Returns `Some` of a list without its first element or `None` if the list is empty.
+
+
+### last
+```
+List.last(l : list('a)) : option('a)
+```
+
+Returns `Some` of the last element of a list or `None` if the list is empty.
+
+
+### find
+```
+List.find(p : 'a => bool, l : list('a)) : option('a)
+```
+
+Finds first element of `l` fulfilling predicate `p` as `Some` or `None` if no such element exists.
+
+
+### find_indices
+```
+List.find_indices(p : 'a => bool, l : list('a)) : list(int)
+```
+
+Returns list of all indices of elements from `l` that fulfill the predicate `p`.
+
+
+### nth
+```
+List.nth(n : int, l : list('a)) : option('a)
+```
+
+Gets `n`th element of `l` as `Some` or `None` if `l` is shorter than `n + 1` or `n` is negative.
+
+
+### get
+```
+List.get(n : int, l : list('a)) : 'a
+```
+
+Gets `n`th element of `l` forcefully, throwing and error if `l` is shorter than `n + 1` or `n` is negative.
+
+
+### length
+```
+List.length(l : list('a)) : int
+```
+
+Returns length of a list.
+
+
+### from_to
+```
+List.from_to(a : int, b : int) : list(int)
+```
+
+Creates an ascending sequence of all integer numbers between `a` and `b` (including `a` and `b`).
+
+
+### from_to_step
+```
+List.from_to_step(a : int, b : int, step : int) : list(int)
+```
+
+Creates an ascending sequence of integer numbers betweeen `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.
+
+
+### replace_at
+```
+List.replace_at(n : int, e : 'a, l : list('a)) : list('a)
+```
+
+Replaces `n`th element of `l` with `e`. Throws an error if `n` is negative or would cause an overflow.
+
+
+### insert_at
+```
+List.insert_at(n : int, e : 'a, l : list('a)) : list('a)
+```
+
+Inserts `e` into `l` to be on position `n` by shifting following elements further. For instance,
+```
+insert_at(2, 9, [1,2,3,4])
+```
+will yield `[1,2,9,3,4]`.
+
+
+### insert_by
+```
+List.insert_by(cmp : (('a, 'a) => bool), x : 'a, l : list('a)) : list('a)
+```
+
+Assuming that cmp represents `<` comparison, inserts `x` before the first element in the list `l` which is greater than it. For instance,
+```
+insert_by((a, b) => a < b, 4, [1,2,3,5,6,7])
+```
+will yield `[1,2,3,4,5,6,7]`
+
+
+### foldr
+```
+List.foldr(cons : ('a, 'b) => 'b, nil : 'b, l : list('a)) : 'b
+```
+
+Right fold of a list. Assuming `l = [x, y, z]` will return `f(x, f(y, f(z, nil)))`.
+Not tail recursive.
+
+
+### foldl
+```
+List.foldl(rcons : ('b, 'a) => 'b, acc : 'b, l : list('a)) : 'b
+```
+
+Left fold of a list. Assuming `l = [x, y, z]` will return `f(f(f(acc, x), y), z)`.
+Tail recursive.
+
+### foreach
+```
+List.foreach(l : list('a), f : 'a => unit) : unit
+```
+
+Evaluates `f` on each element of a list.
+
+
+### reverse
+```
+List.reverse(l : list('a)) : list('a)
+```
+
+Returns a copy of `l` with reversed order of elements.
+
+
+### map
+```
+List.map(f : 'a => 'b, l : list('a)) : list('b)
+```
+
+Maps function `f` over a list. For instance
+```
+map((x) => x == 0, [1, 2, 0, 3, 0])
+```
+will yield `[false, false, true, false, true]`
+
+
+### flat_map
+```
+List.flat_map(f : 'a => list('b), l : list('a)) : list('b)
+```
+
+Maps `f` over a list and then flattens it. For instance
+```
+flat_map((x) => [x, x * 10], [1, 2, 3])
+```
+will yield `[1, 10, 2, 20, 3, 30]`
+
+
+### filter
+```
+List.filter(p : 'a => bool, l : list('a)) : list('a)
+```
+
+Filters out elements of `l` that fulfill predicate `p`. For instance
+```
+filter((x) => x > 0, [-1, 1, -2, 0, 1, 2, -3])
+```
+will yield `[1, 1, 2]`
+
+
+### take
+```
+List.take(n : int, l : list('a)) : list('a)
+```
+
+Takes `n` first elements of `l`. Fails if `n` is negative. If `n` is greater than length of a list it will return whole list.
+
+
+### drop
+```
+List.drop(n : int, l : list('a)) : list('a)
+```
+
+Removes `n` first elements of `l`. Fails if `n` is negative. If `n` is greater than length of a list it will return `[]`.
+
+
+### take_while
+```
+List.take_while(p : 'a => bool, l : list('a)) : list('a)
+```
+
+Returns longest prefix of `l` in which all elements fulfill `p`.
+
+
+### drop_while
+```
+List.drop_while(p : 'a => bool, l : list('a)) : list('a)
+```
+
+Removes longest prefix from `l` in which all elements fulfill `p`.
+
+
+### partition
+```
+List.partition(p : 'a => bool, l : list('a)) : (list('a) * list('a))
+```
+
+Separates elements of `l` that fulfill `p` and these that do not. Elements fulfilling predicate will be in the right list. For instance
+```
+partition((x) => x > 0, [-1, 1, -2, 0, 1, 2, -3])
+```
+will yield `([1, 1, 2], [-1, -2, 0, -3])`
+
+
+### flatten
+```
+List.flatten(ll : list(list('a))) : list('a)
+```
+
+Flattens a list of lists into a one list.
+
+
+### all
+```
+List.all(p : 'a => bool, l : list('a)) : bool
+```
+
+Checks if all elements of a list fulfill predicate `p`.
+
+
+### any
+```
+List.any(p : 'a => bool, l : list('a)) : bool
+```
+
+Checks if any element of a list fulfills predicate `p`.
+
+
+### sum
+```
+List.sum(l : list(int)) : int
+```
+
+Sums elements of a list. Returns 0 if the list is empty.
+
+
+### product
+```
+List.product(l : list(int)) : int
+```
+
+Multiplies elements of a list. Returns 1 if the list is empty.
+
+
+### zip_with
+```
+List.zip_with(f : ('a, 'b) => 'c, l1 : list('a), l2 : list('b)) : list('c)
+```
+
+"zips" two lists with a function. n-th element of resulting list will be equal to `f(x1, x2)` where `x1` and `x2` are n-th elements of `l1` and `l2` respectively. Will cut off the tail of the longer list. For instance
+```
+zip_with((a, b) => a + b, [1,2], [1,2,3])
+```
+will yield `[2,4]`
+
+
+### zip
+```
+List.zip(l1 : list('a), l2 : list('b)) : list('a * 'b)
+```
+
+Special case of [zip_with](#zip_with) where the zipping function is `(a, b) => (a, b)`.
+
+### unzip
+```
+List.unzip(l : list('a * 'b)) : list('a) * list('b)
+```
+
+Opposite to the `zip` operation. Takes a list of pairs and returns pair of lists with respective elements on same indices.
+
+
+### sort
+```
+List.sort(lesser_cmp : ('a, 'a) => bool, l : list('a)) : list('a)
+```
+
+Sorts a list using given comparator. `lesser_cmp(x, y)` should return `true` iff `x < y`. If `lesser_cmp` is not transitive or there exists an element `x` such that `lesser_cmp(x, x)` or there exists a pair of elements `x` and `y` such that `lesser_cmp(x, y) && lesser_cmp(y, x)` then the result is undefined. Currently O(n^2).
+
+
+### intersperse
+```
+List.intersperse(delim : 'a, l : list('a)) : list('a)
+```
+
+Intersperses elements of `l` with `delim`. Does nothing on empty lists and singletons. For instance
+```
+intersperse(0, [1, 2, 3, 4])
+```
+will yield `[1, 0, 2, 0, 3, 0, 4]`
+
+
+### enumerate
+```
+List.enumerate(l : list('a)) : list(int * 'a)
+```
+
+Equivalent to [zip](#zip) with `[0..length(l)]`, but slightly faster.
+
+
+## Option
+
+Common operations on `option` types and lists of `option`s.
+
+### is_none
+```
+Option.is_none(o : option('a)) : bool
+```
+
+Returns true iff `o == None`
+
+
+### is_some
+```
+Option.is_some(o : option('a)) : bool
+```
+
+Returns true iff `o` is not `None`.
+
+
+### match
+```
+Option.match(n : 'b, s : 'a => 'b, o : option('a)) : 'b
+```
+
+Behaves like pattern matching on `option` using two case functions.
+
+
+### default
+```
+Option.default(def : 'a, o : option('a)) : 'a
+```
+
+Escapes `option` wrapping by providing default value for `None`.
+
+
+### force
+```
+Option.force(o : option('a)) : 'a
+```
+
+Forcefully escapes `option` wrapping assuming it is `Some`. Throws error on `None`.
+
+
+### on_elem
+```
+Option.on_elem(o : option('a), f : 'a => unit) : unit
+```
+
+Evaluates `f` on element under `Some`. Does nothing on `None`.
+
+
+### map
+```
+Option.map(f : 'a => 'b, o : option('a)) : option('b)
+```
+
+Maps element under `Some`. Leaves `None` unchanged.
+
+
+### map2
+```
+Option.map2(f : ('a, 'b) => 'c, o1 : option('a), o2 : option('b)) : option('c)
+```
+
+Applies arity 2 function over two `option`s' elements. Returns `Some` iff both of `o1` and `o2` were `Some`, or `None` otherwise. For instance
+```
+map2((a, b) => a + b, Some(1), Some(2))
+```
+will yield `Some(3)` and
+```
+map2((a, b) => a + b, Some(1), None)
+```
+will yield `None`.
+
+
+### map3
+```
+Option.map3(f : ('a, 'b, 'c) => 'd, o1 : option('a), o2 : option('b), o3 : option('c)) : option('d)
+```
+
+Same as [map2](#map2) but with arity 3 function.
+
+
+### app_over
+```
+Option.app_over(f : option ('a => 'b), o : option('a)) : option('b)
+```
+
+Applies function under `option` over argument under `option`. If either of them is `None` the result will be `None` as well. For instance
+```
+app_over(Some((x) => x + 1), Some(1))
+```
+will yield `Some(2)` and
+```
+app_over(Some((x) => x + 1), None)
+```
+will yield `None`.
+
+
+### flat_map
+```
+Option.flat_map(f : 'a => option('b), o : option('a)) : option('b)
+```
+
+Performs monadic bind on an `option`. Extracts element from `o` (if present) and forms new `option` from it. For instance
+```
+flat_map((x) => Some(x + 1), Some(1))
+```
+will yield `Some(2)` and
+```
+flat_map((x) => Some(x + 1), None)
+```
+will yield `None`.
+
+
+### to_list
+```
+Option.to_list(o : option('a)) : list('a)
+```
+
+Turns `o` into an empty (if `None`) or singleton (if `Some`) list.
+
+
+### filter_options
+```
+Option.filter_options(l : list(option('a))) : list('a)
+```
+
+Removes `None`s from list and unpacks all remaining `Some`s. For instance
+```
+filter_options([Some(1), None, Some(2)])
+```
+will yield `[1, 2]`.
+
+
+### seq_options
+```
+Option.seq_options(l : list (option('a))) : option (list('a))
+```
+
+Tries to unpack all elements of a list from `Some`s. Returns `None` if at least element of `l` is `None`. For instance
+```
+seq_options([Some(1), Some(2)])
+```
+will yield `Some([1, 2])`, but
+```
+seq_options([Some(1), Some(2), None])
+```
+will yield `None`.
+
+
+### choose
+```
+Option.choose(o1 : option('a), o2 : option('a)) : option('a)
+```
+
+Out of two `option`s choose the one that is `Some`, or `None` if both are `None`s.
+
+
+### choose_first
+```
+Option.choose_first(l : list(option('a))) : option('a)
+```
+
+Same as [choose](#choose), but chooses from a list insted of two arguments.
+
+
+## Func
+
+Functional combinators.
+
+### id
+```
+Func.id(x : 'a) : 'a
+```
+
+Identity function. Returns its argument.
+
+
+### const
+```
+Func.const(x : 'a) : 'b => 'a = (y) => x
+```
+
+Constant function constructor. Given `x` returns a function that returns `x` regardless of its argument.
+
+
+### flip
+```
+Func.flip(f : ('a, 'b) => 'c) : ('b, 'a) => 'c
+```
+
+Switches order of arguments of arity 2 function.
+
+
+### comp
+```
+Func.comp(f : 'b => 'c, g : 'a => 'b) : 'a => 'c
+```
+
+Function composition. `comp(f, g)(x) == f(g(x))`.
+
+
+### pipe
+```
+Func.pipe(f : 'a => 'b, g : 'b => 'c) : 'a => 'c
+```
+
+Flipped function composition. `pipe(f, g)(x) == g(f(x))`.
+
+
+### rapply
+```
+Func.rapply(x : 'a, f : 'a => 'b) : 'b
+```
+
+Reverse application. `rapply(x, f) == f(x)`.
+
+
+### recur
+```
+Func.recur(f : ('arg => 'res, 'arg) => 'res) : 'arg => 'res
+```
+
+The Z combinator. Allows performing local recursion and having anonymous recursive lambdas. To make function `A => B` recursive the user needs to transform it to take two arguments instead – one of type `A => B` which is going to work as a self-reference, and the other one of type `A` which is the original argument. Therefore, transformed function should have `(A => B, A) => B` signature.
+
+Example usage:
+```
+let factorial = recur((fac, n) => if(n < 2) 1 else n * fac(n - 1))
+```
+
+If the function is going to take more than one argument it will need to be either tuplified or have curried out latter arguments.
+
+Example (factorial with custom step):
+
+```
+// tuplified version
+let factorial_t(n, step) =
+ let fac(rec, args) =
+ let (n, step) = args
+ if(n < 2) 1 else n * rec((n - step, step))
+ recur(fac)((n, step))
+
+// curried version
+let factorial_c(n, step) =
+ let fac(rec, n) = (step) =>
+ if(n < 2) 1 else n * rec(n - 1)(step)
+ recur(fac)(n)(step)
+```
+
+
+### iter
+```
+Func.iter(n : int, f : 'a => 'a) : 'a => 'a
+```
+
+`n`th composition of f with itself, for instance `iter(3, f)` is equivalent to `(x) => f(f(f(x)))`.
+
+
+### curry
+```
+Func.curry2(f : ('a, 'b) => 'c) : 'a => ('b => 'c)
+Func.curry3(f : ('a, 'b, 'c) => 'd) : 'a => ('b => ('c => 'd))
+```
+
+Turns a function that takes n arguments into a curried function that takes
+one argument and returns a function that waits for the rest in the same
+manner. For instance `curry2((a, b) => a + b)(1)(2) == 3`.
+
+
+### uncurry
+```
+Func.uncurry2(f : 'a => ('b => 'c)) : ('a, 'b) => 'c
+Func.uncurry3(f : 'a => ('b => ('c => 'd))) : ('a, 'b, 'c) => 'd
+```
+
+Opposite to [curry](#curry).
+
+
+### tuplify
+```
+Func.tuplify2(f : ('a, 'b) => 'c) : (('a * 'b)) => 'c
+Func.tuplify3(f : ('a, 'b, 'c) => 'd) : 'a * 'b * 'c => 'd
+```
+
+Turns a function that takes n arguments into a function that takes an n-tuple.
+
+
+### untuplify
+```
+Func.untuplify2(f : 'a * 'b => 'c) : ('a, 'b) => 'c
+Func.untuplify3(f : 'a * 'b * 'c => 'd) : ('a, 'b, 'c) => 'd
+```
+
+Opposite to [tuplify](#tuplify).
+
+
+## Pair
+
+Common operations on 2-tuples.
+
+### fst
+```
+Pair.fst(t : ('a * 'b)) : 'a
+```
+
+First element projection.
+
+
+### snd
+```
+Pair.snd(t : ('a * 'b)) : 'b
+```
+
+Second element projection.
+
+
+### map1
+```
+Pair.map1(f : 'a => 'c, t : ('a * 'b)) : ('c * 'b)
+```
+
+Applies function over first element.
+
+
+### map2
+```
+Pair.map2(f : 'b => 'c, t : ('a * 'b)) : ('a * 'c)
+```
+
+Applies function over second element.
+
+
+### bimap
+```
+Pair.bimap(f : 'a => 'c, g : 'b => 'd, t : ('a * 'b)) : ('c * 'd)
+```
+
+Applies functions over respective elements.
+
+
+### swap
+```
+Pair.swap(t : ('a * 'b)) : ('b * 'a)
+```
+
+Swaps elements.
+
+
+## Triple
+
+### fst
+```
+Triple.fst(t : ('a * 'b * 'c)) : 'a
+```
+
+First element projection.
+
+
+### snd
+```
+Triple.snd(t : ('a * 'b * 'c)) : 'b
+```
+
+Second element projection.
+
+
+### thd
+```
+Triple.thd(t : ('a * 'b * 'c)) : 'c
+```
+
+Third element projection.
+
+
+### map1
+```
+Triple.map1(f : 'a => 'm, t : ('a * 'b * 'c)) : ('m * 'b * 'c)
+```
+
+Applies function over first element.
+
+
+### map2
+```
+Triple.map2(f : 'b => 'm, t : ('a * 'b * 'c)) : ('a * 'm * 'c)
+```
+
+Applies function over second element.
+
+
+### map3
+```
+Triple.map3(f : 'c => 'm, t : ('a * 'b * 'c)) : ('a * 'b * 'm)
+```
+
+Applies function over third element.
+
+
+### trimap
+```
+Triple.trimap(f : 'a => 'x, g : 'b => 'y, h : 'c => 'z, t : ('a * 'b * 'c)) : ('x * 'y * 'z)
+```
+
+Applies functions over respective elements.
+
+
+### swap
+```
+Triple.swap(t : ('a * 'b * 'c)) : ('c * 'b * 'a)
+```
+
+Swaps first and third element.
+
+
+### rotr
+```
+Triple.rotr(t : ('a * 'b * 'c)) : ('c * 'a * 'b)
+```
+
+Cyclic rotation of the elements to the right.
+
+
+### rotl
+```
+Triple.rotl(t : ('a * 'b * 'c)) : ('b * 'c * 'a)
+```
+
+Cyclic rotation of the elements to the left.
+
+## BLS12\_381
+
+### Types
+- `fp // Built-in (Montgomery) integer representation 32 bytes`
+- `fr // Built-in (Montgomery) integer representation 48 bytes`
+- `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 }`
+
+### pairing\_check
+```
+BLS12_381.pairing_check(xs : list(g1), ys : list(g2)) : bool
+```
+
+Pairing check of a list of points, `xs` and `ys` should be of equal length.
+
+### int_to_fr
+```
+BLS12_381.int_to_fr(x : int) : fr
+```
+
+Convert an integer to an `fr` - a 32 bytes internal (Montgomery) integer representation.
+
+### int_to_fp
+```
+BLS12_381.int_to_fp(x : int) : fp
+```
+
+Convert an integer to an `fp` - a 48 bytes internal (Montgomery) integer representation.
+
+### fr_to_int
+```
+BLS12_381.fr_to_int(x : fr) : int
+```
+
+Convert a `fr` value into an integer.
+
+### fp_to_int
+```
+BLS12_381.fp_to_int(x : fp) : int
+```
+
+Convert a `fp` value into an integer.
+
+### mk_g1
+```
+BLS12_381.mk_g1(x : int, y : int, z : int) : g1
+```
+
+Construct a `g1` point from three integers.
+
+### mk_g2
+```
+BLS12_381.mk_g2(x1 : int, x2 : int, y1 : int, y2 : int, z1 : int, z2 : int) : g2
+```
+
+Construct a `g2` point from six integers.
+
+### g1_neg
+```
+BLS12_381.g1_neg(p : g1) : g1
+```
+
+Negate a `g1` value.
+
+### g1_norm
+```
+BLS12_381.g1_norm(p : g1) : g1
+```
+
+Normalize a `g1` value.
+
+### g1_valid
+```
+BLS12_381.g1_valid(p : g1) : bool
+```
+
+Check that a `g1` value is a group member.
+
+### g1_is_zero
+```
+BLS12_381.g1_is_zero(p : g1) : bool
+```
+
+Check if a `g1` value corresponds to the zero value of the group.
+
+### g1_add
+```
+BLS12_381.g1_add(p : g1, q : g1) : g1
+```
+
+Add two `g1` values.
+
+### g1_mul
+```
+BLS12_381.g1_mul(k : fr, p : g1) : g1
+```
+
+Scalar multiplication for `g1`.
+
+### g2_neg
+```
+BLS12_381.g2_neg(p : g2) : g2
+```
+
+Negate a `g2` value.
+
+### g2_norm
+```
+BLS12_381.g2_norm(p : g2) : g2
+```
+
+Normalize a `g2` value.
+
+### g2_valid
+```
+BLS12_381.g2_valid(p : g2) : bool
+```
+
+Check that a `g2` value is a group member.
+
+### g2_is_zero
+```
+BLS12_381.g2_is_zero(p : g2) : bool
+```
+
+Check if a `g2` value corresponds to the zero value of the group.
+
+### g2_add
+```
+BLS12_381.g2_add(p : g2, q : g2) : g2
+```
+
+Add two `g2` values.
+
+### g2_mul
+```
+BLS12_381.g2_mul(k : fr, p : g2) : g2
+```
+
+Scalar multiplication for `g2`.
+
+### gt_inv
+```
+BLS12_381.gt_inv(p : gt) : gt
+```
+
+Invert a `gt` value.
+
+### gt_add
+```
+BLS12_381.gt_add(p : gt, q : gt) : gt
+```
+
+Add two `gt` values.
+
+### gt_mul
+```
+BLS12_381.gt_mul(p : gt, q : gt) : gt
+```
+
+Multiply two `gt` values.
+
+### gt_pow
+```
+BLS12_381.gt_pow(p : gt, k : fr) : gt
+```
+
+Calculate exponentiation `p ^ k`.
+
+### gt_is_one
+```
+BLS12_381.gt_is_one(p : gt) : bool
+```
+
+Compare a `gt` value to the unit value of the Gt group.
+
+### pairing
+```
+BLS12_381.pairing(p : g1, q : g2) : gt
+```
+
+Compute the pairing of a `g1` value and a `g2` value.
+
+### miller_loop
+```
+BLS12_381.miller_loop(p : g1, q : g2) : gt
+```
+
+Do the Miller loop stage of pairing for `g1` and `g2`.
+
+### final_exp
+```
+BLS12_381.final_exp(p : gt) : gt
+```
+
+Perform the final exponentiation step of pairing for a `gt` value.