add Opapp to language subset, and work on resulting compile_val case
thoughts about compile_val opapp case, define good_code_env

good_code_env says every expression in the code environment has the
property that if it evaluates to a value in an environment that came
from a closure, and the machine looks like its been set up for a call,
then calling the pointer to that expression will eventually give the
same value.

right now, trying to get good_code_env right to be used as an
assumption. but the real difficulty will be when it comes to having to
prove it (probably only when creating closures).
more thoughts on good_code_env, and notice problems in compile_val statement

might attempt to improve the rest of compile_val briefly first
tweak compile_val statement to use compile_sz and compile_env

i.e. use the facts that those theorems prove to simplify compile_val's
statement slightly. (and cheat on opapp case, and tweak repl proof for
the addition of good_code_env, to get it all to build.)
attempt to fix compile_val statement to allow refs to change

The old statement had been provable because reference-related
expressions are still not in the language subset.

This attempt has revealed a relatively deep problem: in a stateful
language, I reckon I can't use a previous good state as proof that a
final state is good without going through all the intermediate states.
For Let expressions, then, shadowing causes a problem because the
shadowed variable disappears from the goodness invariant in some of the
intermediate states, and I don't know how to get it back when the Let
closes.

Assuming there's no way to solve that, there are at least two ways to
get rid of shadowing:
  1. make all variable names in the intermediate language distinct
  2. use an environment representation that keeps all bindings around
I'm more inclined to do 1, which could be via deBruijn indices, or just
renaming variables on conversion into the intermediate language.
prove CLet case by assuming distinct bound variables

The hope is that we can discharge these extra assumptions with a pass
over the intermediate language that renames binders. Indeed it might be
sufficient to say that such a pass is always possible, without actually
doing it.

But first, should find out if the rest of compile_val goes through with
these extra assumptions about distinct binders.
more cases of compile_val, stuck on list case

Because Cv_bv with one refs does not necessarily imply Cv_bv with
another refs. May be able to fix this by changing the statement of
compile_val in the list case: require a corresponding machine state
after every expression, rather than just at the end of the list of
expressions.
attempt at refined compile_val list case statement
attempt to prove new compile_val statement

up to list case again; not obvious it's going to work yet.
changing refs should not affect Cv_bv; start work from this insight

the only reason Cv_bv has access to the refs is so it can verify that
RefPtrs in closures point to the correct things. These RefPtrs are not
touchable by the source language, so as long as we can prove that they
don't change (although more can be added, when closures are added!)
should be able to change the refs argument to Cv_bv.

Starting to restrict the domain of the location-to-location map to the
locations actually in the store throughout, in preparation for the
required invariant about not touching those RefPtrs...
finish compile_val proof; strengthen conclusion

the new conclusion additionally says that references that aren't
mentioned by the semantic store (which should just be auxiliary closure
refs) stay the same after running the compiled code.

this statement now probably talks about references in the full required
detail. however, it has some extra hypotheses about all binders having
distinct names, which is the next thing to try to discharge...
start work again on opapp case using good_code_env

good_code_env is such a strong assumption that this is likely to go
through... but let's see.
start rethinking good_code_env, about to try another approach

Probably compile_val will need to have every case in which a compiled
expression might appear in its statement (and hence induction
hypotheses). I doubt the pieces can be uncoupled enough to allow proving
any cases (e.g. Tail vs NonTail) separately: it will have to be one big
induction.

This commit mainly pulls out some of the hypotheses in compile_val so
that they might be shared across multiple disjuncts...
Thinking about characterising bytecode solely in terms of effect

Try to define predicates on arbitrary bytecode in terms of what it
expects and what it will deliver, only referring to semantic values and
not semantic expressions. There are at least two cases: code that will
just push its value at the end, and code that will eventually call
Return. These predicates might allow for a way to state what a good code
env is without making semantics induction on what the compiler does
impossible. The compiler should just happen to produce code that
satisfies the predicates.
Merge branch 'master' into opapp

Hoping to get compiler tests to build again, because I may want to change the
compiler while working on verifying function applications.
Get compiler tests to build after merge

 - fix termination proofs (exp_size changed)
 - fix compiler test lib for new annotated source expressions
 - add NONE type annotations to all the compiler tests
get compiler/correctness to build after merge

most changes because of the extra type argument to exp, pat, v.
get all of compile/correctness to build

comment out WIP in compileCorrectnessTheory, and,
update repl_exp_val for recent changes in the compile_val theorem
(including two cheats where we need infrastructure for assuming the
input source expression has distinct bound names)
Merge branch 'opapp'

Mainly to incorporate a working snapshot of the compiler proofs and tests into
the master branch, so they can be maintained as master changes.