Generate a C block item that consists of a given assignment.
(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)
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.
Function:
(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)) (expr-thm-name (pack gin.fn '-correct- gin.thm-index)) ((mv expr-thm-name names-to-avoid) (fresh-logical-name-with-$s-suffix expr-thm-name nil gin.names-to-avoid wrld)) (thm-index (1+ gin.thm-index)) (expr-limit (cons 'binary-+ (cons ''1 (cons asg-limit 'nil)))) (expr-formula (cons 'equal (cons (cons 'exec-expr-call-or-asg (cons (cons 'quote (cons asg 'nil)) (cons gin.compst-var (cons gin.fenv-var (cons gin.limit-var 'nil))))) (cons new-compst 'nil)))) (expr-formula (atc-contextualize expr-formula gin.context gin.fn gin.fn-guard gin.compst-var gin.limit-var expr-limit t wrld)) (expr-hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons 'exec-expr-call-or-asg-when-asg (cons '(:e expr-kind) (cons 'not-zp-of-limit-variable (cons 'compustatep-of-add-frame (cons 'compustatep-of-add-var (cons 'compustatep-of-enter-scope (cons 'compustatep-of-update-var (cons 'compustatep-of-update-object (cons 'compustatep-of-update-static-var (cons asg-thm-name 'nil)))))))))) 'nil)) 'nil))) 'nil)) ((mv expr-event &) (evmac-generate-defthm expr-thm-name :formula expr-formula :hints expr-hints :enable nil)) (stmt (stmt-expr asg)) (stmt-thm-name (pack gin.fn '-correct- thm-index)) ((mv stmt-thm-name names-to-avoid) (fresh-logical-name-with-$s-suffix stmt-thm-name nil names-to-avoid wrld)) (thm-index (1+ thm-index)) (stmt-limit (cons 'binary-+ (cons ''1 (cons expr-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 'nil (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 expr-thm-name '(compustatep-of-update-var compustatep-of-update-object compustatep-of-update-static-var)))))) '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 expr-event stmt-event)) stmt-thm-name nil (type-void) nil new-compst (change-stmt-gin gin :thm-index thm-index :names-to-avoid names-to-avoid :proofs (and stmt-thm-name t)) state))))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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)