flux
flux copied to clipboard
Story for mutating traits
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
)