_images/combine.png

Contracts

A smart contract is a script whose inputs and outputs are data stored on a distributed database. The logic of the contract can be interacted with through transactions and can run complex logic that processes read and writes to the database. Smart contracts can model a specific process associated with a real world financial instrument or contract, but are only a subset of the logic which involves counterparty communication and settlement. They are not an embodiment of legal logic or terms of a contract. Put simply, contracts are effectively a data reconciliation workflow on a database that corresponds to a business process.

Contracts are constructed in Uplink’s scripting language. The contracts constructed in FCL are described in an asset modeling language which does not allow arbitrary computation to be constructed - it is not a general purpose tool. Instead, FCL is constructed to be model a specific set of requirements around the static analysis of contracts and facilitate both humans and machine intelligences to analyze the integrity and all possible states of the contract.:

$ uplink scripts compile <inputfile>

State Diagram

A contract consists of a state sequence diagram which is a directed graph. A contract is only ever in a single state at a point in time. The possible sequence of states that the contract can enter is described as a graph structure of edges and nodes which define the validity of a state transition. This allows us to analyze all possible paths of execution, and their memory states by restricting the methods and logic that a contract can execute while in a state.

_images/Flow.png

Every contract has an initial and terminal state which are are the start and end points of it’s lifetime. The reset of the intermediate states (example: settlement, confirmation, trading etc) are named nodes in the graph which restrict the possible methods and logic that can be called.

_images/dot.png

To generate the graph description of a contract:

$ uplink scripts graph <inputfile>

State Annotations

FCL methods may be annotated with a precondition as in

@annotation
foo() {
  ...
}

annotation names the state the contract has to be in order to allow calls to the annotated method. That means, if there wasn’t a call to transitionTo(:annotation:), calls to foo() will be rejected. State annotations are used to define valid directions inside a contract. This is easily seen when looking at contracts written in AML, our proprietary Asset Moddeling Language, where a contract’s life cycle has to start in the method annotated with @initial and end using the primop terminate(msg).

Turing-Incomplete

FCL was specifically designed as a turing incomplete programming language. General purpose languages like Python and Haskell are turing complete. Turing complete languages give the programmer the ability to write arbitrary programs. In contrast, turing incomplete languages restrict the type of programs one can write. Restricting the kind of programs the user could write might look like a bad idea but as it turns out, being turing complete is a disadvantage when safety and a high degree of analyzability of programs are of highest priority. For example, the famous halting problem tells us that it is impossible to tell if a program will terminate in a finite number of computation steps or run indefinitely. Being turing incomplete makes it possible for us to guarantee program termination.

Uplink and FCL are tailored for financial applications which do not require Turing completeness and greatly profit from the benefits of safety and analyzability.

Totality

FCL is total, all programs and calls to methods terminate in a finite number of steps which is enforced statically. Unbounded computation is rejected statically.

Methods

FCL methods are defined in the source code of smart contracts, directly following global and local variable declarations and assignment. The are comprised of a method name, a list of zero or more arguments, and a function body which may contain variable assignments and primitive operations (defined in the Primitive Operations section) and may or may not return a result.

Methods cannot call themselves nor other contract defined methods within the body, as this would allow for recursion and would severely limit the ways in which the contract code can be statically analyzed. Methods are publically available functions that define the means in which counterparties can interact with smart contracts; they provide the means in which smart contracts make state transitions referenced in the State Diagram section.

Types

FCL is a typed language which assigns a static type to all possible values in the language. This type restricts the possible values and functions that can operate over the expression in the language and prevent invalid states from occurring.

Type Description
int Type of 64 bit integers
float Type of double precision floats
bool Type of booleans
account Type of account addresses
asset Type of asset addresses
contract Type of contract addresses
msg Type of messages
sig Type of ECDSA signature
void Type of void
state Type of graph state labels
date Type of dates
any Type of any type

Built-in Functions

Primitive operations are methods defined in the FCL language specification, usable in any smart contract method body. They provide functionality that allow smart contract composers to perform useful operations that would not be able to be written using other language primitives.

