Minor refactoring of Proof to reduce dependencies (for instance to MergeRule)

[unp1]

This commit factors out pruning, saving and reference resolving functionality to reduce the dependencies of Proof and to make it later easier to realise correct synchronization as well as saving proofs.

Not for this PR, but we should have a discussion about what our proof object should have as basic data structure. My idea:

• merge references and linked goals to once concept independent of merge rule or proof caching
• allow to register reference resolvers that can deal with references
• ask before saving (in the GUI) if references should be resolved
  • if yes, resolve and then pass the proof to the OutputStreamProofSaver
  • if not, the proof is passed to OutputStreamProofSaver which just saves the references (and does not resolve)
  • this allows to remove the line CopyReferenceResolver.copyCachedGoals(proof, null, null, null); from OutputStreamProofSaver. As the saver should not have specific knowledge and it should not change the proof object while saving

[codecov[bot]]

Codecov Report

Attention: 31 lines in your changes are missing coverage. Please review.

Comparison is base (0ab2555) 37.86% compared to head (879d3f7) 37.86%.

Files	Patch %	Lines
...c/main/java/de/uka/ilkd/key/proof/ProofPruner.java	76.81%	10 Missing and 6 partials :warning:
...lkd/key/proof/reference/CopyReferenceResolver.java	65.38%	6 Missing and 3 partials :warning:
...main/java/de/uka/ilkd/key/proof/io/ProofSaver.java	0.00%	6 Missing :warning:

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #3345 +/- ## ========================================= Coverage 37.86% 37.86% - Complexity 16904 16928 +24 ========================================= Files 2055 2057 +2 Lines 125528 125533 +5 Branches 21226 21224 -2 ========================================= + Hits 47525 47529 +4 - Misses 72152 72153 +1 Partials 5851 5851 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

[FliegendeWurst]

Not for this PR, but we should have a discussion about what our proof object should have as basic data structure. My idea:

• merge references and linked goals to once concept independent of merge rule or proof caching

• allow to register reference resolvers that can deal with references

• ask before saving (in the GUI) if references should be resolved

  • if yes, resolve and then pass the proof to the OutputStreamProofSaver
  • if not, the proof is passed to OutputStreamProofSaver which just saves the references (and does not resolve)

I can see how to resolve a cached proof reference (just copy the steps). But I don't really understand the difference between resolving and saving a linked goal yet. A linked goal is always "resolved" by the branch it is linked to, right?

[unp1]

Not for this PR, but we should have a discussion about what our proof object should have as basic data structure. My idea:

• merge references and linked goals to once concept independent of merge rule or proof caching
• allow to register reference resolvers that can deal with references

• ask before saving (in the GUI) if references should be resolved

  • if yes, resolve and then pass the proof to the OutputStreamProofSaver
  • if not, the proof is passed to OutputStreamProofSaver which just saves the references (and does not resolve)

I can see how to resolve a cached proof reference (just copy the steps). But I don't really understand the difference between resolving and saving a linked goal yet. A linked goal is always "resolved" by the branch it is linked to, right?

yes, the resolver would be the application of the merge rule (so the resolver would just be the identity and the correctness justification, the correctness proof of the merge rule). But we would have a common framework for both cases. So we would get rid of the special "linked" case.