bit more work on stating/proving compile_call_val