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

Order sort declarations topologically #4735

Merged
merged 2 commits into from
Jan 16, 2025
Merged

Order sort declarations topologically #4735

merged 2 commits into from
Jan 16, 2025

Conversation

tothtamas28
Copy link
Contributor

  • Compute SCCs based on the dependencies between sorts
  • Generate mutual commands for each SCC in topological order
  • Generate a wrapper inductive for collections sorts for simplicity

@tothtamas28 tothtamas28 self-assigned this Jan 16, 2025
@tothtamas28
Copy link
Contributor Author

tothtamas28 commented Jan 16, 2025 •
edited
Loading

Generated Lean program (compiles in 2-3 mins with a large enough heartbeat bound).

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

inductive SortScheduleCell : Type where
  | «<schedule>» (x0 : SortSchedule) : SortScheduleCell

inductive SortTxTypeCell : Type where
  | «<txType>» (x0 : SortTxType) : SortTxTypeCell

inductive SortBalanceCell : Type where
  | «<balance>» (x0 : SortInt) : SortBalanceCell

inductive SortCoinbaseCell : Type where
  | «<coinbase>» (x0 : SortInt) : SortCoinbaseCell

inductive SortBlockNonceCell : Type where
  | «<blockNonce>» (x0 : SortInt) : SortBlockNonceCell

inductive SortTimestampCell : Type where
  | «<timestamp>» (x0 : SortInt) : SortTimestampCell

inductive SortPreviousHashCell : Type where
  | «<previousHash>» (x0 : SortInt) : SortPreviousHashCell

inductive SortValueCell : Type where
  | «<value>» (x0 : SortInt) : SortValueCell

inductive SortRefundCell : Type where
  | «<refund>» (x0 : SortInt) : SortRefundCell

inductive SortCallDepthCell : Type where
  | «<callDepth>» (x0 : SortInt) : SortCallDepthCell

inductive SortBlobGasUsedCell : Type where
  | «<blobGasUsed>» (x0 : SortInt) : SortBlobGasUsedCell

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

inductive SortTxChainIDCell : Type where
  | «<txChainID>» (x0 : SortInt) : SortTxChainIDCell

inductive SortAcctIDCell : Type where
  | «<acctID>» (x0 : SortInt) : SortAcctIDCell

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

inductive SortGeneratedCounterCell : Type where
  | «<generatedCounter>» (x0 : SortInt) : SortGeneratedCounterCell

inductive SortNumberCell : Type where
  | «<number>» (x0 : SortInt) : SortNumberCell

inductive SortTxMaxFeeCell : Type where
  | «<txMaxFee>» (x0 : SortInt) : SortTxMaxFeeCell

inductive SortTxGasLimitCell : Type where
  | «<txGasLimit>» (x0 : SortInt) : SortTxGasLimitCell

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

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

inductive SortExcessBlobGasCell : Type where
  | «<excessBlobGas>» (x0 : SortInt) : SortExcessBlobGasCell

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

inductive SortTxNonceCell : Type where
  | «<txNonce>» (x0 : SortInt) : SortTxNonceCell

inductive SortPcCell : Type where
  | «<pc>» (x0 : SortInt) : SortPcCell

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

inductive SortGasLimitCell : Type where
  | «<gasLimit>» (x0 : SortInt) : SortGasLimitCell

inductive SortTxGasPriceCell : Type where
  | «<txGasPrice>» (x0 : SortInt) : SortTxGasPriceCell

inductive SortGasPriceCell : Type where
  | «<gasPrice>» (x0 : SortInt) : SortGasPriceCell

inductive SortMemoryUsedCell : Type where
  | «<memoryUsed>» (x0 : SortInt) : SortMemoryUsedCell

inductive SortMsgIDCell : Type where
  | «<msgID>» (x0 : SortInt) : SortMsgIDCell

inductive SortBeaconRootCell : Type where
  | «<beaconRoot>» (x0 : SortInt) : SortBeaconRootCell

inductive SortBaseFeeCell : Type where
  | «<baseFee>» (x0 : SortInt) : SortBaseFeeCell

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

