Skip to content
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

Jump to bottom

Generate structure-s for non-leaf cells #4731

Open
wants to merge 6 commits into
base: develop
Choose a base branch
from
Open

Generate structure-s for non-leaf cells #4731

wants to merge 6 commits into from
+148 −7

Conversation

tothtamas28
Copy link
Contributor

@tothtamas28 tothtamas28 commented Jan 9, 2025 •
edited
Loading

Closes #4723

If the cell is a leaf, an inductive with a single constructor is generated:

inductive SortGasCell : Type where
  | mk (val : SortGas) : SortGasCell

If the cell is non-leaf, a structure with fields corresponding to subcell names is generated:

structure SortGeneratedTopCell : Type where
  kevm : SortKevmCell
  generatedCounter : SortGeneratedCounterCell

Cells are topological sorted w. r. t. their dependencies.

@tothtamas28
Extract cell type generation into a separate step
4a565cd
@tothtamas28
Extract function _param_sorts
33702a7
@tothtamas28
Sort cell type definitions topologically
f9c1621
@tothtamas28
Add custom generator logic for cell sort
314d400 
If the cell is a leaf, an `inductive` with a single constructor `mk` is
generated. Otherwise, a `structure` is generated.
@tothtamas28 tothtamas28 self-assigned this Jan 9, 2025
@tothtamas28 tothtamas28 linked an issue Jan 9, 2025 that may be closed by this pull request
Use structure instead of inductive where possible #4723
Open
@tothtamas28
Copy link
Contributor Author

tothtamas28 commented Jan 9, 2025 •
edited
Loading

The Lean 4 definition generated for evm-semantics.llvm:

Expand 
inductive SortAccessListTx : Type where
  | AccessListTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortAccount) (x4 : SortInt) (x5 : SortBytes) (x6 : SortInt) (x7 : SortJSONs) : SortAccessListTx

inductive SortAccount : Type where
  | inj_SortInt (x : SortInt) : SortAccount
  | «.Account_EVM-TYPES_Account» : SortAccount

inductive SortAccountCode : Type where
  | inj_SortBytes (x : SortBytes) : SortAccountCode

inductive SortAccounts : Type where
  | «{_|_}_EVM_Accounts_AccountsCell_SubstateCell» (x0 : SortAccountsCell) (x1 : SortSubstateCell) : SortAccounts

inductive SortBExp : Type where
  | inj_SortBool (x : SortBool) : SortBExp
  | «#accountNonexistent» (x0 : SortInt) : SortBExp

inductive SortBinStackOp : Type where
  | inj_SortLogOp (x : SortLogOp) : SortBinStackOp
  | ADD_EVM_BinStackOp : SortBinStackOp
  | AND_EVM_BinStackOp : SortBinStackOp
  | BYTE_EVM_BinStackOp : SortBinStackOp
  | DIV_EVM_BinStackOp : SortBinStackOp
  | EQ_EVM_BinStackOp : SortBinStackOp
  | EVMOR_EVM_BinStackOp : SortBinStackOp
  | EXP_EVM_BinStackOp : SortBinStackOp
  | GT_EVM_BinStackOp : SortBinStackOp
  | JUMPI_EVM_BinStackOp : SortBinStackOp
  | LT_EVM_BinStackOp : SortBinStackOp
  | MOD_EVM_BinStackOp : SortBinStackOp
  | MSTORE_EVM_BinStackOp : SortBinStackOp
  | MSTORE8_EVM_BinStackOp : SortBinStackOp
  | MUL_EVM_BinStackOp : SortBinStackOp
  | RETURN_EVM_BinStackOp : SortBinStackOp
  | REVERT_EVM_BinStackOp : SortBinStackOp
  | SAR_EVM_BinStackOp : SortBinStackOp
  | SDIV_EVM_BinStackOp : SortBinStackOp
  | SGT_EVM_BinStackOp : SortBinStackOp
  | SHA3_EVM_BinStackOp : SortBinStackOp
  | SHL_EVM_BinStackOp : SortBinStackOp
  | SHR_EVM_BinStackOp : SortBinStackOp
  | SIGNEXTEND_EVM_BinStackOp : SortBinStackOp
  | SLT_EVM_BinStackOp : SortBinStackOp
  | SMOD_EVM_BinStackOp : SortBinStackOp
  | SSTORE_EVM_BinStackOp : SortBinStackOp
  | SUB_EVM_BinStackOp : SortBinStackOp
  | TSTORE_EVM_BinStackOp : SortBinStackOp
  | XOR_EVM_BinStackOp : SortBinStackOp

inductive SortCallOp : Type where
  | CALL_EVM_CallOp : SortCallOp
  | CALLCODE_EVM_CallOp : SortCallOp

inductive SortCallSixOp : Type where
  | DELEGATECALL_EVM_CallSixOp : SortCallSixOp
  | STATICCALL_EVM_CallSixOp : SortCallSixOp

inductive SortDynamicFeeTx : Type where
  | DynamicFeeTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortAccount) (x5 : SortInt) (x6 : SortBytes) (x7 : SortInt) (x8 : SortJSONs) : SortDynamicFeeTx

inductive SortEndStatusCode : Type where
  | inj_SortExceptionalStatusCode (x : SortExceptionalStatusCode) : SortEndStatusCode
  | EVMC_REVERT_NETWORK_EndStatusCode : SortEndStatusCode
  | EVMC_SUCCESS_NETWORK_EndStatusCode : SortEndStatusCode

inductive SortEndianness : Type where
  | bigEndianBytes : SortEndianness

inductive SortEthereumCommand : Type where
  | «#executeBeaconRoots» : SortEthereumCommand
  | «#finalizeBlock_EVM_EthereumCommand» : SortEthereumCommand
  | «#finishTx_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «#loadAccessList» (x0 : SortJSON) : SortEthereumCommand
  | «#loadAccessListAux» (x0 : SortAccount) (x1 : SortList) : SortEthereumCommand
  | «#rewardOmmers» (x0 : SortJSONs) : SortEthereumCommand
  | «#startBlock_EVM_EthereumCommand» : SortEthereumCommand
  | «check__ETHEREUM-SIMULATION_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «clear_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «clearBLOCK_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «clearNETWORK_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «clearTX_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «exception_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «failure__ETHEREUM-SIMULATION_EthereumCommand_String» (x0 : SortString) : SortEthereumCommand
  | «flush_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «load__STATE-UTILS_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «loadAccount___STATE-UTILS_EthereumCommand_Int_JSON» (x0 : SortInt) (x1 : SortJSON) : SortEthereumCommand
  | «loadTransaction___STATE-UTILS_EthereumCommand_Int_JSON» (x0 : SortInt) (x1 : SortJSON) : SortEthereumCommand
  | loadTx (x0 : SortAccount) : SortEthereumCommand
  | «mkAcct__STATE-UTILS_EthereumCommand_Int» (x0 : SortInt) : SortEthereumCommand
  | «mkTX__STATE-UTILS_EthereumCommand_Int» (x0 : SortInt) : SortEthereumCommand
  | «process__ETHEREUM-SIMULATION_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «run__ETHEREUM-SIMULATION_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «start_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «startTx_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «status__ETHEREUM-SIMULATION_EthereumCommand_StatusCode» (x0 : SortStatusCode) : SortEthereumCommand
  | «success_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand

inductive SortEthereumSimulation : Type where
  | inj_SortAccount (x : SortAccount) : SortEthereumSimulation
  | inj_SortBool (x : SortBool) : SortEthereumSimulation
  | inj_SortBytes (x : SortBytes) : SortEthereumSimulation
  | inj_SortInt (x : SortInt) : SortEthereumSimulation
  | inj_SortJSON (x : SortJSON) : SortEthereumSimulation
  | inj_SortMap (x : SortMap) : SortEthereumSimulation
  | inj_SortOpCodes (x : SortOpCodes) : SortEthereumSimulation
  | inj_SortString (x : SortString) : SortEthereumSimulation
  | inj_SortSubstateLogEntry (x : SortSubstateLogEntry) : SortEthereumSimulation
  | inj_SortTxType (x : SortTxType) : SortEthereumSimulation
  | «.EthereumSimulation_ETHEREUM-SIMULATION_EthereumSimulation» : SortEthereumSimulation
  | «___ETHEREUM-SIMULATION_EthereumSimulation_EthereumCommand_EthereumSimulation» (x0 : SortEthereumCommand) (x1 : SortEthereumSimulation) : SortEthereumSimulation

inductive SortExceptionalStatusCode : Type where
  | EVMC_ACCOUNT_ALREADY_EXISTS_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_BAD_JUMP_DESTINATION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_BALANCE_UNDERFLOW_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_CALL_DEPTH_EXCEEDED_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_INVALID_INSTRUCTION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_INVALID_MEMORY_ACCESS_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_NONCE_EXCEEDED_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_OUT_OF_GAS_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_PRECOMPILE_FAILURE_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_STACK_OVERFLOW_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_STACK_UNDERFLOW_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_STATIC_MODE_VIOLATION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_UNDEFINED_INSTRUCTION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode

inductive SortExp : Type where
  | inj_SortGas (x : SortGas) : SortExp
  | inj_SortInt (x : SortInt) : SortExp
  | Ccall (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortGas) (x3 : SortGas) (x4 : SortInt) (x5 : SortBool) : SortExp
  | Ccallgas (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortGas) (x3 : SortGas) (x4 : SortInt) (x5 : SortBool) : SortExp
  | Cselfdestruct (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortInt) : SortExp

inductive SortG1Point : Type where
  | «(_,_)_KRYPTO_G1Point_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortG1Point

inductive SortG2Point : Type where
  | «(_x_,_x_)_KRYPTO_G2Point_Int_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : SortG2Point

inductive SortGas : Type where
  | inj_SortInt (x : SortInt) : SortGas

inductive SortInternalOp : Type where
  | «#access[_,_]_EVM_InternalOp_OpCode_OpCode» (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | «#addr[_]_EVM_InternalOp_OpCode» (x0 : SortOpCode) : SortInternalOp
  | «#allocateCallGas_EVM_InternalOp» : SortInternalOp
  | «#allocateCreateGas_EVM_InternalOp» : SortInternalOp
  | «#call________EVM_InternalOp_Int_Int_Int_Int_Int_Bytes_Bool» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortBytes) (x6 : SortBool) : SortInternalOp
  | «#callWithCode_________EVM_InternalOp_Int_Int_Int_Bytes_Int_Int_Bytes_Bool» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) (x5 : SortInt) (x6 : SortBytes) (x7 : SortBool) : SortInternalOp
  | «#checkBalanceUnderflow___EVM_InternalOp_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | «#checkCall___EVM_InternalOp_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | «#checkCreate___EVM_InternalOp_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | «#checkDepthExceeded_EVM_InternalOp» : SortInternalOp
  | «#checkNonceExceeded__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#checkPoint_EVM_InternalOp» : SortInternalOp
  | «#create_____EVM_InternalOp_Int_Int_Int_Bytes» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : SortInternalOp
  | «#deductGas_EVM_InternalOp» : SortInternalOp
  | «#deductMemory_EVM_InternalOp» : SortInternalOp
  | «#deductMemoryGas_EVM_InternalOp» : SortInternalOp
  | «#deleteAccounts» (x0 : SortList) : SortInternalOp
  | «#dropCallStack_EVM_InternalOp» : SortInternalOp
  | «#dropWorldState_EVM_InternalOp» : SortInternalOp
  | «#ecadd» (x0 : SortG1Point) (x1 : SortG1Point) : SortInternalOp
  | «#ecmul» (x0 : SortG1Point) (x1 : SortInt) : SortInternalOp
  | «#ecpairing» (x0 : SortList) (x1 : SortList) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) : SortInternalOp
  | «#endBasicBlock_EVM_InternalOp» : SortInternalOp
  | «#exec[_]_EVM_InternalOp_OpCode» (x0 : SortOpCode) : SortInternalOp
  | «#finalizeStorage» (x0 : SortList) : SortInternalOp
  | «#finalizeTx» (x0 : SortBool) : SortInternalOp
  | «#gas[_,_]_EVM_InternalOp_OpCode_OpCode» (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | «#gas[_]_EVM_InternalOp_OpCode» (x0 : SortOpCode) : SortInternalOp
  | «#gasAccess» (x0 : SortSchedule) (x1 : SortOpCode) : SortInternalOp
  | «#gasExec» (x0 : SortSchedule) (x1 : SortOpCode) : SortInternalOp
  | «#incrementNonce__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#memory[_,_]_EVM_InternalOp_OpCode_OpCode» (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | «#mkCall________EVM_InternalOp_Int_Int_Int_Bytes_Int_Bytes_Bool» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) (x5 : SortBytes) (x6 : SortBool) : SortInternalOp
  | «#mkCreate_____EVM_InternalOp_Int_Int_Int_Bytes» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : SortInternalOp
  | «#newAccount__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#newExistingAccount__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#next[_]_EVM_InternalOp_MaybeOpCode» (x0 : SortMaybeOpCode) : SortInternalOp
  | «#popCallStack_EVM_InternalOp» : SortInternalOp
  | «#popWorldState_EVM_InternalOp» : SortInternalOp
  | «#precompiled?(_,_)_EVM_InternalOp_Int_Schedule» (x0 : SortInt) (x1 : SortSchedule) : SortInternalOp
  | «#push_EVM_InternalOp» : SortInternalOp
  | «#pushCallStack_EVM_InternalOp» : SortInternalOp
  | «#pushWorldState_EVM_InternalOp» : SortInternalOp
  | «#refund__EVM_InternalOp_Gas» (x0 : SortGas) : SortInternalOp
  | «#setLocalMem____EVM_InternalOp_Int_Int_Bytes» (x0 : SortInt) (x1 : SortInt) (x2 : SortBytes) : SortInternalOp
  | «#setStack__EVM_InternalOp_WordStack» (x0 : SortWordStack) : SortInternalOp
  | «#transferFunds____EVM_InternalOp_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | «#transferFundsToNonExistent____EVM_InternalOp_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | ___EVM_InternalOp_StackOp_WordStack (x0 : SortStackOp) (x1 : SortWordStack) : SortInternalOp
  | ___EVM_InternalOp_UnStackOp_Int (x0 : SortUnStackOp) (x1 : SortInt) : SortInternalOp
  | ____EVM_InternalOp_BinStackOp_Int_Int (x0 : SortBinStackOp) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | _____EVM_InternalOp_TernStackOp_Int_Int_Int (x0 : SortTernStackOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : SortInternalOp
  | ______EVM_InternalOp_QuadStackOp_Int_Int_Int_Int (x0 : SortQuadStackOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) : SortInternalOp
  | ________EVM_InternalOp_CallSixOp_Int_Int_Int_Int_Int_Int (x0 : SortCallSixOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortInt) : SortInternalOp
  | _________EVM_InternalOp_CallOp_Int_Int_Int_Int_Int_Int_Int (x0 : SortCallOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortInt) (x7 : SortInt) : SortInternalOp
  | pc (x0 : SortOpCode) : SortInternalOp

inductive SortInvalidOp : Type where
  | INVALID_EVM_InvalidOp : SortInvalidOp
  | «UNDEFINED(_)_EVM_InvalidOp_Int» (x0 : SortInt) : SortInvalidOp

inductive SortJSON : Type where
  | inj_SortAccount (x : SortAccount) : SortJSON
  | inj_SortBool (x : SortBool) : SortJSON
  | inj_SortBytes (x : SortBytes) : SortJSON
  | inj_SortInt (x : SortInt) : SortJSON
  | inj_SortMap (x : SortMap) : SortJSON
  | inj_SortOpCodes (x : SortOpCodes) : SortJSON
  | inj_SortString (x : SortString) : SortJSON
  | inj_SortSubstateLogEntry (x : SortSubstateLogEntry) : SortJSON
  | inj_SortTxType (x : SortTxType) : SortJSON
  | JSONEntry (x0 : SortJSONKey) (x1 : SortJSON) : SortJSON
  | JSONList (x0 : SortJSONs) : SortJSON
  | JSONObject (x0 : SortJSONs) : SortJSON
  | JSONnull : SortJSON

inductive SortJSONKey : Type where
  | inj_SortInt (x : SortInt) : SortJSONKey
  | inj_SortString (x : SortString) : SortJSONKey

inductive SortJSONs : Type where
  | «.List{"JSONs"}» : SortJSONs
  | JSONs (x0 : SortJSON) (x1 : SortJSONs) : SortJSONs

inductive SortK : Type where
  | dotk : SortK
  | kseq (x0 : SortKItem) (x1 : SortK) : SortK

inductive SortKItem : Type where
  | inj_SortAccessListTx (x : SortAccessListTx) : SortKItem
  | inj_SortAccessedAccountsCell (x : SortAccessedAccountsCell) : SortKItem
  | inj_SortAccessedStorageCell (x : SortAccessedStorageCell) : SortKItem
  | inj_SortAccount (x : SortAccount) : SortKItem
  | inj_SortAccountCell (x : SortAccountCell) : SortKItem
  | inj_SortAccountCellMap (x : SortAccountCellMap) : SortKItem
  | inj_SortAccountCode (x : SortAccountCode) : SortKItem
  | inj_SortAccounts (x : SortAccounts) : SortKItem
  | inj_SortAccountsCell (x : SortAccountsCell) : SortKItem
  | inj_SortAcctIDCell (x : SortAcctIDCell) : SortKItem
  | inj_SortBExp (x : SortBExp) : SortKItem
  | inj_SortBalanceCell (x : SortBalanceCell) : SortKItem
  | inj_SortBaseFeeCell (x : SortBaseFeeCell) : SortKItem
  | inj_SortBeaconRootCell (x : SortBeaconRootCell) : SortKItem
  | inj_SortBinStackOp (x : SortBinStackOp) : SortKItem
  | inj_SortBlobGasUsedCell (x : SortBlobGasUsedCell) : SortKItem
  | inj_SortBlockCell (x : SortBlockCell) : SortKItem
  | inj_SortBlockNonceCell (x : SortBlockNonceCell) : SortKItem
  | inj_SortBlockhashesCell (x : SortBlockhashesCell) : SortKItem
  | inj_SortBool (x : SortBool) : SortKItem
  | inj_SortBytes (x : SortBytes) : SortKItem
  | inj_SortCallDataCell (x : SortCallDataCell) : SortKItem
  | inj_SortCallDepthCell (x : SortCallDepthCell) : SortKItem
  | inj_SortCallGasCell (x : SortCallGasCell) : SortKItem
  | inj_SortCallOp (x : SortCallOp) : SortKItem
  | inj_SortCallSixOp (x : SortCallSixOp) : SortKItem
  | inj_SortCallStackCell (x : SortCallStackCell) : SortKItem
  | inj_SortCallStateCell (x : SortCallStateCell) : SortKItem
  | inj_SortCallValueCell (x : SortCallValueCell) : SortKItem
  | inj_SortCallerCell (x : SortCallerCell) : SortKItem
  | inj_SortChainIDCell (x : SortChainIDCell) : SortKItem
  | inj_SortCodeCell (x : SortCodeCell) : SortKItem
  | inj_SortCoinbaseCell (x : SortCoinbaseCell) : SortKItem
  | inj_SortDataCell (x : SortDataCell) : SortKItem
  | inj_SortDifficultyCell (x : SortDifficultyCell) : SortKItem
  | inj_SortDynamicFeeTx (x : SortDynamicFeeTx) : SortKItem
  | inj_SortEndStatusCode (x : SortEndStatusCode) : SortKItem
  | inj_SortEndianness (x : SortEndianness) : SortKItem
  | inj_SortEthereumCell (x : SortEthereumCell) : SortKItem
  | inj_SortEthereumCommand (x : SortEthereumCommand) : SortKItem
  | inj_SortEthereumSimulation (x : SortEthereumSimulation) : SortKItem
  | inj_SortEvmCell (x : SortEvmCell) : SortKItem
  | inj_SortExceptionalStatusCode (x : SortExceptionalStatusCode) : SortKItem
  | inj_SortExcessBlobGasCell (x : SortExcessBlobGasCell) : SortKItem
  | inj_SortExitCodeCell (x : SortExitCodeCell) : SortKItem
  | inj_SortExp (x : SortExp) : SortKItem
  | inj_SortExtraDataCell (x : SortExtraDataCell) : SortKItem
  | inj_SortG1Point (x : SortG1Point) : SortKItem
  | inj_SortG2Point (x : SortG2Point) : SortKItem
  | inj_SortGas (x : SortGas) : SortKItem
  | inj_SortGasCell (x : SortGasCell) : SortKItem
  | inj_SortGasLimitCell (x : SortGasLimitCell) : SortKItem
  | inj_SortGasPriceCell (x : SortGasPriceCell) : SortKItem
  | inj_SortGasUsedCell (x : SortGasUsedCell) : SortKItem
  | inj_SortGeneratedCounterCell (x : SortGeneratedCounterCell) : SortKItem
  | inj_SortGeneratedTopCell (x : SortGeneratedTopCell) : SortKItem
  | inj_SortIdCell (x : SortIdCell) : SortKItem
  | inj_SortInt (x : SortInt) : SortKItem
  | inj_SortInterimStatesCell (x : SortInterimStatesCell) : SortKItem
  | inj_SortInternalOp (x : SortInternalOp) : SortKItem
  | inj_SortInvalidOp (x : SortInvalidOp) : SortKItem
  | inj_SortJSON (x : SortJSON) : SortKItem
  | inj_SortJSONKey (x : SortJSONKey) : SortKItem
  | inj_SortJSONs (x : SortJSONs) : SortKItem
  | inj_SortJumpDestsCell (x : SortJumpDestsCell) : SortKItem
  | inj_SortKCell (x : SortKCell) : SortKItem
  | inj_SortKevmCell (x : SortKevmCell) : SortKItem
  | inj_SortLegacyTx (x : SortLegacyTx) : SortKItem
  | inj_SortLengthPrefix (x : SortLengthPrefix) : SortKItem
  | inj_SortLengthPrefixType (x : SortLengthPrefixType) : SortKItem
  | inj_SortList (x : SortList) : SortKItem
  | inj_SortLocalMemCell (x : SortLocalMemCell) : SortKItem
  | inj_SortLogCell (x : SortLogCell) : SortKItem
  | inj_SortLogOp (x : SortLogOp) : SortKItem
  | inj_SortLogsBloomCell (x : SortLogsBloomCell) : SortKItem
  | inj_SortMap (x : SortMap) : SortKItem
  | inj_SortMaybeOpCode (x : SortMaybeOpCode) : SortKItem
  | inj_SortMemoryUsedCell (x : SortMemoryUsedCell) : SortKItem
  | inj_SortMessageCell (x : SortMessageCell) : SortKItem
  | inj_SortMessageCellMap (x : SortMessageCellMap) : SortKItem
  | inj_SortMessagesCell (x : SortMessagesCell) : SortKItem
  | inj_SortMixHashCell (x : SortMixHashCell) : SortKItem
  | inj_SortMode (x : SortMode) : SortKItem
  | inj_SortModeCell (x : SortModeCell) : SortKItem
  | inj_SortMsgIDCell (x : SortMsgIDCell) : SortKItem
  | inj_SortNetworkCell (x : SortNetworkCell) : SortKItem
  | inj_SortNonceCell (x : SortNonceCell) : SortKItem
  | inj_SortNullStackOp (x : SortNullStackOp) : SortKItem
  | inj_SortNumberCell (x : SortNumberCell) : SortKItem
  | inj_SortOmmerBlockHeadersCell (x : SortOmmerBlockHeadersCell) : SortKItem
  | inj_SortOmmersHashCell (x : SortOmmersHashCell) : SortKItem
  | inj_SortOpCode (x : SortOpCode) : SortKItem
  | inj_SortOpCodes (x : SortOpCodes) : SortKItem
  | inj_SortOrigStorageCell (x : SortOrigStorageCell) : SortKItem
  | inj_SortOriginCell (x : SortOriginCell) : SortKItem
  | inj_SortOutputCell (x : SortOutputCell) : SortKItem
  | inj_SortPcCell (x : SortPcCell) : SortKItem
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortKItem
  | inj_SortPreviousHashCell (x : SortPreviousHashCell) : SortKItem
  | inj_SortProgramCell (x : SortProgramCell) : SortKItem
  | inj_SortPushOp (x : SortPushOp) : SortKItem
  | inj_SortQuadStackOp (x : SortQuadStackOp) : SortKItem
  | inj_SortReceiptsRootCell (x : SortReceiptsRootCell) : SortKItem
  | inj_SortRefundCell (x : SortRefundCell) : SortKItem
  | inj_SortSchedule (x : SortSchedule) : SortKItem
  | inj_SortScheduleCell (x : SortScheduleCell) : SortKItem
  | inj_SortScheduleConst (x : SortScheduleConst) : SortKItem
  | inj_SortScheduleFlag (x : SortScheduleFlag) : SortKItem
  | inj_SortSelfDestructCell (x : SortSelfDestructCell) : SortKItem
  | inj_SortSet (x : SortSet) : SortKItem
  | inj_SortSigRCell (x : SortSigRCell) : SortKItem
  | inj_SortSigSCell (x : SortSigSCell) : SortKItem
  | inj_SortSigVCell (x : SortSigVCell) : SortKItem
  | inj_SortSignedness (x : SortSignedness) : SortKItem
  | inj_SortStackOp (x : SortStackOp) : SortKItem
  | inj_SortStateRootCell (x : SortStateRootCell) : SortKItem
  | inj_SortStaticCell (x : SortStaticCell) : SortKItem
  | inj_SortStatusCode (x : SortStatusCode) : SortKItem
  | inj_SortStatusCodeCell (x : SortStatusCodeCell) : SortKItem
  | inj_SortStorageCell (x : SortStorageCell) : SortKItem
  | inj_SortString (x : SortString) : SortKItem
  | inj_SortStringBuffer (x : SortStringBuffer) : SortKItem
  | inj_SortSubstateCell (x : SortSubstateCell) : SortKItem
  | inj_SortSubstateLogEntry (x : SortSubstateLogEntry) : SortKItem
  | inj_SortTernStackOp (x : SortTernStackOp) : SortKItem
  | inj_SortTimestampCell (x : SortTimestampCell) : SortKItem
  | inj_SortToCell (x : SortToCell) : SortKItem
  | inj_SortTouchedAccountsCell (x : SortTouchedAccountsCell) : SortKItem
  | inj_SortTransactionsRootCell (x : SortTransactionsRootCell) : SortKItem
  | inj_SortTransientStorageCell (x : SortTransientStorageCell) : SortKItem
  | inj_SortTxAccessCell (x : SortTxAccessCell) : SortKItem
  | inj_SortTxChainIDCell (x : SortTxChainIDCell) : SortKItem
  | inj_SortTxData (x : SortTxData) : SortKItem
  | inj_SortTxGasLimitCell (x : SortTxGasLimitCell) : SortKItem
  | inj_SortTxGasPriceCell (x : SortTxGasPriceCell) : SortKItem
  | inj_SortTxMaxFeeCell (x : SortTxMaxFeeCell) : SortKItem
  | inj_SortTxNonceCell (x : SortTxNonceCell) : SortKItem
  | inj_SortTxOrderCell (x : SortTxOrderCell) : SortKItem
  | inj_SortTxPendingCell (x : SortTxPendingCell) : SortKItem
  | inj_SortTxPriorityFeeCell (x : SortTxPriorityFeeCell) : SortKItem
  | inj_SortTxType (x : SortTxType) : SortKItem
  | inj_SortTxTypeCell (x : SortTxTypeCell) : SortKItem
  | inj_SortUnStackOp (x : SortUnStackOp) : SortKItem
  | inj_SortUseGasCell (x : SortUseGasCell) : SortKItem
  | inj_SortValueCell (x : SortValueCell) : SortKItem
  | inj_SortWithdrawalsRootCell (x : SortWithdrawalsRootCell) : SortKItem
  | inj_SortWordStack (x : SortWordStack) : SortKItem
  | inj_SortWordStackCell (x : SortWordStackCell) : SortKItem
  | «#accessAccounts__EVM_KItem_Account» (x0 : SortAccount) : SortKItem
  | «#accessAccounts__EVM_KItem_Set» (x0 : SortSet) : SortKItem
  | «#accessAccounts___EVM_KItem_Account_Account» (x0 : SortAccount) (x1 : SortAccount) : SortKItem
  | «#accessAccounts____EVM_KItem_Account_Account_Set» (x0 : SortAccount) (x1 : SortAccount) (x2 : SortSet) : SortKItem
  | «#accessStorage___EVM_KItem_Account_Int» (x0 : SortAccount) (x1 : SortInt) : SortKItem
  | «#codeDeposit__EVM_KItem_Int» (x0 : SortInt) : SortKItem
  | «#finishCodeDeposit___EVM_KItem_Int_Bytes» (x0 : SortInt) (x1 : SortBytes) : SortKItem
  | «#freezerCcall1_» (x0 : SortK) (x1 : SortK) (x2 : SortK) (x3 : SortK) (x4 : SortK) : SortKItem
  | «#freezerCcallgas1_» (x0 : SortK) (x1 : SortK) (x2 : SortK) (x3 : SortK) (x4 : SortK) : SortKItem
  | «#freezerCselfdestruct1_» (x0 : SortK) (x1 : SortK) : SortKItem
  | «#initVM_EVM_KItem» : SortKItem
  | «#mkCodeDeposit__EVM_KItem_Int» (x0 : SortInt) : SortKItem
  | «#return___EVM_KItem_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortKItem
  | «#touchAccounts__EVM_KItem_Account» (x0 : SortAccount) : SortKItem
  | «#touchAccounts___EVM_KItem_Account_Account» (x0 : SortAccount) (x1 : SortAccount) : SortKItem
  | end (x0 : SortStatusCode) : SortKItem
  | execute : SortKItem
  | halt : SortKItem
  | «loadCallState__STATE-UTILS_KItem_JSON» (x0 : SortJSON) : SortKItem
  | loadProgram (x0 : SortBytes) : SortKItem

inductive SortLegacyTx : Type where
  | LegacySignedTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortAccount) (x4 : SortInt) (x5 : SortBytes) (x6 : SortInt) : SortLegacyTx
  | LegacyTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortAccount) (x4 : SortInt) (x5 : SortBytes) : SortLegacyTx

