Verification for codecs and generated code

[mario-bucev]

This PR includes (for the Scala backend only):

• Invertibility proofs for BitStream
• Invertibility for Codec and ACN for the functions used by the PUS-C services (except floating-point and string-related)
• while loops are transformed to recursive top-level functions
• Hoisting of ACN-specialized code into top-level functions, with the ACN dependencies being parameterized
• Precise bitindex calculation (for contracts and proofs)
• SEQUENCE ... OF and strings are now backed by a Vector and not an Array
• Invertibility proofs for SEQUENCE when the -invertibility option is specified