		Search-engine friendly clone of the ACL2 documentation.

Dynamic-environments

Init-denv

Initial dynamic environment.

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

This depends on the prime and the curve, which are passed as parameters to this ACL2 function.

All the other components of the environment are empty.

Definitions and Theorems

Function: init-denv

(defun init-denv (curve)
  (declare (xargs :guard (curvep curve)))
  (let ((__function__ 'init-denv))
    (declare (ignorable __function__))
    (make-denv :call-stack nil
               :functions (init-function-denv)
               :structs (init-struct-denv)
               :screen (init-screen)
               :curve curve)))

Theorem: denvp-of-init-denv

(defthm denvp-of-init-denv
  (b* ((env (init-denv curve)))
    (denvp env))
  :rule-classes :rewrite)

Theorem: init-denv-of-curve-fix-curve

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

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

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