inductive SortLengthPrefix : Type where
  | «_(_,_)_SERIALIZATION_LengthPrefix_LengthPrefixType_Int_Int» (x0 : SortLengthPrefixType) (x1 : SortInt) (x2 : SortInt) : SortLengthPrefix

inductive SortLengthPrefixType : Type where
  | «#list_SERIALIZATION_LengthPrefixType» : SortLengthPrefixType
  | «#str_SERIALIZATION_LengthPrefixType» : SortLengthPrefixType

inductive SortLogOp : Type where
  | LOG (x0 : SortInt) : SortLogOp

inductive SortMaybeOpCode : Type where
  | inj_SortBinStackOp (x : SortBinStackOp) : SortMaybeOpCode
  | inj_SortCallOp (x : SortCallOp) : SortMaybeOpCode
  | inj_SortCallSixOp (x : SortCallSixOp) : SortMaybeOpCode
  | inj_SortInternalOp (x : SortInternalOp) : SortMaybeOpCode
  | inj_SortInvalidOp (x : SortInvalidOp) : SortMaybeOpCode
  | inj_SortLogOp (x : SortLogOp) : SortMaybeOpCode
  | inj_SortNullStackOp (x : SortNullStackOp) : SortMaybeOpCode
  | inj_SortOpCode (x : SortOpCode) : SortMaybeOpCode
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortMaybeOpCode
  | inj_SortPushOp (x : SortPushOp) : SortMaybeOpCode
  | inj_SortQuadStackOp (x : SortQuadStackOp) : SortMaybeOpCode
  | inj_SortStackOp (x : SortStackOp) : SortMaybeOpCode
  | inj_SortTernStackOp (x : SortTernStackOp) : SortMaybeOpCode
  | inj_SortUnStackOp (x : SortUnStackOp) : SortMaybeOpCode
  | «.NoOpCode_EVM_MaybeOpCode» : SortMaybeOpCode

inductive SortMode : Type where
  | NORMAL : SortMode
  | «SUCCESS_ETHEREUM-SIMULATION_Mode» : SortMode
  | VMTESTS : SortMode

inductive SortNullStackOp : Type where
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortNullStackOp
  | ADDRESS_EVM_NullStackOp : SortNullStackOp
  | BASEFEE_EVM_NullStackOp : SortNullStackOp
  | CALLDATASIZE_EVM_NullStackOp : SortNullStackOp
  | CALLER_EVM_NullStackOp : SortNullStackOp
  | CALLVALUE_EVM_NullStackOp : SortNullStackOp
  | CHAINID_EVM_NullStackOp : SortNullStackOp
  | CODESIZE_EVM_NullStackOp : SortNullStackOp
  | COINBASE_EVM_NullStackOp : SortNullStackOp
  | DIFFICULTY_EVM_NullStackOp : SortNullStackOp
  | GAS_EVM_NullStackOp : SortNullStackOp
  | GASLIMIT_EVM_NullStackOp : SortNullStackOp
  | GASPRICE_EVM_NullStackOp : SortNullStackOp
  | JUMPDEST_EVM_NullStackOp : SortNullStackOp
  | MSIZE_EVM_NullStackOp : SortNullStackOp
  | NUMBER_EVM_NullStackOp : SortNullStackOp
  | ORIGIN_EVM_NullStackOp : SortNullStackOp
  | PC_EVM_NullStackOp : SortNullStackOp
  | PREVRANDAO_EVM_NullStackOp : SortNullStackOp
  | RETURNDATASIZE_EVM_NullStackOp : SortNullStackOp
  | SELFBALANCE_EVM_NullStackOp : SortNullStackOp
  | STOP_EVM_NullStackOp : SortNullStackOp
  | TIMESTAMP_EVM_NullStackOp : SortNullStackOp

inductive SortOpCode : Type where
  | inj_SortBinStackOp (x : SortBinStackOp) : SortOpCode
  | inj_SortCallOp (x : SortCallOp) : SortOpCode
  | inj_SortCallSixOp (x : SortCallSixOp) : SortOpCode
  | inj_SortInternalOp (x : SortInternalOp) : SortOpCode
  | inj_SortInvalidOp (x : SortInvalidOp) : SortOpCode
  | inj_SortLogOp (x : SortLogOp) : SortOpCode
  | inj_SortNullStackOp (x : SortNullStackOp) : SortOpCode
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortOpCode
  | inj_SortPushOp (x : SortPushOp) : SortOpCode
  | inj_SortQuadStackOp (x : SortQuadStackOp) : SortOpCode
  | inj_SortStackOp (x : SortStackOp) : SortOpCode
  | inj_SortTernStackOp (x : SortTernStackOp) : SortOpCode
  | inj_SortUnStackOp (x : SortUnStackOp) : SortOpCode
  | PUSHAsm (x0 : SortInt) (x1 : SortInt) : SortOpCode

inductive SortOpCodes : Type where
  | «.OpCodes_EVM-ASSEMBLY_OpCodes» : SortOpCodes
  | «_;__EVM-ASSEMBLY_OpCodes_OpCode_OpCodes» (x0 : SortOpCode) (x1 : SortOpCodes) : SortOpCodes

inductive SortPrecompiledOp : Type where
  | BLAKE2F_EVM_PrecompiledOp : SortPrecompiledOp
  | ECADD_EVM_PrecompiledOp : SortPrecompiledOp
  | ECMUL_EVM_PrecompiledOp : SortPrecompiledOp
  | ECPAIRING_EVM_PrecompiledOp : SortPrecompiledOp
  | ECREC_EVM_PrecompiledOp : SortPrecompiledOp
  | ID_EVM_PrecompiledOp : SortPrecompiledOp
  | MODEXP_EVM_PrecompiledOp : SortPrecompiledOp
  | RIP160_EVM_PrecompiledOp : SortPrecompiledOp
  | SHA256_EVM_PrecompiledOp : SortPrecompiledOp

inductive SortPushOp : Type where
  | PUSH (x0 : SortInt) : SortPushOp
  | PUSHZERO_EVM_PushOp : SortPushOp

inductive SortQuadStackOp : Type where
  | CREATE2_EVM_QuadStackOp : SortQuadStackOp
  | EXTCODECOPY_EVM_QuadStackOp : SortQuadStackOp

inductive SortSchedule : Type where
  | BERLIN_EVM : SortSchedule
  | BYZANTIUM_EVM : SortSchedule
  | CANCUN_EVM : SortSchedule
  | CONSTANTINOPLE_EVM : SortSchedule
  | DEFAULT_EVM : SortSchedule
  | FRONTIER_EVM : SortSchedule
  | HOMESTEAD_EVM : SortSchedule
  | ISTANBUL_EVM : SortSchedule
  | LONDON_EVM : SortSchedule
  | MERGE_EVM : SortSchedule
  | PETERSBURG_EVM : SortSchedule
  | SHANGHAI_EVM : SortSchedule
  | SPURIOUS_DRAGON_EVM : SortSchedule
  | TANGERINE_WHISTLE_EVM : SortSchedule

inductive SortScheduleConst : Type where
  | Gaccesslistaddress_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gaccessliststoragekey_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gbalance_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gbase_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gblockhash_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcall_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcallstipend_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcallvalue_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcodedeposit_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcoldaccountaccess_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcoldsload_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcopy_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcreate_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecadd_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecmul_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecpaircoeff_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecpairconst_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gexp_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gexpbyte_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gextcodecopy_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gextcodesize_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gfround_SCHEDULE_ScheduleConst : SortScheduleConst
  | Ghigh_SCHEDULE_ScheduleConst : SortScheduleConst
  | Ginitcodewordcost_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gjumpdest_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glog_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glogdata_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glogtopic_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glow_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gmemory_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gmid_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gnewaccount_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gquadcoeff_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gquaddivisor_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gselfdestruct_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsha3_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsha3word_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsload_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsstorereset_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsstoreset_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtransaction_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtxcreate_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtxdatanonzero_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtxdatazero_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gverylow_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gwarmstoragedirtystore_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gwarmstorageread_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gzero_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rb_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rmaxquotient_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rselfdestruct_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rsstoreclear_SCHEDULE_ScheduleConst : SortScheduleConst
  | maxCodeSize_SCHEDULE_ScheduleConst : SortScheduleConst
  | maxInitCodeSize_SCHEDULE_ScheduleConst : SortScheduleConst

inductive SortScheduleFlag : Type where
  | Gemptyisnonexistent_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasaccesslist_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasbasefee_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasbeaconroot_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghaschainid_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghascreate2_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasdirtysstore_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasextcodehash_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasmaxinitcodesize_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasmcopy_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasprevrandao_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghaspushzero_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasrejectedfirstbyte_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasreturndata_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasrevert_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasselfbalance_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasshift_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghassstorestipend_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasstaticcall_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghastransient_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghaswarmcoinbase_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Gselfdestructnewaccount_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Gstaticcalldepth_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Gzerovaluenewaccountgas_SCHEDULE_ScheduleFlag : SortScheduleFlag

inductive SortSignedness : Type where
  | signedBytes : SortSignedness
  | unsignedBytes : SortSignedness

inductive SortStackOp : Type where
  | DUP (x0 : SortInt) : SortStackOp
  | SWAP (x0 : SortInt) : SortStackOp

inductive SortStatusCode : Type where
  | inj_SortEndStatusCode (x : SortEndStatusCode) : SortStatusCode
  | inj_SortExceptionalStatusCode (x : SortExceptionalStatusCode) : SortStatusCode
  | «.StatusCode_NETWORK_StatusCode» : SortStatusCode
  | EVMC_INTERNAL_ERROR_NETWORK_StatusCode : SortStatusCode
  | EVMC_REJECTED_NETWORK_StatusCode : SortStatusCode

inductive SortSubstateLogEntry : Type where
  | logEntry (x0 : SortInt) (x1 : SortList) (x2 : SortBytes) : SortSubstateLogEntry

inductive SortTernStackOp : Type where
  | ADDMOD_EVM_TernStackOp : SortTernStackOp
  | CALLDATACOPY_EVM_TernStackOp : SortTernStackOp
  | CODECOPY_EVM_TernStackOp : SortTernStackOp
  | CREATE_EVM_TernStackOp : SortTernStackOp
  | MCOPY_EVM_TernStackOp : SortTernStackOp
  | MULMOD_EVM_TernStackOp : SortTernStackOp
  | RETURNDATACOPY_EVM_TernStackOp : SortTernStackOp

