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 injection instances #4733

Draft
wants to merge 5 commits into
base: cell-structure
Choose a base branch
from
Draft

Generate injection instances #4733

wants to merge 5 commits into from
+201 −2

Conversation

tothtamas28
Copy link
Contributor

@tothtamas28 tothtamas28 commented Jan 14, 2025 •
edited
Loading

Closes #4724

Generate an instance of Inj Subsort Supersort for each pairs (Subsort, Supersort).

If Subsort has no subsorts, inj is just the corresponding constructor:

instance : Inj SortBalanceCell SortKItem where
  inj := SortKItem.inj_SortBalanceCell

otherwise, each injection into the subsort is handled with a case to ensure transitivity:

instance : Inj SortTxData SortKItem where
  inj
    | SortTxData.inj_SortAccessListTx x => SortKItem.inj_SortAccessListTx x
    | SortTxData.inj_SortDynamicFeeTx x => SortKItem.inj_SortDynamicFeeTx x
    | SortTxData.inj_SortLegacyTx x => SortKItem.inj_SortLegacyTx x
    | x => SortKItem.inj_SortTxData x

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

The generated module.

Expand 
instance : Inj SortBalanceCell SortKItem where
  inj := SortKItem.inj_SortBalanceCell

instance : Inj SortBinStackOp SortKItem where
  inj
    | SortBinStackOp.inj_SortLogOp x => SortKItem.inj_SortLogOp x
    | x => SortKItem.inj_SortBinStackOp x

instance : Inj SortSelfDestructCell SortKItem where
  inj := SortKItem.inj_SortSelfDestructCell

instance : Inj SortGasPriceCell SortKItem where
  inj := SortKItem.inj_SortGasPriceCell

instance : Inj SortGeneratedTopCell SortKItem where
  inj := SortKItem.inj_SortGeneratedTopCell

instance : Inj SortJSON SortKItem where
  inj
    | SortJSON.inj_SortAccount x => SortKItem.inj_SortAccount x
    | SortJSON.inj_SortBool x => SortKItem.inj_SortBool x
    | SortJSON.inj_SortBytes x => SortKItem.inj_SortBytes x
    | SortJSON.inj_SortInt x => SortKItem.inj_SortInt x
    | SortJSON.inj_SortMap x => SortKItem.inj_SortMap x
    | SortJSON.inj_SortOpCodes x => SortKItem.inj_SortOpCodes x
    | SortJSON.inj_SortString x => SortKItem.inj_SortString x
    | SortJSON.inj_SortSubstateLogEntry x => SortKItem.inj_SortSubstateLogEntry x
    | SortJSON.inj_SortTxType x => SortKItem.inj_SortTxType x
    | x => SortKItem.inj_SortJSON x

instance : Inj SortEthereumCommand SortKItem where
  inj := SortKItem.inj_SortEthereumCommand

instance : Inj SortTxData SortKItem where
  inj
    | SortTxData.inj_SortAccessListTx x => SortKItem.inj_SortAccessListTx x
    | SortTxData.inj_SortDynamicFeeTx x => SortKItem.inj_SortDynamicFeeTx x
    | SortTxData.inj_SortLegacyTx x => SortKItem.inj_SortLegacyTx x
    | x => SortKItem.inj_SortTxData x

instance : Inj SortNetworkCell SortKItem where
  inj := SortKItem.inj_SortNetworkCell

instance : Inj SortValueCell SortKItem where
  inj := SortKItem.inj_SortValueCell

instance : Inj SortSubstateCell SortKItem where
  inj := SortKItem.inj_SortSubstateCell

instance : Inj SortScheduleCell SortKItem where
  inj := SortKItem.inj_SortScheduleCell

instance : Inj SortStaticCell SortKItem where
  inj := SortKItem.inj_SortStaticCell

instance : Inj SortEndStatusCode SortKItem where
  inj
    | SortEndStatusCode.inj_SortExceptionalStatusCode x => SortKItem.inj_SortExceptionalStatusCode x
    | x => SortKItem.inj_SortEndStatusCode x

instance : Inj SortJumpDestsCell SortKItem where
  inj := SortKItem.inj_SortJumpDestsCell

instance : Inj SortAccount SortKItem where
  inj
    | SortAccount.inj_SortInt x => SortKItem.inj_SortInt x
    | x => SortKItem.inj_SortAccount x

