work on new compile_val

new statement keeps the location map (sm) constant for simplicity, since
it will only need to change when closures are created and expressions
doing so are currently excluded.

up to CCon case
finish CCon case of compile_val

We now need to track a good state down all the sub-expressions as they
are evaluated, and then get a further good state when their values are
combined, because the store might change at every step.

Previously, we just used the good state at the beginning as a basis to
conclude that the final state (with one extra thing on the stack) is
good. That shortcut doesn't work any more, unfortunately.
finish CLet case of compile_val

As it turns out, propagating a good Cenv_bs correspondence down each
step of evaluation is not as necessary as the last commit message would
suggest, since it is possible to change the store argument of Cenv_bs
arbitrarily as long as you can prove that the store correspondence
(s_refs) holds. See the new theorem Cenv_bs_change_store, a trivial
consequence of Cenv_bs_def.

Propagating the invariant properly would be very difficult in the CLet
case, so this is lucky.
start Prim2 case of compile_val; prove lemma: Cevaluate_Clocs

since the correctness theorem for the compilation of prim2s now requires
the semantic-location-to-machine-location map to have all the requisite
locations in its domain, we need to prove that Cevaluate preserves the
property of all values (in the store and environment) being "closed"
under the store's domain.
finish Cprim2 case of new compile_val
CIf case of new compile_val
finish compile_val (and compileCorrectnessTheory)