		Search-engine friendly clone of the ACL2 documentation.

Atc-statement-generation

Atc-gen-block-item-array-asg

Generate a C block item statement that consists of an assignment to an array element.

Signature
(atc-gen-block-item-array-asg var val-term sub-term elem-term elem-type array-write-fn wrapper? gin state) → (mv erp item val-term* limit events thm-name new-inscope new-context thm-index names-to-avoid)
Arguments: var — Guard (symbolp var).; val-term — Guard (pseudo-termp val-term).; sub-term — Guard (pseudo-termp sub-term).; elem-term — Guard (pseudo-termp elem-term).; elem-type — Guard (typep elem-type).; array-write-fn — Guard (symbolp array-write-fn).; wrapper? — Guard (symbolp wrapper?).; gin — Guard (stmt-ginp gin).
Returns: item — Type (block-itemp item).; val-term* — Type (pseudo-termp val-term*), given (symbolp array-write-fn).; limit — Type (pseudo-termp limit).; events — Type (pseudo-event-form-listp events).; thm-name — Type (symbolp thm-name).; new-inscope — Type (atc-symbol-varinfo-alist-listp new-inscope).; new-context — Type (atc-contextp new-context).; thm-index — Type (posp thm-index).; names-to-avoid — Type (symbol-listp names-to-avoid).

This is somewhat analogous to atc-gen-block-item-var-asg.

The limit is set to 4 more than the sum of the limits needed to execute the index and right expressions: 1 to go from exec-block-item to exec-stmt, 1 to go from there to exec-expr on the assignment, 1 to go from there to exec-expr on the left and right sides; the left side is an array subscript expression, so we need 1 more to go to exec-expr on the sub-expressions; the array sub-expression is always a variable so it needs 1 more, which is covered by the limit for the index sub-expression, which is always at least 1, and suffices for the index sub-expression. Instead of adding the limit for the right expression we could take the maximum, but the addition is simpler.

Definitions and Theorems

Function: atc-gen-block-item-array-asg

