Cut on circularity rule application, better error message

[ehildenb]

Related: https://github.com/runtimeverification/k/issues/4359 Related: https://github.com/runtimeverification/haskell-backend/issues/3912

This PR is to support passing the final tests on the RPC prover in KEVM. In particular:

• A bug we've been hitting in Haskell backend gets a better error message, to hopefully be more informative off the bat.
• A duplicate log message in KCFGExplore.section_edge is removed.
• When doing KCFGExlore.section_edge, we were previously just dropping the rule labels of the applied rules on the new edges. Now we save them and store them appropriately on the KCFG.
• When computing the rule labels to store in the KCFG, if the unique-id is not present in teh definition, we still use the supplied unique id because the HB now returns the rule label instead if it's present (https://github.com/runtimeverification/haskell-backend/pull/3916). We just report the location of the rule as UNKNOWN.
• The logic for how we apply circularity rules is refined a bit:
  • When discharging a circularity proof obligation, we always consider the circularity rule itself to be a cut-point rule. That's because we need the state immediately following the application of the circularity rule to compare it to subsumption into the initial target state.
  • When discharging a circularity proof obligation, if we have not made any progress yet on the proof, we first take an execution step of depth 1 before resuming normal execute depth. This is because we cannot inject the circularity rule for consideration until we've made some progress, but want to enable it for consideration as early as possible.
  • A test of IMP that before had to manually massage the cut-point-rules list does not have to do that anymore, and is passing directly.

[PetarMax]

When doing KCFGExlore.section_edge, we were previously just dropping the rule labels of the applied rules on the new edges. Now we save them and store them appropriately on the KCFG.

This is a bug fix then, great.

When discharging a circularity proof obligation, we always consider the circularity rule itself to be a cut-point rule. That's because we need the state immediately following the application of the circularity rule to compare it to subsumption into the initial target state.

This is also essential and it's excellent that it's automatic now.

When discharging a circularity proof obligation, if we have not made any progress yet on the proof, we first take an execution step of depth 1 before resuming normal execute depth. This is because we cannot inject the circularity rule for consideration until we've made some progress, but want to enable it for consideration as early as possible.

Is it reasonable to expect the application of a circularity while executing the first request from the initial node, without any branching first? I think that's what this additional step effectively enables. What would such a circularity mean?

[ehildenb]

@PetarMax in case of a circularity, it will first do one step of execution (to make progress), which will mean it's no longer at the loop head in teh LHS of the rule. The next time it comes to the loop head, the rule will be available as a circularity, so instead of branching (into the loop and out of the loop), it will immediately attempt to take the circularity rule to the conclusion (the RHS). It still needs to check that the reached state is subsumed into the original RHS of the claim at that point.

[PetarMax]

Looks good to me.