		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-exec-stmt-while-for-loop

Generate a version of exec-stmt-while specialized to the loop represented by fn.

Signature
(atc-gen-exec-stmt-while-for-loop fn loop-stmt prog-const names-to-avoid wrld) → (mv events exec-stmt-while-for-fn exec-stmt-while-for-fn-thm updated-names-to-avoid)
Arguments: fn — Guard (symbolp fn).; loop-stmt — Guard (stmtp loop-stmt).; prog-const — Guard (symbolp prog-const).; names-to-avoid — Guard (symbol-listp names-to-avoid).; wrld — Guard (plist-worldp wrld).
Returns: events — Type (pseudo-event-form-listp events).; exec-stmt-while-for-fn — Type (symbolp exec-stmt-while-for-fn).; exec-stmt-while-for-fn-thm — Type (symbolp exec-stmt-while-for-fn-thm).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

The correctness theorem for a loop says that the execution of the loop (via exec-stmt-while) is suitably equivalent to the corresponding ACL2 recursive function fn. The theorem is proved by induction, unsurprisingly. However, due to the form in which the function appears in the theorem, namely that the function is not applied to ACL2 variables, we cannot use the function's induction scheme. But we cannot readily use the induction scheme of the execution functions of the C dynamic semantics, or at least it looks cumbersome to do so, because there are several of them, mutually recursive.

What we really need is an induction scheme related to the loop. Thus we introduce a local function that is like exec-stmt-while but specialized to the loop generated from fn; this function is singly recursive, providing the needed induction scheme. The function does not need to be guard-verified, because it is only used for logic. We also generate a theorem saying that this new function is equivalent to exec-stmt-while applied to the loop; this is critical, because eventually the proof must be about the execution functions of the C dynamic semantics. For robustness, the termination proof for this new function, and the proof of the associated theorem, are carried out in exactly specified theories that should always work.

Definitions and Theorems

Function: atc-gen-exec-stmt-while-for-loop

