diff --git a/Codec.lean b/Codec.lean index 2aa7de4..74991d0 100644 --- a/Codec.lean +++ b/Codec.lean @@ -1,4 +1,5 @@ import Codec.Hex import Codec.Base64 +import Codec.Base32 import Codec.Crc32 import Codec.Percent diff --git a/Codec/Base32.lean b/Codec/Base32.lean new file mode 100644 index 0000000..4690be5 --- /dev/null +++ b/Codec/Base32.lean @@ -0,0 +1,109 @@ +/- + Base 32 as RFC 4648 section 6 defines it: the standard alphabet, + with padding. + + `decode` is strict. It accepts exactly the text `encode` produces: no + missing or extra padding, no padding before the end, no characters + outside the alphabet, no line breaks, and the unused bits before the + padding must be zero. +-/ + +namespace Codec.Base32 + +/-- The 32 characters, in order. -/ +def alphabet : List Char := + "ABCDEFGHIJKLMNOPQRSTUVWXYZ234567".toList + +/-- The character for a value below 32. -/ +def char (n : Nat) : Char := + alphabet.getD n 'A' + +/-- Encode bytes, five at a time into eight characters. -/ +def encode : List UInt8 → List Char + | a :: b :: c :: d :: e :: rest => + let n := a.toNat * 4294967296 + b.toNat * 16777216 + c.toNat * 65536 + + d.toNat * 256 + e.toNat + char (n / 34359738368) :: char (n / 1073741824 % 32) :: + char (n / 33554432 % 32) :: char (n / 1048576 % 32) :: + char (n / 32768 % 32) :: char (n / 1024 % 32) :: + char (n / 32 % 32) :: char (n % 32) :: encode rest + | [a, b, c, d] => + let n := a.toNat * 4294967296 + b.toNat * 16777216 + c.toNat * 65536 + + d.toNat * 256 + [char (n / 34359738368), char (n / 1073741824 % 32), + char (n / 33554432 % 32), char (n / 1048576 % 32), + char (n / 32768 % 32), char (n / 1024 % 32), + char (n / 32 % 32), '='] + | [a, b, c] => + let n := a.toNat * 4294967296 + b.toNat * 16777216 + c.toNat * 65536 + [char (n / 34359738368), char (n / 1073741824 % 32), + char (n / 33554432 % 32), char (n / 1048576 % 32), + char (n / 32768 % 32), '=', '=', '='] + | [a, b] => + let n := a.toNat * 4294967296 + b.toNat * 16777216 + [char (n / 34359738368), char (n / 1073741824 % 32), + char (n / 33554432 % 32), char (n / 1048576 % 32), + '=', '=', '=', '='] + | [a] => + let n := a.toNat * 4294967296 + [char (n / 34359738368), char (n / 1073741824 % 32), + '=', '=', '=', '=', '=', '='] + | [] => [] + +/-- The value of one character of the alphabet. -/ +def value (c : Char) : Option Nat := + if 'A' ≤ c ∧ c ≤ 'Z' then some (c.toNat - 65) + else if '2' ≤ c ∧ c ≤ '7' then some (c.toNat - 24) + else none + +/-- Decode, eight characters at a time into five bytes. Padding may + only end the text. -/ +def decode : List Char → Option (List UInt8) + | [] => some [] + | [c0, c1, '=', '=', '=', '=', '=', '='] => + match value c0, value c1 with + | some v0, some v1 => + if v1 % 4 = 0 then some [(v0 * 8 + v1 / 4).toUInt8] else none + | _, _ => none + | [c0, c1, c2, c3, '=', '=', '=', '='] => + match value c0, value c1, value c2, value c3 with + | some v0, some v1, some v2, some v3 => + if v3 % 16 = 0 then + some [(v0 * 8 + v1 / 4).toUInt8, + (v1 % 4 * 64 + v2 * 2 + v3 / 16).toUInt8] + else none + | _, _, _, _ => none + | [c0, c1, c2, c3, c4, '=', '=', '='] => + match value c0, value c1, value c2, value c3, value c4 with + | some v0, some v1, some v2, some v3, some v4 => + if v4 % 2 = 0 then + some [(v0 * 8 + v1 / 4).toUInt8, + (v1 % 4 * 64 + v2 * 2 + v3 / 16).toUInt8, + (v3 % 16 * 16 + v4 / 2).toUInt8] + else none + | _, _, _, _, _ => none + | [c0, c1, c2, c3, c4, c5, c6, '='] => + match value c0, value c1, value c2, value c3, value c4, value c5, + value c6 with + | some v0, some v1, some v2, some v3, some v4, some v5, some v6 => + if v6 % 8 = 0 then + some [(v0 * 8 + v1 / 4).toUInt8, + (v1 % 4 * 64 + v2 * 2 + v3 / 16).toUInt8, + (v3 % 16 * 16 + v4 / 2).toUInt8, + (v4 % 2 * 128 + v5 * 4 + v6 / 8).toUInt8] + else none + | _, _, _, _, _, _, _ => none + | c0 :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: rest => + match value c0, value c1, value c2, value c3, value c4, value c5, + value c6, value c7, decode rest with + | some v0, some v1, some v2, some v3, some v4, some v5, some v6, + some v7, some tail => + some ((v0 * 8 + v1 / 4).toUInt8 :: + (v1 % 4 * 64 + v2 * 2 + v3 / 16).toUInt8 :: + (v3 % 16 * 16 + v4 / 2).toUInt8 :: + (v4 % 2 * 128 + v5 * 4 + v6 / 8).toUInt8 :: + (v6 % 8 * 32 + v7).toUInt8 :: tail) + | _, _, _, _, _, _, _, _, _ => none + | _ => none + +end Codec.Base32 diff --git a/Main.lean b/Main.lean index f47c182..d292c7e 100644 --- a/Main.lean +++ b/Main.lean @@ -9,6 +9,8 @@ hexdec 48,49,97,66 prints ok:1,171 (or none) b64enc 102,111 prints Zm8= b64dec 90,103,61,61 prints ok:102 (or none) + b32enc 102,111 prints MZXQ==== + b32dec 77,90,88,81,61,61,61,61 prints ok:102,111 (or none) crc 49,50,51 prints the CRC-32 as a decimal number frame 1,2 prints the framed bytes unframe 1,2,3,4,5 prints ok:... (or none) @@ -61,6 +63,8 @@ def answer (op : String) (ns : List Nat) : Option String := do | "hexdec" => return result (Hex.decode (← toChars ns)) | "b64enc" => return String.ofList (Base64.encode (← toBytes ns)) | "b64dec" => return result (Base64.decode (← toChars ns)) + | "b32enc" => return String.ofList (Base32.encode (← toBytes ns)) + | "b32dec" => return result (Base32.decode (← toChars ns)) | "crc" => return toString (Crc32.crc32 (← toBytes ns)).toNat | "frame" => return showBytes (Crc32.frame (← toBytes ns)) | "unframe" => return result (Crc32.unframe (← toBytes ns)) diff --git a/Proofs.lean b/Proofs.lean index 694b150..1913cb6 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -4,5 +4,6 @@ import Proofs.Hex import Proofs.Base64 +import Proofs.Base32 import Proofs.Crc32 import Proofs.Percent diff --git a/Proofs/Base32.lean b/Proofs/Base32.lean new file mode 100644 index 0000000..21d018c --- /dev/null +++ b/Proofs/Base32.lean @@ -0,0 +1,127 @@ +/- + Proofs of the Base32 round trip. + + The statement proved here is the Base32 version of the round trip + statements in `Spec.lean` for the other codecs. A matching statement + for Base32 still has to be added to `Spec.lean` by a reviewer, so + this file is a draft that builds on its own. + + The helper lemmas live in `Codec.Proofs.Base32`. +-/ + +import Codec +import Spec.Defs + +open Codec + +namespace Codec.Proofs.Base32 + +set_option maxRecDepth 10000 in +theorem value_tbl : ∀ n : Fin 32, Base32.value (Base32.char n.val) = some n.val := by + decide +kernel + +theorem value_char {n : Nat} (h : n < 32) : Base32.value (Base32.char n) = some n := + value_tbl ⟨n, h⟩ + +theorem char_ne_pad {n : Nat} (h : n < 32) : Base32.char n ≠ '=' := by + intro e + have hv := value_char h + have hpad : Base32.value '=' = none := by decide + rw [e, hpad] at hv + cases hv + +theorem toNat_toUInt8 {k : Nat} (h : k < 256) : k.toUInt8.toNat = k := by + simp; omega + +end Codec.Proofs.Base32 + +open Codec.Proofs.Base32 + +/-- Decoding gives back what was encoded. -/ +theorem Spec.base32_decode_encode (bs : List UInt8) : + Base32.decode (Base32.encode bs) = some bs := by + induction bs using Base32.encode.induct with + | case1 a b c d e rest ih => + have ha := a.toNat_lt + have hb := b.toNat_lt + have hc := c.toNat_lt + have hd := d.toNat_lt + have he := e.toNat_lt + rw [Base32.encode.eq_1, + Base32.decode.eq_6 _ _ _ _ _ _ _ _ _ + (fun h _ _ _ _ _ _ => char_ne_pad (by omega) h) + (fun h _ _ _ _ => char_ne_pad (by omega) h) + (fun h _ _ _ => char_ne_pad (by omega) h) + (fun h _ => char_ne_pad (by omega) h), + value_char (by omega), value_char (by omega), value_char (by omega), + value_char (by omega), value_char (by omega), value_char (by omega), + value_char (by omega), value_char (by omega), ih] + simp only [Option.some.injEq, List.cons.injEq, and_true] + refine ⟨?_, ?_, ?_, ?_, ?_⟩ <;> apply UInt8.toNat_inj.mp <;> + rw [toNat_toUInt8 (by omega)] <;> omega + | case2 a b c d => + have ha := a.toNat_lt + have hb := b.toNat_lt + have hc := c.toNat_lt + have hd := d.toNat_lt + rw [Base32.encode.eq_2, + Base32.decode.eq_5 _ _ _ _ _ _ _ + (fun h _ _ _ _ => char_ne_pad (by omega) h) + (fun h _ _ => char_ne_pad (by omega) h) + (fun h _ => char_ne_pad (by omega) h), + value_char (by omega), value_char (by omega), value_char (by omega), + value_char (by omega), value_char (by omega), value_char (by omega), + value_char (by omega)] + simp only + rw [ite_eq_left (by omega)] + simp only [Option.some.injEq, List.cons.injEq, and_true] + refine ⟨?_, ?_, ?_, ?_⟩ <;> apply UInt8.toNat_inj.mp <;> + rw [toNat_toUInt8 (by omega)] <;> omega + | case3 a b c => + have ha := a.toNat_lt + have hb := b.toNat_lt + have hc := c.toNat_lt + rw [Base32.encode.eq_3, + Base32.decode.eq_4 _ _ _ _ _ + (fun h _ _ => char_ne_pad (by omega) h) + (fun h => char_ne_pad (by omega) h), + value_char (by omega), value_char (by omega), value_char (by omega), + value_char (by omega), value_char (by omega)] + simp only + rw [ite_eq_left (by omega)] + simp only [Option.some.injEq, List.cons.injEq, and_true] + refine ⟨?_, ?_, ?_⟩ <;> apply UInt8.toNat_inj.mp <;> + rw [toNat_toUInt8 (by omega)] <;> omega + | case4 a b => + have ha := a.toNat_lt + have hb := b.toNat_lt + rw [Base32.encode.eq_4, + Base32.decode.eq_3 _ _ _ _ + (fun h _ => char_ne_pad (by omega) h), + value_char (by omega), value_char (by omega), value_char (by omega), + value_char (by omega)] + simp only + rw [ite_eq_left (by omega)] + simp only [Option.some.injEq, List.cons.injEq, and_true] + refine ⟨?_, ?_⟩ <;> apply UInt8.toNat_inj.mp <;> + rw [toNat_toUInt8 (by omega)] <;> omega + | case5 a => + have ha := a.toNat_lt + rw [Base32.encode.eq_5, Base32.decode.eq_2, value_char (by omega), + value_char (by omega)] + simp only + rw [ite_eq_left (by omega)] + simp only [Option.some.injEq, List.cons.injEq, and_true] + apply UInt8.toNat_inj.mp; rw [toNat_toUInt8 (by omega)]; omega + | case6 => rfl + +/-- The test vectors of RFC 4648, section 10. -/ +theorem Spec.base32_rfc4648_vectors : + Base32.encode (Spec.ascii "") = "".toList ∧ + Base32.encode (Spec.ascii "f") = "MY======".toList ∧ + Base32.encode (Spec.ascii "fo") = "MZXQ====".toList ∧ + Base32.encode (Spec.ascii "foo") = "MZXW6===".toList ∧ + Base32.encode (Spec.ascii "foob") = "MZXW6YQ=".toList ∧ + Base32.encode (Spec.ascii "fooba") = "MZXW6YTB".toList ∧ + Base32.encode (Spec.ascii "foobar") = "MZXW6YTBOI======".toList := by + decide +kernel diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 333f6e2..e280aec 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -2,13 +2,14 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. -- Oracle: Python 3.13.17 `binascii`, `base64`, `zlib` (zlib 1.3), `urllib.parse` +- Oracle: Python 3.12.3 `binascii`, `base64`, `zlib` (zlib 1.3), `urllib.parse` - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261024 - Inputs: 1000000 -- Mutated: 235073 of the inputs are mutated encodings or frames -- By operation: b64dec 117552, b64enc 58769, crc 58771, error 71, frame 58769, hexdec 176323, hexenc 58772, pctdec 294412, pctenc 59024, unframe 117537 -- Malformed requests answered `error`: 71 of 71 +- Mutated: 249760 of the inputs are mutated encodings or frames +- By operation: b32dec 99919, b32enc 49953, b64dec 99920, b64enc 49953, crc 49954, error 75, frame 49952, hexdec 149874, hexenc 49956, pctdec 250332, pctenc 50208, unframe 99904 +- Malformed requests answered `error`: 75 of 75 - Last lines with no LF, sent alone, answered right: 6 of 6 -- Strict base 64 rejections where Python decodes: 10562 (10562 with unused bits before the padding not zero, 0 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) +- Strict base 64 rejections where Python decodes: 11265 (8945 with unused bits before the padding not zero, 2320 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) +- Strict base 32 rejections where Python decodes: 4019 (4019 with base 32 unused bits before the padding not zero, 0 with base 32 padding after a whole group, which Python decodes) - Failures: 0 diff --git a/tests/run_tests.py b/tests/run_tests.py index a6b6440..d0ed770 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -2,8 +2,9 @@ """Differential tests: the Lean codecs against Python's own. The oracles are Python's `binascii.hexlify` and `binascii.unhexlify`, -`base64.b64encode` and strict `binascii.a2b_base64`, `zlib.crc32`, and -for percent-encoding `urllib.parse.quote` with no safe characters and +`base64.b64encode` and strict `binascii.a2b_base64`, `base64.b32encode` +and `base64.b32decode`, `zlib.crc32`, and for percent-encoding +`urllib.parse.quote` with no safe characters and `urllib.parse.unquote_to_bytes`. `unquote_to_bytes` passes a bad escape through as text, where RFC 3986 has none, so text is first checked against what `Spec.PctReads` accepts, as a regular expression, and only @@ -24,9 +25,12 @@ bits before the padding are not zero, and Python 3.11, and 3.12 before 3.12.4, also decode padding after a whole group, such as `Zm9v=` (CPython issue gh-118314). Each such case is checked to be exactly one -of the two, by re-encoding what Python decoded, and counted. Any other -case where Python decodes text that does not re-encode to itself is -compared as usual, and fails. +of the two, by re-encoding what Python decoded, and counted. The same +unused bits difference applies to base 32: Python's `base64.b32decode` +decodes text whose unused bits before the padding are not zero, which +the strict Lean decoder rejects. Those cases are checked the same way +and counted separately. Any other case where Python decodes text that +does not re-encode to itself is compared as usual, and fails. python3 tests/run_tests.py [--seed N] [--count N] @@ -58,6 +62,8 @@ PADDING_BITS = "unused bits before the padding not zero" EXTRA_PADDING = "padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode" +PADDING_BITS_B32 = "base 32 unused bits before the padding not zero" +EXTRA_PADDING_B32 = "base 32 padding after a whole group, which Python decodes" def nums(values): @@ -133,6 +139,7 @@ def decoded(result): ("hexenc 256", "a byte above 255"), ("hexenc 0,511", "a byte above 255"), ("b64enc 1,256", "a byte above 255"), + ("b32enc 1,256", "a byte above 255"), ("crc 1,256", "a byte above 255"), ("frame 0,256", "a byte above 255"), ("unframe 0,1,2,300", "a byte above 255"), @@ -141,6 +148,7 @@ def decoded(result): ("crc 1,18446744073709551617", "a byte of 2^64 + 1, which wraps to 1"), ("hexdec 48,55296", "a surrogate, not a character"), ("b64dec 90,103,61,57343", "a surrogate, not a character"), + ("b32dec 77,89,61,61,61,61,61,57343", "a surrogate, not a character"), ("hexdec 48,1114112", "beyond Unicode"), ("pctenc 37,256", "a byte above 255"), ("pctdec 37,55296", "a surrogate, not a character"), @@ -149,8 +157,10 @@ def decoded(result): ("b64dec 90,103,61,99999999999999999999", "beyond Unicode"), (f"hexdec {wrapped('01', 32)}", "code points that wrap at 2^32 to digits"), (f"b64dec {wrapped('Zm8=', 32)}", "code points that wrap at 2^32 to base 64"), + (f"b32dec {wrapped('MZXQ====', 32)}", "code points that wrap at 2^32 to base 32"), (f"hexdec {wrapped('01', 64)}", "code points that wrap at 2^64 to digits"), (f"b64dec {wrapped('Zm8=', 64)}", "code points that wrap at 2^64 to base 64"), + (f"b32dec {wrapped('MZXQ====', 64)}", "code points that wrap at 2^64 to base 32"), ("hexenc 1" + "0" * 100 + "1", "a number with a hundred digits"), ("crc 1,1" + "0" * 100 + "1", "a number with a hundred digits"), ] @@ -231,6 +241,15 @@ def mutate_pct(rng, text): if kind == 3: return text.swapcase() return text[:i] + "".join(rng.choice(PCT_POOL) for _ in range(rng.randrange(1, 4))) + text[i:] +def oracle_b32decode(text): + try: + raw = text.encode("ascii") + except UnicodeEncodeError: + return None + try: + return base64.b32decode(raw) + except binascii.Error: + return None def oracle_unframe(fr): @@ -255,8 +274,25 @@ def b64_difference(text, py): return None +def b32_difference(text, py): + """Why Python decoded `text` to `py` though strict decoding rejects + it: one of the known differences, or None.""" + canon = base64.b32encode(py).decode() + if canon == text: + return None + core, text_core = canon.rstrip("="), text.rstrip("=") + if (len(canon) == len(text) and canon != core and len(core) == len(text_core) + and core[:-1] == text_core[:-1]): + return PADDING_BITS_B32 + if canon == core and text.startswith(canon) and set(text[len(canon):]) == {"="}: + return EXTRA_PADDING_B32 + return None + + POOL = "AZaz09+/=GgQw-_ .\n\xe9İŁ\U00010030\U0001f441" B64_ALPHABET = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/" +POOL32 = "AZ27=GgQw-_ .\n\xe9İŁ\U00010030\U0001f441" +B32_ALPHABET = "ABCDEFGHIJKLMNOPQRSTUVWXYZ234567" def mutate_text(rng, text): @@ -285,6 +321,29 @@ def mutate_text(rng, text): return text +def mutate_text_b32(rng, text): + """One random mutation of a base 32 encoding.""" + kind = rng.randrange(7) + i = rng.randrange(len(text) + 1) + if kind == 0 and text: + return text[:i % len(text)] + rng.choice(POOL32) + text[i % len(text) + 1:] + if kind == 1: + return text[:i] + rng.choice(POOL32) + text[i:] + if kind == 2 and text: + return text[:i % len(text)] + text[i % len(text) + 1:] + if kind == 3: + return text.swapcase() + if kind == 4: + return text.rstrip("=") + "=" * rng.randrange(9) + if kind == 5 and text: + j = i % len(text) + return text[:j] + chr(ord(text[j]) + rng.choice([0x100, 0x10000, 0x100000])) + text[j + 1:] + core = text.rstrip("=") + if core: + return core[:-1] + rng.choice(B32_ALPHABET) + text[len(core):] + return text + + def mutate_bytes(rng, data): if not data: return bytes([rng.randrange(256)]) @@ -318,6 +377,8 @@ def fixed_cases(): for text in (c, "%4" + c, "%" + c + "1", "a" + c + "%41"): items.append(("pctdec", f"pctdec {text_nums(text)}", decoded(oracle_pctdec(text)), None, False)) + items.append(("b32dec", f"b32dec {text_nums(c * 8)}", decoded(oracle_b32decode(c * 8)), + None, False)) # Every byte alone, and every one-character text: the whole of the # encoder's and the decoder's per-character rules. for b in range(256): @@ -345,6 +406,7 @@ def cases(seed, count): data = rng.randbytes(n) hex_text = binascii.hexlify(data).decode() b64_text = base64.b64encode(data).decode() + b32_text = base64.b32encode(data).decode() frame = data + zlib.crc32(data).to_bytes(4, "little") batch = [ ("hexenc", f"hexenc {nums(data)}", hex_text, None, False), @@ -352,6 +414,8 @@ def cases(seed, count): ("hexdec", f"hexdec {text_nums(hex_text.upper())}", decoded(data), None, False), ("b64enc", f"b64enc {nums(data)}", b64_text, None, False), ("b64dec", f"b64dec {text_nums(b64_text)}", decoded(data), None, False), + ("b32enc", f"b32enc {nums(data)}", b32_text, None, False), + ("b32dec", f"b32dec {text_nums(b32_text)}", decoded(data), None, False), ("crc", f"crc {nums(data)}", str(zlib.crc32(data)), None, False), ("frame", f"frame {nums(data)}", nums(frame), None, False), ("unframe", f"unframe {nums(frame)}", decoded(data), None, False), @@ -363,6 +427,11 @@ def cases(seed, count): why = None if py is None else b64_difference(bad_b64, py) want = "none" if why else decoded(py) batch.append(("b64dec", f"b64dec {text_nums(bad_b64)}", want, why, True)) + bad_b32 = changed(mutate_text_b32, rng, b32_text) + py32 = oracle_b32decode(bad_b32) + why32 = None if py32 is None else b32_difference(bad_b32, py32) + want32 = "none" if why32 else decoded(py32) + batch.append(("b32dec", f"b32dec {text_nums(bad_b32)}", want32, why32, True)) bad_frame = changed(mutate_bytes, rng, frame) batch.append(("unframe", f"unframe {nums(bad_frame)}", decoded(oracle_unframe(bad_frame)), None, True)) pct_text = oracle_pctenc(data) @@ -513,6 +582,8 @@ def main(): malformed = [got for item, got in zip(items, out) if item[0] == "error"] pad_bits = sum(1 for item in items if item[3] == PADDING_BITS) extra_pad = sum(1 for item in items if item[3] == EXTRA_PADDING) + pad_bits_b32 = sum(1 for item in items if item[3] == PADDING_BITS_B32) + extra_pad_b32 = sum(1 for item in items if item[3] == EXTRA_PADDING_B32) lines = [ "# Test results", @@ -529,6 +600,8 @@ def main(): f"- Last lines with no LF, sent alone, answered right: {eof_right} of {len(AT_EOF)}", f"- Strict base 64 rejections where Python decodes: {pad_bits + extra_pad} " f"({pad_bits} with {PADDING_BITS}, {extra_pad} with {EXTRA_PADDING})", + f"- Strict base 32 rejections where Python decodes: {pad_bits_b32 + extra_pad_b32} " + f"({pad_bits_b32} with {PADDING_BITS_B32}, {extra_pad_b32} with {EXTRA_PADDING_B32})", f"- Failures: {len(failures)}", "", ]