Verifying invariant preservation in the type-checker

[clarus]

The goal of this task is to verify that the main type-checker function, verify_instr in https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/move_sui/simulations/move_bytecode_verifier/type_safety.v , preserves the invariants on its parameters. Note that this is not the same as verifying the type-checker, but a step towards it.

• Define TypeSafetyChecker.Valid.t as a record with one field stack calling AbstractStack.Valid.t on the field of the same name.
• State a verify_instr_is_valid lemma that essentially says that if the TypeSafetyChecker.t parameter given to the function is valid, then in case it does not panic then the resulting value of type TypeSafetyChecker.t is also valid.
• Start the proof by doing a few cases. The proof should quickly start with a destruct to follow the match bytecode with of the code.
• Verify the cases which work well. For the other cases, we will need to also make lemma foobar_is_valid for all the foobar functions that are called in other tasks.