Ok, here's my updated understanding of the task itself.

We want to generate random input for each built-in function to ensure that no built-in function ever crashes with an exception. Crucially, at runtime we execute Untyped Plutus Core, which means we don't have types there and the user is allowed to submit an ill-typed program and it will get evaluated and if it happens to succeed, it will be accepted (@michaelpj, right?).

This means that our tests need to cover the ill-typed case just like the well-typed one. We need to make sure that both the cases are present in the generated tests. Which means we need to collect the stats on ill-typed vs well-typed applications (one of the functions from here does that, I always forget which one is for what).

Currently we only generate Constants, we need to generate arbitrary terms too. We don't care about them being sophisticated or well-typed or even well-scoped, so PlutusCore.Generators.AST.genTerm should do the job. A polymorphic built-in function like ifThenElse takes arbitrary terms as its second and third arguments and it'll succeed regardless of types and whether those arguments are constants or not. A monomorphic function will fail, but we want to test failing cases too, so that's fine.

Does this make sense to everyone?

Also, I was wrong about

genArg :: forall k (a :: k). (DefaultUni `Contains` a, PrettyConst a) => TypeRep a -> Gen a

as per the discussion above, but is it possible to make it

genArg :: (a :: *). MakeKnownIn DefaultUni Term a => TypeRep a -> Gen a

and recover the current interface by lifting the resulting a into Term via makeKnown and then rendering the resulting Term with pretty to recover the String part?

If that works out, we'll still need to have a generator of completely arbitrary Terms alongside the well-typed one from the above to test the failure case.

@zliu41 sorry, I thought that would be a good first task, but it turned out to be rather bad. Too vague, touches quite a lot of pieces of the machinery and requires figuring out what actually needs to be done. You're doing great, it's just that I didn't formulate the task properly, which is why you're rewriting different bits and pieces here.

the user is allowed to submit an ill-typed program and it will get evaluated and if it happens to succeed, it will be accepted

@zliu41 sorry, I thought that would be a good first task, but it turned out to be rather bad.

No worries, but it seems testing ill-typed programs can be a separate ticket, since this one only asks for testing that builtin functions don't throw? If so, this would still be a good first task 😃

a generator of completely arbitrary Terms alongside the well-typed one from the above to test the failure case.

That sounds good, so I think where we go from here is: (1) merge this PR after I address existing comments (2) add test cases for ill-typed programs, which will probably go like this:

• test builtin function evaluation with arbitrary terms
• if evaluating a builtin function throws an exception, the test succeeds. Otherwise, verify that the arguments are indeed well-typed.

What do you think?

genArg :: (a :: *). MakeKnownIn DefaultUni Term a => TypeRep a -> Gen a

I'm not sure about this one either, unless there's a way to write things like Just HRefl <- eqTypeRep (typeRepOfTyCon tr) @[] so that we can refine a to [something], which I'm not aware of.

if evaluating a builtin function throws an exception, the test succeeds

Actually I think I may be wrong on this - evaluating a builtin function never throws an exception, even if the arguments are ill-typed, right? Are you suggesting that the tests should verify that, or the tests should verify that the evaluation fails with an error upon getting ill-typed arguments? Either way I feel like it can be done in a separate PR, but if it's the former, then it does belong to this ticket rather than a separate one.

No worries, but it seems testing ill-typed programs can be a separate ticket, since this one only asks for testing that builtin functions don't throw?

Don't throw exceptions, which is orthogonal to well-typedness.

But yes, great point, testing ill-typed programs and ensuring we generate enough test cases of each kind does sound like it deserves a separate PR.

I'm not sure about this one either, unless there's a way to write things like Just HRefl <- eqTypeRep (typeRepOfTyCon tr) @[] so that we can refine a to [something], which I'm not aware of.

You know what, I won't let you keep all the fun for yourself, I'm gonna look at this particular piece and feel free to merge the current approach once ready.

if evaluating a builtin function throws an exception, the test succeeds

Actually I think I may be wrong on this - evaluating a builtin function never throws an exception, even if the arguments are ill-typed, right?

Yes. But we had a bug once where a builtin would throw an exception. That must never happen, hence this whole endeavor.

Are you suggesting that the tests should verify that

