UTF-8 decoding

This file contains the low-level proof that UTF-8 decoding and encoding are inverses. An important corollary is that attempting to decode a byte array that is valid UTF-8 will succeed, which is required for the definition of String.toList.

Char.utf8Size

theorem Char.utf8Size_eq_one_iff {c : Char} : c.utf8Size = 1 ↔ c.val ≤ 127

theorem Char.utf8Size_eq_two_iff {c : Char} : c.utf8Size = 2 ↔ 127 < c.val ∧ c.val ≤ 2047

theorem Char.utf8Size_eq_three_iff {c : Char} : c.utf8Size = 3 ↔ 2047 < c.val ∧ c.val ≤ 65535

theorem Char.utf8Size_eq_four_iff {c : Char} : c.utf8Size = 4 ↔ 65535 < c.val

theorem Char.utf8Size_pos (c : Char) : 0 < c.utf8Size

theorem Char.utf8Size_le_four (c : Char) : c.utf8Size ≤ 4

theorem Char.utf8Size_eq (c : Char) : c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4

utf8EncodeChar

utf8EncodeChar low-level API

def String.utf8EncodeCharFast (c : Char) : List UInt8

Returns the sequence of bytes in a character's UTF-8 encoding.

@[csimp]

theorem String.utf8EncodeChar_eq_utf8EncodeCharFast : utf8EncodeChar = utf8EncodeCharFast

@[simp]

theorem String.length_utf8EncodeChar (c : Char) : (utf8EncodeChar c).length = c.utf8Size

theorem String.utf8EncodeChar_eq_singleton {c : Char} : c.utf8Size = 1 → utf8EncodeChar c = [c.val.toUInt8]

theorem String.utf8EncodeChar_eq_cons_cons {c : Char} : c.utf8Size = 2 → utf8EncodeChar c = [(c.val >>> 6).toUInt8 &&& 31 ||| 192, c.val.toUInt8 &&& 63 ||| 128]

theorem String.utf8EncodeChar_eq_cons_cons_cons {c : Char} : c.utf8Size = 3 → utf8EncodeChar c = [(c.val >>> 12).toUInt8 &&& 15 ||| 224, (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]

theorem String.utf8EncodeChar_eq_cons_cons_cons_cons {c : Char} : c.utf8Size = 4 → utf8EncodeChar c = [(c.val >>> 18).toUInt8 &&& 7 ||| 240, (c.val >>> 12).toUInt8 &&& 63 ||| 128, (c.val >>> 6).toUInt8 &&& 63 ||| 128, c.val.toUInt8 &&& 63 ||| 128]

utf8EncodeChar BitVec API

Size one

Size two

Size three

Size four

parseFirstByte

parseFirstByte definition

inductive ByteArray.utf8DecodeChar?.FirstByte : Type

• invalid : FirstByte
• done : FirstByte
• oneMore : FirstByte
• twoMore : FirstByte
• threeMore : FirstByte

@[inline]

def ByteArray.utf8DecodeChar?.parseFirstByte (b : UInt8) : FirstByte

parseFirstByte low-level API

parseFirstByte BitVec API

Size one

Size two

Size three

Size four

isInvalidContinuationByte definition & API

@[inline]

def ByteArray.utf8DecodeChar?.isInvalidContinuationByte (b : UInt8) : Bool

parseFirstByte, isInvalidContinuationByte and utf8EncodeChar

assemble₁

@[inline]

def ByteArray.utf8DecodeChar?.assemble₁ (w : UInt8) (h : parseFirstByte w = FirstByte.done) : Option Char

@[inline]

def ByteArray.utf8DecodeChar?.verify₁ {w : UInt8} (_w : UInt8) (_h : parseFirstByte w = FirstByte.done) : Bool

assemble₂

@[inline]

def ByteArray.utf8DecodeChar?.assemble₂Unchecked (w x : UInt8) : UInt32

@[inline]

def ByteArray.utf8DecodeChar?.assemble₂ (w x : UInt8) : Option Char

@[inline]

def ByteArray.utf8DecodeChar?.verify₂ (w x : UInt8) : Bool

assemble₃

@[inline]

def ByteArray.utf8DecodeChar?.assemble₃Unchecked (w x y : UInt8) : UInt32

@[inline]

def ByteArray.utf8DecodeChar?.assemble₃ (w x y : UInt8) : Option Char

@[inline]

def ByteArray.utf8DecodeChar?.verify₃ (w x y : UInt8) : Bool

assemble₄

@[inline]

def ByteArray.utf8DecodeChar?.assemble₄Unchecked (w x y z : UInt8) : UInt32

@[inline]

def ByteArray.utf8DecodeChar?.assemble₄ (w x y z : UInt8) : Option Char

@[inline]

def ByteArray.utf8DecodeChar?.verify₄ (w x y z : UInt8) : Bool

@[inline]

def ByteArray.utf8DecodeChar? (bytes : ByteArray) (i : Nat) : Option Char

Decodes and returns the Char whose UTF-8 encoding begins at i in bytes.

Returns none if i is not the start of a valid UTF-8 encoding of a character.

@[inline]

def ByteArray.validateUTF8At (bytes : ByteArray) (i : Nat) : Bool

utf8DecodeChar? low-level API

Main theorems

utf8DecodeChar?_utf8EncodeChar_append and toByteArray_of_utf8DecodeChar?_eq_some are the two main results that together imply that UTF-8 encoding and decoding are inverse.

theorem ByteArray.utf8DecodeChar?_utf8EncodeChar_append {b : ByteArray} {c : Char} : ((String.utf8EncodeChar c).toByteArray ++ b).utf8DecodeChar? 0 = some c

theorem String.toByteArray_utf8EncodeChar_of_utf8DecodeChar?_eq_some {b : ByteArray} {c : Char} (h : b.utf8DecodeChar? 0 = some c) : (utf8EncodeChar c).toByteArray = b.extract 0 c.utf8Size

theorem ByteArray.validateUTF8At_eq_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat} : b.validateUTF8At i = (b.utf8DecodeChar? i).isSome