instance : Inj SortCodeCell SortKItem where
  inj := SortKItem.inj_SortCodeCell

instance : Inj SortMaybeOpCode SortKItem where
  inj
    | SortMaybeOpCode.inj_SortBinStackOp x => SortKItem.inj_SortBinStackOp x
    | SortMaybeOpCode.inj_SortCallOp x => SortKItem.inj_SortCallOp x
    | SortMaybeOpCode.inj_SortCallSixOp x => SortKItem.inj_SortCallSixOp x
    | SortMaybeOpCode.inj_SortInternalOp x => SortKItem.inj_SortInternalOp x
    | SortMaybeOpCode.inj_SortInvalidOp x => SortKItem.inj_SortInvalidOp x
    | SortMaybeOpCode.inj_SortLogOp x => SortKItem.inj_SortLogOp x
    | SortMaybeOpCode.inj_SortNullStackOp x => SortKItem.inj_SortNullStackOp x
    | SortMaybeOpCode.inj_SortOpCode x => SortKItem.inj_SortOpCode x
    | SortMaybeOpCode.inj_SortPrecompiledOp x => SortKItem.inj_SortPrecompiledOp x
    | SortMaybeOpCode.inj_SortPushOp x => SortKItem.inj_SortPushOp x
    | SortMaybeOpCode.inj_SortQuadStackOp x => SortKItem.inj_SortQuadStackOp x
    | SortMaybeOpCode.inj_SortStackOp x => SortKItem.inj_SortStackOp x
    | SortMaybeOpCode.inj_SortTernStackOp x => SortKItem.inj_SortTernStackOp x
    | SortMaybeOpCode.inj_SortUnStackOp x => SortKItem.inj_SortUnStackOp x
    | x => SortKItem.inj_SortMaybeOpCode x

instance : Inj SortLocalMemCell SortKItem where
  inj := SortKItem.inj_SortLocalMemCell

instance : Inj SortMessageCell SortKItem where
  inj := SortKItem.inj_SortMessageCell

instance : Inj SortOmmersHashCell SortKItem where
  inj := SortKItem.inj_SortOmmersHashCell

instance : Inj SortStorageCell SortKItem where
  inj := SortKItem.inj_SortStorageCell

instance : Inj SortLengthPrefixType SortKItem where
  inj := SortKItem.inj_SortLengthPrefixType

instance : Inj SortStackOp SortKItem where
  inj := SortKItem.inj_SortStackOp

instance : Inj SortCallDataCell SortKItem where
  inj := SortKItem.inj_SortCallDataCell

instance : Inj SortScheduleFlag SortKItem where
  inj := SortKItem.inj_SortScheduleFlag

instance : Inj SortAccessedStorageCell SortKItem where
  inj := SortKItem.inj_SortAccessedStorageCell

instance : Inj SortTouchedAccountsCell SortKItem where
  inj := SortKItem.inj_SortTouchedAccountsCell

instance : Inj SortEthereumSimulation SortKItem where
  inj
    | SortEthereumSimulation.inj_SortAccount x => SortKItem.inj_SortAccount x
    | SortEthereumSimulation.inj_SortBool x => SortKItem.inj_SortBool x
    | SortEthereumSimulation.inj_SortBytes x => SortKItem.inj_SortBytes x
    | SortEthereumSimulation.inj_SortInt x => SortKItem.inj_SortInt x
    | SortEthereumSimulation.inj_SortJSON x => SortKItem.inj_SortJSON x
    | SortEthereumSimulation.inj_SortMap x => SortKItem.inj_SortMap x
    | SortEthereumSimulation.inj_SortOpCodes x => SortKItem.inj_SortOpCodes x
    | SortEthereumSimulation.inj_SortString x => SortKItem.inj_SortString x
    | SortEthereumSimulation.inj_SortSubstateLogEntry x => SortKItem.inj_SortSubstateLogEntry x
    | SortEthereumSimulation.inj_SortTxType x => SortKItem.inj_SortTxType x
    | x => SortKItem.inj_SortEthereumSimulation x

instance : Inj SortAccountCode SortKItem where
  inj
    | SortAccountCode.inj_SortBytes x => SortKItem.inj_SortBytes x
    | x => SortKItem.inj_SortAccountCode x

