fn utf8_validity_dfa<'z3>(z3_ctx: &'z3 Context, bytes: &[Int<'z3>]) -> Bool<'z3>Expand description
Build the boolean expression “bytes form a valid UTF-8 sequence”.
Encodes the UTF-8 DFA over the per-byte Z3 terms: every byte is ASCII, a
continuation byte, or a valid lead byte, and a k-byte lead must be
followed by exactly k-1 continuation bytes. Value-range refinements
reject overlong encodings, surrogates (U+D800..=U+DFFF), and code points
above U+10FFFF.