Function | Arguments | Return Type | Description
verify(msg,sig) 2 bool Verify a signature
sign(msg) 1 sig Sign a message
block() 0 int Active block
owner() 0 account Return the owner of a contract
sender() 0 account Return the creator of current transaction
created() 0 int Time of contract creation
address() 0 address Address of contract
validator 0 account Current validator of contract
sha256(any) 1 msg SHA256 digest of a message
accountExists(addr) 1 bool Check if an account exists in world state
assetExists(addr) 1 bool Check if an asset exists in world state
contractExists(addr) 1 bool Check if a contract exists in world state
transferTo(asset,int) 2 void Transfer n asset holdings to account
transferFrom(asset,int,account) 3 void  
transferHoldings(account,asset,int,account) 4 void  
terminate(msg) 1 any Transition to terminal state
now() 0 date Block creation time of current transaction
transitionTo(state) 1 void Transition to named state
currentState() 0 state Get the current state
between(datetime,datetime,datetime) 3 bool Check if $0 lies between $1 (start) and $2 (end)
txHash() 0 msg Hash of current transaction
bound(asset,account) 2 bool Check bound status of an asset / contract pair

Deltas

A delta is a “side-effect” induced by running a method on a script, that alters some aspect of the ledger world state. When a block is mined, all deltas are computed for all transactions and applied to the end-result world-state of the block.

There are five different types of deltas

Delta Description
ModifyGlobal Modify a contract state variable
ModifyLocal Modify a local state variable
ModifyAsset Modify an asset
Atomic Combine two operations as atomic
Terminate Terminate the contract

Deltas are created for updating global variables, local variables, and assets.

  • ModifyGlobal change the global contract state visible to all participants of the network.
  • ModifyLocal describes operations on local storage kept off the network which resides off-chain only on the involved parties’ nodes.
  • ModifyAsset deltas describe asset changes in the ledger world state.
  • Terminate halts contract execution

Data Model

There are two main forms of data storage that exists in Uplink. The main storages are denoted on-ledger and off-ledger, in which data is either contained within a contract’s state or stored locally to a party’s node, respectively. The third is temporary storage, containing data that exists only for the duration of the execution of a contract method call.

  • On-ledger - Data stored on-ledger within a contract’s state (denoted by keyword “global” in top-level variable definitions in contracts).
  • On-ledger encrypted - Data stored on-ledger within a contract’s state and computed on using cryptographic protocols.
  • Off-ledger - Data stored off-ledger on counterparties’ local node (denoted by keyword “local” in top-level variable definitions in contracts).

Global Stores An on-ledger storage that maps variables to their values. These values are stored unencrypted such that their values are visible to all nodes on the network running the contract.

Local Stores An off-ledger storage that maps variables to their values. The state of of these variables is stored on the counterparties local system and are kept in sync by exchanging hashes of their state after every contract interaction. The local state of a contract synchronizes all counterparties local stores without explicitly sharing their data. This is used for private data that is kept hidden from the rest of the network.

Datetimes

In Uplink smart contracts, Dates and times are represented by Datetime values, syntactically designated by ISO8601 formatted strings. These values can be compared to other datetime values and manipulated by adding and subtracting timedeltas, allowing users to write sophisticated datetime logic and conditional branching logic in smart contracts like you may expect in any useful financial DSL.

Syntax

"YYYY-MM-DDThh:mm:ssTZD"
  where
    YYYY = four-digit year
    MM   = two-digit month (01=January, etc.)
    DD   = two-digit day of month (01 through 31)
    hh   = two digits of hour (00 through 23) (am/pm NOT allowed)
    mm   = two digits of minute (00 through 59)
    ss   = two digits of second (00 through 59)
    s    = one or more digits representing a decimal fraction of a second
    TZD  = time zone designator (Z or +hh:mm or -hh:mm)

Example:

"1999-02-23T23:13:40+05:00"
"2015-10-10T00:00:00Z"

Operations:

Datetime == Datetime
Datetime < Datetime
Datetime <= Datetime
Datetime > Datetime
Datetime >= Datetime
Datetime + TimeDelta (*)
Datetime - TimeDelta (*)

[*] Behavior of TimeDelta Additon/Subtraction:

Because Uplink smart contracts support adding and subtracting time deltas using the time units of years and months, there are some non-intuitive properties of these operations that emerge; Notably, adding and then subtracting the same time delta (or vice versa) from a datetime value does not always result in the initial datetime. This arises in situations where the intermediate datetime month has fewer days than the initial datetime. In this case, adding 1 month does not add a consistent number of days to the initial datetime, but instead increments the month number by one. In the case that the resulting day of the month is not a valid day of the month, the day of the month is reduced to the last valid day of the resulting month. This behavior is the same for subtracting delta values from datetime values.:

"2017-08-31T00:00:00Z" + 1mo == "2017-09-30T00:00:00Z"
"2017-10-31T00:00:00Z" - 1mo == "2017-09-30T00:00:00Z"

