• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
      • Defun
      • Declare
      • System-utilities
      • Stobj
      • State
      • Mutual-recursion
      • Memoize
      • Mbe
      • Io
      • Defpkg
      • Apply$
      • Loop$
      • Programming-with-state
      • Arrays
      • Characters
      • Time$
      • Defmacro
      • Loop$-primer
      • Fast-alists
      • Defconst
      • Evaluation
      • Guard
      • Equality-variants
      • Compilation
      • Hons
      • ACL2-built-ins
      • Developers-guide
      • System-attachments
      • Advanced-features
      • Set-check-invariant-risk
      • Numbers
      • Efficiency
      • Irrelevant-formals
      • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
      • Redefining-programs
      • Lists
      • Invariant-risk
      • Errors
      • Defabbrev
      • Conses
      • Alists
      • Set-register-invariant-risk
      • Strings
      • Program-wrapper
      • Get-internal-time
      • Basics
      • Packages
      • Oracle-eval
      • Defmacro-untouchable
      • <<
      • Primitive
      • Revert-world
      • Unmemoize
      • Set-duplicate-keys-action
      • Symbols
      • Def-list-constructor
      • Easy-simplify-term
      • Defiteration
      • Fake-oracle-eval
      • Defopen
      • Sleep
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Programming

Oracle-eval

Evaluate a term and return its result, logically obtained by reading the state's oracle.

Note: for many purposes you may be able to use magic-ev-fncall ev-fncall-w! instead of oracle-eval. Although these alternatives are less flexible, they do not require trust tags.

General form:

(oracle-eval term alist state) --> (mv error val state)

NOTE: Oracle-eval will not operate as intended until the form (ALLOW-REAL-ORACLE-EVAL) is executed at the top level. However, this introduces a trust tag. Ideally, functions should be coded so that oracle-eval is used only heuristically, so that they can work even without the correct operation of oracle-eval.

In the logic, this function reads from the ACL2 oracle twice, to obtain the error message, if any, and the value. In the execution, we instead evaluate the term and return its result. We believe this is sound.

The term can involve free variables that appear in the alist, and can also take state, but it must return a single non-stobj value. Therefore, it cannot modify state.

Oracle-eval is a constrained function, and as such has no execution semantics itself. Instead, an executable version is attached to it (see defattach). By default, this executable version doesn't do anything interesting, because a trust tag is necessary to allow oracle-eval to function as intended. Running (ALLOW-REAL-ORACLE-EVAL) introduces a trust tag and an attachment that runs the "real" oracle-eval.

Definition: oracle-eval

(encapsulate (((oracle-eval * * state)
               => (mv * * state)))
  (local (value-triple :elided))
  (defthm state-p1-of-oracle-eval
    (implies (state-p1 state)
             (state-p1 (mv-nth 2 (oracle-eval term alist state))))))

Definitions and Theorems

Theorem: state-p1-of-oracle-eval

(defthm state-p1-of-oracle-eval
  (implies (state-p1 state)
           (state-p1 (mv-nth 2 (oracle-eval term alist state)))))