Description
This is a tracking issue for the experimental contracts feature compiler-team MCP #759
The feature gate for the issue is #![feature(rustc_contracts)] (external user interface).
There is also a feature gate, #![feature(rustc_contracts_internals)], which covers implementation details not intended for end-user exposure.
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
- Implement the MCP; initial implementation #[contracts::requires(...)] + #[contracts::ensures(...)] #128045
- Add interface for external tools to retrieve the contract specification.
- Add type invariant.
- Adjust documentation (see instructions on rustc-dev-guide)
- Formatting for new syntax has been added to the Style Guide (nightly-style-procedure)
- Stabilization PR (see instructions on rustc-dev-guide)
Unresolved Questions
- Tooling support: How much functionality should be integrated into Rust project provided tooling itself? E.g. should something like miri be exploring fuzzing of data that is fed into functional preconditions as a way to explore state space?
- Syntax bikesheds galore: Define the exact syntax for contract attributes. Should we separate correctness vs safety conditions?
- Static vs dynamic semantics: The idealized contract system would allow contracts to inform both static verification and dynamic validation tools. What's the best way to handle conditions that cannot be checked with both semantics.
- 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. This cannot be expressed as a mere safety::requires form as envisioned above. Should we add something like:
#[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? See original MCP for more details - 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)?
- Panic: How should a panicking expression within a contract be treated? Should users be able to specify conditions that will lead to panic? Should any post-condition be checked during unwind?