In the case of leap years, adding or subtracting time deltas behave the same as in the example above, but the only instance in which this happens is when the initial and resulting years are both a leap year or both not a leap year, and the initial datetime is Feb 29th of the leap year.:

"2016-02-29T00:00:00Z" + 1y    == "2017-02-28T00:00:00Z"
"2015-01-31T00:00:00Z" + 1y1mo == "2016-02-29T00:00:00Z"
"2017-03-31T00:00:00Z" - 1y1mo == "2016-02-29T00:00:00Z"

TimeDeltas

In Uplink smart contracts a timedelta represents an amount of time comprised of years, months, days, hours, minutes, and seconds. The values of each must be positive, and any number of each may be specified. Internal to Uplink, hours, mins, and seconds are capped at 23, 59, and 59 respectively. te that if a larger number of each is specfied in the body of a timedelta literal, they wil roll over into the next time quantity (e.g. 25h will be turned into 1d1h). Though the time units must be written in order, it is not necessary to include every time unit in the value representation of the time delta. For instance, if adding only 1 month and 12 hours is desired, one can write 1mo12h instead of 0y1mo0d12h0m0s.

Syntax:

NyNmoNdNhNmNs
  where
    N = natural number

Examples:

1y6mo3d4h4m2s
(read as 1 year, 6 months, 3 days, 4 hours, 4 mins, and 2 seconds)

6mo12h
(read as 6 months and 12 hours)

1y100d59s
(read as 1 year, 100 days, and 59s)

Operations:

TimeDelta + TimeDelta
TimeDelta - TimeDelta (*)
Datetime + TimeDelta
Datetime - TimeDelta

[*] Note: If the result of one of the units of time in a timedelta is negative after subtraction, that particular unit of time is trimmed to 0. This results from the invariant that timedeltas cannot be negative, i.e. a change in time is intuitively positive, and this positive value can be added or subtracted from a datetime.:

1y6mo2d - 5mo3d == 1y1mo
3y20d50m - 21d35m == 3y15m

Signatures

Signatures are authorizations by counterparties agreeing to allow contracts to mediate asset transfer on their behalf. A signature is a cryptographic signing of proof of an asset’s holdings and the terms of a contract involved. It verifies the coherence of the participant and their involvement in the specific terms and logic of a contract and their holdings in a specific asset represented by the contract.

Private Computation

When local variable (private variables stored off ledger) are manipulated by a contract function call, a Delta is emitted for each atomic manipulation. When a block is mined, every counterparty receives a list of deltas modifying local variabled and applys them to their local storage. In this way, the values of local variables are kept hidden, while manipulation of these variables may still occur. This is acheived through homomorphic encryption, which allows certain mathematical operations to be performed on cryptotext such that when decrypted, the same operations will have been perfomed on the plaintext.

Specifications

_images/Analysis.png

semantic debugger, symbolic execution engine, and a verification infrastructure.

There are two levels involved in the verification of contracts:

  1. Language-level - the coherence of the underlying language’s specification in terms of it’s static and dynamics.
  2. Contract-level - the coherence of a specification of a contracts expected behavior and it’s implementation.
  • Invariants
  • Obligations
  • Permissions
  • Signatures

A statement is considered satisfiable if it is possible to find an interpretation (model) that makes the formula true. The opposites of these concepts are unsatisfiability and invalidity. A formula is unsatisfiable if none of the interpretations make the formula true, and invalid if some such interpretation makes the formula false.

The expected behavior of a contract is a specification in the form of a collection of statements on the possible events that counterparties can trigger and observe during the lifetime of the contract.

  • Safety - That an event will never occur.
  • Liveness - That an event will eventually occur.

The coherence of the specification to the implementation of the contract is known as verification.

The FCL language itself has a set of semantics which define all possible ways that expressions in the language can be evaluated (i.e. dynamics of the language) in terms of ways that the expressions in the language are composed (i.e. the statics of the language).

Interactive Shell

We simulate method call behaviour by executing them in a local, non-ledger environment while recording the Deltas the call emits. Starting the REPL with the notary contract loaded:

uplink scripts repl -v contracts/notary.s

An interactive session using the notary.s contract:

Signatures:
put: (msg) -> ()
isSigAvail: () -> bool
get: () -> sig

FCL> put("Hello world!")
void

FCL> isSigAvail()
True

FCL> get()
41948375291644419605210209193538855353224492619856392092318293986323063962044,107700334619968687379383814047208033848482079826651194719876057606805546217303

