		Search-engine friendly clone of the ACL2 documentation.

Output-execution

Eval-output-expression

Evaluate an output expression.

Signature
(eval-output-expression outexpr curve) → val
Arguments: outexpr — Guard (output-expressionp outexpr).; curve — Guard (curvep curve).
Returns: val — Type (value-resultp val).

Definitions and Theorems

Function: eval-output-expression

(defun eval-output-expression (outexpr curve)
  (declare (xargs :guard (and (output-expressionp outexpr)
                              (curvep curve))))
  (let ((__function__ 'eval-output-expression))
    (declare (ignorable __function__))
    (b* ((expr (output-expression->get outexpr))
         ((unless (expression-valuep expr))
          (reserrf (list :not-value-expression expr))))
      (value-expr-to-value expr curve))))

Theorem: value-resultp-of-eval-output-expression

(defthm value-resultp-of-eval-output-expression
  (b* ((val (eval-output-expression outexpr curve)))
    (value-resultp val))
  :rule-classes :rewrite)

Theorem: eval-output-expression-of-output-expression-fix-outexpr

(defthm eval-output-expression-of-output-expression-fix-outexpr
  (equal (eval-output-expression (output-expression-fix outexpr)
                                 curve)
         (eval-output-expression outexpr curve)))

Theorem: eval-output-expression-output-expression-equiv-congruence-on-outexpr

(defthm
 eval-output-expression-output-expression-equiv-congruence-on-outexpr
 (implies (output-expression-equiv outexpr outexpr-equiv)
          (equal (eval-output-expression outexpr curve)
                 (eval-output-expression outexpr-equiv curve)))
 :rule-classes :congruence)

Theorem: eval-output-expression-of-curve-fix-curve

(defthm eval-output-expression-of-curve-fix-curve
  (equal (eval-output-expression outexpr (curve-fix curve))
         (eval-output-expression outexpr curve)))

Theorem: eval-output-expression-curve-equiv-congruence-on-curve

(defthm eval-output-expression-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (eval-output-expression outexpr curve)
                  (eval-output-expression outexpr curve-equiv)))
  :rule-classes :congruence)