# Contract Examples

## Preliminary Notes

To **verify** the following examples use:

```
zebra -v Filename.fst
```

To **elaborate** and verify the elaborated result use:

```
zebra -e Filename.fst
```

The elaborated file will appear within the `output` subdirectory of your current directory.

In order for most of the examples to work you need to add the following lines at the beginning of your code:

```
open Zen.Cost

let main txSkeleton _ _ _ _ _ _ _ = Zen.ContractResult.ofTxSkel txSkeleton

let cf _ _ _ _ _ _ _ = ret #nat 4
```

## Simple Example

Let's create a simple function which takes a function and an argument and applies the function on the argument:

```
val applyOnce (#a #b:Type): (a -> b) -> a -> b
let applyOnce #_ #_ f x = f x
```

Elaborating the function will yield the following:

```
val applyOnce: #a: Type -> #b: Type -> (a -> b) -> a -> b
let applyOnce #_ #_ f x = inc 1 (f x)
```

That's because function application (`f x`) has a cost of 1, which is embedded into the let-expression with `inc`.

However - trying to compile this function will result in a typing error

* because you can only apply `inc` on a value of a

  `cost` type.

To fix it we modify the function to use `ret` on the result, to lift it into the `cost` monad, and we change the type signature to return a `cost` type (with a cost of 0 since that is the cost `ret` gives):

```
val applyOnce (#a #b:Type): (a -> b) -> a -> cost b 0
let applyOnce #_ #_ f x = ret (f x)
```

Now elaborating the function will yield the following:

```
val applyOnce (#a #b:Type): (a -> b) -> a -> cost b 0
let applyOnce #_ #_ f x = inc 2 (ret (f x))
```

That's because now we have **2 applications**, one of `f` on `x`, and the other of `ret` on the result.

Now the compilation would **still fail** with a typing error:

```
Subtyping check failed; expected type Zen.Cost.Realized.cost _ 0; got type Zen.Cost.Realized.cost _ (0 + 2)
```

That's because while the declared cost is 0, the **inferred** cost (due to the addition of `inc 2`) is 2.

To fix that we now have to declare the **correct** cost within the type, to account for the increment, so `cost b 0` becomes `cost b 2`:

```
val applyOnce (#a #b:Type): (a -> b) -> a -> cost b 2
let applyOnce #_ #_ f x = inc 2 (ret (f x))
```

Now that the syntactic cost is accounted for the program will compile.

## Aggregated Syntactic Cost

The following function takes a function `f` and an argument `x` and applies `f` on `x` and then applies it again on the result:

```
val applyTwice (#a:Type): (a -> a) -> a -> a
let applyTwice #_ f x = f (f x)
```

Elaborating this function will yield the following:

```
val applyTwice (#a:Type): (a -> a) -> a -> a
let applyTwice #_ f x = inc 2 (f (f x))
```

The increment by 2 is due to the fact there are 2 applications.

Again - this format won't do, and to be able to compile the elaborated program we have to lift the result into the cost monad and account for the additional costs:

```
val applyTwice (#a:Type): (a -> a) -> a -> cost a 3
let applyTwice #_ f x = ret (f (f x))
```

which will be elaborated as:

```
val applyTwice: #a: Type -> (a -> a) -> a -> cost a 3
let applyTwice #_ f x = inc 3 (ret (f (f x)))
```

Notice that this time we've predicted the increased elaborated cost in advance, so the original code won't compile (since `ret` gives a cost of 0) while the elaborated code will (since it will add `inc 3` to account for the costs of all the function applications).

In practice - **you won't be able to modify the elaborated code**, since the elaboration is done automatically when activating a contract, so instead you need to elaborate it locally, look at the result, and then modify the **original code** so it would compile right after the elaboration.

## Multiple Clauses

Now let's create another function - which takes a boolean `b`, a function `f`, and another argument `x`, and applies `f` on `x` **once** if `b` is `true` or **twice** if `b` is `false`.

We'll use the previously defined functions to do so:

```
val onceOrTwice (#a:Type): bool -> (a -> a) -> a -> cost a ?
let onceOrTwice #_ b f x = if b then applyOnce f x else applyTwice f x
```

What should be the declared cost of this function?

`applyOnce` gives a cost of **2**, while `applyTwice` gives a cost of **3**, so we have a **collision of costs**.

