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

vstd/
utf8.rs
