		Search-engine friendly clone of the ACL2 documentation.

Atc-theorem-generation

Atc-gen-expr-bool-correct-thm

Generate a correctness theorem for a boolean expression execution.

Signature
(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)
Arguments: fn — Guard (symbolp fn).; fn-guard — Guard (symbolp fn-guard).; context — Guard (atc-contextp context).; expr — Guard (exprp expr).; type — Guard (typep type).; aterm — Guard (pseudo-termp aterm).; cterm — Guard (pseudo-termp cterm).; objdes — Guard (pseudo-termp objdes).; compst-var — Guard (symbolp compst-var).; hints — Guard (true-listp hints).; instructions — Guard (true-listp instructions).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).; thm-index — Guard (posp thm-index).; names-to-avoid — Guard (symbol-listp names-to-avoid).
Returns: thm-event — Type (pseudo-event-formp thm-event).; thm-name — Type (symbolp thm-name).; thm-index — Type (posp thm-index), given (posp thm-index).; names-to-avoid — Type (symbol-listp names-to-avoid), given (symbol-listp 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 aterm (for `ACL2 term') and cterm (for `C term'), both passed as parameters to this ACL2 function (unlike the terms term1 and term2 in atc-gen-expr-pure-correct-thm). The two terms and their relation are slightly different for different kinds of boolean expression terms; see the callers of this ACL2 function for details.

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 cterm for that purpose, as explained above. The other two conjuncts refer to aterm instead: they say that test-value applied to cterm yields aterm, and that aterm is a boolean.

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 exec-expr-pure-when-cond rule in atc-exec-expr-pure-rules.

Definitions and Theorems

Function: atc-gen-expr-bool-correct-thm

(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: pseudo-event-formp-of-atc-gen-expr-bool-correct-thm.thm-event

(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: symbolp-of-atc-gen-expr-bool-correct-thm.thm-name

(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: posp-of-atc-gen-expr-bool-correct-thm.thm-index

(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: symbol-listp-of-atc-gen-expr-bool-correct-thm.names-to-avoid

(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)