• 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
          • Packages
          • Programs
            • Program
            • Lift-program
            • 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
    • Programs

    Lift-program

    Lift a program from the current ACL2 environment to the meta level.

    Signature
    (lift-program fns state) → program
    Arguments
    fns — Guard (symbol-listp fns).
    Returns
    program — Type (programp program).

    We lift all the known packages, along with the functions specified by symbol. In general there are too many functions in the ACL2 environment, so we only lift the specified functions. Care must be exercised so that the list of functions is closed with respect to calls.

    Definitions and Theorems

    Function: lift-program

    (defun lift-program (fns state)
      (declare (xargs :stobjs (state)))
      (declare (xargs :guard (symbol-listp fns)))
      (let ((__function__ 'lift-program))
        (declare (ignorable __function__))
        (b* ((packages (lift-package-list (known-packages+ state)))
             (functions (lift-function-list fns (w state))))
          (make-program :packages packages
                        :functions functions))))

    Theorem: programp-of-lift-program

    (defthm programp-of-lift-program
      (b* ((program (lift-program fns state)))
        (programp program))
      :rule-classes :rewrite)