RFC: Unstable APIs

rfc/src/SUMMARY.md

@@ -9,3 +9,4 @@
 - [0001-mir-linker](rfcs/0001-mir-linker.md)
 - [0002-function-stubbing](rfcs/0002-function-stubbing.md)
 - [0003-cover-statement](rfcs/0003-cover-statement.md)
+- [0006-unstable-api](rfcs/0006-unstable-api.md)

rfc/src/rfcs/0006-unstable-api.md

@@ -0,0 +1,110 @@
+- **Feature Name:** Unstable APIs (unstable-api)
+- **RFC Tracking Issue**: <https://github.com/model-checking/kani/issues/2279>
+- **RFC PR:** <https://github.com/model-checking/kani/pull/2281>
+- **Status:** Under Review
+- **Version:** 0
+
+-------------------
+
+## Summary
+
+Provide a standard option for users to enable experimental APIs and features in Kani,
+and ensure that those APIs are off by default.
+
+## User Impact
+
+Add an opt-in model for users to try experimental APIs.
+The goal is to enable users to try features that aren't stable yet,
+which allow us to get valuable feedback during the development of new features and APIs.
+
+The opt-in model empower the users to control when some instability is acceptable,
+which makes Kani UX more consistent and safe.
+
+In order to reduce friction, we will also standardize how users opt-in to any Kani unstable feature.
+We will use similar syntax to the one used by the Rust compiler and Cargo.
+As part of this work, we will also deprecate and remove `--enable-unstable` option.
+
+Note that although Kani is still on v0, which means that everything is somewhat unstable,
+this allow us to set different bars when it comes to what kind of changes is expected,
+as well as what kind of support we will provide for a feature.
+
+## User Experience
+
+Users will have to invoke Kani with:
+```
+-Z <feature_identifier>
+```
+in order to enable any unstable feature in Kani, including unstable APIs in the Kani library.
+For unstable command line options, we will add `-Z unstable-options`, similar to the Rust compiler.
+E.g.:
+```
+-Z unstable-options --concrete-playback=print
+```
+
+Users will also be able to enable unstable features in their `Cargo.toml` in the `unstable` table
+under `kani` table. E.g:
+```toml
+[package.metadata.kani.unstable]
+unstable-options = true
+
+[workspace.metadata.kani]
+flags = { concrete-playback = true }
+unstable = { unstable-options = true }
+```
+
+In order to mark an API as unstable, we will add the following attribute to the APIs marked as unstable:
+
+```rust
+#[kani::unstable(feature="<IDENTIFIER>", issue="<TRACKING_ISSUE_NUMBER>", reason="<OPTIONAL_DESCRIPTION>")]
+pub fn unstable_api() {}
+```
+
+This is similar to the interface used by [the standard library](https://rustc-dev-guide.rust-lang.org/stability.html#unstable).
+
+If the user tries to use an unstable feature in Kani without explicitly enabling it,
+Kani will trigger an error. For unstable APIs, the error will be trigger during the crate
+compilation.
+
+## Detailed Design
+
+We will add the `-Z` option to both `kani-driver` and `kani-compiler`.
+Kani driver will pass the information to the compiler.
+
+For unstable APIs, the compiler will check if any reachable function uses a unstable feature that was not enabled.
+If that is the case, the compiler will trigger a compilation error.
+
+We will also change the compiler to only generate code for harnesses that match the harness filter.
+The filter is already passed to the compiler, but it is currently only used for stubbing.
+
+### API Stabilization
+
+Once an API has been stabilized, we will remove the `unstable` attributes from the given API.
+If the user tries to enable a feature that was already stabilized,
+Kani will print a warning stating that the feature has been stabilized.
+
+### API Removal
+
+If we decide to remove an API that is marked as unstable, we should follow a regular deprecation
+path (using `#[deprecated]` attribute), and keep the `unstable` flag + attributes, until we are
+ready to remove the feature completely.
+
+## Rational and Alternatives
+
+For this RFC, the suggestion is to only enable experimental features globally for simplicity of use and implementation.
+
+For now, we will trigger a compilation error if an unstable API is reachable from a user crate
+unless if the user opt in for the unstable feature.
+
+We could allow users to specify experimental features on a per-harness basis,
+but it could be tricky to make it clear to the user which harness may be affected by which feature.
+The extra granularity would also be painful when we decide a feature is no longer experimental,
+whether it is stabilized or removed.
+In those cases, users would have to edit each harness that enables the affected feature.
+
+## Open questions
+
+
+## Future possibilities
+
+- Delay the error due to the usage of a unstable API, and only fail at runtime if the API is reachable.
+- Allow users to enable unstable features on a per-harness base.