Execute a binary operator, on two expression values.
(exec-binary op arg1 arg2 env) → evalue+denv
We coerce the expression values to values if needed. We apply the operator. The result is a value. The environment is unchanged.
Function:
(defun exec-binary (op arg1 arg2 env) (declare (xargs :guard (and (binopp op) (expr-valuep arg1) (expr-valuep arg2) (denvp env)))) (let ((__function__ 'exec-binary)) (declare (ignorable __function__)) (b* (((okf arg1) (expr-value-to-value arg1 env)) ((okf arg2) (expr-value-to-value arg2 env)) (curve (denv->curve env)) ((okf val) (binop-case op :and (op-and arg1 arg2) :or (op-or arg1 arg2) :nand (op-nand arg1 arg2) :nor (op-nor arg1 arg2) :eq (op-eq arg1 arg2) :ne (op-ne arg1 arg2) :ge (op-ge arg1 arg2) :gt (op-gt arg1 arg2) :le (op-le arg1 arg2) :lt (op-lt arg1 arg2) :bitxor (op-bitxor arg1 arg2) :bitior (op-bitior arg1 arg2) :bitand (op-bitand arg1 arg2) :shl (op-shl arg1 arg2) :shr (op-shr arg1 arg2) :shl-wrapped (op-shl-wrapped arg1 arg2) :shr-wrapped (op-shr-wrapped arg1 arg2) :add (op-add arg1 arg2 curve) :sub (op-sub arg1 arg2 curve) :mul (op-mul arg1 arg2 curve) :div (op-div arg1 arg2 curve) :rem (op-rem arg1 arg2 curve) :pow (op-pow arg1 arg2 curve) :add-wrapped (op-add-wrapped arg1 arg2 curve) :sub-wrapped (op-sub-wrapped arg1 arg2 curve) :mul-wrapped (op-mul-wrapped arg1 arg2 curve) :div-wrapped (op-div-wrapped arg1 arg2 curve) :rem-wrapped (op-rem-wrapped arg1 arg2 curve) :pow-wrapped (op-pow-wrapped arg1 arg2 curve))) (eval (expr-value-value val))) (make-evalue+denv :evalue eval :denv (denv-fix env)))))
Theorem:
(defthm evalue+denv-resultp-of-exec-binary (b* ((evalue+denv (exec-binary op arg1 arg2 env))) (evalue+denv-resultp evalue+denv)) :rule-classes :rewrite)
Theorem:
(defthm exec-binary-of-binop-fix-op (equal (exec-binary (binop-fix op) arg1 arg2 env) (exec-binary op arg1 arg2 env)))
Theorem:
(defthm exec-binary-binop-equiv-congruence-on-op (implies (binop-equiv op op-equiv) (equal (exec-binary op arg1 arg2 env) (exec-binary op-equiv arg1 arg2 env))) :rule-classes :congruence)
Theorem:
(defthm exec-binary-of-expr-value-fix-arg1 (equal (exec-binary op (expr-value-fix arg1) arg2 env) (exec-binary op arg1 arg2 env)))
Theorem:
(defthm exec-binary-expr-value-equiv-congruence-on-arg1 (implies (expr-value-equiv arg1 arg1-equiv) (equal (exec-binary op arg1 arg2 env) (exec-binary op arg1-equiv arg2 env))) :rule-classes :congruence)
Theorem:
(defthm exec-binary-of-expr-value-fix-arg2 (equal (exec-binary op arg1 (expr-value-fix arg2) env) (exec-binary op arg1 arg2 env)))
Theorem:
(defthm exec-binary-expr-value-equiv-congruence-on-arg2 (implies (expr-value-equiv arg2 arg2-equiv) (equal (exec-binary op arg1 arg2 env) (exec-binary op arg1 arg2-equiv env))) :rule-classes :congruence)
Theorem:
(defthm exec-binary-of-denv-fix-env (equal (exec-binary op arg1 arg2 (denv-fix env)) (exec-binary op arg1 arg2 env)))
Theorem:
(defthm exec-binary-denv-equiv-congruence-on-env (implies (denv-equiv env env-equiv) (equal (exec-binary op arg1 arg2 env) (exec-binary op arg1 arg2 env-equiv))) :rule-classes :congruence)