Corollaries

theorem ByteArray.eq_of_utf8DecodeChar?_eq_some {b : ByteArray} {c : Char} (h : b.utf8DecodeChar? 0 = some c) : b = (String.utf8EncodeChar c).toByteArray ++ b.extract c.utf8Size b.size

theorem ByteArray.exists_of_utf8DecodeChar?_eq_some {b : ByteArray} {c : Char} (h : b.utf8DecodeChar? 0 = some c) : ∃ (l : ByteArray), b = (String.utf8EncodeChar c).toByteArray ++ l

theorem ByteArray.utf8DecodeChar?_eq_utf8DecodeChar?_extract {b : ByteArray} {i : Nat} : b.utf8DecodeChar? i = (b.extract i b.size).utf8DecodeChar? 0

theorem ByteArray.le_size_of_utf8DecodeChar?_eq_some {b : ByteArray} {i : Nat} {c : Char} (h : b.utf8DecodeChar? i = some c) : i + c.utf8Size ≤ b.size

theorem ByteArray.lt_size_of_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat} (h : (b.utf8DecodeChar? i).isSome = true) : i < b.size

theorem ByteArray.lt_size_of_validateUTF8At {b : ByteArray} {i : Nat} : b.validateUTF8At i = true → i < b.size

theorem ByteArray.utf8DecodeChar?_append_eq_some {b : ByteArray} {i : Nat} {c : Char} (h : b.utf8DecodeChar? i = some c) (b' : ByteArray) : (b ++ b').utf8DecodeChar? i = some c

theorem ByteArray.isSome_utf8DecodeChar?_append {b : ByteArray} {i : Nat} (h : (b.utf8DecodeChar? i).isSome = true) (b' : ByteArray) : ((b ++ b').utf8DecodeChar? i).isSome = true

@[inline]

def ByteArray.utf8DecodeChar (bytes : ByteArray) (i : Nat) (h : (bytes.utf8DecodeChar? i).isSome = true) : Char

Decodes and returns the Char whose UTF-8 encoding begins at i in bytes.

This function requires a proof that there is, in fact, a valid Char at i. utf8DecodeChar? is an alternative function that returns Option Char instead of requiring a proof ahead of time.

