[Ada] Proof of Ada.Characters.Handling

[Ada] Proof of Ada.Characters.Handling

gcc/ada/

	* libgnat/a-chahan.adb: Add loop invariants as needed to prove
	subprograms.  Also use extended return statements where
	appropriate and not done already.  Mark data with
	Relaxed_Initialization where needed for initialization by parts.
	Convert regular functions to expression functions where needed
	for proof.
	* libgnat/a-chahan.ads: Add postconditions.
	* libgnat/a-strmap.ads (Model): New ghost function to create a
	publicly visible model of the private data Character_Mapping,
	needed in order to prove subprograms in Ada.Characters.Handling.