inductive SortTxData : Type where
  | inj_SortAccessListTx (x : SortAccessListTx) : SortTxData
  | inj_SortDynamicFeeTx (x : SortDynamicFeeTx) : SortTxData
  | inj_SortLegacyTx (x : SortLegacyTx) : SortTxData

inductive SortTxType : Type where
  | «.TxType_EVM-TYPES_TxType» : SortTxType
  | «AccessList_EVM-TYPES_TxType» : SortTxType
  | «DynamicFee_EVM-TYPES_TxType» : SortTxType
  | «Legacy_EVM-TYPES_TxType» : SortTxType

inductive SortUnStackOp : Type where
  | BALANCE_EVM_UnStackOp : SortUnStackOp
  | BLOCKHASH_EVM_UnStackOp : SortUnStackOp
  | CALLDATALOAD_EVM_UnStackOp : SortUnStackOp
  | EXTCODEHASH_EVM_UnStackOp : SortUnStackOp
  | EXTCODESIZE_EVM_UnStackOp : SortUnStackOp
  | ISZERO_EVM_UnStackOp : SortUnStackOp
  | JUMP_EVM_UnStackOp : SortUnStackOp
  | MLOAD_EVM_UnStackOp : SortUnStackOp
  | NOT_EVM_UnStackOp : SortUnStackOp
  | POP_EVM_UnStackOp : SortUnStackOp
  | SELFDESTRUCT_EVM_UnStackOp : SortUnStackOp
  | SLOAD_EVM_UnStackOp : SortUnStackOp
  | TLOAD_EVM_UnStackOp : SortUnStackOp

inductive SortWordStack : Type where
  | «.WordStack_EVM-TYPES_WordStack» : SortWordStack
  | «_:__EVM-TYPES_WordStack_Int_WordStack» (x0 : SortInt) (x1 : SortWordStack) : SortWordStack

inductive SortBalanceCell : Type where
  | mk (val : SortInt) : SortBalanceCell

inductive SortIdCell : Type where
  | mk (val : SortAccount) : SortIdCell

inductive SortCoinbaseCell : Type where
  | mk (val : SortInt) : SortCoinbaseCell

inductive SortBlockNonceCell : Type where
  | mk (val : SortInt) : SortBlockNonceCell

inductive SortTransientStorageCell : Type where
  | mk (val : SortMap) : SortTransientStorageCell

inductive SortTimestampCell : Type where
  | mk (val : SortInt) : SortTimestampCell

inductive SortStatusCodeCell : Type where
  | mk (val : SortStatusCode) : SortStatusCodeCell

inductive SortMessagesCell : Type where
  | mk (val : SortMessageCellMap) : SortMessagesCell

inductive SortScheduleCell : Type where
  | mk (val : SortSchedule) : SortScheduleCell

inductive SortPreviousHashCell : Type where
  | mk (val : SortInt) : SortPreviousHashCell

inductive SortCodeCell : Type where
  | mk (val : SortAccountCode) : SortCodeCell

inductive SortTxOrderCell : Type where
  | mk (val : SortList) : SortTxOrderCell

inductive SortOrigStorageCell : Type where
  | mk (val : SortMap) : SortOrigStorageCell

inductive SortStaticCell : Type where
  | mk (val : SortBool) : SortStaticCell

inductive SortKCell : Type where
  | mk (val : SortK) : SortKCell

inductive SortExitCodeCell : Type where
  | mk (val : SortInt) : SortExitCodeCell

inductive SortModeCell : Type where
  | mk (val : SortMode) : SortModeCell

inductive SortUseGasCell : Type where
  | mk (val : SortBool) : SortUseGasCell

inductive SortOmmersHashCell : Type where
  | mk (val : SortInt) : SortOmmersHashCell

inductive SortStateRootCell : Type where
  | mk (val : SortInt) : SortStateRootCell

inductive SortTransactionsRootCell : Type where
  | mk (val : SortInt) : SortTransactionsRootCell

inductive SortReceiptsRootCell : Type where
  | mk (val : SortInt) : SortReceiptsRootCell

inductive SortLogsBloomCell : Type where
  | mk (val : SortBytes) : SortLogsBloomCell

inductive SortDifficultyCell : Type where
  | mk (val : SortInt) : SortDifficultyCell

inductive SortNumberCell : Type where
  | mk (val : SortInt) : SortNumberCell

inductive SortGasLimitCell : Type where
  | mk (val : SortInt) : SortGasLimitCell

inductive SortGasUsedCell : Type where
  | mk (val : SortGas) : SortGasUsedCell

inductive SortExtraDataCell : Type where
  | mk (val : SortBytes) : SortExtraDataCell

inductive SortMixHashCell : Type where
  | mk (val : SortInt) : SortMixHashCell

inductive SortBaseFeeCell : Type where
  | mk (val : SortInt) : SortBaseFeeCell

inductive SortWithdrawalsRootCell : Type where
  | mk (val : SortInt) : SortWithdrawalsRootCell

inductive SortBlobGasUsedCell : Type where
  | mk (val : SortInt) : SortBlobGasUsedCell

inductive SortExcessBlobGasCell : Type where
  | mk (val : SortInt) : SortExcessBlobGasCell

inductive SortBeaconRootCell : Type where
  | mk (val : SortInt) : SortBeaconRootCell

inductive SortOmmerBlockHeadersCell : Type where
  | mk (val : SortJSON) : SortOmmerBlockHeadersCell

inductive SortValueCell : Type where
  | mk (val : SortInt) : SortValueCell

inductive SortRefundCell : Type where
  | mk (val : SortInt) : SortRefundCell

inductive SortOutputCell : Type where
  | mk (val : SortBytes) : SortOutputCell

inductive SortCallStackCell : Type where
  | mk (val : SortList) : SortCallStackCell

inductive SortInterimStatesCell : Type where
  | mk (val : SortList) : SortInterimStatesCell

inductive SortTouchedAccountsCell : Type where
  | mk (val : SortSet) : SortTouchedAccountsCell

inductive SortGasPriceCell : Type where
  | mk (val : SortInt) : SortGasPriceCell

inductive SortOriginCell : Type where
  | mk (val : SortAccount) : SortOriginCell

inductive SortBlockhashesCell : Type where
  | mk (val : SortList) : SortBlockhashesCell

inductive SortCallDepthCell : Type where
  | mk (val : SortInt) : SortCallDepthCell

inductive SortToCell : Type where
  | mk (val : SortAccount) : SortToCell

inductive SortTxChainIDCell : Type where
  | mk (val : SortInt) : SortTxChainIDCell

inductive SortAcctIDCell : Type where
  | mk (val : SortInt) : SortAcctIDCell

inductive SortTxAccessCell : Type where
  | mk (val : SortJSON) : SortTxAccessCell

inductive SortStorageCell : Type where
  | mk (val : SortMap) : SortStorageCell

inductive SortProgramCell : Type where
  | mk (val : SortBytes) : SortProgramCell

inductive SortGeneratedCounterCell : Type where
  | mk (val : SortInt) : SortGeneratedCounterCell

inductive SortAccessedAccountsCell : Type where
  | mk (val : SortSet) : SortAccessedAccountsCell

inductive SortTxMaxFeeCell : Type where
  | mk (val : SortInt) : SortTxMaxFeeCell

inductive SortTxGasLimitCell : Type where
  | mk (val : SortInt) : SortTxGasLimitCell

inductive SortGasCell : Type where
  | mk (val : SortGas) : SortGasCell

inductive SortChainIDCell : Type where
  | mk (val : SortInt) : SortChainIDCell

inductive SortAccountsCell : Type where
  | mk (val : SortAccountCellMap) : SortAccountsCell

inductive SortTxPendingCell : Type where
  | mk (val : SortList) : SortTxPendingCell

inductive SortJumpDestsCell : Type where
  | mk (val : SortBytes) : SortJumpDestsCell

inductive SortSigSCell : Type where
  | mk (val : SortBytes) : SortSigSCell

inductive SortDataCell : Type where
  | mk (val : SortBytes) : SortDataCell

inductive SortTxNonceCell : Type where
  | mk (val : SortInt) : SortTxNonceCell

inductive SortPcCell : Type where
  | mk (val : SortInt) : SortPcCell

inductive SortTxTypeCell : Type where
  | mk (val : SortTxType) : SortTxTypeCell

inductive SortSelfDestructCell : Type where
  | mk (val : SortSet) : SortSelfDestructCell

inductive SortLogCell : Type where
  | mk (val : SortList) : SortLogCell

inductive SortAccessedStorageCell : Type where
  | mk (val : SortMap) : SortAccessedStorageCell

inductive SortCallDataCell : Type where
  | mk (val : SortBytes) : SortCallDataCell

inductive SortMsgIDCell : Type where
  | mk (val : SortInt) : SortMsgIDCell

inductive SortTxGasPriceCell : Type where
  | mk (val : SortInt) : SortTxGasPriceCell

inductive SortSigVCell : Type where
  | mk (val : SortInt) : SortSigVCell

inductive SortSigRCell : Type where
  | mk (val : SortBytes) : SortSigRCell

inductive SortTxPriorityFeeCell : Type where
  | mk (val : SortInt) : SortTxPriorityFeeCell

inductive SortCallerCell : Type where
  | mk (val : SortAccount) : SortCallerCell

inductive SortCallValueCell : Type where
  | mk (val : SortInt) : SortCallValueCell

inductive SortWordStackCell : Type where
  | mk (val : SortWordStack) : SortWordStackCell

inductive SortLocalMemCell : Type where
  | mk (val : SortBytes) : SortLocalMemCell

inductive SortMemoryUsedCell : Type where
  | mk (val : SortInt) : SortMemoryUsedCell

inductive SortCallGasCell : Type where
  | mk (val : SortGas) : SortCallGasCell

inductive SortNonceCell : Type where
  | mk (val : SortInt) : SortNonceCell

structure SortBlockCell : Type where
  previousHash : SortPreviousHashCell
  ommersHash : SortOmmersHashCell
  coinbase : SortCoinbaseCell
  stateRoot : SortStateRootCell
  transactionsRoot : SortTransactionsRootCell
  receiptsRoot : SortReceiptsRootCell
  logsBloom : SortLogsBloomCell
  difficulty : SortDifficultyCell
  number : SortNumberCell
  gasLimit : SortGasLimitCell
  gasUsed : SortGasUsedCell
  timestamp : SortTimestampCell
  extraData : SortExtraDataCell
  mixHash : SortMixHashCell
  blockNonce : SortBlockNonceCell
  baseFee : SortBaseFeeCell
  withdrawalsRoot : SortWithdrawalsRootCell
  blobGasUsed : SortBlobGasUsedCell
  excessBlobGas : SortExcessBlobGasCell
  beaconRoot : SortBeaconRootCell
  ommerBlockHeaders : SortOmmerBlockHeadersCell

structure SortNetworkCell : Type where
  chainID : SortChainIDCell
  accounts : SortAccountsCell
  txOrder : SortTxOrderCell
  txPending : SortTxPendingCell
  messages : SortMessagesCell

structure SortSubstateCell : Type where
  selfDestruct : SortSelfDestructCell
  log : SortLogCell
  refund : SortRefundCell
  accessedAccounts : SortAccessedAccountsCell
  accessedStorage : SortAccessedStorageCell

structure SortMessageCell : Type where
  msgID : SortMsgIDCell
  txNonce : SortTxNonceCell
  txGasPrice : SortTxGasPriceCell
  txGasLimit : SortTxGasLimitCell
  to : SortToCell
  value : SortValueCell
  sigV : SortSigVCell
  sigR : SortSigRCell
  sigS : SortSigSCell
  data : SortDataCell
  txAccess : SortTxAccessCell
  txChainID : SortTxChainIDCell
  txPriorityFee : SortTxPriorityFeeCell
  txMaxFee : SortTxMaxFeeCell
  txType : SortTxTypeCell

structure SortCallStateCell : Type where
  program : SortProgramCell
  jumpDests : SortJumpDestsCell
  id : SortIdCell
  caller : SortCallerCell
  callData : SortCallDataCell
  callValue : SortCallValueCell
  wordStack : SortWordStackCell
  localMem : SortLocalMemCell
  pc : SortPcCell
  gas : SortGasCell
  memoryUsed : SortMemoryUsedCell
  callGas : SortCallGasCell
  static : SortStaticCell
  callDepth : SortCallDepthCell

structure SortAccountCell : Type where
  acctID : SortAcctIDCell
  balance : SortBalanceCell
  code : SortCodeCell
  storage : SortStorageCell
  origStorage : SortOrigStorageCell
  transientStorage : SortTransientStorageCell
  nonce : SortNonceCell

structure SortEvmCell : Type where
  output : SortOutputCell
  statusCode : SortStatusCodeCell
  callStack : SortCallStackCell
  interimStates : SortInterimStatesCell
  touchedAccounts : SortTouchedAccountsCell
  callState : SortCallStateCell
  substate : SortSubstateCell
  gasPrice : SortGasPriceCell
  origin : SortOriginCell
  blockhashes : SortBlockhashesCell
  block : SortBlockCell

structure SortEthereumCell : Type where
  evm : SortEvmCell
  network : SortNetworkCell

structure SortKevmCell : Type where
  k : SortKCell
  exitCode : SortExitCodeCell
  mode : SortModeCell
  schedule : SortScheduleCell
  useGas : SortUseGasCell
  ethereum : SortEthereumCell

structure SortGeneratedTopCell : Type where
  kevm : SortKevmCell
  generatedCounter : SortGeneratedCounterCell

abbrev SortAccountCellMap : Type := MapHook SortAcctIDCell SortAccountCell

abbrev SortList : Type := ListHook SortKItem

abbrev SortMap : Type := MapHook SortKItem SortKItem

abbrev SortMessageCellMap : Type := MapHook SortMsgIDCell SortMessageCell

abbrev SortSet : Type := SetHook SortKItem

tothtamas28
tothtamas28 commented Jan 9, 2025
View reviewed changes
pyk/src/pyk/k2lean4/k2lean4.py
assert len(param_sorts) == 1
(param_sort,) = param_sorts
ctor = Ctor('mk', Signature((ExplBinder(('val',), Term(param_sort)),), Term(sort)))
return Inductive(sort, Signature((), Term('Type')), ctors=(ctor,))
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There's some room for simplification here, we could just generate a def or an abbrev. I.e. instead of

inductive SortGasCell : Type where
  | mk (val : SortGas) : SortGasCell

just generate

abbrev SortGasCell : Type := SortGas

or even inline the definition.

The same can be done for sorts with a single subsort:

inductive SortGas : Type where
  | inj_SortInt (x : SortInt) : SortGas

becomes

abbrev SortGas : Type := SortInt

The challenge is ordering declarations in a way that Lean does not complain about undefined types.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is the disadvantage of also using structures for leaf cells? Making

inductive SortGasCell : Type where
  | mk (val : SortGas) : SortGasCell

into

structure SortGasCell : Type where
  val : SortGas

My intuition is that if some cells have different kinds of definitions, that can make it more difficult to deal with in general. Whereas if everything is a structure, you know you'll always be able to access cell contents in the same way ((sg : SortGasCell).val for instance)

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point, the generated projection is probably very useful in this case. I'll change it to a structure.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, now the program does not type check due to circular dependencies between definitions. I'll investigate further, but I might have to the this last commit.

Copy link
Contributor Author

@tothtamas28 tothtamas28 Jan 13, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Reverting, opened an issue:

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've rearranged the definitions with the SCCs as structures in a way that Lean type checks. It's mainly defining abbrevs as soon as they can be defined and swaping the order that some definitions were defined.

This type checks, but we still need a mutual definition to avoid spurious Prop variables in definitions. However, I think this means that we can safely add back the structures for SCC and then use them in mutual definitions like:

mutual
inductive foo : Type where
  | foo_ctor : baz → foo

structure baz : Type where
  baz_ctor : foo
end
Rearranged definition 
abbrev SortBool : Type := Int
abbrev SortBytes: Type := ByteArray
abbrev SortId : Type := String
abbrev SortInt : Type := Int
abbrev SortString : Type := String
abbrev SortStringBuffer : Type := String

abbrev ListHook (E : Type) : Type := List E
abbrev MapHook (K : Type) (V : Type) : Type := List (K × V)
abbrev SetHook (E : Type) : Type := List E


inductive SortAccessListTx : Type where
  | AccessListTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortAccount) (x4 : SortInt) (x5 : SortBytes) (x6 : SortInt) (x7 : SortJSONs) : SortAccessListTx

inductive SortAccount : Type where
  | inj_SortInt (x : SortInt) : SortAccount
  | «.Account_EVM-TYPES_Account» : SortAccount

inductive SortAccountCode : Type where
  | inj_SortBytes (x : SortBytes) : SortAccountCode

inductive SortAccounts : Type where
  | «{_|_}_EVM_Accounts_AccountsCell_SubstateCell» (x0 : SortAccountsCell) (x1 : SortSubstateCell) : SortAccounts

inductive SortBExp : Type where
  | inj_SortBool (x : SortBool) : SortBExp
  | «#accountNonexistent» (x0 : SortInt) : SortBExp

inductive SortBinStackOp : Type where
  | inj_SortLogOp (x : SortLogOp) : SortBinStackOp
  | ADD_EVM_BinStackOp : SortBinStackOp
  | AND_EVM_BinStackOp : SortBinStackOp
  | BYTE_EVM_BinStackOp : SortBinStackOp
  | DIV_EVM_BinStackOp : SortBinStackOp
  | EQ_EVM_BinStackOp : SortBinStackOp
  | EVMOR_EVM_BinStackOp : SortBinStackOp
  | EXP_EVM_BinStackOp : SortBinStackOp
  | GT_EVM_BinStackOp : SortBinStackOp
  | JUMPI_EVM_BinStackOp : SortBinStackOp
  | LT_EVM_BinStackOp : SortBinStackOp
  | MOD_EVM_BinStackOp : SortBinStackOp
  | MSTORE_EVM_BinStackOp : SortBinStackOp
  | MSTORE8_EVM_BinStackOp : SortBinStackOp
  | MUL_EVM_BinStackOp : SortBinStackOp
  | RETURN_EVM_BinStackOp : SortBinStackOp
  | REVERT_EVM_BinStackOp : SortBinStackOp
  | SAR_EVM_BinStackOp : SortBinStackOp
  | SDIV_EVM_BinStackOp : SortBinStackOp
  | SGT_EVM_BinStackOp : SortBinStackOp
  | SHA3_EVM_BinStackOp : SortBinStackOp
  | SHL_EVM_BinStackOp : SortBinStackOp
  | SHR_EVM_BinStackOp : SortBinStackOp
  | SIGNEXTEND_EVM_BinStackOp : SortBinStackOp
  | SLT_EVM_BinStackOp : SortBinStackOp
  | SMOD_EVM_BinStackOp : SortBinStackOp
  | SSTORE_EVM_BinStackOp : SortBinStackOp
  | SUB_EVM_BinStackOp : SortBinStackOp
  | TSTORE_EVM_BinStackOp : SortBinStackOp
  | XOR_EVM_BinStackOp : SortBinStackOp

inductive SortCallOp : Type where
  | CALL_EVM_CallOp : SortCallOp
  | CALLCODE_EVM_CallOp : SortCallOp

inductive SortCallSixOp : Type where
  | DELEGATECALL_EVM_CallSixOp : SortCallSixOp
  | STATICCALL_EVM_CallSixOp : SortCallSixOp

inductive SortDynamicFeeTx : Type where
  | DynamicFeeTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortAccount) (x5 : SortInt) (x6 : SortBytes) (x7 : SortInt) (x8 : SortJSONs) : SortDynamicFeeTx

inductive SortEndStatusCode : Type where
  | inj_SortExceptionalStatusCode (x : SortExceptionalStatusCode) : SortEndStatusCode
  | EVMC_REVERT_NETWORK_EndStatusCode : SortEndStatusCode
  | EVMC_SUCCESS_NETWORK_EndStatusCode : SortEndStatusCode

inductive SortEndianness : Type where
  | bigEndianBytes : SortEndianness

