Property tests for BLS12-381 multi-scalar multiplication

[kwxm]

Closes #7324.
Closes https://github.com/IntersectMBO/plutus-private/issues/1651.

[github-actions]

PR Preview Action v1.6.2
🚀 View preview at https://IntersectMBO.github.io/plutus/pr-preview/pr-7343/
Built to branch gh-pages at 2025-09-19 10:52 UTC. Preview will be ready when the GitHub Pages deployment is complete.

[effectfully]

I'm really not a fan of arbitrary @Integer for reasons specified in this Note:

{- Note [QuickCheck and integral types]
The 'Arbitrary' instances for 'Integer' and 'Int' only generate small integers:

    >>> :set -XTypeApplications
    >>> fmap (any ((> 30) . abs) . concat . concat . concat) . sample' $ arbitrary @[[[Integer]]]
    False
    >>> fmap (any ((> 30) . abs) . concat . concat . concat) . sample' $ arbitrary @[[[Int]]]
    False

We want to generate larger ones, including converted-to-Integer 'minBound' and 'maxBound' of various
integral types. Hence we declare 'nextInterestingBound' and 'highInterestingBound' to specify the
"interesting" ranges to generate positive integers within. We also make it likely to hit either end
of each of those ranges.
-}

Use arbitraryBuiltin @Integer?

[kwxm]

I'm really not a fan of arbitrary @Integer for reasons specified in this Note:

That's what I was trying to fix! In this case, we really want to choose an arbitrary integer in the range [0..p-1], where p is a 255-bit prime, and in fact we want bigger ones to make sure that the reduction modulo p is handled correctly, so most of the time the big generator a couple of lines below is used (which I hope generates numbers uniformly, although I haven't checked). I left the standard generator there so that we'd get things like -1,0,and 1 reasonably often.

[effectfully]

I left the standard generator there so that we'd get things like -1,0,and 1 reasonably often.

arbitraryBuliltin @Integer is better at that too, because it generates those regardless of the size parameter decently often.

This is arbitraryBuiltin @Integer:

         4.40% 0        
         1.74% -1
         1.60% 1

This is arbitrary @Integer:

         3.24% 0     
         2.42% -1
         2.23% 1

So quite similar, except the latter generates fewer 0, -1 and 1 as the size parameter grows while the former generates those at a consistent rate.

Let me know if you want to generate 0 slightly less often or -1/1 slightly more often.

But OK, here's another reason:

255-bit prime, and in fact we want bigger ones to make sure that the reduction modulo p is handled correctly

QuickCheck isn't written with that in mind, the shrinker for Integer at most divides by 2 and you're gonna wait a long time before shrinking for a failing property stops (or it gives up way too early, I don't remember). The arbitraryBuiltin shrinker doesn't have this issue:

-- | Same as 'shrinkIntegral' except includes the square root of the given number (or of its
-- negative if the number is negative, in which case the square root is negated too). We need the
-- former because 'shrinkIntegral' at most divides the number by two, which makes the number smaller
-- way too slow, hence we add square root to speed up the process.
--
-- >>> shrinkIntegralFast (0 :: Integer)
-- []
-- >>> shrinkIntegralFast (1 :: Integer)
-- [0]
-- >>> shrinkIntegralFast (9 :: Integer)
-- [0,3,5,7,8]
-- >>> shrinkIntegralFast (-10000 :: Integer)
-- [0,10000,-100,-5000,-7500,-8750,-9375,-9688,-9844,-9922,-9961,-9981,-9991,-9996,-9998,-9999]

[kwxm]

I used ArbitraryBuiltin for small integers, but I'm not too worried about shrinking the huge ones. These tests do pass and if a failure appears for some reason (like a bug in a library function) I don't think that having a not-very-good shrinker will stop us from working out what's wrong.

[effectfully]

And in other places.

[effectfully]

Nit: foldl' is more appropriate here.

[kwxm]

Hmmm. I did manage to use that in one of the earlier tests but then forgot to do it here: I think I got tripped up there because foldl is imported from the prelude.

[effectfully]

Nit: "Check" instead of "Cheack".

[kwxm]

I think I'll rework these a bit more before merging. The arbitraryConstant function generates a term that has a reasonable chance of being the zero element of the group, but a number of the tests use arbitrary for group elements not embedded in terms, and that doesn't make any attempt to hit zero.

[kwxm]

@effectfully I've reworked this so that the Arbitrary instances for group elements now deliberately produce the zero element 10% of the time (the previous version only did that for constant terms containing group elements). Once I did that a couple of tests that check the serialisation format started failing because zero is encoded specially and the old generator was never producing it (if it had we would essentially have a has collision). We should probably move these generators somewhere else and use them in the ArbitraryBuiltin instances too.