instance : Inj SortNullStackOp SortKItem where
  inj
    | SortNullStackOp.inj_SortPrecompiledOp x => SortKItem.inj_SortPrecompiledOp x
    | x => SortKItem.inj_SortNullStackOp x

instance : Inj SortModeCell SortKItem where
  inj := SortKItem.inj_SortModeCell

instance : Inj SortLogOp SortKItem where
  inj := SortKItem.inj_SortLogOp

instance : Inj SortCallStateCell SortKItem where
  inj := SortKItem.inj_SortCallStateCell

instance : Inj SortOutputCell SortKItem where
  inj := SortKItem.inj_SortOutputCell

instance : Inj SortAccountsCell SortKItem where
  inj := SortKItem.inj_SortAccountsCell

instance : Inj SortQuadStackOp SortKItem where
  inj := SortKItem.inj_SortQuadStackOp

instance : Inj SortTransientStorageCell SortKItem where
  inj := SortKItem.inj_SortTransientStorageCell

instance : Inj SortStringBuffer SortKItem where
  inj := SortKItem.inj_SortStringBuffer

instance : Inj SortBlockCell SortKItem where
  inj := SortKItem.inj_SortBlockCell

instance : Inj SortTimestampCell SortKItem where
  inj := SortKItem.inj_SortTimestampCell

instance : Inj SortGasLimitCell SortKItem where
  inj := SortKItem.inj_SortGasLimitCell

instance : Inj SortWithdrawalsRootCell SortKItem where
  inj := SortKItem.inj_SortWithdrawalsRootCell

instance : Inj SortExcessBlobGasCell SortKItem where
  inj := SortKItem.inj_SortExcessBlobGasCell

instance : Inj SortMode SortKItem where
  inj := SortKItem.inj_SortMode

instance : Inj SortOrigStorageCell SortKItem where
  inj := SortKItem.inj_SortOrigStorageCell

instance : Inj SortAcctIDCell SortKItem where
  inj := SortKItem.inj_SortAcctIDCell

instance : Inj SortBlockhashesCell SortKItem where
  inj := SortKItem.inj_SortBlockhashesCell

instance : Inj SortUseGasCell SortKItem where
  inj := SortKItem.inj_SortUseGasCell

instance : Inj SortBlockNonceCell SortKItem where
  inj := SortKItem.inj_SortBlockNonceCell

instance : Inj SortOpCode SortKItem where
  inj
    | SortOpCode.inj_SortBinStackOp x => SortKItem.inj_SortBinStackOp x
    | SortOpCode.inj_SortCallOp x => SortKItem.inj_SortCallOp x
    | SortOpCode.inj_SortCallSixOp x => SortKItem.inj_SortCallSixOp x
    | SortOpCode.inj_SortInternalOp x => SortKItem.inj_SortInternalOp x
    | SortOpCode.inj_SortInvalidOp x => SortKItem.inj_SortInvalidOp x
    | SortOpCode.inj_SortLogOp x => SortKItem.inj_SortLogOp x
    | SortOpCode.inj_SortNullStackOp x => SortKItem.inj_SortNullStackOp x
    | SortOpCode.inj_SortPrecompiledOp x => SortKItem.inj_SortPrecompiledOp x
    | SortOpCode.inj_SortPushOp x => SortKItem.inj_SortPushOp x
    | SortOpCode.inj_SortQuadStackOp x => SortKItem.inj_SortQuadStackOp x
    | SortOpCode.inj_SortStackOp x => SortKItem.inj_SortStackOp x
    | SortOpCode.inj_SortTernStackOp x => SortKItem.inj_SortTernStackOp x
    | SortOpCode.inj_SortUnStackOp x => SortKItem.inj_SortUnStackOp x
    | x => SortKItem.inj_SortOpCode x

instance : Inj SortTxPriorityFeeCell SortKItem where
  inj := SortKItem.inj_SortTxPriorityFeeCell

instance : Inj SortOmmerBlockHeadersCell SortKItem where
  inj := SortKItem.inj_SortOmmerBlockHeadersCell

instance : Inj SortCallValueCell SortKItem where
  inj := SortKItem.inj_SortCallValueCell

instance : Inj SortWordStack SortKItem where
  inj := SortKItem.inj_SortWordStack

instance : Inj SortSchedule SortKItem where
  inj := SortKItem.inj_SortSchedule

