Explicit range checks

Author: RaoulSchaffranek

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

@@ -1351,8 +1351,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
 
     syntax Bool ::= #isValidJumpDest(Bytes, Int) [function, total]
 
-    rule #isValidJumpDest(PGM, I) => true  requires PGM [ I ] ==Int 91
-    rule #isValidJumpDest(PGM, I) => false [owise]
+    rule #isValidJumpDest(PGM, I) => PGM [ I ] ==Int 91 requires 0 <=Int I andBool I <Int lengthBytes(PGM)
+    rule #isValidJumpDest(PGM, I) => false              [owise]
 
 ```