Documentation

A lazy tree of costs. Convenient for calculating the costs of values of built-in types, because they may have arbitrary branching (in particular a Data object can contain a list of Data objects inside of it).

CostRose gets collapsed to a lazy linear structure down the pipeline, so that we can stream the costs to the outside where, say, the CEK machine picks them up one by one and handles somehow (in particular, subtracts from the remaining budget).

Create a CostRose containing a single cost.

Collapse a CostRose to a lazy linear stream of costs. Retrieving the next element takes O(1) time in the worst case regardless of the recursion pattern of the given CostRose.

When invoking a built-in function, a value of type NumBytesCostedAsNumWords can be used transparently as a built-in Integer but with a different size measure: see Note [Integral types as Integer]. This is required by the integerToByteString builtin, which takes an argument w specifying the width (in bytes) of the output bytestring (zero-padded to the desired size). The memory consumed by the function is given by w, *not* the size of w. The NumBytesCostedAsNumWords type wraps an Int w in a newtype whose ExMemoryUsage is equal to the number of eight-byte words required to contain w bytes, allowing its costing function to work properly. We also use this for replicateByte. If this is used to wrap an argument in the denotation of a builtin then it *MUST* also be used to wrap the same argument in the relevant budgeting benchmark.

A wrapper for Integers whose "memory usage" for costing purposes is the absolute value of the Integer. This is used for costing built-in functions such as shiftByteString and rotateByteString, where the cost may depend on the actual value of the shift argument, not its size. If this is used to wrap an argument in the denotation of a builtin then it *MUST* also be used to wrap the same argument in the relevant budgeting benchmark.

Measure the size of a Value by its totalSize.

Measure the size of a Value by taking the max of (size of the outer map, size of the largest inner map).