Generate a list of block items by appending two lists of block items.
(atc-gen-block-item-list-append term items1 items2 items1-limit items2-limit items1-events items2-events items1-thm items2-thm type new-context new-inscope gin state) → gout
Besides concatenating the two lists, which is easy, we also generate a theorem about exec-block-item-list applied to the concatenation, given theorems about exec-block-item-list applied to each of the two lists.
The generated theorem applies exec-block-item-list to a quoted list of block items that is the concatenation. Thus, we cannot just use a rule about exec-block-item-list applied to append. Instead, we need a rule that backchains to two applications of exec-block-item-list to sublists of the quoted list, obtained via take and nthcdr. We generate this rule as a lemma before the theorem.
We need a limit that suffices for all items. We take the sum of the limits of the two lists of items (instead of the maximum), so the term remains linear. That suffices to execute the items from the first list, but we also need to add 1 to the limit because it takes 1 step to go from the end of the first list to starting the second list.
Function:
(defun atc-gen-block-item-list-append (term items1 items2 items1-limit items2-limit items1-events items2-events items1-thm items2-thm type new-context new-inscope gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp term) (block-item-listp items1) (block-item-listp items2) (pseudo-termp items1-limit) (pseudo-termp items2-limit) (pseudo-event-form-listp items1-events) (pseudo-event-form-listp items2-events) (symbolp items1-thm) (symbolp items2-thm) (typep type) (atc-contextp new-context) (atc-symbol-varinfo-alist-listp new-inscope) (stmt-ginp gin)))) (let ((__function__ 'atc-gen-block-item-list-append)) (declare (ignorable __function__)) (b* ((wrld (w state)) ((stmt-gin gin) gin) (items (append items1 items2)) (items-limit (cons 'binary-+ (cons ''1 (cons (cons 'binary-+ (cons items1-limit (cons items2-limit 'nil))) 'nil)))) ((when (not gin.proofs)) (make-stmt-gout :items items :type type :term term :context gin.context :inscope gin.inscope :limit items-limit :events (append items1-events items2-events) :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid)) (lemma-name (pack gin.fn '-exec-block-item-list-concatenation- gin.thm-index)) ((mv lemma-name names-to-avoid) (fresh-logical-name-with-$s-suffix lemma-name nil gin.names-to-avoid wrld)) (thm-index (1+ gin.thm-index)) (n (len items1)) (m (+ n (len items2))) (lemma-formula (cons 'implies (cons (cons 'and (cons (cons 'syntaxp (cons (cons 'and (cons '(quotep items) (cons (cons 'equal (cons '(len (cadr items)) (cons m 'nil))) 'nil))) 'nil)) (cons (cons 'equal (cons '(len items) (cons m 'nil))) (cons '(not (zp limit)) (cons (cons 'equal (cons 'val?+compst1 (cons (cons 'exec-block-item-list (cons (cons 'take (cons n '(items))) '(compst fenv limit))) 'nil))) '((equal val? (mv-nth 0 val?+compst1)) (value-optionp val?) (equal compst1 (mv-nth 1 val?+compst1)))))))) (cons (cons 'equal (cons '(exec-block-item-list items compst fenv limit) (cons (cons 'if (cons '(valuep val?) (cons '(mv val? compst1) (cons (cons 'exec-block-item-list (cons (cons 'nthcdr (cons n '(items))) (cons 'compst1 (cons 'fenv (cons (cons '- (cons 'limit (cons n 'nil))) 'nil))))) 'nil)))) 'nil))) 'nil)))) (lemma-hints (cons (cons '"Goal" (cons ':in-theory (cons ''(append-of-take-and-nthcdr (:e nfix) value-optionp (:e errorp) len-of-take commutativity-of-+) (cons ':use (cons (cons ':instance (cons 'exec-block-item-list-of-append (cons (cons 'items1 (cons (cons 'take (cons n '(items))) 'nil)) (cons (cons 'items2 (cons (cons 'nthcdr (cons n '(items))) 'nil)) 'nil)))) 'nil))))) 'nil)) ((mv lemma-event &) (evmac-generate-defthm lemma-name :formula lemma-formula :hints lemma-hints :enable nil)) (thm-name (pack gin.fn '-correct- thm-index)) ((mv thm-name names-to-avoid) (fresh-logical-name-with-$s-suffix thm-name nil names-to-avoid wrld)) (thm-index (1+ thm-index)) (new-compst (atc-contextualize-compustate gin.compst-var gin.context new-context)) ((mv result type-formula &) (atc-gen-uterm-result-and-type-formula (untranslate$ term nil state) type gin.affect gin.inscope gin.prec-tags)) (exec-formula (cons 'equal (cons (cons 'exec-block-item-list (cons (cons 'quote (cons items 'nil)) (cons gin.compst-var (cons gin.fenv-var (cons gin.limit-var 'nil))))) (cons (cons 'mv (cons result (cons new-compst 'nil))) 'nil)))) (exec-formula (atc-contextualize exec-formula gin.context gin.fn gin.fn-guard gin.compst-var gin.limit-var items-limit t wrld)) (type-formula (atc-contextualize type-formula gin.context gin.fn gin.fn-guard nil nil nil nil wrld)) (formula (cons 'and (cons exec-formula (cons type-formula 'nil)))) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons lemma-name (cons '(:e len) (cons '(:e take) (cons '(:e nthcdr) (cons 'not-zp-of-limit-variable (cons items1-thm (cons 'mv-nth-of-cons (cons '(:e zp) (cons '(:e value-optionp) (cons items2-thm '((:e valuep) uchar-array-length-of-uchar-array-write schar-array-length-of-schar-array-write ushort-array-length-of-ushort-array-write sshort-array-length-of-sshort-array-write uint-array-length-of-uint-array-write sint-array-length-of-sint-array-write ulong-array-length-of-ulong-array-write slong-array-length-of-slong-array-write ullong-array-length-of-ullong-array-write sllong-array-length-of-sllong-array-write))))))))))) 'nil)) 'nil))) 'nil)) ((mv event &) (evmac-generate-defthm thm-name :formula formula :hints hints :enable nil))) (make-stmt-gout :items items :type type :term term :context new-context :inscope new-inscope :limit items-limit :events (append items1-events items2-events (list lemma-event event)) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid))))
Theorem:
(defthm stmt-goutp-of-atc-gen-block-item-list-append (b* ((gout (atc-gen-block-item-list-append term items1 items2 items1-limit items2-limit items1-events items2-events items1-thm items2-thm type new-context new-inscope gin state))) (stmt-goutp gout)) :rule-classes :rewrite)