Rename verifySignature builtin

[gtrepta]

KPlutus is using the token verifySignature for the ED25519 signature verification builtin. But the Plutus core spec as of July 26th uses verifyEd25519Signature, and the latest Plutus core generates UPLC with this token. So this PR updates KPlutus to use the new name.

[SchmErik]

We need to make sure that the whole semantics complies with July 26th spec.

Some of the tests are actually generated. So I think we must also check that we are using the correct uplc executable, that is, one that conforms with July 26th or the version we decide to comply with.

@ChristianoBraga I'm not exactly sure what you want done to achieve this. Do you mean that you want the expected test results to be updated using a newer version of uplc that supports this keyword?

[ChristianoBraga]

Is it only a change in the name of this builtin that version of July 26th introduced or are there other changes?

Which version of uplc supports this change? I have the most updated version of Plutus and it’s uplc runs all our test with the current name of the builtin.

So if there exists an uplc that supports the new builtin, and perhaps other changes, do the tests from uplc-examples, extracted from uplc remain the same? Does this new uplc version parses and evaluates all other tests?

Em ter., 6 de set. de 2022 às 18:04, Erik Kaneda @.***> escreveu:

We need to make sure that the whole semantics complies with July 26th spec.

Some of the tests are actually generated. So I think we must also check that we are using the correct uplc executable, that is, one that conforms with July 26th or the version we decide to comply with.

@ChristianoBraga https://github.com/ChristianoBraga I'm not exactly sure what you want done to achieve this. Do you mean that you want the expected test results to be updated using a newer version of uplc that supports this keyword?

— Reply to this email directly, view it on GitHub https://github.com/runtimeverification/plutus-core-semantics/pull/309#issuecomment-1238646961, or unsubscribe https://github.com/notifications/unsubscribe-auth/AFNNCENYTIRX742YCAYFRBTV46WUFANCNFSM6AAAAAAQDUHGWQ . You are receiving this because you were mentioned.Message ID: @.*** com>

[ChristianoBraga]

Doesn’t it make sense? I may be overthinking this but I think we must make sure that the change is actually supported, no? Are there other changes?

Em ter., 6 de set. de 2022 às 20:01, Christiano Braga < @.***> escreveu:

Is it only a change in the name of this builtin that version of July 26th introduced or are there other changes?

Which version of uplc supports this change? I have the most updated version of Plutus and it’s uplc runs all our test with the current name of the builtin.

So if there exists an uplc that supports the new builtin, and perhaps other changes, do the tests from uplc-examples, extracted from uplc remain the same? Does this new uplc version parses and evaluates all other tests?

Em ter., 6 de set. de 2022 às 18:04, Erik Kaneda @.***> escreveu:

We need to make sure that the whole semantics complies with July 26th spec.

Some of the tests are actually generated. So I think we must also check that we are using the correct uplc executable, that is, one that conforms with July 26th or the version we decide to comply with.

@ChristianoBraga https://github.com/ChristianoBraga I'm not exactly sure what you want done to achieve this. Do you mean that you want the expected test results to be updated using a newer version of uplc that supports this keyword?

— Reply to this email directly, view it on GitHub https://github.com/runtimeverification/plutus-core-semantics/pull/309#issuecomment-1238646961, or unsubscribe https://github.com/notifications/unsubscribe-auth/AFNNCENYTIRX742YCAYFRBTV46WUFANCNFSM6AAAAAAQDUHGWQ . You are receiving this because you were mentioned.Message ID: @.*** com>

[gtrepta]

I'm using commit 3d7c3d0ce9bced4969eafc16446e40716003793b for Plutus, made on September 1st. The contracts it generates are using the verifyEd25519Signature token for the builtin, and its uplc evaluate command throws an error when it sees (builtin verifySignature):

uplc: ParseErrorB (ParseErrorBundle {bundleErrors = FancyError 6889010 (fromList [ErrorCustom Unknown built-in function 'verifySignature' at test:12378:1034 . Parsable functions are  [ addInteger
                                                                                         , appendByteString
                                                                                         , appendString
                                                                                         , bData
                                                                                         , blake2b_256
                                                                                         , chooseData
                                                                                         , chooseList
                                                                                         , chooseUnit
                                                                                         , ...

[SchmErik]

@gtrepta what happens when you run make update-results on top of your current changes? Does it change any expected outputs that used to use verifySignature?

[ChristianoBraga]

@gtrepta would it be possible for you to check if master implements the current spec in full and so does uplc such that we can claim to comply with it and freeze our implementation to that specification for M3? (As much as possible...)

[gtrepta]

@SchmErik No, nothing changes in regards to verifySignature. It does look like there are a few differences in how uplc is unparsing the terms though.

@ChristianoBraga Are you asking for some kind of equivalence check? I mean, the best we can do is discover and open issues for them and then merge pull requests like this one to fix them.

[ChristianoBraga]

I think it would be important for us to state that we comply with a given version of their specification. We managed to do it until the of M1 I think but then Kenneth started to produce updates without keeping old versions and I think we got lost on version tracking.

Maybe we could take this opportunity, of you identifying this builtin name change, and try to comply with some version of the spec. Most likely will not be the last one as Kenneth already posted an update on polymorphic builtins that I do not think we should try to comply with it, at least not now.

TL;DR: to which version can we state that KPlutus fully complies?

On Fri, Sep 9, 2022 at 3:04 PM gtrepta @.***> wrote:

@SchmErik https://github.com/SchmErik No, nothing changes in regards to verifySignature. It does look like there are a few differences in how uplc is unparsing the terms though.

@ChristianoBraga https://github.com/ChristianoBraga Are you asking for some kind of equivalence check? I mean, the best we can do is discover and open issues for them and then merge pull requests like this one to fix them.

— Reply to this email directly, view it on GitHub https://github.com/runtimeverification/plutus-core-semantics/pull/309#issuecomment-1242306127, or unsubscribe https://github.com/notifications/unsubscribe-auth/AFNNCEKDMQBVGAYLNNOC4M3V5N33JANCNFSM6AAAAAAQDUHGWQ . You are receiving this because you were mentioned.Message ID: @.*** com>

[PetarMax]

As for the pull request itself, this appears to be a simple find-replace, right?

[gtrepta]

As for the pull request itself, this appears to be a simple find-replace, right?

Correct.