(defun atc-gen-exec-stmt-while-for-loop
       (fn loop-stmt
           prog-const names-to-avoid wrld)
 (declare (xargs :guard (and (symbolp fn)
                             (stmtp loop-stmt)
                             (symbolp prog-const)
                             (symbol-listp names-to-avoid)
                             (plist-worldp wrld))))
 (declare (xargs :guard (and (irecursivep+ fn wrld)
                             (stmt-case loop-stmt :while))))
 (let ((__function__ 'atc-gen-exec-stmt-while-for-loop))
  (declare (ignorable __function__))
  (b*
   ((loop-test (stmt-while->test loop-stmt))
    (loop-body (stmt-while->body loop-stmt))
    (exec-stmt-while-for-fn
         (packn-pos (list 'exec-stmt-while-for- fn)
                    fn))
    ((mv exec-stmt-while-for-fn names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          exec-stmt-while-for-fn 'function
          names-to-avoid wrld))
    (exec-stmt-while-for-fn-body
     (cons
      'b*
      (cons
       (cons
        (cons 'fenv
              (cons (cons 'init-fun-env
                          (cons (cons 'preprocess
                                      (cons prog-const 'nil))
                                'nil))
                    'nil))
        (cons
         '((when (zp limit))
           (mv (error :limit)
               (compustate-fix compst)))
         (cons
          (cons
               '(mv test-eval compst)
               (cons (cons 'exec-expr
                           (cons (cons 'quote (cons loop-test 'nil))
                                 '(compst fenv (1- limit))))
                     'nil))
          (cons
           '((when (errorp test-eval))
             (mv test-eval compst))
           (cons
            (cons
             '(unless test-eval)
             (cons
              (cons
               'mv
               (cons
                (cons
                 'error
                 (cons
                  (cons
                   'list
                   (cons
                    ':void-while-test
                    (cons
                     (cons 'expr-fix
                           (cons (cons 'quote (cons loop-test 'nil))
                                 'nil))
                     'nil)))
                  'nil))
                '(compst)))
              'nil))
            (cons
             '(test-eval (apconvert-expr-value test-eval))
             (cons
              '((when (errorp test-eval))
                (mv test-eval compst))
              (cons
               '(test-val (expr-value->value test-eval))
               (cons
                '(continuep (test-value test-val))
                (cons
                 '((when (errorp continuep))
                   (mv continuep compst))
                 (cons
                  '((when (not continuep))
                    (mv (stmt-value-none) compst))
                  (cons
                   (cons
                    '(mv sval compst)
                    (cons
                     (cons 'exec-stmt
                           (cons (cons 'quote (cons loop-body 'nil))
                                 '(compst fenv (1- limit))))
                     'nil))
                   '(((when (errorp sval)) (mv sval compst))
                     ((when (stmt-value-case sval :return))
                      (mv sval compst)))))))))))))))
       (cons (cons exec-stmt-while-for-fn
                   '(compst (1- limit)))
             'nil))))
    (exec-stmt-while-for-fn-hints
     '(("Goal"
          :in-theory
          '(acl2::zp-compound-recognizer nfix natp o-p o-finp o<))))
    ((mv exec-stmt-while-for-fn-event &)
     (evmac-generate-defun exec-stmt-while-for-fn
                           :formals (list 'compst 'limit)
                           :body exec-stmt-while-for-fn-body
                           :measure '(nfix limit)
                           :well-founded-relation 'o<
                           :hints exec-stmt-while-for-fn-hints
                           :verify-guards nil
                           :enable nil))
    (exec-stmt-while-for-fn-thm
         (add-suffix-to-fn exec-stmt-while-for-fn
                           "-TO-EXEC-STMT-WHILE"))
    ((mv exec-stmt-while-for-fn-thm
         names-to-avoid)
     (fresh-logical-name-with-$s-suffix exec-stmt-while-for-fn-thm
                                        nil names-to-avoid wrld))
    ((mv exec-stmt-while-for-fn-thm-event &)
     (evmac-generate-defthm
      exec-stmt-while-for-fn-thm
      :formula
      (cons
       'equal
       (cons
        (cons exec-stmt-while-for-fn '(compst limit))
        (cons
         (cons
          'exec-stmt-while
          (cons
           (cons 'quote (cons loop-test 'nil))
           (cons
               (cons 'quote (cons loop-body 'nil))
               (cons 'compst
                     (cons (cons 'init-fun-env
                                 (cons (cons 'preprocess
                                             (cons prog-const 'nil))
                                       'nil))
                           '(limit))))))
         'nil)))
      :rule-classes nil
      :hints
      (cons
       (cons
        '"Goal"
        (cons
         ':induct
         (cons
          (cons exec-stmt-while-for-fn '(compst limit))
          (cons
           ':in-theory
           (cons
            (cons
             'quote
             (cons
              (cons
               exec-stmt-while-for-fn
               '(exec-stmt-while
                    valuep-when-value-optionp
                    value-optionp-of-stmt-value-return->value?
                    (:e valuep)
                    exec-expr-to-exec-expr-pure-when-expr-pure-limit
                    nfix))
              'nil))
            'nil)))))
       'nil))))
   (mv (list exec-stmt-while-for-fn-event
             exec-stmt-while-for-fn-thm-event)
       exec-stmt-while-for-fn
       exec-stmt-while-for-fn-thm
       names-to-avoid))))

Theorem: pseudo-event-form-listp-of-atc-gen-exec-stmt-while-for-loop.events

(defthm
 pseudo-event-form-listp-of-atc-gen-exec-stmt-while-for-loop.events
 (b* (((mv ?events ?exec-stmt-while-for-fn
           ?exec-stmt-while-for-fn-thm
           ?updated-names-to-avoid)
       (atc-gen-exec-stmt-while-for-loop
            fn loop-stmt
            prog-const names-to-avoid wrld)))
   (pseudo-event-form-listp events))
 :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-exec-stmt-while-for-loop.exec-stmt-while-for-fn

(defthm
 symbolp-of-atc-gen-exec-stmt-while-for-loop.exec-stmt-while-for-fn
 (b* (((mv ?events ?exec-stmt-while-for-fn
           ?exec-stmt-while-for-fn-thm
           ?updated-names-to-avoid)
       (atc-gen-exec-stmt-while-for-loop
            fn loop-stmt
            prog-const names-to-avoid wrld)))
   (symbolp exec-stmt-while-for-fn))
 :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-exec-stmt-while-for-loop.exec-stmt-while-for-fn-thm

(defthm
 symbolp-of-atc-gen-exec-stmt-while-for-loop.exec-stmt-while-for-fn-thm
 (b* (((mv ?events ?exec-stmt-while-for-fn
           ?exec-stmt-while-for-fn-thm
           ?updated-names-to-avoid)
       (atc-gen-exec-stmt-while-for-loop
            fn loop-stmt
            prog-const names-to-avoid wrld)))
   (symbolp exec-stmt-while-for-fn-thm))
 :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-exec-stmt-while-for-loop.updated-names-to-avoid

(defthm
 symbol-listp-of-atc-gen-exec-stmt-while-for-loop.updated-names-to-avoid
 (implies (symbol-listp names-to-avoid)
          (b* (((mv ?events ?exec-stmt-while-for-fn
                    ?exec-stmt-while-for-fn-thm
                    ?updated-names-to-avoid)
                (atc-gen-exec-stmt-while-for-loop
                     fn loop-stmt
                     prog-const names-to-avoid wrld)))
            (symbol-listp updated-names-to-avoid)))
 :rule-classes :rewrite)