To reconcile the collision we manually insert `inc 1` to the `applyOnce f x` clasue to account for the difference between the costs, which would give both clauses of the `if-then-else` a cost of **3**:

```
val onceOrTwice (#a:Type): bool -> (a -> a) -> a -> cost a 3
let onceOrTwice #_ b f x = if b then inc 1 (applyOnce f x) else applyTwice f x
```

However - we still need to account for the syntactic cost of the `onceOrTwice` function itself - to do so we first elaborate the function, which gives us:

```
val onceOrTwice (#a:Type): bool -> (a -> a) -> a -> cost a 3
let onceOrTwice #_ b f x = inc 7 (if b then inc 1 (applyOnce f x) else applyTwice f x)
```

That is beacuse the `then` clause has **4 applications**, while the `else` clause has **3**, and since the syntactic cost of an `if-then-else` is defined as **3** + the maximal syntactic cost out of both clauses, which is **4** in this case, we get a total syntactic cost of **7**, which is embedded with an `inc 7` into the let-expression.

Now to account for the additional cost of **7** we change the declared cost of the function to **10**:

```
val onceOrTwice (#a:Type): bool -> (a -> a) -> a -> cost a 10
let onceOrTwice #_ b f x = inc 7 (if b then inc 1 (applyOnce f x) else applyTwice f x)
```

The elaborated code will now compile.

## Composition

Let's define 2 simple functions on the natural numbers - a function which takes a number and doubles it and a function which adds 7 to a number:

```
val double : nat -> nat
let double x = 2 * x

val add7 : nat -> nat
let add7 x = x + 7
```

We'll also define a function `foo` which would first double a number and then add 7 to the result, by composing the above functions:

```
val foo : nat -> nat
let foo x = add7 (double x)
```

The code will compile just fine, but not the elaboration.

To pass the elaboration we need to make sure all the functions are costed by lifting the results into the `cost` monad:

```
val double : nat -> cost nat 0
let double x = ret (2 * x)

val add7 : nat -> cost nat 0
let add7 x = ret (x + 7)
```

What about `foo`? trying to simply compose `add7` and `double` and lifting the result will now fail to typecheck:

```
val foo : nat -> cost nat 0
let foo x = ret (add7 (double x))
```

That's because we've changed the return type of the functions, so to compose them we have to use the **bind operator** (`>>=`):

```
val foo : nat -> cost nat 0
let foo x = ret x >>= double >>= add7
```

Now elaboration would still fail, so we have to account for the syntactic cost as well - let's look at the elaborated code:

```
val double: nat -> cost nat 0
let double x = (inc 3 (ret (2 * x)))

val add7: nat -> cost nat 0
let add7 x = (inc 3 (ret (x + 7)))

val foo: nat -> cost nat 0
let foo x = (inc 5 (ret x >>= double >>= add7))
```

By looking at the `inc`s we know that the cost of both `double` and `add7` is 3, so we modify their types in the original code:

```
val double : nat -> cost nat 3
let double x = ret (2 * x)

val add7 : nat -> cost nat 3
let add7 x = ret (x + 7)
```

What is the cost of `foo`? trying to simply give it a cost of 5 will **fail**:

```
val foo: nat -> cost nat 5
let foo x = (inc 5 (ret x >>= double >>= add7))
```

That's because we now have to take the costs of `double` and `add7` into account as well.

Recall that the type of the bind operator is: `cost a m -> (a -> cost b n) -> cost b (m+n)`, so it sums up the costs, which means that's exactly what we have to do.

Since the cost of `double` is **3**, the cost of `add7` is **3**, and the syntactic cost of `foo` is **5**, adding them all together gives us a cost of **11**:

```
val foo: nat -> cost nat 11
let foo x = (inc 5 (ret x >>= double >>= add7))
```

Now the elaborated code will compile.

## Recursion

The cost analysis becomes more complex once you introduce recursion.

The following function computes the factorial of a natural number:

```
val fact: nat -> int
let rec fact m =
    match m with
    | 0 -> 1
    | _ -> m * fact (m - 1)
```

Trying to elaborate this function will fail, since it doesn't return a `cost` type.

```
val fact: nat -> int
let rec fact m =
  inc 7
      (match m with
        | 0 -> 1
        | _ -> m * fact (m - 1))
```

To make sure the result is of a `cost` type - we apply `ret` on the base case, and bind the recursion step:

