		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-expr-const

Equality transformation of a constant.

Signature
(xeq-expr-const const info gin) → (mv expr gout)
Arguments: const — Guard (constp const).; info — Guard (expr-const-infop info).; gin — Guard (ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (goutp gout).

Since a constant has no sub-constructs, this is a special case of lifting equalities (see discussion in proof-generation), where there is no equality of sub-constructs to lift, but we just generate a new expression that is identical to the old one, with an equality theorem about them; but, importantly, the theorem includes assertions about the type of the variable and the preservation of variables (see gen-expr-thm).

We generate a theorem if the constant is an integer one, and under the following additional conditions:

If the constant has type (signed or unsigned) int, it fits in 32 bits.
If the constant has type (signed or unsigned) long, it fits in 64 bits.
If the constant has type (signed or unsigned) long long, it fits in 64 bits.

The reason for these additional conditions is that our current dynamic semantics assumes that those types have those sizes, while our validator is more general (c$::valid-iconst takes an implementation environment as input, which specifies the size of those types). Until we extend our dynamic semantics to be more general, we need this additional condition for proof generation.

Definitions and Theorems

Function: xeq-expr-const

(defun xeq-expr-const (const info gin)
 (declare (xargs :guard (and (constp const)
                             (expr-const-infop info)
                             (ginp gin))))
 (declare (xargs :guard (const-annop const)))
 (let ((__function__ 'xeq-expr-const))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (info (expr-const-info-fix info))
    (expr (make-expr-const :const const
                           :info info))
    (gout-no-thm (gout-no-thm gin))
    ((unless (const-case const :int))
     (mv expr gout-no-thm))
    ((iconst iconst)
     (const-int->iconst const))
    ((iconst-info info) iconst.info)
    ((unless (or (and (type-case info.type :sint)
                      (<= info.value (c::sint-max)))
                 (and (type-case info.type :uint)
                      (<= info.value (c::uint-max)))
                 (and (type-case info.type :slong)
                      (<= info.value (c::slong-max)))
                 (and (type-case info.type :ulong)
                      (<= info.value (c::ulong-max)))
                 (and (type-case info.type :sllong)
                      (<= info.value (c::sllong-max)))
                 (and (type-case info.type :ullong)
                      (<= info.value (c::ullong-max)))))
     (mv expr gout-no-thm))
    ((mv & cconst) (c$::ldm-const const))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::expr-const)
            (:e c::const-kind)
            (:e c::const-int->get)
            (:e c::check-iconst)
            (:e c::typep)
            expr-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            ':instance
            (cons 'expr-const-congruence
                  (cons (cons 'const
                              (cons (cons 'quote (cons cconst 'nil))
                                    'nil))
                        'nil)))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-expr-thm expr expr gin.vartys
                   gin.const-new gin.thm-index hints)))
   (mv expr
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

Theorem: exprp-of-xeq-expr-const.expr

(defthm exprp-of-xeq-expr-const.expr
  (b* (((mv ?expr ?gout)
        (xeq-expr-const const info gin)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-expr-const.gout

(defthm goutp-of-xeq-expr-const.gout
  (b* (((mv ?expr ?gout)
        (xeq-expr-const const info gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-xeq-expr-const

(defthm expr-unambp-of-xeq-expr-const
  (b* (((mv ?expr ?gout)
        (xeq-expr-const const info gin)))
    (expr-unambp expr)))

Theorem: expr-annop-of-xeq-expr-const

(defthm expr-annop-of-xeq-expr-const
  (implies (and (const-annop const)
                (expr-const-infop info))
           (b* (((mv ?expr ?gout)
                 (xeq-expr-const const info gin)))
             (expr-annop expr))))

Theorem: expr-aidentp-of-xeq-expr-const

(defthm expr-aidentp-of-xeq-expr-const
  (implies (const-aidentp const gcc)
           (b* (((mv ?expr ?gout)
                 (xeq-expr-const const info gin)))
             (expr-aidentp expr gcc))))

Theorem: xeq-expr-const-of-const-fix-const

(defthm xeq-expr-const-of-const-fix-const
  (equal (xeq-expr-const (const-fix const)
                         info gin)
         (xeq-expr-const const info gin)))

Theorem: xeq-expr-const-const-equiv-congruence-on-const

(defthm xeq-expr-const-const-equiv-congruence-on-const
  (implies (c$::const-equiv const const-equiv)
           (equal (xeq-expr-const const info gin)
                  (xeq-expr-const const-equiv info gin)))
  :rule-classes :congruence)

Theorem: xeq-expr-const-of-expr-const-info-fix-info

(defthm xeq-expr-const-of-expr-const-info-fix-info
  (equal (xeq-expr-const const (expr-const-info-fix info)
                         gin)
         (xeq-expr-const const info gin)))

Theorem: xeq-expr-const-expr-const-info-equiv-congruence-on-info

(defthm xeq-expr-const-expr-const-info-equiv-congruence-on-info
  (implies (c$::expr-const-info-equiv info info-equiv)
           (equal (xeq-expr-const const info gin)
                  (xeq-expr-const const info-equiv gin)))
  :rule-classes :congruence)

Theorem: xeq-expr-const-of-gin-fix-gin

(defthm xeq-expr-const-of-gin-fix-gin
  (equal (xeq-expr-const const info (gin-fix gin))
         (xeq-expr-const const info gin)))

Theorem: xeq-expr-const-gin-equiv-congruence-on-gin

(defthm xeq-expr-const-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (xeq-expr-const const info gin)
                  (xeq-expr-const const info gin-equiv)))
  :rule-classes :congruence)