-
Notifications
You must be signed in to change notification settings - Fork 479
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
SCP-2417: Add builtin function: serialiseData #4447
Conversation
6f9a294
to
798ab1b
Compare
I have added agda support for serialiseData. It was nice to see the NEAT tests picking up discrepencies between the different evaluators as I added the semantics. However I haven't added the Haskell semantics of serialiseData and the tests still pass (I think, waiting for CI). |
I tried cranking the NEAT tests up a notch to generate more terms but the term level tests hadn't terminated after 20 minutes :( |
Do these semantics have to be added? Aren't all these builtin functions kind of "abstract" from Agda's point of view? |
da98594
to
3a2fe92
Compare
@@ -969,6 +972,10 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where | |||
makeBuiltinMeaning | |||
((==) @Data) | |||
(runCostingFunTwoArguments . paramEqualsData) | |||
toBuiltinMeaning SerialiseData = | |||
makeBuiltinMeaning | |||
(BS.toStrict . serialise @Data) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@michaelpj we could have a KnownTypeIn
instance for lazy bytestrings. Probably not worth it though.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Indeed it is not worth it, because the most likely thing to do after calling serialiseData
is to hash the result, e.g. sha3_256(serialiseData(I(3)))
. All our hash builtins (coming from cardano-crypto-class) go through strict bytestrings, since as @kwxm pointed out, they are foreign-imported from C.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, this seems fine.
3a2fe92
to
2220b1e
Compare
Yes, that's right. In Agda we just postulate the existence of them. But, when the agda model is compiled to haskell the postulated builtins are compiled to the real haskell implementations. The fact the tests work without the supplying the implementation means the tests are not actually exercising this code. I think they may be getting applied but as the results are not used the ghc runtime never actually computes them. |
dd8e893
to
e69d00b
Compare
import Data.Foldable (fold, for_) | ||
import Data.Map qualified as Map | ||
import Data.Set qualified as Set | ||
import Plutus.ApiCommon | ||
import Test.Tasty | ||
import Test.Tasty.HUnit | ||
|
||
serialiseDataEx :: CompiledCode Builtins.BuiltinByteString |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't know what's going on with the nix stuff, but this package tries to avoid relying on the plugin. We do that for the other test cases by manually constructing PLC programs, look in Examples.hs
. We could do that here, and then at least we don't have to figure out why things are broken...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I did what u said, let's hope that this fixes nix 🤞
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
yay! LGTM?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
btw, I am going to do a separate PR for the plutus-spec v3 to add serialiseData
e69d00b
to
586b880
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, modulo the costing stuff.
@@ -969,6 +972,10 @@ instance uni ~ DefaultUni => ToBuiltinMeaning uni DefaultFun where | |||
makeBuiltinMeaning | |||
((==) @Data) | |||
(runCostingFunTwoArguments . paramEqualsData) | |||
toBuiltinMeaning SerialiseData = | |||
makeBuiltinMeaning | |||
(BS.toStrict . serialise @Data) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yeah, this seems fine.
586b880
to
98215e8
Compare
@kwxm Hydra could be a real-world example for this and our use case is serializing one or more On the data you show, the cost of all the constructed value looks linear, but with different linear factors? Do you have an idea how the upper values look like, i.e. what makes them more expensive / the costed |
@ch1bo I'm just looking into that. See also #3619. I suspect that the reason that we see a number of separate straight lines is that our generator for |
@ch1bo Take a look at the comments on #4480. I'm off next week, but I'll try to look at the cost of serialising TxOuts when I get back. |
This adds the necessary boilerplate for a new builtin "serialiseData" as described in CIP-0036.
More specifically:
Pre-submit checklist: