Function extern_spec_String_from_utf8_unchecked 

pub unsafe fn extern_spec_String_from_utf8_unchecked(bytes: Vec<u8>) -> String

extern spec for String::from_utf8_unchecked

This is not a real function: its only use is for documentation.

terminates

ghost

requires

exists<s: Seq<char>> s.to_bytes() == bytes@

ensures

result@.to_bytes() == bytes@