diff --git a/CLAUDE.md b/CLAUDE.md new file mode 100644 index 00000000000..88f5bf67283 --- /dev/null +++ b/CLAUDE.md @@ -0,0 +1,81 @@ +# CLAUDE.md + +This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository. + +## Repository Overview + +This is the Rust RFC (Request for Comments) repository. RFCs are design proposals for substantial changes to Rust, Cargo, Crates.io, or the RFC process itself. + +## Current Work Context + +The current focus is on **RFC 0000-extern-impl** (`text/0000-extern-impl.md`), which proposes relaxing the orphan rule while maintaining coherence through "impl dependencies." + +### Key RFC Concept + +The extern impl RFC addresses a fundamental constraint in Rust: the orphan rule requires that trait implementations be in the same crate as either the trait or type. This RFC proposes allowing crates to have "impl dependencies" where they can implement traits/types from dependencies as if they were local, while maintaining coherence through distributed checking. + +### Active Work + +**Formal Specification Plan**: See `extern-impl-formal-spec-plan.md` for the comprehensive plan to improve the RFC's formal specification. This includes: + +1. **Tool selection**: Research concluded that **Forge** (modern Alloy variant) or **Alloy 6** are the best tools for modeling the structural graph properties +2. **Outstanding work phases**: + - Define precise terminology (especially graph-theoretic terms like "immediate dominator") + - Enumerate all coherence invariants (coherence, acyclicity, visibility, checker responsibility, etc.) + - Analyze how generics and associated types interact with the system + - Add performance/complexity analysis + - Review restrictions (e.g., the prohibition on re-exported definitions may be too conservative) + - Build a complete formal specification in Alloy/Forge + +3. **Key invariant**: Each binary is an independent coherence root. Multiple binaries need not be coherent with each other. + +### Current Alloy Spec Issues + +The existing Alloy specification in the RFC (Appendix) is incomplete and has several problems: +- Doesn't model impl-deps as distinct from regular deps +- Doesn't formalize "checker responsibility" +- Contains a tautology in the `dep_coherent_impl_crates` check +- Has a TODO for the most critical constraint + +## RFC File Structure + +- `text/` - Contains all accepted and proposed RFCs +- `text/0000-extern-impl.md` - The extern impl RFC being worked on +- `0000-template.md` - Template for new RFCs +- `README.md` - RFC process documentation + +## Working with RFCs + +RFCs follow a specific structure defined in `0000-template.md`: +- Summary +- Motivation +- Guide-level explanation +- Reference-level explanation +- Drawbacks +- Rationale and alternatives +- Prior art +- Unresolved questions +- Future possibilities + +## Git Workflow + +Current branch: `extern-impl` + +This is a working branch for the extern impl RFC. The RFC is still in draft/revision phase. + +## Next Steps + +Based on the formal specification plan, the immediate next steps are: + +1. Define precise terminology and graph-theoretic concepts +2. Enumerate and formalize all coherence invariants +3. Decide between Forge (modern, better UX) vs Alloy 6 (more established) for the formal spec +4. Build out the formal specification incrementally + +## Key Concepts to Understand + +- **Orphan rule**: Current requirement that trait impls must be in the same crate as the trait or type +- **Coherence**: The property that there's at most one impl of a trait for a given type +- **Impl dependency**: The proposed new dependency type where a crate can implement traits/types from dependencies +- **Checker responsibility**: Which crate is responsible for verifying coherence between multiple implementing crates +- **Binary root**: Each binary crate is the root of its own coherence domain diff --git a/extern-impl-formal-spec-plan.md b/extern-impl-formal-spec-plan.md new file mode 100644 index 00000000000..c77f221c19f --- /dev/null +++ b/extern-impl-formal-spec-plan.md @@ -0,0 +1,328 @@ +# Extern Impl Formal Specification Plan + +This document outlines the plan for improving the formal specification of the extern impl RFC (0000-extern-impl.md). + +## Todo List + +- [x] Research current state of formal verification tools and tooling +- [ ] Define terminology and graph-theoretic concepts +- [ ] Enumerate and formalize all coherence invariants +- [ ] Analyze generic type parameters and associated types +- [ ] Analyze supertraits and their interaction with impl deps +- [ ] Analyze intrinsic methods (impl blocks without traits) +- [ ] Add performance and complexity analysis section +- [ ] Review and revise other spec restrictions +- [ ] Design and implement new formal specification +- [ ] Write separate Cargo RFC for impl dependency representation + +## Proposed Plan + +### Phase 1: Foundations (can be done in parallel) + +**1a. Terminology audit** +- Review current terms: "defining crate", "implementing crate", "impl deps", "adoption", "view" +- Consider alternatives: "providing crate" vs "defining", "extending crate" vs "implementing" +- Graph theory: "least common dominator" vs "lowest common ancestor" vs "convergence point" +- Consider borrowing from module systems literature (ML, Scala implicits) + +**1b. Tool research** ✓ COMPLETED +- Survey formal methods tools with specific criteria: + - Good at modeling graph structures with constraints + - Can express reachability/dominance properties + - Has counter-example generation + - Reasonably mature tooling +- Create comparison matrix: Alloy vs TLA+ vs Lean vs Dafny vs others + +### Phase 2: Formalization (sequential, builds on Phase 1) + +**2a. Complete invariant catalog** +Core invariants to formalize: +1. **Coherence**: `∀(trait, type). |implementations| ≤ 1` +2. **Acyclic deps**: `∀c. c ∉ transitive_deps(c)` +3. **Visibility**: `impl(A, trait, type) ⟹ trait ∈ visible(A) ∧ type ∈ visible(A)` +4. **Orphan extension**: Define precisely when an impl is "local enough" +5. **Check responsibility**: Every impl-pair has exactly one checker +6. **Check completeness**: Checker can see all relevant impls +7. **Binary root**: Each binary is the coherence root; multiple independent binaries need not be coherent with each other + +**2b. Graph-theoretic formalization** +- Define "checker responsibility" precisely +- Is it the immediate dominator? The least common ancestor in the dep tree? +- Formalize: "crate C must check impls I₁, I₂ iff C is the closest crate where both are visible through distinct direct deps" + +### Phase 3: Generics, Associated Types, and Edge Cases (separate deep dive) + +This deserves its own analysis because of several complex interactions. + +**3a. Generics and Associated Types** + +These add complexity because: +- Blanket impls create universal quantification +- Associated types add type-level functions +- Specialization (if/when stabilized) adds partial ordering + +**Key questions:** +1. Does "defining crate" for `impl Trait for Vec` mean the crate defining `Trait`, `Vec`, or the impl itself? +2. Do overlap rules change? (I suspect not, but needs proof) +3. How do associated type constraints interact with visibility? + +**3b. Supertraits** + +Supertraits create implicit dependencies between trait implementations. + +**Key questions:** +1. If `trait A: B` and a type T has `impl A` in crate X and `impl B` in crate Y, does this create coherence issues? +2. Does the existing orphan rule already handle this? (Likely yes, but needs verification) +3. With impl deps: can crate X implement A for T if it has an impl dep on the crate defining A, but T's impl of B is elsewhere? +4. Are there any new coherence concerns when supertrait impls are spread across crates? +5. Does the checker responsibility algorithm need to account for supertrait relationships? + +**Hypothesis**: Supertraits are probably already covered by the existing overlap checking rules, since the type system requires `impl A for T` to prove `T: B` exists. But this needs formal verification. + +**3c. Intrinsic Methods (impl blocks without traits)** + +The current proposal focuses on trait implementations. A natural extension is intrinsic methods. + +**Current Rust**: Multiple `impl Type` blocks are allowed in the same crate, spreading methods across different modules/files. + +**Proposed extension**: Allow `impl Type` blocks across multiple impl crates. + +**Key questions:** +1. How much additional complexity does this add to the proposal? +2. Coherence is simpler (no overlap checking needed between intrinsic methods) +3. But visibility becomes more complex: which methods are visible where? +4. Do we need a "defining crate" concept for intrinsic impls? +5. How does this interact with privacy/visibility rules? +6. Does allowing intrinsic impls in impl-dep crates create security/encapsulation concerns? +7. Should this be in the initial proposal or deferred to future work? + +**Consideration**: The RFC mentions this as a future possibility. It may significantly complicate the Cargo story (how to declare which crate provides which methods?) and the coherence checking story (though simpler than traits). + +**Approach**: Start with simplified model (no generics, no supertraits, no intrinsic methods), then add each dimension incrementally + +### Phase 4: Implementation Concerns (can be parallel with Phase 3) + +**4a. Performance analysis** +- Best case: O(n) linear scan when no impl deps +- Worst case: Could be O(n²) if every crate must check every pair? +- Space: Need to track impl deps in metadata +- Incremental compilation: Which caches invalidate? + +**4b. Restrictions review** +Your specific question about re-exports: +- Current: "You may only implement for types/traits actually defined in my_definitions itself. Re-exports don't count." +- Why this restriction? Probably to avoid ambiguity about which crate is "defining" +- Could lift it if we track def-site precisely in metadata +- Risk: re-export chains could make reasoning harder + +### Phase 5: New Formal Spec (depends on 1b, 2a, 2b) + +**Recommended approach:** +1. **Start with Forge or Alloy 6** for structural properties and counter-example finding +2. **Use Lean 4 or Dafny** for proving the invariants hold (future work) + +**Structure:** +- Module 1: Basic definitions (crates, deps, traits, types, impls) +- Module 2: Visibility and reachability +- Module 3: Original orphan rule (baseline) +- Module 4: Extended orphan rule with impl deps +- Module 5: Checking responsibility assignment +- Module 6: Proof that assigned checks ensure coherence + +### Phase 6: Cargo RFC (separate RFC, depends on Phase 2 and Phase 5) + +This will require a separate RFC submission to define how Cargo represents impl dependencies. **This is likely quite complex and deserves significant design work.** + +**Fundamental architectural challenge: Package vs Crate dependencies** + +Currently, Cargo's dependency model is based on **packages**, while impl deps are fundamentally **crate-level** relationships. Key issues: + +- **One library per package**: Cargo currently allows only one library crate per package (plus build scripts, tests, binaries) +- **Multiple libraries per package**: We likely want to extend Cargo to allow multiple library crates per package with "friend" relationships (impl deps between them) +- **Package-level deps → crate-level deps**: Need to reconcile Cargo's package dependency resolution with rustc's crate-level impl dependency requirements + +**Key challenges:** + +1. **Multiple library crates per package** + - How to declare multiple library crates in `Cargo.toml`? + - Naming scheme for library crates within a package? + - Which library is the "main" one (for backwards compatibility)? + - How do external packages depend on specific library crates within a package? + +2. **Friend/impl relationships within a package** + - Syntax for declaring impl deps between sibling library crates in the same package + - Do these need special visibility rules? + - How does this interact with the module system? + +3. **Cross-package impl dependencies** + - How to specify which library crate within a package is the impl dependency? + - Current proposal: `impl = true` on package dependency, but which crate in the target package? + - Need syntax for package-level dep → specific crate-level impl dep + +4. **Package resolution implications** + - Do impl deps affect resolution differently than regular deps? + - Version compatibility: how do semver rules apply to impl deps? + - Diamond dependencies: what if two packages have impl deps on different versions? + +5. **Publishing and ecosystem concerns** + - Current RFC prohibits publishing crates with impl deps to crates.io + - Workspace restrictions: impl deps only allowed within workspaces (path dependencies) + - How to prevent accidental publishing violations? + - Future: if we allow third-party impls, what are the ecosystem implications? + +6. **Metadata and build system integration** + - What information needs to be in package metadata? + - How do other build tools (Buck/Bazel) represent this? + - Passing impl dep information to rustc via `--extern impl:` + +7. **Interaction with existing features** + - Optional dependencies + - Cargo features and feature flags + - Dev/build dependencies + - Target-specific dependencies + +8. **Error messages and diagnostics** + - When impl dependency constraints are violated + - When someone tries to publish with impl deps + - When cross-workspace impl deps are attempted + +**Research needed:** +- Review other Cargo RFCs that impact dependency resolution +- Study how other build systems handle sub-package dependencies +- Analyze ecosystem impact of multiple libraries per package +- Consider backwards compatibility path + +## Grouping Strategy + +**Can group together:** +- 1a + 1b (terminology and tools inform each other) +- 2a + 2b (invariants and graph theory are intertwined) +- 4a + 4b (both implementation concerns) + +**Must separate:** +- Phase 2 before Phase 5 (need clear invariants before formalizing) +- Phase 3 separate (generics are complex enough to deserve isolated treatment) +- Tool selection (1b) before new spec (Phase 5) + +**Critical path:** 1b → 2a/2b → Phase 5 + +## Specific Recommendations + +**Graph theory term:** The correct term is likely **"immediate dominator"** or **"lowest common dominator"** - the first node in the dependency tree that dominates (can reach) all the implementing crates. In tree terms, it's the "lowest common ancestor" but in a DAG it's the dominator. + +**Re-exports restriction:** Propose relaxing this to "must be defined-or-reexported in the impl-dependency crate" with clear def-site tracking. The restriction seems overly conservative. + +## Formal Verification Tools Research Summary (2024) + +### Current State of Tooling + +**Good news**: Most formal verification tools now have decent VSCode integration, addressing concerns about Alloy's integrated-only environment. + +### Tool Comparison Matrix + +| Tool | IDE Support | Strengths for This Use Case | Weaknesses | 2024 Status | +|------|-------------|------------------------------|------------|-------------| +| **Alloy 6** | VSCode extensions available (multiple options) | ✓ Perfect for relational/graph properties
✓ Excellent counter-example finding
✓ Concise transitive closure
✓ Uses Kodkod SAT solver | - Not for formal proofs
- Bounded model checking only | Active (6.2.0 released Jan 2025) | +| **Forge** | Web-based + local tooling, Sterling visualizer | ✓ Based on Alloy with improvements
✓ Better visualization
✓ More user-friendly | - Teaching-focused
- Smaller community | New (OOPSLA 2024) | +| **TLA+** | Official VSCode extension, very active | ✓ Great for protocols/invariants
✓ Strong community | - Less natural for pure graph properties
- Steeper learning curve | Very active, "Nightly" builds | +| **Dafny** | Excellent VSCode integration, auto-verification | ✓ Can prove implementations correct
✓ Great IDE experience
✓ Verification-aware language | - Requires writing actual code
- Overkill for structural properties | Very active, LSP-based | +| **Lean 4** | VSCode + LSP, best-in-class | ✓ Most powerful prover
✓ Excellent tooling
✓ Strong metaprogramming | - Steep learning curve
- Overkill for this need | Extremely active (DeepMind using it) | +| **Coq** | Two VSCode options (VsCoq official, coq-lsp alternative) | ✓ Mature ecosystem
✓ Good for proofs | - Complex for graph properties
- Not ideal for counter-examples | Active (renamed to Rocq) | +| **Isabelle** | VSCode extension, but jEdit primary | ✓ Very mature
✓ Strong automation | - Tooling not as polished as Lean
- Learning curve | Active but VSCode is secondary | + +### Recommendation for Specific Needs + +Based on requirements (structural graph properties, counter-examples, fixed dependency graphs): + +**Primary tool: Forge or Alloy 6** +- **Forge** if you want better visualization and modern UX (published 2024) +- **Alloy 6** if you want the established tool with more resources +- Both now have VSCode support +- Both use Kodkod's SAT solver underneath (same engine) +- Both excel at relational constraints on graphs + +**For formal proofs later: Lean 4 or Dafny** +- **Lean 4** has the best tooling ecosystem in 2024, but significant learning investment +- **Dafny** is more pragmatic, easier to learn, good IDE integration + +### Specific Findings + +**Alloy improvements:** +- Alloy 6.2.0 (Jan 2025) added mutable state, temporal logic, improved visualizer +- Multiple VSCode extensions now available +- Still uses the integrated Alloy Analyzer, but VSCode extensions bundle it + +**Forge (new discovery):** +- Brown University's modern take on Alloy (2024) +- Better visualization with Sterling +- Language levels for gradual complexity +- Open source: https://github.com/tnelson/Forge + +**P language:** +- Good for state machines and protocols +- Less suited for pure structural properties than Alloy +- Overkill for static graph problem + +**Amazon's formal methods stack (from https://queue.acm.org/detail.cfm?id=3712057):** +- TLA+ for early system design and protocol verification +- P for modeling distributed systems (more programmer-friendly) +- Cedar for authorization policy language +- Dafny for implementation verification +- Kani for Rust code verification + +### Final Recommendation + +1. **Try Forge first** - it's Alloy with 10+ years of UX improvements, published 2024 +2. **Fall back to Alloy 6** if Forge is too teaching-focused or immature +3. **Use VSCode extension for either** to avoid the integrated environment issue +4. **Keep Lean 4 or Dafny in mind** for future formal proofs, but don't start there + +The original instinct about Alloy being right for the problem was correct, and the tooling situation has improved significantly. + +## What the Alloy/Forge Spec Should Look Like + +The problem is purely structural: given a fixed DAG with properties on nodes (definitions, implementations) and edges (deps, impl-deps), can you prove local constraints imply global invariants? + +### Basic Structure + +```alloy +sig Crate { + deps: set Crate, // regular dependencies + impl_deps: set Crate, // impl dependencies (subset of deps) + impls: Trait -> Type, // implementations in this crate +} + +sig Trait { def_crate: one Crate } +sig Type { def_crate: one Crate } + +// impl_deps must be subset of deps +fact { all c: Crate | c.impl_deps in c.deps } + +// Acyclic (build system enforces) +fact { all c: Crate | c not in c.^deps } + +// One binary root +one sig Binary extends Crate {} +fact { all c: Crate - Binary | c in Binary.^deps } +``` + +Then define: +- **Local orphan constraint**: what each crate can implement given its deps/impl_deps +- **Checker responsibility**: which crate must check which impl pairs +- **Prove**: local checks at each crate ⟹ global coherence for Binary + +### Key Insight + +Since each binary has independent coherence: +- Alloy finds counter-examples for a single binary's dep graph +- The property is: "for any dep graph rooted at a Binary, local rules ensure coherence" +- Multiple binaries = multiple separate Alloy checks (they don't interact) + +## Current Alloy Spec Problems + +The existing spec in the RFC has conceptual issues, not tool-choice issues: +1. Doesn't model impl-deps as distinct from regular deps +2. Doesn't formalize "checker responsibility" +3. Has a tautology in `dep_coherent_impl_crates` check +4. Doesn't capture "which crate is responsible for checking coherence" +5. Incomplete - has TODO for the most important constraint diff --git a/text/0000-extern-impl.md b/text/0000-extern-impl.md new file mode 100644 index 00000000000..305bd06ae02 --- /dev/null +++ b/text/0000-extern-impl.md @@ -0,0 +1,643 @@ +- Feature Name: extern_impl +- Start Date: 2023-07-17 +- RFC PR: [rust-lang/rfcs#0000](https://github.com/rust-lang/rfcs/pull/0000) +- Rust Issue: [rust-lang/rust#0000](https://github.com/rust-lang/rust/issues/0000) + +# Summary +[summary]: #summary + +This RFC proposes an opt-in mechanism to relax some of the restrictions of the +orphan rule, while maintaining the soundness of implementation coherence. It +also proposes a minimal Cargo extension to allow this feature to be exercised. +With this, the crate structure (and thus build system dependency graph) can be +decoupled from the actual implementations. + +# Motivation +[motivation]: #motivation + +Rust requires implementation coherence - that is, there's at most one +implementation of a trait for a type. This is required to: +- avoid any ambiguity about which implementation to use when compiling, and +- make sure that adding a new implementation does not change the meaning of +existing code. + +To do this, Rust implements the orphan rule, which requires that at least one of +the trait or the type are defined in the same crate as the implementation (ie is +a "local" definition). The "other" definition must be in a crate which is a +dependency, and as the dependency graph is acyclic, that "other" crate can't +possibly have a conflicting implementation because it can't have both +definitions in scope. + +The effect of this rule imposes some very hard constraints on how a developer +can factor their code into crates. For example it prevents: +- introducing a new trait and implementing it for existing types, without adding + dependencies for those types to all trait users + - more generally, refactoring to break dependency chains +- refactoring code to increase build parallelism +- adding trait implementations for types in crates whose source is generated (eg protobuf) +- splitting libstd/libcore +- multiple conflicting implementations to make different implementation + tradeoffs (eg size vs performance), or bindings to incompatible native + libraries (python 2 vs python 3) + +This RFC proposes an extension to the orphan rule which retains the coherence +invariant, while loosening the "locality" requirement for implementation. This +considerably increases implementation flexibility, at the cost of no longer +being able to enforce the invariant purely locally. + +At the rustc and language level, this mechanism is very general, and allows +almost arbitrary implementation relations between crates. However in practice +unconstrained use of this feature (ie implementing traits for types from +different crates from unrelated origins) would have large impacts on the general +Rust / crates.io ecosystem if not carefully considered. + +As a result, this RFC also proposes a fairly small Cargo extension which allows +the feature to be used within a workspace for experimentation, but leaves the +implications of publishing to crates.io to a future RFC. + +## More concrete example + +Say you've just written a new crate which defines a univeral interface to all +types of databases, called `DBTrait`. You want to make this trait useful from +the outset by implementing it for a number of existing DB crates. + +Today this means your `DBTrait` crate would need to take dependencies on every +one of those DB crates in order to do `impl DBTrait for X`. It also means that +every downstream user of `DBTrait` would also transitively gain those +dependencies. + +Here, `MysqlUser` ends up depending on all of `Mysql`, `MongoDB` and `RocksDB` +even though it only cares about `Mysql`. +```mermaid +graph TB +MysqlUser(MysqlUser) --> DBTrait --> Mysql & MongoDB & RocksDB +``` + +With this RFC, the implementation of `DBTrait` for each of the database crates +would be distributed among multiple implementation crates. Downstream users +would only need to take a dependency on the specific implemenetations they need. + +In this example, `MysqlUser` depends only on `DBTrait` and `DBMysql`, and is +unaffected by the `DBMongo` and `DBRocks` implementations. +```mermaid +graph TB +Bin(MysqlUser) --> DBMysql +DBMysql & DBMongo & DBRocks -->|impl| DBTrait +DBMysql --> Mysql +DBMongo --> MongoDB +DBRocks --> RocksDB +``` +# Guide-level explanation (cargo) +[guide-level-explanation]: #guide-level-explanation + +Within a workspace, you can designate an "impl" relationship between two crates. +For example, in your `my_impls/Cargo.toml` you can put: + +``` +[dependency] +my_definitions = { version = "0.1", path = "../my_definitions", impl = True } +``` + +This means that your `my_impls` crate can add trait implementations using types +or traits defined in `my_definitions`, almost as if they were defined in +`my_definitions`. If you want to use those implementations in other crates, +however, you must also add a dependency to both `my_impls` and `my_definitions` +(or you could re-export the definitions in `my_impls`). + +You may only implement for types/traits actually defined in `my_definitions` +itself. Re-exports don't count. + +The dependency *must* be a path dependency to another crate defined in the same +workspace. Cargo will not allow you specify `impl = True` for other crates. + +Publishing packages with any `impl = True` dependencies to crates.io is not +allowed. + +# Guide-level explanation (rustc) + +In current Rust, when you specify in your build system that a crate depends on +another, this is a "use" dependency - the dependee can use definitions in the +dependant. + +This RFC defines a new dependency relationship: the "impl" dependency. The +dependee can provide implementations for types and traits defined in the +dependant. + +We extend the `rustc` `--extern` flag with an additional `impl` flag: `--extern +impl:dbtrait=dbtrait.rlib`. This means that the crate currently being compiled +with this option, is allowed to implement traits and methods for types defined +in the `dbtrait` crate (the *defining* crate). + +For example: +```rust +//! Defining crate +trait DBTrait {} +``` +```rust +//! Implementation crate, also depends on the `mysql` crate. +use mysql::MySql; + +// Allowed because we're depending on `dbtrait` with `impl` +impl dbtrait::DBTrait for MySql {} +``` + +In other words, when the overlap check is considering what definitions are +"local", both the implementing crate and the defining crate both count. Note +that you may only implement traits and types for crates directly defined in the +defining crate — you cannot implement re-exported types. + +The defining and implementing crates are not the same in other respects. They +still have distinct crate names, defining their own crate-level namespaces. For +example, if they both defined a type `Foo`, it would be two definitions +`defining::Foo` and `implementing::Foo`. + +The terms "implementing" and "defining" describe a property of the dependency +relationship between two crates, not an intrinsic property of the crates +themselves. There are no other constraints on the defining and implementing +crates - they can freely define new traits, types and other items, and +implementations for those types and traits. An implementing crate can be a +defining crate for another crate. + +Regardless, the definitions within the defining crate, the implementing crate, +and between the implementing crate and defining crate must meet the current +coherence requirements. Also if there are multiple implementation crates in +scope in the dependency graph, they must also be coherent. + +# Reference-level explanation +[reference-level-explanation]: #reference-level-explanation + +> The idea of trait +> [coherence](https://rust-lang.github.io/chalk/book/clauses/coherence.html) is +> that, given a trait and some set of types for its type parameters, there +> should be exactly one impl that applies. + +A key part of this are *overlap checks*, which check that not only are there +currently no conflicting implementations, but adding new implementations won't +invalidate or change the meaning of existing code. + +These overlap checks can only be performed if all the relevant implementation +sites are known so they can be checked. This is the role of the *orphan rule*, +which has the consequence that there's only one possible crate in which contain +a given implementation. This is the restriction this RFC proposes to loosen. + +We introduce what could be called *the adoption rule*. This is an extension of +the orphan rule, in which implementations can be in more than one crate, but +some other crate adopts those implementation crates in order to apply the +overlap check across them in order to guarantee coherence. + +The actual details of the overlap check logic are unchanged; the only change is +a wider definition of what's considered a "local definition". + +## Changes to coherence checking + +The key problem we need to solve is how to reconcile the Rust language-level +details (types and traits) with the build system view (dependency relationship +between crates). Coherence is defined in terms of type/trait definitions and +implementations, which forms its own graph. This graph is embedded in the crate +dependency graph — that is there are no edges in the type/trait +implementation graph which are not also present in the crate dependency graph. + +Note that a blanket implementations - `impl Foo for T` - are a universal +quantifier over all types `T`, whether they're in scope or not. However if we're +interested in applying it to specific concrete types, we need only consider +those types which are in scope, which are therefore constrained by the +dependency graph. + +```mermaid +graph TB + CrateC -->|dep| CrateA & CrateB + subgraph CrateA + A["Trait A"] + D["Type D"] + E["Impl A for D"] -..->|impl| A & D + end + subgraph CrateB + B["Type B"] + end + subgraph CrateC + C["Impl A for B"] -..->|impl| A & B + end +``` + +For the discussion below, crate B is visible to crate A if it falls within its +transitive dependencies; a crate is visible to itself. + +```mermaid +graph TB + subgraph A sees only A + c1["A"] --> c2["..."] + c3["B"] + end + subgraph A sees A&B + b1["A"] --> b2["..."] --> b3["B"] + end + subgraph A sees A&B + a1["A"] --> a2["B"] + end +``` + +The general rule is when compiling a crate, `rustc` must check the coherence of +a set of implementations for a type if: +- all those implementations are visible +- no other visible crate has checked them + +This means the compilation of a crate must check for coherence when: +- all the definitions and implementations are within one crate +- if a crate A has an impl dependency (ie, a direct dependency with the impl + option) on crate B, it must check coherency between A and B +- if a crate has two or more crates with implementations for a given definition + within its view via distinct direct dependencies + +This last point is the most complex. For example: +```mermaid +graph TB + T -->|view| A & B -->|impl| D + A & B --> E +``` +Here, `T` must check `A` and `B`'s implementations are coherent with respect to +each other and definitions in `D` and `E`. It can rely that `A` and `B` are each +individually coherent with respect to `D` and `E` because that would have been +checked when `A` and `B` were compiled. + +Note that while `A` and `B` both depend +on `D` and `E`, they need only have a `impl` dependency on one of them; the `impl` +dependency simply means that `D`'s definitions are considered local to `A` and +`B` when seen in terms of the current orphan rule. + +This is OK even if `A` and `B` have different `impl` dependencies: +```mermaid +graph TB + T -->|view| A & B + A -->|impl| D + A --> E + B --> D + B -->|impl| E +``` +Since the groups (`A`, `D` `E`) and (`B`, `D` `E`) must be internally coherent, +and `T` still needs to check the coherence of (`A` and `B`). + +In this case: +```mermaid +graph TB + T --> A -->|view| B & C -->|impl| D +``` +`A` must check the coherence of `B` & `C`'s implementations with respect to `D`. +`T`, however, can rely on `A` having already checked `B` and `C`'s coherence +because both are visible through it's `A` dependency. + +A more complex example: +```mermaid +graph TB + T --> A -->|view| B & C -->|impl| D + B & C --> E + T --> C +``` +`T` can rely on `A` to check the coherence of `B` and `C`, even though `T` has +its own direct dependency on `C`, because `C` is also visible through `A`. + +But in this case: +```mermaid +graph TB + T --> A -->|view| B & C -->|impl| E + B & C --> F + T -->|view| D -->|impl| E +``` +`T` can rely on `A` for the coherency of `B` and `C`, but it must check the +coherence of `B`, `C` and `D` with respect to `E`. + +Note that this can mean that the same crates' coherency can be checked +redundantly. For example: +```mermaid +graph TB + Binary --> X & Y & Z -->|view| A & B -->|impl| C +``` +`X`, `Y` and `Z` are all the first to see the implementations of `A` and `B` +with respect to `C`, so must each do their own coherency checks, even though +`Binary` only needs for this to be performed once. Fortunately these redundant +checks can be done in parallel, but it's still a waste of CPU. See below for +some discussion about optimizing this. + +# Drawbacks +[drawbacks]: #drawbacks + +This adds a fair amount of complexity to a delecate part of the language +semantics and to the compiler's implementation of it. This is opt-in, but one +would need to understand these semantics when using other people's packages +which use this feature. + +If implemented as described here, and enabled in Cargo in an unconstrainted way, +it would enable full third-party implementations. That is, anyone could publish +a package implementing any type or trait in any other package. This would be +fine at small scalle, but at large scales it would mean that if there were two +crates with conflicting implementations, then could never appear in the same +dependency graph. That is a change to private dependencies, which wouldn't +usually be considered compatibility breaking, would cause downstream build +breakage. This would lead to very undesireable ecosystem-wide dynamics. As such +how this feature is used must be very carefully considered. + +# Rationale and alternatives +[rationale-and-alternatives]: #rationale-and-alternatives + +## Features + +In principle you could use Cargo "features" to achieve similar outcomes to the +motivating `DBTrait` example above - you'd define a feature for each DB +implementation, and the consumer would only enable the specific implementations +they want. + +For relatively small Cargo-defined projects, this would probably work fine. You +would lose some of the benefits (like type-only crates for use in declarations), +but it would solve the fundamental "don't want to depend on every DB" problem. + +However, because features are additive, as the dependency graphs get larger it +will tend towards having every feature enabled, so that every subgraph of the +overall dependency graph will end up depending on what everyone else depends on. +As a result, trait-defining crates like `DBTrait` become dependency bottlenecks +which end up single-threading the build. + +(This is particularly acute in cases where Cargo is primarily used as a +dependency management tool, and builds are done with another tool like Buck.) + +Sometimes features are used in a non-additive way, which is technically not +supported, but there's no mechanism to prevent it (or even warn about it). In +contrast, the mechanism described here does allow for separate implementation +crates with conflicting implementations, perhaps to allow for different +implementation tradeoffs, or bindings to different non-Rust implementations. + +Extensive use of features make code navigation difficult. For example, IDE +integration (VS Code + Rust Analyzer) often won't know which features are +enabled, and so will tend to dim feature-controlled code which should be +enabled, or vice versa. + +It's also hard to know which features should be enabled when generating +documentation with `rustdoc`. Not enabling features which are actually used +means that crate functionality goes undocumented, where as enabling too many +unused features can obscure the API the user actually wants to see. + +# Prior art +[prior-art]: #prior-art + +## Generally weak coherence + +Other languages have a very weak notion of coherence. C++ doesn't enforce it at +all, and simply defines conflicting implementations as UB. Haskell allows for +ecosystem wide conflicts, which may or may not be a problem in practice. + +Rust is unique(?) in separately-compiled languages in taking such a strong stand +on this, and it's been mostly beneficial. But it would be nice to have a +mechanism to loosen the constraints on this without admitting unsoundness. + +## Interface/implementation split + +In C and C++, there's a clear separation between "header files" containing a +specification of an interface, and "source files" which contain actual +implementations. Typically a compilation unit which has a dependency on another +compilation unit will include the header files containing the interface +definitions, and can be compiled with that information alone; it does not requre +the implementation of the dependant to be compiled. + +Ideally (and often in practice) this means that the entire program can be +compiled in parallel, with only the final linking step dependent on all the +compilation units. + +The primary disadvantage of this scheme is that the header file definitions must +be manually kept in sync with the implementations, and failing to do so can +cause numerous poor outcomes from linker errors to undefined behaviour. + +Today, Rust approximates this interface/implementation split with pipelined +builds, where `rustc` will generate a metadata object containing a crates +definitions, followed by actual code generation. The dependent compilation can +start as soon as the metadata is available without having to wait for the +generated code. But this still requires metadata for the entire dependency chain +- and for many crates the metadata generation *is* the expensive part of +compilation. + +With this RFC the split can be made more explicit by having actual separate +crates for definitions and implementations. + +# Unresolved questions +[unresolved-questions]: #unresolved-questions + +Intended for close coupled crates from same origin, but *could* be used for +generic third-party impls. + +The big question is what this looks like from a crates.io perspective. If we +could guarantee that `cargo publish` published an entire workspace atomically, +then + + +# Future possibilities +[future-possibilities]: #future-possibilities + +## Support intrinsic implementations + +This RFC focuses on implementing traits for types, since this is the common pain +point. In principle everything described above will also work for intrinsic +implementations, but there's some awkward secondary questions. For example, +intrinsic implementations tend to access the private fields of structs; does +that mean we need add or redefine visibility rules? + +## "Global" third-party implementations + +If this mechanism were broadly enabled for the crates.io ecosystem, it could +cause undesireably ecosystem splits. For example if you have type-defining +package `some_type` and trait defining package `some_trait`, you could have two +separate crates `A` & `B` implementing `some_trait` for `some_type`. If your +package `my_package` contains just one of `A` or `B` in its dependencies, then +all is OK. But at any point, with only a minor patch update, any package could +add the other to its dependencies, preventing your package from compiling. This +kind of brittleness is highly undesireable. + +So is there some way to enable third-party these kinds of third-party +implementation crates in a more general way without introducing this kind of +ecosystem brittleness? + +The [namespacing RFC](https://github.com/Manishearth/namespacing-rfc) +([PR)(https://github.com/rust-lang/rfcs/pull/3243)]) is also looking at +questions relating the the overall crates.io ecosystem. One could imagine a +proposal, for example, that packages within the same namespace could have this +`impl` relationship. But whether that makes sense really depends on the intended +semantics of namespaces. + +## Cached coherence checks + +There are cases where the same coherence properties may be checked multiple +times, if the same implementing crates are dependencies of multiple unrelated +crates. Perhaps these checks could be memoized with the incremental machinery to +avoid the redundancy. + + +## Auto-split crates + +Modules +within crates may have cyclic dependencies, but the crate dependency graph must +be acyclic. But only in extremely pathological cases will a crate's internal +dependency graph consist of a single strongly connected component. + +This opens the possibility of using the mechanism described in this RFC to +automatically partition a crate into sub-crates in order to expose more +built-time parallelism. This could either be performed inline during the build +or some tooling to perform pre-build processing on the crates. + +# Appendix - Alloy spec (WIP) + +--- +title: Alloy spec for Rust implementation coherency +--- + +Note: this is a literate [Alloy](https://alloytools.org/) spec. Download the +most recent version of Alloy from +https://github.com/AlloyTools/org.alloytools.alloy/releases, and see +https://alloy.readthedocs.io for documentation. + +# Alloy spec for Rust implementation coherency + +(TODO: make this fully consistent with the description above.) + +This is a simplified spec of Rust coherency checking. Rust requires that there +are no overlapping or conflicting implementations with a complete Rust program, +as that would allow for ambiguity about which one to use. + +(This applies to all implementations, but here we're only going to consider the +subset of simple trait implementations for types, with no generic type +parameters.) + +## Alloy Spec + +First we define signatures for types and traits. Both are defined in a crate: + +```alloy +sig Trait { + trait_def: one Crate +} + +sig Type { + type_def: one Crate +} +``` + +And crates themselves. Crates can depend on a set of other crates, but the +overall crate dependency graph must be acyclic. Each crate also has a relation +of which trait implementations for which types it contains. + +```alloy +sig Crate { + deps: set Crate, + impls: Trait -> Type, +} { + no this & this.^@deps -- acyclic +} +``` + +A Binary is the unique "top-level" crate which depends on all the other crates +transitively. Or to put it another way, no other crate depends on Binary. + +```alloy +one sig Binary extends Crate {} { + no @deps.this -- nothing depends on Binary + all c: Crate - Binary | c in this.^@deps -- Binary depends on everything else +} +``` + +Let's define the safety invariant we need to enforce, that every implementation +is unique. Or more precisely, for every trait/type pair, there's at most one +crate implementing it. (It's fine if nothing implements it.) + +```alloy +pred coherent_impls[crates: Crate] { + all tr: Trait, ty: Type | lone crates & impls.ty.tr +} +`````` + +This is the basic orphan rule, with a tight definition of "local": either the +type or the trait must be defined in the crate: + +```alloy +pred local_orphan_rule[crates: Crate] { + all crate: crates | + crate.impls in + (crate[trait_def] -> (crate + crate.deps)[type_def]) + + ((crate + crate.deps)[trait_def] -> crate[type_def]) +} +``` + +We can check that if `local_orphan_rule` is true for all crates, then we have +coherence for all crates. This has no counter-examples. + +```alloy +check local_coherent { + -- ie, checking local_orphan_rule on each crate implies that all crates are globally coherent + local_orphan_rule[Crate] => coherent_impls[Crate] +} +``` + +## impl dependencies + +Let's extend the orphan constraint so that the definition of "local" is extended +to immediate dependencies as well. In a way this is simpler than +`local_orphan_rule` because we no longer have to constrain either the type or +trait to be in `crate`. + +```alloy +pred dep_orphan_rule[crates: Crate] { + all crate: crates | + crate.impls in + (crate + crate.deps)[trait_def] -> (crate + crate.deps)[type_def] +} +``` + +However, this is not sufficient to maintain the invariant. This will quickly +find a counter-example with two crates with a duplicate implementation. + +```alloy +check dep_coherent_bad { + dep_orphan_rule[Crate] => coherent_impls[Crate] +} +``` + +We need to add additional constraints to maintain the invariant. First, let's +define a function which, for a given crate which defines types and/or traits, +all the crates with implementations for those definitions: +```alloy +fun impl_crates[c: Crate]: set Crate { + c[trait_def][impls.univ] + c[type_def][impls].univ +} +``` + +We can then apply the constraint in the most general way: for all dependencies +of Binary, all the crates implementing anything must be coherent. We'll ignore +that this is a tautology for now, as we'll tighten this up later. + +```alloy +check dep_coherent_impl_crates { + { + dep_orphan_rule[Crate] -- redundant + all dep: Binary.*deps | + coherent_impls[impl_crates[dep]] -- tautology + } => coherent_impls[Crate] +} for 10 -- make sure there's enough objects to be interesting +``` + +Unfortunately, this doesn't correspond to how the build is actually performed in +practice. When we're compiling a crate which has definitions, we don't know +which crates will have implementations. And when we're compiling the crates with +implementations, we don't know which other crate to cross-check with for +coherence. + +The key insight is that there must be *some* crate which has both the +implementing crates in its transitive dependencies (even if it's the top-level +Binary), which means it can check for coherence when compiling that crate. + +For example, here `Use` is responsible for checking the coherence of `ImplA` and +`ImplB` in its dependencies, but `ImplC` someone else's problem, and `Other` is +not relevant. +```mermaid +graph TD + Use --> ImplA & ImplB + ImplA & ImplB & ImplC --> Defn + Use --> Other +``` + +```alloy +-- TODO check constraint for common deps +```