• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
    • X86isa
    • Axe
      • R1cs-verification-with-axe
      • Prove-equivalence
      • Dags
      • Stp
      • Lifters
      • Read-jar
      • Read-class
    • Execloader
  • Math
  • Testing-utilities

• Axe

Prove-equivalence

Prove that two items (DAGs or terms) are equivalent for all values of all of their variables.

General Form:

(prove-equivalence dag-or-term1
                   dag-or-term2
                   &key
                   :assumptions                ; default nil
                   :types                      ; default nil
                   :tactic                     ; default :rewrite-and-sweep
                   :tests                      ; default 100
                   :print                      ; default :brief
                   :name                       ; default :auto
                   :debug                      ; default nil
                   :max-conflicts              ; default :auto
                   :extra-rules                ; default nil
                   :initial-rule-sets          ; default :auto
                   :monitor                    ; default nil
                   :use-context-when-miteringp ; default nil
                   :normalize-xors             ; default t
                   :interpreted-function-alist ; default nil
                   :check-vars                 ; default t
                   :prove-theorem              ; default nil
                   :local                      ; default t
                   )

Inputs:

dag-or-term1 — (required)

The first DAG or term to compare

dag-or-term2 — (required)

The second DAG or term to compare

:assumptions — default nil

Assumptions to use when proving equivalence, a list of terms (not necessarily translated)

:types — default nil

A test-case-type-alist (alist mapping variables to their test-case-types), or one of the special values :bits or :bytes.

:tactic — default :rewrite-and-sweep

Proof tactic to use for the proof (either :rewrite or :rewrite-and-sweep)

:tests — default 100

How many tests to use to find internal equivalences (a natp)

:print — default :brief

Print verbosity (allows nil, :brief, t, and :verbose)

:name — default :auto

A name to assign to the equivalence term, if desired

:debug — default nil

Whether to leave temp files in place, for debugging

:max-conflicts — default :auto

Initial value of STP max-conflicts (number of conflicts), or :auto (meaning use the default of 60000), or nil (meaning no maximum).

:extra-rules — default nil

The names of extra rules to use when simplifying (a symbol list)

:initial-rule-sets — default :auto

Sequence of rule-sets to apply initially to simplify the miter (:auto means used phased-bv-axe-rule-sets)

:monitor — default nil

Rule names (symbols) to monitor when rewriting

:use-context-when-miteringp — default nil

Whether to use over-arching context when rewriting nodes (causes memoization to be turned off)

:normalize-xors — default t

Whether to normalize XOR nests when simplifying

:interpreted-function-alist — default nil

Provides definitions for non-built-in functions

:check-vars — default t

Whether to check that the two DAGs/terms have exactly the same vars

:prove-theorem — default nil

Whether to produce an ACL2 theorem stating the equivalence (using skip-proofs, currently)

:local — default t

whether to make the generated events local

Description:

If the call to prove-equivalence completes without error, the DAG/terms are equal, given the :assumptions (including the :types).

Usually, the two items (DAGs or terms) have the same set of free variables.

See also prove-equiality, for a variant that supports more exotic options.