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 an axiom for each function signature #4736

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

Generate an axiom for each function signature #4736

wants to merge 2 commits into from

Conversation

tothtamas28
Copy link
Contributor

Closes #4726

K function production

syntax Int ::= foo ( Int ) [function]

becomes

axiom foo (x : SortInt) : Option SortInt

@tothtamas28 tothtamas28 self-assigned this Jan 17, 2025
@rv-jenkins rv-jenkins changed the base branch from master to develop January 17, 2025 14:58
@tothtamas28
Copy link
Contributor Author

Function signatures in KEVM 
axiom append (x0 : SortK) (x1 : SortK) : Option SortK

axiom «#addr» (x0 : SortInt) : Option SortInt

axiom «#addrBytes» (x0 : SortAccount) : Option SortBytes

axiom «#adjustedExpLength» (x0 : SortInt) (x1 : SortInt) (x2 : SortBytes) : Option SortInt

axiom «#adjustedExpLengthAux» (x0 : SortInt) : Option SortInt

axiom «#alignHexString» (x0 : SortString) : Option SortString

axiom «#allPostKeys_ETHEREUM-SIMULATION_Set» : Option SortSet

axiom «#asAccount» (x0 : SortBytes) : Option SortAccount

axiom «#asByteStack» (x0 : SortInt) : Option SortBytes

axiom «#asInteger» (x0 : SortBytes) : Option SortInt

axiom «#asScheduleString» (x0 : SortString) : Option SortSchedule

axiom «#asmOpCode» (x0 : SortOpCode) : Option SortInt

axiom «#asmOpCodes» (x0 : SortOpCodes) : Option SortBytes

axiom «#asmOpCodesAux» (x0 : SortOpCodes) (x1 : SortStringBuffer) : Option SortBytes

axiom «#asmTxPrefix» (x0 : SortInt) : Option SortTxType

axiom «#blockhash» (x0 : SortList) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : Option SortInt

axiom «#bloomFilter» (x0 : SortList) : Option SortBytes

axiom «#bloomFilterAux» (x0 : SortList) (x1 : SortInt) : Option SortBytes

axiom «#changesState» (x0 : SortOpCode) (x1 : SortWordStack) : Option SortBool

axiom «#checkKeys_ETHEREUM-SIMULATION_Set» : Option SortSet

axiom «#dasmOpCode» (x0 : SortInt) (x1 : SortSchedule) : Option SortOpCode

axiom «#dasmTxPrefix» (x0 : SortTxType) : Option SortInt

axiom «#decodeLengthPrefix» (x0 : SortBytes) (x1 : SortInt) : Option SortLengthPrefix

axiom «#decodeLengthPrefixAux» (x0 : SortBytes) (x1 : SortInt) (x2 : SortInt) : Option SortLengthPrefix

axiom «#decodeLengthPrefixLength» (x0 : SortLengthPrefixType) (x1 : SortBytes) (x2 : SortInt) (x3 : SortInt) : Option SortLengthPrefix

axiom «#decodeLengthPrefixLengthAux» (x0 : SortLengthPrefixType) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : Option SortLengthPrefix

axiom «#discardKeys_ETHEREUM-SIMULATION_Set» : Option SortSet

axiom «#ecrec» (x0 : SortBytes) (x1 : SortBytes) (x2 : SortBytes) (x3 : SortBytes) : Option SortBytes

axiom «#ecrecAux» (x0 : SortAccount) : Option SortBytes

axiom «#effectiveGasPrice» (x0 : SortInt) (x1 : SortGeneratedTopCell) : Option SortInt

axiom «#entriesGE» (x0 : SortString) (x1 : SortJSONs) : Option SortJSONs

axiom «#entriesLT» (x0 : SortString) (x1 : SortJSONs) : Option SortJSONs

axiom «#execKeys_ETHEREUM-SIMULATION_Set» : Option SortSet

axiom «#hasPost?(_)_ETHEREUM-SIMULATION_Bool_JSON» (x0 : SortJSON) : Option SortBool

axiom «#hasValidInitCode» (x0 : SortInt) (x1 : SortSchedule) : Option SortBool

