Request: connecting Unicode logic to the string type

[robin-aws]

src/Unicode has a fairly pure implementation of UTF-16 and UTF-8, but it uses bit vector types and doesn't use char or string at all. We definitely need a standard library that does (and the incoming JSON PR does itself, since it needs to encode a string in UTF-8), although this means we'll need at least some Dafny code that is duplicated to account for the difference in behavior from --unicode-char.

[robin-aws]

Addressed by #51 - see https://github.com/dafny-lang/libraries/blob/master/src/Unicode/UnicodeStrings.dfy