[Lean] Generate specs for functions without annotations

[abentkamp]

Public functions without annotations should be handled as if they were annotated True/True (i.e. claim unconditional panic freedom)

Private functions without annotations should be marked as @[spec] so that they get unfolded when calling mvcgen.