Simpadd0-supporting-lemma
Supporting lemma for simpadd0.
We prove a lemma that is relied on
by the proofs generated by the transformation.
The lemma justifies the correctness of the transformation.
The lemma is proved by first proving a few local theorems;
only the lemma is exported.
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.
This is not actually needed to prove the supporting lemma,
but it provides validation.
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: simpadd0-supporting-lemma
(defthm simpadd0-supporting-lemma
(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)))))))
