Function extern_spec_Duration_from_millis 

pub fn extern_spec_Duration_from_millis(millis: u64) -> Duration

extern spec for Duration::from_millis

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

terminates

ghost

ensures

result@ == (millis@ * 1_000_000)