Function generalized_fields_valid 

pub exec fn generalized_fields_valid(bytes: &[u8], main_end: usize) -> bool

requires

main_end <= bytes.len(),

returns

generalized_fields_wf(bytes@, main_end),

Verified executable implementation of generalized_fields_wf.