inductive SortTransactionsRootCell : Type where
  | «<transactionsRoot>» (x0 : SortInt) : SortTransactionsRootCell

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

inductive SortOmmersHashCell : Type where
  | «<ommersHash>» (x0 : SortInt) : SortOmmersHashCell

inductive SortMixHashCell : Type where
  | «<mixHash>» (x0 : SortInt) : SortMixHashCell

inductive SortCallValueCell : Type where
  | «<callValue>» (x0 : SortInt) : SortCallValueCell

inductive SortNonceCell : Type where
  | «<nonce>» (x0 : SortInt) : SortNonceCell

inductive SortWithdrawalsRootCell : Type where
  | «<withdrawalsRoot>» (x0 : SortInt) : SortWithdrawalsRootCell

inductive SortStateRootCell : Type where
  | «<stateRoot>» (x0 : SortInt) : SortStateRootCell

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

inductive SortSigVCell : Type where
  | «<sigV>» (x0 : SortInt) : SortSigVCell

inductive SortExitCodeCell : Type where
  | «<exit-code>» (x0 : SortInt) : SortExitCodeCell

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

inductive SortReceiptsRootCell : Type where
  | «<receiptsRoot>» (x0 : SortInt) : SortReceiptsRootCell

inductive SortTxPriorityFeeCell : Type where
  | «<txPriorityFee>» (x0 : SortInt) : SortTxPriorityFeeCell

inductive SortDifficultyCell : Type where
  | «<difficulty>» (x0 : SortInt) : SortDifficultyCell

inductive SortChainIDCell : Type where
  | «<chainID>» (x0 : SortInt) : SortChainIDCell

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

inductive SortExtraDataCell : Type where
  | «<extraData>» (x0 : SortBytes) : SortExtraDataCell

inductive SortProgramCell : Type where
  | «<program>» (x0 : SortBytes) : SortProgramCell

inductive SortJumpDestsCell : Type where
  | «<jumpDests>» (x0 : SortBytes) : SortJumpDestsCell

inductive SortSigSCell : Type where
  | «<sigS>» (x0 : SortBytes) : SortSigSCell

inductive SortOutputCell : Type where
  | «<output>» (x0 : SortBytes) : SortOutputCell

inductive SortDataCell : Type where
  | «<data>» (x0 : SortBytes) : SortDataCell

inductive SortCallDataCell : Type where
  | «<callData>» (x0 : SortBytes) : SortCallDataCell

inductive SortSigRCell : Type where
  | «<sigR>» (x0 : SortBytes) : SortSigRCell

inductive SortLocalMemCell : Type where
  | «<localMem>» (x0 : SortBytes) : SortLocalMemCell

inductive SortLogsBloomCell : Type where
  | «<logsBloom>» (x0 : SortBytes) : SortLogsBloomCell

inductive SortStaticCell : Type where
  | «<static>» (x0 : SortBool) : SortStaticCell

inductive SortUseGasCell : Type where
  | «<useGas>» (x0 : SortBool) : SortUseGasCell

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

inductive SortModeCell : Type where
  | «<mode>» (x0 : SortMode) : SortModeCell

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

inductive SortWordStackCell : Type where
  | «<wordStack>» (x0 : SortWordStack) : SortWordStackCell

inductive SortGasCell : Type where
  | «<gas>» (x0 : SortGas) : SortGasCell

inductive SortCallGasCell : Type where
  | «<callGas>» (x0 : SortGas) : SortCallGasCell

inductive SortGasUsedCell : Type where
  | «<gasUsed>» (x0 : SortGas) : SortGasUsedCell

inductive SortIdCell : Type where
  | «<id>» (x0 : SortAccount) : SortIdCell

inductive SortToCell : Type where
  | «<to>» (x0 : SortAccount) : SortToCell

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 SortOriginCell : Type where
  | «<origin>» (x0 : SortAccount) : SortOriginCell

inductive SortCallerCell : Type where
  | «<caller>» (x0 : SortAccount) : SortCallerCell

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 SortCodeCell : Type where
  | «<code>» (x0 : SortAccountCode) : SortCodeCell

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