axiom «#inStorage» (x0 : SortMap) (x1 : SortAccount) (x2 : SortInt) : Option SortBool

axiom «#inStorageAux1» (x0 : SortKItem) (x1 : SortInt) : Option SortBool

axiom «#inStorageAux2» (x0 : SortSet) (x1 : SortInt) : Option SortBool

axiom «#isValidCode» (x0 : SortBytes) (x1 : SortSchedule) : Option SortBool

axiom «#loadKeys_ETHEREUM-SIMULATION_Set» : Option SortSet

axiom «#lookupOpCode(_,_,_)_EVM_MaybeOpCode_Bytes_Int_Schedule» (x0 : SortBytes) (x1 : SortInt) (x2 : SortSchedule) : Option SortMaybeOpCode

axiom «#memory» (x0 : SortOpCode) (x1 : SortInt) : Option SortInt

axiom «#memoryUsageUpdate» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : Option SortInt

axiom «#modexp1» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : Option SortBytes

axiom «#modexp2» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : Option SortBytes

axiom «#modexp3» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortBytes) : Option SortBytes

axiom «#modexp4» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : Option SortBytes

axiom «#multComplexity» (x0 : SortInt) : Option SortInt

axiom «#nBits» (x0 : SortInt) : Option SortInt

axiom «#nBytes» (x0 : SortInt) : Option SortInt

axiom «#newMultComplexity» (x0 : SortInt) : Option SortInt

axiom «#padToWidth» (x0 : SortInt) (x1 : SortBytes) : Option SortBytes

axiom «#parseAccessListStorageKeys» (x0 : SortJSONs) : Option SortList

axiom «#parseAccessListStorageKeysAux» (x0 : SortJSONs) (x1 : SortList) : Option SortList

axiom «#parseAddr» (x0 : SortString) : Option SortInt

axiom «#parseHexWord» (x0 : SortString) : Option SortInt

axiom «#parseMap» (x0 : SortJSON) : Option SortMap

axiom «#parseWord» (x0 : SortString) : Option SortInt

axiom «#point» (x0 : SortG1Point) : Option SortBytes

axiom «#postKeys_ETHEREUM-SIMULATION_Set» : Option SortSet

axiom «#precompiled» (x0 : SortInt) : Option SortPrecompiledOp

axiom «#precompiledAccountsSet» (x0 : SortSchedule) : Option SortSet

axiom «#precompiledAccountsSetAux» (x0 : SortInt) : Option SortSet

axiom «#precompiledAccountsUB» (x0 : SortSchedule) : Option SortInt

axiom «#range» (x0 : SortBytes) (x1 : SortInt) (x2 : SortInt) : Option SortBytes

axiom «#removeZeros» (x0 : SortMap) : Option SortMap

axiom «#removeZerosAux» (x0 : SortList) (x1 : SortMap) : Option SortMap

axiom «#rlpDecode» (x0 : SortBytes) : Option SortJSON

axiom «#rlpDecodeAux» (x0 : SortBytes) (x1 : SortLengthPrefix) : Option SortJSON

axiom «#rlpDecodeList» (x0 : SortBytes) (x1 : SortInt) : Option SortJSONs

axiom «#rlpDecodeListAux» (x0 : SortBytes) (x1 : SortInt) (x2 : SortLengthPrefix) : Option SortJSONs

axiom «#rlpDecodeTransaction» (x0 : SortBytes) : Option SortJSONs

axiom «#rlpEncode» (x0 : SortJSON) : Option SortBytes

axiom «#rlpEncodeAddress» (x0 : SortAccount) : Option SortBytes

axiom «#rlpEncodeBytes» (x0 : SortBytes) : Option SortBytes

axiom «#rlpEncodeInt» (x0 : SortInt) : Option SortBytes

axiom «#rlpEncodeJsonAux» (x0 : SortJSONs) (x1 : SortStringBuffer) : Option SortBytes

axiom «#rlpEncodeLength» (x0 : SortBytes) (x1 : SortInt) : Option SortBytes

axiom «#rlpEncodeLengthAux» (x0 : SortBytes) (x1 : SortInt) (x2 : SortBytes) : Option SortBytes

