Remove the iterate SMT option

[strub]

Summary

The iterate option, when enabled, made EcSmt.select retry the SMT call several times, growing the relevance-selected lemma set on each attempt. Compile and llm modes hard-coded it to true at startup, which silently overrode user-specified bounds: a smt() call (max=0) would still ship dozens or hundreds of axioms after one or two retries, and proofs that should fail were closed by lemmas the user never asked for. Interactive mode left iteration off, so the same script behaved differently between batch and REPL.

This drops the option entirely — the parsetree field, the parser keyword, the CLI flag, the scope/checkmode/prover_infos plumbing, and the iteration branch in EcSmt.select. SMT now always runs a single attempt with the lemma set the user requested.

Closes #998.

Test plan

• CI passes on the standard suite
• Reproducer from the issue (smt() after axiom bad : false) is rejected in compile mode

[alleystoughton]

FWIW I had a single change to make in my developments (adding a -> intro pattern).

[fdupress]

Yes, most proofs are developed in interactive mode, so we shouldn't have to worry too much. The main source of chaos will be proof drift when they are checked only in batch mode, but updates to the environment (Why3, provers) take place: the old behaviour would just keep trying until smt went through, hiding the need for a fix.

I'll get started on SHA3 now. Would appreciate help on stdlib if anyone has time.

[fdupress]

In principle, I love it. In practice, I hate that it's happening right now.

I'll slog through SHA3.

[alleystoughton]

I started with the standard library. Not sure how much there is, but will report back.

[fdupress]

SHA3 should be going through. Typical fixes:

1. We need manual handling of pair destruction.
2. We need to manually introduce memory variables before SMT.
3. We need to |> before SMT.

Literally none of the breaks were missing lemmas.

(I am now timing out for the evening. Will try to look at the examples tomorrow, but anyone should feel free to take them on until then :))

[alleystoughton]

I believe there were only two theories failing in the library. I fixed them and pushed.

[alleystoughton]

Well, examples/MEE-CBC/CBC.eca checks for me both in batch and P-G, but is still failing in the CI. Any ideas?

[fdupress]

Try running in the docker container (ghcr.io/easycrypt/ec-build-box:main). You will need to build EC in the box and run the tests there, so slightly annoying. But that will ensure that prover selection resolves in the same way as it does in CI.

Or you could install all the provers that are installed in the docker container. But that's another kind of faff. I can look at it tomorrow.

[alleystoughton]

It was a prover version issue. The offending steps were working with my Z3 (4.15.4), but not CVC5 (1.3.3). I had to explicitly add commutativity. Now it's going through on CI.