Recent nightly runs out of memory on proof that used to work

[nano-o]

The following proof in BLST works with the 3-11 nightly but runs out of memory with the 3-19 and 3-24 nightly releases.
https://github.com/GaloisInc/BLST-Verification/blob/d1ade9ac62e7e8bfa40cacbdaa37444f76ee3863/proof/hash_to_g1.saw#L219

[robdockins]

Is the 3-11 nightly verified to be the last one that works, or is it just one that you happen to know works?

[nano-o]

It's the last one that works.
Btw, to try it, it's best to uncomment all the commented-out statements at the beginning of hash_to_g1.saw and run SAW on this file.

[nano-o]

I mean it's the last among those listed here: https://saw.galois.com/builds/nightly/ (there isn't one nitghtly per day there)

[robdockins]

OK, I'll try to do some bisecting, see if we can figure out what's going on.

[robdockins]

Bisecting indicates this is the first commit where the problem occurs: c95fa20

It's possible some of the rewrites removed by that commit were important for this particular proof, although I thought they all involved the now-removed eq primitive.

[robdockins]

Turns out, the rewriting step that was removed in that patch included both the basic_ss as well as the rewrites related to eq. The particular proof step at issue here is easily solved if we add a simplify basic_ss proof step before dispatching to the solver; some combination of rewrites in there reduces some of these proof obligations to True and makes the proof run about the same as before.

It might be interesting to know why the proof task gives the What4 solver backend such problems without this rewrite, but for now the simple fix is to add another rewrite step, or maybe to incorporate the basic_ss into the fp_simpset that is already being used in that proof.

[nano-o]

Okay, thanks for investigating!

[weaversa]

@robdockins Just tagging that this may be related to #1166 .