Remove trace-based slicing implementation

[rolyp]

Once the ESOP 2025 artifact is submitted we can commit to the graph-based implementation and remove Trace, Eval, EvalBwd, etc.

See also:

• ESOP 2025 web artifact #1130

[rolyp]

@JosephBond Given this task, it might not make sense to spend time diagnosing that graph vs. trace discrepancy for #1197. Perhaps a better strategy is to turn our v0.7.3 tag (the version we submitted to ESOP) into a branch (branches are similar to tags but support revisions and can be “protected” using rules) and then push ahead with removing traces as a precursor to finishing #1197. We can then use v0.7.3 (perhaps renamed to v0.7.3-esop2025-artifact) to do the ESOP artifact work.

[JosephBond]

@rolyp whilst I would agree, the issue I raised in the slack channel remains, since the issue is not just that the trace and graph semantics don't agree, it's that G-Suffices selects nothing in the output, which implies an unknown bug somewhere in the graph semantics, not in the trace semantics. I think we may need to spend some time on it independently of the ESOP artifact

[rolyp]

Ah ok, I read your comment as suggesting that the test failure was due to the selection information being different. But if the graph semantics also somehow calculates the wrong value then yes that’s not something we can avoid having to fix.

[JosephBond]

For further clarification: the graph semantics seems to compute the correct output value, it just computes the wrong selection information on that output value when running G-Suffices. I don't know that it's relevant to the ESOP artifact but it is something that needs to be fixed

[rolyp]

Ok to summarise our understanding so far, one likely problem with the idea of removing the trace-based implementation as a precursor task is that we will need to migrate the round-tripping test to the graph implementation, which will then fail (on our current understanding of the problem).

An alternative suggestion then is to demote the qcut test to a regular test rather than a bwd test. That will still test the round-tripping property, but using an empty δv, which always round-trips successfully. Any problem with graph slicing that remains is orthogonal to #1197, so we needn’t get side-tracked by it.