Cost specification of integerToByteString does not match implementation

[nielstron]

Summary

https://github.com/IntersectMBO/plutus/blob/719fc18a562250e67b369acc3dcbd0dd33037bb5/plutus-core/plutus-core/src/PlutusCore/Evaluation/Machine/CostingFun/Core.hs#L643C1-L649C24

This implementation does not match the specs in https://github.com/IntersectMBO/plutus/blob/719fc18a562250e67b369acc3dcbd0dd33037bb5/doc/cost-model-overview/cost-model-overview.pdf table 2 for integerToByteString

Steps to reproduce the behavior

No response

Actual Result

No response

Expected Result

No response

Describe the approach you would take to fix this

No response

System info

No response

[nielstron]

Based on my estimation of memory cost this should incorrectly compute the costs for conformance test https://github.com/IntersectMBO/plutus/blob/719fc18a562250e67b369acc3dcbd0dd33037bb5/plutus-conformance/test-cases/uplc/evaluation/builtin/semantics/integerToByteString/big-endian/bounded/max-input-fits-max-width/max-input-fits-max-width.uplc.budget.expected

[nielstron]

Resolved, seems to be a non-issue

[nielstron]

After more extensive testing and investigating the aiken implementation it looks like instead of the literal value of y/x, the "cost interpretation of y/x" is used for integerToByteString and replicateByte. This cost interpretation of x is computed as ((x - 1) / 8) + 1 [1]. The fact that y (or x) are transformed in this way is not mentioned in the cost overview and should be added IMO.

[1] https://github.com/aiken-lang/aiken/blob/620fe6b2997537aab655fefaf27b43e5c8ed1916/crates/uplc/src/machine/cost_model.rs#L2634

[kwxm]

This cost interpretation of x is computed as ((x - 1) / 8) + 1 [1]. The fact that y (or x) are transformed in this way is not mentioned in the cost overview and should be added IMO.

It does mention at the top of page 2 that sizes are measured in 8-byte words (which is quite annoying: it'd be a lot simpler if everything was measured in bytes, but it's difficult to change that now) and sizes are mentioned again in Section 2.1 and in the second paragraph of Section 3. Maybe the word "size" is a bit too informal though. I'll think about how to clarify the explanation.

FYI the size measures of the built-in types are defined in this file although there's an added complication that sizes are represented as things called "CostRoses" which let us measure sizes of some of the more complicated types in an incremental way, which helps to save work when we need to calculate the size of complicated types like data. These are trees of numbers and the "real" size is the sum of all of the numbers.

[nielstron]

Thanks for the pointer to the actual calculations. This is quite helpful.

I agree that the description is quite informal, a formalization would be useful (since its also not unambiguous how many 8-byte words any data type requires, i.e. do signs of integers count? how exactly is data (recursively) measured? etc.). I also discovered that I previously costed the ExMem of a BLS ML result at 0 and none of the conformance tests captured this - an unrelated issue.

[kwxm]

a formalization would be useful

We defintely plan to do that at some point, probably by extending the Plutus Core specification to include all the costing-related stuff too. It may be a while before we can find the time to do that though. The current overview is a stopgap so that there's at least some documentation for the time being. Your comments are very useful though: some aspects of the document may not be very clear, so it's helpful to have some feedback that'll help us to improve it.