Mutable references (`&mut T`) with complex aliasing (meta-issue)

[W95Psp]

Hax promotes a functional style in Rust: it doesn't aim at supporting complex mutation schemes.

We allow:

• &mut arguments on user-defined functions;
• pass &mut arguments to any function or operator;
• use of certain &mut-returning functions.

We disallow:

1. defining &mut-returning functions (see cryspen/hax-evit#8);
2. aliasing an &mut-typed variable (i.e. fn f(x: &mut u8) { let y = x; ...}, see Unsupported: implicit reborrowing #419);
3. mutable borrows inside types.

[github-actions]

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.