Sunset `kore-exec`, remove its uses in `kprove`

[geo2a]

The transition to the RPC-based provers, that are based on the kore-rpc and kore-rpc-booster is complete. The old monolithic prover, kore-exec, is only used for regression/integration testing at as point, and I'd argue that there are no production uses of it. We would like to sunset kore-exec and make the RPC servers the only entry-points to the Haskell backend.

The kprove executable uses the Haskell's backend kore-exec to prove K specifications. However, kprove is also used for converting specification to JSON with --emit-json-spec. The second use-case is required, but I'd argue that the first is not.

The main challenge is of course the integration test suites:

• for kore-exec in haskell-backend and,
• for kprove in k. These will need to be adapted for use with the RPC server.

I'd like to start the discussion!

[ehildenb]

KEVM is still testing for tests that aren't passing using the RPC server:

• https://github.com/runtimeverification/evm-semantics/blob/ddef90a245c8f911c0aad2d37530f42595e28570/.github/workflows/test-pr.yml#L119
• https://github.com/runtimeverification/evm-semantics/blob/ddef90a245c8f911c0aad2d37530f42595e28570/kevm-pyk/src/tests/integration/test_prove.py#L326

There are many tests that have not been ported, many of them are because we're missing circularity or depends(...) attributes on the claims (the old prover assumed all rules were circularities and dependencies, the new one is explicit). But there are some deeper failures too.

[Baltoli]

The pain of maintaining kore-exec at this point is possibly not quite enough to go through the process of fixing the failing tests in KEVM, but we might want to come back to fix this in the future.

[Baltoli]

The KEVM tests are very nearly ready for this to happen; we need to do similarly for the integration test suite and tutorial code.

[Baltoli]

Specifically, the regression-new test suite in Pyk

[Baltoli]

4194

[Baltoli]

Query: how best to get a single failing node out of the prover tests at the point they get stuck? The translation we need is from:

< APRProof: A1-SPEC.s1
<     status: ProofStatus.FAILED
<     admitted: False
<     nodes: 4
<     pending: 0
<     failing: 1
<     vacuous: 0
<     stuck: 1
<     terminal: 0
<     refuted: 0
<     bounded: 0
<     execution time: 0s
< Subproofs: 0
< 1 Failure nodes. (0 pending and 1 failing)
<
< Failing nodes:
<
<   Node id: 3
<   Failure reason:
<     Matching failed.
<     The following cells failed matching individually (antecedent #Implies consequent):
<     K_CELL: end ( barConcrete ( X:Int ) ) #Implies end ( baz ( X:Int ) )
<   Path condition:
<     #Top
<   Failed to generate a model.
<
< Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN
---
> kore-exec: [] Warning (WarnStuckClaimState):
>     The configuration's term unifies with the destination's term, but the implication check between the conditions has failed. Location: a1-spec.k:7:1-8:18
> Context:
>     (InfoReachability) while checking the implication
>   #Ceil ( barConcrete ( X ) )
> #And
>   #Not ( #Ceil ( baz ( X ) )
>   #And
>     {
>       barConcrete ( X )
>     #Equals
>       baz ( X )
>     } )
> #And
>   <k>
>     end ( barConcrete ( X ) ) ~> .K
>   </k>
> #And
>   {
>     true
>   #Equals
>     X >Int 0
>   }
> [Error] Prover: backend terminated because the configuration cannot be rewritten further. See output for more details.
make: *** [a1-spec.k] Error 1