Investigate alternate implementations of stub functions

freespek / ssf-mc

EF project Exploring Automatic Model-Checking of the Ethereum specification

Apache License 2.0

4 stars 0 forks source link

Investigate alternate implementations of stub functions #20

Closed Kukovec closed 2 weeks ago

Kukovec commented 3 months ago

Currently, stubs (e.g. GET_VALIDATOR_SET_FOR_SLOT) are implemented as constant operators. We should discuss with our collaborators if/when we want to look into non-constant versions of these operators.

konnov commented 2 weeks ago

I don't think we are going to look into that