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

Allow special characters in generated Lean 4 identifiers #4729

Merged
merged 4 commits into from
Jan 8, 2025
Merged

Allow special characters in generated Lean 4 identifiers #4729

merged 4 commits into from
Jan 8, 2025

Conversation

tothtamas28
Copy link
Contributor

@tothtamas28 tothtamas28 commented Jan 8, 2025 •
edited
Loading

Closes #4722

@tothtamas28 tothtamas28 self-assigned this Jan 8, 2025
@tothtamas28 tothtamas28 linked an issue Jan 8, 2025 that may be closed by this pull request
Generate more concise identifiers for the Lean 4 definition #4722
Closed
@tothtamas28
Copy link
Contributor Author

tothtamas28 commented Jan 8, 2025 •
edited
Loading

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

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

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

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

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

inductive SortAccountCell : Type where
  | «<account>» (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
  | «{_|_}_EVM_Accounts_AccountsCell_SubstateCell» (x0 : SortAccountsCell) (x1 : SortSubstateCell) : SortAccounts

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

inductive SortCodeCell : Type where
  | «<code>» (x0 : SortAccountCode) : SortCodeCell

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

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

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

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

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

inductive SortEndianness : Type where
  | bigEndianBytes : SortEndianness

inductive SortEthereumCell : Type where
  | «<ethereum>» (x0 : SortEvmCell) (x1 : SortNetworkCell) : SortEthereumCell

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

inductive SortLogsBloomCell : Type where
  | «<logsBloom>» (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
  | «.NoOpCode_EVM_MaybeOpCode» : SortMaybeOpCode

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

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

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

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

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

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

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

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

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

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

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

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

inductive SortOmmersHashCell : Type where
  | «<ommersHash>» (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
  | PUSHAsm (x0 : SortInt) (x1 : SortInt) : SortOpCode

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

inductive SortOrigStorageCell : Type where
  | «<origStorage>» (x0 : SortMap) : SortOrigStorageCell

inductive SortOriginCell : Type where
  | «<origin>» (x0 : SortAccount) : SortOriginCell

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

inductive SortTxChainIDCell : Type where
  | «<txChainID>» (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
  | «<txGasLimit>» (x0 : SortInt) : SortTxGasLimitCell

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

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

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

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

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

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

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

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

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

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

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

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

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

inductive SortWordStackCell : Type where
  | «<wordStack>» (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 requested a review from JuanCoRo January 8, 2025 15:07
@tothtamas28 tothtamas28 marked this pull request as ready for review January 8, 2025 18:03
@automergerpr-permission-manager automergerpr-permission-manager bot merged commit 1f7f4a9 into develop Jan 8, 2025
18 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the ident-special-chars branch January 8, 2025 19:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JuanCoRo JuanCoRo JuanCoRo approved these changes

Assignees

@tothtamas28 tothtamas28

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

Successfully merging this pull request may close these issues.

Generate more concise identifiers for the Lean 4 definition
2 participants
@tothtamas28 @JuanCoRo