Aymeric Fromherz

Thank you very much for your interest and your feedback! Regarding your different points: 1/ Indeed, we are for now overly conservative about generating mutable instead of shared borrows for...

Hi @ctz , just wanted to let you know that @msprotz and myself recently worked on removing needless mutable borrows, which hopefully should address your first point above. The latest...

After debugging a bit, I am not sure this is due to recursive functions or traits. Below is a minimized example leading to the same error. The problematic part is...

After discussion with @sonmarcho and @Nadrieril , we decided to rename the current Span into RawSpan, and what was renamed into SpanMeta (previously Meta) into Span. I'll take care of...

This is now ready for review, the PR on the Aeneas side has also been updated.

> There was another change in-between that also upgraded the charon version to `0.1.3`. Could you bump it to `0.1.4`? Done in [4ae6dcc](https://github.com/AeneasVerif/charon/pull/174/commits/4ae6dcc1273a8563c3ac289929cdfc4792f8c5c2)

Looks good to me too, at least as an initial template (we can always extend later). Feel free to merge.

@karthikbhargavan @mamonet do you have an opinion on this?

Similar to https://github.com/AeneasVerif/aeneas/issues/188