Fix proofs: switch to `BigUint` instead of `Saturating<usize>` for proof cost

[bksaiki]

Per discussion with @oflatt, we should switch to BigUint to stop proofs from crashing anymore. This would make a tired Herbie developer happy ;)

[oflatt]

I approve this PR! Leaving so people can see. For context, we were previously using usize for proof costs. Unfortunately, this causes problems when things overflow. Our solution to this was to saturate the integers, but this is buggy for a subtle reason: it's unsound to give a path an arbitrarily large cost because later proofs may think they found something shorter, resulting in a cycle in the proof.

It would be good to confirm that performance isn't impacted too much. For herbie, this change strangely makes things faster on the hamming suite (smaller proofs?).

[bksaiki]

Across all of Herbie's benchmarks, the Racket profiler recorded 153.58s spent extracting proofs compared to 139.49s. Obviously overhead with Racket-side code and FFI calls, but hopefully this provides some data on performance.

[mwillsey]

@oflatt i don’t quite understand why saturation leads to a cycle. Can you elaborate?

[oflatt]

I tried to come up with an example- the problem is when we think a proof is smaller when it really isn't.

Take a look at this explainfind:

      d
      | INT_MAX
      c 
  1 /    \ 1
a.       b

The code uses a common ancestor trick to compute the cost between a and b: cost(a, b) = cost(a, d) + cost(b, d) - cost(c, d) But this can overflow, so cost(a, d) will become INT_MAX. In this way we arbitrarily inflate the costs of different paths.

Imagine we have a graph like this:

               congr(e, f)
a --- b ------------- c
  \                               / expensive
    --------------

   congr(a, c)
e --------- f
    \          / expensive
        g

Lets get a proof from a to c. A cycle happens if we pick edge (b, c) and edge (e, f). However, due to the overflow problem above different edges (the ones marked "expensive") can be arbitrarily incorrectly estimated. So we end up picking both congruence edges, since they have smaller proofs than the expensive edges.

Big integers solve this problem: the cost of an edge cannot be arbitrarily inflated, preventing proofs that contain themselves.