Implementation of `SLOTNUM` support in the solidity syntax, inline assembly and yul. by rodiazet · Pull Request #16881 · argotorg/solidity

rodiazet · 2026-07-23T12:51:47Z

Description

This PR implements support for SLOTNUM opcode in the EVM.
Introduces:

new member slotnum in the block global variable on solidity language level
builtin slotnum() function in yul and inline assembly
reserves slotnum identifier in the yul and inline assembly starting from amsterdam fork.

Comment:
Adding support in libsolidity/formal makes some tests start failing because of lack of resources. Increasing available resources for Z3 solver makes other tests failing on CI, because of lack of resources on the building machine. I introduced additional check in the SMTEncoder to report the block.slotnum is not supported by the solver yet. Other way it crashes. Additional PR is pushed which implements the support in the SMT solver but the resource issue has to be resolved first.

AI Disclosure

No AI tools were used

Claude Code, Anthropic's CLI for Claude (running on the Sonnet 5 model).

matheusaaguiar

Looks good, but I guess we have to fix/circunvent some tests (at least for now)
test_antl_grammar.sh needs to skip slotnum_osaka_function.sol for chk_antlr_grammar to pass.
We can also add a test case in test/libsolidity/ViewPureChecker.cpp and syntaxTests/constants/initialization/block_tx_msg_property.sol (although I guess they depend on restricting the evm version).

cameel · 2026-07-27T14:43:04Z

I updated our guide to cover new opcodes with a high-level builtin based on our past PRs. I did not find anything missing, but please double check: https://notes.argot.org/@solidity-new-opcode-guide#Special-case-Opcodes-with-a-high-level-Solidity-builtin. Especially the Yul part and test coverage.

rodiazet · 2026-07-28T08:32:58Z

I updated our guide to cover new opcodes with a high-level builtin based on our past PRs. I did not find anything missing, but please double check: https://notes.argot.org/@solidity-new-opcode-guide#Special-case-Opcodes-with-a-high-level-Solidity-builtin. Especially the Yul part and test coverage.

Added some additional points to the testing part.

cameel

Other than the two things below, it seems fine, but I only skimmed through it (and did not review the SMT part too carefully). Up to @matheusaaguiar and @blishko to approve it when they think it's ready.

cameel · 2026-07-27T14:49:36Z

+* EVM: Support `block.slotnum` to access the beacon chain slot number of the current block, available since the Amsterdam EVM version ([EIP-7843](https://eips.ethereum.org/EIPS/eip-7843)).

 Compiler Features:
+* Yul: Introduce builtin `slotnum()` for the `SLOTNUM` opcode, available since the Amsterdam EVM version ([EIP-7843](https://eips.ethereum.org/EIPS/eip-7843)).


This is a language feature.

Needs a separate entry for SMT checker as well.

Moved and change log added.

Does not look moved yet.

Also, the SMTChecker change, if it was possible with any other member then it's bugfix. If it wasn't and the problem only appeared with the addition of slotnum I would not mention it at all - it's just a shim, not a proper feature. #16884 will add an entry for it.

cameel · 2026-07-30T11:19:54Z

+uint constant slotnumGlobal = block.slotnum;
+
+contract A {
+    uint constant slotnum = block.slotnum;


We should have a syntax test showing that the builtin returns uint64 rather than uint. You cannot test that directly, but you can show that uint64 works and uint56 does not.

Also, it would be better if the existing tests were generally using uint64 rather than uint, especially the semantic ones.

Added to semanticTests/conversion

blishko · 2026-07-30T13:55:07Z

The SMT part seems OK to me, but we should as an SMTChecker test to show that we are hitting the change.
That will also help the separate PR adding support in the SMTChecker where we can just change that the output for this test changes to the expect one.

nikola-matic

I looked it over as well and aside from Kamil's comments (uint64 test) and changelog, we can merge. Please fix and I'll approve.

blishko · 2026-08-03T20:51:57Z

I looked it over as well and aside from Kamil's comments (uint64 test) and changelog, we can merge. Please fix and I'll approve.

And SMTChecker test.

rodiazet · 2026-08-04T09:00:03Z

I looked it over as well and aside from Kamil's comments (uint64 test) and changelog, we can merge. Please fix and I'll approve.

And SMTChecker test.

Unfortunately SMTChecker tests hardcodes evm version to the current one. This change requires some small infra change, but we have a cmdLineTest which check this test/cmdlineTests/model_checker_unsupported_block_slotnum/err.

…sembly and yul.

…d of crashing.

blishko

Looks good from my side!

matheusaaguiar reviewed Jul 27, 2026

View reviewed changes

cameel reviewed Jul 27, 2026

View reviewed changes

Comment thread docs/cheatsheet.rst Outdated

Comment thread libsolidity/ast/Types.cpp Outdated

Comment thread libyul/backends/evm/EVMDialect.cpp

Comment thread test/libsolidity/semanticTests/inlineAssembly/slotnum_osaka_function.sol Outdated

rodiazet force-pushed the slotnum branch 7 times, most recently from 07faaa5 to 9412786 Compare July 29, 2026 09:36

rodiazet mentioned this pull request Jul 29, 2026

block.slotnum support in SMT solver. #16884

Open

1 task

rodiazet force-pushed the slotnum branch from 6e7adbe to 2883a9a Compare July 29, 2026 10:38

rodiazet requested review from cameel and matheusaaguiar July 29, 2026 11:32

cameel reviewed Jul 30, 2026

View reviewed changes

cameel requested a review from blishko July 30, 2026 11:29

nikola-matic reviewed Aug 3, 2026

View reviewed changes

rodiazet force-pushed the slotnum branch from 2883a9a to 5aa7ec0 Compare August 4, 2026 09:01

rodiazet requested a review from nikola-matic August 4, 2026 09:02

rodiazet added 2 commits August 4, 2026 18:34

Implementation of SLOTNUM support in the solidity syntax, inline as…

3297a5d

…sembly and yul.

SMTChecker: Gracefully report unsupported block/msg/tx members instea…

a3d9995

…d of crashing.

rodiazet force-pushed the slotnum branch from 5aa7ec0 to a3d9995 Compare August 4, 2026 16:36

rodiazet requested a review from cameel August 5, 2026 12:46

blishko approved these changes Aug 5, 2026

View reviewed changes

Uh oh!

Conversation

rodiazet commented Jul 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

AI Disclosure

Uh oh!

matheusaaguiar left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

cameel commented Jul 27, 2026

Uh oh!

rodiazet commented Jul 28, 2026

Uh oh!

cameel left a comment

Choose a reason for hiding this comment

Uh oh!

cameel Jul 27, 2026

Choose a reason for hiding this comment

Uh oh!

nikola-matic Aug 3, 2026

Choose a reason for hiding this comment

Uh oh!

rodiazet Aug 4, 2026

Choose a reason for hiding this comment

Uh oh!

cameel Aug 4, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rodiazet Aug 4, 2026

Choose a reason for hiding this comment

Uh oh!

cameel Jul 30, 2026

Choose a reason for hiding this comment

Uh oh!

rodiazet Aug 4, 2026

Choose a reason for hiding this comment

Uh oh!

blishko commented Jul 30, 2026

Uh oh!

nikola-matic left a comment

Choose a reason for hiding this comment

Uh oh!

blishko commented Aug 3, 2026

Uh oh!

rodiazet commented Aug 4, 2026

Uh oh!

blishko left a comment

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

rodiazet commented Jul 23, 2026 •

edited

Loading

matheusaaguiar left a comment •

edited

Loading

cameel Aug 4, 2026 •

edited

Loading