Generate the correctness theorem for a C loop.
(atc-gen-loop-correct-thm fn typed-formals affect loop-test loop-body prec-fns prec-tags prec-objs prog-const fn-thms fn-result-thm exec-stmt-while-for-fn exec-stmt-while-for-fn-thm termination-of-fn-thm natp-of-measure-of-fn-thm correct-test-thm correct-body-thm limit names-to-avoid state) → (mv events print-event fn-correct-thm updated-names-to-avoid)
We generate the correctness theorem as a lemma first,
then the actual theorem.
The only difference between the two is that
the lemma uses the specialization of exec-stmt-while
that is generated as discussed above,
while the theorem uses the general exec-stmt-while;
the reason is so we can have the right induction, as discussed above.
As explained shortly,
the formula involves (some of) the loop function's formals,
so we take those into account to generate variables for
the computation state, the function environment, and the limit.
The hypotheses include the guard of the loop function,
but we need to replace any pointers with their dereferenced arrays,
and in addition we need to replace the parameters of the loop function
with read-var calls that read the corresponding variables.
The other hypotheses are the same as in atc-gen-cfun-correct-thm,
with the addition of a hypothesis that
the number of frames in the computation state is not zero;
this is always the case when executing a loop.
The arguments of the loop function call are obtained by
replacing its formals with the corresponding read-var calls.
The lemma is proved via proof builder instructions,
by first applying induction
and then calling the prover on all the induction subgoals.
For robustness, first we set the theory to contain
just the specialized exec-stmt-while,
then we apply induction, which therefore must be on that function.
The theory for the subgoal includes
fewer rules than the ones for the full symbolic execution,
because we use the correctness theorems for the loop test and body
as rewrite rules instead, which take care of most of the execution.
The
Similarly to atc-gen-cfun-correct-thm, we stage the proof of the lemma in two phases: see the documentation of that function for motivation.
Function:
(defun atc-gen-loop-correct-thm (fn typed-formals affect loop-test loop-body prec-fns prec-tags prec-objs prog-const fn-thms fn-result-thm exec-stmt-while-for-fn exec-stmt-while-for-fn-thm termination-of-fn-thm natp-of-measure-of-fn-thm correct-test-thm correct-body-thm limit names-to-avoid state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (atc-symbol-varinfo-alistp typed-formals) (symbol-listp affect) (exprp loop-test) (stmtp loop-body) (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) (symbolp fn-result-thm) (symbolp exec-stmt-while-for-fn) (symbolp exec-stmt-while-for-fn-thm) (symbolp termination-of-fn-thm) (symbolp natp-of-measure-of-fn-thm) (symbolp correct-test-thm) (symbolp correct-body-thm) (pseudo-termp limit) (symbol-listp names-to-avoid)))) (declare (xargs :guard (irecursivep+ fn (w state)))) (let ((__function__ 'atc-gen-loop-correct-thm)) (declare (ignorable __function__)) (b* ((wrld (w state)) (correct-thm (cdr (assoc-eq fn fn-thms))) (correct-lemma (add-suffix-to-fn correct-thm "-LEMMA")) ((mv correct-lemma names-to-avoid) (fresh-logical-name-with-$s-suffix correct-lemma 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) '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)) (concl-lemma (cons 'equal (cons (cons exec-stmt-while-for-fn (cons compst-var (cons limit-var 'nil))) (cons (cons 'b* (cons (cons (cons affect-binder (cons (cons fn formals) 'nil)) 'nil) (cons (cons 'mv (cons 'nil (cons final-compst 'nil))) 'nil))) 'nil)))) (concl-thm (cons 'equal (cons (cons 'exec-stmt-while (cons (cons 'quote (cons loop-test 'nil)) (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 (cons fn formals) 'nil)) 'nil) (cons (cons 'mv (cons 'nil (cons final-compst 'nil))) 'nil))) 'nil)))) (formula-lemma (cons 'b* (cons formals-bindings (cons (cons 'implies (cons hyps (cons concl-lemma 'nil))) 'nil)))) (formula-thm (cons 'b* (cons formals-bindings (cons (cons 'implies (cons hyps (cons concl-thm '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)) (result-thms (atc-symbol-fninfo-alist-to-result-thms prec-fns called-fns)) (result-thms (cons fn-result-thm result-thms)) (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)))) (value-kind-thms (atc-string-taginfo-alist-to-value-kind-thms prec-tags)) (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)) (lemma-hints (cons (cons '"Goal" (cons ':do-not-induct (cons 't (cons ':in-theory (cons (cons 'append (cons '*atc-symbolic-computation-state-rules* (cons '*atc-valuep-rules* (cons '*atc-value-listp-rules* (cons '*atc-value-optionp-rules* (cons '*atc-type-of-value-rules* (cons '*atc-type-of-value-option-rules* (cons '*atc-value-array->elemtype-rules* (cons '*atc-array-length-rules* (cons '*atc-array-length-write-rules* (cons '*atc-other-executable-counterpart-rules* (cons '*atc-wrapper-rules* (cons '*atc-distributivity-over-if-rewrite-rules* (cons '*atc-identifier-rules* (cons '*atc-integer-size-rules* (cons '*atc-limit-rules* (cons '*atc-not-error-rules* (cons '*atc-integer-ops-1-return-rewrite-rules* (cons '*atc-integer-ops-2-return-rewrite-rules* (cons '*atc-integer-convs-return-rewrite-rules* (cons '*atc-array-read-return-rewrite-rules* (cons '*atc-array-write-return-rewrite-rules* (cons '*atc-misc-rewrite-rules* (cons '*atc-computation-state-return-rules* (cons '*atc-boolean-from-integer-return-rules* (cons '*atc-type-prescription-rules* (cons '*atc-compound-recognizer-rules* (cons '*integer-value-disjoint-rules* (cons '*array-value-disjoint-rules* (cons '*atc-value-fix-rules* (cons '*atc-flexible-array-member-rules* (cons (cons 'quote (cons (append not-error-thms (append valuep-thms (append value-kind-thms (cons 'not (cons exec-stmt-while-for-fn (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 result-thms (append correct-thms (append measure-thms (cons natp-of-measure-of-fn-thm (append extobj-recognizers (cons correct-test-thm (cons correct-body-thm '(apconvert-expr-value-when-not-value-array value-kind-when-ucharp value-kind-when-scharp value-kind-when-ushortp value-kind-when-sshortp value-kind-when-uintp value-kind-when-sintp value-kind-when-ulongp value-kind-when-slongp value-kind-when-ullongp value-kind-when-sllongp expr-value-fix-when-expr-valuep))))))))))))))))))))) 'nil)) 'nil)))))))))))))))))))))))))))))))) (cons ':use (cons (cons (cons ':instance (cons (cons ':guard-theorem (cons fn 'nil)) (cons ':extra-bindings-ok (alist-to-doublets instantiation)))) (cons (cons ':instance (cons termination-of-fn-thm (cons ':extra-bindings-ok (alist-to-doublets instantiation)))) 'nil)) 'nil))))))) (cons (cons 'and (cons 'stable-under-simplificationp (cons (cons 'quote (cons (cons ':in-theory (cons (cons 'append (cons '*atc-symbolic-computation-state-rules* (cons '*atc-valuep-rules* (cons '*atc-value-listp-rules* (cons '*atc-value-optionp-rules* (cons '*atc-type-of-value-rules* (cons '*atc-type-of-value-option-rules* (cons '*atc-value-array->elemtype-rules* (cons '*atc-array-length-rules* (cons '*atc-array-length-write-rules* (cons '*atc-other-executable-counterpart-rules* (cons '*atc-wrapper-rules* (cons '*atc-distributivity-over-if-rewrite-rules* (cons '*atc-identifier-rules* (cons '*atc-integer-size-rules* (cons '*atc-limit-rules* (cons '*atc-not-error-rules* (cons '*atc-integer-ops-1-return-rewrite-rules* (cons '*atc-integer-ops-2-return-rewrite-rules* (cons '*atc-integer-convs-return-rewrite-rules* (cons '*atc-array-read-return-rewrite-rules* (cons '*atc-array-write-return-rewrite-rules* (cons '*atc-misc-rewrite-rules* (cons '*atc-computation-state-return-rules* (cons '*atc-boolean-from-integer-return-rules* (cons '*atc-type-prescription-rules* (cons '*atc-compound-recognizer-rules* (cons '*integer-value-disjoint-rules* (cons '*array-value-disjoint-rules* (cons '*atc-value-fix-rules* (cons '*atc-flexible-array-member-rules* (cons (cons 'quote (cons (append not-error-thms (append valuep-thms (append value-kind-thms (cons 'not (cons exec-stmt-while-for-fn (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 result-thms (append correct-thms (append measure-thms (cons natp-of-measure-of-fn-thm (append extobj-recognizers (cons correct-test-thm (cons correct-body-thm '(apconvert-expr-value-when-not-value-array value-kind-when-ucharp value-kind-when-scharp value-kind-when-ushortp value-kind-when-sshortp value-kind-when-uintp value-kind-when-sintp value-kind-when-ulongp value-kind-when-slongp value-kind-when-ullongp value-kind-when-sllongp expr-value-fix-when-expr-valuep))))))))))))))))))))) 'nil)) 'nil)))))))))))))))))))))))))))))))) (cons ':expand (cons (cons ':lambdas (cons (cons fn (fsublis-var-lst instantiation formals)) 'nil)) 'nil)))) 'nil)) 'nil))) 'nil))) (lemma-instructions (cons (cons ':in-theory (cons (cons 'quote (cons (cons exec-stmt-while-for-fn 'nil) 'nil)) 'nil)) (cons (cons ':induct (cons (cons exec-stmt-while-for-fn (cons compst-var (cons limit-var 'nil))) 'nil)) (cons (cons ':repeat (cons (cons ':prove (cons ':hints (cons lemma-hints 'nil))) 'nil)) 'nil)))) (thm-hints (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':use (cons (cons correct-lemma (cons exec-stmt-while-for-fn-thm 'nil)) 'nil))))) 'nil)) ((mv correct-lemma-event &) (evmac-generate-defthm correct-lemma :formula formula-lemma :instructions lemma-instructions :enable nil)) ((mv correct-thm-local-event correct-thm-exported-event) (evmac-generate-defthm correct-thm :formula formula-thm :hints thm-hints :enable nil)) (print-event (cons 'cw-event (cons '"~%~x0~|" (cons (cons 'quote (cons correct-thm-exported-event 'nil)) 'nil))))) (mv (list correct-lemma-event correct-thm-local-event correct-thm-exported-event) print-event correct-thm names-to-avoid))))
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-loop-correct-thm.events (b* (((mv ?events ?print-event ?fn-correct-thm ?updated-names-to-avoid) (atc-gen-loop-correct-thm fn typed-formals affect loop-test loop-body prec-fns prec-tags prec-objs prog-const fn-thms fn-result-thm exec-stmt-while-for-fn exec-stmt-while-for-fn-thm termination-of-fn-thm natp-of-measure-of-fn-thm correct-test-thm correct-body-thm limit names-to-avoid state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-atc-gen-loop-correct-thm.print-event (b* (((mv ?events ?print-event ?fn-correct-thm ?updated-names-to-avoid) (atc-gen-loop-correct-thm fn typed-formals affect loop-test loop-body prec-fns prec-tags prec-objs prog-const fn-thms fn-result-thm exec-stmt-while-for-fn exec-stmt-while-for-fn-thm termination-of-fn-thm natp-of-measure-of-fn-thm correct-test-thm correct-body-thm limit names-to-avoid state))) (pseudo-event-formp print-event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-loop-correct-thm.fn-correct-thm (implies (symbol-symbol-alistp fn-thms) (b* (((mv ?events ?print-event ?fn-correct-thm ?updated-names-to-avoid) (atc-gen-loop-correct-thm fn typed-formals affect loop-test loop-body prec-fns prec-tags prec-objs prog-const fn-thms fn-result-thm exec-stmt-while-for-fn exec-stmt-while-for-fn-thm termination-of-fn-thm natp-of-measure-of-fn-thm correct-test-thm correct-body-thm limit names-to-avoid state))) (symbolp fn-correct-thm))) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-loop-correct-thm.updated-names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?events ?print-event ?fn-correct-thm ?updated-names-to-avoid) (atc-gen-loop-correct-thm fn typed-formals affect loop-test loop-body prec-fns prec-tags prec-objs prog-const fn-thms fn-result-thm exec-stmt-while-for-fn exec-stmt-while-for-fn-thm termination-of-fn-thm natp-of-measure-of-fn-thm correct-test-thm correct-body-thm limit names-to-avoid state))) (symbol-listp updated-names-to-avoid))) :rule-classes :rewrite)