Generate a correctness theorem for a boolean expression execution.
(atc-gen-expr-bool-correct-thm fn fn-guard context expr type aterm cterm objdes compst-var hints instructions prec-tags thm-index names-to-avoid state) → (mv thm-event thm-name thm-index names-to-avoid)
This is similar to atc-gen-expr-pure-correct-thm, but with some important differences.
The ACL2 term from which the C expression is generated is boolean-valued,
so the execution of the expression cannot be equal to the term.
Instead, there must be another ACL2 term,
whose value is (the ACL2 model of) a C value,
that the expression execution is equated to in the theorem.
The two terms are
While atc-gen-expr-pure-correct-thm generates a theorem
whose conclusion consists of two conjuncts,
namely the equation with the expression execution
and the type predicate applied to the term,
here we generate four conjuncts.
The first two are similar to atc-gen-expr-pure-correct-thm,
but we use
The reason for the form of this theorem is that
the symbolic execution rules have separate binding hypotheses
for executing the expression and for applying test-value:
for example, see the
Function:
(defun atc-gen-expr-bool-correct-thm (fn fn-guard context expr type aterm cterm 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 aterm) (pseudo-termp cterm) (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-bool-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)) (uaterm (untranslate$ aterm nil state)) (ucterm (untranslate$ cterm 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 ucterm (cons uobjdes 'nil))) 'nil)))) (exec-formula (atc-contextualize exec-formula context fn fn-guard compst-var nil nil t wrld)) (type-formula (cons 'and (cons (cons type-pred (cons ucterm 'nil)) (cons (cons 'equal (cons (cons 'test-value (cons ucterm 'nil)) (cons uaterm 'nil))) (cons (cons 'booleanp (cons uaterm 'nil)) '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-bool-correct-thm.thm-event (b* (((mv ?thm-event ?thm-name ?thm-index ?names-to-avoid) (atc-gen-expr-bool-correct-thm fn fn-guard context expr type aterm cterm 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-bool-correct-thm.thm-name (b* (((mv ?thm-event ?thm-name ?thm-index ?names-to-avoid) (atc-gen-expr-bool-correct-thm fn fn-guard context expr type aterm cterm 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-bool-correct-thm.thm-index (implies (posp thm-index) (b* (((mv ?thm-event ?thm-name ?thm-index ?names-to-avoid) (atc-gen-expr-bool-correct-thm fn fn-guard context expr type aterm cterm 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-bool-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-bool-correct-thm fn fn-guard context expr type aterm cterm objdes compst-var hints instructions prec-tags thm-index names-to-avoid state))) (symbol-listp names-to-avoid))) :rule-classes :rewrite)