Generate a correctness theorem for a pure expression execution.
(atc-gen-expr-pure-correct-thm fn fn-guard context expr type term1 term2 objdes compst-var hints instructions prec-tags thm-index names-to-avoid state) → (mv thm-event thm-name thm-index names-to-avoid)
The function
As theorem name, we combine
The theorem says that
exec-expr-pure called on the quoted expression
is the same as
The hints or instructions to prove the theorem are passed as input, because they depend on the specifics of the expression.
Function:
(defun atc-gen-expr-pure-correct-thm (fn fn-guard context expr type term1 term2 objdes compst-var hints instructions prec-tags thm-index names-to-avoid state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp fn) (symbolp fn-guard) (atc-contextp context) (exprp expr) (typep type) (pseudo-termp term1) (pseudo-termp term2) (pseudo-termp objdes) (symbolp compst-var) (true-listp hints) (true-listp instructions) (atc-string-taginfo-alistp prec-tags) (posp thm-index) (symbol-listp names-to-avoid)))) (let ((__function__ 'atc-gen-expr-pure-correct-thm)) (declare (ignorable __function__)) (b* ((wrld (w state)) (name (pack fn '-correct- thm-index)) ((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix name nil names-to-avoid wrld)) (thm-index (1+ thm-index)) (type-pred (atc-type-to-recognizer type prec-tags)) (uterm1 (untranslate$ term1 nil state)) (uterm2 (untranslate$ term2 nil state)) (uobjdes (untranslate$ objdes nil state)) (exec-formula (cons 'equal (cons (cons 'exec-expr-pure (cons (cons 'quote (cons expr 'nil)) (cons compst-var 'nil))) (cons (cons 'expr-value (cons uterm1 (cons uobjdes 'nil))) 'nil)))) (exec-formula (atc-contextualize exec-formula context fn fn-guard compst-var nil nil t wrld)) (type-formula (cons type-pred (cons uterm2 'nil))) (type-formula (atc-contextualize type-formula context fn fn-guard nil nil nil nil wrld)) (formula (cons 'and (cons exec-formula (cons type-formula 'nil)))) ((mv event &) (evmac-generate-defthm name :formula formula :hints hints :instructions instructions :enable nil))) (mv event name thm-index names-to-avoid))))
Theorem:
(defthm pseudo-event-formp-of-atc-gen-expr-pure-correct-thm.thm-event (b* (((mv ?thm-event ?thm-name ?thm-index ?names-to-avoid) (atc-gen-expr-pure-correct-thm fn fn-guard context expr type term1 term2 objdes compst-var hints instructions prec-tags thm-index names-to-avoid state))) (pseudo-event-formp thm-event)) :rule-classes :rewrite)
Theorem:
(defthm symbolp-of-atc-gen-expr-pure-correct-thm.thm-name (b* (((mv ?thm-event ?thm-name ?thm-index ?names-to-avoid) (atc-gen-expr-pure-correct-thm fn fn-guard context expr type term1 term2 objdes compst-var hints instructions prec-tags thm-index names-to-avoid state))) (symbolp thm-name)) :rule-classes :rewrite)
Theorem:
(defthm posp-of-atc-gen-expr-pure-correct-thm.thm-index (implies (posp thm-index) (b* (((mv ?thm-event ?thm-name ?thm-index ?names-to-avoid) (atc-gen-expr-pure-correct-thm fn fn-guard context expr type term1 term2 objdes compst-var hints instructions prec-tags thm-index names-to-avoid state))) (posp thm-index))) :rule-classes :rewrite)
Theorem:
(defthm symbol-listp-of-atc-gen-expr-pure-correct-thm.names-to-avoid (implies (symbol-listp names-to-avoid) (b* (((mv ?thm-event ?thm-name ?thm-index ?names-to-avoid) (atc-gen-expr-pure-correct-thm fn fn-guard context expr type term1 term2 objdes compst-var hints instructions prec-tags thm-index names-to-avoid state))) (symbol-listp names-to-avoid))) :rule-classes :rewrite)