Every element has an inverse | a+(-a) = 0 for all group elements.

Uncompression should only accept inputs of the expected length, so we check it on random inputs of the incorrect length. Inputs of the expected length are excluded by the incorrectSize predicate; however even if an input did have the expected length it would be very unlikely to deserialise to a point in the group because the cofactors are very big (7.6*10^37 for G1 and 3.1*10^152 for G2).

This tests the case we've omitted in the previous test, and should fail with very high probablity. It's quite difficult to test this with random inputs. We can improve our chances of getting a bytestring which encodes a point on the curve by setting the compression bit and clearing the infinity bit, but about 50% of the samples will still not be the x-coordinate of a point on the curve. We can also generate points with an x-coordinate that's bigger than the field size (especially for G2), which will give us a bad encoding. Maybe this just isn't a very good test.

Check that flipping the sign bit in a compressed nonzero point gives the inverse of the point.

Hashing into G1 or G2 should be collision-free. A failure here would suggest an implementation error somewhere. Here we test multiple messages but always use an empty Domain Separation Tag.

Test that we get no collisions if we keep the message constant but vary the DST. DSTs can be at most 255 bytes long in Plutus Core; there's a test elsewhere that we get a failure for longer DSTs. This test could fail (but not because of a hash collision) if we let it generate longer DSTs because the final list could contain multiple occurrences of CekError.