Fix memory usage in metatheory

[kwxm]

Recall that every builtin type has a size measure that tells you how big a value is, and we base the cost of calling the builtin on the sizes of its arguments. Usually the size measure is (an approximation to) the amount of memory the value takes up, so for an integer the size is the number of 64-bit words required to hold it, which is proportional to the logarithm or the number of digits (so any integer up to size 2^63-1 has size 1).

However, alternative size measures have had to be added for some of the new bitwise builtins. For example, there's a replicateByte function that takes a byte b and an integer n and produces an n-byte bytestring full of copies of b. The CPU and memory usage of this function depend on the actual value of n, not its size. To deal with this sort of thing we've introduced newtype wrappers with non-standard size measures: we use these in the denotations of the builtins to change the memory usage like this but these types are transparent to the builtin machinery so they just look like the normal types in UPLC). However, the Agda code doesn't currently know about these: all that it knows at the moment is that replicateByte takes two integers, and it measures the size of these in the standard way and ends up calculating the cost wrongly (and similarly for some of the other functions). We should fix this. One way would be to introduce new types into the Agda code with specialised size measures, but this might require siginficant additions and some builtins would have to have Agda signatures which differ from their UPLC ones because they'd need to contain the new types.

More specifically, the Agda signatures of the builtins are defined just below here and the size measures are defined here. The problem is that in the Haskell code it's possible to transparently wrap the parameter types in newtype constructors to change the memory usage measure (see here for example), but we currently have no way to do this in Agda. Consider the example of replicateBytes, where the first argument has to be costed as a literal number of bytes rather than by its size an integer. Presumably we could introduce a new type like integerCostedAsNumWords and replace the integer in the Agda signature with that and add a new defaultConstantMeasure for it; however, we'd then have an extra type floating around which would have to be treated as being identical to integer in most contexts (and we'd need several similar types). Maybe it'd be possible to attach some kind of index or attribute to the integer type in order to specify how it should be costed, but working out the best way to do this would require some Agda expertise.