Generate Lean 4 type definitions from a KORE definition

[tothtamas28]

• Add a prelude for basic primitive sorts
• Generate and inductive for each constructed sort
• Generate an abbrev for each collection sort

[tothtamas28]

Generates the following for the LLVM definition of evm-semantics.

Expand

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

inductive SortAccessedAccountsCell : Type where
  | Lbl'_LT_'accessedAccounts'_GT_' (x0 : SortSet) : SortAccessedAccountsCell

inductive SortAccessedStorageCell : Type where
  | Lbl'_LT_'accessedStorage'_GT_' (x0 : SortMap) : SortAccessedStorageCell

inductive SortAccount : Type where
  | inj_SortInt (x : SortInt) : SortAccount
  | Lbl'Stop'Account'Unds'EVM_TYPES'Unds'Account : SortAccount

inductive SortAccountCell : Type where
  | Lbl'_LT_'account'_GT_' (x0 : SortAcctIDCell) (x1 : SortBalanceCell) (x2 : SortCodeCell) (x3 : SortStorageCell) (x4 : SortOrigStorageCell) (x5 : SortTransientStorageCell) (x6 : SortNonceCell) : SortAccountCell

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

inductive SortAccounts : Type where
  | Lbl'LBraUndsPipeUndsRBraUnds'EVM'Unds'Accounts'Unds'AccountsCell'Unds'SubstateCell (x0 : SortAccountsCell) (x1 : SortSubstateCell) : SortAccounts

inductive SortAccountsCell : Type where
  | Lbl'_LT_'accounts'_GT_' (x0 : SortAccountCellMap) : SortAccountsCell

inductive SortAcctIDCell : Type where
  | Lbl'_LT_'acctID'_GT_' (x0 : SortInt) : SortAcctIDCell

inductive SortBExp : Type where
  | inj_SortBool (x : SortBool) : SortBExp
  | Lbl'Hash'accountNonexistent (x0 : SortInt) : SortBExp

inductive SortBalanceCell : Type where
  | Lbl'_LT_'balance'_GT_' (x0 : SortInt) : SortBalanceCell

inductive SortBaseFeeCell : Type where
  | Lbl'_LT_'baseFee'_GT_' (x0 : SortInt) : SortBaseFeeCell

inductive SortBeaconRootCell : Type where
  | Lbl'_LT_'beaconRoot'_GT_' (x0 : SortInt) : SortBeaconRootCell

inductive SortBinStackOp : Type where
  | inj_SortLogOp (x : SortLogOp) : SortBinStackOp
  | LblADD'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblAND'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblBYTE'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblDIV'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblEQ'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblEVMOR'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblEXP'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblGT'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblJUMPI'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblLT'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblMOD'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblMSTORE'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblMSTORE8'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblMUL'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblRETURN'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblREVERT'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSAR'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSDIV'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSGT'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSHA3'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSHL'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSHR'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSIGNEXTEND'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSLT'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSMOD'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSSTORE'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblSUB'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblTSTORE'Unds'EVM'Unds'BinStackOp : SortBinStackOp
  | LblXOR'Unds'EVM'Unds'BinStackOp : SortBinStackOp

inductive SortBlobGasUsedCell : Type where
  | Lbl'_LT_'blobGasUsed'_GT_' (x0 : SortInt) : SortBlobGasUsedCell

