		Search-engine friendly clone of the ACL2 documentation.

Execution

Step-for-loop

Step the loop variable.

Signature
(step-for-loop name env) → new-env
Arguments: name — Guard (identifierp name).; env — Guard (denvp env).
Returns: new-env — Type (denv-resultp new-env).

This is used in exec-for-loop-iterations, after executing the body of the loop and before comparing the stepped variable with the bound. As explained in init-for-loop, the loop variable is actually marked as a constant in the environment. Nonetheless, we increment it here, because this is automatically incremented at each loop iteration, even though its constant status prevents the body of the loop from modifying it.

If the variable does not exist or is not an integer or cannot be safely incremented, we return an error. However, these situations should never arise in well-formed computation states, which we plan for formally prove.

Definitions and Theorems

Function: step-for-loop

(defun step-for-loop (name env)
  (declare (xargs :guard (and (identifierp name) (denvp env))))
  (let ((__function__ 'step-for-loop))
    (declare (ignorable __function__))
    (b* ((info (get-var/const-dinfo name env))
         ((unless info) (reserrf :impossible))
         (val (var/const-dinfo->value info))
         ((unless (int-valuep val))
          (reserrf :impossible))
         (int (int-value-to-int val))
         (new-int (1+ int))
         (new-val (value-case val
                              :u8 (and (< new-int (expt 2 8))
                                       (value-u8 new-int))
                              :u16 (and (< new-int (expt 2 16))
                                        (value-u16 new-int))
                              :u32 (and (< new-int (expt 2 32))
                                        (value-u32 new-int))
                              :u64 (and (< new-int (expt 2 64))
                                        (value-u64 new-int))
                              :u128 (and (< new-int (expt 2 128))
                                         (value-u128 new-int))
                              :i8 (and (< new-int (expt 2 7))
                                       (value-i8 new-int))
                              :i16 (and (< new-int (expt 2 15))
                                        (value-i16 new-int))
                              :i32 (and (< new-int (expt 2 31))
                                        (value-i32 new-int))
                              :i64 (and (< new-int (expt 2 63))
                                        (value-i64 new-int))
                              :i128 (and (< new-int (expt 2 127))
                                         (value-i128 new-int))
                              :bool (impossible)
                              :address (impossible)
                              :field (impossible)
                              :group (impossible)
                              :scalar (impossible)
                              :string (impossible)
                              :tuple (impossible)
                              :struct (impossible)))
         ((unless new-val) (reserrf :impossible))
         (new-info (make-var/const-dinfo :value new-val
                                         :constp t))
         (env (update-var/const-dinfo name new-info env))
         ((unless env) (reserrf :impossible)))
      env)))

Theorem: denv-resultp-of-step-for-loop

(defthm denv-resultp-of-step-for-loop
  (b* ((new-env (step-for-loop name env)))
    (denv-resultp new-env))
  :rule-classes :rewrite)

Theorem: step-for-loop-of-identifier-fix-name

(defthm step-for-loop-of-identifier-fix-name
  (equal (step-for-loop (identifier-fix name)
                        env)
         (step-for-loop name env)))

Theorem: step-for-loop-identifier-equiv-congruence-on-name

(defthm step-for-loop-identifier-equiv-congruence-on-name
  (implies (identifier-equiv name name-equiv)
           (equal (step-for-loop name env)
                  (step-for-loop name-equiv env)))
  :rule-classes :congruence)

Theorem: step-for-loop-of-denv-fix-env

(defthm step-for-loop-of-denv-fix-env
  (equal (step-for-loop name (denv-fix env))
         (step-for-loop name env)))

Theorem: step-for-loop-denv-equiv-congruence-on-env

(defthm step-for-loop-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (step-for-loop name env)
                  (step-for-loop name env-equiv)))
  :rule-classes :congruence)