# `Char.utf8Size` #

source
theorem Char.utf8Size_eq_one_iff {c : Char} :
c.utf8Size = 1 ↔ c.val ≤ 127
source
theorem Char.utf8Size_eq_two_iff {c : Char} :
c.utf8Size = 2 ↔ 127 < c.val ∧ c.val ≤ 2047
source
theorem Char.utf8Size_eq_three_iff {c : Char} :
c.utf8Size = 3 ↔ 2047 < c.val ∧ c.val ≤ 65535
source
theorem Char.utf8Size_eq_four_iff {c : Char} :
c.utf8Size = 4 ↔ 65535 < c.val
source
theorem Char.utf8Size_pos (c : Char) :
0 < c.utf8Size
source
theorem Char.utf8Size_le_four (c : Char) :
c.utf8Size ≤ 4
source
theorem Char.utf8Size_eq (c : Char) :
c.utf8Size = 1 ∨ c.utf8Size = 2 ∨ c.utf8Size = 3 ∨ c.utf8Size = 4

# `utf8EncodeChar` #

## `utf8EncodeChar` low-level API #

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

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

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[csimp]
theorem String.utf8EncodeChar_eq_utf8EncodeCharFast :
utf8EncodeChar = utf8EncodeCharFast
source
@[simp]
theorem String.length_utf8EncodeChar (c : Char) :
(utf8EncodeChar c).length = c.utf8Size
source
theorem String.utf8EncodeChar_eq_singleton {c : Char} :
c.utf8Size = 1 → utf8EncodeChar c = [c.val.toUInt8]
source
theorem String.utf8EncodeChar_eq_cons_cons {c : Char} :
c.utf8Size = 2 → utf8EncodeChar c = [(c.val >>> 6).toUInt8 &&& 31 ||| 192, c.val.toUInt8 &&& 63 ||| 128]
source
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]
source
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 #

source
inductive ByteArray.utf8DecodeChar?.FirstByte :
Type

- invalid : FirstByte
- done : FirstByte
- oneMore : FirstByte
- twoMore : FirstByte
- threeMore : FirstByte

Instances For

source
@[inline]
def ByteArray.utf8DecodeChar?.parseFirstByte (b : UInt8) :
FirstByte
Equations

- One or more equations did not get rendered due to their size.

Instances For

## `parseFirstByte` low-level API #

## `parseFirstByte` BitVec API #

### Size one #

### Size two #

### Size three #

### Size four #

# `isInvalidContinuationByte` definition & API #

source
@[inline]
def ByteArray.utf8DecodeChar?.isInvalidContinuationByte (b : UInt8) :
Bool
Equations

- ByteArray.utf8DecodeChar?.isInvalidContinuationByte b = (b &&& 192 != 128)

Instances For

# `parseFirstByte`, `isInvalidContinuationByte` and `utf8EncodeChar` #

# `assemble₁` #

source
@[inline]
def ByteArray.utf8DecodeChar?.assemble₁ (w : UInt8) (h : parseFirstByte w = FirstByte.done) :
Option Char
Equations

- ByteArray.utf8DecodeChar?.assemble₁ w h = some { val := w.toUInt32, valid := ⋯ }

Instances For

source
@[inline]
def ByteArray.utf8DecodeChar?.verify₁ {w : UInt8} (_w : UInt8) (_h : parseFirstByte w = FirstByte.done) :
Bool
Equations

- ByteArray.utf8DecodeChar?.verify₁ _w _h = true

Instances For

# `assemble₂` #

source
@[inline]
def ByteArray.utf8DecodeChar?.assemble₂Unchecked (w x : UInt8) :
UInt32
Equations

- ByteArray.utf8DecodeChar?.assemble₂Unchecked w x = (w &&& 31).toUInt32 <<< 6 ||| (x &&& 63).toUInt32

Instances For

source
@[inline]
def ByteArray.utf8DecodeChar?.assemble₂ (w x : UInt8) :
Option Char
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[inline]
def ByteArray.utf8DecodeChar?.verify₂ (w x : UInt8) :
Bool
Equations

- One or more equations did not get rendered due to their size.

Instances For

# `assemble₃` #

source
@[inline]
def ByteArray.utf8DecodeChar?.assemble₃Unchecked (w x y : UInt8) :
UInt32
Equations

- ByteArray.utf8DecodeChar?.assemble₃Unchecked w x y = (w &&& 15).toUInt32 <<< 12 ||| (x &&& 63).toUInt32 <<< 6 ||| (y &&& 63).toUInt32

Instances For

source
@[inline]
def ByteArray.utf8DecodeChar?.assemble₃ (w x y : UInt8) :
Option Char
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[inline]
def ByteArray.utf8DecodeChar?.verify₃ (w x y : UInt8) :
Bool
Equations

- One or more equations did not get rendered due to their size.

Instances For

# `assemble₄` #

source
@[inline]
def ByteArray.utf8DecodeChar?.assemble₄Unchecked (w x y z : UInt8) :
UInt32
Equations

