Function extern_spec_Duration_from_micros 

pub fn extern_spec_Duration_from_micros(micros: u64) -> Duration

extern spec for Duration::from_micros

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

terminates

ghost

ensures

result@ == (micros@ * 1_000)