Function extern_spec_Duration_from_secs 

pub fn extern_spec_Duration_from_secs(secs: u64) -> Duration

extern spec for Duration::from_secs

This is not a real function: its only use is for documentation.

terminates

ghost

ensures

result@ == secs_to_nanos(secs@)