Yes.

or the tests should verify that the evaluation fails with an error upon getting ill-typed arguments?

No. That's not true anyway, you can have an ill-typed builtin application that succeeds, we have such tests.

Ok, I can certainly add some tests using arbitrary Terms, which should be easy given we have genTerm.

I feel like the generators for well-typed Terms are still useful (since if we test with arbitrary Terms, probably 99% of the test cases are ill-typed), so I'll keep them, but let me know if you think otherwise.

For well-typed Terms, if we want to generate non-Constants, it seems we need to write some new generators, which I think can be done in a separate PR.

Added tests using arbitrary (not necessarily well-typed) arguments. I think I addressed all review comments so far.

Three functions, VerifySignature, VerifyEcdsaSecp256k1Signature and VerifySchnorrSecp256k1Signature, are currently excluded. I need to figure out how to generate valid inputs for them.

@kwxm do you happen to know some of that? Also do the latter two have tests in the Plutus Tx compiler? We'll need to generate correct as well as incorrect input to make sure exceptions don't occur in both of these cases. It's fine to leave that for a future PR, though.

Each of the signature verification functions takes three bytestrings as arguments, and some of these have to be of specific sizes (you should get an error if they're the wrong size): see the comments in Crypto.hs. The functions take three arguments: a public key, a message, and a signature. They check that the signature's been obtained from the message using the private key corresponding to the public key, returning True if it has and False if it hasn't. For our purposes it shouldn't matter whether or not the signature is correct: the algorithms have to check every bit of the message in order to decide what the result is and there shouldn't be any difference in behaviour for correct and incorrect signatures. I think we can just generate random bytestrings of appropriate lengths and that should do the job (we won't need inputs where the signature really is valid, but we should check what happens when one or more of the inputs have the wrong length)

We already have some generators in the code that we use for generating the cost models for these functions: see here (although the generators need to be rationalised: there's a comment that says "FIXME: this is terrible), and here. We currently only have a benchmark for verifySignature, but Nikos will be adding the other signature functions in the near future.

I don't think there are any tests for these functions in the Plutus Tx compiler, but Koz Ross wrote some extremely comprehensive tests for the builtins in this file (which we should probably rename since it's not just about SECP256k1 any more). In fact that's probably a much better place to look for generators than the file I mentioned before. I think it even does show you how to generate correct signatures, so ignore what I said earlier about not needing to generate them: if we can, we probably should.

This means that our tests need to cover the ill-typed case just like the well-typed one. We need to make sure that both the cases are present in the generated tests.

Ziyang and I discussed this a bit. I think there are at least two bits of the builtin machinery that we might want to test:

• The generic handling of terms and converting them into typed values for builtins to consume.
• The implementation of the builtin functions themselves.

I think it's most useful for this check to focus on the second. That is, we're really trying to test that the dentotation functions are well-behaved here, which means we can assume we already have correctly-typed input.

Checking that the term -> typed constant machinery works properly seems like a separate issue, and one we could test perhaps more directly.

@michaelpj

The generic handling of terms and converting them into typed values for builtins to consume.
The implementation of the builtin functions themselves.

Checking that the term -> typed constant machinery works properly seems like a separate issue, and one we could test perhaps more directly.

With deferred unlifting both are indistinguishable parts of the runtime denotation of a builtin. One can extract a constant from a term implicitly via the ReadKnownIn instance or by manually calling asConstant in the denotation of the builtin and we'll get equal Core in the end. Trying to test the two indistinguishable ways of doing the same thing separately would only increase our chances of missing something.

To put it differently, even with immediate unlifting if the denotation of a builtin takes an Opaque, then it may call asConstant on it and you can't predict if that happens or not just by looking at the types, so this possibility needs to be accounted for and non-Constant terms need to be generated, at which point there's no point in testing asConstant separately, since this is handled by the tests here anyway.

