Function utf8_from_bytes_unchecked 

pub exec fn utf8_from_bytes_unchecked<'a>(bytes: &'a [u8]) -> res : &'a str

requires

vstd::utf8::valid_utf8(bytes.deep_view()),

ensures

res.spec_bytes() == bytes.deep_view(),

res.deep_view() == vstd::utf8::decode_utf8(bytes.deep_view()),