axiom «#rlpEncodeLogs» (x0 : SortList) : Option SortBytes

axiom «#rlpEncodeLogsAux» (x0 : SortList) (x1 : SortStringBuffer) : Option SortBytes

axiom «#rlpEncodeString» (x0 : SortString) : Option SortBytes

axiom «#rlpEncodeTopics» (x0 : SortList) (x1 : SortStringBuffer) : Option SortBytes

axiom «#rlpEncodeWord» (x0 : SortInt) : Option SortBytes

axiom «#sizeWordStack» (x0 : SortWordStack) : Option SortInt

axiom «#stackAdded» (x0 : SortOpCode) : Option SortInt

axiom «#stackDelta» (x0 : SortOpCode) : Option SortInt

axiom «#stackNeeded» (x0 : SortOpCode) : Option SortInt

axiom «#usesAccessList» (x0 : SortOpCode) : Option SortBool

axiom «#usesMemory» (x0 : SortOpCode) : Option SortBool

axiom «#widthOp» (x0 : SortOpCode) : Option SortInt

axiom «#widthOpCode» (x0 : SortInt) : Option SortInt

axiom «#wordBytes» (x0 : SortInt) : Option SortBytes

axiom «#write(_,_,_)_EVM-TYPES_Bytes_Bytes_Int_Int» (x0 : SortBytes) (x1 : SortInt) (x2 : SortInt) : Option SortBytes

axiom Caddraccess (x0 : SortSchedule) (x1 : SortBool) : Option SortInt

axiom Cbalance (x0 : SortSchedule) : Option SortInt

axiom Cextcodecopy (x0 : SortSchedule) (x1 : SortInt) : Option SortInt

axiom Cextcodehash (x0 : SortSchedule) : Option SortInt

axiom Cextcodesize (x0 : SortSchedule) : Option SortInt

axiom Cextra (x0 : SortSchedule) (x1 : SortBool) (x2 : SortInt) (x3 : SortBool) : Option SortInt

axiom Cgascap_Gas (x0 : SortSchedule) (x1 : SortGas) (x2 : SortGas) (x3 : SortInt) : Option SortGas

axiom Cinitcode (x0 : SortSchedule) (x1 : SortInt) : Option SortInt

axiom Cmem (x0 : SortSchedule) (x1 : SortInt) : Option SortInt

axiom Cmodexp (x0 : SortSchedule) (x1 : SortBytes) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) : Option SortInt

axiom Cnew (x0 : SortSchedule) (x1 : SortBool) (x2 : SortInt) : Option SortInt

axiom Csload (x0 : SortSchedule) (x1 : SortBool) : Option SortInt

axiom Csstore (x0 : SortSchedule) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : Option SortInt

axiom Cstorageaccess (x0 : SortSchedule) (x1 : SortBool) : Option SortInt

axiom Cxfer (x0 : SortSchedule) (x1 : SortInt) : Option SortInt

axiom «G*(_,_,_,_)_GAS-FEES_Gas_Gas_Int_Int_Schedule» (x0 : SortGas) (x1 : SortInt) (x2 : SortInt) (x3 : SortSchedule) : Option SortGas

axiom G0base (x0 : SortSchedule) (x1 : SortBytes) (x2 : SortBool) : Option SortInt

axiom G0data (x0 : SortSchedule) (x1 : SortBytes) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) : Option SortInt

axiom Int2BytesNoLen (x0 : SortInt) (x1 : SortEndianness) (x2 : SortSignedness) : Option SortBytes

axiom «M3:2048(_)_EVM_Int_Bytes» (x0 : SortBytes) : Option SortInt

axiom Rsstore (x0 : SortSchedule) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) : Option SortInt

axiom WordStack2List (x0 : SortWordStack) : Option SortList

axiom «_%Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_%sWord__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_&Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_*Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_+Gas__GAS-SYNTAX_Gas_Gas_Gas» (x0 : SortGas) (x1 : SortGas) : Option SortGas

axiom «_+JSONs__JSON-EXT_JSONs_JSONs_JSONs» (x0 : SortJSONs) (x1 : SortJSONs) : Option SortJSONs

axiom «_+Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_-Gas__GAS-SYNTAX_Gas_Gas_Gas» (x0 : SortGas) (x1 : SortGas) : Option SortGas

