Story for mutating traits

[skius]

Inspired by the Flux paper's usage of the std library swap<T>(&mut T, &mut T) function, I was curious why/how Flux was able to pass refinements through the function. I think I reached a conclusion in that one cannot do anything with a T, just move it around, so whatever refinement input swap gets, it will be preserved through to the output.

I came up with the following example that still has a T, but actually changes the T, meaning a generic refinement input can not in general be preserved to the output:

trait MyTrait { fn reset(&mut self); }

impl MyTrait for i32 { 
    fn reset(&mut self) { *self = 0; } 
}

fn swap<T: MyTrait>(a: &mut T, b: &mut T) {
        a.reset();
}

#[flux::sig(fn() -> i32{v: v >= 10})]
fn test() -> i32 {
        let mut x = 10;
        let mut y = 20;
        swap(&mut x, &mut y);
        x
}

In contrast to the paper's function, T is now a MyTrait, with which I can "arbitrarily" modify the values, in particular, refinements from the input may not hold anymore, and indeed, test is not type safe.
What is Flux's story for this (or rephrased, are there plans to support this)? On my system, using commit d64a0a3, running rustc-flux --crate-type=lib file.rs results in no errors and 0 exit code, however, the playground reports an invisible error: link.

(Replacing the MyTrait stuff with just T: Default and *a = Default::default() results in a compiler panic: crates/flux-refineck/src/type_env.rs:143:13: cannot move out of *_1)

[nilehmann]

yes, the analysis is unsound in the presence of trait bounds. We don't have concrete plans to work on it but we would definitely like to tackle it at some point. We just have other projects in mind and resources are limited. It will make a fantastic project if someone wants to get involved!

I do have some ideas though. It all boils down to how you interpret impl MyTrait for i32. Putting aside how it can be implemented, a couple of ideas come to mind.

The first one is that we can interpret impl MyTrait for i32 as implementing the trait on the trivial refinement. Typically when you write a type without refinements, it desugars to a type with a trivial refinement. For i32 this would be i32{v: true}¹.

Under this reading, impl MyTrait for i32 would mean impl MyTrait for i32{v: true}. In this world, you would have to infer the trivial refinement for x and y when calling swap, as that's the only type that implements the trait. Because of this, you would lose all information after the call and the code would be rejected.

This leaves space to be able to implement traits on other refinement types not just the trivial one. For example, you could do impl MyTrait for i32{v: v > 0}. This opens a lot of questions about how trait resolution works and whether you can implement the trait on different refinements. There are also a lot of technical questions about how to implement this on top of rust without modifying the trait solver.

Another idea that is still very vague in my mind is to interpret trait impls using what I call a shape. A shape is what you get when you strip all refinements out of a type, i.e., a plain rust type. You could then interpret impl MyTrait for i32 as something like impl<T> MyTrait for T where shape(T) == i32 to say that the trait is implemented for every possible refinement of i32. In this world, the implementation of reset would be rejected because you cannot prove *self = 0 safe for every possible refinement of i32. This is as far as I've gone with this idea though.

Footnotes

1. In Flux, we represent the trivial refinement a bit differently. This is not documented anywhere, but we have a more general notion of existential types where you can quantify arbitrarily over a refinement variable of some sort. Using a general existential, the trivial refinement type for i32 is written {v:int. i32[v]}, that's it, we represent the set of all i32 values by existentially quantifying over the index. ↩

[skius]