inductive SortEthereumCommand : Type where
  | «#executeBeaconRoots» : SortEthereumCommand
  | «#finalizeBlock_EVM_EthereumCommand» : SortEthereumCommand
  | «#finishTx_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «#loadAccessList» (x0 : SortJSON) : SortEthereumCommand
  | «#loadAccessListAux» (x0 : SortAccount) (x1 : SortList) : SortEthereumCommand
  | «#rewardOmmers» (x0 : SortJSONs) : SortEthereumCommand
  | «#startBlock_EVM_EthereumCommand» : SortEthereumCommand
  | «check__ETHEREUM-SIMULATION_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «clear_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «clearBLOCK_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «clearNETWORK_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «clearTX_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «exception_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «failure__ETHEREUM-SIMULATION_EthereumCommand_String» (x0 : SortString) : SortEthereumCommand
  | «flush_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «load__STATE-UTILS_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «loadAccount___STATE-UTILS_EthereumCommand_Int_JSON» (x0 : SortInt) (x1 : SortJSON) : SortEthereumCommand
  | «loadTransaction___STATE-UTILS_EthereumCommand_Int_JSON» (x0 : SortInt) (x1 : SortJSON) : SortEthereumCommand
  | loadTx (x0 : SortAccount) : SortEthereumCommand
  | «mkAcct__STATE-UTILS_EthereumCommand_Int» (x0 : SortInt) : SortEthereumCommand
  | «mkTX__STATE-UTILS_EthereumCommand_Int» (x0 : SortInt) : SortEthereumCommand
  | «process__ETHEREUM-SIMULATION_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «run__ETHEREUM-SIMULATION_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «start_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «startTx_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «status__ETHEREUM-SIMULATION_EthereumCommand_StatusCode» (x0 : SortStatusCode) : SortEthereumCommand
  | «success_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand

inductive SortEthereumSimulation : Type where
  | inj_SortAccount (x : SortAccount) : SortEthereumSimulation
  | inj_SortBool (x : SortBool) : SortEthereumSimulation
  | inj_SortBytes (x : SortBytes) : SortEthereumSimulation
  | inj_SortInt (x : SortInt) : SortEthereumSimulation
  | inj_SortJSON (x : SortJSON) : SortEthereumSimulation
  | inj_SortMap (x : SortMap) : SortEthereumSimulation
  | inj_SortOpCodes (x : SortOpCodes) : SortEthereumSimulation
  | inj_SortString (x : SortString) : SortEthereumSimulation
  | inj_SortSubstateLogEntry (x : SortSubstateLogEntry) : SortEthereumSimulation
  | inj_SortTxType (x : SortTxType) : SortEthereumSimulation
  | «.EthereumSimulation_ETHEREUM-SIMULATION_EthereumSimulation» : SortEthereumSimulation
  | «___ETHEREUM-SIMULATION_EthereumSimulation_EthereumCommand_EthereumSimulation» (x0 : SortEthereumCommand) (x1 : SortEthereumSimulation) : SortEthereumSimulation

inductive SortExceptionalStatusCode : Type where
  | EVMC_ACCOUNT_ALREADY_EXISTS_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_BAD_JUMP_DESTINATION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_BALANCE_UNDERFLOW_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_CALL_DEPTH_EXCEEDED_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_INVALID_INSTRUCTION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_INVALID_MEMORY_ACCESS_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_NONCE_EXCEEDED_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_OUT_OF_GAS_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_PRECOMPILE_FAILURE_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_STACK_OVERFLOW_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_STACK_UNDERFLOW_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_STATIC_MODE_VIOLATION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_UNDEFINED_INSTRUCTION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode

inductive SortExp : Type where
  | inj_SortGas (x : SortGas) : SortExp
  | inj_SortInt (x : SortInt) : SortExp
  | Ccall (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortGas) (x3 : SortGas) (x4 : SortInt) (x5 : SortBool) : SortExp
  | Ccallgas (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortGas) (x3 : SortGas) (x4 : SortInt) (x5 : SortBool) : SortExp
  | Cselfdestruct (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortInt) : SortExp

inductive SortG1Point : Type where
  | «(_,_)_KRYPTO_G1Point_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortG1Point

inductive SortG2Point : Type where
  | «(_x_,_x_)_KRYPTO_G2Point_Int_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : SortG2Point

inductive SortGas : Type where
  | inj_SortInt (x : SortInt) : SortGas

inductive SortInternalOp : Type where
  | «#access[_,_]_EVM_InternalOp_OpCode_OpCode» (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | «#addr[_]_EVM_InternalOp_OpCode» (x0 : SortOpCode) : SortInternalOp
  | «#allocateCallGas_EVM_InternalOp» : SortInternalOp
  | «#allocateCreateGas_EVM_InternalOp» : SortInternalOp
  | «#call________EVM_InternalOp_Int_Int_Int_Int_Int_Bytes_Bool» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortBytes) (x6 : SortBool) : SortInternalOp
  | «#callWithCode_________EVM_InternalOp_Int_Int_Int_Bytes_Int_Int_Bytes_Bool» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) (x5 : SortInt) (x6 : SortBytes) (x7 : SortBool) : SortInternalOp
  | «#checkBalanceUnderflow___EVM_InternalOp_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | «#checkCall___EVM_InternalOp_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | «#checkCreate___EVM_InternalOp_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | «#checkDepthExceeded_EVM_InternalOp» : SortInternalOp
  | «#checkNonceExceeded__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#checkPoint_EVM_InternalOp» : SortInternalOp
  | «#create_____EVM_InternalOp_Int_Int_Int_Bytes» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : SortInternalOp
  | «#deductGas_EVM_InternalOp» : SortInternalOp
  | «#deductMemory_EVM_InternalOp» : SortInternalOp
  | «#deductMemoryGas_EVM_InternalOp» : SortInternalOp
  | «#deleteAccounts» (x0 : SortList) : SortInternalOp
  | «#dropCallStack_EVM_InternalOp» : SortInternalOp
  | «#dropWorldState_EVM_InternalOp» : SortInternalOp
  | «#ecadd» (x0 : SortG1Point) (x1 : SortG1Point) : SortInternalOp
  | «#ecmul» (x0 : SortG1Point) (x1 : SortInt) : SortInternalOp
  | «#ecpairing» (x0 : SortList) (x1 : SortList) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) : SortInternalOp
  | «#endBasicBlock_EVM_InternalOp» : SortInternalOp
  | «#exec[_]_EVM_InternalOp_OpCode» (x0 : SortOpCode) : SortInternalOp
  | «#finalizeStorage» (x0 : SortList) : SortInternalOp
  | «#finalizeTx» (x0 : SortBool) : SortInternalOp
  | «#gas[_,_]_EVM_InternalOp_OpCode_OpCode» (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | «#gas[_]_EVM_InternalOp_OpCode» (x0 : SortOpCode) : SortInternalOp
  | «#gasAccess» (x0 : SortSchedule) (x1 : SortOpCode) : SortInternalOp
  | «#gasExec» (x0 : SortSchedule) (x1 : SortOpCode) : SortInternalOp
  | «#incrementNonce__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#memory[_,_]_EVM_InternalOp_OpCode_OpCode» (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | «#mkCall________EVM_InternalOp_Int_Int_Int_Bytes_Int_Bytes_Bool» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) (x5 : SortBytes) (x6 : SortBool) : SortInternalOp
  | «#mkCreate_____EVM_InternalOp_Int_Int_Int_Bytes» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : SortInternalOp
  | «#newAccount__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#newExistingAccount__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#next[_]_EVM_InternalOp_MaybeOpCode» (x0 : SortMaybeOpCode) : SortInternalOp
  | «#popCallStack_EVM_InternalOp» : SortInternalOp
  | «#popWorldState_EVM_InternalOp» : SortInternalOp
  | «#precompiled?(_,_)_EVM_InternalOp_Int_Schedule» (x0 : SortInt) (x1 : SortSchedule) : SortInternalOp
  | «#push_EVM_InternalOp» : SortInternalOp
  | «#pushCallStack_EVM_InternalOp» : SortInternalOp
  | «#pushWorldState_EVM_InternalOp» : SortInternalOp
  | «#refund__EVM_InternalOp_Gas» (x0 : SortGas) : SortInternalOp
  | «#setLocalMem____EVM_InternalOp_Int_Int_Bytes» (x0 : SortInt) (x1 : SortInt) (x2 : SortBytes) : SortInternalOp
  | «#setStack__EVM_InternalOp_WordStack» (x0 : SortWordStack) : SortInternalOp
  | «#transferFunds____EVM_InternalOp_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | «#transferFundsToNonExistent____EVM_InternalOp_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | ___EVM_InternalOp_StackOp_WordStack (x0 : SortStackOp) (x1 : SortWordStack) : SortInternalOp
  | ___EVM_InternalOp_UnStackOp_Int (x0 : SortUnStackOp) (x1 : SortInt) : SortInternalOp
  | ____EVM_InternalOp_BinStackOp_Int_Int (x0 : SortBinStackOp) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | _____EVM_InternalOp_TernStackOp_Int_Int_Int (x0 : SortTernStackOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : SortInternalOp
  | ______EVM_InternalOp_QuadStackOp_Int_Int_Int_Int (x0 : SortQuadStackOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) : SortInternalOp
  | ________EVM_InternalOp_CallSixOp_Int_Int_Int_Int_Int_Int (x0 : SortCallSixOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortInt) : SortInternalOp
  | _________EVM_InternalOp_CallOp_Int_Int_Int_Int_Int_Int_Int (x0 : SortCallOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortInt) (x7 : SortInt) : SortInternalOp
  | pc (x0 : SortOpCode) : SortInternalOp

inductive SortInvalidOp : Type where
  | INVALID_EVM_InvalidOp : SortInvalidOp
  | «UNDEFINED(_)_EVM_InvalidOp_Int» (x0 : SortInt) : SortInvalidOp

inductive SortJSON : Type where
  | inj_SortAccount (x : SortAccount) : SortJSON
  | inj_SortBool (x : SortBool) : SortJSON
  | inj_SortBytes (x : SortBytes) : SortJSON
  | inj_SortInt (x : SortInt) : SortJSON
  | inj_SortMap (x : SortMap) : SortJSON
  | inj_SortOpCodes (x : SortOpCodes) : SortJSON
  | inj_SortString (x : SortString) : SortJSON
  | inj_SortSubstateLogEntry (x : SortSubstateLogEntry) : SortJSON
  | inj_SortTxType (x : SortTxType) : SortJSON
  | JSONEntry (x0 : SortJSONKey) (x1 : SortJSON) : SortJSON
  | JSONList (x0 : SortJSONs) : SortJSON
  | JSONObject (x0 : SortJSONs) : SortJSON
  | JSONnull : SortJSON

inductive SortJSONKey : Type where
  | inj_SortInt (x : SortInt) : SortJSONKey
  | inj_SortString (x : SortString) : SortJSONKey

inductive SortJSONs : Type where
  | «.List{"JSONs"}» : SortJSONs
  | JSONs (x0 : SortJSON) (x1 : SortJSONs) : SortJSONs

inductive SortK : Type where
  | dotk : SortK
  | kseq (x0 : SortKItem) (x1 : SortK) : SortK

set_option maxHeartbeats 209000

inductive SortKItem : Type where
  | inj_SortAccessListTx (x : SortAccessListTx) : SortKItem
  | inj_SortAccessedAccountsCell (x : SortAccessedAccountsCell) : SortKItem
  | inj_SortAccessedStorageCell (x : SortAccessedStorageCell) : SortKItem
  | inj_SortAccount (x : SortAccount) : SortKItem
  | inj_SortAccountCell (x : SortAccountCell) : SortKItem
  | inj_SortAccountCellMap (x : SortAccountCellMap) : SortKItem
  | inj_SortAccountCode (x : SortAccountCode) : SortKItem
  | inj_SortAccounts (x : SortAccounts) : SortKItem
  | inj_SortAccountsCell (x : SortAccountsCell) : SortKItem
  | inj_SortAcctIDCell (x : SortAcctIDCell) : SortKItem
  | inj_SortBExp (x : SortBExp) : SortKItem
  | inj_SortBalanceCell (x : SortBalanceCell) : SortKItem
  | inj_SortBaseFeeCell (x : SortBaseFeeCell) : SortKItem
  | inj_SortBeaconRootCell (x : SortBeaconRootCell) : SortKItem
  | inj_SortBinStackOp (x : SortBinStackOp) : SortKItem
  | inj_SortBlobGasUsedCell (x : SortBlobGasUsedCell) : SortKItem
  | inj_SortBlockCell (x : SortBlockCell) : SortKItem
  | inj_SortBlockNonceCell (x : SortBlockNonceCell) : SortKItem
  | inj_SortBlockhashesCell (x : SortBlockhashesCell) : SortKItem
  | inj_SortBool (x : SortBool) : SortKItem
  | inj_SortBytes (x : SortBytes) : SortKItem
  | inj_SortCallDataCell (x : SortCallDataCell) : SortKItem
  | inj_SortCallDepthCell (x : SortCallDepthCell) : SortKItem
  | inj_SortCallGasCell (x : SortCallGasCell) : SortKItem
  | inj_SortCallOp (x : SortCallOp) : SortKItem
  | inj_SortCallSixOp (x : SortCallSixOp) : SortKItem
  | inj_SortCallStackCell (x : SortCallStackCell) : SortKItem
  | inj_SortCallStateCell (x : SortCallStateCell) : SortKItem
  | inj_SortCallValueCell (x : SortCallValueCell) : SortKItem
  | inj_SortCallerCell (x : SortCallerCell) : SortKItem
  | inj_SortChainIDCell (x : SortChainIDCell) : SortKItem
  | inj_SortCodeCell (x : SortCodeCell) : SortKItem
  | inj_SortCoinbaseCell (x : SortCoinbaseCell) : SortKItem
  | inj_SortDataCell (x : SortDataCell) : SortKItem
  | inj_SortDifficultyCell (x : SortDifficultyCell) : SortKItem
  | inj_SortDynamicFeeTx (x : SortDynamicFeeTx) : SortKItem
  | inj_SortEndStatusCode (x : SortEndStatusCode) : SortKItem
  | inj_SortEndianness (x : SortEndianness) : SortKItem
  | inj_SortEthereumCell (x : SortEthereumCell) : SortKItem
  | inj_SortEthereumCommand (x : SortEthereumCommand) : SortKItem
  | inj_SortEthereumSimulation (x : SortEthereumSimulation) : SortKItem
  | inj_SortEvmCell (x : SortEvmCell) : SortKItem
  | inj_SortExceptionalStatusCode (x : SortExceptionalStatusCode) : SortKItem
  | inj_SortExcessBlobGasCell (x : SortExcessBlobGasCell) : SortKItem
  | inj_SortExitCodeCell (x : SortExitCodeCell) : SortKItem
  | inj_SortExp (x : SortExp) : SortKItem
  | inj_SortExtraDataCell (x : SortExtraDataCell) : SortKItem
  | inj_SortG1Point (x : SortG1Point) : SortKItem
  | inj_SortG2Point (x : SortG2Point) : SortKItem
  | inj_SortGas (x : SortGas) : SortKItem
  | inj_SortGasCell (x : SortGasCell) : SortKItem
  | inj_SortGasLimitCell (x : SortGasLimitCell) : SortKItem
  | inj_SortGasPriceCell (x : SortGasPriceCell) : SortKItem
  | inj_SortGasUsedCell (x : SortGasUsedCell) : SortKItem
  | inj_SortGeneratedCounterCell (x : SortGeneratedCounterCell) : SortKItem
  | inj_SortGeneratedTopCell (x : SortGeneratedTopCell) : SortKItem
  | inj_SortIdCell (x : SortIdCell) : SortKItem
  | inj_SortInt (x : SortInt) : SortKItem
  | inj_SortInterimStatesCell (x : SortInterimStatesCell) : SortKItem
  | inj_SortInternalOp (x : SortInternalOp) : SortKItem
  | inj_SortInvalidOp (x : SortInvalidOp) : SortKItem
  | inj_SortJSON (x : SortJSON) : SortKItem
  | inj_SortJSONKey (x : SortJSONKey) : SortKItem
  | inj_SortJSONs (x : SortJSONs) : SortKItem
  | inj_SortJumpDestsCell (x : SortJumpDestsCell) : SortKItem
  | inj_SortKCell (x : SortKCell) : SortKItem
  | inj_SortKevmCell (x : SortKevmCell) : SortKItem
  | inj_SortLegacyTx (x : SortLegacyTx) : SortKItem
  | inj_SortLengthPrefix (x : SortLengthPrefix) : SortKItem
  | inj_SortLengthPrefixType (x : SortLengthPrefixType) : SortKItem
  | inj_SortList (x : SortList) : SortKItem
  | inj_SortLocalMemCell (x : SortLocalMemCell) : SortKItem
  | inj_SortLogCell (x : SortLogCell) : SortKItem
  | inj_SortLogOp (x : SortLogOp) : SortKItem
  | inj_SortLogsBloomCell (x : SortLogsBloomCell) : SortKItem
  | inj_SortMap (x : SortMap) : SortKItem
  | inj_SortMaybeOpCode (x : SortMaybeOpCode) : SortKItem
  | inj_SortMemoryUsedCell (x : SortMemoryUsedCell) : SortKItem
  | inj_SortMessageCell (x : SortMessageCell) : SortKItem
  | inj_SortMessageCellMap (x : SortMessageCellMap) : SortKItem
  | inj_SortMessagesCell (x : SortMessagesCell) : SortKItem
  | inj_SortMixHashCell (x : SortMixHashCell) : SortKItem
  | inj_SortMode (x : SortMode) : SortKItem
  | inj_SortModeCell (x : SortModeCell) : SortKItem
  | inj_SortMsgIDCell (x : SortMsgIDCell) : SortKItem
  | inj_SortNetworkCell (x : SortNetworkCell) : SortKItem
  | inj_SortNonceCell (x : SortNonceCell) : SortKItem
  | inj_SortNullStackOp (x : SortNullStackOp) : SortKItem
  | inj_SortNumberCell (x : SortNumberCell) : SortKItem
  | inj_SortOmmerBlockHeadersCell (x : SortOmmerBlockHeadersCell) : SortKItem
  | inj_SortOmmersHashCell (x : SortOmmersHashCell) : SortKItem
  | inj_SortOpCode (x : SortOpCode) : SortKItem
  | inj_SortOpCodes (x : SortOpCodes) : SortKItem
  | inj_SortOrigStorageCell (x : SortOrigStorageCell) : SortKItem
  | inj_SortOriginCell (x : SortOriginCell) : SortKItem
  | inj_SortOutputCell (x : SortOutputCell) : SortKItem
  | inj_SortPcCell (x : SortPcCell) : SortKItem
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortKItem
  | inj_SortPreviousHashCell (x : SortPreviousHashCell) : SortKItem
  | inj_SortProgramCell (x : SortProgramCell) : SortKItem
  | inj_SortPushOp (x : SortPushOp) : SortKItem
  | inj_SortQuadStackOp (x : SortQuadStackOp) : SortKItem
  | inj_SortReceiptsRootCell (x : SortReceiptsRootCell) : SortKItem
  | inj_SortRefundCell (x : SortRefundCell) : SortKItem
  | inj_SortSchedule (x : SortSchedule) : SortKItem
  | inj_SortScheduleCell (x : SortScheduleCell) : SortKItem
  | inj_SortScheduleConst (x : SortScheduleConst) : SortKItem
  | inj_SortScheduleFlag (x : SortScheduleFlag) : SortKItem
  | inj_SortSelfDestructCell (x : SortSelfDestructCell) : SortKItem
  | inj_SortSet (x : SortSet) : SortKItem
  | inj_SortSigRCell (x : SortSigRCell) : SortKItem
  | inj_SortSigSCell (x : SortSigSCell) : SortKItem
  | inj_SortSigVCell (x : SortSigVCell) : SortKItem
  | inj_SortSignedness (x : SortSignedness) : SortKItem
  | inj_SortStackOp (x : SortStackOp) : SortKItem
  | inj_SortStateRootCell (x : SortStateRootCell) : SortKItem
  | inj_SortStaticCell (x : SortStaticCell) : SortKItem
  | inj_SortStatusCode (x : SortStatusCode) : SortKItem
  | inj_SortStatusCodeCell (x : SortStatusCodeCell) : SortKItem
  | inj_SortStorageCell (x : SortStorageCell) : SortKItem
  | inj_SortString (x : SortString) : SortKItem
  | inj_SortStringBuffer (x : SortStringBuffer) : SortKItem
  | inj_SortSubstateCell (x : SortSubstateCell) : SortKItem
  | inj_SortSubstateLogEntry (x : SortSubstateLogEntry) : SortKItem
  | inj_SortTernStackOp (x : SortTernStackOp) : SortKItem
  | inj_SortTimestampCell (x : SortTimestampCell) : SortKItem
  | inj_SortToCell (x : SortToCell) : SortKItem
  | inj_SortTouchedAccountsCell (x : SortTouchedAccountsCell) : SortKItem
  | inj_SortTransactionsRootCell (x : SortTransactionsRootCell) : SortKItem
  | inj_SortTransientStorageCell (x : SortTransientStorageCell) : SortKItem
  | inj_SortTxAccessCell (x : SortTxAccessCell) : SortKItem
  | inj_SortTxChainIDCell (x : SortTxChainIDCell) : SortKItem
  | inj_SortTxData (x : SortTxData) : SortKItem
  | inj_SortTxGasLimitCell (x : SortTxGasLimitCell) : SortKItem
  | inj_SortTxGasPriceCell (x : SortTxGasPriceCell) : SortKItem
  | inj_SortTxMaxFeeCell (x : SortTxMaxFeeCell) : SortKItem
  | inj_SortTxNonceCell (x : SortTxNonceCell) : SortKItem
  | inj_SortTxOrderCell (x : SortTxOrderCell) : SortKItem
  | inj_SortTxPendingCell (x : SortTxPendingCell) : SortKItem
  | inj_SortTxPriorityFeeCell (x : SortTxPriorityFeeCell) : SortKItem
  | inj_SortTxType (x : SortTxType) : SortKItem
  | inj_SortTxTypeCell (x : SortTxTypeCell) : SortKItem
  | inj_SortUnStackOp (x : SortUnStackOp) : SortKItem
  | inj_SortUseGasCell (x : SortUseGasCell) : SortKItem
  | inj_SortValueCell (x : SortValueCell) : SortKItem
  | inj_SortWithdrawalsRootCell (x : SortWithdrawalsRootCell) : SortKItem
  | inj_SortWordStack (x : SortWordStack) : SortKItem
  | inj_SortWordStackCell (x : SortWordStackCell) : SortKItem
  | «#accessAccounts__EVM_KItem_Account» (x0 : SortAccount) : SortKItem
  | «#accessAccounts__EVM_KItem_Set» (x0 : SortSet) : SortKItem
  | «#accessAccounts___EVM_KItem_Account_Account» (x0 : SortAccount) (x1 : SortAccount) : SortKItem
  | «#accessAccounts____EVM_KItem_Account_Account_Set» (x0 : SortAccount) (x1 : SortAccount) (x2 : SortSet) : SortKItem
  | «#accessStorage___EVM_KItem_Account_Int» (x0 : SortAccount) (x1 : SortInt) : SortKItem
  | «#codeDeposit__EVM_KItem_Int» (x0 : SortInt) : SortKItem
  | «#finishCodeDeposit___EVM_KItem_Int_Bytes» (x0 : SortInt) (x1 : SortBytes) : SortKItem
  | «#freezerCcall1_» (x0 : SortK) (x1 : SortK) (x2 : SortK) (x3 : SortK) (x4 : SortK) : SortKItem
  | «#freezerCcallgas1_» (x0 : SortK) (x1 : SortK) (x2 : SortK) (x3 : SortK) (x4 : SortK) : SortKItem
  | «#freezerCselfdestruct1_» (x0 : SortK) (x1 : SortK) : SortKItem
  | «#initVM_EVM_KItem» : SortKItem
  | «#mkCodeDeposit__EVM_KItem_Int» (x0 : SortInt) : SortKItem
  | «#return___EVM_KItem_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortKItem
  | «#touchAccounts__EVM_KItem_Account» (x0 : SortAccount) : SortKItem
  | «#touchAccounts___EVM_KItem_Account_Account» (x0 : SortAccount) (x1 : SortAccount) : SortKItem
  | end (x0 : SortStatusCode) : SortKItem
  | execute : SortKItem
  | halt : SortKItem
  | «loadCallState__STATE-UTILS_KItem_JSON» (x0 : SortJSON) : SortKItem
  | loadProgram (x0 : SortBytes) : SortKItem

abbrev SortList : Type := ListHook SortKItem

abbrev SortMap : Type := MapHook SortKItem SortKItem

abbrev SortSet : Type := SetHook SortKItem

inductive SortLegacyTx : Type where
  | LegacySignedTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortAccount) (x4 : SortInt) (x5 : SortBytes) (x6 : SortInt) : SortLegacyTx
  | LegacyTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortAccount) (x4 : SortInt) (x5 : SortBytes) : SortLegacyTx

