Bug: `MutBorrowKind::ClosureCapture` not implemented

[RaitoBezarius]

Code snippet to reproduce the bug:

// add your code here
pub struct CountMinSketch {
    // one for each depth
    hashers: Vec<ahash::RandomState>,
    width: usize,
    depth: usize,
    // buckets, width*depth
    buckets: Vec<u32>,
}

impl CountMinSketch {
    fn new(width: usize, depth: usize, rng: &mut (impl RngCore + CryptoRng)) -> Self {
        Self {
            hashers: (0..depth)
                .map(|_| {
                    ahash::RandomState::with_seeds(
                        rng.next_u64(),
                        rng.next_u64(),
                        rng.next_u64(),
                        rng.next_u64(),
                    )
                })
                .collect(),
            width,
            depth,
            buckets: alloc::vec![0; width * depth],
        }
    }
}

Charon version: 962f26311ccdf09a6a3cfeacbccafba22bf3d405

Charon command: nix run "github:AeneasVerif/aeneas/b1ca1ff00c15a550eab385d58306697a4a68d674#charon"

Charon output:

thread 'rustc' panicked at src/bin/charon-driver/translate/translate_functions_to_ullbc.rs:51:51:
not implemented
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
error: Thread panicked when extracting body.
  --> rustyguard-utils/src/rate_limiter.rs:60:5
   |
60 |     fn new(width: usize, depth: usize, rng: &mut (impl RngCore + CryptoRng)) -> Self {
   |     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[WARN charon_driver::translate::translate_predicates:685] Could not find a clause for parameter:
- target param: @TraitDecl20<F, (B, core::iter::range::{impl core::iter::traits::iterator::Iterator for @Adt2<A>}#15<A>[@TraitClause0]::Item)>
- available clauses:
[Self]: core::iter::traits::iterator::Iterator<@Adt2<A>>
[@TraitClause0]: core::iter::range::Step<A>
[@TraitClause1]: @TraitDecl20<F, (B, A)>
[@TraitClause2]: @TraitDecl21<R>
- context: core::iter::range::{impl#15}::try_fold
[WARN charon_driver::translate::translate_predicates:685] Could not find a clause for parameter:
- target param: core::ops::function::FnMut<FFF, (AAA, core::iter::range::{impl core::iter::traits::iterator::Iterator for @Adt2<A>}#15<A>[@TraitClause0]::Item)>
- available clauses:
[Self]: core::iter::traits::iterator::Iterator<@Adt2<A>>
[@TraitClause0]: core::iter::range::Step<A>
[@TraitClause1]: core::ops::function::FnMut<FFF, (AAA, A)>
- context: core::iter::range::{impl#15}::fold
error: could not compile `rustyguard-utils` (lib) due to 3 previous errors
Error: Charon driver exited with code 101

Any other steps needed to reproduce:

Explain the bug: N/A.

[Nadrieril]

This error comes from the mutable borrow in a closure: this uses a special type of borrow MutBorrowKind::ClosureCapture which we'll have to support. Thanks for the report!

[Nadrieril]

Minimized:

struct Rng;

impl Rng {
    fn next_u64(&mut self) {}
}

fn new(rng: &mut Rng) {
    let _ = || {
        rng.next_u64();
    };
}

[sonmarcho]

Which changes in Charon were required to support this?

[RaitoBezarius]

I assume this one: https://github.com/AeneasVerif/charon/pull/339/commits/87fc7ebe1b7841be90676bd7b86aa1698f8be021

[sonmarcho]

Thanks!