instance : Inj SortSigVCell SortKItem where
  inj := SortKItem.inj_SortSigVCell

instance : Inj SortDifficultyCell SortKItem where
  inj := SortKItem.inj_SortDifficultyCell

instance : Inj SortTxMaxFeeCell SortKItem where
  inj := SortKItem.inj_SortTxMaxFeeCell

instance : Inj SortLogCell SortKItem where
  inj := SortKItem.inj_SortLogCell

instance : Inj SortBExp SortKItem where
  inj
    | SortBExp.inj_SortBool x => SortKItem.inj_SortBool x
    | x => SortKItem.inj_SortBExp x

instance : Inj SortExceptionalStatusCode SortKItem where
  inj := SortKItem.inj_SortExceptionalStatusCode

instance : Inj SortSubstateLogEntry SortKItem where
  inj := SortKItem.inj_SortSubstateLogEntry

instance : Inj SortExtraDataCell SortKItem where
  inj := SortKItem.inj_SortExtraDataCell

instance : Inj SortOpCodes SortKItem where
  inj := SortKItem.inj_SortOpCodes

instance : Inj SortStatusCodeCell SortKItem where
  inj := SortKItem.inj_SortStatusCodeCell

instance : Inj SortGas SortKItem where
  inj
    | SortGas.inj_SortInt x => SortKItem.inj_SortInt x
    | x => SortKItem.inj_SortGas x

instance : Inj SortTransactionsRootCell SortKItem where
  inj := SortKItem.inj_SortTransactionsRootCell

instance : Inj SortMemoryUsedCell SortKItem where
  inj := SortKItem.inj_SortMemoryUsedCell

instance : Inj SortPrecompiledOp SortKItem where
  inj := SortKItem.inj_SortPrecompiledOp

instance : Inj SortGasUsedCell SortKItem where
  inj := SortKItem.inj_SortGasUsedCell

instance : Inj SortTxTypeCell SortKItem where
  inj := SortKItem.inj_SortTxTypeCell

instance : Inj SortCallerCell SortKItem where
  inj := SortKItem.inj_SortCallerCell

instance : Inj SortInt SortKItem where
  inj := SortKItem.inj_SortInt

instance : Inj SortSigSCell SortKItem where
  inj := SortKItem.inj_SortSigSCell

instance : Inj SortAccessListTx SortKItem where
  inj := SortKItem.inj_SortAccessListTx

instance : Inj SortIdCell SortKItem where
  inj := SortKItem.inj_SortIdCell

instance : Inj SortEvmCell SortKItem where
  inj := SortKItem.inj_SortEvmCell

instance : Inj SortLengthPrefix SortKItem where
  inj := SortKItem.inj_SortLengthPrefix

instance : Inj SortMixHashCell SortKItem where
  inj := SortKItem.inj_SortMixHashCell

instance : Inj SortJSONs SortKItem where
  inj := SortKItem.inj_SortJSONs

instance : Inj SortCallStackCell SortKItem where
  inj := SortKItem.inj_SortCallStackCell

instance : Inj SortMessageCellMap SortKItem where
  inj
    | SortMessageCellMap.inj_SortMessageCell x => SortKItem.inj_SortMessageCell x
    | x => SortKItem.inj_SortMessageCellMap x

instance : Inj SortBeaconRootCell SortKItem where
  inj := SortKItem.inj_SortBeaconRootCell

instance : Inj SortEndianness SortKItem where
  inj := SortKItem.inj_SortEndianness

instance : Inj SortBool SortKItem where
  inj := SortKItem.inj_SortBool

instance : Inj SortTxAccessCell SortKItem where
  inj := SortKItem.inj_SortTxAccessCell

instance : Inj SortSigRCell SortKItem where
  inj := SortKItem.inj_SortSigRCell

instance : Inj SortOriginCell SortKItem where
  inj := SortKItem.inj_SortOriginCell

instance : Inj SortJSONKey SortKItem where
  inj
    | SortJSONKey.inj_SortInt x => SortKItem.inj_SortInt x
    | SortJSONKey.inj_SortString x => SortKItem.inj_SortString x
    | x => SortKItem.inj_SortJSONKey x

instance : Inj SortList SortKItem where
  inj := SortKItem.inj_SortList

instance : Inj SortNonceCell SortKItem where
  inj := SortKItem.inj_SortNonceCell

