Function extern_spec_Instant_now 

pub fn extern_spec_Instant_now() -> Instant

extern spec for Instant::now

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

ensures

result@ >= 0