Skip to content

add infallible serialization functionality#43

Draft
matty-kuhn wants to merge 2 commits into
secure-foundations:mainfrom
matty-kuhn:infallible-serialization
Draft

add infallible serialization functionality#43
matty-kuhn wants to merge 2 commits into
secure-foundations:mainfrom
matty-kuhn:infallible-serialization

Conversation

@matty-kuhn
Copy link
Copy Markdown

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
Copy link
Copy Markdown
Author

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
Copy link
Copy Markdown
Collaborator

y1ca1 commented Apr 14, 2026

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
Copy link
Copy Markdown
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants