# 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. ![](/files/-MQvV5jIfEOPaOpNjEKN) 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 is **declared** by the > > **developer** and **verified** by the **type system** > 2. **Syntactic Cost** - which is **computed** by the **elaborator** $$\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 `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`. ## Compositional Cost 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. ## 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. ![](/files/-MQvY0PfbHLMe4g82b8r) ![](/files/-MQvXlVo832J1PMc0N2t) ![](/files/-MQvXuiC3Du6eUGV5OMx) --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://docs.zenprotocol.com/contract-cost.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.