Function generalized_fraction_valid 

pub exec fn generalized_fraction_valid<const DER: bool>(
    bytes: &[u8],
    main_end: usize,
    zone_start: usize,
) -> bool

requires

main_end <= zone_start <= bytes.len(),

returns

generalized_fraction_wf::<DER>(bytes@, main_end, zone_start),

Verified executable implementation of generalized_fraction_wf.