-
Notifications
You must be signed in to change notification settings - Fork 10
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Typestatify part 2 #132
Typestatify part 2 #132
Conversation
This is impeding the upcoming typestate-ification. When it is re-introduced later at a higher level, files removed in this commit can be reused as starting points.
This is a rather minimal version in that the API is only altered as necessary -- setting c_r is not deferred yet. Note that this already not only reduces the size of the Done initiator, but also frees it from lifetime constraints (because at that point it doesn't need to know the setup details any more).
Primarily, this changes the State structs of edhoc.rs to use type state. Unlike for the lib.rs interface in previous commits, this uses generics and a marker trait instead of standalone types, mainly because there is only little to be gained by adding and removing fields over time as they become populated or consumed. (That change can also be made later with way less refactoring impact). As a result, functions that could only return the WrongState error (eg. the edhoc_exporter function) now are infallible, and the WrongState error variant is removed. Changes to some of the functions led to minor rewrites (where State was stored in the same mutable variable for its in and out form previously, which is not possible any more here) and the Success error state could be removed from them. That state was ever only used in locally mutable errors, and never returned. The Success state was removed from the EDHOCError enum, and all other functions that relied on mutable local errors or states
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So far looking good!
r_process_message_3 and decode_plaintext_3 were redone completely based on the typestatify (and thus main) branch, just applying the logical changes from the typestatify-lowlevel branch. Some minor fixes where the automerge misstepped were fixed as indicated by the compiler.
I think this is ready for more thorough review now. |
…codes' This is mainly removing references to fallible results (removing the need for both the assertion that it's OK and the subsequent unwrap), and recreation of empty state because the typestatified (even empty) states can't be reused any more. Closes: openwsn-berkeley#114
5d6e42d
to
b780a32
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks for this PR! Left a few comments, mostly for my understanding. There are some conflicts due to the merge of #134, I will try to address them. I also ran the fstar
generation with hax
and it works normally.
Building on #128, this changes the low-level interfaces of edhoc.rs to also use typestating (albeit with a different style of typestating -- we could change it later, or I can even change to the one used with #128 in this PR still, but I think it makes sense at least initially this way, and it's easy to change later).