add infallible serialization functionality

[matty-kuhn]

this work was borne out of the discussion here: #41

the bulk of the changes actually lie in vest/src/infallible.rs, which contains the definitions for secure_serialize and serialize_infallible. all the other changes in the diff lie in the different codegen for different test files

[matty-kuhn]

as mentioned here: #help > vest serialization proof strengthening, i'm planning to narrow the scope of this, to strengthening the postconditions on serialize, instead of adding a new function/trait

[y1ca1]

Thanks for taking the time to do this! The strengthened conditions looks good to me and I agree changing the existing serializer functions would be the easiest path (so no new traits, no duplicate serializing logics, and hopefully relatively small proof changes).

[matty-kuhn]

I added some changes to rework so that instead of creating a new trait, i strengthened the post conditions on Combinator. this breaks some of the code in vest-examples, specifically the ones that have custom Combinator implementations

[y1ca1]

@matty-kuhn can you take a look at the new serializer API and let me know if that make sense to you? There's also a new API called prepare that can dynamically check for compliance and overflows if the user doesn't want to manually establish any proof obligations.
Any feedback is welcome!

[matty-kuhn]

@y1ca1 I like that API! that feels much cleaner than what I came up with, and also seems much easier to understand. I also appreciate the prepare, which I feel like would eliminate a whole class of proof work of convincing verus that your serialization will in fact succeed. The one small question I have is kind of only tangentially related, and is about the recent addition of general & mut support in verus. I think that either having these APIs use a &mut [u8], or having two different versions, one with a Vec<u8> and the other with [u8], to help with use in code that doesn't want to use vecs (and vecs can always be coerced into slices)