Repository: rust
Issue: Tracking Issue for Contracts
Labels: T-lang,T-compiler,C-tracking-issue,F-rustc_contracts

This is a tracking issue for the MCP "Contracts" (https://github.com/rust-lang/compiler-team/issues/759).
The feature gate for the issue is `#![feature(rustc_contracts)]`.

### About tracking issues

Tracking issues are used to record the overall progress of implementation.
They are also used as hubs connecting to other relevant issues, e.g., bugs or open design questions.
A tracking issue is however *not* meant for large scale discussion, questions, or bug reports about a feature.
Instead, open a dedicated issue for the specific matter and add the relevant feature gate label.
Discussion comments will get marked as off-topic or deleted.
Repeated discussions on the tracking issue may lead to the tracking issue getting locked.

### Steps
<!--
Include each step required to complete the feature. Typically this is a PR
implementing a feature, followed by a PR that stabilises the feature. However
for larger features an implementation could be broken up into multiple PRs.
-->

- [ ] Implement the MCP (cc @rust-lang/compiler)
- [ ] Adjust documentation ([see instructions on rustc-dev-guide][doc-guide])
- [ ] Formatting for new syntax has been added to the [Style Guide] ([nightly-style-procedure])
- [ ] Stabilization PR ([see instructions on rustc-dev-guide][stabilization-guide])

[stabilization-guide]: https://rustc-dev-guide.rust-lang.org/stabilization_guide.html#stabilization-pr
[doc-guide]: https://rustc-dev-guide.rust-lang.org/stabilization_guide.html#documentation-prs
[nightly-style-procedure]: https://github.com/rust-lang/style-team/blob/master/nightly-style-procedure.md 
[Style Guide]: https://github.com/rust-lang/rust/tree/master/src/doc/style-guide

### Unresolved Questions
<!--
Include any open questions that need to be answered before the feature can be
stabilised.
-->



Syntax bikesheds galore: I am not thrilled by the prospect of writing #[rustc_contracts::requires(for safety: ...)] all over the place.
For example, an earlier draft of this MCP had used #[safety::requires(...)], which I find far more palatable, but may pose serious hazards for compatibility with existing code bases.
I am leaving identification of "a good syntax" as an open problem.

Static vs dynamic semantics: My idealized contract system would allow contracts to inform both static verification and dynamic validation tools. Some contracts like forall! do not have an "obviously right" dynamic interpretation.

Safety post-obligations: The safety criteria for some unsafe methods is stated as a constraint on how the caller uses the return value from a method.
For example: str::as_bytes_mut says "The caller must ensure that the content of the slice is valid UTF-8 before the borrow ends and the underlying str is used."
This cannot be expressed as a mere safety::requires form as envisioned above.
(My best guess is that such contracts require a richer structure, such as an entiretly hypothetical #[safety::at_lifetime_end(|output| str::from_utf8(output).is_ok())], which could only be checked in the future, right before the &mut u8 borrow expires and the reference is again capable of being treated as a &mut str.)

Correctness invariants: As mentioned above, there is probably utility in being able to attach invariants to a type that are used for proving functional correctness. But it is not as clear where to establish the points where correctness invariants must be checked. It may make more sense here to use something like refinement types, where explicit method calls (potentially in ghost code) would (re)establish such invariants.

Purity: Do contracts need to be pure (i.e. have no non-local side-effects)? Some verification tools will require this.

Panic: How should a panicking expression within a contract be treated? Some of the above code was written with slice's get method rather than the index operator, in order to sidestep this question. But rather than disallowing panic entirely (i.e. treating it as a improperly written contract), it might be more natural to interpret a panic within a contract expression as a contract failure.
### Implementation history

<!--
Include a list of all the PRs that were involved in implementing the feature.
-->