Simplify definition of cce_aux

Was carrying around a counter for no reason (probably got confused by
the same name being used for an internally bound variable).
make clear a case in cce_aux can't happen, and think about good_code_env

Resigned now to the option of just saying that the output of the
compiler appears, exactly, at the specified label. Any more semantic
characterisation of a good code environment will run into infinite
regress problems, because to prove that the result of compile_code_env
is good will require assuming that the whole code env compile_code_env
produces is good.

Next step: want the code environment in the semantics (the first
argument to Cevaluate) to store the desired closure environment and the
names (and number) of the arguments. Currently it only stores the body
(and the semantics assumes that body is good for whatever closure is the
value of the operand expression). (The implementation, of course,
already keeps track of the env and argument count.)
WIP: attempt at extending semantic code env

Make it store all the information that should be in the closure
associated with the label. There is also an implementation code env, but
this currently still only stores the body (and some other information is
in ecs and env_azs). Also, start thoughts on how to use this extra info
to define good_code_env.

Trying to get the proofs to rebuild, this doesn't seem right. Probably
better to have the extra information in an extra argument to Cevaluate
rather than clobbering the stuff that depends on the way the code
environment currently works. Also might want to make it match env_azs
more closely.
Revert "WIP: attempt at extending semantic code env"

This reverts commit f644d5181095446bded4791f289f618b5a4ac38b.
Going to try putting the extra info in a different argument instead.
simplify semantic representation of non-recursive closures

rather than generate a fresh variable to be the name of such closures,
just allow them to have an empty list of names of other closures in the
bundle.
get proofs to work with tweak to closure rep

main aim was: avoid having duplicated cases for recursive and
non-recursive closures: delay the difference between them as long as
possible. (previously there was no difference at all, but we want a
small difference to avoid the dummy fresh variable.)
start adding extra argument to Cevaluate

which is the "bound variables" environment - labels mapped to the
argument list of the corresponding closure, and the list of names of
functions in the same recursive block.

proofs not updated yet.
update proofs for new argument to Cevaluate
add the position of the closure to the extra env

and write a plausible potential definition of good_code_env, that uses
bind_fv to generate the compile-time environment just like the compiler
actually does.
resume work on Call case of compile_val

with the new good_code_env in the antecedent of the theorem statement
abstract some of compile_val's statement out

as code_for_push.
preparing to also include conclusions about code_for_return.
work on definition of code_for_return

and start seeing how it affects the statement and proof of compile_val.
wondering if it's worth trying to collapse the tail and non-tail cases
(e.g. principled ways like ANF or CPS transformation, or maybe some
ad-hoc way of treating the non-tail situations as a degenerate tail
situation?)
theorem about retbc (the code that does a Return)

namely, that it pops all the let-bound variables and arguments and jumps
to the return code pointer.
prove first two cases of new compile_val

new statement has conclusions about both code_for_push and
code_for_return. when the emitted code doesn't depend on cs.tail, these
cases are basically duplicates (given retbc_thm). so these cases went
through easily. next up is one that involves using the inductive
hypotheses...
rethinking how to state compile_val

want to be able to reuse a theorem that says if code is good for push,
then the same code appended by retbc is good for return. this should
then cover all the cases where the compiler generates the same code
(i.e. knows it's not going to jump).
prove CVar case of compile_val with a tweaked statement

using a theorem that allows reuse of the result for code_for_push when
proving the code_for_return conjunct if the code is the same.
next two cases of compile_val

including a recursive case: inductive hypothesis worked ok.
up to CLet case of new compile_val

first case where the code for TCTail differs from that for TCNonTail (so
will actually be proving something new).
start tackling CCall case of new compile_val

(skipping CLet case for now, since CCall case might prompt major
restatement, but hopefully it will just go through...)
fix Cv_bv_rules for change to closure representation

this slipped through the cracks when the change (empty list for
non-recursive closures, rather than singleton fresh variable) was made