Skip to content

Changes needed to handle CSE #54

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

Open
nishantjr wants to merge 5 commits into
base: ulm
Choose a base branch
from
Open

Changes needed to handle CSE #54

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
f7a63e9
create-invalid: Replace [owise] with explicit side condition
nishantjr May 13, 2025
adedb7c
Configuration: Generalize <gas> to allow infinite gas
nishantjr May 9, 2025
e63c753
Add <worldState> cell for capturing side-effects of impure hooks
nishantjr May 12, 2025
f0257cd
Tweaks to evm semantics to make summarizaion easier.
nishantjr May 22, 2025
277aa01
Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
nishantjr Jun 3, 2025
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
3 changes: 3 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -377,6 +377,9 @@ Bytes helper functions
rule #padToWidth(N, BS) => padLeftBytes(BS, N, 0) requires 0 <=Int N [concrete]
rule #padRightToWidth(N, BS) => BS requires notBool (0 <=Int N) [concrete]
rule #padRightToWidth(N, BS) => padRightBytes(BS, N, 0) requires 0 <=Int N [concrete]

syntax Bool ::= Bytes "==Bytes" Bytes [symbol(_==Bytes_), function, total]
rule B1 ==Bytes B2 => B1 ==K B2
```

Accounts
Expand Down
38 changes: 27 additions & 11 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 @@ -57,7 +57,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
<wordStack> .List </wordStack> // \mu_s
<localMem> .Bytes </localMem> // \mu_m
<pc> 0 </pc> // \mu_pc
<gas> $GAS:Int </gas> // \mau_g
<gas> ($GAS:Int):Gas </gas> // \mau_g
<memoryUsed> 0 </memoryUsed> // \mu_i
<callGas> 0:Gas </callGas>

Expand All @@ -68,7 +68,20 @@ In the comments next to each cell, we've marked which component of the YellowPap
// -------------------------------------
</evm>
</ethereum>
```

For symbolic execution, we create an additional cell, to capture the
side-effects of impure hooks.

```symbolic
<worldState> .WorldState </worldState>

syntax WorldState ::= ".WorldState" [function, total]
rule <k> WS:WorldState => .K ... </k>
<worldState> _ => WS </worldState>
```

```k
syntax EthereumSimulation
// -------------------------
```
Expand Down Expand Up @@ -955,7 +968,9 @@ For each `CALL*` operation, we make a corresponding call to `#call` and a state-
[preserves-definedness]

rule [create-invalid]:
<k> CREATE _ _ _ => #end EVMC_OUT_OF_GAS ... </k> [owise]
<k> CREATE _ _ MEMWIDTH => #end EVMC_OUT_OF_GAS ... </k>
<schedule> SCHED </schedule>
requires notBool #hasValidInitCode(MEMWIDTH, SCHED)
```

`CREATE2` will attempt to `#create` the account, but with the new scheme for choosing the account address.
Expand Down Expand Up @@ -1171,17 +1186,18 @@ Precompiled Contracts
rule <k> KZGPOINTEVAL => #end EVMC_SUCCESS ... </k>
<output> _ => Int2Bytes(32, 4096, BE) +Bytes Int2Bytes(32, blsModulus, BE) </output>
requires lengthBytes( CallData() ) ==Int 192
andBool #kzg2vh(substrBytes(CallData(), 96, 144)) ==K substrBytes(CallData(), 0, 32)
andBool #kzg2vh(substrBytes(CallData(), 96, 144)) ==Bytes substrBytes(CallData(), 0, 32)
andBool Bytes2Int(substrBytes(CallData(), 32, 64), BE, Unsigned) <Int blsModulus
andBool Bytes2Int(substrBytes(CallData(), 64, 96), BE, Unsigned) <Int blsModulus
andBool verifyKZGProof(substrBytes(CallData(), 96, 144), substrBytes(CallData(), 32, 64), substrBytes(CallData(), 64, 96), substrBytes(CallData(), 144, 192))

rule <k> KZGPOINTEVAL => #end EVMC_PRECOMPILE_FAILURE ... </k>
requires lengthBytes( CallData() ) =/=Int 192
orBool #kzg2vh(substrBytes(CallData(), 96, 144)) =/=K substrBytes(CallData(), 0, 32)
orBool Bytes2Int(substrBytes(CallData(), 32, 64), BE, Unsigned) >=Int blsModulus
orBool Bytes2Int(substrBytes(CallData(), 64, 96), BE, Unsigned) >=Int blsModulus
orBool notBool verifyKZGProof(substrBytes(CallData(), 96, 144), substrBytes(CallData(), 32, 64), substrBytes(CallData(), 64, 96), substrBytes(CallData(), 144, 192))
requires notBool
( lengthBytes( CallData() ) ==Int 192
andBool #kzg2vh(substrBytes(CallData(), 96, 144)) ==Bytes substrBytes(CallData(), 0, 32)
andBool Bytes2Int(substrBytes(CallData(), 32, 64), BE, Unsigned) <Int blsModulus
andBool Bytes2Int(substrBytes(CallData(), 64, 96), BE, Unsigned) <Int blsModulus
andBool verifyKZGProof(substrBytes(CallData(), 96, 144), substrBytes(CallData(), 32, 64), substrBytes(CallData(), 64, 96), substrBytes(CallData(), 144, 192)))

syntax Bytes ::= #kzg2vh ( Bytes ) [symbol(#kzg2vh), function, total]
// ---------------------------------------------------------------------
Expand Down Expand Up @@ -1535,8 +1551,8 @@ Overall Gas
<memoryUsed> MU => MU' </memoryUsed> <schedule> SCHED </schedule>

rule <k> _G:Gas ~> (#deductMemoryGas => #deductGas) ... </k> //Required for verification
rule <k> G:Int ~> #deductGas => #end EVMC_OUT_OF_GAS ... </k> <gas> GAVAIL:Int </gas> requires GAVAIL <Int G
rule <k> G:Int ~> #deductGas => .K ... </k> <gas> GAVAIL:Int => GAVAIL -Int G </gas> requires G <=Int GAVAIL
rule <k> G:Gas ~> #deductGas => #end EVMC_OUT_OF_GAS ... </k> <gas> GAVAIL </gas> requires GAVAIL <Gas G
rule <k> G:Gas ~> #deductGas => .K ... </k> <gas> GAVAIL => GAVAIL -Gas G </gas> requires G <=Gas GAVAIL

syntax Bool ::= #inStorage ( Map , Account , Int ) [symbol(#inStorage), function, total]
| #inStorageAux1 ( KItem , Int ) [symbol(#inStorageAux1), function, total]
Expand Down Expand Up @@ -1881,7 +1897,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
// ------------------------------------------
rule <schedule> SCHED </schedule>
<k> #allocateCreateGas => .K ... </k>
<gas> GAVAIL => #if Gstaticcalldepth << SCHED >> #then 0 #else GAVAIL /Int 64 #fi </gas>
<gas> GAVAIL => #if Gstaticcalldepth << SCHED >> #then 0 #else GAVAIL /Gas 64 #fi </gas>
<callGas> _ => #if Gstaticcalldepth << SCHED >> #then GAVAIL #else #allBut64th(GAVAIL) #fi </callGas>
[preserves-definedness]
```
Expand Down
Loading