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 where possible #4731

Merged
merged 2 commits into from
Jan 17, 2025
Merged

Generate structure-s where possible #4731

merged 2 commits into from
Jan 17, 2025

Conversation

tothtamas28
Copy link
Contributor

@tothtamas28 tothtamas28 commented Jan 9, 2025 •
edited
Loading

Closes #4723
Closes #4732

For cells, if the cell is a leaf, a structure with a single field is generated:

structure SortGasCell : Type where
  val : SortGas

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

structure SortGeneratedTopCell : Type where
  kevm : SortKevmCell
  generatedCounter : SortGeneratedCounterCell

Additionally, collections have also been changed to structure-s:

structure SortMessageCellMap : Type where
    coll : List (SortMsgIDCell × SortMessageCell)

@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
Closed
@tothtamas28
Copy link
Contributor Author

tothtamas28 commented Jan 9, 2025 •
edited
Loading

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

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

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

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 SortSignedness : Type where
  | signedBytes : SortSignedness
  | unsignedBytes : SortSignedness

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 SortCallOp : Type where
  | CALL_EVM_CallOp : SortCallOp
  | CALLCODE_EVM_CallOp : SortCallOp

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 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 SortTxType : Type where
  | «.TxType_EVM-TYPES_TxType» : SortTxType
  | «AccessList_EVM-TYPES_TxType» : SortTxType
  | «DynamicFee_EVM-TYPES_TxType» : SortTxType
  | «Legacy_EVM-TYPES_TxType» : SortTxType

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 SortEndianness : Type where
  | bigEndianBytes : SortEndianness

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

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

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 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

structure SortScheduleCell : Type where
  val : SortSchedule

structure SortTxTypeCell : Type where
  val : SortTxType

structure SortBalanceCell : Type where
  val : SortInt

structure SortCoinbaseCell : Type where
  val : SortInt

structure SortBlockNonceCell : Type where
  val : SortInt

structure SortTimestampCell : Type where
  val : SortInt

structure SortPreviousHashCell : Type where
  val : SortInt

structure SortValueCell : Type where
  val : SortInt

structure SortRefundCell : Type where
  val : SortInt

structure SortCallDepthCell : Type where
  val : SortInt

structure SortBlobGasUsedCell : Type where
  val : SortInt

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

structure SortTxChainIDCell : Type where
  val : SortInt

structure SortAcctIDCell : Type where
  val : SortInt

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

structure SortGeneratedCounterCell : Type where
  val : SortInt

structure SortNumberCell : Type where
  val : SortInt

structure SortTxMaxFeeCell : Type where
  val : SortInt

structure SortTxGasLimitCell : Type where
  val : SortInt

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

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

structure SortExcessBlobGasCell : Type where
  val : SortInt

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

structure SortTxNonceCell : Type where
  val : SortInt

structure SortPcCell : Type where
  val : SortInt

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

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

structure SortGasLimitCell : Type where
  val : SortInt

structure SortTxGasPriceCell : Type where
  val : SortInt

structure SortGasPriceCell : Type where
  val : SortInt

structure SortMemoryUsedCell : Type where
  val : SortInt

structure SortMsgIDCell : Type where
  val : SortInt

structure SortBeaconRootCell : Type where
  val : SortInt

structure SortBaseFeeCell : Type where
  val : SortInt

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

structure SortTransactionsRootCell : Type where
  val : SortInt

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

structure SortOmmersHashCell : Type where
  val : SortInt

structure SortMixHashCell : Type where
  val : SortInt

structure SortCallValueCell : Type where
  val : SortInt

structure SortNonceCell : Type where
  val : SortInt

structure SortWithdrawalsRootCell : Type where
  val : SortInt

structure SortStateRootCell : Type where
  val : SortInt

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

structure SortSigVCell : Type where
  val : SortInt

structure SortExitCodeCell : Type where
  val : SortInt

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

structure SortReceiptsRootCell : Type where
  val : SortInt

structure SortTxPriorityFeeCell : Type where
  val : SortInt

structure SortDifficultyCell : Type where
  val : SortInt

structure SortChainIDCell : Type where
  val : SortInt

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

structure SortExtraDataCell : Type where
  val : SortBytes

structure SortProgramCell : Type where
  val : SortBytes

structure SortJumpDestsCell : Type where
  val : SortBytes

structure SortSigSCell : Type where
  val : SortBytes

structure SortOutputCell : Type where
  val : SortBytes

structure SortDataCell : Type where
  val : SortBytes

structure SortCallDataCell : Type where
  val : SortBytes

structure SortSigRCell : Type where
  val : SortBytes

