Security of BLS batch verification

As a note, many eth2 clients are using 64-bit scalars as suggested by @vbuterin here. I had a discussion with @asn a while back and more recently with Kev Aundray and they both mentioned the same 128 bit like you @alinush. My goal with this is to verify that value formally because we (Lodestar) and the Lighthouse team use Vitalik’s suggested 64-bit scalars. In Vitalik we all trust so sure that number is correct but thought it prudent to just revisit. Pinging @AgeManning and @dapplion for visibility.