External function calls, what to do?

[ehildenb]

Right now the set_free_balance calls these external functions:

• $ext_blake2_256
• $ext_clear_storage
• $ext_set_storage
• $ext_twox_128

We have two options for dealing with this:

• Make abstract "loose" K specs of these functions behavior, in terms of the expected overall change in the state. Works well for functions which take input and give back some well-structured output (eg. $ext_blake2_256). Specs are "loose" because we cannot verify them over the existing code. Might not work in all cases.
• Compile said functions to Wasm and actually try to build a specification for them. Depending on their size, this can be very time consuming.

Either way, it might be helpful to have the Wasm implementations of these functions available. But if in reality people use the non-Wasm implementations, this doesn't add any security to have specifications of these functions.

[Demi-Marie]

@ehildenb I think the first approach is better, at least in this case. The second approach will not be practical, as it would involve verifying all of RocksDB. I would love to do that, but that is far beyond the scope of this project.