Consolidate single-proof and multi-proof parallelism

Currently, there is a parallel_advance_proof function in pyk for taking advantage of multiple cores when using a single proof, and kontrol and kevm each use their own version of parallelism for groups of proofs. We should expand parallel_advance_proof so that instead of just one proof, it handles a dynamic set of proofs possibly in subproof relations with each other, and submits their steps to the same ThreadPool within the same loop. This should take into account subproof status, e.g., if a proof has a pending subproof, it could be considered to not have any available steps. To accommodate the CSE use case in kontrol, stepping a proof should have the possibility to generate a new subproof which is added to the overall set of proofs, and when a proof is passed, it should be made available to its parent as a rule through add-module.

Also, the current Prover and parallel_advance_proof implementations are type-parameterized to a specific type of proof, but if we have a multi-proof prover that works in the same way, it would be ideal to be able to handle both APR and Equality proofs.

The current parallel-compatible implementation of APRProver is built around the assumption that a single server is used. It is possible that could cause this proposed system to be slower than the systems in place in kontrol and KEVM, which use a separate server per proof, because a single KoreServer has some times when its threads will share access to LLVM backend hooked functions (https://github.com/runtimeverification/hs-backend-booster/pull/493). It would be nice if we could simply use a different create_prover function that also starts a new server, but then you run into the issue of having to somehow keep the module-related state in sync between the different servers.

Building the subproof graph out of claim dependencies is a behavior currently in KEVM but which is also desired in pyk. (#4290) This should be upstreamed into pyk but should be separate from the multi-proof parallel step-based prover mentioned above, and the claim dependency graph can be represented as a subproof graph prior to passing this graph to the parallel prove function.