Function generalized_zonestart 

pub exec fn generalized_zonestart(bytes: &[u8]) -> zone_start : usize

ensures

zone_start <= bytes.len(),

returns

generalized_zone_start(bytes@),

Verified executable implementation of generalized_zone_start.