		Search-engine friendly clone of the ACL2 documentation.

Atc-theorem-generation

Atc-gen-expr-pure-correct-thm

Generate a correctness theorem for a pure expression execution.

Signature
(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)
Arguments: fn — Guard (symbolp fn).; fn-guard — Guard (symbolp fn-guard).; context — Guard (atc-contextp context).; expr — Guard (exprp expr).; type — Guard (typep type).; term1 — Guard (pseudo-termp term1).; term2 — Guard (pseudo-termp term2).; 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).

The function fn that the expression is part of is passed as input.

As theorem name, we combine fn with correct and with the theorem index. The name just needs to be unique locally to the call to ATC, so we expect that generally no $ signs will need to be added by fresh-logical-name-with-$s-suffix.

The theorem says that exec-expr-pure called on the quoted expression is the same as term1; it also says that term2 has the expression's type. Often term1 and term2 are the same, but sometimes they differ, e.g. when term1 is a -ptr variable while term2 is the same variable without -ptr. The input objdes is a term that denotes an object designator, or nil if no object designator is applicable: this is the object designator that the expression denotes, if any. The terms are untranslated, to make them more readable, in particular to eliminate quotes before numbers. Terms, expression, and type are passed as inputs.

The hints or instructions to prove the theorem are passed as input, because they depend on the specifics of the expression.

Definitions and Theorems

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

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

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

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

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

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