Contract Cost
Last updated
Last updated
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 for the cost of the term M.
In practice the actual cost (relative to the cost model) is not computed directly, instead - the cost is decomposed into 2 components:
Compositional Cost - which is declared by the
developer and verified by the type system
Syntactic Cost - which is computed by the elaborator
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:
That the term returns an output which is wrapped in the cost
monad.
That all the syntactic cost is accounted for.
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 ( is equivalent to ), 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).
