Metatheory: add Value built-in type with postulated functions

[basetunnel]

Adds a postulated type Value and corresponding postulated built-in functions. Fixes fixes https://github.com/IntersectMBO/plutus-private/issues/1796.

I've also refactored the pattern matching of convertModel, while I was changing it to work for the new built-in functions. convertModel had a catch-all clause that broke the Agda CEK machine after a new RawModel constructor was added (which is used by one of the value built-ins). Such problems should from now on be caught by the coverage checker.

This also fixes https://github.com/IntersectMBO/plutus-private/issues/2283.

[ana-pantilie]

Mostly looks good, but I'm concerned about the budget changes and there's also one potentially problematic change I've pointed out in the review.

Could the budget changes be explained by the fact that they were marked as "failing" and they weren't checked by CI? I know we've made multiple changes to the cost model between first adding the tests and this PR. Or did something in this PR trigger the modifications?

[basetunnel]

but I'm concerned about the budget changes

Could the budget changes be explained by the fact that they were marked as "failing" and they weren't checked by CI? I know we've made multiple changes to the cost model between first adding the tests and this PR.

That's what I assumed too, I'll try to see if I can verify that.