Specify `String::as_mut_vec`?

[Lysxia]

impl String {
  unsafe fn as_mut_vec(&mut self) -> &mut Vec<u8>
}

Issue split from https://github.com/creusot-rs/creusot/issues/1379

Ideally some post_requires clause would exist (factoring out the requirements into a predicate to use it both in the ensures and post_requires clauses).

This is what we refer to as "after_expiry" or a pledge

[Lysxia]

I wonder if we can use CPS as a workaround?

unsafe fn with_mut_vec(&mut self, k: for<'a> impl FnOnce(&'a mut Vec<u8>) -> R) -> R

[jhjourdan]

This is definitely an option indeed, even though on the long term I would prefer supporting open borrows.