		Search-engine friendly clone of the ACL2 documentation.

Atc-function-and-loop-generation

Atc-gen-loop-test-correct-thm

Generate the correctness theorem for the test of a loop.

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

This is a step towards generating more modular and controlled loop proofs. The hints are more than needed for now, as they include rules about statement execution, which does not apply here. We will make the hints more nuanced later.

We generate two conjuncts in the conclusion. One conjunct, as expected, says that executing the test yields the same as the ACL2 term test-term that represents the test. Note that we need to wrap exec-expr-pure into test-value, because the ACL2 term is boolean, and so we need to convert the C value to a boolean. The other conjunct says that exec-expr-pure does not return an error. This is needed in the generated proof for the whole loop, which equates the function generated by atc-gen-exec-stmt-while-for-loop to the execution of the loop: that function's body includes a check that exec-expr-pure does not yield an error, and so this other conjunct here serves to eliminate the case that that check fails.

Definitions and Theorems

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

(defun atc-gen-loop-test-correct-thm
       (fn typed-formals
           loop-test test-term fn-thms prec-tags
           prec-objs names-to-avoid state)
 (declare (xargs :stobjs (state)))
 (declare
      (xargs :guard (and (symbolp fn)
                         (atc-symbol-varinfo-alistp typed-formals)
                         (exprp loop-test)
                         (pseudo-termp test-term)
                         (symbol-symbol-alistp fn-thms)
                         (atc-string-taginfo-alistp prec-tags)
                         (atc-string-objinfo-alistp prec-objs)
                         (symbol-listp names-to-avoid))))
 (let ((__function__ 'atc-gen-loop-test-correct-thm))
  (declare (ignorable __function__))
  (b*
   ((wrld (w state))
    (correct-thm (cdr (assoc-eq fn fn-thms)))
    (correct-test-thm (add-suffix-to-fn correct-thm "-TEST"))
    ((mv correct-test-thm names-to-avoid)
     (fresh-logical-name-with-$s-suffix correct-test-thm
                                        nil names-to-avoid wrld))
    (formals (strip-cars typed-formals))
    (compst-var (genvar$ 'atc
                         "COMPST" nil formals state))
    ((mv formals-bindings hyps & instantiation)
     (atc-gen-outer-bindings-and-hyps
          typed-formals compst-var t prec-objs))
    (hyps
     (cons 'and
           (cons (cons 'compustatep
                       (cons compst-var 'nil))
                 (cons (cons '>
                             (cons (cons 'compustate-frames-number
                                         (cons compst-var 'nil))
                                   '(0)))
                       (append hyps
                               (cons (untranslate$ (uguard+ fn wrld)
                                                   nil state)
                                     'nil))))))
    (concl
     (cons
      'and
      (cons
       (cons
        'not
        (cons
         (cons 'errorp
               (cons (cons 'exec-expr-pure
                           (cons (cons 'quote (cons loop-test 'nil))
                                 (cons compst-var 'nil)))
                     'nil))
         'nil))
       (cons
        (cons
         'not
         (cons
          (cons
           'errorp
           (cons
            (cons
               'apconvert-expr-value
               (cons (cons 'exec-expr-pure
                           (cons (cons 'quote (cons loop-test 'nil))
                                 (cons compst-var 'nil)))
                     'nil))
            'nil))
          'nil))
        (cons
         (cons
          'equal
          (cons
           (cons
            'test-value
            (cons
             (cons
              'expr-value->value
              (cons
               (cons
                'apconvert-expr-value
                (cons
                     (cons 'exec-expr-pure
                           (cons (cons 'quote (cons loop-test 'nil))
                                 (cons compst-var 'nil)))
                     'nil))
               'nil))
             'nil))
           (cons test-term 'nil)))
         'nil)))))
    (formula (cons 'b*
                   (cons formals-bindings
                         (cons (cons 'implies
                                     (cons hyps (cons concl 'nil)))
                               'nil))))
    (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))
    (struct-reader-return-thms
         (atc-string-taginfo-alist-to-reader-return-thms prec-tags))
    (member-read-thms
         (atc-string-taginfo-alist-to-member-read-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
                (cons
                 'not
                 (cons
                  'not-errorp-when-expr-valuep
                  (append
                   not-error-thms
                   (append
                      valuep-thms
                      (append
                           value-kind-thms
                           (append struct-reader-return-thms
                                   (append member-read-thms
                                           extobj-recognizers)))))))
                '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-test-thm-event &)
     (evmac-generate-defthm correct-test-thm
                            :formula formula
                            :hints hints
                            :enable nil)))
   (mv (list correct-test-thm-event)
       correct-test-thm names-to-avoid))))

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

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

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

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

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

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