Generate the correctness theorem for the test of a loop.
(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)
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
Function:
(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:
(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:
(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:
(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)