Function table for the EVM dialect of Yul.
(evm-funtable) → funtab
This is based on the table in [Solidity], referenced in static-safety-checking-evm.
In order to enter the information concisely, we introduce a macro that builds a nest of omap::updates.
Function:
(defun evm-funtable-build-fn (args) (if (endp args) nil (cons 'omap::update (cons (cons 'identifier (cons (first args) 'nil)) (cons (cons 'make-funtype (cons ':in (cons (second args) (cons ':out (cons (third args) 'nil))))) (cons (evm-funtable-build-fn (cdddr args)) 'nil))))))
Function:
(defun evm-funtable nil (declare (xargs :guard t)) (let ((__function__ 'evm-funtable)) (declare (ignorable __function__)) (evm-funtable-build "stop" 0 0 "add" 2 1 "sub" 2 1 "mul" 2 1 "div" 2 1 "sdiv" 2 1 "mod" 2 1 "smod" 2 1 "exp" 2 1 "not" 1 1 "lt" 2 1 "gt" 2 1 "slt" 2 1 "sgt" 2 1 "eq" 2 1 "iszero" 1 1 "and" 2 1 "or" 2 1 "xor" 2 1 "byte" 2 1 "shl" 2 1 "shr" 2 1 "sar" 2 1 "addmod" 3 1 "mulmod" 3 1 "signextend" 2 1 "keccak256" 2 1 "pc" 0 1 "pop" 1 0 "mload" 1 1 "mstore" 2 0 "mstore8" 2 0 "sload" 1 1 "sstore" 2 0 "msize" 0 1 "gas" 0 1 "address" 0 1 "balance" 1 1 "selfbalance" 0 1 "caller" 0 1 "callvalue" 0 1 "calldataload" 1 1 "calldatasize" 0 1 "calldatacopy" 3 0 "codesize" 0 1 "codecopy" 3 0 "extcodesize" 1 1 "extcodecopy" 4 0 "returndatasize" 0 1 "returndatacopy" 3 0 "extcodehash" 1 1 "create" 3 1 "create2" 4 1 "call" 7 1 "callcode" 7 1 "delegatecall" 6 1 "staticcall" 6 1 "return" 2 0 "revert" 2 0 "selfdestruct" 1 0 "invalid" 0 0 "log0" 2 0 "log1" 3 0 "log2" 4 0 "log3" 5 0 "log4" 6 0 "chainid" 0 1 "basefee" 0 1 "origin" 0 1 "gasprice" 0 1 "blockhash" 1 1 "coinbase" 0 1 "timestamp" 0 1 "number" 0 1 "difficulty" 0 1 "gaslimit" 0 1)))
Theorem:
(defthm funtablep-of-evm-funtable (b* ((funtab (evm-funtable))) (funtablep funtab)) :rule-classes :rewrite)