		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-loop-body-correct-thm

Generate the correctness theorem for the body of a loop.

Signature
(atc-gen-loop-body-correct-thm fn typed-formals affect loop-body test-term body-term prec-fns prec-tags prec-objs prog-const fn-thms limit names-to-avoid state) → (mv local-events correct-body-thm updated-names-to-avoid)
Arguments: fn — Guard (symbolp fn).; typed-formals — Guard (atc-symbol-varinfo-alistp typed-formals).; affect — Guard (symbol-listp affect).; loop-body — Guard (stmtp loop-body).; test-term — Guard (pseudo-termp test-term).; body-term — Guard (pseudo-termp body-term).; prec-fns — Guard (atc-symbol-fninfo-alistp prec-fns).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; prec-objs — Guard (atc-string-objinfo-alistp prec-objs).; prog-const — Guard (symbolp prog-const).; fn-thms — Guard (symbol-symbol-alistp fn-thms).; limit — Guard (pseudo-termp limit).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: local-events — Type (pseudo-event-form-listp local-events).; correct-body-thm — Type (symbolp correct-body-thm).; updated-names-to-avoid — Type (symbol-listp updated-names-to-avoid), given (symbol-listp names-to-avoid).

For the purpose of making the proofs generated by ATC more modular, we generate a separate local theorem for the correctness of each generated loop body; we plan to change the loop correctness theorem to make use of this theorem, instead of proving the whole loop, including its body.

Definitions and Theorems

Function: atc-gen-loop-body-correct-thm

