Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Extending KEVM configuration with <wordStackSize> #2628

Closed
wants to merge 16 commits into from
Closed

Extending KEVM configuration with <wordStackSize> #2628

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
16 commits
Select commit Hold shift + click to select a range
738f381
introducing <wordStackSize>
PetarMax Sep 20, 2024
b356fd1
adding underflow constraints
PetarMax Sep 20, 2024
2342626
revisiting tests
PetarMax Sep 20, 2024
cf6f637
optimizations
PetarMax Sep 20, 2024
8c3052a
correction
PetarMax Sep 20, 2024
efe6943
correction
PetarMax Sep 20, 2024
50b3744
adjusting #setStack
PetarMax Sep 20, 2024
866597c
correction
PetarMax Sep 20, 2024
2afff4c
correction
PetarMax Sep 20, 2024
ea61073
swap optimization correction
PetarMax Sep 20, 2024
5f79a96
correction
PetarMax Sep 20, 2024
fe573fa
removing duplicated wordStackSize
PetarMax Sep 21, 2024
557d6d9
capitalising WSSIZE
PetarMax Sep 23, 2024
9fb19d3
Merge branch 'master' into petar/builtin-wordstack-size
PetarMax Sep 25, 2024
00f2300
Merge branch 'master' into petar/builtin-wordstack-size
PetarMax Sep 25, 2024
ad069a0
Merge branch 'master' into petar/builtin-wordstack-size
PetarMax Sep 25, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
85 changes: 45 additions & 40 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -64,12 +64,13 @@ In the comments next to each cell, we've marked which component of the YellowPap
<callValue> 0 </callValue> // I_v

// \mu_*
<wordStack> .WordStack </wordStack> // \mu_s
<localMem> .Bytes </localMem> // \mu_m
<pc> 0 </pc> // \mu_pc
<gas> 0:Gas </gas> // \mau_g
<memoryUsed> 0 </memoryUsed> // \mu_i
<callGas> 0:Gas </callGas>
<wordStack> .WordStack </wordStack> // \mu_s
<wordStackSize> 0 </wordStackSize>
<localMem> .Bytes </localMem> // \mu_m
<pc> 0 </pc> // \mu_pc
<gas> 0:Gas </gas> // \mau_g
<memoryUsed> 0 </memoryUsed> // \mu_i
<callGas> 0:Gas </callGas>

