# Experimental Contract Attributes

The [MCP-759](https://github.com/rust-lang/compiler-team/issues/759) proposed the addition of experimental unstable attributes for behaviorial specification, and intrinsics for enabling better tools to validate and verify those specifications.

The goal is to eventually enable Rust, as a language, to allow users to write specifications in formal code-like language. More details can be found in the [MCP-759](https://github.com/rust-lang/compiler-team/issues/759).

## Initial Implementation

In the [PR #128045](https://github.com/rust-lang/rust/pull/128045), we are introducing a simple form of `#[contracts::requires]` and `#[contracts::ensures]`, while [PR #138374](https://github.com/rust-lang/rust/pull/138374) adds support for contract in constant functions.

While `requires` expects a side-effect free boolean expression, the `ensures` expects a side-effect free closure definition that takes the reference to the function return value.

For example, a developer could annotate `NonNull` methods with the following safety contracts:

#![feature(contracts)]
extern crate core;
use core::contracts;

impl<T: ?Sized> NonNull<T> {
    #[contracts::requires(!ptr.is_null())]
    pub const unsafe fn new_unchecked(ptr: *mut T) -> Self {
        // SAFETY: the caller must guarantee that `ptr` is non-null.
        unsafe {
            NonNull { pointer: ptr as _ }
        }
    }

    #[contracts::ensures(|new_ptr| !new_ptr.is_null())]
    pub const fn as_ptr(self) -> *mut T {
        self.pointer as *mut T
    }
}

A user can optionally turn the contract into runtime checks executed before and after the function annotated with contract has been called.

Additionally, other verification tools can be used in order to check the annotated contracts.

### Compilation Stages

In order to turn the contract annotations into runtime checks, we have implemented the following changes.

1. **Built-in Macro**: The `requires` and `ensures` were implemented as builtin macros that expands the function signature by adding a `rustc_contracts_requires` and `rustc_contracts_ensures` clauses respectively, both containing a closure definition.
The `NonNull` methods signature from the example above would be expanded to the following in this stage:

    pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
        rustc_contract_requires(|| !ptr.is_null())
    { /* body */ }

    pub const fn as_ptr(self) -> *mut T
        rustc_contract_ensures(|new_ptr| !new_ptr.is_null())
    { /* body */ }

2. **AST Extension**: The parser was extended to accept optional `rustc_contracts_requires` and `rustc_contracts_ensures` clauses, and store them as part of the function AST node.
This change to the syntax is perma-unstable. It can be enabled via `rustc_contracts_internals` unstable feature.
3. **AST Lowering**:
a. **Contract closures**: During body lowering, the contract clauses lowered to become closures in the function prelude. For the `ensures` closure, the compile will inject a call to `build_check_ensures` with the `ensures` closure to help with type inference.
b. **Requires check**: Also in the function prelude, the compiler will inject a call to the new intrinsic `contract_check_requires` to check the `requires` closure.
b. **Ensures check**: The compiler will insert a call to `contract_check_ensures` intrinsics at every function return point, as well as at the end of the function.

The `NonNull` examples above will look like[^hir] the following after all these stages:

    const unsafe fn new_unchecked(ptr: *mut T) -> Self {
        contract_check_requires(|| !ptr.is_null());
        {
            // SAFETY: the caller must guarantee that `ptr` is non-null.
            unsafe { NonNull{ pointer: ptr as _,} }
        }
    }

    const fn as_ptr(self) -> *mut T {
        let __ensures_checker = contract_build_check_ensures(|new_ptr| !new_ptr.is_null());
        contract_check_ensures({ self.pointer as *mut T }, __ensures_checker)
    }

[^hir]: The code below was extracted with `-Zunpretty=hir` and edited for clarity.

### Feature gates

We have added two feature gates to contracts:

1. `rustc_contracts`: Enables the usage of contract attributes.
2. `rustc_contracts_internal`: Perma-unstable attribute that enables the explicit usage of the extended signature with contract clauses.

We have also added a new configuration: `contract_checks` to enable the usage of `#[cfg(contract_checks)` to check if contract checks are enabled.

### Command arguments

We have added a new unstable argument `-Zcontract-checks=[yes|no]` that allows users to enable / disable the runtime checks. The behavior of this feature is similar to `-Zub_checks`.

### New Intrinsics

We are introducing 3 new intrinsics in this PR.

1. `contract_checks`: Returns whether contract's runtime checks have been enabled.
2. `contract_check_requires` / `contract_check_ensures` : Invoke the contract closure to check whether the specification holds.

## Limitations

### Contract Order of Evaluation

TODO: Document the current limitation that ensures clauses are evaluated before dropping arguments. See [this zulip thread](https://rust-lang.zulipchat.com/#narrow/channel/544080-t-lang.2Fcontracts/topic/Order.20of.20evaluation.20between.20ensures.20and.20dropping.20parameters).

### Lack of API for querying contracts

TODO: Talk about verification and analysis tools integration. Contracts are embedded into a function body early on, which doesn't allow tools to easily analyze contracts.

### Built-in Macro

The current implementation of the contracts built-in macros is rather fragile. We couldn't implement a more robust solution with the existing macro infrastructure.

The contract macros differ from all the existing attributes like built-in macros.
The input for contracts macro is an arbitrary expression, while existing macros accept a restricted AST as an input (`MetaItem`).

:::spoiler Expand this for more background on existing implementation.

There are two different ways to define attribute macros in the Rust compiler today:
1. `Attr`: A token-based attribute macro. It takes two `TokenStream` as input, the annotated item, and the content of the attribute. It should produce a new `TokenStream` for the item.
2. `LegacyAttr`: An AST-based attribute macro. It takes a `MetaItem` and an `Annotable` item as input representing the content of the attribute and the annotated item. Note that `MetaItem` is restricted It produces one or more `Annotable` as a result.
All the attributes like built-in macros defined in the Rust compiler today implement the this variant.

However, for contracts, the input for the macro is an arbitrary expression. Thus, we had to use the `Attr` trait.

/// A syntax extension kind.
pub enum SyntaxExtensionKind {
    /// A token-based attribute macro.
    Attr(
        /// An expander with signature (TokenStream, TokenStream) -> TokenStream.
        /// The first TokenStream is the attribute itself, the second is the annotated item.
        /// The produced TokenStream replaces the input TokenStream.
        Box<dyn AttrProcMacro + sync::DynSync + sync::DynSend>,
    ),

    /// An AST-based attribute macro.
    LegacyAttr(
        /// An expander with signature (AST, AST) -> AST.
        /// The first AST fragment is the attribute itself, the second is the annotated item.
        /// The produced AST fragment replaces the input AST fragment.
        Box<dyn MultiItemModifier + sync::DynSync + sync::DynSend>,
    ),
    
    /* .. */
}

/// Trait used by the `Attr` variant.
pub trait AttrProcMacro {
    fn expand<'cx>(
        &self,
        ecx: &'cx mut ExtCtxt<'_>,
        span: Span,
        annotation: TokenStream,
        annotated: TokenStream,
    ) -> Result<TokenStream, ErrorGuaranteed>;
}

/// Trait used by the `LegacyAttr` variant.
pub trait MultiItemModifier {
    /// `meta_item` is the attribute, and `item` is the item being modified.
    fn expand(
        &self,
        ecx: &mut ExtCtxt<'_>,
        span: Span,
        meta_item: &ast::MetaItem,
        item: Annotatable,
        is_derive_const: bool,
    ) -> ExpandResult<Vec<Annotatable>, Annotatable>;
}

:::

We couldn't leverage the `Parser` either. We were able to use the `Parser` to retrieve the annotated item, and inject the contract expression in the item, however, there is no easy way to convert the modified AST item back to `TokenStream`. Calls to `TokenStream::from_ast` would result in the original `TokenStream`, and the contract clauses would be lost.

Ideally we should extend the attribute expander to support a TokenStream annotation atop an AST annotated item, so that it would again be trivial to inject the attribute payload into an unambiguous spot in the AST.

Another possibility was proposed [here](https://github.com/rust-lang/rust/issues/146808#issuecomment-3418389466), which would be to directly integrate with syn / quote.

### AST Lowering

When writing a contract, users should be able to omit the type annotation on the ensures clause. I.e.:

#[core::contracts::ensures(let old_val = val; |ret| ret.is_none_or(|x| x > old_val))]
fn increment(val: isize) -> Option<isize> {
    val.checked_add(1)
}

instead of:

#[core::contracts::ensures(let old_val = val; |ret: &Option<isize>| ret.is_none_or(|x| x > old_val))]
fn increment(val: isize) -> Option<isize> {
    val.checked_add(1)
}

For that, rustc should lower the following code to:

fn increment(val: isize) -> Option<isize> {
    let __ens_checker : Fn(&Option<isize)) -> bool = {
        let old_val = val;
        |ret| ret.is_none_or(|x| x > old_val)
    };
    core::intrinsics::contract_check_ensures(__ens_checker, { val.checked_add(1) })
}

The existing lowering logic makes it rather hard to add the explicit type annotation, while the function call is fairly straight forward. Thus, rustc adds a call to an identity function named `build_check_ensures` for now:

fn increment(val: isize) -> Option<isize> {
    let __ens_checker = core::contracts::build_check_ensures ({
        let old_val = val;
        |ret| ret.is_none_or(|x| x > old_val)
    });
    core::intrinsics::contract_check_ensures(__ens_checker, { val.checked_add(1) })
}

### Target Functions

In this initial implementation, contracts can only be attached to functions that have a body, excluding foreign functions, many intrinsics and trait declarations.

We would likely to eventually remove that restriction, but it will require redesigning the contract instrumentation. We would also need to decide how to encode the contract check. We could for example add the instrumentation in the callee body.

## Contracts Re-architecture

The current contract implementation was designed as a temporary solution to unblock early experimentation and validation. While functional, it presents several architectural limitations documented in previous sections, making it unsuitable for long-term stabilization.

We believe a better solution would be to introduce dedicated HIR elements for contract components, similar to the existing closure
implementation. Contract instrumentation would be implemented as a dedicated MIR instrumentation pass that runs only when contracts are enabled.

The exact implementation details is still not entirely clear, and feedback would be extremely valuable at this point. One possibility would be to generate a separate HIR element that reflects the function signature, and contains the contract logic. For example:

fn func_with_contract(args: FnArgs) {
   pre_cond(&args);                          // This could capture argument values
   let ret_val = original_fn(/*move*/ args); // Drop occurs before post-cond
   post_cond(&ret_val);
   ret_val
}

The MIR transformation would either rewrite the body of the original function, or re-route usages of the original function to the one with contracts. Re-routing would be suitable for functions without bodies, such as external functions, and intrinsics. Replacing function bodies would be more friendly for things like trait implementations.

While we theoretically don't need to generate actual functions as HIR elements, and the MIR pass could be responsible for assembling it. This approach may be necessary to ensure proper contract type checking and borrow checking integration. Using dedicated elements would provide consistency with existing language constructs in the HIR, and ensure zero runtime overhead for builds without contracts.

## Future work

1. Add interface for external tools to retrieve the contract specification.
2. Split correctness / safety contracts (per [all-hands discussion](https://hackmd.io/@qnR1-HVLRx-dekU5dvtvkw/SyUuR6SZgx#Spec))
3. Improve the existing architecture.
4. Annotate the standard library with contracts.
a. Relationship between `ub_checks` and `contracts`.
4. Add support for type invariant.
5. Add more tests + improve implementation.
6. Improve error handling and diagnostic messages.
7. Potential changes to the contract annotation syntax:
a. Safety vs correctness vs panic freedom
b. Contract stability

## Questions

*Please feel free to add any questions you might have*