		Search-engine friendly clone of the ACL2 documentation.

Flattening

Init-fenv

Initial flattening environment.

Signature
(init-fenv curve) → env
Arguments: curve — Guard (curvep curve).
Returns: env — Type (fenvp env).

This only contains the prime and the curve and the curve order (scalar-prime), and no constants.

Definitions and Theorems

Function: init-fenv

(defun init-fenv (curve)
  (declare (xargs :guard (curvep curve)))
  (let ((__function__ 'init-fenv))
    (declare (ignorable __function__))
    (make-fenv :constants nil
               :curve curve)))

Theorem: fenvp-of-init-fenv

(defthm fenvp-of-init-fenv
  (b* ((env (init-fenv curve)))
    (fenvp env))
  :rule-classes :rewrite)

Theorem: init-fenv-of-curve-fix-curve

(defthm init-fenv-of-curve-fix-curve
  (equal (init-fenv (curve-fix curve))
         (init-fenv curve)))

Theorem: init-fenv-curve-equiv-congruence-on-curve

(defthm init-fenv-curve-equiv-congruence-on-curve
  (implies (curve-equiv curve curve-equiv)
           (equal (init-fenv curve)
                  (init-fenv curve-equiv)))
  :rule-classes :congruence)