• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
        • Transformations
        • Language
          • Abstract-syntax
          • Dynamic-semantics
          • Concrete-syntax
          • Static-soundness
          • Static-semantics
            • Static-safety-checking
            • Static-shadowing-checking
            • Mode-set-result
            • Literal-evaluation
            • Static-identifier-checking
            • Static-safety-checking-evm
              • Evm-funtable
              • Check-safe-top-block-evm
            • Mode-set
            • Modes
          • Errors
        • Yul-json
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Static-safety-checking-evm

Evm-funtable

Function table for the EVM dialect of Yul.

Signature

(evm-funtable) → funtab

Returns

funtab — Type (funtablep 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.

Definitions and Theorems

Function: evm-funtable-build-fn

(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: evm-funtable

(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: funtablep-of-evm-funtable

(defthm funtablep-of-evm-funtable
  (b* ((funtab (evm-funtable)))
    (funtablep funtab))
  :rule-classes :rewrite)