Mutation through `Deref`/`DerefMut` traits

[W95Psp]

Often, methods are not defined on a type T but rather on <T as std::ops::Deref>::Target: when you call x.foo(), you are actually calling x.deref().foo() or x.deref_mut().foo().

The latter is an issue for hax: if you mutate the deref_mut version of x, hax needs to know how to propagate the change into x itself. Though, often, the deref trait is implemented for smart pointers, and x is more or less equivalent to x.deref().

We have an allowlist for transparent T deref implementation (when, in the backends, we extract <T as std::ops::Deref>::Target as T).

Some patterns are not covered, this issue lists them. Feel free to comment if you find new such patterns. If you want to be sure that you issue is relevant here, you can run cargo hax into -d i fstar (or another backend) and use the web debugger to see wether a deref_mut appears at the error location.

Things we should treat as transparent

Vec<T> (Target is &[T])

(spotted by @franziskuskiefer in https://github.com/hacspec/hax/issues/490)

// XXX: (RefMut) At this position, Hax was expecting an expression of the shape 
//      `&mut _`. Hax forbids `f(x)` (where `f` expects a mutable reference as 
//      input) when `x` is not a place expression[1] or when it is a dereference 
//      expression. 
// 
// NOTE: This goes through when `a` is an array. 
fn xor(mut a: Vec<u8>, b: [u8; 4]) -> Vec<u8> { 
    for i in 0..4 { 
        a[i] ^= b[i] 
    } 
    a 
} 

[W95Psp]

It is probably related to https://github.com/hacspec/hax/issues/231

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.