Handle `IndexMut` and `UpdateAt` in Rust

[W95Psp]

Currently we don't support user-defined impls of IndexMut. We need a way of translating IndexMut impls, probably as UpdateAt (a hax only construct).

[franziskuskiefer]

We use hax::fstar for now to inject the necessary code. We'll fix this properly later.

[W95Psp]

In more details, the work around is:

struct Foo(u8);

impl std::ops::Index<()> for Foo {
    type Output = u8;
    fn index(&self, idx: ()) -> &u8 {
        &self.0
    }
}

#[hax_lib::exclude]
impl std::ops::IndexMut<()> for Foo {
    fn index_mut(&mut self, idx: ()) -> &mut u8 {
        &mut self.0
    }
}

#[hax_lib::fstar::after(
    r#"
instance _: Rust_primitives.Hax.update_at_tc $:Foo $:{()} = {
   super_index = (_ by (Tactics.Typeclasses.tcresolve ()));
   update_at = $update_at;
}
"#
)]
fn update_at(mut x: Foo, i: (), v: u8) -> Foo {
    Foo(v)
}

[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.

[W95Psp]

We have a workaround, but we should still be able to support those directly.

[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.

[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.

[franziskuskiefer]

Closing in favour of full &mut support