axiom «_-Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_/Gas__GAS-SYNTAX_Gas_Gas_Gas» (x0 : SortGas) (x1 : SortGas) : Option SortGas

axiom «_/Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_/sWord__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_<<Byte__WORD_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_<<Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» (x0 : SortScheduleFlag) (x1 : SortSchedule) : Option SortBool

axiom «_<=Gas__GAS-SYNTAX_Bool_Gas_Gas» (x0 : SortGas) (x1 : SortGas) : Option SortBool

axiom «_<=String__STRING-COMMON_Bool_String_String» (x0 : SortString) (x1 : SortString) : Option SortBool

axiom «_<Gas__GAS-SYNTAX_Bool_Gas_Gas» (x0 : SortGas) (x1 : SortGas) : Option SortBool

axiom «_<Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» (x0 : SortScheduleConst) (x1 : SortSchedule) : Option SortInt

axiom «_=/=Int_» (x0 : SortInt) (x1 : SortInt) : Option SortBool

axiom «_=/=K_» (x0 : SortK) (x1 : SortK) : Option SortBool

axiom «_=/=String__STRING-COMMON_Bool_String_String» (x0 : SortString) (x1 : SortString) : Option SortBool

axiom «_==Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_>=String__STRING-COMMON_Bool_String_String» (x0 : SortString) (x1 : SortString) : Option SortBool

axiom «_>>Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_>>sWord__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_>Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_[_:=_]_EVM-TYPES_WordStack_WordStack_Int_Int» (x0 : SortWordStack) (x1 : SortInt) (x2 : SortInt) : Option SortWordStack

axiom «_[_]_EVM-TYPES_Int_WordStack_Int» (x0 : SortWordStack) (x1 : SortInt) : Option SortInt

axiom «_^Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom _andBool_ (x0 : SortBool) (x1 : SortBool) : Option SortBool

axiom _andThenBool_ (x0 : SortBool) (x1 : SortBool) : Option SortBool

axiom _impliesBool_ (x0 : SortBool) (x1 : SortBool) : Option SortBool

axiom _orBool_ (x0 : SortBool) (x1 : SortBool) : Option SortBool

axiom «_s<Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_up/Int__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_xorWord__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «_|Set__SET_Set_Set_Set» (x0 : SortSet) (x1 : SortSet) : Option SortSet

axiom «_|Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom abs (x0 : SortInt) : Option SortInt

axiom accountEmpty (x0 : SortAccountCode) (x1 : SortInt) (x2 : SortInt) : Option SortBool

axiom asWord (x0 : SortBytes) : Option SortInt