instance : Inj SortGasCell SortKItem where
  inj := SortKItem.inj_SortGasCell

instance : Inj SortTxType SortKItem where
  inj := SortKItem.inj_SortTxType

instance : Inj SortExp SortKItem where
  inj
    | SortExp.inj_SortGas x => SortKItem.inj_SortGas x
    | SortExp.inj_SortInt x => SortKItem.inj_SortInt x
    | x => SortKItem.inj_SortExp x

instance : Inj SortTxPendingCell SortKItem where
  inj := SortKItem.inj_SortTxPendingCell

instance : Inj SortAccountCell SortKItem where
  inj := SortKItem.inj_SortAccountCell

instance : Inj SortUnStackOp SortKItem where
  inj := SortKItem.inj_SortUnStackOp

instance : Inj SortTxChainIDCell SortKItem where
  inj := SortKItem.inj_SortTxChainIDCell

instance : Inj SortTxOrderCell SortKItem where
  inj := SortKItem.inj_SortTxOrderCell

instance : Inj SortDataCell SortKItem where
  inj := SortKItem.inj_SortDataCell

instance : Inj SortPcCell SortKItem where
  inj := SortKItem.inj_SortPcCell

instance : Inj SortProgramCell SortKItem where
  inj := SortKItem.inj_SortProgramCell

instance : Inj SortDynamicFeeTx SortKItem where
  inj := SortKItem.inj_SortDynamicFeeTx

instance : Inj SortInterimStatesCell SortKItem where
  inj := SortKItem.inj_SortInterimStatesCell

instance : Inj SortMap SortKItem where
  inj := SortKItem.inj_SortMap

instance : Inj SortBytes SortKItem where
  inj := SortKItem.inj_SortBytes

instance : Inj SortEthereumCell SortKItem where
  inj := SortKItem.inj_SortEthereumCell

instance : Inj SortTxGasPriceCell SortKItem where
  inj := SortKItem.inj_SortTxGasPriceCell

instance : Inj SortBaseFeeCell SortKItem where
  inj := SortKItem.inj_SortBaseFeeCell

instance : Inj SortRefundCell SortKItem where
  inj := SortKItem.inj_SortRefundCell

instance : Inj SortCallGasCell SortKItem where
  inj := SortKItem.inj_SortCallGasCell

instance : Inj SortPreviousHashCell SortKItem where
  inj := SortKItem.inj_SortPreviousHashCell

instance : Inj SortToCell SortKItem where
  inj := SortKItem.inj_SortToCell

instance : Inj SortAccounts SortKItem where
  inj := SortKItem.inj_SortAccounts

instance : Inj SortG1Point SortKItem where
  inj := SortKItem.inj_SortG1Point

instance : Inj SortReceiptsRootCell SortKItem where
  inj := SortKItem.inj_SortReceiptsRootCell

instance : Inj SortInternalOp SortKItem where
  inj := SortKItem.inj_SortInternalOp

instance : Inj SortTxGasLimitCell SortKItem where
  inj := SortKItem.inj_SortTxGasLimitCell

instance : Inj SortGeneratedCounterCell SortKItem where
  inj := SortKItem.inj_SortGeneratedCounterCell

instance : Inj SortStateRootCell SortKItem where
  inj := SortKItem.inj_SortStateRootCell

instance : Inj SortTernStackOp SortKItem where
  inj := SortKItem.inj_SortTernStackOp

instance : Inj SortKCell SortKItem where
  inj := SortKItem.inj_SortKCell

instance : Inj SortCallSixOp SortKItem where
  inj := SortKItem.inj_SortCallSixOp

instance : Inj SortExitCodeCell SortKItem where
  inj := SortKItem.inj_SortExitCodeCell

instance : Inj SortSignedness SortKItem where
  inj := SortKItem.inj_SortSignedness

instance : Inj SortG2Point SortKItem where
  inj := SortKItem.inj_SortG2Point

instance : Inj SortMessagesCell SortKItem where
  inj := SortKItem.inj_SortMessagesCell

instance : Inj SortMsgIDCell SortKItem where
  inj := SortKItem.inj_SortMsgIDCell

instance : Inj SortString SortKItem where
  inj := SortKItem.inj_SortString

