Bring Base32 onto main (stacked slice, from initial-import branch)

Codec.lean

@@ -1,4 +1,5 @@
 import Codec.Hex
 import Codec.Base64
+import Codec.Base32
 import Codec.Crc32
 import Codec.Percent

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

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))

Proofs.lean

@@ -4,5 +4,6 @@
 
 import Proofs.Hex
 import Proofs.Base64
+import Proofs.Base32
 import Proofs.Crc32
 import Proofs.Percent

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

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