• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • 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
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
          • Axe-r1cs
          • Axe-lifters
          • Axe-core
          • Axe-provers
          • Axe-rewriters
          • Axe-jvm
          • Axe-x86
            • Def-unrolled
            • Prove-functions-equivalent
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
          • Axe-r1cs
          • Axe-lifters
          • Axe-core
          • Axe-provers
          • Axe-rewriters
          • Axe-jvm
          • Axe-x86
            • Def-unrolled
            • Prove-functions-equivalent
          • Execloader
        • Math
        • Testing-utilities
      • Axe-x86
      • Axe-lifters

      Prove-functions-equivalent

      A tool to prove two x86 binary functions equivalent.

      Description:

      This runs def-unrolled twice, once for each executable, and then tries to prove the two resulting lifted computations equal using rewriting and SMT solving.

      General Form:

      (prove-functions-equivalent executable1
                                  target1
                                  inputs1
                                  output1
                                  executable2
                                  target2
                                  inputs2
                                  output2
                                  &key
                                  :extra-rules ; default nil
                                  :count-hits  ; default :auto
                                  :print       ; default :auto
                                  )

      Inputs:

      executable1 — (required)

      The first executable. Usually a string (a filename).

      target1 — (required)

      The target to lift in the first executable. See the :target option of def-unrolled.

      inputs1 — (required)

      Information about the inputs of the first executable. See the :inputs option of def-unrolled. Corresponding inputs should have the same names in the :inputs2 below.

      output1 — (required)

      Which output to extract from the first executable. See the :output option of def-unrolled.

      executable2 — (required)

      The second executable. Usually a string (a filename).

      target2 — (required)

      The target to lift in the second executable. See the :target option of def-unrolled.

      inputs2 — (required)

      Information about the inputs of the second executable. See the :inputs option of def-unrolled. Corresponding inputs should have the same names in the :inputs1 above.

      output2 — (required)

      Which output to extract from the second executable. See the :output option of def-unrolled.

      :extra-rules — default nil

      Extra rules to use during lifting.

      :count-hits — default :auto

      Whether to count rewrite rule hits.

      :print — default :auto

      Verbosity level.