instance : Inj SortStatusCode SortKItem where
  inj
    | SortStatusCode.inj_SortEndStatusCode x => SortKItem.inj_SortEndStatusCode x
    | SortStatusCode.inj_SortExceptionalStatusCode x => SortKItem.inj_SortExceptionalStatusCode x
    | x => SortKItem.inj_SortStatusCode x

instance : Inj SortWordStackCell SortKItem where
  inj := SortKItem.inj_SortWordStackCell

instance : Inj SortBlobGasUsedCell SortKItem where
  inj := SortKItem.inj_SortBlobGasUsedCell

instance : Inj SortAccountCellMap SortKItem where
  inj
    | SortAccountCellMap.inj_SortAccountCell x => SortKItem.inj_SortAccountCell x
    | x => SortKItem.inj_SortAccountCellMap x

instance : Inj SortKevmCell SortKItem where
  inj := SortKItem.inj_SortKevmCell

instance : Inj SortLegacyTx SortKItem where
  inj := SortKItem.inj_SortLegacyTx

instance : Inj SortCallDepthCell SortKItem where
  inj := SortKItem.inj_SortCallDepthCell

instance : Inj SortAccessedAccountsCell SortKItem where
  inj := SortKItem.inj_SortAccessedAccountsCell

instance : Inj SortCoinbaseCell SortKItem where
  inj := SortKItem.inj_SortCoinbaseCell

instance : Inj SortCallOp SortKItem where
  inj := SortKItem.inj_SortCallOp

instance : Inj SortSet SortKItem where
  inj := SortKItem.inj_SortSet

instance : Inj SortScheduleConst SortKItem where
  inj := SortKItem.inj_SortScheduleConst

instance : Inj SortInvalidOp SortKItem where
  inj := SortKItem.inj_SortInvalidOp

instance : Inj SortLogsBloomCell SortKItem where
  inj := SortKItem.inj_SortLogsBloomCell

instance : Inj SortTxNonceCell SortKItem where
  inj := SortKItem.inj_SortTxNonceCell

instance : Inj SortNumberCell SortKItem where
  inj := SortKItem.inj_SortNumberCell

instance : Inj SortChainIDCell SortKItem where
  inj := SortKItem.inj_SortChainIDCell

instance : Inj SortPushOp SortKItem where
  inj := SortKItem.inj_SortPushOp

instance : Inj SortAccountCell SortAccountCellMap where
  inj := SortAccountCellMap.inj_SortAccountCell

instance : Inj SortMessageCell SortMessageCellMap where
  inj := SortMessageCellMap.inj_SortMessageCell

instance : Inj SortLogOp SortBinStackOp where
  inj := SortBinStackOp.inj_SortLogOp

instance : Inj SortInt SortGas where
  inj := SortGas.inj_SortInt

instance : Inj SortSubstateLogEntry SortJSON where
  inj := SortJSON.inj_SortSubstateLogEntry

instance : Inj SortAccount SortJSON where
  inj
    | SortAccount.inj_SortInt x => SortJSON.inj_SortInt x
    | x => SortJSON.inj_SortAccount x

instance : Inj SortOpCodes SortJSON where
  inj := SortJSON.inj_SortOpCodes

instance : Inj SortString SortJSON where
  inj := SortJSON.inj_SortString

instance : Inj SortMap SortJSON where
  inj := SortJSON.inj_SortMap

instance : Inj SortTxType SortJSON where
  inj := SortJSON.inj_SortTxType

instance : Inj SortBool SortJSON where
  inj := SortJSON.inj_SortBool

instance : Inj SortBytes SortJSON where
  inj := SortJSON.inj_SortBytes

instance : Inj SortInt SortJSON where
  inj := SortJSON.inj_SortInt

instance : Inj SortPrecompiledOp SortNullStackOp where
  inj := SortNullStackOp.inj_SortPrecompiledOp

instance : Inj SortInt SortJSONKey where
  inj := SortJSONKey.inj_SortInt

instance : Inj SortString SortJSONKey where
  inj := SortJSONKey.inj_SortString

instance : Inj SortInt SortExp where
  inj := SortExp.inj_SortInt

instance : Inj SortGas SortExp where
  inj
    | SortGas.inj_SortInt x => SortExp.inj_SortInt x
    | x => SortExp.inj_SortGas x

instance : Inj SortBool SortBExp where
  inj := SortBExp.inj_SortBool

instance : Inj SortUnStackOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortUnStackOp

