fn push_halmos_lengths( values: &mut Vec<String>, field: &str, value: &str, flag: &str, ) -> Result<(), String>