APR-unsound behaviour when rule RHS definedness cannot be established

[PetarMax]

In discussion with @virgil-serbanuta, I have understood that when applying rules whose RHS contains partial functions, the behaviour of the backend should roughly amount to the following:

1. Branch on #Ceil(RHS)
2. In the branch with #Ceil(RHS), apply the rule and continue
3. In the branch with #Not (#Ceil (RHS)), do not apply the rule

which amounts to implicitly having #Ceil(RHS) as a requires. Normally, the #Not (#Ceil (RHS)) branch can be trivially discarded, and cases in which it cannot indicate a problem with how the semantics is defined.

Currently, the behaviour is:

1. Apply the rule
2. Branch on definedness

This leads to configurations in which both a term and the fact that this term is not defined are present, leading to legitimate branches being discarded as vacuous and therefore breaking all-path-reachability.

This was revealed by this PR (before commit a35b70e, in which pyk was made to check subsumption into the target nodes only in the case of terminal nodes if the target is terminal. This broke this test, which used this rule

    rule <k> ECREC => #end EVMC_SUCCESS ... </k>
         <callData> DATA </callData>
         <output> _ => #ecrec(#range(DATA, 0, 32), #range(DATA, 32, 32), #range(DATA, 64, 32), #range(DATA, 96, 32)) </output>

and treated the branch in which the above #ecrec was both present in the <output> cell and declared as not defined (via #Not (#Ceil ( ... ))).

[virgil-serbanuta]

FWIW, I think that a LHS => RHS rule should have #Ceil(RHS) in the requires clause (either added by the user, or added automatically by the frontend when compiling to kore). I don't think that the backend should behave as if the requires clause has #Ceil(RHS) without that being the case.

Alternately, it would make sense to split on #Ceil(RHS), then fail with a "Inconsistent semantics" error if the #Not (#Ceil (RHS)) branch is not #Bottom.

Sorry if I misunderstood things.

[PetarMax]

@virgil-serbanuta You haven't misunderstood, this is exactly the point. Thank you!

The only thing - I wouldn't fail immediately with an "Inconsistent semantics" error, perhaps a different rule can be applied in the #Not (#Ceil (...)) world, but if there isn't any, then I'd think it's time for that error, yes.

[jberthold]

Related discussion on slack: https://runtimeverification.slack.com/archives/CC360GUTG/p1691579037826229?thread_ts=1691576058.510699&cid=CC360GUTG