(svstmtlist-compile-top x &key sclimit (nb-delayp 't)) → (mv ok warnings final-st constraints blk-masks nonblk-masks)
Function:
(defun svstmtlist-compile-top-fn (x sclimit nb-delayp) (declare (xargs :guard (and (svstmtlist-p x) (natp sclimit)))) (let ((__function__ 'svstmtlist-compile-top)) (declare (ignorable __function__)) (b* (((mv ok warnings st jst blk-masks nonblk-masks) (svstmtlist-compile x (make-svstate) sclimit nb-delayp nil nil nil)) ((svjumpstate jst)) (final-st (svstate-fork (svstate-merge-branches jst.returncond jst.returnst st)))) (svjumpstate-free jst) (svstate-free st) (mv ok warnings final-st jst.constraints blk-masks nonblk-masks))))
Theorem:
(defthm vl-warninglist-p-of-svstmtlist-compile-top.warnings (b* (((mv vl::?ok vl::?warnings ?final-st ?constraints ?blk-masks ?nonblk-masks) (svstmtlist-compile-top-fn x sclimit nb-delayp))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm svstate-p-of-svstmtlist-compile-top.final-st (b* (((mv vl::?ok vl::?warnings ?final-st ?constraints ?blk-masks ?nonblk-masks) (svstmtlist-compile-top-fn x sclimit nb-delayp))) (svstate-p final-st)) :rule-classes :rewrite)
Theorem:
(defthm constraintlist-p-of-svstmtlist-compile-top.constraints (b* (((mv vl::?ok vl::?warnings ?final-st ?constraints ?blk-masks ?nonblk-masks) (svstmtlist-compile-top-fn x sclimit nb-delayp))) (constraintlist-p constraints)) :rule-classes :rewrite)
Theorem:
(defthm 4vmask-alist-p-of-svstmtlist-compile-top.blk-masks (b* (((mv vl::?ok vl::?warnings ?final-st ?constraints ?blk-masks ?nonblk-masks) (svstmtlist-compile-top-fn x sclimit nb-delayp))) (4vmask-alist-p blk-masks)) :rule-classes :rewrite)
Theorem:
(defthm 4vmask-alist-p-of-svstmtlist-compile-top.nonblk-masks (b* (((mv vl::?ok vl::?warnings ?final-st ?constraints ?blk-masks ?nonblk-masks) (svstmtlist-compile-top-fn x sclimit nb-delayp))) (4vmask-alist-p nonblk-masks)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-svstmtlist-compile-top (b* (((mv vl::?ok vl::?warnings ?final-st ?constraints ?blk-masks ?nonblk-masks) (svstmtlist-compile-top-fn x sclimit nb-delayp))) (implies (and (svarlist-addr-p (svstmtlist-vars x)) ok) (and (svarlist-addr-p (svstate-vars final-st)) (svarlist-addr-p (constraintlist-vars constraints))))))
Theorem:
(defthm svstmtlist-compile-top-fn-of-svstmtlist-fix-x (equal (svstmtlist-compile-top-fn (svstmtlist-fix x) sclimit nb-delayp) (svstmtlist-compile-top-fn x sclimit nb-delayp)))
Theorem:
(defthm svstmtlist-compile-top-fn-svstmtlist-equiv-congruence-on-x (implies (svstmtlist-equiv x x-equiv) (equal (svstmtlist-compile-top-fn x sclimit nb-delayp) (svstmtlist-compile-top-fn x-equiv sclimit nb-delayp))) :rule-classes :congruence)
Theorem:
(defthm svstmtlist-compile-top-fn-of-nfix-sclimit (equal (svstmtlist-compile-top-fn x (nfix sclimit) nb-delayp) (svstmtlist-compile-top-fn x sclimit nb-delayp)))
Theorem:
(defthm svstmtlist-compile-top-fn-nat-equiv-congruence-on-sclimit (implies (nat-equiv sclimit sclimit-equiv) (equal (svstmtlist-compile-top-fn x sclimit nb-delayp) (svstmtlist-compile-top-fn x sclimit-equiv nb-delayp))) :rule-classes :congruence)