Add conditions for generic compress and serialize functions

[mamonet]

This PR makes generic serialize.rs panic-free by adding the following changes

• Add pre/post conditions for functions in generic serialize.rs and make sure they pass the verification (Keep functions of lower priority marked as lax - compress_then_serialize_5/compress_then_serialize_11)
• Add conditions for compress functions in the following vector modules traits.rs/portable.rs/avx2.rs
• Add conditions with proofs for high-level compress functions in vector/portable/compress.rs (no avx2 proofs are added yet)

[mamonet]

I invested a fair amount of time trying to address the slow verification of functions in serialize module. Here is my observation, at some point of verifying stacked operations F* gets overwhelmed and starts to fail to resolve basic arithmetics and the process could take several minutes and may lead to endless loop of reasoning. To make sure a certain function is under threshold and has normal verification process, we have to determine the operations that SMT struggles with the most, such as nested loops or complex arithmetics, and make them opaque by using opaque_to_smt qualifier and revealing where needed. By using that feature, verifying Serialize module is done in seconds rather than a few minutes for each function. I think we should use that qualifier intensively as the proofs scale to make the verification process maintainable and to have a headroom for further modifications as the conditions are still volatile in the current state.