Rekindling Specialization

# Rekindling Specialization :candle: _Dominik Stolz_ --- In Creusot, we need ```rust impl<T> Invariant for T { fn inv(self) -> bool { true } } ``` and ```rust impl<T: Ord> Invariant for BTreeMap<T> { /* ... */ } ``` but coherence says **no**! :sparkles:Specialization:sparkles: to the rescue!   --- ### Lifetime Erasure + Specialization = :boom:? ```rust impl<'a> Trait for (&'a T, &'a T) { /* ... */ } ``` cannot specialize ```rust impl<'a, 'b> Trait for (&'a T, &'b T) { /* ... */ } ``` Indistinguishable after lifetime erasure </br> Codegen has no lifetimes but needs them for resolution  :boom:  --- ### `min_specialization` :arrow_right: Rule out problematic specializations ...but, quite conservatively :question: Is this actually sound? :question: Can we relax the rules?  --- ### Soundness :ballot_box_with_check: - Paper proof of _lifetime independence_ - Treat trait resolution as black-box - WIP formalization in Coq --- ### Trajectory - Finish the Coq proof - Experiment with relaxing `min_specialization` - Implement in a-mir-formality - Write an RFC --- ### FIN --- ```js Lt ::= static | VarId Ty ::= rigid [Param] | VarId Param ::= Lt | Ty TraitRef ::= TraitId [Param] Wc ::= impl TraitRef | outlives Lt Lt Impl ::= ImplId TraitRef [Wc] Env ::= [Impl] [Wc] ``` --- ## Substitution $subst \subseteq (\text{VarId} \rightarrow \text{Param}) \times T \times T$ $s : \text{VarId} \rightarrow \text{Param}$ $$ \frac{s(v) = p}{subst\; s\; v\; p} $$ $$ \frac{subst\; s\; p\; p'}{subst\; s\; (\mathtt{rigid}\; [p \ldots])\; (\mathtt{rigid}\; [p' \ldots])} $$ --- ## Applicability $app \subseteq \text{Env} \times \text{TraitRef} \times \text{Impl}$ $$ \frac{\begin{array} \.\exists s, wc'. &subst\; s\; tr\; tr' \\ \land &subst\; s\; wc\; wc' \\ \land &hold\; \Gamma\; wcs' \end{array}}{app\; \Gamma\; tr\; (id, tr', [wc, \ldots])} $$ --- ## Overlap $overlap \subseteq \text{Env} \times \text{Impl} \times \text{Impl}$ $$ overlap\; \Gamma\; i_1\; i_2 \\ \iff \\ \exists tr. app\; \Gamma\; tr\; i_1\; \land app\; \Gamma\; tr\; i_2 $$ --- ## Resolution $resolve : \text{Env} \rightarrow \text{TraitRef} \rightharpoondown \text{Impl}$ $$ resolve(\Gamma, tr) = i \implies i \in \Gamma \land app\; \Gamma\; tr\; i $$ --- ## Resolution $resolve : \text{Env} \rightarrow \text{TraitRef} \rightharpoondown \text{Impl}$ $$ resolve(\Gamma, tr) = i \implies i \in \Gamma \land app\; \Gamma\; tr\; i $$ --- ## Specialiazation $$ resolve(\Gamma, tr) = i \\ \implies \\ \forall i'. app\; \Gamma\; tr\; i' \implies i \le i' $$ ---