Attribute Macro proven_externally 

#[proven_externally]