```
let rec fact m =
    match m with
    | 0 -> ret 1
    | _ -> fact (m - 1) >>= (fun r -> ret (m * r))
```

We might prefer to use some syntactic sugar to make the code look nicer:

```
let rec fact m =
    match m with
    | 0 -> ret 1
    | _ -> let! r = fact (m - 1)
           in ret (m * r)
```

What should be the return type of the new function? we can start with `cost int 0`:

```
val fact: nat -> cost int 0
let rec fact m =
    match m with
    | 0 -> ret 1
    | _ -> let! r = fact (m - 1)
           in ret (m * r)
```

Now the elaborated code will not compile, but it will give us some hints on how to specify the cost correctly:

```
val fact: nat -> cost int 0
let rec fact m =
  inc 10
      (match m with
        | 0 -> ret 1
        | _ -> let! r = fact (m - 1)
               in ret (m * r))
```

We might be tempted to assign a cost of **10** to the function, but that won't do - if the cost of `fact` is **10** then `fact (m - 1)` will have a cost of **10** and after accounting for the incremented syntactic cost (which is added by `inc 10`) we'll get that the **actual** cost of the function is **20**.

In fact - assuming **any** constant cost will yield a **contradiction**, since we'll always get another 10 steps added to what we've started with, which indicates that it is impossible to assign a constant cost to the function.

How do we resolve it? by making the cost **parametric** in the size of the input, by using **dependent types**.

First we explicitly declare the **name** of the input parameter **in the type**:

```
val fact: (m:nat) -> cost int 0
```

Then we can use this name within the cost expression, for example like this:

```
val fact: (m:nat) -> cost int m
```

But this won't do - we have to figure out the actual dependency of the cost on the parameter.

Let's assume for now the cost is some function `fact_c` on `m`:

```
val fact: (m:nat) -> cost int (fact_c m)
```

Looking at the definition of `fact` again - we immediately see a problem - the cost of `ret 1` is always **0**, while the cost of `fact (m-1)` is `fact_c (m-1)`, which **can't be 0**, so we have 2 pattern matching clauses with different costs.

This will result in a typing error when we try to compile the code, since all clauses of a `match-with` must return a result of the same type.

To fix that we need to add the difference to the first clause, like this (notice this is a modification of the original code, **not** the elaborated code):

```
val fact: (m:nat) -> cost int (fact_c m)
let rec fact m =
    match m with
    | 0 -> inc (fact_c (m-1)) (ret 1)
    | _ -> let! r = fact (m-1)
           in ret (m * r)
```

Instead of using `ret` and then `inc` we can just use `incRet`, which combines the 2:

```
val fact: (m:nat) -> cost int (fact_c m)
let rec fact m =
    match m with
    | 0 -> incRet (fact_c (m-1)) 1
    | _ -> let! r = fact (m-1)
           in ret (m * r)
```

Now we have to figure out what `fact_c` is.

Since the elaborator adds **10** to the cost, and this value didn't change with the addition of the `incRet` to the first clause (since the total syntactic cost for a `match-with` is determined only by the syntactically heaviest clause, which is still the second clause), we get **10** added to the cost **with each call to the function**, which means that the **base case** has **at least** a cost of **10**, and with each **recursion step** another **10** is added, so we get the following recurrence relation:

```
fact_c m = 10 + fact_c (m - 1)
```

What is the base case (for `m = 0`)?

Since we know it is **at least 10** (since the cost is increased by 10 and it can never be decreased), we can try assigning it to be 10, which gives us the solution:

```
fact_c m = 10 * (m + 1)
```

So let's try it:

```
val fact: (m:nat) -> cost int (10 * (m+1))
let rec fact m =
    match m with
    | 0 -> incRet (10 * m) 1
    | _ -> let! r = fact (m-1)
           in ret (m * r)
```

Now the function is elaborated to:

```
val fact: m: nat -> cost int (10 * (m + 1))
let rec fact m =
    inc 10
      (match m with
        | 0 -> incRet (10 * m) 1
        | _ -> let! r = fact (m - 1) in ret (m * r))
```

The program now compiles successfully, which indicates that the cost is now correct.

The keen-sighted reader will notice that the first clause `incRet (10 * m) 1` is operationally equivalent to `ret 1`, since the only case in which this clause is executed is when `m = 0`, but since all clauses must return a result of the same type, no matter if they are executed or not, the only way to pass the type checker is by explicitly handling the cost for all possible values of `m`.