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 8 commits into
base: amsterdam-foundation
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
8 commits
Select commit Hold shift + click to select a range
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
19 changes: 14 additions & 5 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
Loading