instance : Inj SortCallOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortCallOp

instance : Inj SortTernStackOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortTernStackOp

instance : Inj SortNullStackOp SortMaybeOpCode where
  inj
    | SortNullStackOp.inj_SortPrecompiledOp x => SortMaybeOpCode.inj_SortPrecompiledOp x
    | x => SortMaybeOpCode.inj_SortNullStackOp x

instance : Inj SortBinStackOp SortMaybeOpCode where
  inj
    | SortBinStackOp.inj_SortLogOp x => SortMaybeOpCode.inj_SortLogOp x
    | x => SortMaybeOpCode.inj_SortBinStackOp x

instance : Inj SortInvalidOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortInvalidOp

instance : Inj SortCallSixOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortCallSixOp

instance : Inj SortLogOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortLogOp

instance : Inj SortPrecompiledOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortPrecompiledOp

instance : Inj SortOpCode SortMaybeOpCode where
  inj
    | SortOpCode.inj_SortBinStackOp x => SortMaybeOpCode.inj_SortBinStackOp x
    | SortOpCode.inj_SortCallOp x => SortMaybeOpCode.inj_SortCallOp x
    | SortOpCode.inj_SortCallSixOp x => SortMaybeOpCode.inj_SortCallSixOp x
    | SortOpCode.inj_SortInternalOp x => SortMaybeOpCode.inj_SortInternalOp x
    | SortOpCode.inj_SortInvalidOp x => SortMaybeOpCode.inj_SortInvalidOp x
    | SortOpCode.inj_SortLogOp x => SortMaybeOpCode.inj_SortLogOp x
    | SortOpCode.inj_SortNullStackOp x => SortMaybeOpCode.inj_SortNullStackOp x
    | SortOpCode.inj_SortPrecompiledOp x => SortMaybeOpCode.inj_SortPrecompiledOp x
    | SortOpCode.inj_SortPushOp x => SortMaybeOpCode.inj_SortPushOp x
    | SortOpCode.inj_SortQuadStackOp x => SortMaybeOpCode.inj_SortQuadStackOp x
    | SortOpCode.inj_SortStackOp x => SortMaybeOpCode.inj_SortStackOp x
    | SortOpCode.inj_SortTernStackOp x => SortMaybeOpCode.inj_SortTernStackOp x
    | SortOpCode.inj_SortUnStackOp x => SortMaybeOpCode.inj_SortUnStackOp x
    | x => SortMaybeOpCode.inj_SortOpCode x

instance : Inj SortPushOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortPushOp

instance : Inj SortQuadStackOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortQuadStackOp

instance : Inj SortStackOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortStackOp

instance : Inj SortInternalOp SortMaybeOpCode where
  inj := SortMaybeOpCode.inj_SortInternalOp

instance : Inj SortSubstateLogEntry SortEthereumSimulation where
  inj := SortEthereumSimulation.inj_SortSubstateLogEntry

instance : Inj SortAccount SortEthereumSimulation where
  inj
    | SortAccount.inj_SortInt x => SortEthereumSimulation.inj_SortInt x
    | x => SortEthereumSimulation.inj_SortAccount x

instance : Inj SortOpCodes SortEthereumSimulation where
  inj := SortEthereumSimulation.inj_SortOpCodes

instance : Inj SortString SortEthereumSimulation where
  inj := SortEthereumSimulation.inj_SortString

instance : Inj SortJSON SortEthereumSimulation where
  inj
    | SortJSON.inj_SortAccount x => SortEthereumSimulation.inj_SortAccount x
    | SortJSON.inj_SortBool x => SortEthereumSimulation.inj_SortBool x
    | SortJSON.inj_SortBytes x => SortEthereumSimulation.inj_SortBytes x
    | SortJSON.inj_SortInt x => SortEthereumSimulation.inj_SortInt x
    | SortJSON.inj_SortMap x => SortEthereumSimulation.inj_SortMap x
    | SortJSON.inj_SortOpCodes x => SortEthereumSimulation.inj_SortOpCodes x
    | SortJSON.inj_SortString x => SortEthereumSimulation.inj_SortString x
    | SortJSON.inj_SortSubstateLogEntry x => SortEthereumSimulation.inj_SortSubstateLogEntry x
    | SortJSON.inj_SortTxType x => SortEthereumSimulation.inj_SortTxType x
    | x => SortEthereumSimulation.inj_SortJSON x

