Allow splitting on "happy path" of common rules

In discussion with @tothtamas28 we realized that

a) overflows and underflows are rare issues in practice that you might want to investigate separately from the happy path,
b) in theory overflows and underflows can happen in a myriad of places in EVM code, and
c) modulo make SMT solving a lot harder.

We had the idea that it would be great -- at least for our project -- to always split on chop operations, where we would get one path where there are no chop present in the constraints.

A way to do this would be to modify the chop rule

rule chop ( I:Int ) => I               requires          0 <=Int I andBool I <Int pow256 
 [concrete, smt-lemma]
rule chop ( I:Int ) => I modInt pow256 requires notBool (0 <=Int I andBool I <Int pow256) [concrete, smt-lemma]

Or something similar (we could also use priority on the rule which strips the modulo. This would then be handled separately by a Markdown code selector tag to not interfere with the ordinary semantics.

The same approach can be taken with other problematic rules. While simplifications and lemmas can often help, an approach like this could let us more aggressively find and explore happy paths and gather all the constraints on them. Ideally this type of splitting behavior would be hidden behind a flag or configuration choice.

Start with the chop rule in kevm-pyk/kproj/evm-semantics/word.md at the linked location and review how the proposed rule split interacts with the existing semantics. Then trace how a Markdown code selector tag or configuration flag could isolate happy-path splitting without affecting ordinary semantics; done means the behavior is configurable and separates paths without changing the default behavior.