Cleanups to specifications to enable modularity, re-provability

[ehildenb]

Soft Blocked on: runtimeverification/k#4402 (will pass CI without this, but functionality will remain broken, same as on current master)
Blocked on: runtimeverification/k#4411
Blocked on: #2465

These changes are to work towards modularizing the MCD proof suite. Currently, when run with the RPC server, we're running each proof independently instead of re-using subfunctions (eg. using Vat.adduu for Vat.frob). This moves us in that direction.

• Currently, if a proof is already saved and passing on disc, we still load a KoreServer, which takes several seconds. Now, we skip loading the KoreServer in this case, just reporting it back as already passing (much faster re-runs).
• When we are viewing or showing a proof, or pruneing and edge or sectioning an edge, we currently were loading a proof and all it's dependencies. This causes crashes. Now, instead we used Minor cleanups to prover, kast k#4402 to make sure we only load the main proof.
• The return of KCFGExplore.section_edge is fixed. It used to return the new KCFG, but now it just updates it in place. The type-checker didn't catch this because of how the value was unused.
• We remove the mention of the <exit-code> cell from the mcd and benchmarks proof-suites, as it's never relevant to proofs and is more configuration than is needed. Also some minor formatting issues.
• Turns on using the booster by default for kevm prove ... invocations.
• Does not repeat the --use-booster option for kevm section-edge ..., instead just relies on the existing RPCOptions that have been imported.
• Removes the manual insertion of a KSequence on the <k> cell for proofs, which is no longer needed.

TODO: update required status checks since --use-booster got switched to --no-use-booster.