More efficient egraphs/dags in assembly equivalence checker

[JasonGross]

We should consider how to get better asymptotics on the equivalence checker, given that we now have invocations that take nearly an hour to run.

For example, in p448-mul-callgrind-with-source.7z.zip, we have

1.5M calls to merge_node taking 18% of the total time, about 40% of this time is spent in indexof and another 14% is spent in N.of_nat. We could presumably make this a lot more efficient by storing (a) an efficient map of N to nodes (based on FMapPositive), (b) the total number of nodes present (as an N), and (c) an trie mapping ops (more generally nodes) to indices in the dag. In light of #1193, we will probably also want to store a thunked assoc list mapping description strings to lists of dag indices. We may also need to associate with this data a proof that it all lines up; if we need to carry this around it should either live in dag_ok or it should be encoded as a boolean equality (or perhaps True -> check_good ... = true to avoid vm_compute and native_compute eagerly evaluating the proofs).

[JasonGross]

I would upload perf record data for p434, but perf.data is almost 9GB, and the output of perf script is 158 GB, and trying to make a flame graph OOMs (see brendangregg/FlameGraph#282).

[JasonGross]

Here's perf data for p224:
p224-mul.perf.data.zip
word_by_word_montgomery.zip
word_by_word_montgomery_sources.zip
flame graph: p224-mul-perf.svg.gz

[JasonGross]

And here's for p256:
p256-mul.perf.data.tar.gz

[JasonGross]

I tried doing this in #1342 / #1293 (comment) , but it made things slower. More performance profiling required