Thank you for the detailed reply, interesting thoughts! This seems like a challenging problem indeed. (As a side note, I'm really fascinated by this project, thanks for working on it!)

A thought for a 'hack' to fix soundness: Have you played around with the thought of restricting polymorphic refinements as soon as a trait bound is introduced? I.e., the current fn <T, p>(T{v: p(v)}) (excuse my notation) would be restricted in the case of trait bounds to the trivial refinement fn <T: Bound>(T{v: true})? I suspect this would break a lot of things you get for free with the type system, but I don't have the overview to say for sure. Actually, this seems semantically equivalent to the one case of your first idea where a trait is only (and can only be) implemented for the trivial refinement.

A second thought, this time about your first idea:

This opens a lot of questions about how trait resolution works and whether you can implement the trait on different refinements. There are also a lot of technical questions about how to implement this on top of rust without modifying the trait solver.

Both questions seem quite important to me, so what if instead of allowing whole different method impl's for different refinement trait bounds, we have different refinement signatures depending on the actual refinement?

Maybe an example to illustrate this idea:
impl MyTrait for i32 desugars to impl<p> MyTrait for i32{v: p(v)}. Now the reset method requires p(0), and this bubbles up to the trait impl, essentially saying impl<p: p(0)> MyTrait for i32{v: p(v)}. The benefit of this over the shape idea (as far as I can tell), is that now you just need a supertype of i32[0] and the implementation is not restricted. This would be extended to multiple methods in a trait by just requiring the conjunction of all the methods' preconditions. Furthermore, this can all happen after regular Rust trait resolution, as there is only one impl for i32.

Without knowledge of Flux's inner workings, I would assume something like the following to happen: From Rust, Flux sees that T ~= <i32 as MyTrait>. Now, for the "refinement trait resolution" to succeed, Flux needs to infer a p for which p(0) (the precondition of <i32 as MyTrait>) holds. Because swap is generic, it has a generic q refinement predicate for i32, from which Flux must prove p(0). Because q is unconstrained, this fails.

An (admittedly) significant downside to this approach is that I don't know how a user could specify a precondition to swap that satisfies the precondition of an arbitrary <T as MyTrait>. I don't know if this is a general impossibility, or just missing surface syntax. However, something that I could see perhaps working is (inventing syntax here):

fn swap<T: MyTrait, q: predicate>(&mut T{v: q(v)}, &mut T{v: q(v)}) requires precondition(q, T, MyTrait) {...}

where precondition(q, T, MyTrait) returns whether the precondition q satisfies the precondition for each T, i.e., in the i32 case it would be equivalent to requires q(0).

With this signature, Flux could only infer some supertype of {0, 10, 20} for the swap call in test, and the postcondition verification would fail.

(Another downside to this, I suppose, is that standard library methods probably aren't valid Flux anymore?)

[nilehmann]

A thought for a 'hack' to fix soundness: Have you played around with the thought of restricting polymorphic refinements as soon as a trait bound is introduced? I.e., the current fn <T, p>(T{v: p(v)}) (excuse my notation) would be restricted in the case of trait bounds to the trivial refinement fn <T: Bound>(T{v: true})? I suspect this would break a lot of things you get for free with the type system, but I don't have the overview to say for sure. Actually, this seems semantically equivalent to the one case of your first idea where a trait is only (and can only be) implemented for trivial the refinement.

Something like this wouldn't be too hard to implement, at least to handle the example in the op. You have the right intuition, but the details are a bit different. When you have a function fn foo<T>(x: T) and you call it with i32, e.g., foo(0), the way it works is that we generate an i32 refined with a kvar, i.e., i32{v: $k(v)}, where $k is a predicate we need to infer. Note that the function itself is not parameterized by a predicate, but by a type and we instantiate with a type we need to infer, this end up having a similar effect to your example though. Once you add a bound fn foo<T: Bound>(x: T) the most natural way to implement it would be to still generate i32{v: $k(v)}, but then constraint it such that it has type the trait is implemented on. In this case, you would generate i32{v: $k(v)} <: i32{v: true} and i32{v: true} <: i32{v: $k(v)} to constraint the type to be the trivial refinement (I think it needs to be invariant). But you could also as you suggest avoid the extra step and instantiate T with i32{v: true} directly.

Both questions seem quite important to me, so what if instead of allowing whole different method impl's for different refinement trait bounds, we have different refinement signatures depending on the actual refinement?

Maybe an example to illustrate this idea:
impl MyTrait for i32 desugars to impl

MyTrait for i32{v: p(v)}. Now the reset method requires p(0), and this bubbles up to the trait impl, essentially saying impl<p: p(0)> MyTrait for i32{v: p(v)}. The benefit of this over the shape idea (as far as I can tell), is that now you just need a supertype of i32[0] and the implementation is not restricted. This would be extended to multiple methods in a trait by just requiring the conjunction of all the methods' preconditions. Furthermore, this can all happen after regular Rust trait resolution, as there is only one impl for i32.

Without knowledge of Flux's inner workings, I would assume something like the following to happen: From Rust, Flux sees that T ~= . Now, for the "refinement trait resolution" to succeed, Flux needs to infer a p for which p(0) (the precondition of ) holds. Because swap is generic, it has a generic q refinement predicate for i32, from which Flux must prove p(0). Because q is unconstrained, this fails.

An (admittedly) significant downside to this approach is that I don't know how a user could specify a precondition to swap that satisfies the precondition of an arbitrary . I don't know if this is a general impossibility, or just missing surface syntax. However, something that I could see perhaps working is (inventing syntax here):

fn swap<T: MyTrait, q: predicate>(&mut T{v: q(v)}, &mut T{v: q(v)}) requires precondition(q, T, MyTrait) {...}

where precondition(q, T, MyTrait) returns whether the precondition q satisfies the precondition for each T, i.e., in the i32 case it would be equivalent to requires q(0).

With this signature, Flux could only infer some supertype of {0, 10, 20} for the swap call in test, and the postcondition verification would fail.

This feels similar in spirit to the shape idea. You could also introduce bounds using shapes, e.g., saying impl<T> MyTrait for T where shape(T) = i32, i32{v: v == 0} <: T (actually, now I realize that the subtyping bound subsumes the shape constraint, so you maybe don't need that) I think there's a difference in style on whether you are being parametric on types or predicates

Anyhow, agree that you need some form of constraining the refinements the trait is being implemented on. I also fancy the idea of using more parametric predicates. For example, one thing I know we will need is associated predicates. I have an example in mind where you want to refine the Index/IndexMut trait. The idea is to constrain the indices such that they are contained in the collection. However, you only know what being contained means once you have a specific implementation, so you have to be parametric on the being contained predicate. I'm envisioning something like:

pub trait Index<Idx> {
    type Output;
    predicate p: (Self, Idx) -> bool;

    fn index(&self, index: Idx{Self::p(index)}) -> &Self::Output;
}

impl<T> Index<usize> for RVec<T> {
    type Output = T;
    predicate p = |vec, index| 0 <= index && index < vec.len;
    
    fn index(&self: RVec<T>[@vec], index: usize{0 <= index && index < vec.len}) -> &T { ... }
}

This hides a lot of complexity and it touches on some recent progress we've been making around polymorphic sorts

[skius]

Exciting stuff! I will definitely be following the progress :)

Feel free to close this issue if you're already tracking this somewhere/have other plans

[nilehmann]

I'm converting this into a discussion because it has interesting context, but there's no specific issue.