- ByteArray.utf8DecodeChar?.assemble₄Unchecked w x y z = (w &&& 7).toUInt32 <<< 18 ||| (x &&& 63).toUInt32 <<< 12 ||| (y &&& 63).toUInt32 <<< 6 ||| (z &&& 63).toUInt32

Instances For

source
@[inline]
def ByteArray.utf8DecodeChar?.assemble₄ (w x y z : UInt8) :
Option Char
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[inline]
def ByteArray.utf8DecodeChar?.verify₄ (w x y z : UInt8) :
Bool
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[inline]
def ByteArray.validateUTF8At (bytes : ByteArray) (i : Nat) :
Bool
Equations

- One or more equations did not get rendered due to their size.

Instances For

# `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.

source
theorem ByteArray.utf8DecodeChar?_utf8EncodeChar_append {b : ByteArray} {c : Char} :
((String.utf8EncodeChar c).toByteArray ++ b).utf8DecodeChar? 0 = some c
source
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
source
theorem ByteArray.validateUTF8At_eq_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat} :
b.validateUTF8At i = (b.utf8DecodeChar? i).isSome

# Corollaries #

source
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
source
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
source
theorem ByteArray.utf8DecodeChar?_eq_utf8DecodeChar?_extract {b : ByteArray} {i : Nat} :
b.utf8DecodeChar? i = (b.extract i b.size).utf8DecodeChar? 0
source
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
source
theorem ByteArray.lt_size_of_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat} (h : (b.utf8DecodeChar? i).isSome = true) :
i < b.size
source
theorem ByteArray.lt_size_of_validateUTF8At {b : ByteArray} {i : Nat} :
b.validateUTF8At i = true → i < b.size
source
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
source
theorem ByteArray.isSome_utf8DecodeChar?_append {b : ByteArray} {i : Nat} (h : (b.utf8DecodeChar? i).isSome = true) (b' : ByteArray) :
((b ++ b').utf8DecodeChar? i).isSome = true
source
@[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.

Equations

- bytes.utf8DecodeChar i h = (bytes.utf8DecodeChar? i).get h

Instances For

source
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
source
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 ⋯
source
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'
source
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)
source
@[simp]
theorem List.utf8DecodeChar?_utf8Encode_singleton_append {b : ByteArray} {c : Char} :
([c].utf8Encode ++ b).utf8DecodeChar? 0 = some c
source
@[simp]
theorem List.utf8DecodeChar?_utf8Encode_singleton {c : Char} :
[c].utf8Encode.utf8DecodeChar? 0 = some c
source
@[simp]
theorem List.utf8DecodeChar?_utf8Encode_cons {l : List Char} {c : Char} :
(c :: l).utf8Encode.utf8DecodeChar? 0 = some c
source
@[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` #

source
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.

Equations

- c.IsUTF8FirstByte = (c &&& 128 = 0 ∨ c &&& 224 = 192 ∨ c &&& 240 = 224 ∨ c &&& 248 = 240)

Instances For

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

- UInt8.instDecidableIsUTF8FirstByte = inferInstanceAs (Decidable (c &&& 128 = 0 ∨ c &&& 224 = 192 ∨ c &&& 240 = 224 ∨ c &&& 248 = 240))

source
@[simp]
theorem UInt8.isUTF8FirstByte_getElem_utf8EncodeChar {c : Char} {i : Nat} {hi : i < (String.utf8EncodeChar c).length} :
(String.utf8EncodeChar c)[i].IsUTF8FirstByte ↔ i = 0
source
theorem UInt8.isUTF8FirstByte_getElem_zero_utf8EncodeChar {c : Char} :
(String.utf8EncodeChar c)[0].IsUTF8FirstByte
source
def UInt8.utf8ByteSize (c : UInt8) (_h : c.IsUTF8FirstByte) :
Nat
Equations

- c.utf8ByteSize _h = if c &&& 128 = 0 then 1 else if c &&& 224 = 192 then 2 else if c &&& 240 = 224 then 3 else 4

Instances For

source
theorem ByteArray.isUTF8FirstByte_getElem_zero_utf8EncodeChar_append {c : Char} {b : ByteArray} :
((String.utf8EncodeChar c).toByteArray ++ b)[0].IsUTF8FirstByte
source
theorem ByteArray.isUTF8FirstByte_of_isSome_utf8DecodeChar? {b : ByteArray} {i : Nat} (h : (b.utf8DecodeChar? i).isSome = true) :
b[i].IsUTF8FirstByte
source
theorem ByteArray.isUTF8FirstByte_of_validateUTF8At {b : ByteArray} {i : Nat} (h : b.validateUTF8At i = true) :
b[i].IsUTF8FirstByte
source
theorem ByteArray.utf8Size_utf8DecodeChar {b : ByteArray} {i : Nat} {h : (b.utf8DecodeChar? i).isSome = true} :
(b.utf8DecodeChar i h).utf8Size = b[i].utf8ByteSize ⋯