[Ada] Add more annotations and assertions in the runtime