Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Generate Lean 4 type definitions from a KORE definition #4717

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

Generate Lean 4 type definitions from a KORE definition #4717

wants to merge 6 commits into from

Conversation

tothtamas28
Copy link
Contributor

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

@tothtamas28 tothtamas28 self-assigned this Dec 20, 2024
@tothtamas28
Copy link
Contributor Author

tothtamas28 commented Dec 20, 2024 •
edited
Loading

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

@tothtamas28 tothtamas28 marked this pull request as ready for review December 20, 2024 14:26
@tothtamas28 tothtamas28 requested a review from JuanCoRo December 20, 2024 14:27
@JuanCoRo
Copy link
Member

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
Copy link
Member

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
Copy link
Member

@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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JuanCoRo JuanCoRo JuanCoRo left review comments

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

Assignees

@tothtamas28 tothtamas28

Labels
lean4-backend
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@tothtamas28 @JuanCoRo @ehildenb