Skip to content

Commit ca29e6e

Browse files
Move result into requires-clause
1 parent 4e68a3d commit ca29e6e

File tree

1 file changed

+3
-3
lines changed
  • kevm-pyk/src/kevm_pyk/kproj/evm-semantics

1 file changed

+3
-3
lines changed

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

+3-3
Original file line numberDiff line numberDiff line change
@@ -1349,10 +1349,10 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
13491349
rule #computeValidJumpDestsWithinBound(PGM, I, RESULT) => .Set
13501350
13511351
1352-
syntax Bool ::= #isValidJumpDest ( Bytes, Int ) [function, total]
1352+
syntax Bool ::= #isValidJumpDest(Bytes, Int) [function, total]
13531353
1354-
rule #isValidJumpDest(PGM, I) => PGM [ I ] ==Int 91 requires 0 <=Int I andBool I <Int lengthBytes(PGM)
1355-
rule #isValidJumpDest(PGM, I) => false [owise]
1354+
rule #isValidJumpDest(PGM, I) => true requires PGM [ I ] ==Int 91
1355+
rule #isValidJumpDest(PGM, I) => false [owise]
13561356
13571357
rule
13581358
```

0 commit comments

Comments
 (0)