[Ada] Proof of Ada.Strings.Maps

[Ada] Proof of Ada.Strings.Maps

gcc/ada/

	* libgnat/a-strmap.adb: Add ghost code for proof.
	(To_Range): This is the most involved proof, as it requires
	creating the result of the call to To_Domain as a ghost
	variable, and show the unicity of this result in order to prove
	the postcondition.
	* libgnat/a-strmap.ads: (SPARK_Proof_Sorted_Character_Sequence):
	New ghost function.
	(To_Domain): Add postcondition regarding sorting of result.
	(To_Range): Fix postcondition that should compare Length instead
	of Last for the results of To_Domain and To_Range, as the value
	of Last for an empty result is not specified in the Ada RM.