valid_utf8_concat

vstd::utf8

Function valid_utf8_concat 

Source 
pub broadcast proof fn valid_utf8_concat(b1: Seq<u8>, b2: Seq<u8>)
Expand description
requires
#[trigger] valid_utf8(b1),
#[trigger] valid_utf8(b2),
ensures
#[trigger] valid_utf8(b1 + b2),

Ensures that concatenating two valid UTF-8 byte sequence results in a valid UTF-8 byte sequence.