Skip to content

Commit abb872f

Browse files
committed
kevm-pyk/evm: fix issue with rule strcuture
1 parent f830589 commit abb872f

1 file changed

Lines changed: 10 additions & 10 deletions

File tree

  • kevm-pyk/src/kevm_pyk/kproj/evm-semantics

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

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -380,19 +380,19 @@ The `#next [_]` operator initiates execution by:
380380
syntax Bool ::= #stackUnderflow ( WordStack , OpCode ) [symbol(#stackUnderflow), macro]
381381
| #stackOverflow ( WordStack , OpCode ) [symbol(#stackOverflow), macro]
382382
// --------------------------------------------------------------------------------------
383-
rule #stackUnderflow( _WS , _POP:PushOp ) => false
384-
rule #stackUnderflow( _WS , _IOP:InvalidOp ) => false
385-
rule #stackUnderflow( _WS , _NOP:NullStackOp ) => false
386-
rule #stackUnderflow( _W0 : _WS , _UOP:UnStackOp ) => false
387-
rule #stackUnderflow( _W0 : _W1 : _WS , BOP:BinStackOp ) => false requires notBool isLogOp(BOP)
388-
rule #stackUnderflow( _W0 : _W1 : _W2 : _WS , _TOP:TernStackOp ) => false
389-
rule #stackUnderflow( _W0 : _W1 : _W2 : _W3 : _WS , _QOP:QuadStackOp ) => false
390-
rule #stackUnderflow( _W0 : _W1 : _W2 : _W3 : _W4 : _W5 : _W6 : _WS , _CSOP:CallSixOp ) => false
383+
rule #stackUnderflow( _WS , _POP:PushOp ) => false
384+
rule #stackUnderflow( _WS , _IOP:InvalidOp ) => false
385+
rule #stackUnderflow( _WS , _NOP:NullStackOp ) => false
386+
rule #stackUnderflow( _W0 : _WS , _UOP:UnStackOp ) => false
387+
rule #stackUnderflow( _W0 : _W1 : _WS , BOP:BinStackOp ) => false requires notBool isLogOp(BOP)
388+
rule #stackUnderflow( _W0 : _W1 : _W2 : _WS , _TOP:TernStackOp ) => false
389+
rule #stackUnderflow( _W0 : _W1 : _W2 : _W3 : _WS , _QOP:QuadStackOp ) => false
390+
rule #stackUnderflow( _W0 : _W1 : _W2 : _W3 : _W4 : _W5 : _W6 : _WS , _CSOP:CallSixOp ) => false
391391
rule #stackUnderflow( _W0 : _W1 : _W2 : _W3 : _W4 : _W5 : _W6 : _W7 : _WS , COP:CallOp ) => false requires notBool isCallSixOp(COP)
392392
rule #stackUnderflow(WS, _POP:OpCode) => #sizeWordStack(WS) <Int #stackNeeded(OP) [owise]
393393
394-
rule #stackOverflow(_WS, OP) => false requires #stackDelta(OP) <=Int 0
395-
rule #stackOverflow(WS, OP) => 1024 <Int #sizeWordStack(WS) +Int #stackDelta(OP) requires [owise]
394+
rule #stackOverflow(_WS, OP) => false requires #stackDelta(OP) <=Int 0
395+
rule #stackOverflow(WS, OP) => 1024 <Int #sizeWordStack(WS) +Int #stackDelta(OP) [owise]
396396
397397
syntax Int ::= #stackNeeded ( OpCode ) [symbol(#stackNeeded), function]
398398
// -----------------------------------------------------------------------

0 commit comments

Comments
 (0)