<static> false </static>
<callDepth> 0 </callDepth>
Expand Down Expand Up @@ -330,23 +331,25 @@ The `#next [_]` operator initiates execution by:
...
</k>
<wordStack> WS </wordStack>
<wordStackSize> WSSIZE </wordStackSize>
<static> STATIC:Bool </static>
requires notBool ( #stackUnderflow(WS, OP) orBool #stackOverflow(WS, OP) )
requires notBool ( #stackUnderflow(WSSIZE, OP) orBool #stackOverflow(WSSIZE, OP) )
andBool notBool ( STATIC andBool #changesState(OP, WS) )

rule <k> #next [ OP ] => #end EVMC_STACK_UNDERFLOW ... </k>
<wordStack> WS </wordStack>
requires #stackUnderflow(WS, OP)
<wordStackSize> WSSIZE </wordStackSize>
requires #stackUnderflow(WSSIZE, OP)

rule <k> #next [ OP ] => #end EVMC_STACK_OVERFLOW ... </k>
<wordStack> WS </wordStack>
requires #stackOverflow(WS, OP)
<wordStackSize> WSSIZE </wordStackSize>
requires #stackOverflow(WSSIZE, OP)

rule <k> #next [ OP ] => #end EVMC_STATIC_MODE_VIOLATION ... </k>
<wordStack> WS </wordStack>
<wordStackSize> WSSIZE </wordStackSize>
<static> STATIC:Bool </static>
requires STATIC andBool #changesState(OP, WS)
andBool notBool ( #stackUnderflow(WS, OP) orBool #stackOverflow(WS, OP) )
andBool notBool ( #stackUnderflow(WSSIZE, OP) orBool #stackOverflow(WSSIZE, OP) )
```

### Exceptional Checks
Expand All @@ -356,11 +359,11 @@ The `#next [_]` operator initiates execution by:
- `#stackDelta` is the delta the stack will have after the opcode executes.

```k
syntax Bool ::= #stackUnderflow ( WordStack , OpCode ) [symbol(#stackUnderflow), macro]
| #stackOverflow ( WordStack , OpCode ) [symbol(#stackOverflow), macro]
syntax Bool ::= #stackUnderflow ( Int , OpCode ) [symbol(#stackUnderflow), macro]
| #stackOverflow ( Int , OpCode ) [symbol(#stackOverflow), macro]
// ---------------------------------------------------------------------------------------
rule #stackUnderflow(WS, OP:OpCode) => #sizeWordStack(WS) <Int #stackNeeded(OP)
rule #stackOverflow (WS, OP) => #sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024
rule #stackUnderflow(WSSIZE, OP:OpCode) => WSSIZE <Int #stackNeeded(OP)
rule #stackOverflow (WSSIZE, OP) => WSSIZE +Int #stackDelta(OP) >Int 1024

syntax Int ::= #stackNeeded ( OpCode ) [symbol(#stackNeeded), function]
// -----------------------------------------------------------------------
Expand Down Expand Up @@ -449,18 +452,18 @@ Here we load the correct number of arguments from the `wordStack` based on the s
| TernStackOp Int Int Int
| QuadStackOp Int Int Int Int
// -------------------------------------------------
rule <k> #exec [ UOP:UnStackOp ] => #gas [ UOP , UOP W0 ] ~> UOP W0 ... </k> <wordStack> W0 : WS => WS </wordStack>
rule <k> #exec [ BOP:BinStackOp ] => #gas [ BOP , BOP W0 W1 ] ~> BOP W0 W1 ... </k> <wordStack> W0 : W1 : WS => WS </wordStack>
rule <k> #exec [ TOP:TernStackOp ] => #gas [ TOP , TOP W0 W1 W2 ] ~> TOP W0 W1 W2 ... </k> <wordStack> W0 : W1 : W2 : WS => WS </wordStack>
rule <k> #exec [ QOP:QuadStackOp ] => #gas [ QOP , QOP W0 W1 W2 W3 ] ~> QOP W0 W1 W2 W3 ... </k> <wordStack> W0 : W1 : W2 : W3 : WS => WS </wordStack>
rule <k> #exec [ UOP:UnStackOp ] => #gas [ UOP , UOP W0 ] ~> UOP W0 ... </k> <wordStack> W0 : WS => WS </wordStack> <wordStackSize> WSSIZE => WSSIZE -Int 1 </wordStackSize>
rule <k> #exec [ BOP:BinStackOp ] => #gas [ BOP , BOP W0 W1 ] ~> BOP W0 W1 ... </k> <wordStack> W0 : W1 : WS => WS </wordStack> <wordStackSize> WSSIZE => WSSIZE -Int 2 </wordStackSize>
rule <k> #exec [ TOP:TernStackOp ] => #gas [ TOP , TOP W0 W1 W2 ] ~> TOP W0 W1 W2 ... </k> <wordStack> W0 : W1 : W2 : WS => WS </wordStack> <wordStackSize> WSSIZE => WSSIZE -Int 3 </wordStackSize>
rule <k> #exec [ QOP:QuadStackOp ] => #gas [ QOP , QOP W0 W1 W2 W3 ] ~> QOP W0 W1 W2 W3 ... </k> <wordStack> W0 : W1 : W2 : W3 : WS => WS </wordStack> <wordStackSize> WSSIZE => WSSIZE -Int 4 </wordStackSize>
```

`StackOp` is used for opcodes which require a large portion of the stack.

```k
syntax InternalOp ::= StackOp WordStack
// ---------------------------------------
rule <k> #exec [ SO:StackOp ] => #gas [ SO , SO WS ] ~> SO WS ... </k> <wordStack> WS </wordStack>
syntax InternalOp ::= StackOp WordStack Int
// -------------------------------------------
rule <k> #exec [ SO:StackOp ] => #gas [ SO , SO WS WSSIZE ] ~> SO WS WSSIZE ... </k> <wordStack> WS </wordStack> <wordStackSize> WSSIZE </wordStackSize>
```

The `CallOp` opcodes all interpret their second argument as an address.
Expand All @@ -469,8 +472,8 @@ The `CallOp` opcodes all interpret their second argument as an address.
syntax InternalOp ::= CallSixOp Int Int Int Int Int Int
| CallOp Int Int Int Int Int Int Int
// -----------------------------------------------------------
rule <k> #exec [ CSO:CallSixOp ] => #gas [ CSO , CSO W0 W1 W2 W3 W4 W5 ] ~> CSO W0 W1 W2 W3 W4 W5 ... </k> <wordStack> W0 : W1 : W2 : W3 : W4 : W5 : WS => WS </wordStack>
rule <k> #exec [ CO:CallOp ] => #gas [ CO , CO W0 W1 W2 W3 W4 W5 W6 ] ~> CO W0 W1 W2 W3 W4 W5 W6 ... </k> <wordStack> W0 : W1 : W2 : W3 : W4 : W5 : W6 : WS => WS </wordStack>
rule <k> #exec [ CSO:CallSixOp ] => #gas [ CSO , CSO W0 W1 W2 W3 W4 W5 ] ~> CSO W0 W1 W2 W3 W4 W5 ... </k> <wordStack> W0 : W1 : W2 : W3 : W4 : W5 : WS => WS </wordStack> <wordStackSize> WSSIZE => WSSIZE -Int 6 </wordStackSize>
rule <k> #exec [ CO:CallOp ] => #gas [ CO , CO W0 W1 W2 W3 W4 W5 W6 ] ~> CO W0 W1 W2 W3 W4 W5 W6 ... </k> <wordStack> W0 : W1 : W2 : W3 : W4 : W5 : W6 : WS => WS </wordStack> <wordStackSize> WSSIZE => WSSIZE -Int 7 </wordStackSize>
```

### Address Conversion
Expand Down Expand Up @@ -768,10 +771,10 @@ These are just used by the other operators for shuffling local execution state a
- `#setStack_` will set the current stack to the given one.

```k
syntax InternalOp ::= "#push" | "#setStack" WordStack
// -----------------------------------------------------
rule <k> W0:Int ~> #push => .K ... </k> <wordStack> WS => W0 : WS </wordStack>
rule <k> #setStack WS => .K ... </k> <wordStack> _ => WS </wordStack>
syntax InternalOp ::= "#push" | "#setStack" WordStack Int
// ---------------------------------------------------------
rule <k> W0:Int ~> #push => .K ... </k> <wordStack> WS => W0 : WS </wordStack> <wordStackSize> WSSIZE => WSSIZE +Int 1 </wordStackSize>
rule <k> #setStack WS WSSIZE => .K ... </k> <wordStack> _ => WS </wordStack> <wordStackSize> _ => WSSIZE </wordStackSize>
```

- `#newAccount_` allows declaring a new empty account with the given address (and assumes the rounding to 160 bits has already occurred).
Expand Down Expand Up @@ -893,8 +896,8 @@ Some operators don't calculate anything, they just push the stack around a bit.
syntax StackOp ::= DUP ( Int ) [symbol(DUP)]
| SWAP ( Int ) [symbol(SWAP)]
// ----------------------------------------------
rule <k> DUP(N) WS:WordStack => #setStack ((WS [ N -Int 1 ]) : WS) ... </k>
rule <k> SWAP(N) (W0 : WS) => #setStack ((WS [ N -Int 1 ]) : (WS [ N -Int 1 := W0 ])) ... </k>
rule <k> DUP(N) WS:WordStack WSSIZE => #setStack ((WS [ N -Int 1 ]) : WS) (WSSIZE +Int 1) ... </k>
rule <k> SWAP(N) (W0 : WS) WSSIZE => #setStack ((WS [ N -Int 1 ]) : (WS [ N -Int 1 := W0 ])) WSSIZE ... </k>

syntax PushOp ::= "PUSHZERO"
| PUSH ( Int ) [symbol(PUSH)]
Expand Down Expand Up @@ -1168,9 +1171,10 @@ These operators query about the current return data buffer.
rule <k> LOG(N) MEMSTART MEMWIDTH => .K ... </k>
<id> ACCT </id>
<wordStack> WS => #drop(N, WS) </wordStack>
<wordStackSize> WSSIZE => WSSIZE -Int N </wordStackSize>
<localMem> LM </localMem>
<log> L => L ListItem({ ACCT | WordStack2List(#take(N, WS)) | #range(LM, MEMSTART, MEMWIDTH) }) </log>
requires #sizeWordStack(WS) >=Int N
requires WSSIZE >=Int N
```

Ethereum Network OpCodes
Expand Down Expand Up @@ -1400,12 +1404,13 @@ The various `CALL*` (and other inter-contract control flow) operations will be d

syntax KItem ::= "#initVM"
// --------------------------
rule <k> #initVM => .K ... </k>
<pc> _ => 0 </pc>
<memoryUsed> _ => 0 </memoryUsed>
<output> _ => .Bytes </output>
<wordStack> _ => .WordStack </wordStack>
<localMem> _ => .Bytes </localMem>
rule <k> #initVM => .K ... </k>
<pc> _ => 0 </pc>
<memoryUsed> _ => 0 </memoryUsed>
<output> _ => .Bytes </output>
<wordStack> _ => .WordStack </wordStack>
<wordStackSize> _ => 0 </wordStackSize>
<localMem> _ => .Bytes </localMem>

syntax KItem ::= "#loadProgram" Bytes [symbol(loadProgram)]
// -----------------------------------------------------------
Expand Down Expand Up @@ -2250,8 +2255,8 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
rule <k> #gasExec(SCHED, MSTORE _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, MSTORE8 _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, PUSH(_)) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, DUP(_) _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, SWAP(_) _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, DUP(_) _ _) => Gverylow < SCHED > ... </k>
rule <k> #gasExec(SCHED, SWAP(_) _ _) => Gverylow < SCHED > ... </k>

// Wlow
rule <k> #gasExec(SCHED, MUL _ _) => Glow < SCHED > ... </k>
Expand Down
58 changes: 47 additions & 11 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,6 +27,9 @@ module EVM-OPTIMIZATIONS
<wordStack>
( WS => 0 : WS )
</wordStack>
<wordStackSize>
( WSSIZE => WSSIZE +Int 1 )
</wordStackSize>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
Expand All @@ -42,7 +45,8 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( #if USEGAS #then Gbase < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( #sizeWordStack( WS ) <=Int 1023 )
andBool ( 0 <=Int WSSIZE )
andBool ( WSSIZE <=Int 1023 )
[priority(40)]

rule
Expand All @@ -66,6 +70,9 @@ module EVM-OPTIMIZATIONS
<wordStack>
( WS => #asWord( #range(PGM, PCOUNT +Int 1, N) ) : WS )
</wordStack>
<wordStackSize>
( WSSIZE => WSSIZE +Int 1 )
</wordStackSize>
<pc>
( PCOUNT => ( ( PCOUNT +Int N ) +Int 1 ) )
</pc>
Expand All @@ -81,7 +88,8 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( #sizeWordStack( WS ) <=Int 1023 )
andBool ( 0 <=Int WSSIZE )
andBool ( WSSIZE <=Int 1023 )
[priority(40)]

rule
Expand All @@ -102,6 +110,9 @@ module EVM-OPTIMIZATIONS
<wordStack>
( WS => WS [ ( N +Int -1 ) ] : WS )
</wordStack>
<wordStackSize>
( WSSIZE => WSSIZE +Int 1 )
</wordStackSize>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
Expand All @@ -116,9 +127,10 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires N <=Int #sizeWordStack(WS)
requires N <=Int WSSIZE
andBool ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( #sizeWordStack( WS ) <=Int 1023 )
andBool ( 0 <=Int WSSIZE )
andBool ( WSSIZE <=Int 1023 )
[priority(40)]

rule
Expand All @@ -139,6 +151,9 @@ module EVM-OPTIMIZATIONS
<wordStack>
( W0 : WS => WS [ ( N +Int -1 ) ] : ( WS [ ( N +Int -1 ) := W0 ] ) )
</wordStack>
<wordStackSize>
WSSIZE
</wordStackSize>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
Expand All @@ -153,9 +168,10 @@ module EVM-OPTIMIZATIONS
</ethereum>
...
</kevm>
requires N <=Int #sizeWordStack(WS)
requires N +Int 1 <=Int WSSIZE
andBool ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( #sizeWordStack( WS ) <=Int 1023 )
andBool ( 0 <=Int WSSIZE )
andBool ( WSSIZE <=Int 1024 )
[priority(40)]

rule
Expand All @@ -176,6 +192,9 @@ module EVM-OPTIMIZATIONS
<wordStack>
( W0 : W1 : WS => chop( ( W0 +Int W1 ) ) : WS )
</wordStack>
<wordStackSize>
WSSIZE => WSSIZE -Int 1
</wordStackSize>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
Expand All @@ -191,7 +210,8 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( #sizeWordStack( WS ) <=Int 1023 )
andBool ( 2 <=Int WSSIZE )
andBool ( WSSIZE <=Int 1023 )
[priority(40)]

rule
Expand All @@ -212,6 +232,9 @@ module EVM-OPTIMIZATIONS
<wordStack>
( W0 : W1 : WS => chop( ( W0 -Int W1 ) ) : WS )
</wordStack>
<wordStackSize>
WSSIZE => WSSIZE -Int 1
</wordStackSize>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
Expand All @@ -227,7 +250,8 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( #sizeWordStack( WS ) <=Int 1023 )
andBool ( 2 <=Int WSSIZE )
andBool ( WSSIZE <=Int 1023 )
[priority(40)]

rule
Expand All @@ -248,6 +272,9 @@ module EVM-OPTIMIZATIONS
<wordStack>
( W0 : W1 : WS => W0 &Int W1 : WS )
</wordStack>
<wordStackSize>
WSSIZE => WSSIZE -Int 1
</wordStackSize>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
Expand All @@ -263,7 +290,8 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( #sizeWordStack( WS ) <=Int 1023 )
andBool ( 2 <=Int WSSIZE )
andBool ( WSSIZE <=Int 1023 )
[priority(40)]

rule
Expand All @@ -284,6 +312,9 @@ module EVM-OPTIMIZATIONS
<wordStack>
( W0 : W1 : WS => bool2Word( W0 <Int W1 ) : WS )
</wordStack>
<wordStackSize>
WSSIZE => WSSIZE -Int 1
</wordStackSize>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
Expand All @@ -299,7 +330,8 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( #sizeWordStack( WS ) <=Int 1023 )
andBool ( 2 <=Int WSSIZE )
andBool ( WSSIZE <=Int 1023 )
[priority(40)]

rule
Expand All @@ -320,6 +352,9 @@ module EVM-OPTIMIZATIONS
<wordStack>
( W0 : W1 : WS => bool2Word( W1 <Int W0 ) : WS )
</wordStack>
<wordStackSize>
WSSIZE => WSSIZE -Int 1
</wordStackSize>
<pc>
( PCOUNT => ( PCOUNT +Int 1 ) )
</pc>
Expand All @@ -335,7 +370,8 @@ module EVM-OPTIMIZATIONS
...
</kevm>
requires ( #if USEGAS #then Gverylow < SCHED > <=Gas GAVAIL #else true #fi )
andBool ( #sizeWordStack( WS ) <=Int 1023 )
andBool ( 2 <=Int WSSIZE )
andBool ( WSSIZE <=Int 1023 )
[priority(40)]


Expand Down
1 change: 1 addition & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,7 @@ module STATE-UTILS
<callData> _ => .Bytes </callData>
<callValue> _ => 0 </callValue>
<wordStack> _ => .WordStack </wordStack>
<wordStackSize> _ => 0 </wordStackSize>
<localMem> _ => .Bytes </localMem>
<pc> _ => 0 </pc>
<gas> _ => 0 </gas>
Expand Down
5 changes: 3 additions & 2 deletions media/201908-trufflecon/add-gas-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,10 @@ module ADD-GAS-SPEC
rule <k> #next [ ADD ] => . ... </k>
<schedule> SCHEDULE </schedule>
<wordStack> W0 : W1 : WS => chop(W0 +Int W1) : WS </wordStack>
<wordStackSize> WSSIZE => WSSIZE -Int 1 </wordStackSize>
<pc> PCOUNT => PCOUNT +Int 1 </pc>
<gas> G => G -Int Gverylow < SCHEDULE > </gas>
requires notBool ( #stackUnderflow ( W0 : W1 : WS , ADD )
orBool #stackOverflow ( W0 : W1 : WS , ADD )
requires notBool ( #stackUnderflow ( WSSIZE , ADD )
orBool #stackOverflow ( WSSIZE , ADD )
)
endmodule
3 changes: 2 additions & 1 deletion media/201908-trufflecon/add-overflow-spec.k
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,10 @@ module ADD-OVERFLOW-SPEC
rule <k> #next [ ADD ] => . ... </k>
<schedule> SCHEDULE </schedule>
<wordStack> W0 : W1 : WS => chop(W0 +Int W1) : WS </wordStack>
<wordStackSize> WSSIZE => WSSIZE -Int 1 </wordStackSize>
<pc> PCOUNT => PCOUNT +Int 1 </pc>
<gas> G => G -Int Gverylow < SCHEDULE > </gas>
requires G >=Int Gverylow < SCHEDULE >
andBool notBool ( #stackUnderflow ( W0 : W1 : WS , ADD )
andBool notBool ( #stackUnderflow ( WSSIZE , ADD )
)
endmodule
Loading
Loading