Tracking Issue for Contracts

[pnkfelix]

This is a tracking issue for the MCP "Contracts" (rust-lang/compiler-team#759).
The feature gate for the issue is #![feature(contracts)].

Current (2025-03-20) design doc: https://hackmd.io/@celinaval/B1UEl3tUyl

Liaison: @Nadrieril (appointed here)

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

• Approve as lang experiment.
  • #[contracts::requires(...)] + #[contracts::ensures(...)] #128045 (comment)
• Implement the MCP (cc @rust-lang/compiler). Initial implementation: #[contracts::requires(...)] + #[contracts::ensures(...)] #128045
• Add interface for external tools to retrieve the contract specification.
• Add type invariant.
• Improve error message (include #[track_caller])
• Adjust documentation (see instructions on rustc-dev-guide)
• 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?

Implementation history

Compiler support

• #[contracts::requires(...)] + #[contracts::ensures(...)] #128045

Standard library usage

• Add contracts for all functions in Alignment #136578

[traviscross]

@rustbot labels +T-lang

[traviscross]

We've approved this as as lang experiment:

• #[contracts::requires(...)] + #[contracts::ensures(...)] #128045 (comment)

@nikomatsakis is serving as the liaison.