inductive SortLengthPrefix : Type where
  | «_(_,_)_SERIALIZATION_LengthPrefix_LengthPrefixType_Int_Int» (x0 : SortLengthPrefixType) (x1 : SortInt) (x2 : SortInt) : SortLengthPrefix

inductive SortLengthPrefixType : Type where
  | «#list_SERIALIZATION_LengthPrefixType» : SortLengthPrefixType
  | «#str_SERIALIZATION_LengthPrefixType» : SortLengthPrefixType

inductive SortLogOp : Type where
  | LOG (x0 : SortInt) : SortLogOp

inductive SortMaybeOpCode : Type where
  | inj_SortBinStackOp (x : SortBinStackOp) : SortMaybeOpCode
  | inj_SortCallOp (x : SortCallOp) : SortMaybeOpCode
  | inj_SortCallSixOp (x : SortCallSixOp) : SortMaybeOpCode
  | inj_SortInternalOp (x : SortInternalOp) : SortMaybeOpCode
  | inj_SortInvalidOp (x : SortInvalidOp) : SortMaybeOpCode
  | inj_SortLogOp (x : SortLogOp) : SortMaybeOpCode
  | inj_SortNullStackOp (x : SortNullStackOp) : SortMaybeOpCode
  | inj_SortOpCode (x : SortOpCode) : SortMaybeOpCode
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortMaybeOpCode
  | inj_SortPushOp (x : SortPushOp) : SortMaybeOpCode
  | inj_SortQuadStackOp (x : SortQuadStackOp) : SortMaybeOpCode
  | inj_SortStackOp (x : SortStackOp) : SortMaybeOpCode
  | inj_SortTernStackOp (x : SortTernStackOp) : SortMaybeOpCode
  | inj_SortUnStackOp (x : SortUnStackOp) : SortMaybeOpCode
  | «.NoOpCode_EVM_MaybeOpCode» : SortMaybeOpCode

inductive SortMode : Type where
  | NORMAL : SortMode
  | «SUCCESS_ETHEREUM-SIMULATION_Mode» : SortMode
  | VMTESTS : SortMode

inductive SortNullStackOp : Type where
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortNullStackOp
  | ADDRESS_EVM_NullStackOp : SortNullStackOp
  | BASEFEE_EVM_NullStackOp : SortNullStackOp
  | CALLDATASIZE_EVM_NullStackOp : SortNullStackOp
  | CALLER_EVM_NullStackOp : SortNullStackOp
  | CALLVALUE_EVM_NullStackOp : SortNullStackOp
  | CHAINID_EVM_NullStackOp : SortNullStackOp
  | CODESIZE_EVM_NullStackOp : SortNullStackOp
  | COINBASE_EVM_NullStackOp : SortNullStackOp
  | DIFFICULTY_EVM_NullStackOp : SortNullStackOp
  | GAS_EVM_NullStackOp : SortNullStackOp
  | GASLIMIT_EVM_NullStackOp : SortNullStackOp
  | GASPRICE_EVM_NullStackOp : SortNullStackOp
  | JUMPDEST_EVM_NullStackOp : SortNullStackOp
  | MSIZE_EVM_NullStackOp : SortNullStackOp
  | NUMBER_EVM_NullStackOp : SortNullStackOp
  | ORIGIN_EVM_NullStackOp : SortNullStackOp
  | PC_EVM_NullStackOp : SortNullStackOp
  | PREVRANDAO_EVM_NullStackOp : SortNullStackOp
  | RETURNDATASIZE_EVM_NullStackOp : SortNullStackOp
  | SELFBALANCE_EVM_NullStackOp : SortNullStackOp
  | STOP_EVM_NullStackOp : SortNullStackOp
  | TIMESTAMP_EVM_NullStackOp : SortNullStackOp

inductive SortOpCode : Type where
  | inj_SortBinStackOp (x : SortBinStackOp) : SortOpCode
  | inj_SortCallOp (x : SortCallOp) : SortOpCode
  | inj_SortCallSixOp (x : SortCallSixOp) : SortOpCode
  | inj_SortInternalOp (x : SortInternalOp) : SortOpCode
  | inj_SortInvalidOp (x : SortInvalidOp) : SortOpCode
  | inj_SortLogOp (x : SortLogOp) : SortOpCode
  | inj_SortNullStackOp (x : SortNullStackOp) : SortOpCode
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortOpCode
  | inj_SortPushOp (x : SortPushOp) : SortOpCode
  | inj_SortQuadStackOp (x : SortQuadStackOp) : SortOpCode
  | inj_SortStackOp (x : SortStackOp) : SortOpCode
  | inj_SortTernStackOp (x : SortTernStackOp) : SortOpCode
  | inj_SortUnStackOp (x : SortUnStackOp) : SortOpCode
  | PUSHAsm (x0 : SortInt) (x1 : SortInt) : SortOpCode

inductive SortOpCodes : Type where
  | «.OpCodes_EVM-ASSEMBLY_OpCodes» : SortOpCodes
  | «_;__EVM-ASSEMBLY_OpCodes_OpCode_OpCodes» (x0 : SortOpCode) (x1 : SortOpCodes) : SortOpCodes

inductive SortPrecompiledOp : Type where
  | BLAKE2F_EVM_PrecompiledOp : SortPrecompiledOp
  | ECADD_EVM_PrecompiledOp : SortPrecompiledOp
  | ECMUL_EVM_PrecompiledOp : SortPrecompiledOp
  | ECPAIRING_EVM_PrecompiledOp : SortPrecompiledOp
  | ECREC_EVM_PrecompiledOp : SortPrecompiledOp
  | ID_EVM_PrecompiledOp : SortPrecompiledOp
  | MODEXP_EVM_PrecompiledOp : SortPrecompiledOp
  | RIP160_EVM_PrecompiledOp : SortPrecompiledOp
  | SHA256_EVM_PrecompiledOp : SortPrecompiledOp

inductive SortPushOp : Type where
  | PUSH (x0 : SortInt) : SortPushOp
  | PUSHZERO_EVM_PushOp : SortPushOp

inductive SortQuadStackOp : Type where
  | CREATE2_EVM_QuadStackOp : SortQuadStackOp
  | EXTCODECOPY_EVM_QuadStackOp : SortQuadStackOp

inductive SortSchedule : Type where
  | BERLIN_EVM : SortSchedule
  | BYZANTIUM_EVM : SortSchedule
  | CANCUN_EVM : SortSchedule
  | CONSTANTINOPLE_EVM : SortSchedule
  | DEFAULT_EVM : SortSchedule
  | FRONTIER_EVM : SortSchedule
  | HOMESTEAD_EVM : SortSchedule
  | ISTANBUL_EVM : SortSchedule
  | LONDON_EVM : SortSchedule
  | MERGE_EVM : SortSchedule
  | PETERSBURG_EVM : SortSchedule
  | SHANGHAI_EVM : SortSchedule
  | SPURIOUS_DRAGON_EVM : SortSchedule
  | TANGERINE_WHISTLE_EVM : SortSchedule

inductive SortScheduleConst : Type where
  | Gaccesslistaddress_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gaccessliststoragekey_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gbalance_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gbase_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gblockhash_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcall_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcallstipend_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcallvalue_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcodedeposit_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcoldaccountaccess_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcoldsload_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcopy_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcreate_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecadd_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecmul_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecpaircoeff_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecpairconst_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gexp_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gexpbyte_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gextcodecopy_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gextcodesize_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gfround_SCHEDULE_ScheduleConst : SortScheduleConst
  | Ghigh_SCHEDULE_ScheduleConst : SortScheduleConst
  | Ginitcodewordcost_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gjumpdest_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glog_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glogdata_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glogtopic_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glow_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gmemory_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gmid_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gnewaccount_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gquadcoeff_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gquaddivisor_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gselfdestruct_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsha3_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsha3word_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsload_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsstorereset_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsstoreset_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtransaction_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtxcreate_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtxdatanonzero_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtxdatazero_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gverylow_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gwarmstoragedirtystore_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gwarmstorageread_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gzero_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rb_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rmaxquotient_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rselfdestruct_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rsstoreclear_SCHEDULE_ScheduleConst : SortScheduleConst
  | maxCodeSize_SCHEDULE_ScheduleConst : SortScheduleConst
  | maxInitCodeSize_SCHEDULE_ScheduleConst : SortScheduleConst

inductive SortScheduleFlag : Type where
  | Gemptyisnonexistent_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasaccesslist_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasbasefee_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasbeaconroot_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghaschainid_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghascreate2_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasdirtysstore_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasextcodehash_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasmaxinitcodesize_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasmcopy_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasprevrandao_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghaspushzero_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasrejectedfirstbyte_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasreturndata_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasrevert_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasselfbalance_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasshift_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghassstorestipend_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasstaticcall_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghastransient_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghaswarmcoinbase_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Gselfdestructnewaccount_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Gstaticcalldepth_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Gzerovaluenewaccountgas_SCHEDULE_ScheduleFlag : SortScheduleFlag

inductive SortSignedness : Type where
  | signedBytes : SortSignedness
  | unsignedBytes : SortSignedness

inductive SortStackOp : Type where
  | DUP (x0 : SortInt) : SortStackOp
  | SWAP (x0 : SortInt) : SortStackOp

inductive SortStatusCode : Type where
  | inj_SortEndStatusCode (x : SortEndStatusCode) : SortStatusCode
  | inj_SortExceptionalStatusCode (x : SortExceptionalStatusCode) : SortStatusCode
  | «.StatusCode_NETWORK_StatusCode» : SortStatusCode
  | EVMC_INTERNAL_ERROR_NETWORK_StatusCode : SortStatusCode
  | EVMC_REJECTED_NETWORK_StatusCode : SortStatusCode

inductive SortSubstateLogEntry : Type where
  | logEntry (x0 : SortInt) (x1 : SortList) (x2 : SortBytes) : SortSubstateLogEntry

inductive SortTernStackOp : Type where
  | ADDMOD_EVM_TernStackOp : SortTernStackOp
  | CALLDATACOPY_EVM_TernStackOp : SortTernStackOp
  | CODECOPY_EVM_TernStackOp : SortTernStackOp
  | CREATE_EVM_TernStackOp : SortTernStackOp
  | MCOPY_EVM_TernStackOp : SortTernStackOp
  | MULMOD_EVM_TernStackOp : SortTernStackOp
  | RETURNDATACOPY_EVM_TernStackOp : SortTernStackOp

inductive SortTxData : Type where
  | inj_SortAccessListTx (x : SortAccessListTx) : SortTxData
  | inj_SortDynamicFeeTx (x : SortDynamicFeeTx) : SortTxData
  | inj_SortLegacyTx (x : SortLegacyTx) : SortTxData

inductive SortTxType : Type where
  | «.TxType_EVM-TYPES_TxType» : SortTxType
  | «AccessList_EVM-TYPES_TxType» : SortTxType
  | «DynamicFee_EVM-TYPES_TxType» : SortTxType
  | «Legacy_EVM-TYPES_TxType» : SortTxType

inductive SortUnStackOp : Type where
  | BALANCE_EVM_UnStackOp : SortUnStackOp
  | BLOCKHASH_EVM_UnStackOp : SortUnStackOp
  | CALLDATALOAD_EVM_UnStackOp : SortUnStackOp
  | EXTCODEHASH_EVM_UnStackOp : SortUnStackOp
  | EXTCODESIZE_EVM_UnStackOp : SortUnStackOp
  | ISZERO_EVM_UnStackOp : SortUnStackOp
  | JUMP_EVM_UnStackOp : SortUnStackOp
  | MLOAD_EVM_UnStackOp : SortUnStackOp
  | NOT_EVM_UnStackOp : SortUnStackOp
  | POP_EVM_UnStackOp : SortUnStackOp
  | SELFDESTRUCT_EVM_UnStackOp : SortUnStackOp
  | SLOAD_EVM_UnStackOp : SortUnStackOp
  | TLOAD_EVM_UnStackOp : SortUnStackOp

inductive SortWordStack : Type where
  | «.WordStack_EVM-TYPES_WordStack» : SortWordStack
  | «_:__EVM-TYPES_WordStack_Int_WordStack» (x0 : SortInt) (x1 : SortWordStack) : SortWordStack

structure SortBalanceCell : Type where
  val : SortInt

structure SortIdCell : Type where
  val : SortAccount

structure SortCoinbaseCell : Type where
  val : SortInt

structure SortBlockNonceCell : Type where
  val : SortInt

structure SortTransientStorageCell : Type where
  val : SortMap

structure SortTimestampCell : Type where
  val : SortInt

structure SortStatusCodeCell : Type where
  val : SortStatusCode

structure SortScheduleCell : Type where
  val : SortSchedule

structure SortPreviousHashCell : Type where
  val : SortInt

structure SortCodeCell : Type where
  val : SortAccountCode

structure SortTxOrderCell : Type where
  val : SortList

structure SortOrigStorageCell : Type where
  val : SortMap

structure SortStaticCell : Type where
  val : SortBool

structure SortKCell : Type where
  val : SortK

structure SortExitCodeCell : Type where
  val : SortInt

structure SortModeCell : Type where
  val : SortMode

structure SortUseGasCell : Type where
  val : SortBool

structure SortOmmersHashCell : Type where
  val : SortInt

structure SortStateRootCell : Type where
  val : SortInt

structure SortTransactionsRootCell : Type where
  val : SortInt

structure SortReceiptsRootCell : Type where
  val : SortInt

structure SortLogsBloomCell : Type where
  val : SortBytes

structure SortDifficultyCell : Type where
  val : SortInt

structure SortNumberCell : Type where
  val : SortInt

structure SortGasLimitCell : Type where
  val : SortInt

structure SortGasUsedCell : Type where
  val : SortGas

structure SortExtraDataCell : Type where
  val : SortBytes

structure SortMixHashCell : Type where
  val : SortInt

structure SortBaseFeeCell : Type where
  val : SortInt

structure SortWithdrawalsRootCell : Type where
  val : SortInt

structure SortBlobGasUsedCell : Type where
  val : SortInt

structure SortExcessBlobGasCell : Type where
  val : SortInt

structure SortBeaconRootCell : Type where
  val : SortInt

structure SortOmmerBlockHeadersCell : Type where
  val : SortJSON

structure SortValueCell : Type where
  val : SortInt

structure SortRefundCell : Type where
  val : SortInt

structure SortOutputCell : Type where
  val : SortBytes

structure SortCallStackCell : Type where
  val : SortList

structure SortInterimStatesCell : Type where
  val : SortList

structure SortTouchedAccountsCell : Type where
  val : SortSet

structure SortGasPriceCell : Type where
  val : SortInt

structure SortOriginCell : Type where
  val : SortAccount

structure SortBlockhashesCell : Type where
  val : SortList

structure SortCallDepthCell : Type where
  val : SortInt

structure SortToCell : Type where
  val : SortAccount

structure SortTxChainIDCell : Type where
  val : SortInt

structure SortAcctIDCell : Type where
  val : SortInt

structure SortTxAccessCell : Type where
  val : SortJSON

structure SortStorageCell : Type where
  val : SortMap

structure SortProgramCell : Type where
  val : SortBytes

structure SortGeneratedCounterCell : Type where
  val : SortInt

structure SortAccessedAccountsCell : Type where
  val : SortSet

structure SortTxMaxFeeCell : Type where
  val : SortInt

structure SortTxGasLimitCell : Type where
  val : SortInt

structure SortGasCell : Type where
  val : SortGas

structure SortChainIDCell : Type where
  val : SortInt

