		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-block-item-asg

Generate a C block item that consists of a given assignment.

Signature
(atc-gen-block-item-asg asg asg-limit asg-events asg-thm-name new-compst gin state) → (mv item item-limit item-events item-thm thm-index names-to-avoid)
Arguments: asg — Guard (exprp asg).; asg-limit — Guard (pseudo-termp asg-limit).; asg-events — Guard (pseudo-event-form-listp asg-events).; asg-thm-name — Guard (symbolp asg-thm-name).; new-compst — An untranslated term.; gin — Guard (stmt-ginp gin).
Returns: item — Type (block-itemp item).; item-limit — Type (pseudo-termp item-limit).; item-events — Type (pseudo-event-form-listp item-events), given (pseudo-event-form-listp asg-events).; item-thm — Type (symbolp item-thm).; thm-index — Type (posp thm-index).; names-to-avoid — Type (symbol-listp names-to-avoid).

This lifts an assignment to a block item with the assignment. It also lifts the theorem about the assignment to a theorem about the block item.

We increase the limit by 1, because we need 1 to go from exec-stmt to its :expr case and to exec-expr.

Definitions and Theorems

Function: atc-gen-block-item-asg

(defun atc-gen-block-item-asg
       (asg asg-limit asg-events
            asg-thm-name new-compst gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (exprp asg)
                             (pseudo-termp asg-limit)
                             (pseudo-event-form-listp asg-events)
                             (symbolp asg-thm-name)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-block-item-asg))
  (declare (ignorable __function__))
  (b*
   (((stmt-gin gin) gin)
    (wrld (w state))
    (stmt (stmt-expr asg))
    (stmt-thm-name (pack gin.fn '-correct- gin.thm-index))
    ((mv stmt-thm-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          stmt-thm-name
          nil gin.names-to-avoid wrld))
    (thm-index (1+ gin.thm-index))
    (stmt-limit (cons '+
                      (cons ''1 (cons asg-limit 'nil))))
    (stmt-formula
     (cons
         'equal
         (cons (cons 'exec-stmt
                     (cons (cons 'quote (cons stmt 'nil))
                           (cons gin.compst-var
                                 (cons gin.fenv-var
                                       (cons gin.limit-var 'nil)))))
               (cons (cons 'mv
                           (cons '(stmt-value-none)
                                 (cons new-compst 'nil)))
                     'nil))))
    (stmt-formula
         (atc-contextualize stmt-formula gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var stmt-limit t wrld))
    (stmt-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            'exec-stmt-when-expr
            (cons
             '(:e stmt-kind)
             (cons
              'not-zp-of-limit-variable
              (cons
                 '(:e stmt-expr->get)
                 (cons asg-thm-name
                       '(compustatep-of-update-var
                             compustatep-of-update-object
                             compustatep-of-update-static-var
                             mv-nth-of-cons (:e zp)
                             (:e value-optionp)
                             valuep-when-ucharp valuep-when-scharp
                             valuep-when-ushortp valuep-when-sshortp
                             valuep-when-uintp valuep-when-sintp
                             valuep-when-ulongp valuep-when-slongp
                             valuep-when-ullongp valuep-when-sllongp
                             value-optionp-when-valuep
                             expr-value-optionp-when-expr-valuep
                             expr-valuep-of-expr-value))))))
           'nil))
         'nil)))
      'nil))
    ((mv stmt-event &)
     (evmac-generate-defthm stmt-thm-name
                            :formula stmt-formula
                            :hints stmt-hints
                            :enable nil)))
   (atc-gen-block-item-stmt
        stmt stmt-limit
        (append asg-events (list stmt-event))
        stmt-thm-name nil (type-void)
        '(stmt-value-none)
        new-compst
        (change-stmt-gin gin
                         :thm-index thm-index
                         :names-to-avoid names-to-avoid
                         :proofs (and stmt-thm-name t))
        state))))

Theorem: block-itemp-of-atc-gen-block-item-asg.item

(defthm block-itemp-of-atc-gen-block-item-asg.item
  (b* (((mv ?item ?item-limit ?item-events
            ?item-thm ?thm-index ?names-to-avoid)
        (atc-gen-block-item-asg asg asg-limit asg-events
                                asg-thm-name new-compst gin state)))
    (block-itemp item))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-gen-block-item-asg.item-limit

(defthm pseudo-termp-of-atc-gen-block-item-asg.item-limit
  (b* (((mv ?item ?item-limit ?item-events
            ?item-thm ?thm-index ?names-to-avoid)
        (atc-gen-block-item-asg asg asg-limit asg-events
                                asg-thm-name new-compst gin state)))
    (pseudo-termp item-limit))
  :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-atc-gen-block-item-asg.item-events

(defthm
      pseudo-event-form-listp-of-atc-gen-block-item-asg.item-events
 (implies
  (pseudo-event-form-listp asg-events)
  (b* (((mv ?item ?item-limit ?item-events
            ?item-thm ?thm-index ?names-to-avoid)
        (atc-gen-block-item-asg asg asg-limit asg-events
                                asg-thm-name new-compst gin state)))
    (pseudo-event-form-listp item-events)))
 :rule-classes :rewrite)

Theorem: symbolp-of-atc-gen-block-item-asg.item-thm

(defthm symbolp-of-atc-gen-block-item-asg.item-thm
  (b* (((mv ?item ?item-limit ?item-events
            ?item-thm ?thm-index ?names-to-avoid)
        (atc-gen-block-item-asg asg asg-limit asg-events
                                asg-thm-name new-compst gin state)))
    (symbolp item-thm))
  :rule-classes :rewrite)

Theorem: posp-of-atc-gen-block-item-asg.thm-index

(defthm posp-of-atc-gen-block-item-asg.thm-index
  (b* (((mv ?item ?item-limit ?item-events
            ?item-thm ?thm-index ?names-to-avoid)
        (atc-gen-block-item-asg asg asg-limit asg-events
                                asg-thm-name new-compst gin state)))
    (posp thm-index))
  :rule-classes (:rewrite :type-prescription))

Theorem: symbol-listp-of-atc-gen-block-item-asg.names-to-avoid

(defthm symbol-listp-of-atc-gen-block-item-asg.names-to-avoid
  (b* (((mv ?item ?item-limit ?item-events
            ?item-thm ?thm-index ?names-to-avoid)
        (atc-gen-block-item-asg asg asg-limit asg-events
                                asg-thm-name new-compst gin state)))
    (symbol-listp names-to-avoid))
  :rule-classes :rewrite)