		Search-engine friendly clone of the ACL2 documentation.

Semantics-deeply-embedded

Eval-expr

Evaluate an expression, given an assignment and a prime field.

Signature
(eval-expr expr asg p) → nat
Arguments: expr — Guard (expressionp expr).; asg — Guard (assignmentp asg).; p — Guard (primep p).
Returns: nat — Type (nat-resultp nat), given (primep p).

In effect, this extends the assignment from variables to expressions. If a variable is not in the assignment, it is an error, indicated by nil. The evaluation is in the context of a prime field, so a constant expression is reduced modulo the prime. An addition or multiplication expression is evaluated recursively, propagating errors and combining the results with the field addition and multiplication operations. If the assignment is for a prime field, and the evaluation returns a natural number (not an error), that natural number is in the prime field.

Definitions and Theorems

Function: eval-expr

(defun
 eval-expr (expr asg p)
 (declare (xargs :guard (and (expressionp expr)
                             (assignmentp asg)
                             (primep p))))
 (declare (xargs :guard (assignment-wfp asg p)))
 (let
    ((__function__ 'eval-expr))
    (declare (ignorable __function__))
    (expression-case
         expr
         :const (mod expr.value p)
         :var (b* ((pair (omap::in expr.name (assignment-fix asg))))
                  (if (consp pair)
                      (nfix (cdr pair))
                      (reserr nil)))
         :add (b* (((ok val1) (eval-expr expr.arg1 asg p))
                   ((ok val2) (eval-expr expr.arg2 asg p)))
                  (add val1 val2 p))
         :mul (b* (((ok val1) (eval-expr expr.arg1 asg p))
                   ((ok val2) (eval-expr expr.arg2 asg p)))
                  (mul val1 val2 p)))))

Theorem: nat-resultp-of-eval-expr

(defthm nat-resultp-of-eval-expr
        (implies (primep p)
                 (b* ((nat (eval-expr expr asg p)))
                     (nat-resultp nat)))
        :rule-classes :rewrite)

Theorem: fep-of-eval-expr

(defthm fep-of-eval-expr
        (implies (and (primep p)
                      (assignmentp asg)
                      (assignment-wfp asg p)
                      (not (reserrp (eval-expr expr asg p))))
                 (fep (eval-expr expr asg p) p)))

Theorem: eval-expr-of-expression-fix-expr

(defthm eval-expr-of-expression-fix-expr
        (equal (eval-expr (expression-fix expr) asg p)
               (eval-expr expr asg p)))

Theorem: eval-expr-expression-equiv-congruence-on-expr

(defthm eval-expr-expression-equiv-congruence-on-expr
        (implies (expression-equiv expr expr-equiv)
                 (equal (eval-expr expr asg p)
                        (eval-expr expr-equiv asg p)))
        :rule-classes :congruence)

Theorem: eval-expr-of-assignment-fix-asg

(defthm eval-expr-of-assignment-fix-asg
        (equal (eval-expr expr (assignment-fix asg) p)
               (eval-expr expr asg p)))

Theorem: eval-expr-assignment-equiv-congruence-on-asg

(defthm eval-expr-assignment-equiv-congruence-on-asg
        (implies (assignment-equiv asg asg-equiv)
                 (equal (eval-expr expr asg p)
                        (eval-expr expr asg-equiv p)))
        :rule-classes :congruence)