Leftpad implementation and proof in SPARK

This small example shows the implementation and proof of Leftpad in SPARK, to answer this challenge.

You can verify the proof using SPARK as follows:

$ gnatprove -P test --report=all

and compile and run the simple test case as follows using GNAT Pro:

$ gprbuild -p -P test
$ ./obj/test_padding