sophia.tex

\section{Sophia smart contracts}
\label{sect:sophia}

Smart contracts \cite{szabo1996smart,hhz007} are
programs on the blockchain that can perform tasks with the data on that
blockchain. Typically contracts have state (data), which is recorded on the
chain. A call to a function in the contract results in a return value
and updated state, both put back on the chain as a result of the
call.

Smart contracts are an active research field
\cite{DBLP:journals/corr/abs-1710-06372} and a substantial amount of
  effort goes in to studying the verification and validation of smart contracts
  \cite{magazzeni2017validation,bhargavan2016formal}.

There are two major technical challenges for smart contract
implementations. The first challenge is to make the contracts
execute fast without requiring too many resources. In a blockchain
implementation, contract execution is performed in a
\textit{virtual machine}. This is an execution engine with formally
defined semantics, such that all implementations perform exactly the
same computation steps, with exactly the same result and charging
exactly the same amount of gas. The \blockchain\ defines two virtual
machines, the AEVM, inspired by the Ethereum blockchain, and the more
safe and efficient FATE virtual machine.

The second challenge is to design a language to express contracts in
such a way that one can understand and reason about the contract
both as a human, but also mechanically by computer programs. The
language should by design protect contract designers against
vulnerabilities that can be exploited. Sophia is a functional language
to accommodate for these properties. It is designed as a contract
language with security and user comfort in mind. In particular,
vulnerabilities in contracts in other languages
\cite{atzei2017survey,mehar2019understanding,delmolino2016step} have been
studied with the goal to
avoid the possibility to make such mistakes in Sophia.

% Contracts are put on chain by contract create
% transactions, specifying their byte code and data to compute the
% initial state. A contract on chain is called by contract call
% transactions\footnote{in
%  \aet\ contracts are executed by explicit calls, there is no
%  mechanism to automatically progress computation.}. Each contract
% creation and contract call requires computation effort and the user is paying
% for that effort by paying for \textit{gas}. Each operation is
% associated with a certain amount of gas and the total used gas is paid
% for. The user specifies how much gas is provided in the transaction. A
% surplus is returned. If there is too little gas provided, the
% transaction is accepted (it is recorded
% on the chain), and the user pays for transaction fee and gas,
% but the contract computation fails and the contract state remains unchanged.

\subsection{The Sophia language}

