Function utc_time_to_bytes 

pub exec fn utc_time_to_bytes<Output: OutputBuf>(value: &UtcTime, obuf: &mut Output)

requires

value.wf(),

old(obuf).fits(utc_time_bytes(*value).len()),

ensures

final(obuf)@ == old(obuf)@ + utc_time_bytes(*value),

forall |n| old(obuf).fits(utc_time_bytes(*value).len() + n) <==> final(obuf).fits(n),

old(obuf).same_destination(final(obuf)),

Writes utc_time_bytes directly to an output buffer without allocating.