perf(test): remove redundant integration test executions

[Stevengre]

Summary

• Skip LLVM backend test_exec_smir tests in CI — keep Haskell only, since it's the backend used for proving and bugs there have higher impact
• Skip test_prove_termination in CI — the same 19 programs are already executed via test_exec_smir[*-haskell]

This is done via a pytest -k filter in the CI workflow only — no test code is modified, so all tests remain available for local development.

Deselected: 58 of 247 tests (39 LLVM exec_smir + 19 prove_termination)

Risk Analysis

• LLVM backend regression will be missed in the previous test, which should be handled by future test framework refactoring. But if we don't add new exec_smir test or add new exec_smir test with llvm to update expected files, the result is the same as we run CI before.
• test_prove_termination just uses prove-rs to validate the termination, which is the same as the comparison with the current expected files. I believe that there is no risk to remove them in this way.

Expected CI time reduction

~2h37m → ~1h20m (based on this run)

Test plan

• Integration tests pass with the -k filter applied
• Verify CI time improvement

Resolves #971 (Phase 1)

[mariaKt]

LLVM backend regression will be missed in the previous test, which should be handled by future test framework refactoring. But if we don't add new exec_smir test or add new exec_smir test with llvm to update expected files, the result is the same as we run CI before.

I am not sure I understand what you mean here, could you clarify?

[Stevengre]

LLVM backend regression will be missed in the previous test, which should be handled by future test framework refactoring.

I thin exec_smir test is just for mir-semantics availability of llvm backend. If we assume the backends are correct, what we need to do is just leaving some quick tests for llvm backend to make sure our semantics can run on it. That's what I mean about refactoring. But just a thought for now.

But if we don't add new exec_smir test or add new exec_smir test with llvm to update expected files, the result is the same as we run CI before.

Existing tests have been validated by both backends. If we assume that the backends are correct, the semantics may only cause problem because new rules will introduce nd. This case, haskell backend will produce different expected file and will show errors in CI.

@mariaKt I don't this description is enough. Please let me know if you have more questions.

[dkcumming]

If we assume the backends are correct

Is it true that we can assume the backends are correct? I thought the main way that we were finding regressions in the backends was from the test suites of the semantics using them. I thought the main way @jberthold was finding out about problems in the haskell backend was from the KEVM test suite, and I feel that when Pi Squared changed the LLVM backend in the past we noticed it in our semantics tests. @ehildenb @palinatolmach what do you think? I am interested in the speed up, but is this the right way to go? It feels to me the solution we would really like is to have #853 implemented - but I don't know how likely that is