RFC Function Contracts

[JustusAdam]

Rendered

Proposes the addition of function contracts and mechanisms to check them and use them as modular abstractions.

[celinval]

I like this structure much better! Thanks.

I haven't finished reviewing it yet. I'll keep looking at it later today.

I do have two things I would like to discuss:

1. Our previous contract implementation uses #[kani::modifies] instead of assigns. I like that better.
2. I think it should be up to the user to verify their contracts. We shouldn't enforce it inside Kani, especially for contracts defined in a dependency.

[celinval]

Please don't forget to change the summary.md file

[adpaco-aws]

The "User Experience" section is structured in a way that makes it a little hard-to-follow. It seems to me that you're trying to tackle three problems at once: specification, checking and replacement. Maybe each could have their own subsection instead of being itemized?
There's a similar issue with "Rationale and alternatives" and "Future possibilities", although I haven't carefully read them yet.

[adpaco-aws]

Thanks @JustusAdam , it's looking great! Only a couple technical comments, the rest are more related to writing.

[celinval]

Almost there. :)

[celinval]

BTW, please wait for a second approval before merging. Thanks!

[adpaco-aws]

Thanks @JustusAdam ! Please take care of unresolved comments before merging.

[JustusAdam]

BTW, please wait for a second approval before merging. Thanks!

I'm going to wait for @remi-delmas-3000 to give it another look because there are some unresolved comments before merging.