Smart Contracts

Consensus

Use Cases

Troubleshooting

For Miners

Powered By GitBook

Contract Cost

The Cost Model

Central to the analysis of contracts cost is the notion of a *cost model*.

A *cost model* for a language assigns a natural number to each closed term in the language in such a way that the term should take **at most** this number of "abstract steps" to evaluate, this natural number is called *the cost* of that term (relative to that cost model).

The abstract steps could be, for example, beta-reductions, so if the cost of a term M is n it would take at most n beta-reductions to reduce M to a normal form with the chosen evaluation strategy of the language.

The cost is defined **recursively** on the structure of the term, and it could depend on the **values** of some of its subterms, so we can think of the cost as a term in the language which **evalutes** to a natural number.

We use the notation

$c\left(M\right)$

for the cost of the term M.Notice how the cost of both **function abstraction** and **applied let clause** is **0** - that's because function abstraction is in a **weak head normal form** - it's not evaluated further until it is applied on an argument, so as far as the execution environment is concerned it is **already a value**, so it won't be evaluated further; The cost of applied let clause is **0** as well, since an applied let expression if equivalent to a beta redex where the argument is itself a lambda (**internalized**, through the use of inc (which would be explained later).

$\textbf{let} \: f \: x = N \: \textbf{in} \: M$

is equivalent to $\left(\lambda f.M\right) \: \left(\lambda x.N\right)$

), so it is considered the same; In both cases the cost of the body of the function is In practice the actual cost (relative to the cost model) is **not computed directly**, instead - the cost is decomposed into 2 components:

1.

2.

â€‹

$\textbf{total cost}=\textbf{compositional cost}+\textbf{syntactic cost}$

In fact - given general recursion it is **impossible** to automatically compute the cost of any arbitrary term in the language.

Another deviation from the cost model is that the cost we give in practice is an **upper bound** on the cost given by the cost model, because it is easier to compute, but since the cost model itself is an upper bound on the number of steps the approximation we use in practice still gives a valid upper bound.

The **syntactic cost** is given to terms **by virtue of their form**, and acts as a **seed** which the **compositional cost** later **propogates** into the program through the **type system**.

The Cost Type

Given a cost model we define a special type constructor **value** of type

`cost`

to indicate that a term of type *cost*

` A m`

, where `A`

is a type and `m`

is a natural number, would take at most `m`

steps to produce a `A`

.Dually - we use the type **represents a value** of type A which **has taken** at most

`cost A m`

to indicate that a term of this type `m`

steps to evaluate.When a **term** *costed term*, with a *cost* of m.

`M`

has the type `cost A m`

we say that M is a When a **function** *costed function*, with a *cost* of

`f`

has the type` A -> cost B m`

we say that `f`

is a `m`

, which means that when given an input of type `A`

it takes `f`

at most `m`

steps to produce an output of type `B`

.Compositional Cost

The **indexed monad**, indexed over the additive monoid of the natural numbers, so whenever you compose (using Kleisli composition) 2 costed functions

`cost`

type constructor behaves as a an `f : B -> cost C n`

and` g : A -> cost B m`

you get a function of type `A -> cost C (m + n) `

where the cost is the sum of the costs of `f`

and `g`

.The **bind** operator (

`>>=`

) has the type signature:`bind: cost a m -> (a -> cost b n) -> cost b (m+n)`

In practice - the *ZF* is implemented as **the identity monad,** where the index could be set arbitrarily, so as far as *ZF** is concerned - **it is up to the developer to honestly declare the costs of terms*.

`cost`

monad in The compiler only makes sure that the costs are **composed correctly**.

To enforce the validity of the costs we combine the compiler with an **elaborator**, which would be explained in detail later on.

To lift a term into the monad we use the

`ret`

function, which is the unit of the monad and has the type `ret : a -> cost a 0`

. Since the `ret`

function gives a term a cost of `0`

, we use the function `inc : (m:nat) -> cost a n -> cost a (n+m)`

to increase the declared cost of a term.Syntactic Cost

The cost monad can only ensure that costs are composed correctly, but it cannot enforce the declared costs to conform to the cost model - it completely trusts the developer to declare costs honestly.

In order to actually **enforce** the cost model, we use a device called *the elaborator*.

The elaborator scans the syntax trees of the terms and recursively sums up the cost of each branch, adding additional constant cost with each clause and primitive operation.

Eventually, when the elaborator reaches either a **lambda expression**, or a **let expression** (which could be a **top-level let**) - it embeds the accumulated cost of the body of the expression into the body, by replacing it with an application of the inc function, along with the accumulated cost, on the body; this ensures 2 things:

1.

That the term returns an output which is wrapped in the cost

monad.

2.

That all the syntactic cost is accounted for.

Last modified 9mo ago

Copy link