structure SortTxPendingCell : Type where
  val : SortList

structure SortJumpDestsCell : Type where
  val : SortBytes

structure SortSigSCell : Type where
  val : SortBytes

structure SortDataCell : Type where
  val : SortBytes

structure SortTxNonceCell : Type where
  val : SortInt

structure SortPcCell : Type where
  val : SortInt

structure SortTxTypeCell : Type where
  val : SortTxType

structure SortSelfDestructCell : Type where
  val : SortSet

structure SortLogCell : Type where
  val : SortList

structure SortAccessedStorageCell : Type where
  val : SortMap

structure SortCallDataCell : Type where
  val : SortBytes

structure SortMsgIDCell : Type where
  val : SortInt

structure SortTxGasPriceCell : Type where
  val : SortInt

structure SortSigVCell : Type where
  val : SortInt

structure SortSigRCell : Type where
  val : SortBytes

structure SortTxPriorityFeeCell : Type where
  val : SortInt

structure SortCallerCell : Type where
  val : SortAccount

structure SortCallValueCell : Type where
  val : SortInt

structure SortWordStackCell : Type where
  val : SortWordStack

structure SortLocalMemCell : Type where
  val : SortBytes

structure SortMemoryUsedCell : Type where
  val : SortInt

structure SortCallGasCell : Type where
  val : SortGas

structure SortNonceCell : Type where
  val : SortInt

structure SortBlockCell : Type where
  previousHash : SortPreviousHashCell
  ommersHash : SortOmmersHashCell
  coinbase : SortCoinbaseCell
  stateRoot : SortStateRootCell
  transactionsRoot : SortTransactionsRootCell
  receiptsRoot : SortReceiptsRootCell
  logsBloom : SortLogsBloomCell
  difficulty : SortDifficultyCell
  number : SortNumberCell
  gasLimit : SortGasLimitCell
  gasUsed : SortGasUsedCell
  timestamp : SortTimestampCell
  extraData : SortExtraDataCell
  mixHash : SortMixHashCell
  blockNonce : SortBlockNonceCell
  baseFee : SortBaseFeeCell
  withdrawalsRoot : SortWithdrawalsRootCell
  blobGasUsed : SortBlobGasUsedCell
  excessBlobGas : SortExcessBlobGasCell
  beaconRoot : SortBeaconRootCell
  ommerBlockHeaders : SortOmmerBlockHeadersCell

structure SortSubstateCell : Type where
  selfDestruct : SortSelfDestructCell
  log : SortLogCell
  refund : SortRefundCell
  accessedAccounts : SortAccessedAccountsCell
  accessedStorage : SortAccessedStorageCell

structure SortMessageCell : Type where
  msgID : SortMsgIDCell
  txNonce : SortTxNonceCell
  txGasPrice : SortTxGasPriceCell
  txGasLimit : SortTxGasLimitCell
  to : SortToCell
  value : SortValueCell
  sigV : SortSigVCell
  sigR : SortSigRCell
  sigS : SortSigSCell
  data : SortDataCell
  txAccess : SortTxAccessCell
  txChainID : SortTxChainIDCell
  txPriorityFee : SortTxPriorityFeeCell
  txMaxFee : SortTxMaxFeeCell
  txType : SortTxTypeCell

abbrev SortMessageCellMap : Type := MapHook SortMsgIDCell SortMessageCell

structure SortMessagesCell : Type where
  val : SortMessageCellMap

structure SortCallStateCell : Type where
  program : SortProgramCell
  jumpDests : SortJumpDestsCell
  id : SortIdCell
  caller : SortCallerCell
  callData : SortCallDataCell
  callValue : SortCallValueCell
  wordStack : SortWordStackCell
  localMem : SortLocalMemCell
  pc : SortPcCell
  gas : SortGasCell
  memoryUsed : SortMemoryUsedCell
  callGas : SortCallGasCell
  static : SortStaticCell
  callDepth : SortCallDepthCell

structure SortAccountCell : Type where
  acctID : SortAcctIDCell
  balance : SortBalanceCell
  code : SortCodeCell
  storage : SortStorageCell
  origStorage : SortOrigStorageCell
  transientStorage : SortTransientStorageCell
  nonce : SortNonceCell

abbrev SortAccountCellMap : Type := MapHook SortAcctIDCell SortAccountCell

structure SortAccountsCell : Type where
  val : SortAccountCellMap

structure SortNetworkCell : Type where
  chainID : SortChainIDCell
  accounts : SortAccountsCell
  txOrder : SortTxOrderCell
  txPending : SortTxPendingCell
  messages : SortMessagesCell

structure SortEvmCell : Type where
  output : SortOutputCell
  statusCode : SortStatusCodeCell
  callStack : SortCallStackCell
  interimStates : SortInterimStatesCell
  touchedAccounts : SortTouchedAccountsCell
  callState : SortCallStateCell
  substate : SortSubstateCell
  gasPrice : SortGasPriceCell
  origin : SortOriginCell
  blockhashes : SortBlockhashesCell
  block : SortBlockCell

structure SortEthereumCell : Type where
  evm : SortEvmCell
  network : SortNetworkCell

structure SortKevmCell : Type where
  k : SortKCell
  exitCode : SortExitCodeCell
  mode : SortModeCell
  schedule : SortScheduleCell
  useGas : SortUseGasCell
  ethereum : SortEthereumCell

structure SortGeneratedTopCell : Type where
  kevm : SortKevmCell
  generatedCounter : SortGeneratedCounterCell

@tothtamas28 tothtamas28 requested a review from JuanCoRo January 9, 2025 20:53
@tothtamas28 tothtamas28 marked this pull request as ready for review January 9, 2025 20:53
@tothtamas28 tothtamas28 changed the title Generate structure-s for non-leaf cells Generate structure-s for cells Jan 10, 2025
@tothtamas28 tothtamas28 marked this pull request as draft January 10, 2025 22:44
@tothtamas28 tothtamas28 changed the title Generate structure-s for cells Generate structure-s for non-leaf cells Jan 13, 2025
@JuanCoRo
Copy link
Member

Posting here the latest Lean 4 generated definition for evm-semantics.llvm:

Click to expand 
inductive SortAccessListTx : Type where
  | AccessListTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortAccount) (x4 : SortInt) (x5 : SortBytes) (x6 : SortInt) (x7 : SortJSONs) : SortAccessListTx

inductive SortAccount : Type where
  | inj_SortInt (x : SortInt) : SortAccount
  | «.Account_EVM-TYPES_Account» : SortAccount

inductive SortAccountCode : Type where
  | inj_SortBytes (x : SortBytes) : SortAccountCode

inductive SortAccounts : Type where
  | «{_|_}_EVM_Accounts_AccountsCell_SubstateCell» (x0 : SortAccountsCell) (x1 : SortSubstateCell) : SortAccounts

inductive SortBExp : Type where
  | inj_SortBool (x : SortBool) : SortBExp
  | «#accountNonexistent» (x0 : SortInt) : SortBExp

inductive SortBinStackOp : Type where
  | inj_SortLogOp (x : SortLogOp) : SortBinStackOp
  | ADD_EVM_BinStackOp : SortBinStackOp
  | AND_EVM_BinStackOp : SortBinStackOp
  | BYTE_EVM_BinStackOp : SortBinStackOp
  | DIV_EVM_BinStackOp : SortBinStackOp
  | EQ_EVM_BinStackOp : SortBinStackOp
  | EVMOR_EVM_BinStackOp : SortBinStackOp
  | EXP_EVM_BinStackOp : SortBinStackOp
  | GT_EVM_BinStackOp : SortBinStackOp
  | JUMPI_EVM_BinStackOp : SortBinStackOp
  | LT_EVM_BinStackOp : SortBinStackOp
  | MOD_EVM_BinStackOp : SortBinStackOp
  | MSTORE_EVM_BinStackOp : SortBinStackOp
  | MSTORE8_EVM_BinStackOp : SortBinStackOp
  | MUL_EVM_BinStackOp : SortBinStackOp
  | RETURN_EVM_BinStackOp : SortBinStackOp
  | REVERT_EVM_BinStackOp : SortBinStackOp
  | SAR_EVM_BinStackOp : SortBinStackOp
  | SDIV_EVM_BinStackOp : SortBinStackOp
  | SGT_EVM_BinStackOp : SortBinStackOp
  | SHA3_EVM_BinStackOp : SortBinStackOp
  | SHL_EVM_BinStackOp : SortBinStackOp
  | SHR_EVM_BinStackOp : SortBinStackOp
  | SIGNEXTEND_EVM_BinStackOp : SortBinStackOp
  | SLT_EVM_BinStackOp : SortBinStackOp
  | SMOD_EVM_BinStackOp : SortBinStackOp
  | SSTORE_EVM_BinStackOp : SortBinStackOp
  | SUB_EVM_BinStackOp : SortBinStackOp
  | TSTORE_EVM_BinStackOp : SortBinStackOp
  | XOR_EVM_BinStackOp : SortBinStackOp

inductive SortCallOp : Type where
  | CALL_EVM_CallOp : SortCallOp
  | CALLCODE_EVM_CallOp : SortCallOp

inductive SortCallSixOp : Type where
  | DELEGATECALL_EVM_CallSixOp : SortCallSixOp
  | STATICCALL_EVM_CallSixOp : SortCallSixOp

inductive SortDynamicFeeTx : Type where
  | DynamicFeeTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortAccount) (x5 : SortInt) (x6 : SortBytes) (x7 : SortInt) (x8 : SortJSONs) : SortDynamicFeeTx

inductive SortEndStatusCode : Type where
  | inj_SortExceptionalStatusCode (x : SortExceptionalStatusCode) : SortEndStatusCode
  | EVMC_REVERT_NETWORK_EndStatusCode : SortEndStatusCode
  | EVMC_SUCCESS_NETWORK_EndStatusCode : SortEndStatusCode

inductive SortEndianness : Type where
  | bigEndianBytes : SortEndianness

inductive SortEthereumCommand : Type where
  | «#executeBeaconRoots» : SortEthereumCommand
  | «#finalizeBlock_EVM_EthereumCommand» : SortEthereumCommand
  | «#finishTx_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «#loadAccessList» (x0 : SortJSON) : SortEthereumCommand
  | «#loadAccessListAux» (x0 : SortAccount) (x1 : SortList) : SortEthereumCommand
  | «#rewardOmmers» (x0 : SortJSONs) : SortEthereumCommand
  | «#startBlock_EVM_EthereumCommand» : SortEthereumCommand
  | «check__ETHEREUM-SIMULATION_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «clear_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «clearBLOCK_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «clearNETWORK_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «clearTX_STATE-UTILS_EthereumCommand» : SortEthereumCommand
  | «exception_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «failure__ETHEREUM-SIMULATION_EthereumCommand_String» (x0 : SortString) : SortEthereumCommand
  | «flush_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «load__STATE-UTILS_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «loadAccount___STATE-UTILS_EthereumCommand_Int_JSON» (x0 : SortInt) (x1 : SortJSON) : SortEthereumCommand
  | «loadTransaction___STATE-UTILS_EthereumCommand_Int_JSON» (x0 : SortInt) (x1 : SortJSON) : SortEthereumCommand
  | loadTx (x0 : SortAccount) : SortEthereumCommand
  | «mkAcct__STATE-UTILS_EthereumCommand_Int» (x0 : SortInt) : SortEthereumCommand
  | «mkTX__STATE-UTILS_EthereumCommand_Int» (x0 : SortInt) : SortEthereumCommand
  | «process__ETHEREUM-SIMULATION_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «run__ETHEREUM-SIMULATION_EthereumCommand_JSON» (x0 : SortJSON) : SortEthereumCommand
  | «start_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «startTx_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand
  | «status__ETHEREUM-SIMULATION_EthereumCommand_StatusCode» (x0 : SortStatusCode) : SortEthereumCommand
  | «success_ETHEREUM-SIMULATION_EthereumCommand» : SortEthereumCommand

inductive SortEthereumSimulation : Type where
  | inj_SortAccount (x : SortAccount) : SortEthereumSimulation
  | inj_SortBool (x : SortBool) : SortEthereumSimulation
  | inj_SortBytes (x : SortBytes) : SortEthereumSimulation
  | inj_SortInt (x : SortInt) : SortEthereumSimulation
  | inj_SortJSON (x : SortJSON) : SortEthereumSimulation
  | inj_SortMap (x : SortMap) : SortEthereumSimulation
  | inj_SortOpCodes (x : SortOpCodes) : SortEthereumSimulation
  | inj_SortString (x : SortString) : SortEthereumSimulation
  | inj_SortSubstateLogEntry (x : SortSubstateLogEntry) : SortEthereumSimulation
  | inj_SortTxType (x : SortTxType) : SortEthereumSimulation
  | «.EthereumSimulation_ETHEREUM-SIMULATION_EthereumSimulation» : SortEthereumSimulation
  | «___ETHEREUM-SIMULATION_EthereumSimulation_EthereumCommand_EthereumSimulation» (x0 : SortEthereumCommand) (x1 : SortEthereumSimulation) : SortEthereumSimulation

inductive SortExceptionalStatusCode : Type where
  | EVMC_ACCOUNT_ALREADY_EXISTS_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_BAD_JUMP_DESTINATION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_BALANCE_UNDERFLOW_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_CALL_DEPTH_EXCEEDED_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_INVALID_INSTRUCTION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_INVALID_MEMORY_ACCESS_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_NONCE_EXCEEDED_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_OUT_OF_GAS_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_PRECOMPILE_FAILURE_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_STACK_OVERFLOW_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_STACK_UNDERFLOW_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_STATIC_MODE_VIOLATION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode
  | EVMC_UNDEFINED_INSTRUCTION_NETWORK_ExceptionalStatusCode : SortExceptionalStatusCode

inductive SortExp : Type where
  | inj_SortGas (x : SortGas) : SortExp
  | inj_SortInt (x : SortInt) : SortExp
  | Ccall (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortGas) (x3 : SortGas) (x4 : SortInt) (x5 : SortBool) : SortExp
  | Ccallgas (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortGas) (x3 : SortGas) (x4 : SortInt) (x5 : SortBool) : SortExp
  | Cselfdestruct (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortInt) : SortExp

inductive SortG1Point : Type where
  | «(_,_)_KRYPTO_G1Point_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortG1Point

inductive SortG2Point : Type where
  | «(_x_,_x_)_KRYPTO_G2Point_Int_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : SortG2Point

inductive SortGas : Type where
  | inj_SortInt (x : SortInt) : SortGas

