UTF-8 encode and decode: Difference between revisions

The following code is quite long but consists largely of proofs. UTF-8 is a complicated encoding, but also a well defined encoding,one whichthat lends itself to compile-time verification methods.