(defun atc-gen-block-item-array-asg
       (var val-term sub-term elem-term elem-type
            array-write-fn wrapper? gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbolp var)
                             (pseudo-termp val-term)
                             (pseudo-termp sub-term)
                             (pseudo-termp elem-term)
                             (typep elem-type)
                             (symbolp array-write-fn)
                             (symbolp wrapper?)
                             (stmt-ginp gin))))
 (let ((__function__ 'atc-gen-block-item-array-asg))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (irr-block-item)
     nil nil nil nil nil (irr-atc-context)
     1 nil)
    ((stmt-gin gin) gin)
    (wrld (w state))
    ((unless (eq wrapper? nil))
     (reterr
      (msg
       "The array write term ~x0 to which ~x1 is bound ~
               has the ~x2 wrapper, which is disallowed."
       val-term var wrapper?)))
    ((unless (member-eq var gin.affect))
     (reterr
      (msg
       "The array ~x0 is being written to, ~
               but it is not among the variables ~x1 ~
               currently affected."
       var gin.affect)))
    ((erp (expr-gout arr))
     (atc-gen-expr-pure
          var
          (make-expr-gin :context gin.context
                         :inscope gin.inscope
                         :prec-tags gin.prec-tags
                         :fn gin.fn
                         :fn-guard gin.fn-guard
                         :compst-var gin.compst-var
                         :thm-index gin.thm-index
                         :names-to-avoid gin.names-to-avoid
                         :proofs gin.proofs)
          state))
    ((erp (expr-gout sub))
     (atc-gen-expr-pure
          sub-term
          (make-expr-gin :context gin.context
                         :inscope gin.inscope
                         :prec-tags gin.prec-tags
                         :fn gin.fn
                         :fn-guard gin.fn-guard
                         :compst-var gin.compst-var
                         :thm-index arr.thm-index
                         :names-to-avoid arr.names-to-avoid
                         :proofs (and arr.thm-name t))
          state))
    ((erp (expr-gout elem))
     (atc-gen-expr-pure
          elem-term
          (make-expr-gin :context gin.context
                         :inscope gin.inscope
                         :prec-tags gin.prec-tags
                         :fn gin.fn
                         :fn-guard gin.fn-guard
                         :compst-var gin.compst-var
                         :thm-index sub.thm-index
                         :names-to-avoid sub.names-to-avoid
                         :proofs (and sub.thm-name t))
          state))
    ((unless (and (type-case arr.type :array)
                  (equal (type-array->of arr.type)
                         elem-type)))
     (reterr
      (msg
       "The array ~x0 of type ~x1 ~
               does not have the expected array type of ~x2. ~
               This is indicative of ~
               unreachable code under the guards, ~
               given that the code is guard-verified."
       var arr.type elem-type)))
    ((unless (type-integerp sub.type))
     (reterr
      (msg
       "The array ~x0 of type ~x1 ~
               is being indexed with ~
               a subscript ~x2 of non-integer type ~x3, ~
               instead of integer type as expected.
               This is indicative of ~
               unreachable code under the guards, ~
               given that the code is guard-verified."
       var arr.type sub-term sub.type)))
    ((unless (equal elem.type elem-type))
     (reterr
      (msg
       "The array ~x0 of type ~x1 ~
               is being written to with ~
               an element ~x2 of type x3, ~
               instead of type ~x4 as expected.
               This is indicative of ~
               unreachable code under the guards, ~
               given that the code is guard-verified."
       var arr.type
       elem-term elem.type elem-type)))
    (asg (make-expr-binary :op (binop-asg)
                           :arg1 (make-expr-arrsub :arr arr.expr
                                                   :sub sub.expr)
                           :arg2 elem.expr))
    (stmt (stmt-expr asg))
    (item (block-item-stmt stmt))
    ((unless (expr-purep sub.expr))
     (reterr (raise "Internal error: non-pure expression ~x0."
                    sub.expr)))
    ((unless (expr-purep elem.expr))
     (reterr (raise "Internal error: non-pure expression ~x0."
                    elem.expr)))
    (sub-limit (cons 'quote
                     (cons (expr-pure-limit sub.expr) 'nil)))
    (right-limit (cons 'quote
                       (cons (expr-pure-limit elem.expr)
                             'nil)))
    (sub+right-limit
         (cons '+
               (cons sub-limit (cons right-limit 'nil))))
    (left+right-limit (cons '+
                            (cons ''1 (cons sub+right-limit 'nil))))
    (expr-limit (cons '+
                      (cons ''1
                            (cons left+right-limit 'nil))))
    (stmt-limit (cons '+
                      (cons ''1 (cons expr-limit 'nil))))
    (item-limit (cons '+
                      (cons ''1 (cons stmt-limit 'nil))))
    (varinfo (atc-get-var var gin.inscope))
    ((unless varinfo)
     (reterr
          (raise "Internal error: no information for variable ~x0."
                 var)))
    ((when (eq array-write-fn 'quote))
     (reterr (raise "Internal error: array writer is QUOTE.")))
    (array-write-term
         (cons array-write-fn
               (cons var
                     (cons sub.term (cons elem.term 'nil)))))
    ((when (not elem.thm-name))
     (retok item array-write-term item-limit
            (append arr.events sub.events elem.events)
            nil gin.inscope gin.context
            elem.thm-index elem.names-to-avoid))
    (okp-lemma-name (pack gin.fn '-asg-
                          elem.thm-index '-okp-lemma))
    ((mv okp-lemma-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          okp-lemma-name
          nil elem.names-to-avoid wrld))
    (thm-index (1+ elem.thm-index))
    (elem-fixtype (pack (type-kind elem-type)))
    (index-okp (pack elem-fixtype '-array-index-okp))
    (okp-lemma-formula (cons index-okp
                             (cons var (cons sub.term 'nil))))
    (okp-lemma-formula
         (atc-contextualize okp-lemma-formula gin.context gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (okp-lemma-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
          (cons 'quote
                (cons (cons gin.fn-guard '(if* test* declar assign))
                      'nil))
          (cons ':use
                (cons (cons ':guard-theorem
                            (cons gin.fn 'nil))
                      'nil)))))
      'nil))
    ((mv okp-lemma-event &)
     (evmac-generate-defthm okp-lemma-name
                            :formula okp-lemma-formula
                            :hints okp-lemma-hints
                            :enable nil))
    (new-compst
      (if
        (atc-var-info->externalp varinfo)
        (cons 'update-static-var
              (cons (cons 'ident
                          (cons (cons 'quote
                                      (cons (symbol-name var) 'nil))
                                'nil))
                    (cons array-write-term
                          (cons gin.compst-var 'nil))))
        (cons 'update-object
              (cons (add-suffix-to-fn var "-OBJDES")
                    (cons array-write-term
                          (cons gin.compst-var 'nil))))))
    (new-compst (untranslate$ new-compst nil state))
    (asg-thm-name (pack gin.fn '-correct- thm-index))
    ((mv asg-thm-name names-to-avoid)
     (fresh-logical-name-with-$s-suffix
          asg-thm-name nil names-to-avoid wrld))
    (thm-index (1+ thm-index))
    (uterm (untranslate$ elem.term nil state))
    (exec-formula
     (cons
      'equal
      (cons (cons 'exec-expr
                  (cons (cons 'quote (cons asg 'nil))
                        (cons gin.compst-var
                              (cons gin.fenv-var
                                    (cons gin.limit-var 'nil)))))
            (cons (cons 'mv
                        (cons (cons 'expr-value (cons uterm '(nil)))
                              (cons new-compst 'nil)))
                  'nil))))
    (exec-formula
         (atc-contextualize exec-formula gin.context
                            gin.fn gin.fn-guard gin.compst-var
                            gin.limit-var expr-limit t wrld))
    (pred (atc-type-to-recognizer elem.type gin.prec-tags))
    (type-formula (cons pred (cons uterm 'nil)))
    (type-formula
         (atc-contextualize type-formula gin.context gin.fn
                            gin.fn-guard nil nil nil nil wrld))
    (asg-formula
         (cons 'and
               (cons exec-formula (cons type-formula 'nil))))
    (exec-expr-when-asg-arrsub-when-elem-fixtype-arrayp-for-modular-proofs
         (pack 'exec-expr-when-asg-arrsub-when-
               elem-fixtype
               '-arrayp-for-modular-proofs))
    (value-kind-when-sub-type-pred
         (atc-type-to-value-kind-thm sub.type gin.prec-tags))
    (value-kind-when-elem-type-pred
         (atc-type-to-value-kind-thm elem-type gin.prec-tags))
    (valuep-when-sub-type-pred
         (atc-type-to-valuep-thm sub.type gin.prec-tags))
    (valuep-when-elem-type-pred
         (atc-type-to-valuep-thm elem-type gin.prec-tags))
    (valuep-when-arr-type-pred
         (atc-type-to-valuep-thm arr.type gin.prec-tags))
    (sub-type-pred (atc-type-to-recognizer sub.type gin.prec-tags))
    (cintegerp-when-sub-type-pred
         (pack 'cintegerp-when- sub-type-pred))
    (elem-fixtype-arrayp-of-elem-fixtype-array-write
         (pack elem-fixtype '-arrayp-of-
               elem-fixtype '-array-write))
    (elem-fixtype-array-length-of-elem-fixtype-array-write
         (pack elem-fixtype '-array-length-of-
               elem-fixtype '-array-write))
    (type-of-value-when-elem-fixtype-arrayp
         (atc-type-to-type-of-value-thm arr.type gin.prec-tags))
    (value-array->length-when-elem-fixtype-arrayp
         (pack 'value-array->length-when-
               elem-fixtype '-arrayp))
    (apconvert-expr-value-when-elem-fixtype-arrayp
         (pack 'apconvert-expr-value-when-
               elem-fixtype '-arrayp))
    (return-type-of-type-elem-fixtype (pack 'return-type-of-type-
                                            elem-fixtype))
    (asg-hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         (cons
          'quote
          (cons
           (cons
            exec-expr-when-asg-arrsub-when-elem-fixtype-arrayp-for-modular-proofs
            (cons
             '(:e expr-kind)
             (cons
              '(:e expr-binary->op)
              (cons
               '(:e expr-binary->arg1)
               (cons
                '(:e expr-binary->arg2)
                (cons
                 '(:e expr-arrsub->arr)
                 (cons
                  '(:e expr-arrsub->sub)
                  (cons
                   '(:e expr-ident->get)
                   (cons
                    '(:e binop-kind)
                    (cons
                     'not-zp-of-limit-variable
                     (cons
                      'not-zp-of-limit-minus-const
                      (cons
                       arr.thm-name
                       (cons
                        'expr-valuep-of-expr-value
                        (cons
                         'apconvert-expr-value-when-not-value-array
                         (cons
                          'expr-value->value-of-expr-value
                          (cons
                           'value-fix-when-valuep
                           (cons
                            (atc-var-info->thm varinfo)
                            (cons
                             sub.thm-name
                             (cons
                              value-kind-when-sub-type-pred
                              (cons
                               valuep-when-sub-type-pred
                               (cons
                                cintegerp-when-sub-type-pred
                                (cons
                                 okp-lemma-name
                                 (cons
                                  elem.thm-name
                                  (cons
                                   value-kind-when-elem-type-pred
                                   (cons
                                    valuep-when-elem-type-pred
                                    (cons
                                     'write-object-to-update-object
                                     (cons
                                      'write-object-okp-when-valuep-of-read-object-no-syntaxp
                                      (cons
                                       valuep-when-arr-type-pred
                                       (cons
                                        elem-fixtype-arrayp-of-elem-fixtype-array-write
                                        (cons
                                         type-of-value-when-elem-fixtype-arrayp
                                         (cons
                                          value-array->length-when-elem-fixtype-arrayp
                                          (cons
                                           elem-fixtype-array-length-of-elem-fixtype-array-write
                                           (cons
                                            apconvert-expr-value-when-elem-fixtype-arrayp
                                            (cons
                                             'objdesign-optionp-of-objdesign-of-var
                                             (cons
                                              'objdesignp-when-objdesign-optionp
                                              (cons
                                               'return-type-of-value-pointer
                                               (cons
                                                'value-pointer-validp-of-value-pointer
                                                (cons
                                                 'return-type-of-pointer-valid
                                                 (cons
                                                  'value-pointer->reftype-of-value-pointer
                                                  (cons
                                                   'type-fix-when-typep
                                                   (cons
                                                    return-type-of-type-elem-fixtype
                                                    '(value-pointer->designator-of-value-pointer
                                                      pointer-valid->get-of-pointer-valid
                                                      objdesign-fix-when-objdesignp
                                                      write-object-of-objdesign-of-var-to-write-var
                                                      write-var-to-write-static-var
                                                      var-autop-of-add-frame
                                                      var-autop-of-enter-scope
                                                      var-autop-of-add-var
                                                      var-autop-of-update-var
                                                      var-autop-of-update-static-var
                                                      var-autop-of-update-object
                                                      write-static-var-to-update-static-var
                                                      write-static-var-okp-of-add-var
                                                      write-static-var-okp-of-enter-scope
                                                      write-static-var-okp-of-add-frame
                                                      write-static-var-okp-when-valuep-of-read-static-var
                                                      read-object-of-objdesign-static
                                                      ident-fix-when-identp
                                                      identp-of-ident
                                                      equal-of-ident-and-ident
                                                      (:e str-fix)
                                                      compustatep-of-update-object
                                                      compustatep-of-update-static-var
                                                      expr-valuep-of-expr-value
                                                      expr-value->value-of-expr-value
                                                      value-fix-when-valuep
                                                      (:e
                                                       expr-pure-limit)
                                                      (:e
                                                         expr-purep)
                                                      max))))))))))))))))))))))))))))))))))))))))))
           'nil))
         'nil)))
      'nil))
    ((mv asg-event &)
     (evmac-generate-defthm asg-thm-name
                            :formula asg-formula
                            :hints asg-hints
                            :enable nil))
    ((mv item item-limit item-events
         item-thm-name thm-index names-to-avoid)
     (atc-gen-block-item-asg
          asg expr-limit
          (append arr.events sub.events elem.events
                  (list okp-lemma-event asg-event))
          asg-thm-name new-compst
          (change-stmt-gin gin
                           :thm-index thm-index
                           :names-to-avoid names-to-avoid
                           :proofs (and asg-thm-name t))
          state))
    (new-context
     (atc-context-extend
      gin.context
      (list
       (make-atc-premise-cvalue :var var
                                :term array-write-term)
       (make-atc-premise-compustate
          :var gin.compst-var :term
          (if (atc-var-info->externalp varinfo)
              (cons 'update-static-var
                    (cons (cons 'ident
                                (cons (symbol-name var) 'nil))
                          (cons var (cons gin.compst-var 'nil))))
            (cons 'update-object
                  (cons (add-suffix-to-fn var "-OBJDES")
                        (cons var (cons gin.compst-var 'nil)))))))))
    (new-inscope-rules
     (cons
      'objdesign-of-var-of-update-object
      (cons
       'objdesign-of-var-of-enter-scope-iff
       (cons
        'objdesign-of-var-of-add-var-iff
        (cons
         'read-object-auto/static-of-update-object-alloc
         (cons
          'read-object-of-update-object-same
          (cons
           'read-object-of-update-object-disjoint
           (cons
            'read-object-of-objdesign-of-var-of-add-var
            (cons
             'read-object-of-objdesign-of-var-of-enter-scope
             (cons
              'objdesign-kind-of-objdesign-of-var
              (cons
               'compustate-frames-number-of-add-var-not-zero
               (cons
                'compustate-frames-number-of-enter-scope-not-zero
                (cons
                 'object-disjointp-commutative
                 (cons
                  'value-fix-when-valuep
                  (cons
                   'remove-flexible-array-member-when-absent
                   (cons
                    'not-flexible-array-member-p-when-ucharp
                    (cons
                     'not-flexible-array-member-p-when-scharp
                     (cons
                      'not-flexible-array-member-p-when-ushortp
                      (cons
                       'not-flexible-array-member-p-when-sshortp
                       (cons
                        'not-flexible-array-member-p-when-uintp
                        (cons
                         'not-flexible-array-member-p-when-sintp
                         (cons
                          'not-flexible-array-member-p-when-ulongp
                          (cons
                           'not-flexible-array-member-p-when-slongp
                           (cons
                            'not-flexible-array-member-p-when-ullongp
                            (cons
                             'not-flexible-array-member-p-when-sllongp
                             (cons
                              'not-flexible-array-member-p-when-uchar-arrayp
                              (cons
                               'not-flexible-array-member-p-when-schar-arrayp
                               (cons
                                'not-flexible-array-member-p-when-ushort-arrayp
                                (cons
                                 'not-flexible-array-member-p-when-sshort-arrayp
                                 (cons
                                  'not-flexible-array-member-p-when-uint-arrayp
                                  (cons
                                   'not-flexible-array-member-p-when-sint-arrayp
                                   (cons
                                    'not-flexible-array-member-p-when-ulong-arrayp
                                    (cons
                                     'not-flexible-array-member-p-when-slong-arrayp
                                     (cons
                                      'not-flexible-array-member-p-when-ullong-arrayp
                                      (cons
                                       'not-flexible-array-member-p-when-sllong-arrayp
                                       (cons
                                        'not-flexible-array-member-p-when-value-pointer
                                        (cons
                                         'valuep-when-ucharp
                                         (cons
                                          'valuep-when-scharp
                                          (cons
                                           'valuep-when-ushortp
                                           (cons
                                            'valuep-when-sshortp
                                            (cons
                                             'valuep-when-uintp
                                             (cons
                                              'valuep-when-sintp
                                              (cons
                                               'valuep-when-ulongp
                                               (cons
                                                'valuep-when-slongp
                                                (cons
                                                 'valuep-when-ullongp
                                                 (cons
                                                  'valuep-when-sllongp
                                                  (cons
                                                   valuep-when-arr-type-pred
                                                   (cons
                                                    elem-fixtype-arrayp-of-elem-fixtype-array-write
                                                    '(ident-fix-when-identp
                                                      identp-of-ident
                                                      equal-of-ident-and-ident
                                                      (:e str-fix)
                                                      objdesign-of-var-of-update-static-var-iff
                                                      read-object-of-objdesign-of-var-of-update-static-var-different
                                                      read-object-of-objdesign-of-var-of-update-static-var-same
                                                      var-autop-of-add-frame
                                                      var-autop-of-enter-scope
                                                      var-autop-of-add-var
                                                      var-autop-of-update-var
                                                      var-autop-of-update-static-var
                                                      var-autop-of-update-object)))))))))))))))))))))))))))))))))))))))))))))))))
    ((mv new-inscope
         new-inscope-events names-to-avoid)
     (atc-gen-new-inscope gin.fn gin.fn-guard
                          gin.inscope new-context gin.compst-var
                          new-inscope-rules gin.prec-tags
                          thm-index names-to-avoid wrld))
    (thm-index (1+ thm-index))
    (events (append item-events new-inscope-events)))
   (retok item array-write-term item-limit
          events item-thm-name new-inscope
          new-context thm-index names-to-avoid))))

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

(defthm block-itemp-of-atc-gen-block-item-array-asg.item
  (b* (((mv acl2::?erp ?item ?val-term*
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-block-item-array-asg
             var
             val-term sub-term elem-term elem-type
             array-write-fn wrapper? gin state)))
    (block-itemp item))
  :rule-classes :rewrite)

Theorem: pseudo-termp-of-atc-gen-block-item-array-asg.val-term*

(defthm pseudo-termp-of-atc-gen-block-item-array-asg.val-term*
  (implies (symbolp array-write-fn)
           (b* (((mv acl2::?erp ?item ?val-term*
                     ?limit ?events ?thm-name ?new-inscope
                     ?new-context ?thm-index ?names-to-avoid)
                 (atc-gen-block-item-array-asg
                      var
                      val-term sub-term elem-term elem-type
                      array-write-fn wrapper? gin state)))
             (pseudo-termp val-term*)))
  :rule-classes :rewrite)

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

(defthm pseudo-termp-of-atc-gen-block-item-array-asg.limit
  (b* (((mv acl2::?erp ?item ?val-term*
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-block-item-array-asg
             var
             val-term sub-term elem-term elem-type
             array-write-fn wrapper? gin state)))
    (pseudo-termp limit))
  :rule-classes :rewrite)

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

(defthm
     pseudo-event-form-listp-of-atc-gen-block-item-array-asg.events
  (b* (((mv acl2::?erp ?item ?val-term*
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-block-item-array-asg
             var
             val-term sub-term elem-term elem-type
             array-write-fn wrapper? gin state)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

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

(defthm symbolp-of-atc-gen-block-item-array-asg.thm-name
  (b* (((mv acl2::?erp ?item ?val-term*
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-block-item-array-asg
             var
             val-term sub-term elem-term elem-type
             array-write-fn wrapper? gin state)))
    (symbolp thm-name))
  :rule-classes :rewrite)

Theorem: atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-array-asg.new-inscope

(defthm
 atc-symbol-varinfo-alist-listp-of-atc-gen-block-item-array-asg.new-inscope
 (b* (((mv acl2::?erp ?item ?val-term*
           ?limit ?events ?thm-name ?new-inscope
           ?new-context ?thm-index ?names-to-avoid)
       (atc-gen-block-item-array-asg
            var
            val-term sub-term elem-term elem-type
            array-write-fn wrapper? gin state)))
   (atc-symbol-varinfo-alist-listp new-inscope))
 :rule-classes :rewrite)

Theorem: atc-contextp-of-atc-gen-block-item-array-asg.new-context

(defthm atc-contextp-of-atc-gen-block-item-array-asg.new-context
  (b* (((mv acl2::?erp ?item ?val-term*
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-block-item-array-asg
             var
             val-term sub-term elem-term elem-type
             array-write-fn wrapper? gin state)))
    (atc-contextp new-context))
  :rule-classes :rewrite)

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

(defthm posp-of-atc-gen-block-item-array-asg.thm-index
  (b* (((mv acl2::?erp ?item ?val-term*
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-block-item-array-asg
             var
             val-term sub-term elem-term elem-type
             array-write-fn wrapper? gin state)))
    (posp thm-index))
  :rule-classes :rewrite)

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

(defthm symbol-listp-of-atc-gen-block-item-array-asg.names-to-avoid
  (b* (((mv acl2::?erp ?item ?val-term*
            ?limit ?events ?thm-name ?new-inscope
            ?new-context ?thm-index ?names-to-avoid)
        (atc-gen-block-item-array-asg
             var
             val-term sub-term elem-term elem-type
             array-write-fn wrapper? gin state)))
    (symbol-listp names-to-avoid))
  :rule-classes :rewrite)