New to Spark, working an example

[addaon@gmail.com]

Folks, new to this list, so not quite sure on etiquette.

I've been trying to understand Spark-2014 well enough to work through an example, and understand the capabilities and workflow of the tools. The example I chose was an example of floor(lg(n)) for n positive.

Rather than put a long post here, I'll refer to my (long) post at stackoverflow: https://stackoverflow.com/questions/53752715/proving-floor-log2-in-spark. (If this is bad etiquette here, let me know, and I'll fix -- but it does seem a bit silly to duplicate the content in two locations.)

Since SO seems to have a very limited Ada/Spark community, I'm hoping someone here can point me in the right direction. Basically, trying to understand what tools I should be trying to understand at this point. :-) Should I be looking at proving this with just a better understanding of how to write loop invariants; through appropriate lemmas; through an external prover like Coq; or something else?

Thanks!