# 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

### 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.

### 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.

## Alternative Solutions

Initially, we tried to make contract a new hir element, such as a `closure`, but that required changes to every stage of IR lowering, and we couldn't get a working solution in a reasonable timeline for start early experimentation.

That said, the existing solution is not the one that we are planning to stabilize, and we are currently exploring a more robust solution that would replace the contract AST lowering. One possibility would be to replace the contract instrumentation with a MIR pass.

## Future work

1. Add interface for external tools to retrieve the contract specification.
2. Improve the existing architecture.
3. 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*