Comment on page

# Contract Cost

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 ($\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 **internalized**, through the use of inc (which would be explained later).In practice the actual cost (relative to the cost model) is

**not computed directly**, instead - the cost is decomposed into 2 components:

1.Compositional Cost- which isdeclaredby thedeveloperandverifiedby thetype system 2.Syntactic Cost- which iscomputedby theelaborator

$\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**.Given a cost model we define a special type constructor

`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 **value**of type`A`

.Dually - we use the type

`cost A m`

to indicate that a term of this type **represents a value**of type A which**has taken**at most`m`

steps to evaluate.When a

**term**`M`

has the type `cost A m`

we say that M is a *costed term*, with a*cost*of m.When a

**function**`f`

has the type` A -> cost B m`

we say that `f`

is a *costed function*, with a*cost*of`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`

.The

`cost`

type constructor behaves as a an **indexed monad**, indexed over the additive monoid of the natural numbers, so whenever you compose (using Kleisli composition) 2 costed functions`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

`cost`

monad in *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***The validity of the cost of a term is not fully enforced by the compiler!**

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.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 costmonad. 2.That all the syntactic cost is accounted for.

Last modified 2yr ago