axiom bit (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom «bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : Option SortInt

axiom blockHashHeaderBaseFeeBytes (x0 : SortBytes) (x1 : SortBytes) (x2 : SortBytes) (x3 : SortBytes) (x4 : SortBytes) (x5 : SortBytes) (x6 : SortBytes) (x7 : SortBytes) (x8 : SortBytes) (x9 : SortBytes) (x10 : SortBytes) (x11 : SortBytes) (x12 : SortBytes) (x13 : SortBytes) (x14 : SortBytes) (x15 : SortBytes) : Option SortInt

axiom blockHashHeaderBlobBeacon (x0 : SortBytes) (x1 : SortBytes) (x2 : SortBytes) (x3 : SortBytes) (x4 : SortBytes) (x5 : SortBytes) (x6 : SortBytes) (x7 : SortBytes) (x8 : SortBytes) (x9 : SortBytes) (x10 : SortBytes) (x11 : SortBytes) (x12 : SortBytes) (x13 : SortBytes) (x14 : SortBytes) (x15 : SortBytes) (x16 : SortBytes) (x17 : SortBytes) (x18 : SortBytes) (x19 : SortBytes) : Option SortInt

axiom blockHashHeaderBytes (x0 : SortBytes) (x1 : SortBytes) (x2 : SortBytes) (x3 : SortBytes) (x4 : SortBytes) (x5 : SortBytes) (x6 : SortBytes) (x7 : SortBytes) (x8 : SortBytes) (x9 : SortBytes) (x10 : SortBytes) (x11 : SortBytes) (x12 : SortBytes) (x13 : SortBytes) (x14 : SortBytes) : Option SortInt

axiom blockHashHeaderWithdrawalsBytes (x0 : SortBytes) (x1 : SortBytes) (x2 : SortBytes) (x3 : SortBytes) (x4 : SortBytes) (x5 : SortBytes) (x6 : SortBytes) (x7 : SortBytes) (x8 : SortBytes) (x9 : SortBytes) (x10 : SortBytes) (x11 : SortBytes) (x12 : SortBytes) (x13 : SortBytes) (x14 : SortBytes) (x15 : SortBytes) (x16 : SortBytes) : Option SortInt

axiom blockHeaderHash (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortBytes) (x7 : SortInt) (x8 : SortInt) (x9 : SortInt) (x10 : SortInt) (x11 : SortInt) (x12 : SortBytes) (x13 : SortInt) (x14 : SortInt) : Option SortInt

axiom blockHeaderHashBaseFee (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortBytes) (x7 : SortInt) (x8 : SortInt) (x9 : SortInt) (x10 : SortInt) (x11 : SortInt) (x12 : SortBytes) (x13 : SortInt) (x14 : SortInt) (x15 : SortInt) : Option SortInt

axiom blockHeaderHashBlobBeacon (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortBytes) (x7 : SortInt) (x8 : SortInt) (x9 : SortInt) (x10 : SortInt) (x11 : SortInt) (x12 : SortBytes) (x13 : SortInt) (x14 : SortInt) (x15 : SortInt) (x16 : SortInt) (x17 : SortInt) (x18 : SortInt) (x19 : SortInt) : Option SortInt

axiom blockHeaderHashWithdrawals (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) (x3 : SortInt) (x4 : SortInt) (x5 : SortInt) (x6 : SortBytes) (x7 : SortInt) (x8 : SortInt) (x9 : SortInt) (x10 : SortInt) (x11 : SortInt) (x12 : SortBytes) (x13 : SortInt) (x14 : SortInt) (x15 : SortInt) (x16 : SortInt) : Option SortInt

axiom bool2Word (x0 : SortBool) : Option SortInt

axiom byte (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom chop (x0 : SortInt) : Option SortInt

axiom computeValidJumpDests (x0 : SortBytes) : Option SortBytes

axiom computeValidJumpDestsAux (x0 : SortBytes) (x1 : SortInt) (x2 : SortBytes) : Option SortBytes

axiom computeValidJumpDestsWithinBound (x0 : SortBytes) (x1 : SortInt) (x2 : SortBytes) : Option SortBytes

axiom «countAllOccurrences(_,_)_STRING-COMMON_Int_String_String» (x0 : SortString) (x1 : SortString) : Option SortInt

axiom dropWordStack (x0 : SortInt) (x1 : SortWordStack) : Option SortWordStack

axiom «freshInt(_)_INT_Int_Int» (x0 : SortInt) : Option SortInt

axiom «gas2Int(_)_GAS-SYNTAX_Int_Gas» (x0 : SortGas) : Option SortInt

axiom getBloomFilterBit (x0 : SortBytes) (x1 : SortInt) : Option SortInt

axiom getTxData (x0 : SortInt) (x1 : SortGeneratedTopCell) : Option SortTxData

axiom hashTxData (x0 : SortTxData) : Option SortBytes

axiom initDataCell : Option SortDataCell

axiom initSigRCell : Option SortSigRCell

axiom initSigSCell : Option SortSigSCell

axiom initSigVCell : Option SortSigVCell

axiom initToCell : Option SortToCell

axiom initTxAccessCell : Option SortTxAccessCell

axiom initTxMaxFeeCell : Option SortTxMaxFeeCell

axiom initTxNonceCell : Option SortTxNonceCell

axiom initTxPriorityFeeCell : Option SortTxPriorityFeeCell

axiom initTxTypeCell : Option SortTxTypeCell

axiom initValueCell : Option SortValueCell

axiom isAccessListTx (x0 : SortK) : Option SortBool

axiom isAddr1Op (x0 : SortOpCode) : Option SortBool

axiom isAddr2Op (x0 : SortOpCode) : Option SortBool

axiom isCallSixOp (x0 : SortK) : Option SortBool

axiom isDynamicFeeTx (x0 : SortK) : Option SortBool

axiom isInAccessList (x0 : SortAccount) (x1 : SortInt) (x2 : SortJSON) : Option SortBool

axiom isInAccessListStorage (x0 : SortInt) (x1 : SortJSON) : Option SortBool

axiom isInt (x0 : SortK) : Option SortBool

axiom isKResult (x0 : SortK) : Option SortBool

axiom isLegacyTx (x0 : SortK) : Option SortBool

axiom isLogOp (x0 : SortK) : Option SortBool

axiom isNullStackOp (x0 : SortK) : Option SortBool

axiom isPrecompiledAccount (x0 : SortInt) (x1 : SortSchedule) : Option SortBool

axiom isPushOp (x0 : SortK) : Option SortBool

axiom kite {SortSort : Type} (x0 : SortBool) (x1 : SortSort) (x2 : SortSort) : Option SortSort

axiom keccak (x0 : SortBytes) : Option SortInt

axiom listAsBytes (x0 : SortList) : Option SortList

axiom log256Int (x0 : SortInt) : Option SortInt

axiom lookup (x0 : SortMap) (x1 : SortInt) : Option SortInt

axiom mapWriteRange (x0 : SortBytes) (x1 : SortInt) (x2 : SortBytes) : Option SortBytes

axiom «minGas(_,_)_GAS-SYNTAX_Gas_Gas_Gas» (x0 : SortGas) (x1 : SortGas) : Option SortGas

axiom «minInt(_,_)_INT-COMMON_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom newAddr (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom newAddrCreate2 (x0 : SortInt) (x1 : SortInt) (x2 : SortBytes) : Option SortInt

axiom notBool_ (x0 : SortBool) : Option SortBool

axiom parseByteStack (x0 : SortString) : Option SortBytes

axiom parseHexBytes (x0 : SortString) : Option SortBytes

axiom parseHexBytesAux (x0 : SortString) : Option SortBytes

axiom powmod (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : Option SortInt

axiom qsortJSONs (x0 : SortJSONs) : Option SortJSONs

axiom «replace(_,_,_,_)_STRING-COMMON_String_String_String_String_Int» (x0 : SortString) (x1 : SortString) (x2 : SortString) (x3 : SortInt) : Option SortString

axiom «replaceAll(_,_,_)_STRING-COMMON_String_String_String_String» (x0 : SortString) (x1 : SortString) (x2 : SortString) : Option SortString

axiom rlpEncodeTxData (x0 : SortTxData) : Option SortBytes

axiom senderBytes (x0 : SortBytes) (x1 : SortInt) (x2 : SortBytes) (x3 : SortBytes) : Option SortAccount

axiom senderReturn (x0 : SortBytes) : Option SortAccount

axiom senderTxData (x0 : SortTxData) (x1 : SortInt) (x2 : SortBytes) (x3 : SortBytes) (x4 : SortInt) : Option SortAccount

axiom setBloomFilterBits (x0 : SortBytes) : Option SortInt

axiom sgn (x0 : SortInt) : Option SortInt

axiom signextend (x0 : SortInt) (x1 : SortInt) : Option SortInt

axiom sizeWordStackAux (x0 : SortWordStack) (x1 : SortInt) : Option SortInt

axiom sortedJSONs (x0 : SortJSONs) : Option SortBool

axiom takeWordStack (x0 : SortInt) (x1 : SortWordStack) : Option SortWordStack

axiom word2Bool (x0 : SortInt) : Option SortBool

axiom «~Word__EVM-TYPES_Int_Int» (x0 : SortInt) : Option SortInt

@tothtamas28 tothtamas28 force-pushed the uninterpreted-functions branch from afcc15b to 4d6e830 Compare January 17, 2025 15:02
@tothtamas28 tothtamas28 requested a review from JuanCoRo January 17, 2025 15:12
@tothtamas28 tothtamas28 marked this pull request as ready for review January 17, 2025 15:12
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
lean4-backend
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Generate function stubs
2 participants
@tothtamas28 @JuanCoRo