I was too sloppy with that well-typed/ill-typed distinction. We don't care about an ifThenElse application being ill-typed: as long as the first argument is a boolean constant, the application succeeds and it doesn't matter whether the branches are of the same type. So the distinction should be between succeeding and failing applications and this is what should be tracked (in a subsequent PR as we've all agreed).

Does this all make sense?

Okay, I think I agree with that.

I was too sloppy with that well-typed/ill-typed distinction.

Well, ill-typed applications are one obvious class of failing applications!

Well, ill-typed applications are one obvious class of failing applications!

Not necessarily! An ill-typed application can run just fine, even in the typed world (i.e. the CK machine). Here's a PR with a test. So the well-typed vs ill-typed dichotomy seems completely orthogonal to what we're trying to achieve here.

Not necessarily! An ill-typed application can run just fine, even in the typed world (i.e. the CK machine).

Ugh, this is hard to talk about. We don't check anything for arguments that are type variables, but we do for those that aren't. I was trying to talk about applications-that-fail-because-of-unlifting-of-constants-to-particular-types, I don't know what to call that 😅

Yeah, ok, I think we're on the same page.

Did you test that it fails if we actually have a builtin that throws?

Yeah I manually verified it. Once we make the test polymorphic in fun we can add such a test case.

@effectfully I've switched to your approach in be2efd3, and now we are generating arbitrary Terms for Opaque arguments, in the "success" cases, which happens to be what we wanted.

I think you also suggested, in a separate PR, generating well-typed Terms for Opaque, rather than arbitrary ones (in other words, for IfThenElse we should generate Terms of the same type for both branches), right? This seems much trickier since we don't have an existing generators for Terms of a specific type. So just want to make sure it is worth doing.

I think you also suggested, in a separate PR, generating well-typed Terms for Opaque, rather than arbitrary ones (in other words, for IfThenElse we should generate Terms of the same type for both branches), right?

Not quite.

So I think that for SomeConstant we need to generate:

• constants of the right type. I.e. if it's a (a, b) there, we need to generate a tuple. And if a and/or b happen to be type variables (which is always the case with our builtins when a tuple appears inside of SomeConstant), then elements of the tuple need to be generated with random types (for example, a Bool and an Integer, a Text and a Text -- just two completely arbitrary constants, possibly but not necessarily of the same type)
• constants of the wrong type. I.e. if it's a (a, b) there, we should occasionally generate an arbitrary constant (most of which are going to be non-tuples) to test the unhappy path
• arbitrary terms (most of which are going to be non-constants) to test an even more unhappy path

Similarly for monomorphic builtins we want to generate constants of the right type (most often), constants of the wrong type (rarely) and non-constants (even more rarely).

And for Opaque I think we can just use the same generator that will be implemented for SomeConstant. At least I can't come up with a reason to differentiate them in any way. This does mean that we'll get very few well-typed applications of ifThenElse, but as I'm explaining to myself above we don't care about them being well-typed anyway, we only care whether evaluation succeeds or not.

Hope this is not too messy of an explanation of what I have in mind.

constants of the right type.

We already generate constants of the right type, but right now everything is instantiated to Integer, and that part does need to be updated to allow instantiation to arbitrary types.

constants of the wrong type. I.e. if it's a (a, b) there, we should occasionally generate an arbitrary constant

I feel like this is covered by testing with arbitrary Terms, since an arbitrary Term already has a 10% chance to be a constant. Any particular reason that we need to test this case more?

And for Opaque I think we can just use the same generator that will be implemented for SomeConstant.

Same question as above - since Opaque is supposed to accept any Term, there seems to be even less reason to generate constants-only test cases for Opaque.

I feel like this is covered by testing with arbitrary Terms, since an arbitrary Term already has a 10% chance to be a constant. Any particular reason that we need to test this case more?

Good point, not sure what I was thinking about.

since Opaque is supposed to accept any Term, there seems to be even less reason to generate constants-only test cases for Opaque.

It accepts any value, but a builtin is allowed to attempt to extract a constant out of it and then it can look at the type tag of that constant etc. I.e. from the point of view of these tests there doesn't seem to be any difference between SomeConstant and Opaque.

I do now realize we don't need to consider the case of constants of the wrong type separately, it'll be enough to just generate arbitrary terms and some of them will be constants making things ill-typed. Thanks for catching.

The comment on the test is good, but given how much discussion there has been here it might be worth expanding it into a longer Note? What do you think @zliu41 ? "Comprehensively generating arguments for builtin functions" or something