Function extern_spec_From__ref_str_Vec_u8_from 

pub fn extern_spec_From__ref_str_Vec_u8_from(s: &str) -> Vec<u8> 

extern spec for Vec<u8>::from

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

ghost

ensures

result@ == s@.to_bytes()