Function der_real_bytes_wf_exec 

pub exec fn der_real_bytes_wf_exec(bytes: &[u8]) -> ok : bool

ensures

ok == der_real_bytes_wf(bytes@),

Executable checker for all canonical DER REAL contents forms.