instance : Inj SortMap SortEthereumSimulation where
  inj := SortEthereumSimulation.inj_SortMap

instance : Inj SortTxType SortEthereumSimulation where
  inj := SortEthereumSimulation.inj_SortTxType

instance : Inj SortBool SortEthereumSimulation where
  inj := SortEthereumSimulation.inj_SortBool

instance : Inj SortBytes SortEthereumSimulation where
  inj := SortEthereumSimulation.inj_SortBytes

instance : Inj SortInt SortEthereumSimulation where
  inj := SortEthereumSimulation.inj_SortInt

instance : Inj SortInt SortAccount where
  inj := SortAccount.inj_SortInt

instance : Inj SortBytes SortAccountCode where
  inj := SortAccountCode.inj_SortBytes

instance : Inj SortUnStackOp SortOpCode where
  inj := SortOpCode.inj_SortUnStackOp

instance : Inj SortCallOp SortOpCode where
  inj := SortOpCode.inj_SortCallOp

instance : Inj SortTernStackOp SortOpCode where
  inj := SortOpCode.inj_SortTernStackOp

instance : Inj SortNullStackOp SortOpCode where
  inj
    | SortNullStackOp.inj_SortPrecompiledOp x => SortOpCode.inj_SortPrecompiledOp x
    | x => SortOpCode.inj_SortNullStackOp x

instance : Inj SortBinStackOp SortOpCode where
  inj
    | SortBinStackOp.inj_SortLogOp x => SortOpCode.inj_SortLogOp x
    | x => SortOpCode.inj_SortBinStackOp x

instance : Inj SortInvalidOp SortOpCode where
  inj := SortOpCode.inj_SortInvalidOp

instance : Inj SortCallSixOp SortOpCode where
  inj := SortOpCode.inj_SortCallSixOp

instance : Inj SortLogOp SortOpCode where
  inj := SortOpCode.inj_SortLogOp

instance : Inj SortPrecompiledOp SortOpCode where
  inj := SortOpCode.inj_SortPrecompiledOp

instance : Inj SortPushOp SortOpCode where
  inj := SortOpCode.inj_SortPushOp

instance : Inj SortQuadStackOp SortOpCode where
  inj := SortOpCode.inj_SortQuadStackOp

instance : Inj SortStackOp SortOpCode where
  inj := SortOpCode.inj_SortStackOp

instance : Inj SortInternalOp SortOpCode where
  inj := SortOpCode.inj_SortInternalOp

instance : Inj SortAccessListTx SortTxData where
  inj := SortTxData.inj_SortAccessListTx

instance : Inj SortDynamicFeeTx SortTxData where
  inj := SortTxData.inj_SortDynamicFeeTx

instance : Inj SortLegacyTx SortTxData where
  inj := SortTxData.inj_SortLegacyTx

instance : Inj SortExceptionalStatusCode SortEndStatusCode where
  inj := SortEndStatusCode.inj_SortExceptionalStatusCode

instance : Inj SortEndStatusCode SortStatusCode where
  inj
    | SortEndStatusCode.inj_SortExceptionalStatusCode x => SortStatusCode.inj_SortExceptionalStatusCode x
    | x => SortStatusCode.inj_SortEndStatusCode x

instance : Inj SortExceptionalStatusCode SortStatusCode where
  inj := SortStatusCode.inj_SortExceptionalStatusCode

@tothtamas28 tothtamas28 requested a review from JuanCoRo January 14, 2025 16:25
@tothtamas28 tothtamas28 linked an issue Jan 14, 2025 that may be closed by this pull request
Generate injection instances #4724
Open
JuanCoRo
JuanCoRo reviewed Jan 15, 2025
View reviewed changes
pyk/src/pyk/k2lean4/model.py
object.__setattr__(self, 'val', val)
object.__setattr__(self, 'attr_kind', attr_kind)
object.__setattr__(self, 'priority', priority)
object.__setattr__(self, 'ident', ident)
Copy link
Member

Choose a reason for hiding this comment

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

Maybe this is too paranoid, but strictly speaking, I think priorities have to be nonnegative

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

Assignees

@tothtamas28 tothtamas28

Labels
lean4-backend
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Generate injection instances
2 participants
@tothtamas28 @JuanCoRo