Verify flattening of the abstract stack

[clarus]

The type-checker uses an AbstractStack.t that is a stack of types instead of a stack of values as used in the interpreter. It is implemented by grouping the same types with a counter:

Module AbstractStack.
  Record t (A : Set) : Set := {
    values : list (Z * A);
    len : Z;
  }.

The goal of this task is to show that for the primitive operations, such as pop and push, it behaves as a stack of type list A where we do not group the elements.

The proofs to complete are in the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/move_sui/proofs/move_abstract_stack/lib.v and marked as Admitted:

• flatten_push_n
• flatten_pop_eq_n
• flatten_pop_any_n