		Search-engine friendly clone of the ACL2 documentation.

Execution

Exec-file-main

Execute the main function of a file.

Signature
(exec-file-main file args curve limit) → result
Arguments: file — Guard (filep file).; args — Guard (value-listp args).; curve — Guard (curvep curve).; limit — Guard (natp limit).
Returns: result — Type (value-resultp result).

Besides the file, we supply the argument values, as well as the prime and the curve; we also need to supply a limit for the execution functions. The limit could be so large that it never runs out in practice (if the Leo code terminates). In the future, we may be able to calculate automatically a sufficiently large limit that suffices to execute the program to completion.

We construct the dynamic environment from the file, and then we use the execution (ACL2) function for (Leo) functions, which takes values as arguments.

The final result is either a value or an error. This error may be any that happens in execution, including not finding the main function, if the file does not have one.

Definitions and Theorems

Function: exec-file-main

(defun exec-file-main (file args curve limit)
  (declare (xargs :guard (and (filep file)
                              (value-listp args)
                              (curvep curve)
                              (natp limit))))
  (let ((__function__ 'exec-file-main))
    (declare (ignorable __function__))
    (b* (((okf env)
          (build-denv-from-file file curve))
         ((okf val+env)
          (exec-function (identifier "main")
                         args env limit))
         (val (evalue+denv->evalue val+env))
         (env (evalue+denv->denv val+env)))
      (expr-value-to-value val env))))

Theorem: value-resultp-of-exec-file-main

(defthm value-resultp-of-exec-file-main
  (b* ((result (exec-file-main file args curve limit)))
    (value-resultp result))
  :rule-classes :rewrite)

Theorem: exec-file-main-of-file-fix-file

(defthm exec-file-main-of-file-fix-file
  (equal (exec-file-main (file-fix file)
                         args curve limit)
         (exec-file-main file args curve limit)))

Theorem: exec-file-main-file-equiv-congruence-on-file

(defthm exec-file-main-file-equiv-congruence-on-file
  (implies (file-equiv file file-equiv)
           (equal (exec-file-main file args curve limit)
                  (exec-file-main file-equiv args curve limit)))
  :rule-classes :congruence)

Theorem: exec-file-main-of-value-list-fix-args

(defthm exec-file-main-of-value-list-fix-args
  (equal (exec-file-main file (value-list-fix args)
                         curve limit)
         (exec-file-main file args curve limit)))

Theorem: exec-file-main-value-list-equiv-congruence-on-args

(defthm exec-file-main-value-list-equiv-congruence-on-args
  (implies (value-list-equiv args args-equiv)
           (equal (exec-file-main file args curve limit)
                  (exec-file-main file args-equiv curve limit)))
  :rule-classes :congruence)

Theorem: exec-file-main-of-curve-fix-curve

(defthm exec-file-main-of-curve-fix-curve
  (equal (exec-file-main file args (curve-fix curve)
                         limit)
         (exec-file-main file args curve limit)))

Theorem: exec-file-main-curve-equiv-congruence-on-curve

(defthm exec-file-main-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (exec-file-main file args curve limit)
                  (exec-file-main file args curve-equiv limit)))
  :rule-classes :congruence)

Theorem: exec-file-main-of-nfix-limit

(defthm exec-file-main-of-nfix-limit
  (equal (exec-file-main file args curve (nfix limit))
         (exec-file-main file args curve limit)))

Theorem: exec-file-main-nat-equiv-congruence-on-limit

(defthm exec-file-main-nat-equiv-congruence-on-limit
  (implies (acl2::nat-equiv limit limit-equiv)
           (equal (exec-file-main file args curve limit)
                  (exec-file-main file args curve limit-equiv)))
  :rule-classes :congruence)