		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-implementation

Simpadd0-supporting-proofs

Supporting proofs for simpadd0.

Here we prove some general supporting theorems that justify the correctness of the transformation, and that can be leveraged to generate proofs when the transformation is run.

First, we show that an expression satisfying c$::expr-zerop successfully translates via the language definition mapping. This is the expression recognized as ``zero'' by this transformation.

Then we prove, via a few theorems that build on each other, that executing an expression of the form x + 0, where the 0 part is characterized by c$::expr-zerop, is like executing just x, under the assumption that x is accessible in the computation state and contains a value of type int. We use c::valuep and c::value-case to express that the value has type int; since we have available a number of theorems, used in the proofs generated by c::atc, that involve the predicate c::sintp from the shallow embedding, we show that c::sintp is equivalent to the use of c::valuep and c::value-case, so we can relieve the hypotheses of those theorems from the shallow embedding, and prove the theorems below more succinctly.

A subtlety of the theorem about the equivalence of executing x + 0 and x is that expression execution, in our formal semantics, returns an expression value of type c::expr-value, which consists of a value and an optional object designator. The latter is non-nil for lvalues, i.e. expressions that designate an object. While x + 0 is not an lvalue, x is; so, strictly speaking, their execution is not quite equivalent, but the value part of their expression values are the same. This should suffice to generate proofs for this transformation: in valid code, x + 0 is never treated as an lvalue, and so if we replace it with x, the surrounding code, which does not change, just needs the value of x, via the usual lvalue conversion.

Definitions and Theorems

Theorem: ldm-expr-when-expr-zerop

(defthm ldm-expr-when-expr-zerop
 (implies
  (c$::expr-zerop expr)
  (equal
   (c$::ldm-expr expr)
   (mv
    nil
    (c::expr-const
         (c::const-int
              (c::make-iconst :value 0
                              :base (c::iconst-base-oct)
                              :unsignedp nil
                              :length (c::iconst-length-none))))))))

Theorem: sintp-alt-def

(defthm c::sintp-alt-def
  (equal (c::sintp x)
         (and (c::valuep x)
              (c::value-case x :sint))))

Theorem: add-integer-values-of-sint-and-sint0

(defthm c::add-integer-values-of-sint-and-sint0
  (implies (and (c::valuep val)
                (c::value-case val :sint)
                (equal sint0 (c::value-sint 0)))
           (equal (c::add-integer-values val sint0)
                  val)))

Theorem: uaconvert-values-of-sint-and-sint0

(defthm c::uaconvert-values-of-sint-and-sint0
  (implies (and (c::valuep val)
                (c::value-case val :sint)
                (equal sint0 (c::value-sint 0)))
           (equal (c::uaconvert-values val sint0)
                  (mv val sint0))))

Theorem: add-arithmetic-values-of-sint-and-sint0

(defthm c::add-arithmetic-values-of-sint-and-sint0
  (implies (and (c::valuep val)
                (c::value-case val :sint)
                (equal sint0 (c::value-sint 0)))
           (equal (c::add-arithmetic-values val sint0)
                  val)))

Theorem: add-values-of-sint-and-sint0

(defthm c::add-values-of-sint-and-sint0
  (implies (and (c::valuep val)
                (c::value-case val :sint)
                (equal sint0 (c::value-sint 0)))
           (equal (c::add-values val sint0) val)))

Theorem: exec-of-var+zero-to-exec-var

(defthm exec-of-var+zero-to-exec-var
 (implies
  (and (c::objdesign-of-var var compst)
       (c$::expr-zerop zero))
  (b* ((val (c::read-object (c::objdesign-of-var var compst)
                            compst)))
   (implies
    (and (c::valuep val)
         (c::value-case val :sint))
    (equal
        (c::expr-value->value
             (c::exec-expr-pure
                  (c::expr-binary (c::binop-add)
                                  (c::expr-ident var)
                                  (mv-nth 1 (c$::ldm-expr zero)))
                  compst))
        (c::expr-value->value (c::exec-expr-pure (c::expr-ident var)
                                                 compst)))))))