Skip to content

EIP-7928: block-level access lists #2875

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
anvacaru wants to merge 18 commits into
base: master
Choose a base branch
from
Open

EIP-7928: block-level access lists #2875

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
18 commits
Select commit Hold shift + click to select a range
6ea0fa6
kproj/{schedule,evm}.md, kevm_pyk/{gst_to_kore,cli}.py: define the Am…
anvacaru Jul 13, 2026
a13da59
kproj/{evm,state-utils,serialization,driver}.md, kevm_pyk/gst_to_kore…
anvacaru Jul 13, 2026
16ac866
tests/execution-spec-tests: pin fixtures to tests-glamsterdam-devnet@…
anvacaru Jul 24, 2026
d3dfcac
kproj/schedule.md: add amsterdam blob schedule constants (target 14 /…
anvacaru Jul 17, 2026
eb96e6e
kevm-pyk/src/tests/utils.py: tolerate blank lines in skip-list files
anvacaru Jul 23, 2026
2c85203
kproj/evm.md, kevm_pyk/gst_to_kore.py: drop narrative comments
anvacaru Jul 24, 2026
7524832
update script description
anvacaru Jul 24, 2026
cd82c58
tests/execution-spec-tests/failing.llvm: sort failing fixtures
anvacaru Jul 24, 2026
2fbd62f
schedule.md: align schedule vars
anvacaru Jul 24, 2026
3c03c06
cleanups
anvacaru Jul 24, 2026
75e6f61
kproj/{schedule,evm,state-utils}.md: add eip-7928 BAL cells, journal …
anvacaru Jul 21, 2026
09e003f
kproj/{evm,driver}.md: journal eip-7928 BAL writes, reads, and touches
anvacaru Jul 21, 2026
c8916f6
kproj/evm.md: build, encode, and validate the eip-7928 BAL in #finali…
anvacaru Jul 21, 2026
96bb226
kproj/driver.md: drop the redundant sender balance capture in #deduct…
anvacaru Jul 27, 2026
ddf030d
kproj/evm.md: validate the BAL after exceptionally halting transactions
anvacaru Jul 27, 2026
7c8c6b6
update fixture failing list
anvacaru Jul 27, 2026
4cbc6f2
formatting
anvacaru Jul 27, 2026
fff1500
formatting
anvacaru Jul 27, 2026
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
2 changes: 2 additions & 0 deletions kevm-pyk/src/kevm_pyk/cli.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1007,6 +1007,8 @@ def evm_chain_args(self) -> ArgumentParser:
'SHANGHAI',
'CANCUN',
'PRAGUE',
'OSAKA',
'AMSTERDAM',
)
modes = ('NORMAL', 'VMTESTS')

Expand Down
10 changes: 10 additions & 0 deletions kevm-pyk/src/kevm_pyk/gst_to_kore.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,9 @@
'Frontier': 'FRONTIER',
'Homestead': 'HOMESTEAD',
'EIP150': 'TANGERINE_WHISTLE',
'TangerineWhistle': 'TANGERINE_WHISTLE',
'EIP158': 'SPURIOUS_DRAGON',
'SpuriousDragon': 'SPURIOUS_DRAGON',
'Byzantium': 'BYZANTIUM',
'Constantinople': 'CONSTANTINOPLE',
'ConstantinopleFix': 'PETERSBURG',
Expand All @@ -51,6 +53,12 @@
'CancunToPragueAtTime15k': 'PRAGUE',
'Osaka': 'OSAKA',
'PragueToOsakaAtTime15k': 'OSAKA',
'Amsterdam': 'AMSTERDAM',
'BPO2ToAmsterdamAtTime15k': 'AMSTERDAM',
'OsakaToBPO1AtTime15k': 'OSAKA',
'BPO1ToBPO2AtTime15k': 'OSAKA',
'BPO2ToBPO3AtTime15k': 'AMSTERDAM',
'BPO3ToBPO4AtTime15k': 'AMSTERDAM',
}

