Verify the TLS public API

[vkanne-msft]

Goal of this task is to have fully verified top level API. @nikswamy is the primary owner driving this.

[nikswamy]

Not much progress on this since the Cambridge all-hands summit, I'm afraid.

I've mostly been working on many F* features in support of Kremlin/Record layer, notably more normalization. Also, I've been working on the AEAD invariant in the record layer.

At this rate, I suspect that I will not be able to finish this by November 1---hope to get the proof of the AEAD invariant done by then. I expect to work on this top-level API proof post November 1, hopefully will be done by November 15th.