Generate the correctness theorem for a C function.
(atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals affect typed-formals context-preamble compst-var fenv-var limit-var fn-thms fn-fun-env-thm init-scope-expand-thm init-scope-scopep-thm push-init-thm pop-frame-thm body-thm body-type body-limit prec-tags prec-objs names-to-avoid state) → (mv events print-event name lemma-name names-to-avoid)
This will eventually replace atc-gen-cfun-correct-thm, once the modular proof generation approach is completed.
We make use of other modular theorems, whose names are passed to this ACL2 function. We use 1 more than the limit for the body as limit bound, because we need 1 to go from exec-fun to exec-block-item-list, which is what the body's theorem refers to.
We enable declar and assign in the generated hints
because the correctness theorem generated about the body of the function
(i.e.
Function:
(defun atc-gen-fun-correct-thm (fn fn-guard fn-def* init-formals affect typed-formals context-preamble compst-var fenv-var limit-var fn-thms fn-fun-env-thm init-scope-expand-thm init-scope-scopep-thm push-init-thm pop-frame-thm body-thm body-type body-limit prec-tags prec-objs names-to-avoid state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (symbolp fn-guard) (symbolp fn-def*) (symbol-listp init-formals) (symbol-listp affect) (atc-symbol-varinfo-alistp typed-formals) (true-listp context-preamble) (symbolp compst-var) (symbolp fenv-var) (symbolp limit-var) (symbol-symbol-alistp fn-thms) (symbolp fn-fun-env-thm) (symbolp init-scope-expand-thm) (symbolp init-scope-scopep-thm) (symbolp push-init-thm) (symbolp pop-frame-thm) (symbolp body-thm) (typep body-type) (pseudo-termp body-limit) (atc-string-taginfo-alistp prec-tags) (atc-string-objinfo-alistp prec-objs) (symbol-listp names-to-avoid)))) (let ((__function__ 'atc-gen-fun-correct-thm)) (declare (ignorable __function__)) (b* ((wrld (w state)) (lemma-name (pack fn '-correct)) ((mv lemma-name names-to-avoid) (fresh-logical-name-with-$s-suffix lemma-name nil names-to-avoid wrld)) (formals (formals+ fn wrld)) (result-var (if (type-case body-type :void) nil (genvar$ 'atc "RESULT" nil formals state))) (limit (cons 'binary-+ (cons ''1 (cons body-limit 'nil)))) (affect-new (acl2::add-suffix-to-fn-lst affect "-NEW")) (fn-results (append (and result-var (list result-var)) affect-new)) (fn-binder (if (endp (cdr fn-results)) (car fn-results) (cons 'mv fn-results))) (new-compst (atc-gen-fun-endstate affect typed-formals compst-var prec-objs)) (exec-hyps (cons 'and (cons (cons 'compustatep (cons compst-var 'nil)) (append context-preamble (cons (cons fn-guard formals) (cons (cons 'integerp (cons limit-var 'nil)) (cons (cons '>= (cons limit-var (cons limit 'nil))) 'nil))))))) (exec-concl (cons 'equal (cons (cons 'exec-fun (cons (cons 'ident (cons (symbol-name fn) 'nil)) (cons (cons 'list init-formals) (cons compst-var (cons fenv-var (cons limit-var 'nil)))))) (cons (cons 'mv (cons result-var (cons new-compst 'nil))) 'nil)))) (type-hyps (cons fn-guard formals)) ((mv type-concl &) (atc-gen-term-type-formula (cons fn formals) body-type affect (list typed-formals) prec-tags)) (exec-formula (cons 'implies (cons exec-hyps (cons (cons 'b* (cons (cons (cons fn-binder (cons (cons fn formals) 'nil)) 'nil) (cons exec-concl 'nil))) 'nil)))) (type-formula (cons 'implies (cons type-hyps (cons type-concl 'nil)))) (lemma-formula (cons 'and (cons exec-formula (cons type-formula 'nil)))) (valuep-when-type-pred (and result-var (atc-type-to-valuep-thm body-type prec-tags))) (type-of-value-when-type-pred (and result-var (atc-type-to-type-of-value-thm body-type prec-tags))) (type-to-quoted-thm? (and result-var (atc-type-to-type-to-quoted-thms body-type prec-tags))) (lemma-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-fun-open (cons 'not-zp-of-limit-variable (cons fn-fun-env-thm (cons init-scope-expand-thm (cons init-scope-scopep-thm (cons push-init-thm (cons body-thm (cons '(:e fun-info->body) (cons 'mv-nth-of-cons (cons '(:e zp) (cons 'value-optionp-when-valuep (cons '(:e value-optionp) (cons '(:e type-of-value-option) (append (and result-var (list* valuep-when-type-pred type-of-value-when-type-pred type-to-quoted-thm?)) (cons 'type-of-value-option-when-valuep (cons '(:e fun-info->result) (cons '(:e tyname-to-type) (append (and result-var (type-integerp body-type) (cons (cons ':e (cons (pack 'type- (type-kind body-type)) 'nil)) 'nil)) (cons pop-frame-thm (cons fn-def* '(declar assign))))))))))))))))))))) 'nil)) 'nil))) 'nil)) ((mv lemma-event &) (evmac-generate-defthm lemma-name :formula lemma-formula :hints lemma-hints :enable nil)) (name (cdr (assoc-eq fn fn-thms))) (formula (cons 'implies (cons (cons 'and (cons (cons 'compustatep (cons compst-var 'nil)) (append context-preamble (cons (untranslate$ (uguard+ fn wrld) nil state) (cons (cons 'integerp (cons limit-var 'nil)) (cons (cons '>= (cons limit-var (cons limit 'nil))) 'nil)))))) (cons (cons 'b* (cons (cons (cons fn-binder (cons (cons fn formals) 'nil)) 'nil) (cons exec-concl 'nil))) 'nil)))) (hints (cons (cons '"Goal" (cons ':use (cons lemma-name (cons ':in-theory (cons (cons 'quote (cons (cons fn-guard 'nil) 'nil)) 'nil))))) 'nil)) ((mv local-event exported-event) (evmac-generate-defthm name :formula formula :hints hints :enable nil)) (print-event (cons 'cw-event (cons '"~%~x0~|" (cons (cons 'quote (cons exported-event 'nil)) 'nil))))) (mv (list lemma-event local-event exported-event) print-event name lemma-name names-to-avoid))))
Theorem:
(defthm pseudo-event-form-listp-of-atc-gen-fun-correct-thm.events (b* (((mv ?events ?print-event ?name ?lemma-name ?names-to-avoid) (atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals affect typed-formals context-preamble compst-var fenv-var limit-var fn-thms fn-fun-env-thm init-scope-expand-thm init-scope-scopep-thm push-init-thm pop-frame-thm body-thm body-type body-limit prec-tags prec-objs names-to-avoid state))) (pseudo-event-form-listp events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-formp-of-atc-gen-fun-correct-thm.print-event (b* (((mv ?events ?print-event ?name ?lemma-name ?names-to-avoid) (atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals affect typed-formals context-preamble compst-var fenv-var limit-var fn-thms fn-fun-env-thm init-scope-expand-thm init-scope-scopep-thm push-init-thm pop-frame-thm body-thm body-type body-limit prec-tags prec-objs names-to-avoid state))) (pseudo-event-formp print-event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-fun-correct-thm.name (implies (symbol-symbol-alistp fn-thms) (b* (((mv ?events ?print-event ?name ?lemma-name ?names-to-avoid) (atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals affect typed-formals context-preamble compst-var fenv-var limit-var fn-thms fn-fun-env-thm init-scope-expand-thm init-scope-scopep-thm push-init-thm pop-frame-thm body-thm body-type body-limit prec-tags prec-objs names-to-avoid state))) (symbolp name))) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-fun-correct-thm.lemma-name (b* (((mv ?events ?print-event ?name ?lemma-name ?names-to-avoid) (atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals affect typed-formals context-preamble compst-var fenv-var limit-var fn-thms fn-fun-env-thm init-scope-expand-thm init-scope-scopep-thm push-init-thm pop-frame-thm body-thm body-type body-limit prec-tags prec-objs names-to-avoid state))) (symbolp lemma-name)) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-fun-correct-thm.names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?events ?print-event ?name ?lemma-name ?names-to-avoid) (atc-gen-fun-correct-thm fn fn-guard fn-def* init-formals affect typed-formals context-preamble compst-var fenv-var limit-var fn-thms fn-fun-env-thm init-scope-expand-thm init-scope-scopep-thm push-init-thm pop-frame-thm body-thm body-type body-limit prec-tags prec-objs names-to-avoid state))) (symbol-listp names-to-avoid))) :rule-classes :rewrite)