zxlive icon indicating copy to clipboard operation
zxlive copied to clipboard

Bug saving/loading proofs

Open wlcsm opened this issue 2 years ago • 3 comments

There is a bug where sometimes proofs are not saved or loaded correctly.

Example:

  1. Start with the default diagram and fuse the two circled spiders Screenshot 2023-11-28 at 9 10 23 pm

to get

Screenshot 2023-11-28 at 9 10 28 pm
  1. Save the proof and open it from the file again to get the following incorrect diagram Screenshot 2023-11-28 at 9 10 47 pm

wlcsm avatar Nov 28 '23 21:11 wlcsm

I think this issue is more general than proofs and applies to all graphs. Maybe an issue should be filed named something like "vertices are renumbered on save/open graph, leading to bugs", and this specific issue with incorrect proof saving/loading should be considered blocked by that.

As noted in https://github.com/Quantomatic/zxlive/pull/213#issuecomment-1859230170, the numbering of the nodes can change when a graph is saved and then re-opened.

The numbering of the nodes can matter, which means that the graph which is re-opened is functionally not the same graph as the one which was saved. For example, the "fuse spiders" rule currently fuses the selected vertices into the node with the lowest numbering. When the app is first opened, the nodes are numbered with 0, 1, 2, and 3 as the input nodes, 4, 5, 6, 7 in the second row, and so on. The first image in the first comment in this issue shows the fusion of vertices 14 and 18 by this ordering, which should fuse both into 14 (node on left), as shown here:

Screenshot from 2023-12-17 22-22-48

This differs from the image shown above, which has fused them into the node on the right. (Presumably, this output was generated after the initial demo graph had been saved, then re-opened.) Of course, since "only connectivity matters", these are really the same diagram. Still, it might be unexpected behaviour for a user to carry out an operation on a graph, and get visually different results based on how it was saved/opened.

Similarly, when I re-open the proof, this is what I get:

Screenshot from 2023-12-17 22-29-57

This is the wrong graph, but it is a different wrong graph than above! Clearly, there is a bug in applying the diffs for proofs, which might be because some piece of code assumes the numbering will be kept the same.

dlyongemallo avatar Dec 17 '23 21:12 dlyongemallo

I've isolated the source of the bug. It's this commit: PR #204.

If this commit is reverted, the proofs are saved and loaded correctly.

dlyongemallo avatar Dec 17 '23 21:12 dlyongemallo

Of course, since that commit is intended to fix something (an error produced by saving a phase spider with a parameter), reverting it will reintroduce that issue. So either to_json/from_json have to be changed to fix this issue, or the parametrised phase spider issue will have to be fixed in some other way.

dlyongemallo avatar Dec 17 '23 21:12 dlyongemallo