theorem ByteArray.add_utf8Size_utf8DecodeChar_le_size {b : ByteArray} {i : Nat} {h : (b.utf8DecodeChar? i).isSome = true} : i + (b.utf8DecodeChar i h).utf8Size ≤ b.size

theorem ByteArray.utf8DecodeChar_eq_utf8DecodeChar_extract {b : ByteArray} {i : Nat} {h : (b.utf8DecodeChar? i).isSome = true} : b.utf8DecodeChar i h = (b.extract i b.size).utf8DecodeChar 0 ⋯

theorem ByteArray.utf8DecodeChar_extract_congr {bytes : ByteArray} (i j j' : Nat) {h : ((bytes.extract i j).utf8DecodeChar? 0).isSome = true} {h' : ((bytes.extract i j').utf8DecodeChar? 0).isSome = true} : (bytes.extract i j).utf8DecodeChar 0 h = (bytes.extract i j').utf8DecodeChar 0 h'

theorem ByteArray.utf8EncodeChar_utf8DecodeChar {b : ByteArray} {i : Nat} {h : (b.utf8DecodeChar? i).isSome = true} : (String.utf8EncodeChar (b.utf8DecodeChar i h)).toByteArray = b.extract i (i + (b.utf8DecodeChar i h).utf8Size)

@[simp]

theorem List.utf8DecodeChar?_utf8Encode_singleton_append {b : ByteArray} {c : Char} : ([c].utf8Encode ++ b).utf8DecodeChar? 0 = some c

@[simp]

theorem List.utf8DecodeChar?_utf8Encode_singleton {c : Char} : [c].utf8Encode.utf8DecodeChar? 0 = some c

@[simp]

theorem List.utf8DecodeChar?_utf8Encode_cons {l : List Char} {c : Char} : (c :: l).utf8Encode.utf8DecodeChar? 0 = some c

@[simp]

theorem List.utf8DecodeChar_utf8Encode_cons {l : List Char} {c : Char} {h : ((c :: l).utf8Encode.utf8DecodeChar? 0).isSome = true} : (c :: l).utf8Encode.utf8DecodeChar 0 h = c

UInt8.IsUTF8FirstByte

def UInt8.IsUTF8FirstByte (c : UInt8) : Prop

Predicate for whether a byte can appear as the first byte of the UTF-8 encoding of a Unicode scalar value.

@[implicit_reducible, inline]

instance UInt8.instDecidableIsUTF8FirstByte {c : UInt8} : Decidable c.IsUTF8FirstByte

@[simp]

theorem UInt8.isUTF8FirstByte_getElem_utf8EncodeChar {c : Char} {i : Nat} {hi : i < (String.utf8EncodeChar c).length} : (String.utf8EncodeChar c)[i].IsUTF8FirstByte ↔ i = 0

theorem UInt8.isUTF8FirstByte_getElem_zero_utf8EncodeChar {c : Char} : (String.utf8EncodeChar c)[0].IsUTF8FirstByte

@[inline]

def UInt8.utf8ByteSize (c : UInt8) (_h : c.IsUTF8FirstByte) : Nat

theorem UInt8.utf8ByteSize_pos (c : UInt8) (h : c.IsUTF8FirstByte) : 0 < c.utf8ByteSize h

theorem ByteArray.isUTF8FirstByte_getElem_zero_utf8EncodeChar_append {c : Char} {b : ByteArray} : ((String.utf8EncodeChar c).toByteArray ++ b)[0].IsUTF8FirstByte

theorem ByteArray.isUTF8FirstByte_of_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat} (h : (b.utf8DecodeChar? i).isSome = true) : b[i].IsUTF8FirstByte

theorem ByteArray.isUTF8FirstByte_of_validateUTF8At {b : ByteArray} {i : Nat} (h : b.validateUTF8At i = true) : b[i].IsUTF8FirstByte

theorem ByteArray.utf8Size_utf8DecodeChar {b : ByteArray} {i : Nat} {h : (b.utf8DecodeChar? i).isSome = true} : (b.utf8DecodeChar i h).utf8Size = b[i].utf8ByteSize ⋯