Milnes strings

[briangmilnes]

I have 'thickened' strings quite a bit. There are additions to the end of FStar.String.fst that define a partial string equality and string equality and provide a string difference (for upcoming Final testing framework). The added functions are in FStar.String.Base and quite a few proofs in FStar.String.Properties. As well as as a decidable equality class on streq.

FStar.String.Properties has 36 proofs showing the relationships between streq, streq' (it's boolean equivalent), lengths, indexes and the string differencer first_diff.

This, as expected, does not seem to increase proof times.

I did not include Base and Properties into FStar.String.fsti, so it's questionable if I have the right form here. And is it right to name the property streq and the boolean streq'?

I also added a tests/validate-time/Test.FStar.String.fst to test this.

And adjusted fstar.mk to allow overwriting of WARN_ERROR so I could cut down some warnings in validate-time tests.