• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
      • Soft
      • C
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
        • Primitive-functions
        • Translated-terms
        • Values
        • Evaluation
        • Program-equivalence
        • Functions
          • Function
          • Function-lookup
          • Function-option
          • Lift-function
          • Lift-function-list
          • Function-set
        • Packages
        • Programs
        • Interpreter
        • Evaluation-states
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Functions

Function-lookup

Look up a function in a set, by name.

Signature

(function-lookup name functions) → function?

Arguments

name — Guard (symbol-valuep name).

functions — Guard (function-setp functions).

Returns

function? — Type (function-optionp function?).

We return the first function in the set with the given name, if any. If there is none, we return nil.

When a set of functions represents all the function definitions in an ACL2 environment, the list will have unique function names; this will be formalized elsewhere. Under this condition, returning the first function found is as good as returning any function with that name in the set, since there can be at most one.

Definitions and Theorems

Function: function-lookup

(defun function-lookup (name functions)
  (declare (xargs :guard (and (symbol-valuep name)
                              (function-setp functions))))
  (let ((__function__ 'function-lookup))
    (declare (ignorable __function__))
    (b* (((when (or (not (mbt (function-setp functions)))
                    (emptyp functions)))
          nil)
         (function (head functions))
         ((when (symbol-value-equiv name (function->name function)))
          function))
      (function-lookup name (tail functions)))))

Theorem: function-optionp-of-function-lookup

(defthm function-optionp-of-function-lookup
  (b* ((function? (function-lookup name functions)))
    (function-optionp function?))
  :rule-classes :rewrite)

Theorem: function-lookup-of-symbol-value-fix-name

(defthm function-lookup-of-symbol-value-fix-name
  (equal (function-lookup (symbol-value-fix name)
                          functions)
         (function-lookup name functions)))

Theorem: function-lookup-symbol-value-equiv-congruence-on-name

(defthm function-lookup-symbol-value-equiv-congruence-on-name
  (implies (symbol-value-equiv name name-equiv)
           (equal (function-lookup name functions)
                  (function-lookup name-equiv functions)))
  :rule-classes :congruence)

Theorem: function-lookup-of-function-set-fix-functions

(defthm function-lookup-of-function-set-fix-functions
  (equal (function-lookup name (function-set-fix functions))
         (function-lookup name functions)))

Theorem: function-lookup-function-set-equiv-congruence-on-functions

(defthm function-lookup-function-set-equiv-congruence-on-functions
  (implies (function-set-equiv functions functions-equiv)
           (equal (function-lookup name functions)
                  (function-lookup name functions-equiv)))
  :rule-classes :congruence)