inductive SortBlockCell : Type where
  | Lbl'_LT_'block'_GT_' (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 SortBlockNonceCell : Type where
  | Lbl'_LT_'blockNonce'_GT_' (x0 : SortInt) : SortBlockNonceCell

inductive SortBlockhashesCell : Type where
  | Lbl'_LT_'blockhashes'_GT_' (x0 : SortList) : SortBlockhashesCell

inductive SortCallDataCell : Type where
  | Lbl'_LT_'callData'_GT_' (x0 : SortBytes) : SortCallDataCell

inductive SortCallDepthCell : Type where
  | Lbl'_LT_'callDepth'_GT_' (x0 : SortInt) : SortCallDepthCell

inductive SortCallGasCell : Type where
  | Lbl'_LT_'callGas'_GT_' (x0 : SortGas) : SortCallGasCell

inductive SortCallOp : Type where
  | LblCALL'Unds'EVM'Unds'CallOp : SortCallOp
  | LblCALLCODE'Unds'EVM'Unds'CallOp : SortCallOp

inductive SortCallSixOp : Type where
  | LblDELEGATECALL'Unds'EVM'Unds'CallSixOp : SortCallSixOp
  | LblSTATICCALL'Unds'EVM'Unds'CallSixOp : SortCallSixOp

inductive SortCallStackCell : Type where
  | Lbl'_LT_'callStack'_GT_' (x0 : SortList) : SortCallStackCell

inductive SortCallStateCell : Type where
  | Lbl'_LT_'callState'_GT_' (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 SortCallValueCell : Type where
  | Lbl'_LT_'callValue'_GT_' (x0 : SortInt) : SortCallValueCell

inductive SortCallerCell : Type where
  | Lbl'_LT_'caller'_GT_' (x0 : SortAccount) : SortCallerCell

inductive SortChainIDCell : Type where
  | Lbl'_LT_'chainID'_GT_' (x0 : SortInt) : SortChainIDCell

inductive SortCodeCell : Type where
  | Lbl'_LT_'code'_GT_' (x0 : SortAccountCode) : SortCodeCell

inductive SortCoinbaseCell : Type where
  | Lbl'_LT_'coinbase'_GT_' (x0 : SortInt) : SortCoinbaseCell

inductive SortDataCell : Type where
  | Lbl'_LT_'data'_GT_' (x0 : SortBytes) : SortDataCell

inductive SortDifficultyCell : Type where
  | Lbl'_LT_'difficulty'_GT_' (x0 : SortInt) : SortDifficultyCell

inductive SortDynamicFeeTx : Type where
  | LblDynamicFeeTxData (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
  | LblEVMC'Unds'REVERT'Unds'NETWORK'Unds'EndStatusCode : SortEndStatusCode
  | LblEVMC'Unds'SUCCESS'Unds'NETWORK'Unds'EndStatusCode : SortEndStatusCode

inductive SortEndianness : Type where
  | LblbigEndianBytes : SortEndianness

inductive SortEthereumCell : Type where
  | Lbl'_LT_'ethereum'_GT_' (x0 : SortEvmCell) (x1 : SortNetworkCell) : SortEthereumCell

inductive SortEthereumCommand : Type where
  | Lbl'Hash'executeBeaconRoots : SortEthereumCommand
  | Lbl'Hash'finalizeBlock'Unds'EVM'Unds'EthereumCommand : SortEthereumCommand
  | Lbl'Hash'finishTx'Unds'ETHEREUM_SIMULATION'Unds'EthereumCommand : SortEthereumCommand
  | Lbl'Hash'loadAccessList (x0 : SortJSON) : SortEthereumCommand
  | Lbl'Hash'loadAccessListAux (x0 : SortAccount) (x1 : SortList) : SortEthereumCommand
  | Lbl'Hash'rewardOmmers (x0 : SortJSONs) : SortEthereumCommand
  | Lbl'Hash'startBlock'Unds'EVM'Unds'EthereumCommand : SortEthereumCommand
  | Lblcheck'UndsUnds'ETHEREUM_SIMULATION'Unds'EthereumCommand'Unds'JSON (x0 : SortJSON) : SortEthereumCommand
  | Lblclear'Unds'STATE_UTILS'Unds'EthereumCommand : SortEthereumCommand
  | LblclearBLOCK'Unds'STATE_UTILS'Unds'EthereumCommand : SortEthereumCommand
  | LblclearNETWORK'Unds'STATE_UTILS'Unds'EthereumCommand : SortEthereumCommand
  | LblclearTX'Unds'STATE_UTILS'Unds'EthereumCommand : SortEthereumCommand
  | Lblexception'Unds'ETHEREUM_SIMULATION'Unds'EthereumCommand : SortEthereumCommand
  | Lblfailure'UndsUnds'ETHEREUM_SIMULATION'Unds'EthereumCommand'Unds'String (x0 : SortString) : SortEthereumCommand
  | Lblflush'Unds'ETHEREUM_SIMULATION'Unds'EthereumCommand : SortEthereumCommand
  | Lblload'UndsUnds'STATE_UTILS'Unds'EthereumCommand'Unds'JSON (x0 : SortJSON) : SortEthereumCommand
  | LblloadAccount'UndsUndsUnds'STATE_UTILS'Unds'EthereumCommand'Unds'Int'Unds'JSON (x0 : SortInt) (x1 : SortJSON) : SortEthereumCommand
  | LblloadTransaction'UndsUndsUnds'STATE_UTILS'Unds'EthereumCommand'Unds'Int'Unds'JSON (x0 : SortInt) (x1 : SortJSON) : SortEthereumCommand
  | LblloadTx (x0 : SortAccount) : SortEthereumCommand
  | LblmkAcct'UndsUnds'STATE_UTILS'Unds'EthereumCommand'Unds'Int (x0 : SortInt) : SortEthereumCommand
  | LblmkTX'UndsUnds'STATE_UTILS'Unds'EthereumCommand'Unds'Int (x0 : SortInt) : SortEthereumCommand
  | Lblprocess'UndsUnds'ETHEREUM_SIMULATION'Unds'EthereumCommand'Unds'JSON (x0 : SortJSON) : SortEthereumCommand
  | Lblrun'UndsUnds'ETHEREUM_SIMULATION'Unds'EthereumCommand'Unds'JSON (x0 : SortJSON) : SortEthereumCommand
  | Lblstart'Unds'ETHEREUM_SIMULATION'Unds'EthereumCommand : SortEthereumCommand
  | LblstartTx'Unds'ETHEREUM_SIMULATION'Unds'EthereumCommand : SortEthereumCommand
  | Lblstatus'UndsUnds'ETHEREUM_SIMULATION'Unds'EthereumCommand'Unds'StatusCode (x0 : SortStatusCode) : SortEthereumCommand
  | Lblsuccess'Unds'ETHEREUM_SIMULATION'Unds'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
  | Lbl'Stop'EthereumSimulation'Unds'ETHEREUM_SIMULATION'Unds'EthereumSimulation : SortEthereumSimulation
  | Lbl'UndsUndsUnds'ETHEREUM_SIMULATION'Unds'EthereumSimulation'Unds'EthereumCommand'Unds'EthereumSimulation (x0 : SortEthereumCommand) (x1 : SortEthereumSimulation) : SortEthereumSimulation

inductive SortEvmCell : Type where
  | Lbl'_LT_'evm'_GT_' (x0 : SortOutputCell) (x1 : SortStatusCodeCell) (x2 : SortCallStackCell) (x3 : SortInterimStatesCell) (x4 : SortTouchedAccountsCell) (x5 : SortCallStateCell) (x6 : SortSubstateCell) (x7 : SortGasPriceCell) (x8 : SortOriginCell) (x9 : SortBlockhashesCell) (x10 : SortBlockCell) : SortEvmCell

inductive SortExceptionalStatusCode : Type where
  | LblEVMC'Unds'ACCOUNT'Unds'ALREADY'Unds'EXISTS'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'BAD'Unds'JUMP'Unds'DESTINATION'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'BALANCE'Unds'UNDERFLOW'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'CALL'Unds'DEPTH'Unds'EXCEEDED'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'INVALID'Unds'INSTRUCTION'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'INVALID'Unds'MEMORY'Unds'ACCESS'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'NONCE'Unds'EXCEEDED'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'OUT'Unds'OF'Unds'GAS'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'PRECOMPILE'Unds'FAILURE'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'STACK'Unds'OVERFLOW'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'STACK'Unds'UNDERFLOW'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'STATIC'Unds'MODE'Unds'VIOLATION'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode
  | LblEVMC'Unds'UNDEFINED'Unds'INSTRUCTION'Unds'NETWORK'Unds'ExceptionalStatusCode : SortExceptionalStatusCode

inductive SortExcessBlobGasCell : Type where
  | Lbl'_LT_'excessBlobGas'_GT_' (x0 : SortInt) : SortExcessBlobGasCell

inductive SortExitCodeCell : Type where
  | Lbl'_LT_'exit_code'_GT_' (x0 : SortInt) : SortExitCodeCell

inductive SortExp : Type where
  | inj_SortGas (x : SortGas) : SortExp
  | inj_SortInt (x : SortInt) : SortExp
  | LblCcall (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortGas) (x3 : SortGas) (x4 : SortInt) (x5 : SortBool) : SortExp
  | LblCcallgas (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortGas) (x3 : SortGas) (x4 : SortInt) (x5 : SortBool) : SortExp
  | LblCselfdestruct (x0 : SortSchedule) (x1 : SortBExp) (x2 : SortInt) : SortExp

inductive SortExtraDataCell : Type where
  | Lbl'_LT_'extraData'_GT_' (x0 : SortBytes) : SortExtraDataCell

inductive SortG1Point : Type where
  | Lbl'LParUndsCommUndsRParUnds'KRYPTO'Unds'G1Point'Unds'Int'Unds'Int (x0 : SortInt) (x1 : SortInt) : SortG1Point

inductive SortG2Point : Type where
  | Lbl'LParUnds'x'UndsCommUnds'x'UndsRParUnds'KRYPTO'Unds'G2Point'Unds'Int'Unds'Int'Unds'Int'Unds'Int (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : SortG2Point

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

inductive SortGasCell : Type where
  | Lbl'_LT_'gas'_GT_' (x0 : SortGas) : SortGasCell

inductive SortGasLimitCell : Type where
  | Lbl'_LT_'gasLimit'_GT_' (x0 : SortInt) : SortGasLimitCell

inductive SortGasPriceCell : Type where
  | Lbl'_LT_'gasPrice'_GT_' (x0 : SortInt) : SortGasPriceCell

inductive SortGasUsedCell : Type where
  | Lbl'_LT_'gasUsed'_GT_' (x0 : SortGas) : SortGasUsedCell

inductive SortGeneratedCounterCell : Type where
  | Lbl'_LT_'generatedCounter'_GT_' (x0 : SortInt) : SortGeneratedCounterCell

inductive SortGeneratedTopCell : Type where
  | Lbl'_LT_'generatedTop'_GT_' (x0 : SortKevmCell) (x1 : SortGeneratedCounterCell) : SortGeneratedTopCell

inductive SortIdCell : Type where
  | Lbl'_LT_'id'_GT_' (x0 : SortAccount) : SortIdCell

inductive SortInterimStatesCell : Type where
  | Lbl'_LT_'interimStates'_GT_' (x0 : SortList) : SortInterimStatesCell

inductive SortInternalOp : Type where
  | Lbl'Hash'access'LSqBUndsCommUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode'Unds'OpCode (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | Lbl'Hash'addr'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode (x0 : SortOpCode) : SortInternalOp
  | Lbl'Hash'allocateCallGas'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'allocateCreateGas'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'call'UndsUndsUndsUndsUndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int'Unds'Int'Unds'Int'Unds'Int'Unds'Bytes'Unds'Bool (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortBytes) (x6 : SortBool) : SortInternalOp
  | Lbl'Hash'callWithCode'UndsUndsUndsUndsUndsUndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int'Unds'Int'Unds'Bytes'Unds'Int'Unds'Int'Unds'Bytes'Unds'Bool (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) (x5 : SortInt) (x6 : SortBytes) (x7 : SortBool) : SortInternalOp
  | Lbl'Hash'checkBalanceUnderflow'UndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | Lbl'Hash'checkCall'UndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | Lbl'Hash'checkCreate'UndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int (x0 : SortInt) (x1 : SortInt) : SortInternalOp
  | Lbl'Hash'checkDepthExceeded'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'checkNonceExceeded'UndsUnds'EVM'Unds'InternalOp'Unds'Int (x0 : SortInt) : SortInternalOp
  | Lbl'Hash'checkPoint'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'create'UndsUndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int'Unds'Int'Unds'Bytes (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : SortInternalOp
  | Lbl'Hash'deductGas'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'deductMemory'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'deductMemoryGas'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'deleteAccounts (x0 : SortList) : SortInternalOp
  | Lbl'Hash'dropCallStack'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'dropWorldState'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'ecadd (x0 : SortG1Point) (x1 : SortG1Point) : SortInternalOp
  | Lbl'Hash'ecmul (x0 : SortG1Point) (x1 : SortInt) : SortInternalOp
  | Lbl'Hash'ecpairing (x0 : SortList) (x1 : SortList) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) : SortInternalOp
  | Lbl'Hash'endBasicBlock'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'exec'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode (x0 : SortOpCode) : SortInternalOp
  | Lbl'Hash'finalizeStorage (x0 : SortList) : SortInternalOp
  | Lbl'Hash'finalizeTx (x0 : SortBool) : SortInternalOp
  | Lbl'Hash'gas'LSqBUndsCommUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode'Unds'OpCode (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | Lbl'Hash'gas'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode (x0 : SortOpCode) : SortInternalOp
  | Lbl'Hash'gasAccess (x0 : SortSchedule) (x1 : SortOpCode) : SortInternalOp
  | Lbl'Hash'gasExec (x0 : SortSchedule) (x1 : SortOpCode) : SortInternalOp
  | Lbl'Hash'incrementNonce'UndsUnds'EVM'Unds'InternalOp'Unds'Int (x0 : SortInt) : SortInternalOp
  | Lbl'Hash'memory'LSqBUndsCommUndsRSqBUnds'EVM'Unds'InternalOp'Unds'OpCode'Unds'OpCode (x0 : SortOpCode) (x1 : SortOpCode) : SortInternalOp
  | Lbl'Hash'mkCall'UndsUndsUndsUndsUndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int'Unds'Int'Unds'Bytes'Unds'Int'Unds'Bytes'Unds'Bool (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) (x4 : SortInt) (x5 : SortBytes) (x6 : SortBool) : SortInternalOp
  | Lbl'Hash'mkCreate'UndsUndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int'Unds'Int'Unds'Bytes (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : SortInternalOp
  | Lbl'Hash'newAccount'UndsUnds'EVM'Unds'InternalOp'Unds'Int (x0 : SortInt) : SortInternalOp
  | Lbl'Hash'newExistingAccount'UndsUnds'EVM'Unds'InternalOp'Unds'Int (x0 : SortInt) : SortInternalOp
  | Lbl'Hash'next'LSqBUndsRSqBUnds'EVM'Unds'InternalOp'Unds'MaybeOpCode (x0 : SortMaybeOpCode) : SortInternalOp
  | Lbl'Hash'popCallStack'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'popWorldState'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'precompiled'QuesLParUndsCommUndsRParUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Schedule (x0 : SortInt) (x1 : SortSchedule) : SortInternalOp
  | Lbl'Hash'push'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'pushCallStack'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'pushWorldState'Unds'EVM'Unds'InternalOp : SortInternalOp
  | Lbl'Hash'refund'UndsUnds'EVM'Unds'InternalOp'Unds'Gas (x0 : SortGas) : SortInternalOp
  | Lbl'Hash'setLocalMem'UndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int'Unds'Bytes (x0 : SortInt) (x1 : SortInt) (x2 : SortBytes) : SortInternalOp
  | Lbl'Hash'setStack'UndsUnds'EVM'Unds'InternalOp'Unds'WordStack (x0 : SortWordStack) : SortInternalOp
  | Lbl'Hash'transferFunds'UndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int'Unds'Int (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | Lbl'Hash'transferFundsToNonExistent'UndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'Int'Unds'Int'Unds'Int (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'StackOp'Unds'WordStack (x0 : SortStackOp) (x1 : SortWordStack) : SortInternalOp
  | Lbl'UndsUndsUnds'EVM'Unds'InternalOp'Unds'UnStackOp'Unds'Int (x0 : SortUnStackOp) (x1 : SortInt) : SortInternalOp
  | Lbl'UndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'BinStackOp'Unds'Int'Unds'Int (x0 : SortBinStackOp) (x1 : SortInt) (x2 : SortInt) : SortInternalOp
  | Lbl'UndsUndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'TernStackOp'Unds'Int'Unds'Int'Unds'Int (x0 : SortTernStackOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : SortInternalOp
  | Lbl'UndsUndsUndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'QuadStackOp'Unds'Int'Unds'Int'Unds'Int'Unds'Int (x0 : SortQuadStackOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) : SortInternalOp
  | Lbl'UndsUndsUndsUndsUndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'CallSixOp'Unds'Int'Unds'Int'Unds'Int'Unds'Int'Unds'Int'Unds'Int (x0 : SortCallSixOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortInt) : SortInternalOp
  | Lbl'UndsUndsUndsUndsUndsUndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'CallOp'Unds'Int'Unds'Int'Unds'Int'Unds'Int'Unds'Int'Unds'Int'Unds'Int (x0 : SortCallOp) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortInt) (x7 : SortInt) : SortInternalOp
  | Lblpc (x0 : SortOpCode) : SortInternalOp

inductive SortInvalidOp : Type where
  | LblINVALID'Unds'EVM'Unds'InvalidOp : SortInvalidOp
  | LblUNDEFINED'LParUndsRParUnds'EVM'Unds'InvalidOp'Unds'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
  | LblJSONEntry (x0 : SortJSONKey) (x1 : SortJSON) : SortJSON
  | LblJSONList (x0 : SortJSONs) : SortJSON
  | LblJSONObject (x0 : SortJSONs) : SortJSON
  | LblJSONnull : SortJSON

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

inductive SortJSONs : Type where
  | Lbl'Stop'List'LBraQuot'JSONs'QuotRBra' : SortJSONs
  | LblJSONs (x0 : SortJSON) (x1 : SortJSONs) : SortJSONs

inductive SortJumpDestsCell : Type where
  | Lbl'_LT_'jumpDests'_GT_' (x0 : SortBytes) : SortJumpDestsCell

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

inductive SortKCell : Type where
  | Lbl'_LT_'k'_GT_' (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
  | Lbl'Hash'accessAccounts'UndsUnds'EVM'Unds'KItem'Unds'Account (x0 : SortAccount) : SortKItem
  | Lbl'Hash'accessAccounts'UndsUnds'EVM'Unds'KItem'Unds'Set (x0 : SortSet) : SortKItem
  | Lbl'Hash'accessAccounts'UndsUndsUnds'EVM'Unds'KItem'Unds'Account'Unds'Account (x0 : SortAccount) (x1 : SortAccount) : SortKItem
  | Lbl'Hash'accessAccounts'UndsUndsUndsUnds'EVM'Unds'KItem'Unds'Account'Unds'Account'Unds'Set (x0 : SortAccount) (x1 : SortAccount) (x2 : SortSet) : SortKItem
  | Lbl'Hash'accessStorage'UndsUndsUnds'EVM'Unds'KItem'Unds'Account'Unds'Int (x0 : SortAccount) (x1 : SortInt) : SortKItem
  | Lbl'Hash'codeDeposit'UndsUnds'EVM'Unds'KItem'Unds'Int (x0 : SortInt) : SortKItem
  | Lbl'Hash'finishCodeDeposit'UndsUndsUnds'EVM'Unds'KItem'Unds'Int'Unds'Bytes (x0 : SortInt) (x1 : SortBytes) : SortKItem
  | Lbl'Hash'freezerCcall1'Unds' (x0 : SortK) (x1 : SortK) (x2 : SortK) (x3 : SortK) (x4 : SortK) : SortKItem
  | Lbl'Hash'freezerCcallgas1'Unds' (x0 : SortK) (x1 : SortK) (x2 : SortK) (x3 : SortK) (x4 : SortK) : SortKItem
  | Lbl'Hash'freezerCselfdestruct1'Unds' (x0 : SortK) (x1 : SortK) : SortKItem
  | Lbl'Hash'initVM'Unds'EVM'Unds'KItem : SortKItem
  | Lbl'Hash'mkCodeDeposit'UndsUnds'EVM'Unds'KItem'Unds'Int (x0 : SortInt) : SortKItem
  | Lbl'Hash'return'UndsUndsUnds'EVM'Unds'KItem'Unds'Int'Unds'Int (x0 : SortInt) (x1 : SortInt) : SortKItem
  | Lbl'Hash'touchAccounts'UndsUnds'EVM'Unds'KItem'Unds'Account (x0 : SortAccount) : SortKItem
  | Lbl'Hash'touchAccounts'UndsUndsUnds'EVM'Unds'KItem'Unds'Account'Unds'Account (x0 : SortAccount) (x1 : SortAccount) : SortKItem
  | Lblend (x0 : SortStatusCode) : SortKItem
  | Lblexecute : SortKItem
  | Lblhalt : SortKItem
  | LblloadCallState'UndsUnds'STATE_UTILS'Unds'KItem'Unds'JSON (x0 : SortJSON) : SortKItem
  | LblloadProgram (x0 : SortBytes) : SortKItem

inductive SortKevmCell : Type where
  | Lbl'_LT_'kevm'_GT_' (x0 : SortKCell) (x1 : SortExitCodeCell) (x2 : SortModeCell) (x3 : SortScheduleCell) (x4 : SortUseGasCell) (x5 : SortEthereumCell) : SortKevmCell

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

inductive SortLengthPrefix : Type where
  | Lbl'UndsLParUndsCommUndsRParUnds'SERIALIZATION'Unds'LengthPrefix'Unds'LengthPrefixType'Unds'Int'Unds'Int (x0 : SortLengthPrefixType) (x1 : SortInt) (x2 : SortInt) : SortLengthPrefix

inductive SortLengthPrefixType : Type where
  | Lbl'Hash'list'Unds'SERIALIZATION'Unds'LengthPrefixType : SortLengthPrefixType
  | Lbl'Hash'str'Unds'SERIALIZATION'Unds'LengthPrefixType : SortLengthPrefixType

inductive SortLocalMemCell : Type where
  | Lbl'_LT_'localMem'_GT_' (x0 : SortBytes) : SortLocalMemCell

inductive SortLogCell : Type where
  | Lbl'_LT_'log'_GT_' (x0 : SortList) : SortLogCell

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

inductive SortLogsBloomCell : Type where
  | Lbl'_LT_'logsBloom'_GT_' (x0 : SortBytes) : SortLogsBloomCell

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
  | Lbl'Stop'NoOpCode'Unds'EVM'Unds'MaybeOpCode : SortMaybeOpCode

inductive SortMemoryUsedCell : Type where
  | Lbl'_LT_'memoryUsed'_GT_' (x0 : SortInt) : SortMemoryUsedCell

inductive SortMessageCell : Type where
  | Lbl'_LT_'message'_GT_' (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 SortMessagesCell : Type where
  | Lbl'_LT_'messages'_GT_' (x0 : SortMessageCellMap) : SortMessagesCell

inductive SortMixHashCell : Type where
  | Lbl'_LT_'mixHash'_GT_' (x0 : SortInt) : SortMixHashCell

inductive SortMode : Type where
  | LblNORMAL : SortMode
  | LblSUCCESS'Unds'ETHEREUM_SIMULATION'Unds'Mode : SortMode
  | LblVMTESTS : SortMode

inductive SortModeCell : Type where
  | Lbl'_LT_'mode'_GT_' (x0 : SortMode) : SortModeCell

inductive SortMsgIDCell : Type where
  | Lbl'_LT_'msgID'_GT_' (x0 : SortInt) : SortMsgIDCell

inductive SortNetworkCell : Type where
  | Lbl'_LT_'network'_GT_' (x0 : SortChainIDCell) (x1 : SortAccountsCell) (x2 : SortTxOrderCell) (x3 : SortTxPendingCell) (x4 : SortMessagesCell) : SortNetworkCell

inductive SortNonceCell : Type where
  | Lbl'_LT_'nonce'_GT_' (x0 : SortInt) : SortNonceCell

inductive SortNullStackOp : Type where
  | inj_SortPrecompiledOp (x : SortPrecompiledOp) : SortNullStackOp
  | LblADDRESS'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblBASEFEE'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblCALLDATASIZE'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblCALLER'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblCALLVALUE'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblCHAINID'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblCODESIZE'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblCOINBASE'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblDIFFICULTY'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblGAS'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblGASLIMIT'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblGASPRICE'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblJUMPDEST'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblMSIZE'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblNUMBER'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblORIGIN'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblPC'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblPREVRANDAO'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblRETURNDATASIZE'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblSELFBALANCE'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblSTOP'Unds'EVM'Unds'NullStackOp : SortNullStackOp
  | LblTIMESTAMP'Unds'EVM'Unds'NullStackOp : SortNullStackOp

inductive SortNumberCell : Type where
  | Lbl'_LT_'number'_GT_' (x0 : SortInt) : SortNumberCell

inductive SortOmmerBlockHeadersCell : Type where
  | Lbl'_LT_'ommerBlockHeaders'_GT_' (x0 : SortJSON) : SortOmmerBlockHeadersCell

inductive SortOmmersHashCell : Type where
  | Lbl'_LT_'ommersHash'_GT_' (x0 : SortInt) : SortOmmersHashCell

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
  | LblPUSHAsm (x0 : SortInt) (x1 : SortInt) : SortOpCode

inductive SortOpCodes : Type where
  | Lbl'Stop'OpCodes'Unds'EVM_ASSEMBLY'Unds'OpCodes : SortOpCodes
  | Lbl'UndsSClnUndsUnds'EVM_ASSEMBLY'Unds'OpCodes'Unds'OpCode'Unds'OpCodes (x0 : SortOpCode) (x1 : SortOpCodes) : SortOpCodes

inductive SortOrigStorageCell : Type where
  | Lbl'_LT_'origStorage'_GT_' (x0 : SortMap) : SortOrigStorageCell

inductive SortOriginCell : Type where
  | Lbl'_LT_'origin'_GT_' (x0 : SortAccount) : SortOriginCell

inductive SortOutputCell : Type where
  | Lbl'_LT_'output'_GT_' (x0 : SortBytes) : SortOutputCell

inductive SortPcCell : Type where
  | Lbl'_LT_'pc'_GT_' (x0 : SortInt) : SortPcCell

inductive SortPrecompiledOp : Type where
  | LblBLAKE2F'Unds'EVM'Unds'PrecompiledOp : SortPrecompiledOp
  | LblECADD'Unds'EVM'Unds'PrecompiledOp : SortPrecompiledOp
  | LblECMUL'Unds'EVM'Unds'PrecompiledOp : SortPrecompiledOp
  | LblECPAIRING'Unds'EVM'Unds'PrecompiledOp : SortPrecompiledOp
  | LblECREC'Unds'EVM'Unds'PrecompiledOp : SortPrecompiledOp
  | LblID'Unds'EVM'Unds'PrecompiledOp : SortPrecompiledOp
  | LblMODEXP'Unds'EVM'Unds'PrecompiledOp : SortPrecompiledOp
  | LblRIP160'Unds'EVM'Unds'PrecompiledOp : SortPrecompiledOp
  | LblSHA256'Unds'EVM'Unds'PrecompiledOp : SortPrecompiledOp

inductive SortPreviousHashCell : Type where
  | Lbl'_LT_'previousHash'_GT_' (x0 : SortInt) : SortPreviousHashCell

inductive SortProgramCell : Type where
  | Lbl'_LT_'program'_GT_' (x0 : SortBytes) : SortProgramCell

inductive SortPushOp : Type where
  | LblPUSH (x0 : SortInt) : SortPushOp
  | LblPUSHZERO'Unds'EVM'Unds'PushOp : SortPushOp

inductive SortQuadStackOp : Type where
  | LblCREATE2'Unds'EVM'Unds'QuadStackOp : SortQuadStackOp
  | LblEXTCODECOPY'Unds'EVM'Unds'QuadStackOp : SortQuadStackOp

inductive SortReceiptsRootCell : Type where
  | Lbl'_LT_'receiptsRoot'_GT_' (x0 : SortInt) : SortReceiptsRootCell

inductive SortRefundCell : Type where
  | Lbl'_LT_'refund'_GT_' (x0 : SortInt) : SortRefundCell

inductive SortSchedule : Type where
  | LblBERLIN'Unds'EVM : SortSchedule
  | LblBYZANTIUM'Unds'EVM : SortSchedule
  | LblCANCUN'Unds'EVM : SortSchedule
  | LblCONSTANTINOPLE'Unds'EVM : SortSchedule
  | LblDEFAULT'Unds'EVM : SortSchedule
  | LblFRONTIER'Unds'EVM : SortSchedule
  | LblHOMESTEAD'Unds'EVM : SortSchedule
  | LblISTANBUL'Unds'EVM : SortSchedule
  | LblLONDON'Unds'EVM : SortSchedule
  | LblMERGE'Unds'EVM : SortSchedule
  | LblPETERSBURG'Unds'EVM : SortSchedule
  | LblSHANGHAI'Unds'EVM : SortSchedule
  | LblSPURIOUS'Unds'DRAGON'Unds'EVM : SortSchedule
  | LblTANGERINE'Unds'WHISTLE'Unds'EVM : SortSchedule

inductive SortScheduleCell : Type where
  | Lbl'_LT_'schedule'_GT_' (x0 : SortSchedule) : SortScheduleCell

inductive SortScheduleConst : Type where
  | LblGaccesslistaddress'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGaccessliststoragekey'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGbalance'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGbase'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGblockhash'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGcall'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGcallstipend'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGcallvalue'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGcodedeposit'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGcoldaccountaccess'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGcoldsload'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGcopy'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGcreate'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGecadd'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGecmul'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGecpaircoeff'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGecpairconst'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGexp'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGexpbyte'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGextcodecopy'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGextcodesize'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGfround'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGhigh'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGinitcodewordcost'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGjumpdest'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGlog'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGlogdata'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGlogtopic'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGlow'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGmemory'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGmid'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGnewaccount'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGquadcoeff'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGquaddivisor'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGselfdestruct'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGsha3'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGsha3word'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGsload'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGsstorereset'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGsstoreset'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGtransaction'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGtxcreate'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGtxdatanonzero'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGtxdatazero'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGverylow'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGwarmstoragedirtystore'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGwarmstorageread'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblGzero'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblRb'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblRmaxquotient'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblRselfdestruct'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblRsstoreclear'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblmaxCodeSize'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst
  | LblmaxInitCodeSize'Unds'SCHEDULE'Unds'ScheduleConst : SortScheduleConst

inductive SortScheduleFlag : Type where
  | LblGemptyisnonexistent'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasaccesslist'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasbasefee'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasbeaconroot'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhaschainid'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhascreate2'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasdirtysstore'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasextcodehash'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasmaxinitcodesize'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasmcopy'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasprevrandao'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhaspushzero'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasrejectedfirstbyte'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasreturndata'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasrevert'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasselfbalance'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasshift'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhassstorestipend'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhasstaticcall'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhastransient'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGhaswarmcoinbase'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGselfdestructnewaccount'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGstaticcalldepth'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag
  | LblGzerovaluenewaccountgas'Unds'SCHEDULE'Unds'ScheduleFlag : SortScheduleFlag

inductive SortSelfDestructCell : Type where
  | Lbl'_LT_'selfDestruct'_GT_' (x0 : SortSet) : SortSelfDestructCell

inductive SortSigRCell : Type where
  | Lbl'_LT_'sigR'_GT_' (x0 : SortBytes) : SortSigRCell

inductive SortSigSCell : Type where
  | Lbl'_LT_'sigS'_GT_' (x0 : SortBytes) : SortSigSCell

inductive SortSigVCell : Type where
  | Lbl'_LT_'sigV'_GT_' (x0 : SortInt) : SortSigVCell

inductive SortSignedness : Type where
  | LblsignedBytes : SortSignedness
  | LblunsignedBytes : SortSignedness

inductive SortStackOp : Type where
  | LblDUP (x0 : SortInt) : SortStackOp
  | LblSWAP (x0 : SortInt) : SortStackOp

inductive SortStateRootCell : Type where
  | Lbl'_LT_'stateRoot'_GT_' (x0 : SortInt) : SortStateRootCell

inductive SortStaticCell : Type where
  | Lbl'_LT_'static'_GT_' (x0 : SortBool) : SortStaticCell

inductive SortStatusCode : Type where
  | inj_SortEndStatusCode (x : SortEndStatusCode) : SortStatusCode
  | inj_SortExceptionalStatusCode (x : SortExceptionalStatusCode) : SortStatusCode
  | Lbl'Stop'StatusCode'Unds'NETWORK'Unds'StatusCode : SortStatusCode
  | LblEVMC'Unds'INTERNAL'Unds'ERROR'Unds'NETWORK'Unds'StatusCode : SortStatusCode
  | LblEVMC'Unds'REJECTED'Unds'NETWORK'Unds'StatusCode : SortStatusCode

inductive SortStatusCodeCell : Type where
  | Lbl'_LT_'statusCode'_GT_' (x0 : SortStatusCode) : SortStatusCodeCell

inductive SortStorageCell : Type where
  | Lbl'_LT_'storage'_GT_' (x0 : SortMap) : SortStorageCell

inductive SortSubstateCell : Type where
  | Lbl'_LT_'substate'_GT_' (x0 : SortSelfDestructCell) (x1 : SortLogCell) (x2 : SortRefundCell) (x3 : SortAccessedAccountsCell) (x4 : SortAccessedStorageCell) : SortSubstateCell

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

inductive SortTernStackOp : Type where
  | LblADDMOD'Unds'EVM'Unds'TernStackOp : SortTernStackOp
  | LblCALLDATACOPY'Unds'EVM'Unds'TernStackOp : SortTernStackOp
  | LblCODECOPY'Unds'EVM'Unds'TernStackOp : SortTernStackOp
  | LblCREATE'Unds'EVM'Unds'TernStackOp : SortTernStackOp
  | LblMCOPY'Unds'EVM'Unds'TernStackOp : SortTernStackOp
  | LblMULMOD'Unds'EVM'Unds'TernStackOp : SortTernStackOp
  | LblRETURNDATACOPY'Unds'EVM'Unds'TernStackOp : SortTernStackOp

inductive SortTimestampCell : Type where
  | Lbl'_LT_'timestamp'_GT_' (x0 : SortInt) : SortTimestampCell

inductive SortToCell : Type where
  | Lbl'_LT_'to'_GT_' (x0 : SortAccount) : SortToCell

inductive SortTouchedAccountsCell : Type where
  | Lbl'_LT_'touchedAccounts'_GT_' (x0 : SortSet) : SortTouchedAccountsCell

inductive SortTransactionsRootCell : Type where
  | Lbl'_LT_'transactionsRoot'_GT_' (x0 : SortInt) : SortTransactionsRootCell

inductive SortTransientStorageCell : Type where
  | Lbl'_LT_'transientStorage'_GT_' (x0 : SortMap) : SortTransientStorageCell

inductive SortTxAccessCell : Type where
  | Lbl'_LT_'txAccess'_GT_' (x0 : SortJSON) : SortTxAccessCell

inductive SortTxChainIDCell : Type where
  | Lbl'_LT_'txChainID'_GT_' (x0 : SortInt) : SortTxChainIDCell

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

inductive SortTxGasLimitCell : Type where
  | Lbl'_LT_'txGasLimit'_GT_' (x0 : SortInt) : SortTxGasLimitCell

inductive SortTxGasPriceCell : Type where
  | Lbl'_LT_'txGasPrice'_GT_' (x0 : SortInt) : SortTxGasPriceCell

inductive SortTxMaxFeeCell : Type where
  | Lbl'_LT_'txMaxFee'_GT_' (x0 : SortInt) : SortTxMaxFeeCell

inductive SortTxNonceCell : Type where
  | Lbl'_LT_'txNonce'_GT_' (x0 : SortInt) : SortTxNonceCell

inductive SortTxOrderCell : Type where
  | Lbl'_LT_'txOrder'_GT_' (x0 : SortList) : SortTxOrderCell

inductive SortTxPendingCell : Type where
  | Lbl'_LT_'txPending'_GT_' (x0 : SortList) : SortTxPendingCell

inductive SortTxPriorityFeeCell : Type where
  | Lbl'_LT_'txPriorityFee'_GT_' (x0 : SortInt) : SortTxPriorityFeeCell

inductive SortTxType : Type where
  | Lbl'Stop'TxType'Unds'EVM_TYPES'Unds'TxType : SortTxType
  | LblAccessList'Unds'EVM_TYPES'Unds'TxType : SortTxType
  | LblDynamicFee'Unds'EVM_TYPES'Unds'TxType : SortTxType
  | LblLegacy'Unds'EVM_TYPES'Unds'TxType : SortTxType

inductive SortTxTypeCell : Type where
  | Lbl'_LT_'txType'_GT_' (x0 : SortTxType) : SortTxTypeCell

inductive SortUnStackOp : Type where
  | LblBALANCE'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblBLOCKHASH'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblCALLDATALOAD'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblEXTCODEHASH'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblEXTCODESIZE'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblISZERO'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblJUMP'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblMLOAD'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblNOT'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblPOP'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblSELFDESTRUCT'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblSLOAD'Unds'EVM'Unds'UnStackOp : SortUnStackOp
  | LblTLOAD'Unds'EVM'Unds'UnStackOp : SortUnStackOp

inductive SortUseGasCell : Type where
  | Lbl'_LT_'useGas'_GT_' (x0 : SortBool) : SortUseGasCell

inductive SortValueCell : Type where
  | Lbl'_LT_'value'_GT_' (x0 : SortInt) : SortValueCell

inductive SortWithdrawalsRootCell : Type where
  | Lbl'_LT_'withdrawalsRoot'_GT_' (x0 : SortInt) : SortWithdrawalsRootCell

inductive SortWordStack : Type where
  | Lbl'Stop'WordStack'Unds'EVM_TYPES'Unds'WordStack : SortWordStack
  | Lbl'UndsColnUndsUnds'EVM_TYPES'Unds'WordStack'Unds'Int'Unds'WordStack (x0 : SortInt) (x1 : SortWordStack) : SortWordStack

inductive SortWordStackCell : Type where
  | Lbl'_LT_'wordStack'_GT_' (x0 : SortWordStack) : SortWordStackCell

 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]

Still reviewing, but I've got two cosmetic questions:

1. Is it safe to drop the Sort prefix? Given that, every Sort will be an inductive type
2. For cells specifically, maybe they're easier to deal with if they're defined as structures rather than inductives (even tho they're the same under the hood)

Also, do you think it's possible to eliminate all the Kore verbosity, such as Lbl, '_LT_', and so on?

[ehildenb]

The Kore verbosity comes from having limited characters available in Kore for expressing things, and from having explicit types/sorts for everything. We can probably use a different munger to make at least the quoted stuff less verbose (since Lean4 is more flexible with the allowed characters showing up in its identifiers), but not sure it's a good idea to remove the type information.

[JuanCoRo]

@ehildenb, by removing type information, do you mean removing the Sort prefix or underscores such as 'Unds'EVM?

What would be a good way of representing this constructor of SortInternalOp?

Lbl'UndsUndsUndsUndsUndsUndsUndsUndsUnds'EVM'Unds'InternalOp'Unds'CallOp'Unds'Int'Unds'Int'Unds'Int'Unds'Int'Unds'Int'Unds'Int'Unds'Int

Another thing we could do is keep the raw translation as verbose as Kore is, and try to use abbrev or notations to mask that for the user

[tothtamas28]

Is it safe to drop the Sort prefix? Given that, every Sort will be an inductive type

Probably so, yes. Consider

module TEST
    syntax Foo ::= "Foo" [symbol(Foo)]
endmodule

In definition.kore, we'll have SortFoo for the sort and LblFoo for the constructor. So for the sake of maintaining uniqueness we could drop either the Sort or the Lbl prefix (but not both). But dropping Lbl is not an option actually, since then identifiers could start with a ', which is not valid Lean.

[tothtamas28]

For cells specifically, maybe they're easier to deal with if they're defined as structures rather than inductives (even tho they're the same under the hood)

Good point, this can be done if all children of a given cell are cells themselves.

[tothtamas28]

Also, do you think it's possible to eliminate all the Kore verbosity, such as Lbl, 'LT', and so on?

Yes, there are a few characters we could unmunge like ! or ?, or just put the unmunged symbol directly between a « and ».

(https://lean-lang.org/doc/reference/latest//Source-Files/Files/#keywords-and-identifiers)

[JuanCoRo]

this can be done if all children of a given cell are cells themselves

Can't cells always be modeled as a product type? If I understand correctly, even if cells don't have cells as children, their structure is still that of a product type, which is what a structure is under the hood. Maybe I'm misunderstanding something 🙏

[tothtamas28]

Can't cells always be modeled as a product type? If I understand correctly, even if cells don't have cells as children, their structure is still that of a product type, which is what a structure is under the hood.

We could use structure even in that case, it's just not obvious what a meaningful identifier for a non-cell field would be.

[tothtamas28]

I'd prefer to address the improvements suggested here (namely, the use of structure and unmunged identifiers) in separate PRs. @JuanCoRo, if you have no objection, let's merge this.

[JuanCoRo]

LGTM!