More guidance on where to continue execution

Currently, we are not prioritizing any order on the frontier node exploration. But often, we can have branches that the user thinks are uninteresting or infeasible. So we could have a way for the user to say "keep exploring branch B1, but do not explore B2, B3, B4, because I will go and find a way to refute those branches".

Perhaps we could basically build a smaller proof obligation (an equality proof that reduces to false) that then the user has to discharge.

• Automated proof handling (sub-proof obligations). Proofs carry with them a list sub-proofs (can be added directly to Proof class, and we can add Proof.add_subproof(proof: Proof) -> None, which injects these subproofs. summary is modified to aso print out the status of subproof obligations. Pyk PR: https://github.com/runtimeverification/pyk/pull/394
• Generic functionality for refute-edge in APRProof class. APRProver.refute_edge method is added, which allows specifying a given edge as refuted and will:
  • Apply expanded to the target of the edge to prevert further exploration.
  • Do APRPRoof.add_subproof with the Equality proof specifying that the edge condition goes to false.
• Working test in either k-files/simple-proofs.k module or k-files/imp-simple-spec.k module. The key is a specification that leads to a branch, run the rpoof until teh branch is introduced, and then call the refute_edge routine on one of the branches, and assert that the resulting Equality proof that is generated looks correct.
• Test said functionality on KEVM proofs.

Start by reading APRProof and APRProver.refute_edge, then review the existing working test in k-files/simple-proofs.k or k-files/imp-simple-spec.k. Add a comparable test for KEVM proofs and verify that refuting a selected branch creates the expected Equality sub-proof and prevents further exploration.