Pyk RPC prover not interpreting K funcitonal claims as equality proofs

[ehildenb]

Currently, we are using kprove --dry-run --emit-json ... to read in specifications for the pyk RPC prover. This is good because we get access to the parser, but it also makes it so that we are not able to tell whether something is a functional claim or not. For functional claims, we want to build equality predicates instead, and simplify those to #Top. Currently, instead it discharges them like reachability queries (which is more similar to an implication check than a conditional equality check).

I'm not sure if this can be fixed without modifying the frontend. For example, we made need to add an argument to kprove --dry-run --emit-json ... that says: --no-infer-k-cell ..., which leaves a given proof alone if there is no K cell attached to it.

I need to inspect the generated JSON more to determine if the frontend is adding this inferred K cell or not.

[gtrepta]

Now that #3812 is merged, is there work here that needs to be done to integrate it?

[ehildenb]

• We need to change pyk's invocation of kprove for extracting claims to always use this option: https://github.com/runtimeverification/pyk/blob/eb583c8275258537e0f6bba1f46e2a2c2bbfa6c9/src/pyk/ktool/kprove.py#L332 (and thread that option through the various places needed in the KProve class linked there).
• We need to unrevert the reverts to KEVM which were done here: Update dependency: deps/pyk_release evm-semantics#2197. These changes originally removed the runLemma => doneLemma style proofs, thinking that it would turn on EqualityProof usage, but because K was inferring <k> cell automatically, it did not have that effect. So when this change was introduced to K, it started building EqualityProof instead (this logic here and here), and it turns out that those EqualityProof were not passing, because they are discharged differently than reachability proofs. So those need to be debugged.