structure SortLocalMemCell : Type where
  val : SortBytes

structure SortLogsBloomCell : Type where
  val : SortBytes

structure SortStaticCell : Type where
  val : SortBool

structure SortUseGasCell : Type where
  val : SortBool

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

structure SortModeCell : Type where
  val : SortMode

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

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

structure SortWordStackCell : Type where
  val : SortWordStack

structure SortGasCell : Type where
  val : SortGas

structure SortCallGasCell : Type where
  val : SortGas

structure SortGasUsedCell : Type where
  val : SortGas

structure SortIdCell : Type where
  val : SortAccount

structure SortToCell : Type where
  val : SortAccount

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

structure SortOriginCell : Type where
  val : SortAccount

structure SortCallerCell : Type where
  val : SortAccount

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

structure SortCodeCell : Type where
  val : SortAccountCode

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 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

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 SortStatusCodeCell : Type where
  val : SortStatusCode

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

  structure SortAccessedAccountsCell : Type where
    val : SortSet

  structure SortAccessedStorageCell : Type where
    val : SortMap

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

  structure SortAccountCellMap : Type where
    coll : List (SortAcctIDCell × SortAccountCell)

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

  structure SortAccountsCell : Type where
    val : SortAccountCellMap

  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 SortBlockhashesCell : Type where
    val : SortList

  structure SortCallStackCell : Type where
    val : SortList

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

  structure SortEthereumCell : Type where
    evm : SortEvmCell
    network : SortNetworkCell

  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

  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 SortGeneratedTopCell : Type where
    kevm : SortKevmCell
    generatedCounter : SortGeneratedCounterCell

  structure SortInterimStatesCell : Type where
    val : SortList

  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 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 SortJSONs : Type where
    | «.List{"JSONs"}» : SortJSONs
    | JSONs (x0 : SortJSON) (x1 : SortJSONs) : SortJSONs

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

  structure SortKCell : Type where
    val : 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

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

  structure SortList : Type where
    coll : List SortKItem

  structure SortLogCell : Type where
    val : SortList

  structure SortMap : Type where
    coll : List (SortKItem × SortKItem)

  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

  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 SortMessageCellMap : Type where
    coll : List (SortMsgIDCell × SortMessageCell)

  structure SortMessagesCell : Type where
    val : SortMessageCellMap

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

  structure SortOmmerBlockHeadersCell : Type where
    val : SortJSON

  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

  structure SortOrigStorageCell : Type where
    val : SortMap

  structure SortSelfDestructCell : Type where
    val : SortSet

  structure SortSet : Type where
    coll : List SortKItem

  structure SortStorageCell : Type where
    val : SortMap

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

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

  structure SortTouchedAccountsCell : Type where
    val : SortSet

  structure SortTransientStorageCell : Type where
    val : SortMap

  structure SortTxAccessCell : Type where
    val : SortJSON

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

  structure SortTxOrderCell : Type where
    val : SortList

  structure SortTxPendingCell : Type where
    val : SortList
end

@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
@tothtamas28 tothtamas28 marked this pull request as draft January 15, 2025 09:31
@tothtamas28 tothtamas28 changed the title Generate structure-s for non-leaf cells Generate structure-s for cell sorts Jan 16, 2025
@tothtamas28 tothtamas28 linked an issue Jan 16, 2025 that may be closed by this pull request
Generate structure-s for leaf cells #4732
Closed
@tothtamas28 tothtamas28 changed the base branch from develop to inj-class January 16, 2025 16:34
Base automatically changed from inj-class to develop January 17, 2025 10:43
@tothtamas28 tothtamas28 changed the title Generate structure-s for cell sorts Generate structure-s where possible Jan 17, 2025
@tothtamas28 tothtamas28 marked this pull request as ready for review January 17, 2025 11:24
@tothtamas28 tothtamas28 requested a review from JuanCoRo January 17, 2025 11:25
JuanCoRo
JuanCoRo approved these changes Jan 17, 2025
View reviewed changes
Copy link
Member

@JuanCoRo JuanCoRo left a comment

Choose a reason for hiding this comment

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

Awesome 🚀

@tothtamas28 tothtamas28 merged commit 57a3bfa into develop Jan 17, 2025
25 of 65 checks passed
@tothtamas28 tothtamas28 deleted the cell-structure branch January 17, 2025 14:53
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JuanCoRo JuanCoRo JuanCoRo approved these changes

Assignees

@tothtamas28 tothtamas28

Labels
automerge lean4-backend
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Generate structure-s for leaf cells Use structure instead of inductive where possible
2 participants
@tothtamas28 @JuanCoRo