_GST_DISCARD_KEYS: Final = frozenset(
Expand All @@ -65,6 +73,8 @@
'hasBigInt',
'config',
'network',
'receipts',
'blockAccessList',
]
)
_GST_LOAD_KEYS: Final = frozenset(
Expand Down
35 changes: 25 additions & 10 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
<txPending> ListItem(TXID:Int) ... </txPending>
<chainID> B </chainID>
<gas> _ => 0 </gas>
<balIndex> I => I +Int 1 </balIndex>
<message>
<msgID> TXID </msgID>
<sigV> TW </sigV>
Expand All @@ -117,7 +118,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
syntax EthereumCommand ::= loadTx ( Account ) [symbol(loadTx)]
// --------------------------------------------------------------
rule <k> loadTx(ACCTFROM)
=> #accessAccounts ACCTFROM #newAddr(ACCTFROM, NONCE) #precompiledAccountsSet(SCHED)
=> #balTouch ACCTFROM ~> #balTouch #newAddr(ACCTFROM, NONCE) ~> #balCaptureBalance ACCTFROM BAL
~> #accessAccounts ACCTFROM #newAddr(ACCTFROM, NONCE) #precompiledAccountsSet(SCHED)
~> #deductBlobGas
~> #loadAccessList(TA)
~> #loadAuthorities(AUTH)
Expand Down Expand Up @@ -156,7 +158,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
andBool GLIMIT >=Int maxInt(G0(SCHED, CODE, true), Ctxfloor(SCHED, CODE))

rule <k> loadTx(ACCTFROM)
=> #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED)
=> #balTouch ACCTFROM ~> #balTouch ACCTTO ~> #balCaptureBalance ACCTFROM BAL ~> #balCaptureNonce ACCTFROM NONCE
~> #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED)
~> #deductBlobGas
~> #loadAccessList(TA)
~> #loadAuthorities(AUTH)
Expand Down Expand Up @@ -311,7 +314,7 @@ Processing SetCode Transaction Authority Entries
orBool (#asWord(NONCE) >=Int maxUInt64)

rule <k> #setDelegation(AUTHORITY, CID, NONCE, ADDR)
=> #touchAccounts AUTHORITY ~> #accessAccounts AUTHORITY
=> #balTouch AUTHORITY ~> #touchAccounts AUTHORITY ~> #accessAccounts AUTHORITY
~> #addAuthority(AUTHORITY, CID, NONCE, ADDR)
...
</k> [owise]
Expand All @@ -328,7 +331,10 @@ Processing SetCode Transaction Authority Entries
requires notBool (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE))
orBool (notBool #asWord(NONCE) ==K ACCTNONCE)

rule <k> #addAuthority(AUTHORITY, _CID, NONCE, ADDR) => .K ... </k>
rule <k> #addAuthority(AUTHORITY, _CID, NONCE, ADDR)
=> #balCaptureCode AUTHORITY ACCTCODE ~> #balCaptureNonce AUTHORITY ACCTNONCE
...
</k>
<schedule> SCHED </schedule>
<refund> REFUND => REFUND +Int Gnewaccount < SCHED > -Int Gauthbase < SCHED > </refund>
<account>
Expand All @@ -340,7 +346,10 @@ Processing SetCode Transaction Authority Entries
requires (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE))
andBool #asWord(NONCE) ==K ACCTNONCE

rule <k> #addAuthority(AUTHORITY, _CID, NONCE, ADDR) => .K ... </k>
rule <k> #addAuthority(AUTHORITY, _CID, NONCE, ADDR)
=> #balCaptureCode AUTHORITY .Bytes ~> #balCaptureNonce AUTHORITY 0
...
</k>
<accounts>
( .Bag
=>
Expand Down Expand Up @@ -624,6 +633,7 @@ Here we check the other post-conditions associated with an EVM test.
SetItem("receiptTrie") SetItem("stateRoot") SetItem("timestamp")
SetItem("transactionsTrie") SetItem("uncleHash") SetItem("baseFeePerGas") SetItem("withdrawalsRoot")
SetItem("blobGasUsed") SetItem("excessBlobGas") SetItem("parentBeaconBlockRoot") SetItem("requestsHash")
SetItem("blockAccessListHash") SetItem("slotNumber")
)

rule <k> check "blockHeader" : { "bloom" : VALUE } => .K ... </k> <logsBloom> VALUE </logsBloom>
Expand All @@ -647,6 +657,8 @@ Here we check the other post-conditions associated with an EVM test.
rule <k> check "blockHeader" : { "excessBlobGas" : VALUE } => .K ... </k> <excessBlobGas> VALUE </excessBlobGas>
rule <k> check "blockHeader" : { "parentBeaconBlockRoot": VALUE } => .K ... </k> <beaconRoot> VALUE </beaconRoot>
rule <k> check "blockHeader" : { "requestsHash" : VALUE } => .K ... </k> <requestsRoot> VALUE </requestsRoot>
rule <k> check "blockHeader" : { "blockAccessListHash" : VALUE } => .K ... </k> <balHash> VALUE </balHash>
rule <k> check "blockHeader" : { "slotNumber" : VALUE } => .K ... </k> <slotNumber> VALUE </slotNumber>


rule <k> check "blockHeader" : { "hash": HASH:Bytes } => .K ...</k>
Expand All @@ -671,11 +683,14 @@ Here we check the other post-conditions associated with an EVM test.
<excessBlobGas> EB </excessBlobGas>
<beaconRoot> BR </beaconRoot>
<requestsRoot> RR </requestsRoot>
requires #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN) ==Int #asWord(HASH)
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF) ==Int #asWord(HASH)
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR) ==Int #asWord(HASH)
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR) ==Int #asWord(HASH)
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR, RR) ==Int #asWord(HASH)
<balHash> BAL </balHash>
<slotNumber> SN </slotNumber>
requires #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN) ==Int #asWord(HASH)
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF) ==Int #asWord(HASH)
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR) ==Int #asWord(HASH)
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR) ==Int #asWord(HASH)
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR, RR) ==Int #asWord(HASH)
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR, RR, BAL, SN) ==Int #asWord(HASH)

rule <k> check { "genesisBlockHeader" : BLOCKHEADER } => check "genesisBlockHeader" : BLOCKHEADER ... </k>
// ---------------------------------------------------------------------------------------------------------
Expand Down
Loading