vstd/
utf8.rs

1//! Definitions for UTF-8 encoding and decoding of character sequences.
2//!
3//! [UTF-8](https://en.wikipedia.org/wiki/UTF-8) is a variable-width character encoding scheme.
4//! Each character is encoded with between 1 and 4 bytes.
5//! Specifications for encoding and decoding characters to their UTF-8 byte sequences are given by [`encode_utf8`] and [`decode_utf8`], respectively.
6//! Characters in the ASCII character set are encoded in UTF-8 with 1-byte encodings identical to those used by ASCII.
7//! Thus, some UTF-8 byte sequences can also be considered ASCII byte sequences, as defined in [`is_ascii_chars`].
8//!
9//! UTF-8 encodes numerical values called Unicode _scalars_ (see below), which assign a unique value to each Unicode character.
10//! A scalar value is encoded in UTF-8 using a leading byte and between 0 and 3 continuation bytes, where larger scalar values require more continuation bytes.
11//! The first part of the bit pattern in the leading byte is reserved for describing the number of bytes in the scalar's encoding (e.g., [`is_leading_byte_width_1`]).
12//! The rest of the leading byte contains data bits corresponding to the scalar's value (e.g., [`leading_bits_width_1`]).
13//! The continuation bytes also follow a specific bit pattern ([`is_continuation_byte`]) and contain the remainder of the data bits ([`continuation_bits`]).
14//!
15//! This module makes use of terminology from the [Unicode standard](https://www.unicode.org/glossary/).
16//! A Unicode _scalar_ is a numerical value (represented in this module as a `u32`) corresponding to a character that can be encoded in UTF-8.
17//! All Rust `char`s correspond to Unicode scalars ([`char_is_scalar`]),
18//! and every numerical value encoded in a UTF-8 byte sequence must fall within the range defined for Unicode scalars ([`is_scalar`]).
19//! The Unicode standard also defines a _codepoint_ to be a numerical value which falls in the range available for encoding characters in UTF-8.
20//! This may sound similar to the definition of scalar.
21//! However, the definition of codepoint is more permissive than that for scalars,
22//! as it includes some values which are technically possible to encode in the UTF-8 scheme,
23//! but in fact are not legal Unicode values
24//! (namely, the [high-surrogate and low-surrogate ranges](https://en.wikipedia.org/wiki/UTF-8#Surrogates)).
25//! To align with the Unicode terminology, in this module, we use the term "scalar" to describe the numerical values
26//! which can be encoded in valid UTF-8 byte sequences, and the term "codepoint" to describe numerical values which
27//! are learned upon decoding a byte sequence but may or may not be legal Unicode values.
28use super::prelude::*;
29use super::seq::*;
30
31use verus as verus_skip_verusfmt; // verusfmt doesn't handle s[..e] yet
32verus_skip_verusfmt! {
33
34broadcast use super::seq::group_seq_lemmas;
35/* Decoding UTF-8 to chars */
36
37/// True when the given byte conforms to the bit pattern for the first byte of a 1-byte UTF-8 encoding of a single codepoint.
38/// The byte must have the form 0xxxxxxx.
39pub open spec fn is_leading_byte_width_1(byte: u8) -> bool {
40    0x00 <= byte <= 0x7f
41}
42
43/// True when the given byte conforms to the bit pattern for the first byte of a 2-byte UTF-8 encoding of a single codepoint.
44/// The byte must have the form 110xxxxx.
45pub open spec fn is_leading_byte_width_2(byte: u8) -> bool {
46    0xc0 <= byte <= 0xdf
47}
48
49/// True when the given byte conforms to the bit pattern for the first byte of a 3-byte UTF-8 encoding of a single codepoint.
50/// The byte must have the form 1110xxxx.
51pub open spec fn is_leading_byte_width_3(byte: u8) -> bool {
52    0xe0 <= byte <= 0xef
53}
54
55/// True when the given byte conforms to the bit pattern for the first byte of a 4-byte UTF-8 encoding of a single codepoint.
56/// The byte must have the form 11110xxx.
57pub open spec fn is_leading_byte_width_4(byte: u8) -> bool {
58    0xf0 <= byte <= 0xf7
59}
60
61/// True when the given byte conforms to the bit pattern for a continuation byte of a UTF-8 encoding of a single codepoint.
62/// The byte must have the form 10xxxxxx.
63pub open spec fn is_continuation_byte(byte: u8) -> bool {
64    0x80 <= byte <= 0xbf
65}
66
67/// Value of the 6 data bits from the given continuation byte, assuming that it is a valid continuation byte for a UTF-8 encoding.
68pub open spec fn continuation_bits(byte: u8) -> u32
69    recommends
70        is_continuation_byte(byte),
71{
72    // 0x3f = 0011 1111
73    (byte & 0x3f) as u32
74}
75
76/// Value of the 7 data bits from the given byte, assuming that it is a valid leading byte for a 1-byte UTF-8 encoding.
77pub open spec fn leading_bits_width_1(byte: u8) -> u32
78    recommends
79        is_leading_byte_width_1(byte),
80{
81    // 0x7f = 0111 1111
82    (byte & 0x7F) as u32
83}
84
85/// Value of the 5 data bits from the given byte, assuming that it is a valid leading byte for a 2-byte UTF-8 encoding.
86pub open spec fn leading_bits_width_2(byte: u8) -> u32
87    recommends
88        is_leading_byte_width_2(byte),
89{
90    // 0x1f = 0001 1111
91    (byte & 0x1F) as u32
92}
93
94/// Value of the 4 data bits from the given byte, assuming that it is a valid leading byte for a 3-byte UTF-8 encoding.
95pub open spec fn leading_bits_width_3(byte: u8) -> u32
96    recommends
97        is_leading_byte_width_3(byte),
98{
99    // 0x0f = 0000 1111
100    (byte & 0x0F) as u32
101}
102
103/// Value of the 3 data bits from the given byte, assuming that it is a valid leading byte for a 4-byte UTF-8 encoding.
104pub open spec fn leading_bits_width_4(byte: u8) -> u32
105    recommends
106        is_leading_byte_width_4(byte),
107{
108    // 0x07 = 0000 0111
109    (byte & 0x07) as u32
110}
111
112/// The codepoint encoded by the given byte, assuming that it is a valid leading byte for a 1-byte UTF-8 encoding.
113pub open spec fn codepoint_width_1(byte1: u8) -> u32
114    recommends
115        is_leading_byte_width_1(byte1),
116{
117    leading_bits_width_1(byte1)
118}
119
120// 0xc1 = 1100 0001
121// 0xc1 & 0x1f = 0x01
122// 0x01 << 6 = 0100 0000 = 0x40
123// If byte2 = 0xff then byte2 & 0x3f = 0x3f = 0011 1111
124// so highest possible is 0111 1111 = 0x7f < 0x80
125/// The codepoint encoded by the given 2 bytes, assuming that they are a valid leading and continuation byte, respectively, for 2-byte UTF-8 encoding.
126pub open spec fn codepoint_width_2(byte1: u8, byte2: u8) -> u32
127    recommends
128        is_leading_byte_width_2(byte1),
129        is_continuation_byte(byte2),
130{
131    (leading_bits_width_2(byte1) << 6) | continuation_bits(byte2)
132}
133
134/// The codepoint encoded by the given 3 bytes, assuming that they are a valid leading and continuation bytes, respectively, for 3-byte UTF-8 encoding.
135pub open spec fn codepoint_width_3(byte1: u8, byte2: u8, byte3: u8) -> u32
136    recommends
137        is_leading_byte_width_3(byte1),
138        is_continuation_byte(byte2),
139        is_continuation_byte(byte3),
140{
141    (leading_bits_width_3(byte1) << 12) | (continuation_bits(byte2) << 6) | continuation_bits(byte3)
142}
143
144// 0xf7 = 1111 0111
145// 0xf7 & 0x07 = 0x07
146// 0x07 << 18 = 0001 1100 0000 0000 0000 0000 = 0x1c0000
147// 0xf5 = 1111 0101
148// 0xf5 & 0x07 = 0x05
149// 0x05 << 18 = 0001 0100 0000 0000 0000 0000 = 0x140000
150/// The codepoint encoded by the given 4 bytes, assuming that they are a valid leading and continuation bytes, respectively, for 4-byte UTF-8 encoding.
151pub open spec fn codepoint_width_4(byte1: u8, byte2: u8, byte3: u8, byte4: u8) -> u32
152    recommends
153        is_leading_byte_width_4(byte1),
154        is_continuation_byte(byte2),
155        is_continuation_byte(byte3),
156        is_continuation_byte(byte4),
157{
158    (leading_bits_width_4(byte1) << 18) | (continuation_bits(byte2) << 12) | (continuation_bits(
159        byte3,
160    ) << 6) | continuation_bits(byte4)
161}
162
163/// True when the given byte sequence begins with a well-formed leading byte and an appropriate number of well-formed continuation bytes for a UTF-8 encoding of a single codepoint.
164pub open spec fn valid_leading_and_continuation_bytes_first_codepoint(bytes: Seq<u8>) -> bool {
165    ||| (bytes.len() >= 1 && is_leading_byte_width_1(bytes[0]))
166    ||| (bytes.len() >= 2 && is_leading_byte_width_2(bytes[0]) && is_continuation_byte(bytes[1]))
167    ||| (bytes.len() >= 3 && is_leading_byte_width_3(bytes[0]) && is_continuation_byte(bytes[1])
168        && is_continuation_byte(bytes[2]))
169    ||| (bytes.len() >= 4 && is_leading_byte_width_4(bytes[0]) && is_continuation_byte(bytes[1])
170        && is_continuation_byte(bytes[2]) && is_continuation_byte(bytes[3]))
171}
172
173/// Returns the first codepoint encoded in UTF-8 in the given byte sequence, assuming that the sequence begins with a well-formed leading byte and an appropriate number of well-formed continuation bytes.
174pub open spec fn decode_first_codepoint(bytes: Seq<u8>) -> u32
175    recommends
176        valid_leading_and_continuation_bytes_first_codepoint(bytes),
177{
178    if is_leading_byte_width_1(bytes[0]) {
179        codepoint_width_1(bytes[0])
180    } else if is_leading_byte_width_2(bytes[0]) {
181        codepoint_width_2(bytes[0], bytes[1])
182    } else if is_leading_byte_width_3(bytes[0]) {
183        codepoint_width_3(bytes[0], bytes[1], bytes[2])
184    } else {
185        codepoint_width_4(bytes[0], bytes[1], bytes[2], bytes[3])
186    }
187}
188
189/// The length in bytes of the first codepoint encoded in UTF-8 in the given byte sequence, assuming that the sequence begins with a well-formed leading byte and an appropriate number of well-formed continuation bytes.
190pub open spec fn length_of_first_codepoint(bytes: Seq<u8>) -> int
191    recommends
192        valid_leading_and_continuation_bytes_first_codepoint(bytes),
193{
194    if is_leading_byte_width_1(bytes[0]) {
195        1
196    } else if is_leading_byte_width_2(bytes[0]) {
197        2
198    } else if is_leading_byte_width_3(bytes[0]) {
199        3
200    } else {
201        4
202    }
203}
204
205/// True when the given codepoint, when encoded in UTF-8 using `len` number of bytes, would not be an "overlong encoding".
206/// An overlong encoding is one that uses more bytes than needed to encode the given value.
207pub open spec fn not_overlong_encoding(codepoint: u32, len: int) -> bool {
208    &&& (len == 2 ==> 0x80 <= codepoint)
209    &&& (len == 3 ==> 0x800 <= codepoint)
210    &&& (len == 4 ==> 0x10000 <= codepoint <= 0x10ffff)
211}
212
213/// True when the given codepoint does not fall into the "surrogate range" of the Unicode standard.
214/// The surrogate range contains values which are technically possible to encode in UTF-8 but are not valid Unicode scalars.
215pub open spec fn not_surrogate(codepoint: u32) -> bool {
216    !(0xD800 <= codepoint <= 0xDFFF)
217}
218
219/// True when the given byte sequence begins with a well-formed UTF-8 encoding of a single scalar.
220/// To be a well-formed encoding, the bytes must: follow the expected bit pattern for leading and continuation bytes
221/// for a single scalar encoding, not be an "overlong encoding", and not fall in the surrogate range.
222pub open spec fn valid_first_scalar(bytes: Seq<u8>) -> bool {
223    &&& valid_leading_and_continuation_bytes_first_codepoint(bytes)
224    &&& not_overlong_encoding(decode_first_codepoint(bytes), length_of_first_codepoint(bytes))
225    &&& not_surrogate(decode_first_codepoint(bytes))
226}
227
228/// The first scalar encoded in UTF-8 in the given byte sequence, assuming that the sequence begins with a well-formed encoding of a single scalar.
229pub open spec fn decode_first_scalar(bytes: Seq<u8>) -> u32
230    recommends
231        valid_first_scalar(bytes),
232{
233    decode_first_codepoint(bytes)
234}
235
236/// The length in bytes of first scalar encoded in UTF-8 in the given byte sequence, assuming that the sequence begins with a well-formed encoding of a single scalar.
237pub open spec fn length_of_first_scalar(bytes: Seq<u8>) -> int
238    recommends
239        valid_first_scalar(bytes),
240{
241    length_of_first_codepoint(bytes)
242}
243
244/// Removes the first scalar encoded in UTF-8 in the given byte sequence and returns the rest of the sequence, assuming that the sequence begins with a well-formed encoding of a single scalar.
245pub open spec fn pop_first_scalar(bytes: Seq<u8>) -> Seq<u8>
246    recommends
247        valid_first_scalar(bytes),
248{
249    bytes[length_of_first_scalar(bytes)..]
250}
251
252proof fn lemma_pop_first_scalar_decreases(bytes: Seq<u8>)
253    requires
254        valid_first_scalar(bytes),
255    ensures
256        pop_first_scalar(bytes).len() < bytes.len(),
257{
258    assert(length_of_first_scalar(bytes) <= bytes.len() as int);
259    assert(pop_first_scalar(bytes).len() == bytes.len() as int - length_of_first_scalar(bytes)) by {
260        lemma_seq_subrange_len(bytes, length_of_first_scalar(bytes), bytes.len() as int)
261    };
262}
263
264/// Takes the bytes corresponding to the first scalar encoded in UTF-8 in the given byte sequence, assuming that the sequence begins with a well-formed encoding of a single scalar.
265pub open spec fn take_first_scalar(bytes: Seq<u8>) -> Seq<u8>
266    recommends
267        valid_first_scalar(bytes),
268{
269    bytes[..length_of_first_scalar(bytes)]
270}
271
272/// True when the given bytes form a valid UTF-8 encoding.
273pub open spec fn valid_utf8(bytes: Seq<u8>) -> bool
274    decreases bytes.len(),
275{
276    bytes.len() != 0 ==> valid_first_scalar(bytes) && valid_utf8(pop_first_scalar(bytes))
277}
278
279/// The sequence of characters encoded as Unicode scalars in the given bytes, assuming that the bytes form a valid UTF-8 encoding.
280pub open spec fn decode_utf8(bytes: Seq<u8>) -> Seq<char>
281    recommends
282        valid_utf8(bytes),
283    decreases bytes.len(),
284    when valid_utf8(bytes)
285{
286    if bytes.len() == 0 {
287        seq![]
288    } else {
289        seq![decode_first_scalar(bytes) as char] + decode_utf8(pop_first_scalar(bytes))
290    }
291}
292
293/// The length in bytes of the last scalar encoded in UTF-8 in the given byte sequence, assuming that the bytes form a valid UTF-8 encoding.
294pub open spec fn length_of_last_scalar(bytes: Seq<u8>) -> int
295    recommends
296        valid_utf8(bytes),
297        bytes.len() > 0,
298{
299    let n = bytes.len() as int;
300    if !is_continuation_byte(bytes[n - 1]) {
301        1
302    } else if !is_continuation_byte(bytes[n - 2]) {
303        2
304    } else if !is_continuation_byte(bytes[n - 3]) {
305        3
306    } else {
307        4
308    }
309}
310
311/// Takes the bytes corresponding to the last scalar encoded in UTF-8 in the given byte sequence, assuming that the bytes form a valid UTF-8 encoding.
312pub open spec fn take_last_scalar(bytes: Seq<u8>) -> Seq<u8>
313    recommends
314        valid_utf8(bytes),
315        bytes.len() > 0,
316{
317    let len = length_of_last_scalar(bytes);
318    bytes[bytes.len() - len..]
319}
320
321/// The last scalar encoded in UTF-8 in the given byte sequence, assuming that the bytes form a valid UTF-8 encoding.
322pub open spec fn decode_last_scalar(bytes: Seq<u8>) -> u32
323    recommends
324        valid_utf8(bytes),
325        bytes.len() > 0,
326{
327    let n = bytes.len() as int;
328    if !is_continuation_byte(bytes[n - 1]) {
329        codepoint_width_1(bytes[n - 1])
330    } else if !is_continuation_byte(bytes[n - 2]) {
331        codepoint_width_2(bytes[n - 2], bytes[n - 1])
332    } else if !is_continuation_byte(bytes[n - 3]) {
333        codepoint_width_3(bytes[n - 3], bytes[n - 2], bytes[n - 1])
334    } else {
335        codepoint_width_4(bytes[n - 4], bytes[n - 3], bytes[n - 2], bytes[n - 1])
336    }
337}
338
339/* Encoding chars as UTF-8 */
340
341/// True when the given value is a Unicode scalar with a 1-byte UTF-8 encoding.
342pub open spec fn has_width_1_encoding(v: u32) -> bool {
343    0 <= v <= 0x7F
344}
345
346/// True when the given value is a Unicode scalar with a 2-byte UTF-8 encoding.
347pub open spec fn has_width_2_encoding(v: u32) -> bool {
348    0x80 <= v <= 0x7FF
349}
350
351/// True when the given value is a Unicode scalar with a 3-byte UTF-8 encoding.
352pub open spec fn has_width_3_encoding(v: u32) -> bool {
353    0x800 <= v <= 0xFFFF && !(0xD800 <= v <= 0xDFFF)
354}
355
356/// True when the given value is a Unicode scalar with a 4-byte UTF-8 encoding.
357pub open spec fn has_width_4_encoding(v: u32) -> bool {
358    0x10000 <= v <= 0x10FFFF
359}
360
361/// True when the given `u32` represents a Unicode scalar, i.e., a value that can be encoded in UTF-8.
362/// This definition is equivalent to: `0 <= v <= 0x10ffff && !(0xD800 <= v <= 0xDFFF)`.
363pub open spec fn is_scalar(v: u32) -> bool {
364    ||| has_width_1_encoding(v)
365    ||| has_width_2_encoding(v)
366    ||| has_width_3_encoding(v)
367    ||| has_width_4_encoding(v)
368}
369
370/// The first (and only) byte of the UTF-8 encoding of the given scalar value, assuming that the scalar has a 1-byte UTF-8 encoding.
371pub open spec fn leading_byte_width_1(scalar: u32) -> u8
372    recommends
373        has_width_1_encoding(scalar),
374{
375    (scalar & 0x7F) as u8
376}
377
378/// The first byte of the UTF-8 encoding of the given scalar value, assuming that the scalar has a 2-byte UTF-8 encoding.
379pub open spec fn leading_byte_width_2(scalar: u32) -> u8
380    recommends
381        has_width_2_encoding(scalar),
382{
383    0xC0 | ((scalar >> 6) & 0x1F) as u8
384}
385
386/// The first byte of the UTF-8 encoding of the given scalar value, assuming that the scalar has a 3-byte UTF-8 encoding.
387pub open spec fn leading_byte_width_3(scalar: u32) -> u8
388    recommends
389        has_width_3_encoding(scalar),
390{
391    0xE0 | ((scalar >> 12) & 0x0F) as u8
392}
393
394/// The first byte of the UTF-8 encoding of the given scalar value, assuming that the scalar has a 4-byte UTF-8 encoding.
395pub open spec fn leading_byte_width_4(scalar: u32) -> u8
396    recommends
397        has_width_4_encoding(scalar),
398{
399    0xF0 | ((scalar >> 18) & 0x7) as u8
400}
401
402/// The last continuation byte of the UTF-8 encoding of the given scalar value, assuming that the scalar has a 2, 3, or 4-byte UTF-8 encoding.
403pub open spec fn last_continuation_byte(scalar: u32) -> u8
404    recommends
405        has_width_2_encoding(scalar) || has_width_3_encoding(scalar) || has_width_4_encoding(
406            scalar,
407        ),
408{
409    0x80 | (scalar & 0x3F) as u8
410}
411
412/// The second-to-last continuation byte of the UTF-8 encoding of the given scalar value, assuming that the scalar has a 3 or 4-byte UTF-8 encoding.
413pub open spec fn second_last_continuation_byte(scalar: u32) -> u8
414    recommends
415        has_width_3_encoding(scalar) || has_width_4_encoding(scalar),
416{
417    0x80 | ((scalar >> 6) & 0x3F) as u8
418}
419
420/// The third-to-last continuation byte of the UTF-8 encoding of the given scalar value, assuming that the scalar has a 4-byte UTF-8 encoding.
421pub open spec fn third_last_continuation_byte(scalar: u32) -> u8
422    recommends
423        has_width_4_encoding(scalar),
424{
425    0x80 | ((scalar >> 12) & 0x3F) as u8
426}
427
428/// The UTF-8 encoding of the given value, assuming that it is a Unicode scalar.
429pub open spec fn encode_scalar(scalar: u32) -> Seq<u8>
430    recommends
431        is_scalar(scalar),
432{
433    if has_width_1_encoding(scalar) {
434        seq![leading_byte_width_1(scalar)]
435    } else if has_width_2_encoding(scalar) {
436        seq![leading_byte_width_2(scalar), last_continuation_byte(scalar)]
437    } else if has_width_3_encoding(scalar) {
438        seq![
439            leading_byte_width_3(scalar),
440            second_last_continuation_byte(scalar),
441            last_continuation_byte(scalar),
442        ]
443    } else {
444        seq![
445            leading_byte_width_4(scalar),
446            third_last_continuation_byte(scalar),
447            second_last_continuation_byte(scalar),
448            last_continuation_byte(scalar),
449        ]
450    }
451}
452
453/// The UTF-8 encoding of the given `char` sequence.
454pub open spec fn encode_utf8(chars: Seq<char>) -> Seq<u8>
455    decreases chars.len(),
456{
457    if chars.len() == 0 {
458        seq![]
459    } else {
460        encode_scalar(chars[0] as u32) + encode_utf8(chars.drop_first())
461    }
462}
463
464// See `vstd::std_specs::char` for the `char::len_utf8`/`char::is_whitespace`
465// `assume_specification`s that relate this module's model to those real
466// std-library methods.
467/// [`encode_utf8`] distributes over sequence concatenation.
468pub broadcast proof fn encode_utf8_concat(a: Seq<char>, b: Seq<char>)
469    ensures
470        #[trigger] encode_utf8(a + b) == encode_utf8(a) + encode_utf8(b),
471    decreases a.len(),
472{
473    if a.len() == 0 {
474        assert(a + b =~= b);
475    } else {
476        assert((a + b).drop_first() =~= a.drop_first() + b);
477        encode_utf8_concat(a.drop_first(), b);
478        assert(encode_scalar(a[0] as u32) + (encode_utf8(a.drop_first()) + encode_utf8(b)) =~= (
479        encode_scalar(a[0] as u32) + encode_utf8(a.drop_first())) + encode_utf8(b));
480    }
481}
482
483/// Specialization of [`encode_utf8_concat`] for appending one `char`.
484pub broadcast proof fn encode_utf8_push(chars: Seq<char>, c: char)
485    ensures
486        #[trigger] encode_utf8(chars.push(c)) == encode_utf8(chars) + encode_scalar(c as u32),
487{
488    assert(chars.push(c) =~= chars + seq![c]);
489    encode_utf8_concat(chars, seq![c]);
490    assert(seq![c].drop_first() =~= Seq::<char>::empty());
491    assert(encode_utf8(seq![c]) =~= encode_scalar(c as u32) + encode_utf8(Seq::<char>::empty()));
492}
493
494/// Growing a prefix by at least one `char` strictly increases its encoded
495/// byte length.
496pub proof fn lemma_encode_utf8_len_strictly_monotonic(s: Seq<char>, i: int, j: int)
497    requires
498        0 <= i < j <= s.len(),
499    ensures
500        encode_utf8(s[..i]).len() < encode_utf8(s[..j]).len(),
501{
502    assert(s[0..i] + s[i..j] =~= s[..j]);
503    encode_utf8_concat(s[..i], s[i..j]);
504    assert(s[i..j].len() == j - i);
505}
506
507/* Correspondence between encode_utf8 and decode_utf8 definitions */
508
509// Performing encode followed by decode on a scalar with a 1-byte UTF-8 encoding results in the same value.
510proof fn encode_decode_width_1(c: u32)
511    by (bit_vector)
512    requires
513        has_width_1_encoding(c),
514    ensures
515        ({
516            let b1 = leading_byte_width_1(c);
517            &&& is_leading_byte_width_1(b1)
518            &&& codepoint_width_1(b1) == c
519        }),
520{
521}
522
523// Performing decode followed by encode on a 1-byte UTF-8 encoding results in the same byte.
524proof fn decode_encode_width_1(b1: u8)
525    by (bit_vector)
526    requires
527        is_leading_byte_width_1(b1),
528    ensures
529        ({
530            let c = codepoint_width_1(b1);
531            &&& has_width_1_encoding(c)
532            &&& leading_byte_width_1(c) == b1
533        }),
534{
535}
536
537// Performing encode followed by decode on a scalar with a 2-byte UTF-8 encoding  results in the same value.
538proof fn encode_decode_width_2(c: u32)
539    by (bit_vector)
540    requires
541        has_width_2_encoding(c),
542    ensures
543        ({
544            let b1 = leading_byte_width_2(c);
545            let b2 = last_continuation_byte(c);
546            &&& is_leading_byte_width_2(b1)
547            &&& is_continuation_byte(b2)
548            &&& codepoint_width_2(b1, b2) == c
549        }),
550{
551}
552
553// Performing decode followed by encode on a 2-byte UTF-8 encoding results in the same bytes.
554proof fn decode_encode_width_2(b1: u8, b2: u8)
555    by (bit_vector)
556    requires
557        is_leading_byte_width_2(b1),
558        is_continuation_byte(b2),
559        not_overlong_encoding(codepoint_width_2(b1, b2), 2),
560    ensures
561        ({
562            let c = codepoint_width_2(b1, b2);
563            &&& has_width_2_encoding(c)
564            &&& leading_byte_width_2(c) == b1
565            &&& last_continuation_byte(c) == b2
566        }),
567{
568}
569
570// Performing encode followed by decode on a scalar with a 3-byte UTF-8 encoding  results in the same value.
571proof fn encode_decode_width_3(c: u32)
572    by (bit_vector)
573    requires
574        has_width_3_encoding(c),
575    ensures
576        ({
577            let b1 = leading_byte_width_3(c);
578            let b2 = second_last_continuation_byte(c);
579            let b3 = last_continuation_byte(c);
580            &&& is_leading_byte_width_3(b1)
581            &&& is_continuation_byte(b2)
582            &&& is_continuation_byte(b3)
583            &&& codepoint_width_3(b1, b2, b3) == c
584        }),
585{
586}
587
588// Performing decode followed by encode on a 3-byte UTF-8 encoding results in the same bytes.
589proof fn decode_encode_width_3(b1: u8, b2: u8, b3: u8)
590    by (bit_vector)
591    requires
592        is_leading_byte_width_3(b1),
593        is_continuation_byte(b2),
594        is_continuation_byte(b3),
595        not_overlong_encoding(codepoint_width_3(b1, b2, b3), 3),
596        not_surrogate(codepoint_width_3(b1, b2, b3)),
597    ensures
598        ({
599            let c = codepoint_width_3(b1, b2, b3);
600            &&& has_width_3_encoding(c)
601            &&& leading_byte_width_3(c) == b1
602            &&& second_last_continuation_byte(c) == b2
603            &&& last_continuation_byte(c) == b3
604        }),
605{
606}
607
608// Performing encode followed by decode on a scalar with a 4-byte UTF-8 encoding results in the same value.
609proof fn encode_decode_width_4(c: u32)
610    by (bit_vector)
611    requires
612        has_width_4_encoding(c),
613    ensures
614        ({
615            let b1 = leading_byte_width_4(c);
616            let b2 = third_last_continuation_byte(c);
617            let b3 = second_last_continuation_byte(c);
618            let b4 = last_continuation_byte(c);
619            &&& is_leading_byte_width_4(b1)
620            &&& is_continuation_byte(b2)
621            &&& is_continuation_byte(b3)
622            &&& is_continuation_byte(b4)
623            &&& codepoint_width_4(b1, b2, b3, b4) == c
624        }),
625{
626}
627
628// Performing decode followed by encode on a 4-byte UTF-8 encoding results in the same bytes.
629proof fn decode_encode_width_4(b1: u8, b2: u8, b3: u8, b4: u8)
630    by (bit_vector)
631    requires
632        is_leading_byte_width_4(b1),
633        is_continuation_byte(b2),
634        is_continuation_byte(b3),
635        is_continuation_byte(b4),
636        not_overlong_encoding(codepoint_width_4(b1, b2, b3, b4), 4),
637    ensures
638        ({
639            let c = codepoint_width_4(b1, b2, b3, b4);
640            &&& has_width_4_encoding(c)
641            &&& leading_byte_width_4(c) == b1
642            &&& third_last_continuation_byte(c) == b2
643            &&& second_last_continuation_byte(c) == b3
644            &&& last_continuation_byte(c) == b4
645        }),
646{
647}
648
649/// A `char` always represents a Unicode scalar value.
650pub broadcast proof fn char_is_scalar(c: char)
651    ensures
652        is_scalar(#[trigger] (c as u32)),
653{
654}
655
656/// Ensures that a `char`, when cast to a `u32`, can be cast back to a `char`.
657pub broadcast proof fn char_u32_cast(c: char, u: u32)
658    requires
659        u == #[trigger] (c as u32),
660    ensures
661        #[trigger] (u as char) == c,
662{
663}
664
665/// Properties of the first scalar from the result of [`encode_utf8`].
666pub proof fn encode_utf8_first_scalar(chars: Seq<char>)
667    requires
668        chars.len() > 0,
669    ensures
670        decode_first_scalar(encode_utf8(chars)) == chars[0] as u32,
671        length_of_first_scalar(encode_utf8(chars)) == encode_scalar(chars[0] as u32).len(),
672        valid_first_scalar(encode_utf8(chars)),
673{
674    char_is_scalar(chars[0]);
675    let s = chars[0] as u32;
676    if has_width_1_encoding(s) {
677        encode_decode_width_1(s);
678    } else if has_width_2_encoding(s) {
679        encode_decode_width_2(s);
680    } else if has_width_3_encoding(s) {
681        encode_decode_width_3(s);
682    } else {
683        encode_decode_width_4(s);
684    }
685}
686
687/// Ensures the result of [`encode_utf8`] always satisfies [`valid_utf8`].
688pub broadcast proof fn encode_utf8_valid_utf8(chars: Seq<char>)
689    ensures
690        valid_utf8(#[trigger] encode_utf8(chars)),
691    decreases chars.len(),
692{
693    if chars.len() == 0 {
694    } else {
695        let bytes = encode_utf8(chars);
696        encode_utf8_first_scalar(chars);
697        assert(pop_first_scalar(bytes) =~= encode_utf8(chars.drop_first()));
698        encode_utf8_valid_utf8(chars.drop_first());
699    }
700}
701
702/// Ensures that performing [`encode_utf8`] followed by [`decode_utf8`] results in the original `char` sequence.
703pub broadcast proof fn encode_utf8_decode_utf8(chars: Seq<char>)
704    ensures
705        #[trigger] decode_utf8(encode_utf8(chars)) == chars,
706    decreases chars.len(),
707{
708    broadcast use encode_utf8_valid_utf8;
709
710    if chars.len() == 0 {
711    } else {
712        let bytes = encode_utf8(chars);
713        encode_utf8_first_scalar(chars);
714        char_u32_cast(chars[0], decode_first_scalar(bytes));
715
716        assert(pop_first_scalar(bytes) =~= encode_utf8(chars.drop_first()));
717        let rest = chars.drop_first();
718        encode_utf8_decode_utf8(rest);
719    }
720}
721
722/// Properties of the first scalar from the result of [`decode_utf8`].
723pub proof fn decode_utf8_first_scalar(bytes: Seq<u8>)
724    requires
725        valid_utf8(bytes),
726        bytes.len() > 0,
727    ensures
728        encode_scalar((decode_first_scalar(bytes) as char) as u32) == take_first_scalar(bytes),
729{
730    if is_leading_byte_width_1(bytes[0]) {
731        decode_encode_width_1(bytes[0]);
732    } else if is_leading_byte_width_2(bytes[0]) {
733        decode_encode_width_2(bytes[0], bytes[1]);
734    } else if is_leading_byte_width_3(bytes[0]) {
735        decode_encode_width_3(bytes[0], bytes[1], bytes[2]);
736    } else {
737        decode_encode_width_4(bytes[0], bytes[1], bytes[2], bytes[3]);
738    }
739}
740
741/// Ensures that performing [`decode_utf8`] followed by [`encode_utf8`] results in the original byte sequence.
742pub broadcast proof fn decode_utf8_encode_utf8(bytes: Seq<u8>)
743    requires
744        valid_utf8(bytes),
745    ensures
746        #[trigger] encode_utf8(decode_utf8(bytes)) == bytes,
747    decreases bytes.len(),
748{
749    broadcast use encode_utf8_valid_utf8;
750
751    if bytes.len() == 0 {
752    } else {
753        let chars = decode_utf8(bytes);
754        let first = decode_first_scalar(bytes) as char;
755        let rest = pop_first_scalar(bytes);
756
757        char_is_scalar(first);
758        assert(encode_scalar(first as u32) == take_first_scalar(bytes)) by {
759            decode_utf8_first_scalar(bytes);
760        }
761
762        assert(chars.drop_first() =~= decode_utf8(rest));
763        decode_utf8_encode_utf8(rest);
764    }
765}
766
767/* Partial UTF-8 sequences */
768
769/// True when the first `i` bytes in the given sequence represent a valid UTF-8 encoding.
770pub open spec fn partial_valid_utf8(bytes: Seq<u8>, i: int) -> bool {
771    0 <= i <= bytes.len() && valid_utf8(bytes[..i])
772}
773
774/// Ensures that a byte sequence is not a valid UTF-8 byte sequence when it has a suffix that is not a valid UTF-8 byte sequence.
775pub proof fn partial_valid_partial_invalid_utf8(bytes: Seq<u8>, i: int)
776    requires
777        0 <= i <= bytes.len(),
778        valid_utf8(bytes[..i]),
779        !valid_utf8(bytes[i..]),
780    ensures
781        !valid_utf8(bytes),
782{
783    partial_valid_utf8_invalid_subrange_helper(bytes, i, 0);
784    assert(bytes[..bytes.len()] =~= bytes);
785}
786
787proof fn partial_valid_utf8_invalid_subrange_helper(bytes: Seq<u8>, i: int, j: int)
788    requires
789        0 <= j <= i <= bytes.len(),
790        valid_utf8(bytes[..i]),
791        !valid_utf8(bytes[i..]),
792        valid_utf8(bytes[..j]),
793        valid_utf8(bytes[j..i]),
794    ensures
795        !valid_utf8(bytes[j..]),
796    decreases (bytes.len() - j),
797{
798    if j == i {
799    } else {
800        let bytes_j = bytes[j..];
801        if valid_first_scalar(bytes_j) {
802            partial_valid_utf8_extend(bytes, j);
803            let k = length_of_first_scalar(bytes_j);
804
805            assert(pop_first_scalar(bytes[j..i]) == bytes[j + k..i]);
806
807            partial_valid_utf8_invalid_subrange_helper(bytes, i, j + k);
808
809            assert(bytes_j[k..] == bytes[j + k..]);
810        }
811    }
812}
813
814/// Ensures that concatenating two valid UTF-8 byte sequence results in a valid UTF-8 byte sequence.
815pub broadcast proof fn valid_utf8_concat(b1: Seq<u8>, b2: Seq<u8>)
816    requires
817        #[trigger] valid_utf8(b1),
818        #[trigger] valid_utf8(b2),
819    ensures
820        #[trigger] valid_utf8(b1 + b2),
821    decreases b1.len(),
822{
823    if b1.len() == 0 {
824        assert(b1 + b2 == b2) by { Seq::add_empty_left(b1, b2) };
825        assert(valid_utf8(b1 + b2));
826    } else {
827        let rest = pop_first_scalar(b1);
828        assert(pop_first_scalar(b1).len() < b1.len()) by { lemma_pop_first_scalar_decreases(b1) };
829        valid_utf8_concat(rest, b2);
830        assert(pop_first_scalar(b1 + b2) =~= rest + b2);
831        assert(valid_utf8(b1 + b2));
832    }
833}
834
835/// Ensures that if the prefix of a byte sequence is valid UTF-8, and remainder of the sequence begins with a valid UTF-8 encoding of a single scalar,
836/// then the prefix extended by that scalar encoding is also valid UTF-8.
837pub broadcast proof fn partial_valid_utf8_extend(bytes: Seq<u8>, i: int)
838    requires
839        #[trigger] partial_valid_utf8(bytes, i),
840        #[trigger] valid_first_scalar(bytes[i..]),
841    ensures
842        #[trigger] partial_valid_utf8(
843            bytes,
844            i + length_of_first_scalar(bytes[i..]),
845        ),
846{
847    reveal_with_fuel(valid_utf8, 2);
848    let scalar = bytes[i..i + length_of_first_scalar(bytes[i..])];
849    valid_utf8_concat(bytes[..i], scalar);
850    assert(bytes[..i] + scalar =~= bytes[..i + length_of_first_scalar(bytes[i..])]);
851}
852
853/// Ensures that if the prefix of a byte sequence is valid UTF-8, and remainder of the sequence begins with a subsequence of valid UTF-8 encodings for 1-byte scalars (i.e. ASCII characters),
854/// then the prefix extended by that subsequence is also valid UTF-8.
855pub broadcast proof fn partial_valid_utf8_extend_ascii_block(bytes: Seq<u8>, start: int, end: int)
856    requires
857        forall|i: int|
858            0 <= start <= i < end <= bytes.len() ==> #[trigger] is_leading_byte_width_1(bytes[i]),
859        partial_valid_utf8(bytes, start),
860        0 <= start <= end <= bytes.len(),
861    ensures
862        #![trigger partial_valid_utf8(bytes, start), partial_valid_utf8(bytes, end)]
863        partial_valid_utf8(bytes, end),
864    decreases end - start,
865{
866    if end == start {
867    } else {
868        partial_valid_utf8_extend_ascii_block(bytes, start, end - 1);
869
870        let b = bytes[end - 1];
871        assert(is_leading_byte_width_1(b));
872        partial_valid_utf8_extend(bytes, end - 1);
873    }
874}
875
876/* Reasoning about character boundaries */
877
878/// True when the given index into the byte sequence is the first byte of a character's encoding or the end of the sequence, assuming that the sequence is valid UTF-8.
879pub open spec fn is_char_boundary(bytes: Seq<u8>, index: int) -> bool
880    recommends
881        valid_utf8(bytes),
882    decreases bytes.len(),
883    when valid_utf8(bytes)
884{
885    if index == 0 {
886        true
887    } else if index < 0 || bytes.len() < index {
888        false
889    } else {
890        is_char_boundary(pop_first_scalar(bytes), index - length_of_first_scalar(bytes))
891    }
892}
893
894proof fn take_first_scalar_valid_utf8(bytes: Seq<u8>)
895    requires
896        valid_utf8(bytes),
897    ensures
898        bytes.len() > 0 ==> valid_utf8(take_first_scalar(bytes)),
899{
900    reveal_with_fuel(valid_utf8, 2);
901}
902
903/// Ensures that the two subsequences formed by splitting a valid UTF-8 byte sequence at a character boundary are also valid UTF-8 byte sequences.
904pub broadcast proof fn valid_utf8_split(bytes: Seq<u8>, index: int)
905    requires
906        valid_utf8(bytes),
907        is_char_boundary(bytes, index),
908    ensures
909        #![trigger valid_utf8(bytes[..index]), is_char_boundary(bytes, index)]
910        #![trigger valid_utf8(bytes[index..]), is_char_boundary(bytes, index)]
911        valid_utf8(bytes[..index]),
912        valid_utf8(bytes[index..]),
913    decreases bytes.len(),
914{
915    if index == 0 {
916        assert(bytes =~= bytes[index..]);
917    } else {
918        broadcast use lemma_seq_subrange_len;
919
920        let s1 = bytes[..index];
921        let s2 = bytes[index..];
922        let head = take_first_scalar(bytes);
923        let tail = pop_first_scalar(bytes);
924        let new_offset = index - length_of_first_scalar(bytes);
925        // recursive call: show valid on split for tail
926        valid_utf8_split(tail, new_offset);
927        let n1 = tail[..new_offset];
928        let n2 = tail[new_offset..];
929        // now we need to concatenate the head back on
930        assert(s1 =~= head + n1) by {
931            assert(s1.len() == head.len() + n1.len()) by {
932                // to use subrange len axiom, we need to show that new_offset is in bounds for tail
933                is_char_boundary_len_first_scalar(bytes, index);
934            }
935        }
936        assert(valid_utf8(head + n1)) by {
937            take_first_scalar_valid_utf8(bytes);
938            valid_utf8_concat(head, n1);
939        }
940        assert(s2 =~= n2);
941    }
942}
943
944/// Ensures that a valid UTF-8 byte sequence can be decoded by separately decoding the two subsequences formed by splitting the original sequence at a character boundary.
945pub broadcast proof fn decode_utf8_split(bytes: Seq<u8>, index: int)
946    requires
947        valid_utf8(bytes),
948        is_char_boundary(bytes, index),
949    ensures
950        #![trigger decode_utf8(bytes[..index]), is_char_boundary(bytes, index)]
951        #![trigger decode_utf8(bytes[index..]), is_char_boundary(bytes, index)]
952        decode_utf8(bytes) =~= decode_utf8(bytes[..index]) + decode_utf8(bytes[index..]),
953    decreases index,
954{
955    if index == 0 {
956        assert(bytes[index..] =~= bytes);
957    } else {
958        let first = bytes[..index];
959        let second = bytes[index..];
960        is_char_boundary_len_first_scalar(bytes, index);
961        valid_utf8_split(bytes, index);
962        let bytes_tail = pop_first_scalar(bytes);
963        let first_tail = pop_first_scalar(first);
964        let bytes_head = decode_first_scalar(bytes) as char;
965        let first_head = decode_first_scalar(first) as char;
966        let new_index = (index - length_of_first_scalar(bytes)) as int;
967        decode_utf8_split(bytes_tail, new_index);
968        assert(second =~= bytes_tail[new_index..]);
969        assert(first_tail =~= bytes_tail[..new_index]);
970    }
971}
972
973proof fn is_char_boundary_len_first_scalar(bytes: Seq<u8>, index: int)
974    requires
975        valid_utf8(bytes),
976        is_char_boundary(bytes, index),
977    ensures
978        index > 0 ==> index >= length_of_first_scalar(bytes),
979{
980    reveal_with_fuel(is_char_boundary, 2);
981}
982
983/// Ensures that the start and end of a valid UTF-8 byte sequence are character boundaries.
984pub broadcast proof fn is_char_boundary_start_end_of_seq(bytes: Seq<u8>)
985    requires
986        valid_utf8(bytes),
987    ensures
988        #![trigger is_char_boundary(bytes, 0)]
989        #![trigger is_char_boundary(bytes, bytes.len() as int)]
990        is_char_boundary(bytes, 0),
991        is_char_boundary(bytes, bytes.len() as int),
992    decreases bytes.len(),
993{
994    if bytes.len() == 0 {
995    } else {
996        is_char_boundary_start_end_of_seq(pop_first_scalar(bytes));
997    }
998}
999
1000/// Ensures that any byte in a valid UTF-8 byte sequence falls on a character boundary (i.e. the first byte in a codepoint's encoding) if and only if it does not have the form of a UTF-8 continuation byte.
1001pub broadcast proof fn is_char_boundary_iff_not_is_continuation_byte(bytes: Seq<u8>, index: int)
1002    requires
1003        valid_utf8(bytes),
1004        0 <= index < bytes.len(),
1005    ensures
1006        #[trigger] is_char_boundary(bytes, index) <==> !(#[trigger] is_continuation_byte(
1007            bytes[index],
1008        )),
1009    decreases bytes.len(),
1010{
1011    if 0 <= index < length_of_first_scalar(bytes) {
1012        reveal_with_fuel(is_char_boundary, 2);
1013    } else {
1014        is_char_boundary_iff_not_is_continuation_byte(
1015            pop_first_scalar(bytes),
1016            index - length_of_first_scalar(bytes),
1017        );
1018    }
1019}
1020
1021/// Ensures that any byte in a valid UTF-8 byte sequence falls on a character boundary (i.e. the first byte in a codepoint's encoding) if and only if it has the form of a UTF-8 leading byte.
1022pub broadcast proof fn is_char_boundary_iff_is_leading_byte(bytes: Seq<u8>, index: int)
1023    requires
1024        valid_utf8(bytes),
1025        0 <= index < bytes.len(),
1026    ensures
1027        #![trigger is_char_boundary(bytes, index), is_leading_byte_width_1(bytes[index])]
1028        #![trigger is_char_boundary(bytes, index), is_leading_byte_width_2(bytes[index])]
1029        #![trigger is_char_boundary(bytes, index), is_leading_byte_width_3(bytes[index])]
1030        #![trigger is_char_boundary(bytes, index), is_leading_byte_width_4(bytes[index])]
1031        is_char_boundary(bytes, index) <==> (is_leading_byte_width_1(bytes[index])
1032            || is_leading_byte_width_2(bytes[index]) || is_leading_byte_width_3(bytes[index])
1033            || is_leading_byte_width_4(bytes[index])),
1034    decreases bytes.len(),
1035{
1036    if 0 <= index < length_of_first_scalar(bytes) {
1037        reveal_with_fuel(is_char_boundary, 2);
1038    } else {
1039        is_char_boundary_iff_is_leading_byte(
1040            pop_first_scalar(bytes),
1041            index - length_of_first_scalar(bytes),
1042        );
1043    }
1044}
1045
1046pub broadcast proof fn valid_utf8_last(s: Seq<u8>)
1047    requires
1048        valid_utf8(s),
1049        s.len() > 0,
1050    ensures
1051        #![trigger is_continuation_byte(s.last())]
1052        #![trigger is_leading_byte_width_1(s.last())]
1053        !is_continuation_byte(s.last()) ==> is_leading_byte_width_1(s.last()),
1054    decreases s.len(),
1055{
1056    // this proof must be discharged recursively, since valid_utf8 only tells you information
1057    // about the first codepoint and recurses from there
1058    let first = decode_first_scalar(s);
1059    let rest = pop_first_scalar(s);
1060
1061    if rest.len() == 0 {
1062        if s.len() > 1 {
1063            assert(is_continuation_byte(s[s.len() - 1]));
1064        }
1065    } else {
1066        valid_utf8_last(rest);
1067    }
1068}
1069
1070/* Bit-level reasoning */
1071
1072/// Formulates the byte ranges for each type of byte in UTF-8 (leading and continuation) in terms of bitwise operators instead of ranges.
1073pub broadcast proof fn utf8_byte_ranges_bitwise(b: u8)
1074    by (bit_vector)
1075    ensures
1076        #![trigger b & 0x80]
1077        #![trigger b & 0xf0]
1078        #![trigger b & 0xf8]
1079        #![trigger b & 0xe0]
1080        #![trigger b & 0xc0]
1081        0x00 <= b <= 0x7f <==> b & 0x80 == 0,
1082        0xc0 <= b <= 0xdf <==> b & 0xe0 == 0xc0,
1083        0xe0 <= b <= 0xef <==> b & 0xf0 == 0xe0,
1084        0xf0 <= b <= 0xf7 <==> b & 0xf8 == 0xf0,
1085        0x80 <= b <= 0xbf <==> b & 0xc0 == 0x80,
1086{
1087}
1088
1089/* ASCII */
1090
1091/// True when the given character sequence only contains ASCII characters.
1092pub open spec fn is_ascii_chars(chars: Seq<char>) -> bool {
1093    forall|i| 0 <= i < chars.len() ==> '\0' <= #[trigger] chars[i] <= '\u{7f}'
1094}
1095
1096/// Ensures that the UTF-8 encoding for an ASCII character sequence has the same length of the original sequence and corresponds byte-by-byte to the characters in the original sequence.
1097pub broadcast proof fn is_ascii_chars_encode_utf8(chars: Seq<char>)
1098    requires
1099        #[trigger] is_ascii_chars(chars),
1100    ensures
1101        chars.len() == encode_utf8(chars).len(),
1102        forall|i|
1103            #![trigger chars[i]]
1104            #![trigger encode_utf8(chars)[i]]
1105            0 <= i < chars.len() ==> chars[i] as u8 == encode_utf8(chars)[i],
1106    decreases chars.len(),
1107{
1108    if chars.len() == 0 {
1109    } else {
1110        let c0 = chars[0] as u32;
1111        assert(c0 as u8 == leading_byte_width_1(c0)) by (bit_vector)
1112            requires
1113                has_width_1_encoding(c0),
1114        ;
1115        is_ascii_chars_encode_utf8(chars.drop_first());
1116    }
1117}
1118
1119/// Ensures that all characters in an ASCII character sequence have a numerical representation that falls in the range 0 (inclusive) to 128 (exclusive).
1120pub broadcast proof fn is_ascii_chars_nat_bound(chars: Seq<char>)
1121    ensures
1122        #[trigger] is_ascii_chars(chars) ==> forall|i: int|
1123            0 <= i < chars.len() ==> (chars.index(i) as nat) < 128,
1124{
1125}
1126
1127/// Ensures that an ASCII character sequence is formed by the concatenation of two ASCII character sequences.
1128pub broadcast proof fn is_ascii_chars_concat(c1: Seq<char>, c2: Seq<char>, c3: Seq<char>)
1129    requires
1130        c1 =~= c2 + c3,
1131    ensures
1132        #![trigger c2 + c3, is_ascii_chars(c1), is_ascii_chars(c2), is_ascii_chars(c3)]
1133        is_ascii_chars(c1) <==> is_ascii_chars(c2) && is_ascii_chars(c3),
1134{
1135    if (is_ascii_chars(c1)) {
1136        assert(c2 =~= c1[..c2.len()]);
1137        assert(c3 =~= c1[c2.len()..c1.len()]);
1138    }
1139}
1140
1141pub broadcast group group_utf8_lib {
1142    encode_utf8_valid_utf8,
1143    encode_utf8_decode_utf8,
1144    decode_utf8_encode_utf8,
1145    char_is_scalar,
1146    char_u32_cast,
1147    valid_utf8_concat,
1148    partial_valid_utf8_extend,
1149    partial_valid_utf8_extend_ascii_block,
1150    valid_utf8_split,
1151    decode_utf8_split,
1152    is_char_boundary_start_end_of_seq,
1153    is_char_boundary_iff_not_is_continuation_byte,
1154    is_char_boundary_iff_is_leading_byte,
1155    valid_utf8_last,
1156    utf8_byte_ranges_bitwise,
1157    is_ascii_chars_encode_utf8,
1158    is_ascii_chars_nat_bound,
1159    is_ascii_chars_concat,
1160    encode_utf8_concat,
1161    encode_utf8_push,
1162}
1163
1164} // verus!
vstd/utf8.rs

vstd/
utf8.rs
