I have a situation where a change in the proof term produced by a tactic seems to make the verification of a `lia`

proof on uint63 objects explode the stack. I guess this is a standard problem and that either `lia`

or the proofs in `Uint63.v`

need care in general?? If so, does someone has an expertise on what kind of pitfalls to avoid?

Do you have an example?

`lia`

itself should not really care about tactic-produced terms. Perhaps the stack overflow is in `zify`

instead?

Do you have an example?

I was working on the proof term produced by `assert`

. If I apparently-innocently contract a letin there, then the compilation of `Uint63.v`

stackoverflows when checking Uint63.v. It seems to expand with depth 63 the body of a big fixpoint, or something like that.

Depending on which fixpoint you are talking about, you might be interested in https://github.com/coq/coq/issues/17626

Yes, looks similar. I'll try to find which fixpoint it is exactly.

I suspect it is `iter2_sqrt`

.

Hmm... That code is extremely confusing. The whole point of Newton's iteration is that you can get the result in 7 iterations, but here the number of iteration seems to be 2^63. I understand that it might make the proof simpler to make a few more useless iterations, but going from 7 to 2^63 seems overkill.

Last updated: Oct 13 2024 at 01:02 UTC