### Describe the feature Essentially just implement https://github.com/leanEthereum/leanSpec/pull/449, but gated behind a devnet4 feature flag. ### Additional context _No response_