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.

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

Remove generated Option type for total functions #4741

Draft
wants to merge 1 commit into
base: develop
Choose a base branch
from

Conversation

JuanCoRo
Copy link
Member

By default, every generated uninterpreted function symbol has Option X as the return type, even for functions with the total attribute.

This PR checks the total attribute and generates the Option type depending on it.

@JuanCoRo
Copy link
Member Author

Function module for evm-semantics
axiom append (x0 : SortK) (x1 : SortK) : Option SortK

axiom «#addr» (x0 : SortInt) : 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) : SortString

axiom «#allPostKeys_ETHEREUM-SIMULATION_Set» : Option SortSet

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

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

axiom «#asInteger» (x0 : SortBytes) : 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) : 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) : SortBytes

axiom «#ecrecAux» (x0 : SortAccount) : 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) : SortBool

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

axiom «#inStorageAux2» (x0 : SortSet) (x1 : SortInt) : 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) : SortMaybeOpCode

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

axiom «#memoryUsageUpdate» (x0 : SortInt) (x1 : SortInt) (x2 : SortInt) : 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) : 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) : SortSet

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

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

axiom «#range» (x0 : SortBytes) (x1 : SortInt) (x2 : SortInt) : 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) : SortInt

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

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

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

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

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

axiom «#widthOp» (x0 : SortOpCode) : 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) : SortInt

axiom Cbalance (x0 : SortSchedule) : SortInt

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

axiom Cextcodehash (x0 : SortSchedule) : SortInt

axiom Cextcodesize (x0 : SortSchedule) : SortInt

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

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

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

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

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

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

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

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

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

axiom Cxfer (x0 : SortSchedule) (x1 : SortInt) : 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) : SortBytes

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

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

axiom WordStack2List (x0 : SortWordStack) : SortList

axiom «_%Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : 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) : SortInt

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

axiom «_+Gas__GAS-SYNTAX_Gas_Gas_Gas» (x0 : SortGas) (x1 : SortGas) : 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) : SortInt

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

axiom «_-Word__EVM-TYPES_Int_Int_Int» (x0 : SortInt) (x1 : SortInt) : 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) : 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) : SortInt

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

axiom abs (x0 : SortInt) : SortInt

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

axiom asWord (x0 : SortBytes) : 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) : SortInt

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

axiom chop (x0 : SortInt) : SortInt

axiom computeValidJumpDests (x0 : SortBytes) : 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) : SortInt

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

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

axiom «gas2Int(_)_GAS-SYNTAX_Int_Gas» (x0 : SortGas) : 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 : SortDataCell

axiom initSigRCell : SortSigRCell

axiom initSigSCell : SortSigSCell

axiom initSigVCell : SortSigVCell

axiom initToCell : SortToCell

axiom initTxAccessCell : SortTxAccessCell

axiom initTxMaxFeeCell : SortTxMaxFeeCell

axiom initTxNonceCell : SortTxNonceCell

axiom initTxPriorityFeeCell : SortTxPriorityFeeCell

axiom initTxTypeCell : SortTxTypeCell

axiom initValueCell : SortValueCell

axiom isAccessListTx (x0 : SortK) : SortBool

axiom isAddr1Op (x0 : SortOpCode) : SortBool

axiom isAddr2Op (x0 : SortOpCode) : SortBool

axiom isCallSixOp (x0 : SortK) : SortBool

axiom isDynamicFeeTx (x0 : SortK) : SortBool

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

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

axiom isInt (x0 : SortK) : SortBool

axiom isKResult (x0 : SortK) : SortBool

axiom isLegacyTx (x0 : SortK) : SortBool

axiom isLogOp (x0 : SortK) : SortBool

axiom isNullStackOp (x0 : SortK) : SortBool

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

axiom isPushOp (x0 : SortK) : SortBool

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

axiom keccak (x0 : SortBytes) : SortInt

axiom listAsBytes (x0 : SortList) : Option SortList

axiom log256Int (x0 : SortInt) : Option SortInt

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

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

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

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

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

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

axiom notBool_ (x0 : SortBool) : 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) : 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) : SortString

axiom rlpEncodeTxData (x0 : SortTxData) : Option SortBytes

axiom senderBytes (x0 : SortBytes) (x1 : SortInt) (x2 : SortBytes) (x3 : SortBytes) : 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) : SortInt

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

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

axiom sortedJSONs (x0 : SortJSONs) : Option SortBool

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

axiom word2Bool (x0 : SortInt) : SortBool

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

@tothtamas28
Copy link
Contributor

Let's postpone this change for now. I'd like to first have a (to some extent working) function definition generator in place for partial functions, then we can figure out how to satisfy the stronger type constraint.

A few ideas on how it could be done are listed in section Totality of #4552.

@JuanCoRo JuanCoRo marked this pull request as draft January 21, 2025 15:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants