Safely zero-extend an already-sized, unsigned expression to finalwidth.
(vl-expandsizes-zeroextend x finalwidth ctx warnings) → (mv successp warnings new-x)
Warning: this function should typically only be called by the expression-sizing transform.
If an extension is needed, we introduce an explicit concatenation, e.g., if
we are expanding
Function:
(defun vl-expandsizes-zeroextend (x finalwidth ctx warnings) (declare (xargs :guard (and (vl-expr-p x) (natp finalwidth) (vl-context-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (vl-expr->finalwidth x) (eq (vl-expr->finaltype x) :vl-unsigned)))) (let ((__function__ 'vl-expandsizes-zeroextend)) (declare (ignorable __function__)) (b* ((x (vl-expr-fix x)) (ctx (vl-context-fix ctx)) (finalwidth (lnfix finalwidth)) (x.finalwidth (lnfix (vl-expr->finalwidth x))) ((when (> x.finalwidth finalwidth)) (mv nil (fatal :type :vl-programming-error :msg "~a0: trying to zero-extend ~a1, which has width ~x2, ~ to ~x3 bits??? Serious bug in our sizing code." :args (list ctx x x.finalwidth finalwidth)) x)) ((when (eql x.finalwidth finalwidth)) (mv t (ok) x)) (pad-width (- finalwidth x.finalwidth)) (zero-guts (make-vl-constint :value 0 :origwidth pad-width :origtype :vl-unsigned :wasunsized nil)) (zero-atom (make-vl-atom :guts zero-guts :finalwidth pad-width :finaltype :vl-unsigned)) (atts (acons (hons-copy "VL_ZERO_EXTENSION") nil nil)) (concat (make-vl-nonatom :op :vl-concat :args (list zero-atom x) :finalwidth finalwidth :finaltype :vl-unsigned :atts atts))) (mv t (ok) concat))))
Theorem:
(defthm booleanp-of-vl-expandsizes-zeroextend.successp (b* (((mv ?successp ?warnings ?new-x) (vl-expandsizes-zeroextend x finalwidth ctx warnings))) (booleanp successp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-warninglist-p-of-vl-expandsizes-zeroextend.warnings (b* (((mv ?successp ?warnings ?new-x) (vl-expandsizes-zeroextend x finalwidth ctx warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm vl-expr-p-of-vl-expandsizes-zeroextend.new-x (b* (((mv ?successp ?warnings ?new-x) (vl-expandsizes-zeroextend x finalwidth ctx warnings))) (vl-expr-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm warning-irrelevance-of-vl-expandsizes-zeroextend (let ((ret1 (vl-expandsizes-zeroextend x finalwidth ctx warnings)) (ret2 (vl-expandsizes-zeroextend x finalwidth nil nil))) (implies (syntaxp (not (and (equal ctx ''nil) (equal warnings ''nil)))) (and (equal (mv-nth 0 ret1) (mv-nth 0 ret2)) (equal (mv-nth 2 ret1) (mv-nth 2 ret2))))))
Theorem:
(defthm vl-expr->finalwidth-of-vl-expandsizes-zeroextend (implies (and (mv-nth 0 (vl-expandsizes-zeroextend x finalwidth ctx warnings)) (force (vl-expr->finalwidth x)) (force (equal (vl-expr->finaltype x) :vl-unsigned))) (equal (vl-expr->finalwidth (mv-nth 2 (vl-expandsizes-zeroextend x finalwidth ctx warnings))) (nfix finalwidth))))
Theorem:
(defthm no-change-loser-of-vl-expandsizes-zeroextend (let ((ret (vl-expandsizes-zeroextend x finalwidth ctx warnings))) (implies (not (mv-nth 0 ret)) (equal (mv-nth 2 ret) (vl-expr-fix x)))))
Theorem:
(defthm vl-expr->finaltype-of-vl-expandsizes-zeroextend (let ((ret (vl-expandsizes-zeroextend x finalwidth ctx warnings))) (implies (and (mv-nth 0 ret) (force (vl-expr->finalwidth x)) (force (equal (vl-expr->finaltype x) :vl-unsigned))) (equal (vl-expr->finaltype (mv-nth 2 ret)) :vl-unsigned))))
Theorem:
(defthm vl-expr-welltyped-p-of-vl-expandsizes-zeroextend (let ((ret (vl-expandsizes-zeroextend x finalwidth ctx warnings))) (implies (and (mv-nth 0 ret) (force (vl-expr-welltyped-p x)) (force (vl-expr->finalwidth x)) (force (equal (vl-expr->finaltype x) :vl-unsigned))) (vl-expr-welltyped-p (mv-nth 2 ret)))))
Theorem:
(defthm vl-expandsizes-zeroextend-of-vl-expr-fix-x (equal (vl-expandsizes-zeroextend (vl-expr-fix x) finalwidth ctx warnings) (vl-expandsizes-zeroextend x finalwidth ctx warnings)))
Theorem:
(defthm vl-expandsizes-zeroextend-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-expandsizes-zeroextend x finalwidth ctx warnings) (vl-expandsizes-zeroextend x-equiv finalwidth ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-expandsizes-zeroextend-of-nfix-finalwidth (equal (vl-expandsizes-zeroextend x (nfix finalwidth) ctx warnings) (vl-expandsizes-zeroextend x finalwidth ctx warnings)))
Theorem:
(defthm vl-expandsizes-zeroextend-nat-equiv-congruence-on-finalwidth (implies (acl2::nat-equiv finalwidth finalwidth-equiv) (equal (vl-expandsizes-zeroextend x finalwidth ctx warnings) (vl-expandsizes-zeroextend x finalwidth-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-expandsizes-zeroextend-of-vl-context-fix-ctx (equal (vl-expandsizes-zeroextend x finalwidth (vl-context-fix ctx) warnings) (vl-expandsizes-zeroextend x finalwidth ctx warnings)))
Theorem:
(defthm vl-expandsizes-zeroextend-vl-context-equiv-congruence-on-ctx (implies (vl-context-equiv ctx ctx-equiv) (equal (vl-expandsizes-zeroextend x finalwidth ctx warnings) (vl-expandsizes-zeroextend x finalwidth ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-expandsizes-zeroextend-of-vl-warninglist-fix-warnings (equal (vl-expandsizes-zeroextend x finalwidth ctx (vl-warninglist-fix warnings)) (vl-expandsizes-zeroextend x finalwidth ctx warnings)))
Theorem:
(defthm vl-expandsizes-zeroextend-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-expandsizes-zeroextend x finalwidth ctx warnings) (vl-expandsizes-zeroextend x finalwidth ctx warnings-equiv))) :rule-classes :congruence)