inductive SortInternalOp : Type where
  | «#access[_,_]_EVM_InternalOp_OpCode_OpCode» (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | «#addr[_]_EVM_InternalOp_OpCode» (x0 : SortOpCode) : SortInternalOp
  | «#allocateCallGas_EVM_InternalOp» : SortInternalOp
  | «#allocateCreateGas_EVM_InternalOp» : SortInternalOp
  | «#call________EVM_InternalOp_Int_Int_Int_Int_Int_Bytes_Bool» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortBytes) (x6 : SortBool) : SortInternalOp
  | «#callWithCode_________EVM_InternalOp_Int_Int_Int_Bytes_Int_Int_Bytes_Bool» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) (x5 : SortInt) (x6 : SortBytes) (x7 : SortBool) : SortInternalOp
  | «#checkBalanceUnderflow___EVM_InternalOp_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | «#checkCall___EVM_InternalOp_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | «#checkCreate___EVM_InternalOp_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | «#checkDepthExceeded_EVM_InternalOp» : SortInternalOp
  | «#checkNonceExceeded__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#checkPoint_EVM_InternalOp» : SortInternalOp
  | «#create_____EVM_InternalOp_Int_Int_Int_Bytes» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : SortInternalOp
  | «#deductGas_EVM_InternalOp» : SortInternalOp
  | «#deductMemory_EVM_InternalOp» : SortInternalOp
  | «#deductMemoryGas_EVM_InternalOp» : SortInternalOp
  | «#deleteAccounts» (x0 : SortList) : SortInternalOp
  | «#dropCallStack_EVM_InternalOp» : SortInternalOp
  | «#dropWorldState_EVM_InternalOp» : SortInternalOp
  | «#ecadd» (x0 : SortG1Point) (x1 : SortG1Point) : SortInternalOp
  | «#ecmul» (x0 : SortG1Point) (x1 : SortInt) : SortInternalOp
  | «#ecpairing» (x0 : SortList) (x1 : SortList) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) : SortInternalOp
  | «#endBasicBlock_EVM_InternalOp» : SortInternalOp
  | «#exec[_]_EVM_InternalOp_OpCode» (x0 : SortOpCode) : SortInternalOp
  | «#finalizeStorage» (x0 : SortList) : SortInternalOp
  | «#finalizeTx» (x0 : SortBool) : SortInternalOp
  | «#gas[_,_]_EVM_InternalOp_OpCode_OpCode» (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | «#gas[_]_EVM_InternalOp_OpCode» (x0 : SortOpCode) : SortInternalOp
  | «#gasAccess» (x0 : SortSchedule) (x1 : SortOpCode) : SortInternalOp
  | «#gasExec» (x0 : SortSchedule) (x1 : SortOpCode) : SortInternalOp
  | «#incrementNonce__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#memory[_,_]_EVM_InternalOp_OpCode_OpCode» (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | «#mkCall________EVM_InternalOp_Int_Int_Int_Bytes_Int_Bytes_Bool» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) (x5 : SortBytes) (x6 : SortBool) : SortInternalOp
  | «#mkCreate_____EVM_InternalOp_Int_Int_Int_Bytes» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : SortInternalOp
  | «#newAccount__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#newExistingAccount__EVM_InternalOp_Int» (x0 : SortInt) : SortInternalOp
  | «#next[_]_EVM_InternalOp_MaybeOpCode» (x0 : SortMaybeOpCode) : SortInternalOp
  | «#popCallStack_EVM_InternalOp» : SortInternalOp
  | «#popWorldState_EVM_InternalOp» : SortInternalOp
  | «#precompiled?(_,_)_EVM_InternalOp_Int_Schedule» (x0 : SortInt) (x1 : SortSchedule) : SortInternalOp
  | «#push_EVM_InternalOp» : SortInternalOp
  | «#pushCallStack_EVM_InternalOp» : SortInternalOp
  | «#pushWorldState_EVM_InternalOp» : SortInternalOp
  | «#refund__EVM_InternalOp_Gas» (x0 : SortGas) : SortInternalOp
  | «#setLocalMem____EVM_InternalOp_Int_Int_Bytes» (x0 : SortInt) (x1 : SortInt) (x2 : SortBytes) : SortInternalOp
  | «#setStack__EVM_InternalOp_WordStack» (x0 : SortWordStack) : SortInternalOp
  | «#transferFunds____EVM_InternalOp_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | «#transferFundsToNonExistent____EVM_InternalOp_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | ___EVM_InternalOp_StackOp_WordStack (x0 : SortStackOp) (x1 : SortWordStack) : SortInternalOp
  | ___EVM_InternalOp_UnStackOp_Int (x0 : SortUnStackOp) (x1 : SortInt) : SortInternalOp
  | ____EVM_InternalOp_BinStackOp_Int_Int (x0 : SortBinStackOp) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | _____EVM_InternalOp_TernStackOp_Int_Int_Int (x0 : SortTernStackOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : SortInternalOp
  | ______EVM_InternalOp_QuadStackOp_Int_Int_Int_Int (x0 : SortQuadStackOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) : SortInternalOp
  | ________EVM_InternalOp_CallSixOp_Int_Int_Int_Int_Int_Int (x0 : SortCallSixOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortInt) : SortInternalOp
  | _________EVM_InternalOp_CallOp_Int_Int_Int_Int_Int_Int_Int (x0 : SortCallOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortInt) (x7 : SortInt) : SortInternalOp
  | pc (x0 : SortOpCode) : SortInternalOp

inductive SortInvalidOp : Type where
  | INVALID_EVM_InvalidOp : SortInvalidOp
  | «UNDEFINED(_)_EVM_InvalidOp_Int» (x0 : SortInt) : SortInvalidOp

inductive SortJSON : Type where
  | inj_SortAccount (x : SortAccount) : SortJSON
  | inj_SortBool (x : SortBool) : SortJSON
  | inj_SortBytes (x : SortBytes) : SortJSON
  | inj_SortInt (x : SortInt) : SortJSON
  | inj_SortMap (x : SortMap) : SortJSON
  | inj_SortOpCodes (x : SortOpCodes) : SortJSON
  | inj_SortString (x : SortString) : SortJSON
  | inj_SortSubstateLogEntry (x : SortSubstateLogEntry) : SortJSON
  | inj_SortTxType (x : SortTxType) : SortJSON
  | JSONEntry (x0 : SortJSONKey) (x1 : SortJSON) : SortJSON
  | JSONList (x0 : SortJSONs) : SortJSON
  | JSONObject (x0 : SortJSONs) : SortJSON
  | JSONnull : SortJSON

inductive SortJSONKey : Type where
  | inj_SortInt (x : SortInt) : SortJSONKey
  | inj_SortString (x : SortString) : SortJSONKey

inductive SortJSONs : Type where
  | «.List{"JSONs"}» : SortJSONs
  | JSONs (x0 : SortJSON) (x1 : SortJSONs) : SortJSONs

inductive SortK : Type where
  | dotk : SortK
  | kseq (x0 : SortKItem) (x1 : SortK) : SortK

inductive SortKItem : Type where
  | inj_SortAccessListTx (x : SortAccessListTx) : SortKItem
  | inj_SortAccessedAccountsCell (x : SortAccessedAccountsCell) : SortKItem
  | inj_SortAccessedStorageCell (x : SortAccessedStorageCell) : SortKItem
  | inj_SortAccount (x : SortAccount) : SortKItem
  | inj_SortAccountCell (x : SortAccountCell) : SortKItem
  | inj_SortAccountCellMap (x : SortAccountCellMap) : SortKItem
  | inj_SortAccountCode (x : SortAccountCode) : SortKItem
  | inj_SortAccounts (x : SortAccounts) : SortKItem
  | inj_SortAccountsCell (x : SortAccountsCell) : SortKItem
  | inj_SortAcctIDCell (x : SortAcctIDCell) : SortKItem
  | inj_SortBExp (x : SortBExp) : SortKItem
  | inj_SortBalanceCell (x : SortBalanceCell) : SortKItem
  | inj_SortBaseFeeCell (x : SortBaseFeeCell) : SortKItem
  | inj_SortBeaconRootCell (x : SortBeaconRootCell) : SortKItem
  | inj_SortBinStackOp (x : SortBinStackOp) : SortKItem
  | inj_SortBlobGasUsedCell (x : SortBlobGasUsedCell) : SortKItem
  | inj_SortBlockCell (x : SortBlockCell) : SortKItem
  | inj_SortBlockNonceCell (x : SortBlockNonceCell) : SortKItem
  | inj_SortBlockhashesCell (x : SortBlockhashesCell) : SortKItem
  | inj_SortBool (x : SortBool) : SortKItem
  | inj_SortBytes (x : SortBytes) : SortKItem
  | inj_SortCallDataCell (x : SortCallDataCell) : SortKItem
  | inj_SortCallDepthCell (x : SortCallDepthCell) : SortKItem
  | inj_SortCallGasCell (x : SortCallGasCell) : SortKItem
  | inj_SortCallOp (x : SortCallOp) : SortKItem
  | inj_SortCallSixOp (x : SortCallSixOp) : SortKItem
  | inj_SortCallStackCell (x : SortCallStackCell) : SortKItem
  | inj_SortCallStateCell (x : SortCallStateCell) : SortKItem
  | inj_SortCallValueCell (x : SortCallValueCell) : SortKItem
  | inj_SortCallerCell (x : SortCallerCell) : SortKItem
  | inj_SortChainIDCell (x : SortChainIDCell) : SortKItem
  | inj_SortCodeCell (x : SortCodeCell) : SortKItem
  | inj_SortCoinbaseCell (x : SortCoinbaseCell) : SortKItem
  | inj_SortDataCell (x : SortDataCell) : SortKItem
  | inj_SortDifficultyCell (x : SortDifficultyCell) : SortKItem
  | inj_SortDynamicFeeTx (x : SortDynamicFeeTx) : SortKItem
  | inj_SortEndStatusCode (x : SortEndStatusCode) : SortKItem
  | inj_SortEndianness (x : SortEndianness) : SortKItem
  | inj_SortEthereumCell (x : SortEthereumCell) : SortKItem
  | inj_SortEthereumCommand (x : SortEthereumCommand) : SortKItem
  | inj_SortEthereumSimulation (x : SortEthereumSimulation) : SortKItem
  | inj_SortEvmCell (x : SortEvmCell) : SortKItem
  | inj_SortExceptionalStatusCode (x : SortExceptionalStatusCode) : SortKItem
  | inj_SortExcessBlobGasCell (x : SortExcessBlobGasCell) : SortKItem
  | inj_SortExitCodeCell (x : SortExitCodeCell) : SortKItem
  | inj_SortExp (x : SortExp) : SortKItem
  | inj_SortExtraDataCell (x : SortExtraDataCell) : SortKItem
  | inj_SortG1Point (x : SortG1Point) : SortKItem
  | inj_SortG2Point (x : SortG2Point) : SortKItem
  | inj_SortGas (x : SortGas) : SortKItem
  | inj_SortGasCell (x : SortGasCell) : SortKItem
  | inj_SortGasLimitCell (x : SortGasLimitCell) : SortKItem
  | inj_SortGasPriceCell (x : SortGasPriceCell) : SortKItem
  | inj_SortGasUsedCell (x : SortGasUsedCell) : SortKItem
  | inj_SortGeneratedCounterCell (x : SortGeneratedCounterCell) : SortKItem
  | inj_SortGeneratedTopCell (x : SortGeneratedTopCell) : SortKItem
  | inj_SortIdCell (x : SortIdCell) : SortKItem
  | inj_SortInt (x : SortInt) : SortKItem
  | inj_SortInterimStatesCell (x : SortInterimStatesCell) : SortKItem
  | inj_SortInternalOp (x : SortInternalOp) : SortKItem
  | inj_SortInvalidOp (x : SortInvalidOp) : SortKItem
  | inj_SortJSON (x : SortJSON) : SortKItem
  | inj_SortJSONKey (x : SortJSONKey) : SortKItem
  | inj_SortJSONs (x : SortJSONs) : SortKItem
  | inj_SortJumpDestsCell (x : SortJumpDestsCell) : SortKItem
  | inj_SortKCell (x : SortKCell) : SortKItem
  | inj_SortKevmCell (x : SortKevmCell) : SortKItem
  | inj_SortLegacyTx (x : SortLegacyTx) : SortKItem
  | inj_SortLengthPrefix (x : SortLengthPrefix) : SortKItem
  | inj_SortLengthPrefixType (x : SortLengthPrefixType) : SortKItem
  | inj_SortList (x : SortList) : SortKItem
  | inj_SortLocalMemCell (x : SortLocalMemCell) : SortKItem
  | inj_SortLogCell (x : SortLogCell) : SortKItem
  | inj_SortLogOp (x : SortLogOp) : SortKItem
  | inj_SortLogsBloomCell (x : SortLogsBloomCell) : SortKItem
  | inj_SortMap (x : SortMap) : SortKItem
  | inj_SortMaybeOpCode (x : SortMaybeOpCode) : SortKItem
  | inj_SortMemoryUsedCell (x : SortMemoryUsedCell) : SortKItem
  | inj_SortMessageCell (x : SortMessageCell) : SortKItem
  | inj_SortMessageCellMap (x : SortMessageCellMap) : SortKItem
  | inj_SortMessagesCell (x : SortMessagesCell) : SortKItem
  | inj_SortMixHashCell (x : SortMixHashCell) : SortKItem
  | inj_SortMode (x : SortMode) : SortKItem
  | inj_SortModeCell (x : SortModeCell) : SortKItem
  | inj_SortMsgIDCell (x : SortMsgIDCell) : SortKItem
  | inj_SortNetworkCell (x : SortNetworkCell) : SortKItem
  | inj_SortNonceCell (x : SortNonceCell) : SortKItem
  | inj_SortNullStackOp (x : SortNullStackOp) : SortKItem
  | inj_SortNumberCell (x : SortNumberCell) : SortKItem
  | inj_SortOmmerBlockHeadersCell (x : SortOmmerBlockHeadersCell) : SortKItem
  | inj_SortOmmersHashCell (x : SortOmmersHashCell) : SortKItem
  | inj_SortOpCode (x : SortOpCode) : SortKItem
  | inj_SortOpCodes (x : SortOpCodes) : SortKItem
  | inj_SortOrigStorageCell (x : SortOrigStorageCell) : SortKItem
  | inj_SortOriginCell (x : SortOriginCell) : SortKItem
  | inj_SortOutputCell (x : SortOutputCell) : SortKItem
  | inj_SortPcCell (x : SortPcCell) : SortKItem
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortKItem
  | inj_SortPreviousHashCell (x : SortPreviousHashCell) : SortKItem
  | inj_SortProgramCell (x : SortProgramCell) : SortKItem
  | inj_SortPushOp (x : SortPushOp) : SortKItem
  | inj_SortQuadStackOp (x : SortQuadStackOp) : SortKItem
  | inj_SortReceiptsRootCell (x : SortReceiptsRootCell) : SortKItem
  | inj_SortRefundCell (x : SortRefundCell) : SortKItem
  | inj_SortSchedule (x : SortSchedule) : SortKItem
  | inj_SortScheduleCell (x : SortScheduleCell) : SortKItem
  | inj_SortScheduleConst (x : SortScheduleConst) : SortKItem
  | inj_SortScheduleFlag (x : SortScheduleFlag) : SortKItem
  | inj_SortSelfDestructCell (x : SortSelfDestructCell) : SortKItem
  | inj_SortSet (x : SortSet) : SortKItem
  | inj_SortSigRCell (x : SortSigRCell) : SortKItem
  | inj_SortSigSCell (x : SortSigSCell) : SortKItem
  | inj_SortSigVCell (x : SortSigVCell) : SortKItem
  | inj_SortSignedness (x : SortSignedness) : SortKItem
  | inj_SortStackOp (x : SortStackOp) : SortKItem
  | inj_SortStateRootCell (x : SortStateRootCell) : SortKItem
  | inj_SortStaticCell (x : SortStaticCell) : SortKItem
  | inj_SortStatusCode (x : SortStatusCode) : SortKItem
  | inj_SortStatusCodeCell (x : SortStatusCodeCell) : SortKItem
  | inj_SortStorageCell (x : SortStorageCell) : SortKItem
  | inj_SortString (x : SortString) : SortKItem
  | inj_SortStringBuffer (x : SortStringBuffer) : SortKItem
  | inj_SortSubstateCell (x : SortSubstateCell) : SortKItem
  | inj_SortSubstateLogEntry (x : SortSubstateLogEntry) : SortKItem
  | inj_SortTernStackOp (x : SortTernStackOp) : SortKItem
  | inj_SortTimestampCell (x : SortTimestampCell) : SortKItem
  | inj_SortToCell (x : SortToCell) : SortKItem
  | inj_SortTouchedAccountsCell (x : SortTouchedAccountsCell) : SortKItem
  | inj_SortTransactionsRootCell (x : SortTransactionsRootCell) : SortKItem
  | inj_SortTransientStorageCell (x : SortTransientStorageCell) : SortKItem
  | inj_SortTxAccessCell (x : SortTxAccessCell) : SortKItem
  | inj_SortTxChainIDCell (x : SortTxChainIDCell) : SortKItem
  | inj_SortTxData (x : SortTxData) : SortKItem
  | inj_SortTxGasLimitCell (x : SortTxGasLimitCell) : SortKItem
  | inj_SortTxGasPriceCell (x : SortTxGasPriceCell) : SortKItem
  | inj_SortTxMaxFeeCell (x : SortTxMaxFeeCell) : SortKItem
  | inj_SortTxNonceCell (x : SortTxNonceCell) : SortKItem
  | inj_SortTxOrderCell (x : SortTxOrderCell) : SortKItem
  | inj_SortTxPendingCell (x : SortTxPendingCell) : SortKItem
  | inj_SortTxPriorityFeeCell (x : SortTxPriorityFeeCell) : SortKItem
  | inj_SortTxType (x : SortTxType) : SortKItem
  | inj_SortTxTypeCell (x : SortTxTypeCell) : SortKItem
  | inj_SortUnStackOp (x : SortUnStackOp) : SortKItem
  | inj_SortUseGasCell (x : SortUseGasCell) : SortKItem
  | inj_SortValueCell (x : SortValueCell) : SortKItem
  | inj_SortWithdrawalsRootCell (x : SortWithdrawalsRootCell) : SortKItem
  | inj_SortWordStack (x : SortWordStack) : SortKItem
  | inj_SortWordStackCell (x : SortWordStackCell) : SortKItem
  | «#accessAccounts__EVM_KItem_Account» (x0 : SortAccount) : SortKItem
  | «#accessAccounts__EVM_KItem_Set» (x0 : SortSet) : SortKItem
  | «#accessAccounts___EVM_KItem_Account_Account» (x0 : SortAccount) (x1 : SortAccount) : SortKItem
  | «#accessAccounts____EVM_KItem_Account_Account_Set» (x0 : SortAccount) (x1 : SortAccount) (x2 : SortSet) : SortKItem
  | «#accessStorage___EVM_KItem_Account_Int» (x0 : SortAccount) (x1 : SortInt) : SortKItem
  | «#codeDeposit__EVM_KItem_Int» (x0 : SortInt) : SortKItem
  | «#finishCodeDeposit___EVM_KItem_Int_Bytes» (x0 : SortInt) (x1 : SortBytes) : SortKItem
  | «#freezerCcall1_» (x0 : SortK) (x1 : SortK) (x2 : SortK) (x3 : SortK) (x4 : SortK) : SortKItem
  | «#freezerCcallgas1_» (x0 : SortK) (x1 : SortK) (x2 : SortK) (x3 : SortK) (x4 : SortK) : SortKItem
  | «#freezerCselfdestruct1_» (x0 : SortK) (x1 : SortK) : SortKItem
  | «#initVM_EVM_KItem» : SortKItem
  | «#mkCodeDeposit__EVM_KItem_Int» (x0 : SortInt) : SortKItem
  | «#return___EVM_KItem_Int_Int» (x0 : SortInt) (x1 : SortInt) : SortKItem
  | «#touchAccounts__EVM_KItem_Account» (x0 : SortAccount) : SortKItem
  | «#touchAccounts___EVM_KItem_Account_Account» (x0 : SortAccount) (x1 : SortAccount) : SortKItem
  | end (x0 : SortStatusCode) : SortKItem
  | execute : SortKItem
  | halt : SortKItem
  | «loadCallState__STATE-UTILS_KItem_JSON» (x0 : SortJSON) : SortKItem
  | loadProgram (x0 : SortBytes) : SortKItem

inductive SortLegacyTx : Type where
  | LegacySignedTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortAccount) (x4 : SortInt) (x5 : SortBytes) (x6 : SortInt) : SortLegacyTx
  | LegacyTxData (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortAccount) (x4 : SortInt) (x5 : SortBytes) : SortLegacyTx

inductive SortLengthPrefix : Type where
  | «_(_,_)_SERIALIZATION_LengthPrefix_LengthPrefixType_Int_Int» (x0 : SortLengthPrefixType) (x1 : SortInt) (x2 : SortInt) : SortLengthPrefix

inductive SortLengthPrefixType : Type where
  | «#list_SERIALIZATION_LengthPrefixType» : SortLengthPrefixType
  | «#str_SERIALIZATION_LengthPrefixType» : SortLengthPrefixType

inductive SortLogOp : Type where
  | LOG (x0 : SortInt) : SortLogOp

inductive SortMaybeOpCode : Type where
  | inj_SortBinStackOp (x : SortBinStackOp) : SortMaybeOpCode
  | inj_SortCallOp (x : SortCallOp) : SortMaybeOpCode
  | inj_SortCallSixOp (x : SortCallSixOp) : SortMaybeOpCode
  | inj_SortInternalOp (x : SortInternalOp) : SortMaybeOpCode
  | inj_SortInvalidOp (x : SortInvalidOp) : SortMaybeOpCode
  | inj_SortLogOp (x : SortLogOp) : SortMaybeOpCode
  | inj_SortNullStackOp (x : SortNullStackOp) : SortMaybeOpCode
  | inj_SortOpCode (x : SortOpCode) : SortMaybeOpCode
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortMaybeOpCode
  | inj_SortPushOp (x : SortPushOp) : SortMaybeOpCode
  | inj_SortQuadStackOp (x : SortQuadStackOp) : SortMaybeOpCode
  | inj_SortStackOp (x : SortStackOp) : SortMaybeOpCode
  | inj_SortTernStackOp (x : SortTernStackOp) : SortMaybeOpCode
  | inj_SortUnStackOp (x : SortUnStackOp) : SortMaybeOpCode
  | «.NoOpCode_EVM_MaybeOpCode» : SortMaybeOpCode

inductive SortMode : Type where
  | NORMAL : SortMode
  | «SUCCESS_ETHEREUM-SIMULATION_Mode» : SortMode
  | VMTESTS : SortMode

inductive SortNullStackOp : Type where
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortNullStackOp
  | ADDRESS_EVM_NullStackOp : SortNullStackOp
  | BASEFEE_EVM_NullStackOp : SortNullStackOp
  | CALLDATASIZE_EVM_NullStackOp : SortNullStackOp
  | CALLER_EVM_NullStackOp : SortNullStackOp
  | CALLVALUE_EVM_NullStackOp : SortNullStackOp
  | CHAINID_EVM_NullStackOp : SortNullStackOp
  | CODESIZE_EVM_NullStackOp : SortNullStackOp
  | COINBASE_EVM_NullStackOp : SortNullStackOp
  | DIFFICULTY_EVM_NullStackOp : SortNullStackOp
  | GAS_EVM_NullStackOp : SortNullStackOp
  | GASLIMIT_EVM_NullStackOp : SortNullStackOp
  | GASPRICE_EVM_NullStackOp : SortNullStackOp
  | JUMPDEST_EVM_NullStackOp : SortNullStackOp
  | MSIZE_EVM_NullStackOp : SortNullStackOp
  | NUMBER_EVM_NullStackOp : SortNullStackOp
  | ORIGIN_EVM_NullStackOp : SortNullStackOp
  | PC_EVM_NullStackOp : SortNullStackOp
  | PREVRANDAO_EVM_NullStackOp : SortNullStackOp
  | RETURNDATASIZE_EVM_NullStackOp : SortNullStackOp
  | SELFBALANCE_EVM_NullStackOp : SortNullStackOp
  | STOP_EVM_NullStackOp : SortNullStackOp
  | TIMESTAMP_EVM_NullStackOp : SortNullStackOp

inductive SortOpCode : Type where
  | inj_SortBinStackOp (x : SortBinStackOp) : SortOpCode
  | inj_SortCallOp (x : SortCallOp) : SortOpCode
  | inj_SortCallSixOp (x : SortCallSixOp) : SortOpCode
  | inj_SortInternalOp (x : SortInternalOp) : SortOpCode
  | inj_SortInvalidOp (x : SortInvalidOp) : SortOpCode
  | inj_SortLogOp (x : SortLogOp) : SortOpCode
  | inj_SortNullStackOp (x : SortNullStackOp) : SortOpCode
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortOpCode
  | inj_SortPushOp (x : SortPushOp) : SortOpCode
  | inj_SortQuadStackOp (x : SortQuadStackOp) : SortOpCode
  | inj_SortStackOp (x : SortStackOp) : SortOpCode
  | inj_SortTernStackOp (x : SortTernStackOp) : SortOpCode
  | inj_SortUnStackOp (x : SortUnStackOp) : SortOpCode
  | PUSHAsm (x0 : SortInt) (x1 : SortInt) : SortOpCode

inductive SortOpCodes : Type where
  | «.OpCodes_EVM-ASSEMBLY_OpCodes» : SortOpCodes
  | «_;__EVM-ASSEMBLY_OpCodes_OpCode_OpCodes» (x0 : SortOpCode) (x1 : SortOpCodes) : SortOpCodes

