Generate the correctness theorem for the body of a loop.
(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)
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.
Function:
(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 'nil (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 (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 measure-thms))))))))))))))) '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:
(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:
(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:
(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)