How to specify types with interior mutability

[xldenis]

@fpoli sent me this example problem which raises some interesting issues about #[trusted] and interior mutability:

mod lib {
    use ::std::sync::Mutex;
    use creusot_contracts::*;

    #[repr(C)]
    pub struct T<'a> {
        inner: &'a mut u32,
        mutex: Mutex<()>,
    }

    impl<'a> T<'a> {
        #[trusted]
        pub fn new(inner_mut: &'a mut u32) -> Self {
            T { inner: inner_mut, mutex: Mutex::new(()) }
        }
    }

    #[ensures(*this == ^this)]
    #[ensures(result == *this.inner)]
    pub fn query<'a>(this: &mut T<'a>) -> u32 {
        *this.inner
    }

    #[trusted]
    pub fn increment<'a>(this: &T<'a>) {
        let _guard = this.mutex.lock();
        unsafe {
            let ptr: *mut *mut u32 = ::std::mem::transmute(&this.inner);
            **ptr = **ptr + 1;
        }
    }
}

fn test<'a>(mut t: lib::T<'a>) {
    let a = lib::query(&mut t);
    lib::increment(&t);
    let b = lib::query(&mut t);
    assert!(a == b);
}

The issue is that apparently (according to Ralf), increment is not UB, and thus we can use to Mutex to interiorly mutate the inner field of T.
This means that we should treat all of T as a Cell, and thus actually can't give query an informative specification.
However, this is a big trap: the contract for query is correct, there's no reason we shouldn't be able to use that, and somehow the addition of a separate increment function invalidates that contract.
One issue I have here, is that creusot provides no useful feedback to help you understand the issue, and second, we provide no useful mechanism to specify query (it would be nice to say that its a non-decreasing value).