inductive SortCallStateCell : Type where
  | «<callState>» (x0 : SortProgramCell) (x1 : SortJumpDestsCell) (x2 : SortIdCell) (x3 : SortCallerCell) (x4 : SortCallDataCell) (x5 : SortCallValueCell) (x6 : SortWordStackCell) (x7 : SortLocalMemCell) (x8 : SortPcCell) (x9 : SortGasCell) (x10 : SortMemoryUsedCell) (x11 : SortCallGasCell) (x12 : SortStaticCell) (x13 : SortCallDepthCell) : SortCallStateCell

inductive SortStatusCodeCell : Type where
  | «<statusCode>» (x0 : SortStatusCode) : SortStatusCodeCell

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

  inductive SortAccessedAccountsCell : Type where
    | «<accessedAccounts>» (x0 : SortSet) : SortAccessedAccountsCell

  inductive SortAccessedStorageCell : Type where
    | «<accessedStorage>» (x0 : SortMap) : SortAccessedStorageCell

  inductive SortAccountCell : Type where
    | «<account>» (x0 : SortAcctIDCell) (x1 : SortBalanceCell) (x2 : SortCodeCell) (x3 : SortStorageCell) (x4 : SortOrigStorageCell) (x5 : SortTransientStorageCell) (x6 : SortNonceCell) : SortAccountCell

  inductive SortAccountCellMap : Type where
    | mk (coll : List (SortAcctIDCell × SortAccountCell)) : SortAccountCellMap

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

  inductive SortAccountsCell : Type where
    | «<accounts>» (x0 : SortAccountCellMap) : SortAccountsCell

  inductive SortBlockCell : Type where
    | «<block>» (x0 : SortPreviousHashCell) (x1 : SortOmmersHashCell) (x2 : SortCoinbaseCell) (x3 : SortStateRootCell) (x4 : SortTransactionsRootCell) (x5 : SortReceiptsRootCell) (x6 : SortLogsBloomCell) (x7 : SortDifficultyCell) (x8 : SortNumberCell) (x9 : SortGasLimitCell) (x10 : SortGasUsedCell) (x11 : SortTimestampCell) (x12 : SortExtraDataCell) (x13 : SortMixHashCell) (x14 : SortBlockNonceCell) (x15 : SortBaseFeeCell) (x16 : SortWithdrawalsRootCell) (x17 : SortBlobGasUsedCell) (x18 : SortExcessBlobGasCell) (x19 : SortBeaconRootCell) (x20 : SortOmmerBlockHeadersCell) : SortBlockCell

  inductive SortBlockhashesCell : Type where
    | «<blockhashes>» (x0 : SortList) : SortBlockhashesCell

  inductive SortCallStackCell : Type where
    | «<callStack>» (x0 : SortList) : SortCallStackCell

  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 SortEthereumCell : Type where
    | «<ethereum>» (x0 : SortEvmCell) (x1 : SortNetworkCell) : SortEthereumCell

  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 SortEvmCell : Type where
    | «<evm>» (x0 : SortOutputCell) (x1 : SortStatusCodeCell) (x2 : SortCallStackCell) (x3 : SortInterimStatesCell) (x4 : SortTouchedAccountsCell) (x5 : SortCallStateCell) (x6 : SortSubstateCell) (x7 : SortGasPriceCell) (x8 : SortOriginCell) (x9 : SortBlockhashesCell) (x10 : SortBlockCell) : SortEvmCell

  inductive SortGeneratedTopCell : Type where
    | «<generatedTop>» (x0 : SortKevmCell) (x1 : SortGeneratedCounterCell) : SortGeneratedTopCell

  inductive SortInterimStatesCell : Type where
    | «<interimStates>» (x0 : SortList) : SortInterimStatesCell

  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

  inductive SortKCell : Type where
    | «<k>» (x0 : SortK) : SortKCell

  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 SortKevmCell : Type where
    | «<kevm>» (x0 : SortKCell) (x1 : SortExitCodeCell) (x2 : SortModeCell) (x3 : SortScheduleCell) (x4 : SortUseGasCell) (x5 : SortEthereumCell) : SortKevmCell

  inductive SortList : Type where
    | mk (coll : List SortKItem) : SortList

  inductive SortLogCell : Type where
    | «<log>» (x0 : SortList) : SortLogCell

  inductive SortMap : Type where
    | mk (coll : List (SortKItem × SortKItem)) : SortMap

  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 SortMessageCell : Type where
    | «<message>» (x0 : SortMsgIDCell) (x1 : SortTxNonceCell) (x2 : SortTxGasPriceCell) (x3 : SortTxGasLimitCell) (x4 : SortToCell) (x5 : SortValueCell) (x6 : SortSigVCell) (x7 : SortSigRCell) (x8 : SortSigSCell) (x9 : SortDataCell) (x10 : SortTxAccessCell) (x11 : SortTxChainIDCell) (x12 : SortTxPriorityFeeCell) (x13 : SortTxMaxFeeCell) (x14 : SortTxTypeCell) : SortMessageCell

  inductive SortMessageCellMap : Type where
    | mk (coll : List (SortMsgIDCell × SortMessageCell)) : SortMessageCellMap

  inductive SortMessagesCell : Type where
    | «<messages>» (x0 : SortMessageCellMap) : SortMessagesCell

  inductive SortNetworkCell : Type where
    | «<network>» (x0 : SortChainIDCell) (x1 : SortAccountsCell) (x2 : SortTxOrderCell) (x3 : SortTxPendingCell) (x4 : SortMessagesCell) : SortNetworkCell

  inductive SortOmmerBlockHeadersCell : Type where
    | «<ommerBlockHeaders>» (x0 : SortJSON) : SortOmmerBlockHeadersCell

  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 SortOrigStorageCell : Type where
    | «<origStorage>» (x0 : SortMap) : SortOrigStorageCell

  inductive SortSelfDestructCell : Type where
    | «<selfDestruct>» (x0 : SortSet) : SortSelfDestructCell

  inductive SortSet : Type where
    | mk (coll : List SortKItem) : SortSet

  inductive SortStorageCell : Type where
    | «<storage>» (x0 : SortMap) : SortStorageCell

  inductive SortSubstateCell : Type where
    | «<substate>» (x0 : SortSelfDestructCell) (x1 : SortLogCell) (x2 : SortRefundCell) (x3 : SortAccessedAccountsCell) (x4 : SortAccessedStorageCell) : SortSubstateCell

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

  inductive SortTouchedAccountsCell : Type where
    | «<touchedAccounts>» (x0 : SortSet) : SortTouchedAccountsCell

  inductive SortTransientStorageCell : Type where
    | «<transientStorage>» (x0 : SortMap) : SortTransientStorageCell

  inductive SortTxAccessCell : Type where
    | «<txAccess>» (x0 : SortJSON) : SortTxAccessCell

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

  inductive SortTxOrderCell : Type where
    | «<txOrder>» (x0 : SortList) : SortTxOrderCell

  inductive SortTxPendingCell : Type where
    | «<txPending>» (x0 : SortList) : SortTxPendingCell
end

@rv-jenkins rv-jenkins changed the base branch from master to develop January 16, 2025 12:35
@tothtamas28 tothtamas28 requested a review from JuanCoRo January 16, 2025 12:35
@tothtamas28 tothtamas28 mentioned this pull request Jan 16, 2025
Merged
@tothtamas28 tothtamas28 marked this pull request as ready for review January 16, 2025 13:49
@JuanCoRo
Copy link
Member

Maybe the generated definition could include a bound like set_option maxHeartbeats 10000000 since it'll be needed anyway, and it's also a sort of sanity check on what used to work. The maxHearbeats could also be a parameter passed

@tothtamas28
Copy link
Contributor Author

Maybe the generated definition could include a bound like set_option maxHeartbeats 10000000

Definitely, the final product should be such that imports, options, etc. are generated so that minimal to no user interaction is needed.

JuanCoRo
JuanCoRo approved these changes Jan 16, 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.

Nice!

@automergerpr-permission-manager automergerpr-permission-manager bot merged commit 03253f8 into develop Jan 16, 2025
19 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the sort-ordering branch January 16, 2025 20:02
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.
2 participants
@tothtamas28 @JuanCoRo