Sophia is a functional programming language \cite{hughes1989functional}.
The main unit of code in Sophia is the \textit{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 \textit{contract instance} is an entity living on the
blockchain (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 \texttt{state}
encapsulating its local state. When creating a new contract the
\texttt{init} entrypoint is executed and the state is initialized to its
return value.


\subsubsection{Dutch auction contract}

As an example, let us consider an auction contract.  In such an
auction contract, a user could auction an object in the real world by
creating and posting a contract to the blockchain, using a \textbf{contract
create transaction}. Let us assume that
this is a Dutch auction, then the initial price
would be set high and for each new key-block that is mined (representing
time) the price is decreased. Someone buys the object by calling a
\texttt{bid} function. When this bidding \textbf{contract call transaction}
executes,
the contract computes the price given the current block number; if the caller
has
supplied enough coins in that call, the seller is paid, the
bidder is charged (possibly refunded the extras) and the contract
enters a non sellable state for the object. The next bidder will fail
the call and only pays for transaction costs, not for the object.

The complete Sophia code for a Dutch auction is presented here:

\begin{verbatim}
contract DutchAuction =

  record state = { amount : int,
                   height : int,
                   dec    : int,
                   sold   : bool }

  entrypoint init(price, decrease) : state =
    { amount = price,
      height = Chain.block_height,
      dec    = decrease,
      sold   = false }

  stateful payable entrypoint bid() =
    require( !state.sold, "sold"  )
    let price = demanded_price()
    require( Contract.balance >= price, "not enough tokens" )
    Chain.spend(Contract.creator, price)
    Chain.spend(Call.origin, Contract.balance)
    put(state{sold = true})

  function demanded_price() : int =
    state.amount - (Chain.block_height - state.height) * state.dec

\end{verbatim}

The contract languages and hence the evaluation in the virtual
machine, must have access to blockchain primitives like the height of
the chain and caller accounts. Typically, all blockchain
primitives are available from within a contract.

Note that the contract create transaction includes the contract
byte code, not the source code, together with information on
which version of the compiler is used. Compiled for FATE this contract
results in 254 bytes, whereas compiled for the AEVM 2092 bytes are
needed. The gas needed to compute the initial state is 240 for FATE compared
to 741 for the AEVM.

The \texttt{init} function is called when the contract is created to
compute the initial state of the contract. The \texttt{init} function
is not part of the byte code, such that it cannot accidentally be
called again. If one wants to reset the state, this has to be
explicitly programmed to avoid expensive exploits
\cite{suiche2017280}.
The contract designer also has to explicitly mention whether the
state of the contract is changed in a call (using the
\texttt{stateful} keyword).
Entrypoints can be called from outside the contract, whereas functions
are only accessible from within the contract.

The keyword \texttt{payable} is added to explicitly state which
function calls expect to come with additional tokens in the contract
call transaction. These tokens are added to the contract balance
before the call is made. If, however, the call is reverted by a failing
\texttt{require}d condition, then the provided tokens are returned.

The transparency of the blockchain guarantees that it is verifiable
that the first valid bid on chain\footnote{The \blockchain\
  does not guarantee that the first one posting a valid bid becomes
  the first one on chain.} is correctly paying the right
price. Moreover, it is verifiable that the bidding call transactions accepted
later are
only charged a transaction fee and the cost of execution.
The sale conditions are transparent, but whether the actual object ever
arrives is outside the scope of the blockchain


\subsubsection{State Channel example}

Contracts can be deployed on-chain or in a state channel. State channels
provide means for two parties for executing transactions off-chain. Once the
channel is opened on-chain all the communication is moved off-chain and it is
just between the two participants. It is not limited by blockchain
throughputh, fees or gas costs. This provides a new environment to run
contracts in. In order to make most out of it, off-chain contracts can use
on-chain data.

An example of the use of off-chain contract and an on-chain oracle can be
illustrated with a simple insurance contract. Note that all computation on a
blockchain must be deterministic in order to be able to validate the results.
If not exactly the same, the corresponding state hashes will differ. This is
true especially with state channels as contracts are executed by both
participants in their own context. This requires both to share the same view
of the chain\footnote{We achieve this by specifying the on-chain environment
as part of the off-chain update.}.

Running a simple insurance contract in which one user provides the service
while the other insures their property for a certain timeframe from hailstorm
requires some input from real life data. This is where oracle input comes: for
the example we have an on-chain Oracle to produce data on whether there has
been a hailstorm in a certain city. It publishes data pinned in time with a
corresponding block height when it occurred. Later on the insured participant
can use this response in order to claim their compensation. This can be done
off-chain and it wouldn't consume any gas. If the insurer refuses to follow
the contract, the insured party can use the blockchain as an arbiter and
execute the contract on-chain.

So assume there is such an oracle, monitoring the weather and registered with
a reasonable query fee covering for its cost of operation. The oracle has an
identifier, for the example say
\begin{quote}
  \textit{"ok\_shEHMV8Q2F1HR86pcyF7DYpudg8hnvJwJuVE3berWpbktnL2R"}.
\end{quote}
We can now write a Sophia contract that takes this oracle identifier as input
of its initialization and uses it for claiming the insurance. 

\begin{verbatim}
contract ChannelInsurance =

  type city_t       = string
  type gen_height_t = int
  type query_t      = city_t * gen_height_t
  type answer_t     = bool
  type oracle_id    = oracle(query_t, answer_t)
  type query_id     = oracle_query(query_t, answer_t)

  record state = { oracle          : oracle_id,
                   city            : city_t,
                   active_from     : gen_height_t,
                   active_to       : gen_height_t,
                   price_per_gen   : int,
                   compensation    : int
                   }

  entrypoint init(oracle : oracle_id, city: city_t, 
    price_per_gen: int, compensation: int) : state =
        { oracle          = oracle,
          city            = city,
          price_per_gen   = price_per_gen,
          compensation    = compensation,
          active_from     = 0,
          active_to       = 0
          }

  stateful payable entrypoint insure() =
    require(Call.caller != Contract.creator, "service_provider")
    require(Contract.balance + Call.value >= state.compensation, 
        "not_enough_compensation")
    let period : int = Call.value / state.price_per_gen
    if (Chain.block_height >= state.active_to) // expired, renew
      put(state{ active_from = Chain.block_height,
                 active_to = Chain.block_height + period})
    else // not expired, extend
      put(state{ active_to = state.active_to + period })

  stateful entrypoint withdraw(amount: int) =
    require(Call.caller == Contract.creator, "not_service_provider")
    if (Chain.block_height =< state.active_to) // insured
      require(Contract.balance - amount >= state.compensation, 
        "not_enough_compensation")
    Chain.spend(Contract.creator, amount)

  payable entrypoint deposit() =
    require(Call.caller == Contract.creator, "not_service_provider")

  entrypoint get_insurance_range() =
    (state.active_from, state.active_to)

  stateful entrypoint claim_insurance(q: query_id) =
    require(Call.caller != Contract.creator, "service_provider")
    switch(Oracle.get_answer(state.oracle, q))
      None         =>
        abort("no_response")
      Some(was_there_hailstorm) =>
        let (city, generation) = Oracle.get_question(state.oracle, q)
        require(city == state.city, "different_city")
        let is_in_range = generation >= state.active_from 
            && generation =< state.active_to
        require(is_in_range, "not_in_insurance_range")
        require(was_there_hailstorm, "different_response")
        Chain.spend(Call.caller, state.compensation)
        put(state{ active_from = 0,
                   active_to = 0})

\end{verbatim}

The contract is deployed by the insurance service provider in a state channel.
It stores the reference to the trusted oracle in its state, the price it
expects for insurance for a single generation and in which city the insured
city belongs to. It also contains the insured interval in block heights, which
initially is set to 0.

The creator of this contract may now deposit initial amount for compensation.

\begin{verbatim}
  payable entrypoint deposit() =
    require(Call.caller == Contract.creator, "not_service_provider")
\end{verbatim}

Note that there is a check there: only the owner of the contract - being the
service provider - can execute that function. Since the insured participant is
not expected to call that function - any attempt of doing so will result in
aborting the call. This is true both off-chain and on-chain in a forced
progress scenario.

The keyword \verb+payable+ expresses that we expect the caller to add a token
amount to the contract call transaction, which could be checked by comparing
\verb+Call.value+. There is no restriction for the amount being deposited in
the contract and this could be done in a couple of different steps if needed.

Once the compensation is present in the contract, the other party can
call the \verb+insure+ function.

\begin{verbatim}
  stateful payable entrypoint insure() =
    require(Call.caller != Contract.creator, "service_provider")
    require(Contract.balance + Call.value >= state.compensation, 
        "not_enough_compensation")
    let period : int = Call.value / state.price_per_gen
    if (Chain.block_height >= state.active_to) // expired, renew
      put(state{ active_from = Chain.block_height,
                 active_to = Chain.block_height + period})
    else // not expired, extend
      put(state{ active_to = state.active_to + period })
\end{verbatim}

There are some checks that it is not the insurance provider that is calling
the contract and that the contract has enough tokens to cover the compensation
in case of a hailstorm. If those pass the corresponding insurance period is
calculated according to the tokens dedicated in the contract and the state is
updated accordingly. Note that if there is an active insurance at the moment,
the existing time frame is just extended. This allows for continuous insurances.

Once an insurance event takes place, the insured party simply claims their
due, providing the Oracle's response.

\begin{verbatim}
  stateful entrypoint claim_insurance(q: query_id) =
    require(Call.caller != Contract.creator, "service_provider")
    switch(Oracle.get_answer(state.oracle, q))
      None         =>
        abort("no_response")
      Some(was_there_hailstorm) =>
        let (city, generation) = Oracle.get_question(state.oracle, q)
        require(city == state.city, "different_city")
        let is_in_range = generation >= state.active_from 
            && generation =< state.active_to
        require(is_in_range, "not_in_insurance_range")
        require(was_there_hailstorm, "different_response")
        Chain.spend(Call.caller, state.compensation)
        put(state{ active_from = 0,
                   active_to = 0})
\end{verbatim}

Note that if any of the checks fail, the whole execution of the contract
fails. This makes the state channel contract safe and trustless in both
off-chain environment and in forced progress context. It is worth mentioning
that in both scenarios it is only the two participants that can execute the
contract. This is a big difference with on-chain deployed contracts.

If all checks pass, the caller of the contract - the insured party - claims
the compensation and the insurance is considered to closed.

This contract is far from fully secure, but illustrates an example of
how contracts in state channels can use on-chain data.

\subsection{Readable Smart Contracts in Lexon}
Human readable smart contracts compiling to Sophia.
...

\subsection{The FATE virtual machine}
\label{sect:fate}

The Fast Aeternity Transaction Engine (FATE) VM uses transactions as
its basic operations and operates directly on the state tree of the
\aet\ chain. This enables native integration with first class
objects such as oracles, the naming system, and state channels since
those are all managed by specific types of transactions described on
the protocol level. FATE is a simple-to-use machine language, superior
to the more traditional byte-code virtual machines currently used on
other platforms. It enables easier, safe coding, faster transactions,
and smaller code sizes. It is custom-built to seamlessly integrate
with the functional smart contract language Sophia.

\subsubsection{More secure}

Every operation and every value is typed. Any type violation results in
an exception and reverts all state changes. This prevents people to
circumvent the compiler and write or modify their own FATE code to use
type violations as an attack vector.

The instruction memory is divided into functions and basic
blocks. Only basic blocks can be indexed and used as jump
destinations. This is a precaution to be unable to jump to arbitrary
positions in memory. It also fit FATE's function style by
having function calls instead of jumps. Moreover, data and control
flow are separated, one cannot possibly modify the running
contract, since the code memory cannot be written to.

FATE is “functional” in the sense that “updates” of data structures,
such as tuples, lists or maps do not change the old values of the
structure, instead a new version is created.  FATE does have the
ability to write the value of an operation back to the same register
or stack position as one of the arguments, in effect updating the
memory.

FATE solves a fundamental problem programmers run into when coding for
Ethereum: integer overflow, weak type checking and poor data
flow. FATE checks all arithmetic operations to keep the right meaning
of it. Integers cannot overflow, since FATE uses unbounded integer
arithmetic (cf.\ Bignums \cite{serpette1989bignum}). Floats are not
part of the language, avoiding a bunch of issues associated with
floating point arithmetic. Also you cannot cast types (e.g\ integers to
booleans). This makes
FATE ultimately a safer coding platform for smart contracts.

\subsubsection{More efficient}

FATE uses high level instructions. There are instructions to operate
on the chain state tree in a safe and formalized way. Likewise the
virtual machine has high-level support for most of the transactions
available on the \blockchain. There are operations such as
`ORACLE\_CHECK\_QUERY' for querying an oracle or `AENS\_CLAIM' for
claiming a name.

Having higher level instructions makes the code
deployed smaller and it reduces the blockchain size. FATE contracts
use on average ten times less space than the same contract compiled to
the AEVM, the Ethereum compatible VM. At the same time, it performs on
average much faster and uses therefore less gas.

FATE byte code by itself is already a readable program. For example, the bid
function of the Dutch auction contract compiles to this code:

\begin{verbatim}
FUNCTION bid( ) : {tuple,[]}
  ;; BB : 0
          ELEMENT a 3 store1
          NOT a a
          JUMPIF a 2
  ;; BB : 1
          ABORT "sold"
  ;; BB : 2
          CALL "(h:p"
  ;; BB : 3
          POP var1
          BALANCE a
          EGT a a var1
          JUMPIF a 5
  ;; BB : 4
          ABORT "not enough tokens"
  ;; BB : 5
          CREATOR a
          SPEND a var1
          BALANCE a
          ORIGIN a
          SPEND a a
          SETELEMENT store1 3 store1 true
          RETURNR ()
\end{verbatim}

The notion \verb+BB+ stands for basic block and jumps are always to
such a basic block. Note that for example `CREATOR', `SPEND' and
`BALANCE' are native instructions used in basic block 5. The
instruction \verb+ CALL "(h:p"+ in basic block 2 looks a bit cryptic for a call
to  the
function \verb+demanded_price()+. Each function name is hashed to 4
bytes that are printed as a string.

Both memory constraints and computation efficiency are important to
enable smaller contracts to to get more computation into a micro-block.