Derive Fintype for Pallas/Vesta computably

[daira]

https://zcash.github.io/ironwood/formal-verification.html says:

A structure with data fields cannot be inhabited by proof-irrelevant existence, and a plain def cannot conjure the data from mere existence via choice — the compiler enforces this, so noncomputable is not permitted for these definitions. One scoped exception: the arbitrary-domain adversary reduction (globalReachSet, splitFamilyRand) is noncomputable, solely because it materializes a Fintype instance for the Vesta curve group (Fintype.ofFinite); the witness data those endpoints produce still flows through the same computable relation kernels.

The exception can be removed. While a Fintype for a ~ $2^{254}$-sized field wouldn't be practically evaluable, it's structurally computable, since we can embed the curve points into Option (Fq × Fq) and Fintype (Option (Fq × Fq)) already exists computably.

(Maybe this can be done generally for all curves, or at least all ShortWeierstrass curves.)