Generate an empty list of block items.
(atc-gen-block-item-list-none term gin state) → gout
The empty list of block items itself is trivial of course, but we also generate a theorem about exec-block-item-list applied to the empty list of block items. This provide uniformity with non-empty lists of block items, when lists of block items that may be empty or not are involved within larger constructs.
We return 1 as the limit, which is needed in exec-block-item-list to not return an error due to the limit being exhausted.
Function:
(defun atc-gen-block-item-list-none (term gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (pseudo-termp term) (stmt-ginp gin)))) (let ((__function__ 'atc-gen-block-item-list-none)) (declare (ignorable __function__)) (b* (((stmt-gin gin) gin) (wrld (w state)) (limit (pseudo-term-quote 1)) ((when (not gin.proofs)) (make-stmt-gout :items nil :type (type-void) :term term :context gin.context :inscope gin.inscope :limit limit :events nil :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid)) (name (pack gin.fn '-correct- gin.thm-index)) ((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix name nil gin.names-to-avoid wrld)) (thm-index (1+ gin.thm-index)) (exec-formula (cons 'equal (cons (cons 'exec-block-item-list (cons 'nil (cons gin.compst-var (cons gin.fenv-var (cons gin.limit-var 'nil))))) (cons (cons 'mv (cons 'nil (cons gin.compst-var 'nil))) 'nil)))) (exec-formula (atc-contextualize exec-formula gin.context gin.fn gin.fn-guard gin.compst-var gin.limit-var limit t wrld)) ((mv type-formula type-thms) (atc-gen-term-type-formula (untranslate$ term nil state) (type-void) gin.affect gin.inscope gin.prec-tags)) (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 'exec-block-item-list-of-nil (cons 'not-zp-of-limit-variable (cons 'compustatep-of-add-frame (cons 'compustatep-of-enter-scope (cons 'compustatep-of-exit-scope (cons 'compustatep-of-add-var (cons 'compustatep-of-update-var (cons 'compustatep-of-update-object (cons 'compustatep-of-update-static-var (cons 'compustatep-of-if*-when-both-compustatep (append type-thms '(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 mv-nth-of-cons (:e zp))))))))))))) 'nil)) 'nil))) 'nil)) ((mv event &) (evmac-generate-defthm name :formula formula :hints hints :enable nil))) (make-stmt-gout :items nil :type (type-void) :term term :context gin.context :inscope gin.inscope :limit limit :events (list event) :thm-name name :thm-index thm-index :names-to-avoid names-to-avoid))))
Theorem:
(defthm stmt-goutp-of-atc-gen-block-item-list-none (b* ((gout (atc-gen-block-item-list-none term gin state))) (stmt-goutp gout)) :rule-classes :rewrite)