inductive SortPrecompiledOp : Type where
  | BLAKE2F_EVM_PrecompiledOp : SortPrecompiledOp
  | ECADD_EVM_PrecompiledOp : SortPrecompiledOp
  | ECMUL_EVM_PrecompiledOp : SortPrecompiledOp
  | ECPAIRING_EVM_PrecompiledOp : SortPrecompiledOp
  | ECREC_EVM_PrecompiledOp : SortPrecompiledOp
  | ID_EVM_PrecompiledOp : SortPrecompiledOp
  | MODEXP_EVM_PrecompiledOp : SortPrecompiledOp
  | RIP160_EVM_PrecompiledOp : SortPrecompiledOp
  | SHA256_EVM_PrecompiledOp : SortPrecompiledOp

inductive SortPushOp : Type where
  | PUSH (x0 : SortInt) : SortPushOp
  | PUSHZERO_EVM_PushOp : SortPushOp

inductive SortQuadStackOp : Type where
  | CREATE2_EVM_QuadStackOp : SortQuadStackOp
  | EXTCODECOPY_EVM_QuadStackOp : SortQuadStackOp

inductive SortSchedule : Type where
  | BERLIN_EVM : SortSchedule
  | BYZANTIUM_EVM : SortSchedule
  | CANCUN_EVM : SortSchedule
  | CONSTANTINOPLE_EVM : SortSchedule
  | DEFAULT_EVM : SortSchedule
  | FRONTIER_EVM : SortSchedule
  | HOMESTEAD_EVM : SortSchedule
  | ISTANBUL_EVM : SortSchedule
  | LONDON_EVM : SortSchedule
  | MERGE_EVM : SortSchedule
  | PETERSBURG_EVM : SortSchedule
  | SHANGHAI_EVM : SortSchedule
  | SPURIOUS_DRAGON_EVM : SortSchedule
  | TANGERINE_WHISTLE_EVM : SortSchedule

inductive SortScheduleConst : Type where
  | Gaccesslistaddress_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gaccessliststoragekey_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gbalance_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gbase_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gblockhash_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcall_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcallstipend_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcallvalue_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcodedeposit_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcoldaccountaccess_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcoldsload_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcopy_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gcreate_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecadd_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecmul_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecpaircoeff_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gecpairconst_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gexp_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gexpbyte_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gextcodecopy_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gextcodesize_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gfround_SCHEDULE_ScheduleConst : SortScheduleConst
  | Ghigh_SCHEDULE_ScheduleConst : SortScheduleConst
  | Ginitcodewordcost_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gjumpdest_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glog_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glogdata_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glogtopic_SCHEDULE_ScheduleConst : SortScheduleConst
  | Glow_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gmemory_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gmid_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gnewaccount_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gquadcoeff_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gquaddivisor_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gselfdestruct_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsha3_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsha3word_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsload_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsstorereset_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gsstoreset_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtransaction_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtxcreate_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtxdatanonzero_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gtxdatazero_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gverylow_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gwarmstoragedirtystore_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gwarmstorageread_SCHEDULE_ScheduleConst : SortScheduleConst
  | Gzero_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rb_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rmaxquotient_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rselfdestruct_SCHEDULE_ScheduleConst : SortScheduleConst
  | Rsstoreclear_SCHEDULE_ScheduleConst : SortScheduleConst
  | maxCodeSize_SCHEDULE_ScheduleConst : SortScheduleConst
  | maxInitCodeSize_SCHEDULE_ScheduleConst : SortScheduleConst

inductive SortScheduleFlag : Type where
  | Gemptyisnonexistent_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasaccesslist_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasbasefee_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasbeaconroot_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghaschainid_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghascreate2_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasdirtysstore_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasextcodehash_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasmaxinitcodesize_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasmcopy_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasprevrandao_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghaspushzero_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasrejectedfirstbyte_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasreturndata_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasrevert_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasselfbalance_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasshift_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghassstorestipend_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghasstaticcall_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghastransient_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Ghaswarmcoinbase_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Gselfdestructnewaccount_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Gstaticcalldepth_SCHEDULE_ScheduleFlag : SortScheduleFlag
  | Gzerovaluenewaccountgas_SCHEDULE_ScheduleFlag : SortScheduleFlag

inductive SortSignedness : Type where
  | signedBytes : SortSignedness
  | unsignedBytes : SortSignedness

inductive SortStackOp : Type where
  | DUP (x0 : SortInt) : SortStackOp
  | SWAP (x0 : SortInt) : SortStackOp

inductive SortStatusCode : Type where
  | inj_SortEndStatusCode (x : SortEndStatusCode) : SortStatusCode
  | inj_SortExceptionalStatusCode (x : SortExceptionalStatusCode) : SortStatusCode
  | «.StatusCode_NETWORK_StatusCode» : SortStatusCode
  | EVMC_INTERNAL_ERROR_NETWORK_StatusCode : SortStatusCode
  | EVMC_REJECTED_NETWORK_StatusCode : SortStatusCode

inductive SortSubstateLogEntry : Type where
  | logEntry (x0 : SortInt) (x1 : SortList) (x2 : SortBytes) : SortSubstateLogEntry

inductive SortTernStackOp : Type where
  | ADDMOD_EVM_TernStackOp : SortTernStackOp
  | CALLDATACOPY_EVM_TernStackOp : SortTernStackOp
  | CODECOPY_EVM_TernStackOp : SortTernStackOp
  | CREATE_EVM_TernStackOp : SortTernStackOp
  | MCOPY_EVM_TernStackOp : SortTernStackOp
  | MULMOD_EVM_TernStackOp : SortTernStackOp
  | RETURNDATACOPY_EVM_TernStackOp : SortTernStackOp

inductive SortTxData : Type where
  | inj_SortAccessListTx (x : SortAccessListTx) : SortTxData
  | inj_SortDynamicFeeTx (x : SortDynamicFeeTx) : SortTxData
  | inj_SortLegacyTx (x : SortLegacyTx) : SortTxData

inductive SortTxType : Type where
  | «.TxType_EVM-TYPES_TxType» : SortTxType
  | «AccessList_EVM-TYPES_TxType» : SortTxType
  | «DynamicFee_EVM-TYPES_TxType» : SortTxType
  | «Legacy_EVM-TYPES_TxType» : SortTxType

inductive SortUnStackOp : Type where
  | BALANCE_EVM_UnStackOp : SortUnStackOp
  | BLOCKHASH_EVM_UnStackOp : SortUnStackOp
  | CALLDATALOAD_EVM_UnStackOp : SortUnStackOp
  | EXTCODEHASH_EVM_UnStackOp : SortUnStackOp
  | EXTCODESIZE_EVM_UnStackOp : SortUnStackOp
  | ISZERO_EVM_UnStackOp : SortUnStackOp
  | JUMP_EVM_UnStackOp : SortUnStackOp
  | MLOAD_EVM_UnStackOp : SortUnStackOp
  | NOT_EVM_UnStackOp : SortUnStackOp
  | POP_EVM_UnStackOp : SortUnStackOp
  | SELFDESTRUCT_EVM_UnStackOp : SortUnStackOp
  | SLOAD_EVM_UnStackOp : SortUnStackOp
  | TLOAD_EVM_UnStackOp : SortUnStackOp

inductive SortWordStack : Type where
  | «.WordStack_EVM-TYPES_WordStack» : SortWordStack
  | «_:__EVM-TYPES_WordStack_Int_WordStack» (x0 : SortInt) (x1 : SortWordStack) : SortWordStack

inductive SortBalanceCell : Type where
  | mk (val : SortInt) : SortBalanceCell

inductive SortIdCell : Type where
  | mk (val : SortAccount) : SortIdCell

inductive SortCoinbaseCell : Type where
  | mk (val : SortInt) : SortCoinbaseCell

inductive SortBlockNonceCell : Type where
  | mk (val : SortInt) : SortBlockNonceCell

inductive SortTransientStorageCell : Type where
  | mk (val : SortMap) : SortTransientStorageCell

inductive SortTimestampCell : Type where
  | mk (val : SortInt) : SortTimestampCell

inductive SortStatusCodeCell : Type where
  | mk (val : SortStatusCode) : SortStatusCodeCell

inductive SortMessagesCell : Type where
  | mk (val : SortMessageCellMap) : SortMessagesCell

inductive SortScheduleCell : Type where
  | mk (val : SortSchedule) : SortScheduleCell

inductive SortPreviousHashCell : Type where
  | mk (val : SortInt) : SortPreviousHashCell

inductive SortCodeCell : Type where
  | mk (val : SortAccountCode) : SortCodeCell

inductive SortTxOrderCell : Type where
  | mk (val : SortList) : SortTxOrderCell

inductive SortOrigStorageCell : Type where
  | mk (val : SortMap) : SortOrigStorageCell

inductive SortStaticCell : Type where
  | mk (val : SortBool) : SortStaticCell

inductive SortKCell : Type where
  | mk (val : SortK) : SortKCell

inductive SortExitCodeCell : Type where
  | mk (val : SortInt) : SortExitCodeCell

inductive SortModeCell : Type where
  | mk (val : SortMode) : SortModeCell

inductive SortUseGasCell : Type where
  | mk (val : SortBool) : SortUseGasCell

inductive SortOmmersHashCell : Type where
  | mk (val : SortInt) : SortOmmersHashCell

inductive SortStateRootCell : Type where
  | mk (val : SortInt) : SortStateRootCell

inductive SortTransactionsRootCell : Type where
  | mk (val : SortInt) : SortTransactionsRootCell

inductive SortReceiptsRootCell : Type where
  | mk (val : SortInt) : SortReceiptsRootCell

inductive SortLogsBloomCell : Type where
  | mk (val : SortBytes) : SortLogsBloomCell

inductive SortDifficultyCell : Type where
  | mk (val : SortInt) : SortDifficultyCell

inductive SortNumberCell : Type where
  | mk (val : SortInt) : SortNumberCell

inductive SortGasLimitCell : Type where
  | mk (val : SortInt) : SortGasLimitCell

inductive SortGasUsedCell : Type where
  | mk (val : SortGas) : SortGasUsedCell

inductive SortExtraDataCell : Type where
  | mk (val : SortBytes) : SortExtraDataCell

inductive SortMixHashCell : Type where
  | mk (val : SortInt) : SortMixHashCell

inductive SortBaseFeeCell : Type where
  | mk (val : SortInt) : SortBaseFeeCell

inductive SortWithdrawalsRootCell : Type where
  | mk (val : SortInt) : SortWithdrawalsRootCell

inductive SortBlobGasUsedCell : Type where
  | mk (val : SortInt) : SortBlobGasUsedCell

inductive SortExcessBlobGasCell : Type where
  | mk (val : SortInt) : SortExcessBlobGasCell

inductive SortBeaconRootCell : Type where
  | mk (val : SortInt) : SortBeaconRootCell

inductive SortOmmerBlockHeadersCell : Type where
  | mk (val : SortJSON) : SortOmmerBlockHeadersCell

inductive SortValueCell : Type where
  | mk (val : SortInt) : SortValueCell

inductive SortRefundCell : Type where
  | mk (val : SortInt) : SortRefundCell

inductive SortOutputCell : Type where
  | mk (val : SortBytes) : SortOutputCell

inductive SortCallStackCell : Type where
  | mk (val : SortList) : SortCallStackCell

inductive SortInterimStatesCell : Type where
  | mk (val : SortList) : SortInterimStatesCell

inductive SortTouchedAccountsCell : Type where
  | mk (val : SortSet) : SortTouchedAccountsCell

inductive SortGasPriceCell : Type where
  | mk (val : SortInt) : SortGasPriceCell

inductive SortOriginCell : Type where
  | mk (val : SortAccount) : SortOriginCell

inductive SortBlockhashesCell : Type where
  | mk (val : SortList) : SortBlockhashesCell

inductive SortCallDepthCell : Type where
  | mk (val : SortInt) : SortCallDepthCell

inductive SortToCell : Type where
  | mk (val : SortAccount) : SortToCell

inductive SortTxChainIDCell : Type where
  | mk (val : SortInt) : SortTxChainIDCell

inductive SortAcctIDCell : Type where
  | mk (val : SortInt) : SortAcctIDCell

inductive SortTxAccessCell : Type where
  | mk (val : SortJSON) : SortTxAccessCell

inductive SortStorageCell : Type where
  | mk (val : SortMap) : SortStorageCell

inductive SortProgramCell : Type where
  | mk (val : SortBytes) : SortProgramCell

inductive SortGeneratedCounterCell : Type where
  | mk (val : SortInt) : SortGeneratedCounterCell

inductive SortAccessedAccountsCell : Type where
  | mk (val : SortSet) : SortAccessedAccountsCell

inductive SortTxMaxFeeCell : Type where
  | mk (val : SortInt) : SortTxMaxFeeCell

inductive SortTxGasLimitCell : Type where
  | mk (val : SortInt) : SortTxGasLimitCell

inductive SortGasCell : Type where
  | mk (val : SortGas) : SortGasCell

inductive SortChainIDCell : Type where
  | mk (val : SortInt) : SortChainIDCell

inductive SortAccountsCell : Type where
  | mk (val : SortAccountCellMap) : SortAccountsCell

inductive SortTxPendingCell : Type where
  | mk (val : SortList) : SortTxPendingCell

inductive SortJumpDestsCell : Type where
  | mk (val : SortBytes) : SortJumpDestsCell

inductive SortSigSCell : Type where
  | mk (val : SortBytes) : SortSigSCell

inductive SortDataCell : Type where
  | mk (val : SortBytes) : SortDataCell

inductive SortTxNonceCell : Type where
  | mk (val : SortInt) : SortTxNonceCell

inductive SortPcCell : Type where
  | mk (val : SortInt) : SortPcCell

inductive SortTxTypeCell : Type where
  | mk (val : SortTxType) : SortTxTypeCell

inductive SortSelfDestructCell : Type where
  | mk (val : SortSet) : SortSelfDestructCell

inductive SortLogCell : Type where
  | mk (val : SortList) : SortLogCell

inductive SortAccessedStorageCell : Type where
  | mk (val : SortMap) : SortAccessedStorageCell

inductive SortCallDataCell : Type where
  | mk (val : SortBytes) : SortCallDataCell

inductive SortMsgIDCell : Type where
  | mk (val : SortInt) : SortMsgIDCell

inductive SortTxGasPriceCell : Type where
  | mk (val : SortInt) : SortTxGasPriceCell

inductive SortSigVCell : Type where
  | mk (val : SortInt) : SortSigVCell

inductive SortSigRCell : Type where
  | mk (val : SortBytes) : SortSigRCell

inductive SortTxPriorityFeeCell : Type where
  | mk (val : SortInt) : SortTxPriorityFeeCell

inductive SortCallerCell : Type where
  | mk (val : SortAccount) : SortCallerCell

inductive SortCallValueCell : Type where
  | mk (val : SortInt) : SortCallValueCell

inductive SortWordStackCell : Type where
  | mk (val : SortWordStack) : SortWordStackCell

inductive SortLocalMemCell : Type where
  | mk (val : SortBytes) : SortLocalMemCell

inductive SortMemoryUsedCell : Type where
  | mk (val : SortInt) : SortMemoryUsedCell

inductive SortCallGasCell : Type where
  | mk (val : SortGas) : SortCallGasCell

inductive SortNonceCell : Type where
  | mk (val : SortInt) : SortNonceCell

structure SortBlockCell : Type where
  previousHash : SortPreviousHashCell
  ommersHash : SortOmmersHashCell
  coinbase : SortCoinbaseCell
  stateRoot : SortStateRootCell
  transactionsRoot : SortTransactionsRootCell
  receiptsRoot : SortReceiptsRootCell
  logsBloom : SortLogsBloomCell
  difficulty : SortDifficultyCell
  number : SortNumberCell
  gasLimit : SortGasLimitCell
  gasUsed : SortGasUsedCell
  timestamp : SortTimestampCell
  extraData : SortExtraDataCell
  mixHash : SortMixHashCell
  blockNonce : SortBlockNonceCell
  baseFee : SortBaseFeeCell
  withdrawalsRoot : SortWithdrawalsRootCell
  blobGasUsed : SortBlobGasUsedCell
  excessBlobGas : SortExcessBlobGasCell
  beaconRoot : SortBeaconRootCell
  ommerBlockHeaders : SortOmmerBlockHeadersCell

structure SortNetworkCell : Type where
  chainID : SortChainIDCell
  accounts : SortAccountsCell
  txOrder : SortTxOrderCell
  txPending : SortTxPendingCell
  messages : SortMessagesCell

structure SortSubstateCell : Type where
  selfDestruct : SortSelfDestructCell
  log : SortLogCell
  refund : SortRefundCell
  accessedAccounts : SortAccessedAccountsCell
  accessedStorage : SortAccessedStorageCell

structure SortMessageCell : Type where
  msgID : SortMsgIDCell
  txNonce : SortTxNonceCell
  txGasPrice : SortTxGasPriceCell
  txGasLimit : SortTxGasLimitCell
  to : SortToCell
  value : SortValueCell
  sigV : SortSigVCell
  sigR : SortSigRCell
  sigS : SortSigSCell
  data : SortDataCell
  txAccess : SortTxAccessCell
  txChainID : SortTxChainIDCell
  txPriorityFee : SortTxPriorityFeeCell
  txMaxFee : SortTxMaxFeeCell
  txType : SortTxTypeCell

structure SortCallStateCell : Type where
  program : SortProgramCell
  jumpDests : SortJumpDestsCell
  id : SortIdCell
  caller : SortCallerCell
  callData : SortCallDataCell
  callValue : SortCallValueCell
  wordStack : SortWordStackCell
  localMem : SortLocalMemCell
  pc : SortPcCell
  gas : SortGasCell
  memoryUsed : SortMemoryUsedCell
  callGas : SortCallGasCell
  static : SortStaticCell
  callDepth : SortCallDepthCell

structure SortAccountCell : Type where
  acctID : SortAcctIDCell
  balance : SortBalanceCell
  code : SortCodeCell
  storage : SortStorageCell
  origStorage : SortOrigStorageCell
  transientStorage : SortTransientStorageCell
  nonce : SortNonceCell

structure SortEvmCell : Type where
  output : SortOutputCell
  statusCode : SortStatusCodeCell
  callStack : SortCallStackCell
  interimStates : SortInterimStatesCell
  touchedAccounts : SortTouchedAccountsCell
  callState : SortCallStateCell
  substate : SortSubstateCell
  gasPrice : SortGasPriceCell
  origin : SortOriginCell
  blockhashes : SortBlockhashesCell
  block : SortBlockCell

structure SortEthereumCell : Type where
  evm : SortEvmCell
  network : SortNetworkCell

structure SortKevmCell : Type where
  k : SortKCell
  exitCode : SortExitCodeCell
  mode : SortModeCell
  schedule : SortScheduleCell
  useGas : SortUseGasCell
  ethereum : SortEthereumCell

structure SortGeneratedTopCell : Type where
  kevm : SortKevmCell
  generatedCounter : SortGeneratedCounterCell

abbrev SortAccountCellMap : Type := MapHook SortAcctIDCell SortAccountCell

abbrev SortList : Type := ListHook SortKItem

abbrev SortMap : Type := MapHook SortKItem SortKItem

abbrev SortMessageCellMap : Type := MapHook SortMsgIDCell SortMessageCell

abbrev SortSet : Type := SetHook SortKItem

@JuanCoRo
Copy link
Member

In the latest definition I'm seeing the following errors. We need not address them here though:

  1. The definition of SortKItem is throwing a timeout at 'whnf' error. This can be circumvented by increasing set_option maxHeartbeats, where the default is 200000. Currently, if we increase it to 204700 the error appears no longer.
  2. Since we're not importing Prelude.lean, the hooks at the end of the file produce an error. We might not care about this for the moment though!

@tothtamas28
Copy link
Contributor Author

  1. The definition of SortKItem is throwing a timeout at 'whnf' error.

Hopefully, the ordering described in #4732 will resolve this.

  1. Since we're not importing Prelude.lean, the hooks at the end of the file produce an error.

Yes, for now compiling the prelude and importing it is a manual step.

@tothtamas28 tothtamas28 marked this pull request as ready for review January 14, 2025 15:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JuanCoRo JuanCoRo Awaiting requested review from JuanCoRo

At least 1 approving review is required to merge this pull request.

Assignees

@tothtamas28 tothtamas28

Labels
lean4-backend
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Use structure instead of inductive where possible
2 participants
@tothtamas28 @JuanCoRo