Of interest are the Signatures and GlobalStorage contents fields. Signatures tells us which methods are loaded and how to call them. GlobalStorage contents depicts a mapping of global variables to their current values stored on the ledger.

Calling put() outputs:

FCL> put("Hello world")
    TempStorage =
        <empty>
    GlobalStorage =
        isSet : bool = False
        signature : any = undefined
    State = get
    Deltas =
        global isSet = True
        global signature = 41948375291644419605210209193538855353224492619856392092318293986323063962044,65432732904269095599117150201436533272177021737227908010721698477004321211036
        state = get
    Return = void

Return value shows the value returned by the method and deltas depict the Deltas emitted. In line with the notary’s code, isSet is set to True and signature gets assigned the ECDSA signature resulting from signing the supplied message.

Calling get() returns the signature’s value and leaves the variables untouched.:

FCL> get()
    TempStorage =
        x : msg = Hello world
    GlobalStorage =
        isSet : bool = True
        signature : sig = 41948375291644419605210209193538855353224492619856392092318293986323063962044,65432732904269095599117150201436533272177021737227908010721698477004321211036
    State = get
    Deltas =

    Return = 41948375291644419605210209193538855353224492619856392092318293986323063962044,65432732904269095599117150201436533272177021737227908010721698477004321211036

Individual expression and primitive operations can be evaluated as well:

FCL> address()
    State = get
    Deltas =

    Return = GnbRYHmoKwVXbbQrVdxpKZGmMg6jDQjaTBKohFoBujzH

FCL> transitionTo(:get)
    State = get
    Deltas =
        state = get
    Return = void

FCL> 12 * 15
    State = get
    Deltas =
        state = get
    Return = 180

Example: Minimal

global int x = 0 ;

transition initial -> set;
transition set -> get;
transition get -> terminal;

@get
getX () {
  terminate("Now I die.");
  return x;
}

@set
setX () {
  x = 42;
  transitionTo(:get);
  return void;
}

Example: Notary

global sig signature;
global bool isSet = False;

transition initial -> get;
transition get -> terminal;

@put
put(msg x) {
  if (sender() != owner()) {
    return void;
  } else { if (!isSet) {
      signature = sign(x);
      isSet = True;
    };
};

@isSigAvail
isSigAvail() {
  return isSet;
}

@get
get() {
  if (isSet) {
    return signature;
  } else {
    terminate("This is the end.");
  };
}

Grammar

Symbols

definition       =
concatenation    ,
termination      ;
alternation      |
optional         [ ... ]
repetition       { ... }
grouping         ( ... )
string-literal   " ... "
string-literal   ' ... '
comment          // ...
multicomment     /* ... */

Numbers

digit   = 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
digits  = digit , { digit }
integer = [-] , digits
float   = [-] , digits , "." , digits

Letters

lower   = 'a' | 'b' | 'c' | 'd' | 'e' | 'f' | 'g' | 'h' | 'i' | 'j' | 'k' | 'l' | 'm'
        | 'n' | 'o' | 'p' | 'q' | 'r' | 's' | 't' | 'u' | 'v' | 'w' | 'x' | 'y' | 'z'
upper   = 'A' | 'B' | 'C' | 'D' | 'E' | 'F' | 'G' | 'H' | 'I' | 'J' | 'K' | 'L' | 'M'
        | 'N' | 'O' | 'P' | 'Q' | 'R' | 'S' | 'T' | 'U' | 'V' | 'W' | 'X' | 'Y' | 'Z'
letter  = upper | lower

Literals

addr     = '"' , letter , { letter } , '"'
message  = "'" , letter , { letter } , "'"
datetime = "'" ISO 8601 "'"
literal  = integer | float | addr | message | False | True | datetime

Types

type    = "int" | "float" | "bool" | "account" | "asset" | "contract" | "msg" | "sig" | "void" | "datetime"

Expressions

var     = letter , [ "'" | "_" | { var } ]
args    = "(" , expr , [ "," , { expr } ] , ")"
block   = "{" , expr , "}"
expr    = var
        | literal
        | expr , ";" , expr
        | expr , "+" , expr
        | expr , "-" , expr
        | expr , "*" , expr
        | var  , "=" , expr
        | var  , args
        | "if" , expr , block
        | "if" , expr , block , "else" ,block
        | "before" , args , block
        | "after" , args , block
        | "between" , args , block
        | return expr

Note: Toplevel

def     = [ "global" | "local" ] , type , var , "=" , expr , ";"
method  = var , args , "{" , [ expr , ";" ] , "}"
program = [ def , { def } ] , [ method , { method } ]