Instruct Aeneas not to lower modeled functions

[joshlf]

We can do this by passing --opaque path::to::function (Zulip thread).

it's trickier if you want to mention impl items. for inherent impls you have to write path::to::module::_::function_name where the _ will match the impl block. for trait impls there's a special {impl path::to::trait for path::to::type}::method_name that's a bit tricky to get right at the moment but works nicely. you can also use the same trick as inherent impls, that works too

– @Nadrieril