(defun atc-gen-loop-body-correct-thm
       (fn typed-formals
           affect loop-body test-term body-term
           prec-fns prec-tags prec-objs prog-const
           fn-thms limit names-to-avoid state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (symbolp fn)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (symbol-listp affect)
                         (stmtp loop-body)
                         (pseudo-termp test-term)
                         (pseudo-termp body-term)
                         (atc-symbol-fninfo-alistp prec-fns)
                         (atc-string-taginfo-alistp prec-tags)
                         (atc-string-objinfo-alistp prec-objs)
                         (symbolp prog-const)
                         (symbol-symbol-alistp fn-thms)
                         (pseudo-termp limit)
                         (symbol-listp names-to-avoid))))
 (let ((__function__ 'atc-gen-loop-body-correct-thm))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (correct-thm (cdr (assoc-eq fn fn-thms)))
    (correct-body-thm (add-suffix-to-fn correct-thm "-BODY"))
    ((mv correct-body-thm names-to-avoid)
     (fresh-logical-name-with-$s-suffix correct-body-thm
                                        nil names-to-avoid wrld))
    (formals (formals+ fn wrld))
    (compst-var (genvar$ 'atc
                         "COMPST" nil formals state))
    (fenv-var (genvar$ 'atc "FENV" nil formals state))
    (limit-var (genvar$ 'atc
                        "LIMIT" nil formals state))
    ((mv formals-bindings
         hyps subst instantiation)
     (atc-gen-outer-bindings-and-hyps
          typed-formals compst-var t prec-objs))
    (diff-pointer-hyps
         (atc-gen-object-disjoint-hyps (strip-cdrs subst)))
    (hyps
     (cons
      'and
      (cons
       (cons 'compustatep
             (cons compst-var 'nil))
       (cons
        (cons '>
              (cons (cons 'compustate-frames-number
                          (cons compst-var 'nil))
                    '(0)))
        (cons
         (cons 'equal
               (cons fenv-var
                     (cons (cons 'init-fun-env
                                 (cons (cons 'preprocess
                                             (cons prog-const 'nil))
                                       'nil))
                           'nil)))
         (cons
          (cons 'integerp (cons limit-var 'nil))
          (cons
           (cons '>=
                 (cons limit-var (cons limit 'nil)))
           (append
              hyps
              (append diff-pointer-hyps
                      (cons (untranslate$ (uguard+ fn wrld)
                                          nil state)
                            (cons (untranslate$ test-term nil state)
                                  'nil)))))))))))
    (affect-new (acl2::add-suffix-to-fn-lst affect "-NEW"))
    (affect-binder (if (endp (cdr affect-new))
                       (car affect-new)
                     (cons 'mv affect-new)))
    (final-compst
         (atc-gen-loop-final-compustate affect typed-formals
                                        subst compst-var prec-objs))
    (body-term (atc-loop-body-term-subst body-term fn affect))
    (concl
     (cons
      'equal
      (cons
       (cons 'exec-stmt
             (cons (cons 'quote (cons loop-body 'nil))
                   (cons compst-var
                         (cons fenv-var (cons limit-var 'nil)))))
       (cons
        (cons 'b*
              (cons (cons (cons affect-binder (cons body-term 'nil))
                          'nil)
                    (cons (cons 'mv
                                (cons '(stmt-value-none)
                                      (cons final-compst 'nil)))
                          'nil)))
        'nil))))
    (formula (cons 'b*
                   (cons formals-bindings
                         (cons (cons 'implies
                                     (cons hyps (cons concl 'nil)))
                               'nil))))
    (called-fns (all-fnnames (ubody+ fn wrld)))
    (not-error-thms
         (atc-string-taginfo-alist-to-not-error-thms prec-tags))
    (valuep-thms
         (atc-string-taginfo-alist-to-valuep-thms prec-tags))
    (value-kind-thms
         (atc-string-taginfo-alist-to-value-kind-thms prec-tags))
    (result-thms
       (atc-symbol-fninfo-alist-to-result-thms prec-fns called-fns))
    (struct-reader-return-thms
         (atc-string-taginfo-alist-to-reader-return-thms prec-tags))
    (struct-writer-return-thms
         (atc-string-taginfo-alist-to-writer-return-thms prec-tags))
    (correct-thms
      (atc-symbol-fninfo-alist-to-correct-thms prec-fns called-fns))
    (measure-thms (atc-symbol-fninfo-alist-to-measure-nat-thms
                       prec-fns (strip-cars prec-fns)))
    (type-prescriptions-called
         (loop$ for callable in (strip-cars prec-fns)
                collect
                (cons ':t (cons callable 'nil))))
    (type-prescriptions-struct-readers
         (loop$ for reader in
                (atc-string-taginfo-alist-to-readers prec-tags)
                collect (cons ':t (cons reader 'nil))))
    (type-of-value-thms
         (atc-string-taginfo-alist-to-type-of-value-thms prec-tags))
    (flexiblep-thms
         (atc-string-taginfo-alist-to-flexiblep-thms prec-tags))
    (member-read-thms
         (atc-string-taginfo-alist-to-member-read-thms prec-tags))
    (member-write-thms
         (atc-string-taginfo-alist-to-member-write-thms prec-tags))
    (extobj-recognizers
         (atc-string-objinfo-alist-to-recognizers prec-objs))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':do-not-induct
        (cons
         't
         (cons
          ':in-theory
          (cons
           (cons
            'union-theories
            (cons
             '(theory 'atc-all-rules)
             (cons
              (cons
               'quote
               (cons
                (append
                 not-error-thms
                 (append
                  valuep-thms
                  (append
                   value-kind-thms
                   (cons
                    'not
                    (cons
                     'return-type-of-stmt-value-return
                     (cons
                      'return-type-of-stmt-value-none
                      (cons
                       'stmt-value-return->value?-of-stmt-value-return
                       (cons
                        'stmt-value-return-of-value-option-fix-value?
                        (cons
                         '(:e value-option-fix)
                         (append
                          struct-reader-return-thms
                          (append
                           struct-writer-return-thms
                           (append
                            type-of-value-thms
                            (append
                             flexiblep-thms
                             (append
                              member-read-thms
                              (append
                               member-write-thms
                               (append
                                type-prescriptions-called
                                (append
                                 type-prescriptions-struct-readers
                                 (append
                                  extobj-recognizers
                                  (append
                                   result-thms
                                   (append
                                    correct-thms
                                    (append
                                     measure-thms
                                     '(expr-value-optionp-when-expr-valuep
                                           expr-pure-limit
                                           max))))))))))))))))))))))
                'nil))
              'nil)))
           (cons
            ':use
            (cons
             (cons
              (cons ':instance
                    (cons (cons ':guard-theorem (cons fn 'nil))
                          (cons ':extra-bindings-ok
                                (alist-to-doublets instantiation))))
              'nil)
             '(:expand :lambdas))))))))
      'nil))
    ((mv correct-body-thm-event &)
     (evmac-generate-defthm correct-body-thm
                            :formula formula
                            :hints hints
                            :enable nil)))
   (mv (list correct-body-thm-event)
       correct-body-thm names-to-avoid))))

Theorem: pseudo-event-form-listp-of-atc-gen-loop-body-correct-thm.local-events

(defthm
 pseudo-event-form-listp-of-atc-gen-loop-body-correct-thm.local-events
 (b* (((mv ?local-events ?correct-body-thm
           ?updated-names-to-avoid)
       (atc-gen-loop-body-correct-thm
            fn typed-formals
            affect loop-body test-term body-term
            prec-fns prec-tags prec-objs prog-const
            fn-thms limit names-to-avoid state)))
   (pseudo-event-form-listp local-events))
 :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-loop-body-correct-thm.correct-body-thm

(defthm symbolp-of-atc-gen-loop-body-correct-thm.correct-body-thm
  (b* (((mv ?local-events ?correct-body-thm
            ?updated-names-to-avoid)
        (atc-gen-loop-body-correct-thm
             fn typed-formals
             affect loop-body test-term body-term
             prec-fns prec-tags prec-objs prog-const
             fn-thms limit names-to-avoid state)))
    (symbolp correct-body-thm))
  :rule-classes :rewrite)

Theorem: symbol-listp-of-atc-gen-loop-body-correct-thm.updated-names-to-avoid

(defthm
 symbol-listp-of-atc-gen-loop-body-correct-thm.updated-names-to-avoid
 (implies (symbol-listp names-to-avoid)
          (b* (((mv ?local-events ?correct-body-thm
                    ?updated-names-to-avoid)
                (atc-gen-loop-body-correct-thm
                     fn typed-formals
                     affect loop-body test-term body-term
                     prec-fns prec-tags prec-objs prog-const
                     fn-thms limit names-to-avoid state)))
            (symbol-listp updated-names-to-avoid)))
 :rule-classes :rewrite)