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 https://github.com/flux-rs/flux/commit/d64a0a3e1af71553d43f8d5ea0b3c3eb797b0626, 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)