WIP: start on new statement of compile_val

to account for exceptions. cheat on all the cases in the proof where it
comes up, for now, and try to get the other parts of the original proof
working with the new statement.

might want to tweak the statement more, though, to make the proof avoid
early case splits.
rework compile_val statement, and prove CRaise cases

hoping the new statement will make other cases more straightforward to
structure too... might also want to (re)move the case-split in the
compiler's definition for compiling CIf.
make compiler avoid case split on CIf case

it was emitting slightly different code based on whether in tail
position or non-tail position, but the non-tail position code works for
both: it just generates an extra irrelevant (since the tail code will
return before it gets there) jump and label. this should hopefully make
the proof shorter.
fix bug in compilation of CHandle, add test for it

need to account for the extra code pointer and stack pointer on the
stack when calculating variable offsets.
work on CHandle case of compile_val theorem
work on CHandle case of compile_val

done the code_for_push part, but might need to tweak the statement to be
able to use code_for_push_return to get the other part for free.
tweak statement of compile_val, prove first CHandle case

without having to reprove cases that should be simple consequences of
other cases. next up is the CHandle case that actually invokes the
handler.
WIP: second CHandle case
more CHandle case, but wanting to change statement

it seems too unwieldy, or maybe impossible, to use code_for_push_return
after the code and the call_context are already fixed... the statement
of the theorem needs to universally quantify over these things later so
the quantifier appears in the inductive hypothesis.
start working on tweaked statement for compile_val
possible bugfix of compilation of Handle

The issue is how to compile a handle expression in tail position.

If no exception is raised, we need to jump to the return pointer of the
last called function.

If an exception is raised, we need to jump to the handler code, and then
it needs to (eventually) jump to the return pointer. (Or raise another
exception or whatever...)

Previously, in the non-exception case, I was jumping to the return
pointer _after_ jumping over the handler code. But that means in the
exception case, when the handler code finishes (and jumps correctly)
there is some leftover junk code after it implementing the original
expression's return. I don't know if this can show up as bad behaviour,
but it at least doesn't get along with the way the proof works (which
assumes the machine runs to the end of the code for an expression).

Now the original expression's return is before the handler code starts,
which seems much more sensible.
WIP: still working on the raise/handle cases of compile_val
reprove first CHandle case, for the new implementation and statement

unfortunately I can't see how to avoid proving the tail and non-tail
cases of this sub-case separately, since the proofs aren't identical
(though they're somewhat similar).
another statement tweak
work on second CHandle case, done all but the re-raise case
finish CHandle cases

So now we have a statement of the theorem that is probably adequate for
exceptions, since all the raise and handle cases are proved. Hopefully
the proofs for the other cases will work with the new statement too.
up to end of CCon cases
up to first CLet case
finish CLet cases, up to CLetrec
tweak statement of compile_val yet again, and fix partial proof

we need the conclusion to be about all of the code in the bytecode
state, not just the prefix after compilation, because previously
compiled closures might be in the later part of the code and they are
needed in the inductive hypothesis.