Update proof graph serialization to address #62

[petervdonovan]

This PR implements one of the proposed solutions under #62, "Modify argus-driver to return a graph (with cycles and multiple parents of the same node) instead of a tree, and only treat it as a tree for presentation purposes, within the JSX code."

The changes in this PR are already enough to make Argus more helpful for my personal use, but I'd like to see if we can upstream this so that other users can benefit.

#62 seems to be solved here -- for example, the code snippet listed there that previously caused a stack overflow now renders in such a way that the tree view can be manually expanded down to an arbitrary depth, which represents the infinite cyclic path through the proof obligations:

I'm opening this as a draft to solicit high-level feedback before I put in the work necessary to make this ready to merge. For example,

• Do we like this general approach? Is it compatible with the design philosophy behind Argus?
• Do we need to maintain Erotisi?
• The changes here, which replace a tree with a more general graph, mean that some concepts in the code don't really make sense anymore. For example, do we still need the depth-based weighting heuristics, or the concept of a "path to the root" (both of which are commented out in this PR)?

[gavinleroy]

Wow, thank you for all the work!

Do we like this general approach? Is it compatible with the design philosophy behind Argus?

I don't see any reason why this would be incompatible with the design philosophy of Argus because it seems the resulting UI would remain unchanged.

Do we need to maintain Erotisi?

No, there are several things that we tried in earlier versions that were kept around for evaluation, but they can be removed now. The Erotisi panel is one of them.

The changes here, which replace a tree with a more general graph, mean that some concepts in the code don't really make sense anymore. For example, do we still need the depth-based weighting heuristics, or the concept of a "path to the root" (both of which are commented out in this PR)?

Again we should just remove these things. The depth-based heuristics were used for evaluation but we can get rid of them now.

---

Overall, I think this is a great direction for Argus to go. I will take some time later today to read the PR in depth and see if there's anything I'd like to comment on. I believe the only thing that needs to "majorly change" is the bottom-view in the IDE, but I could have missed something as I skimmed this.

[petervdonovan]

OK, I think this is ready for review. I tried out the bottom-up view with the changes in this PR, and it seemed to work -- but of course it's still possible that something is subtly broken.

[gavinleroy]

Thank you for putting in the work to make our tool better, it is very appreciated!

I will review this over the weekend and test it on our corpus of example programs to double check that nothing has changed. So far it looks good!

[petervdonovan]

nix develop .#ci -vL --command ci-check passes locally now. My bad for not running it locally before.

[gavinleroy]

My bad for not running it locally before.

I usually don't expect others to use Nix locally, it just makes my life easier ;) Thanks for the contribution, I'll publish a new release soon and this change will go upstream.