diff --git a/Codec/Proofs.lean b/Codec/Proofs.lean
new file mode 100644
index 0000000..52a7395
--- /dev/null
+++ b/Codec/Proofs.lean
@@ -0,0 +1,12 @@
+/-
+  The proofs, one file per codec.
+-/
+
+import Codec.Proofs.Hex
+import Codec.Proofs.Base64
+import Codec.Proofs.Base32
+import Codec.Proofs.Crc32
+import Codec.Proofs.Percent
+import Codec.Proofs.Pem
+import Codec.Proofs.Luhn
+import Codec.Proofs.Iban
diff --git a/Proofs/Base32.lean b/Codec/Proofs/Base32.lean
similarity index 84%
rename from Proofs/Base32.lean
rename to Codec/Proofs/Base32.lean
index 21d018c..53fb028 100644
--- a/Proofs/Base32.lean
+++ b/Codec/Proofs/Base32.lean
@@ -2,15 +2,15 @@
   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
+  statements in `Codec/Spec.lean` for the other codecs. A matching statement
+  for Base32 still has to be added to `Codec/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
+import Codec.Spec.Defs
 
 open Codec
 
@@ -38,7 +38,7 @@ end Codec.Proofs.Base32
 open Codec.Proofs.Base32
 
 /-- Decoding gives back what was encoded. -/
-theorem Spec.base32_decode_encode (bs : List UInt8) :
+theorem Codec.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 =>
@@ -116,12 +116,12 @@ theorem Spec.base32_decode_encode (bs : List UInt8) :
   | 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
+theorem Codec.Spec.base32_rfc4648_vectors :
+    Base32.encode (Codec.Spec.ascii "") = "".toList ∧
+    Base32.encode (Codec.Spec.ascii "f") = "MY======".toList ∧
+    Base32.encode (Codec.Spec.ascii "fo") = "MZXQ====".toList ∧
+    Base32.encode (Codec.Spec.ascii "foo") = "MZXW6===".toList ∧
+    Base32.encode (Codec.Spec.ascii "foob") = "MZXW6YQ=".toList ∧
+    Base32.encode (Codec.Spec.ascii "fooba") = "MZXW6YTB".toList ∧
+    Base32.encode (Codec.Spec.ascii "foobar") = "MZXW6YTBOI======".toList := by
   decide +kernel
diff --git a/Proofs/Base64.lean b/Codec/Proofs/Base64.lean
similarity index 85%
rename from Proofs/Base64.lean
rename to Codec/Proofs/Base64.lean
index 866af02..830cfe9 100644
--- a/Proofs/Base64.lean
+++ b/Codec/Proofs/Base64.lean
@@ -1,9 +1,9 @@
 /-
-  Proofs of the Base64 statements in `Spec.lean`, under the same names.
+  Proofs of the Base64 statements in `Codec/Spec.lean`, under the same names.
 -/
 
 import Codec
-import Spec.Defs
+import Codec.Spec.Defs
 
 open Codec
 
@@ -13,12 +13,12 @@ theorem charLe (a c : Char) : a ≤ c ↔ a.toNat ≤ c.toNat := by
   simp [Char.le_def, UInt32.le_iff_toNat_le]
 
 set_option maxRecDepth 10000 in
-theorem char_tbl : ∀ n : Fin 64, Base64.char n.val = Spec.base64Char n.val := by decide +kernel
+theorem char_tbl : ∀ n : Fin 64, Base64.char n.val = Codec.Spec.base64Char n.val := by decide +kernel
 set_option maxRecDepth 10000 in
 theorem value_tbl : ∀ n : Fin 64, Base64.value (Base64.char n.val) = some n.val := by
   decide +kernel
 
-theorem char_eq {n : Nat} (h : n < 64) : Base64.char n = Spec.base64Char n :=
+theorem char_eq {n : Nat} (h : n < 64) : Base64.char n = Codec.Spec.base64Char n :=
   char_tbl ⟨n, h⟩
 
 theorem value_char {n : Nat} (h : n < 64) : Base64.value (Base64.char n) = some n :=
@@ -94,19 +94,19 @@ end Codec.Proofs.Base64
 
 open Codec.Proofs.Base64
 
-theorem Spec.base64_encode_nil : Base64.encode [] = [] := by
+theorem Codec.Spec.base64_encode_nil : Base64.encode [] = [] := by
   simp [Base64.encode]
 
 /-- Three bytes, the first in the high bits, form one group. -/
-theorem Spec.base64_encode_three (a b c : UInt8) (rest : List UInt8) :
+theorem Codec.Spec.base64_encode_three (a b c : UInt8) (rest : List UInt8) :
     Base64.encode (a :: b :: c :: rest) =
-      Spec.base64Group (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8 + c.toNat) ++
+      Codec.Spec.base64Group (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8 + c.toNat) ++
         Base64.encode rest := by
   rw [Base64.encode.eq_1]
   have ha := a.toNat_lt
   have hb := b.toNat_lt
   have hc := c.toNat_lt
-  simp only [Spec.base64Group, List.cons_append, List.nil_append]
+  simp only [Codec.Spec.base64Group, List.cons_append, List.nil_append]
   have e1 : (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8 + c.toNat) / 2 ^ 18 % 64 =
       (a.toNat * 65536 + b.toNat * 256 + c.toNat) / 262144 := by omega
   have e2 : (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8 + c.toNat) / 2 ^ 12 % 64 =
@@ -120,13 +120,13 @@ theorem Spec.base64_encode_three (a b c : UInt8) (rest : List UInt8) :
 
 /-- Two final bytes: zero bits fill the group, which is cut to three
     characters and padded with one `=`. -/
-theorem Spec.base64_encode_two (a b : UInt8) :
+theorem Codec.Spec.base64_encode_two (a b : UInt8) :
     Base64.encode [a, b] =
-      (Spec.base64Group (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8)).take 3 ++ ['='] := by
+      (Codec.Spec.base64Group (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8)).take 3 ++ ['='] := by
   rw [Base64.encode.eq_2]
   have ha := a.toNat_lt
   have hb := b.toNat_lt
-  simp only [Spec.base64Group, List.take, List.cons_append, List.nil_append]
+  simp only [Codec.Spec.base64Group, List.take, List.cons_append, List.nil_append]
   have e1 : (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8) / 2 ^ 18 % 64 =
       (a.toNat * 65536 + b.toNat * 256) / 262144 := by omega
   have e2 : (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8) / 2 ^ 12 % 64 =
@@ -137,17 +137,17 @@ theorem Spec.base64_encode_two (a b : UInt8) :
 
 /-- One final byte: the group is cut to two characters and padded with
     `==`. -/
-theorem Spec.base64_encode_one (a : UInt8) :
-    Base64.encode [a] = (Spec.base64Group (a.toNat * 2 ^ 16)).take 2 ++ ['=', '='] := by
+theorem Codec.Spec.base64_encode_one (a : UInt8) :
+    Base64.encode [a] = (Codec.Spec.base64Group (a.toNat * 2 ^ 16)).take 2 ++ ['=', '='] := by
   rw [Base64.encode.eq_3]
   have ha := a.toNat_lt
-  simp only [Spec.base64Group, List.take, List.cons_append, List.nil_append]
+  simp only [Codec.Spec.base64Group, List.take, List.cons_append, List.nil_append]
   have e1 : (a.toNat * 2 ^ 16) / 2 ^ 18 % 64 = (a.toNat * 65536) / 262144 := by omega
   have e2 : (a.toNat * 2 ^ 16) / 2 ^ 12 % 64 = (a.toNat * 65536) / 4096 % 64 := by omega
   rw [e1, e2, char_eq (by omega), char_eq (by omega)]
 
 /-- Decoding gives back what was encoded. -/
-theorem Spec.base64_decode_encode (bs : List UInt8) :
+theorem Codec.Spec.base64_decode_encode (bs : List UInt8) :
     Base64.decode (Base64.encode bs) = some bs := by
   induction bs using Base64.encode.induct with
   | case1 a b c rest ih =>
@@ -180,7 +180,7 @@ theorem Spec.base64_decode_encode (bs : List UInt8) :
   | case4 => rfl
 
 /-- Decoding is strict: whatever it accepts is exactly an encoding. -/
-theorem Spec.base64_encode_decode (cs : List Char) (bs : List UInt8) :
+theorem Codec.Spec.base64_encode_decode (cs : List Char) (bs : List UInt8) :
     Base64.decode cs = some bs → Base64.encode bs = cs := by
   induction cs using Base64.decode.induct generalizing bs with
   | case1 =>
@@ -268,12 +268,12 @@ theorem Spec.base64_encode_decode (cs : List Char) (bs : List UInt8) :
     cases h
 
 /-- The test vectors of RFC 4648, section 10. -/
-theorem Spec.base64_rfc4648_vectors :
-    Base64.encode (Spec.ascii "") = "".toList ∧
-    Base64.encode (Spec.ascii "f") = "Zg==".toList ∧
-    Base64.encode (Spec.ascii "fo") = "Zm8=".toList ∧
-    Base64.encode (Spec.ascii "foo") = "Zm9v".toList ∧
-    Base64.encode (Spec.ascii "foob") = "Zm9vYg==".toList ∧
-    Base64.encode (Spec.ascii "fooba") = "Zm9vYmE=".toList ∧
-    Base64.encode (Spec.ascii "foobar") = "Zm9vYmFy".toList := by
+theorem Codec.Spec.base64_rfc4648_vectors :
+    Base64.encode (Codec.Spec.ascii "") = "".toList ∧
+    Base64.encode (Codec.Spec.ascii "f") = "Zg==".toList ∧
+    Base64.encode (Codec.Spec.ascii "fo") = "Zm8=".toList ∧
+    Base64.encode (Codec.Spec.ascii "foo") = "Zm9v".toList ∧
+    Base64.encode (Codec.Spec.ascii "foob") = "Zm9vYg==".toList ∧
+    Base64.encode (Codec.Spec.ascii "fooba") = "Zm9vYmE=".toList ∧
+    Base64.encode (Codec.Spec.ascii "foobar") = "Zm9vYmFy".toList := by
   decide +kernel
diff --git a/Proofs/Crc32.lean b/Codec/Proofs/Crc32.lean
similarity index 87%
rename from Proofs/Crc32.lean
rename to Codec/Proofs/Crc32.lean
index a55562a..8f67aa0 100644
--- a/Proofs/Crc32.lean
+++ b/Codec/Proofs/Crc32.lean
@@ -1,15 +1,15 @@
 /-
-  Proofs of the Crc32 statements in `Spec.lean`, under the same names.
+  Proofs of the Crc32 statements in `Codec/Spec.lean`, under the same names.
 
   The main fact is that the table-driven `Crc32.update` agrees with the
-  bit-at-a-time `Spec.crcByte`. `step` is linear over xor, so `step8` is
+  bit-at-a-time `Codec.Spec.crcByte`. `step` is linear over xor, so `step8` is
   too; eight steps of a value whose low byte is zero just shift it right
   by eight; hence `step8 x = step8 (x &&& 0xFF) ^^^ (x >>> 8)`, and
   `table[i]! = step8 i` for `i < 256`.
 -/
 
 import Codec
-import Spec.Defs
+import Codec.Spec.Defs
 
 open Codec
 
@@ -129,9 +129,9 @@ theorem table_get (i : Nat) (h : i < 256) : table[i]! = step8 i.toUInt32 := by
   simp [table, h]
 
 
-theorem crcBit_eq : Spec.crcBit = step := by
+theorem crcBit_eq : Codec.Spec.crcBit = step := by
   funext c
-  unfold Spec.crcBit step
+  unfold Codec.Spec.crcBit step
   have h1 : c / (2 : UInt32) = c >>> (1 : UInt32) := by
     apply UInt32.toNat_inj.1
     simp [Nat.shiftRight_eq_div_pow]
@@ -146,8 +146,8 @@ theorem crcBit_eq : Spec.crcBit = step := by
   · have h' : ¬ (c % (2 : UInt32) = 1) := fun h' => h (h2.1 h')
     simp only [h, h', ite_false]
 
-theorem crcByte_eq (c : UInt32) (b : UInt8) : Spec.crcByte c b = step8 (c ^^^ b.toUInt32) := by
-  unfold Spec.crcByte
+theorem crcByte_eq (c : UInt32) (b : UInt8) : Codec.Spec.crcByte c b = step8 (c ^^^ b.toUInt32) := by
+  unfold Codec.Spec.crcByte
   rw [crcBit_eq]
   rfl
 
@@ -168,9 +168,9 @@ theorem update_eq (c : UInt32) (b : UInt8) : update c b = step8 (c ^^^ b.toUInt3
     rw [this, UInt32.xor_zero]
   rw [e1, e2, ← step8_split]
 
-theorem le32_eq (x : UInt32) : le32 x = Spec.le32 x := by
+theorem le32_eq (x : UInt32) : le32 x = Codec.Spec.le32 x := by
   have hx : x.toNat < 2 ^ 32 := x.toNat_lt
-  unfold le32 Spec.le32
+  unfold le32 Codec.Spec.le32
   simp only [List.cons.injEq, and_true]
   refine ⟨?_, ?_, ?_, ?_⟩ <;> apply UInt8.toNat_inj.1 <;>
     simp [Nat.shiftRight_eq_div_pow] <;> omega
@@ -181,32 +181,32 @@ end Codec.Proofs.Crc32
 
 open Codec.Proofs.Crc32 in
 /-- The table-driven code computes the CRC-32 defined above. -/
-theorem Spec.crc32_eq (bs : List UInt8) : Crc32.crc32 bs = Spec.crc32 bs := by
-  unfold Crc32.crc32 Spec.crc32
-  have : Crc32.update = Spec.crcByte := by
+theorem Codec.Spec.crc32_eq (bs : List UInt8) : Crc32.crc32 bs = Codec.Spec.crc32 bs := by
+  unfold Crc32.crc32 Codec.Spec.crc32
+  have : Crc32.update = Codec.Spec.crcByte := by
     funext c b; rw [update_eq, crcByte_eq]
   rw [this]
 
 /-- The code gives the standard check value. -/
-theorem Spec.crc32_check : Crc32.crc32 (Spec.ascii "123456789") = 0xCBF43926 := by
-  rw [Spec.crc32_eq]
+theorem Codec.Spec.crc32_check : Crc32.crc32 (Codec.Spec.ascii "123456789") = 0xCBF43926 := by
+  rw [Codec.Spec.crc32_eq]
   decide +kernel
 
 open Codec.Proofs.Crc32 in
 /-- A frame is the message followed by its CRC-32, low byte first. -/
-theorem Spec.frame_layout (bs : List UInt8) :
-    Crc32.frame bs = bs ++ Spec.le32 (Spec.crc32 bs) := by
-  rw [Crc32.frame, Spec.crc32_eq, le32_eq]
+theorem Codec.Spec.frame_layout (bs : List UInt8) :
+    Crc32.frame bs = bs ++ Codec.Spec.le32 (Codec.Spec.crc32 bs) := by
+  rw [Crc32.frame, Codec.Spec.crc32_eq, le32_eq]
 
 open Codec.Proofs.Crc32 in
 /-- Unframing a frame gives back the message. -/
-theorem Spec.unframe_frame (bs : List UInt8) :
+theorem Codec.Spec.unframe_frame (bs : List UInt8) :
     Crc32.unframe (Crc32.frame bs) = some bs := by
   unfold Crc32.unframe Crc32.frame
   simp [le32_length]
 
 /-- Unframing accepts nothing else: whatever it accepts is a frame. -/
-theorem Spec.frame_unframe (fr bs : List UInt8) :
+theorem Codec.Spec.frame_unframe (fr bs : List UInt8) :
     Crc32.unframe fr = some bs → Crc32.frame bs = fr := by
   unfold Crc32.unframe
   intro h
diff --git a/Proofs/Hex.lean b/Codec/Proofs/Hex.lean
similarity index 65%
rename from Proofs/Hex.lean
rename to Codec/Proofs/Hex.lean
index 56afbfd..5ec1413 100644
--- a/Proofs/Hex.lean
+++ b/Codec/Proofs/Hex.lean
@@ -1,22 +1,22 @@
 /-
-  Proofs of the Hex statements in `Spec.lean`, under the same names.
+  Proofs of the Hex statements in `Codec/Spec.lean`, under the same names.
 
   The helper lemmas live in `Codec.Proofs.Hex`. The facts about single
   characters are checked by `decide` over the ASCII range (code points
-  below 128); above it, `Hex.value` gives `none` and `Spec.asciiLower`
+  below 128); above it, `Hex.value` gives `none` and `Codec.Spec.asciiLower`
   changes nothing.
 -/
 
 import Codec
-import Spec.Defs
+import Codec.Spec.Defs
 
 open Codec
 
 namespace Codec.Proofs.Hex
 
-/-- `Hex.digit` and `Spec.hexDigit` agree below 16 (they differ only in the
+/-- `Hex.digit` and `Codec.Spec.hexDigit` agree below 16 (they differ only in the
     default for out-of-range values). -/
-theorem digit_eq_hexDigit : ∀ n : Fin 16, Hex.digit n.val = Spec.hexDigit n.val := by decide
+theorem digit_eq_hexDigit : ∀ n : Fin 16, Hex.digit n.val = Codec.Spec.hexDigit n.val := by decide
 
 theorem value_digit_fin : ∀ n : Fin 16, Hex.value (Hex.digit n.val) = some n.val := by decide
 
@@ -24,11 +24,11 @@ theorem value_digit_fin : ∀ n : Fin 16, Hex.value (Hex.digit n.val) = some n.v
 theorem value_small : ∀ n : Fin 128,
     Hex.value (Char.ofNat n.val) = none ∨
     ∃ h : Fin 16, Hex.value (Char.ofNat n.val) = some h.val ∧
-      Spec.asciiLower (Char.ofNat n.val) = Hex.digit h.val := by decide
+      Codec.Spec.asciiLower (Char.ofNat n.val) = Hex.digit h.val := by decide
 
 /-- On ASCII characters, lowercasing does not change the hex value. -/
 theorem value_lower_small : ∀ n : Fin 128,
-    Hex.value (Spec.asciiLower (Char.ofNat n.val)) = Hex.value (Char.ofNat n.val) := by decide
+    Hex.value (Codec.Spec.asciiLower (Char.ofNat n.val)) = Hex.value (Char.ofNat n.val) := by decide
 
 theorem value_big (c : Char) (h : 128 ≤ c.toNat) : Hex.value c = none := by
   simp only [Hex.value, Char.le_def, UInt32.le_iff_toNat_le, Char.toNat_val]
@@ -41,21 +41,21 @@ theorem value_big (c : Char) (h : 128 ≤ c.toNat) : Hex.value c = none := by
       · omega
       · rfl
 
-theorem lower_big (c : Char) (h : 128 ≤ c.toNat) : Spec.asciiLower c = c := by
-  simp only [Spec.asciiLower, Char.le_def, UInt32.le_iff_toNat_le, Char.toNat_val]
+theorem lower_big (c : Char) (h : 128 ≤ c.toNat) : Codec.Spec.asciiLower c = c := by
+  simp only [Codec.Spec.asciiLower, Char.le_def, UInt32.le_iff_toNat_le, Char.toNat_val]
   simp only [Char.reduceToNat]
   split
   · omega
   · rfl
 
-theorem value_lower (c : Char) : Hex.value (Spec.asciiLower c) = Hex.value c := by
+theorem value_lower (c : Char) : Hex.value (Codec.Spec.asciiLower c) = Hex.value c := by
   by_cases h : c.toNat < 128
   · have := value_lower_small ⟨c.toNat, h⟩
     simpa only [Char.ofNat_toNat] using this
   · rw [lower_big c (by omega)]
 
 theorem value_some (c : Char) (h : Nat) (hv : Hex.value c = some h) :
-    h < 16 ∧ Spec.asciiLower c = Hex.digit h := by
+    h < 16 ∧ Codec.Spec.asciiLower c = Hex.digit h := by
   by_cases hc : c.toNat < 128
   · rcases value_small ⟨c.toNat, hc⟩ with h1 | ⟨k, h1, h2⟩
     · simp only [Char.ofNat_toNat] at h1
@@ -68,7 +68,7 @@ theorem value_some (c : Char) (h : Nat) (hv : Hex.value c = some h) :
   · rw [value_big c (by omega)] at hv
     cases hv
 
-theorem digit_hexDigit (n : Nat) (h : n < 16) : Hex.digit n = Spec.hexDigit n :=
+theorem digit_hexDigit (n : Nat) (h : n < 16) : Hex.digit n = Codec.Spec.hexDigit n :=
   digit_eq_hexDigit ⟨n, h⟩
 
 theorem value_digit (n : Nat) (h : n < 16) : Hex.value (Hex.digit n) = some n :=
@@ -88,18 +88,18 @@ end Codec.Proofs.Hex
 
 open Codec.Proofs.Hex
 
-theorem Spec.hex_encode_nil : Hex.encode [] = [] := rfl
+theorem Codec.Spec.hex_encode_nil : Hex.encode [] = [] := rfl
 
 /-- Each byte is two digits, high half first. -/
-theorem Spec.hex_encode_cons (b : UInt8) (bs : List UInt8) :
+theorem Codec.Spec.hex_encode_cons (b : UInt8) (bs : List UInt8) :
     Hex.encode (b :: bs) =
-      Spec.hexDigit (b.toNat / 16) :: Spec.hexDigit (b.toNat % 16) :: Hex.encode bs := by
+      Codec.Spec.hexDigit (b.toNat / 16) :: Codec.Spec.hexDigit (b.toNat % 16) :: Hex.encode bs := by
   have h1 : b.toNat / 16 < 16 := by have := b.toNat_lt; omega
   have h2 : b.toNat % 16 < 16 := Nat.mod_lt _ (by decide)
   rw [Hex.encode, digit_hexDigit _ h1, digit_hexDigit _ h2]
 
 /-- Decoding gives back what was encoded. -/
-theorem Spec.hex_decode_encode (bs : List UInt8) :
+theorem Codec.Spec.hex_decode_encode (bs : List UInt8) :
     Hex.decode (Hex.encode bs) = some bs := by
   induction bs with
   | nil => rfl
@@ -110,8 +110,8 @@ theorem Spec.hex_decode_encode (bs : List UInt8) :
     simp only [byte_split]
 
 /-- Decoding accepts any mix of upper and lower case. -/
-theorem Spec.hex_decode_any_case (cs : List Char) (bs : List UInt8) :
-    cs.map Spec.asciiLower = Hex.encode bs → Hex.decode cs = some bs := by
+theorem Codec.Spec.hex_decode_any_case (cs : List Char) (bs : List UInt8) :
+    cs.map Codec.Spec.asciiLower = Hex.encode bs → Hex.decode cs = some bs := by
   induction bs generalizing cs with
   | nil =>
     intro h
@@ -140,8 +140,8 @@ theorem Spec.hex_decode_any_case (cs : List Char) (bs : List UInt8) :
 
 /-- Decoding accepts nothing else: whatever it accepts is an encoding,
     up to case. -/
-theorem Spec.hex_encode_decode (cs : List Char) (bs : List UInt8) :
-    Hex.decode cs = some bs → Hex.encode bs = cs.map Spec.asciiLower := by
+theorem Codec.Spec.hex_encode_decode (cs : List Char) (bs : List UInt8) :
+    Hex.decode cs = some bs → Hex.encode bs = cs.map Codec.Spec.asciiLower := by
   induction cs using Hex.decode.induct generalizing bs with
   | case1 =>
     intro h
@@ -174,19 +174,19 @@ theorem Spec.hex_encode_decode (cs : List Char) (bs : List UInt8) :
 /-- The test vectors of RFC 4648, section 10. The RFC writes them in
     uppercase: encoding gives them in lowercase, and decoding reads them
     as the RFC writes them. -/
-theorem Spec.hex_rfc4648_vectors :
-    Hex.encode (Spec.ascii "") = "".toList ∧
-    Hex.encode (Spec.ascii "f") = "66".toList ∧
-    Hex.encode (Spec.ascii "fo") = "666f".toList ∧
-    Hex.encode (Spec.ascii "foo") = "666f6f".toList ∧
-    Hex.encode (Spec.ascii "foob") = "666f6f62".toList ∧
-    Hex.encode (Spec.ascii "fooba") = "666f6f6261".toList ∧
-    Hex.encode (Spec.ascii "foobar") = "666f6f626172".toList ∧
-    Hex.decode "".toList = some (Spec.ascii "") ∧
-    Hex.decode "66".toList = some (Spec.ascii "f") ∧
-    Hex.decode "666F".toList = some (Spec.ascii "fo") ∧
-    Hex.decode "666F6F".toList = some (Spec.ascii "foo") ∧
-    Hex.decode "666F6F62".toList = some (Spec.ascii "foob") ∧
-    Hex.decode "666F6F6261".toList = some (Spec.ascii "fooba") ∧
-    Hex.decode "666F6F626172".toList = some (Spec.ascii "foobar") := by
+theorem Codec.Spec.hex_rfc4648_vectors :
+    Hex.encode (Codec.Spec.ascii "") = "".toList ∧
+    Hex.encode (Codec.Spec.ascii "f") = "66".toList ∧
+    Hex.encode (Codec.Spec.ascii "fo") = "666f".toList ∧
+    Hex.encode (Codec.Spec.ascii "foo") = "666f6f".toList ∧
+    Hex.encode (Codec.Spec.ascii "foob") = "666f6f62".toList ∧
+    Hex.encode (Codec.Spec.ascii "fooba") = "666f6f6261".toList ∧
+    Hex.encode (Codec.Spec.ascii "foobar") = "666f6f626172".toList ∧
+    Hex.decode "".toList = some (Codec.Spec.ascii "") ∧
+    Hex.decode "66".toList = some (Codec.Spec.ascii "f") ∧
+    Hex.decode "666F".toList = some (Codec.Spec.ascii "fo") ∧
+    Hex.decode "666F6F".toList = some (Codec.Spec.ascii "foo") ∧
+    Hex.decode "666F6F62".toList = some (Codec.Spec.ascii "foob") ∧
+    Hex.decode "666F6F6261".toList = some (Codec.Spec.ascii "fooba") ∧
+    Hex.decode "666F6F626172".toList = some (Codec.Spec.ascii "foobar") := by
   decide +kernel
diff --git a/Proofs/Iban.lean b/Codec/Proofs/Iban.lean
similarity index 88%
rename from Proofs/Iban.lean
rename to Codec/Proofs/Iban.lean
index be06ca5..866b9e2 100644
--- a/Proofs/Iban.lean
+++ b/Codec/Proofs/Iban.lean
@@ -1,10 +1,10 @@
 /-
-  Proofs of the Iban statements in `Spec.lean`, under the same names. The
+  Proofs of the Iban statements in `Codec/Spec.lean`, under the same names. The
   helper lemmas live in `Codec.Proofs.Iban`.
 -/
 
 import Codec
-import Spec.Defs
+import Codec.Spec.Defs
 
 open Codec
 
@@ -18,20 +18,20 @@ theorem isDigit_iff (c : Char) : Iban.isDigit c = true ↔ 48 ≤ c.toNat ∧ c.
 theorem isUpper_iff (c : Char) : Iban.isUpper c = true ↔ 65 ≤ c.toNat ∧ c.toNat ≤ 90 := by
   simp [Iban.isUpper, Char.le_def, UInt32.le_iff_toNat_le, Char.toNat_val]
 
-theorem ibanDigit_iff (c : Char) : Spec.ibanDigit c ↔ 48 ≤ c.toNat ∧ c.toNat ≤ 57 := by
-  simp [Spec.ibanDigit, Char.le_def, UInt32.le_iff_toNat_le, Char.toNat_val]
+theorem ibanDigit_iff (c : Char) : Codec.Spec.ibanDigit c ↔ 48 ≤ c.toNat ∧ c.toNat ≤ 57 := by
+  simp [Codec.Spec.ibanDigit, Char.le_def, UInt32.le_iff_toNat_le, Char.toNat_val]
 
-theorem ibanLetter_iff (c : Char) : Spec.ibanLetter c ↔ 65 ≤ c.toNat ∧ c.toNat ≤ 90 := by
-  simp [Spec.ibanLetter, Char.le_def, UInt32.le_iff_toNat_le, Char.toNat_val]
+theorem ibanLetter_iff (c : Char) : Codec.Spec.ibanLetter c ↔ 65 ≤ c.toNat ∧ c.toNat ≤ 90 := by
+  simp [Codec.Spec.ibanLetter, Char.le_def, UInt32.le_iff_toNat_le, Char.toNat_val]
 
-theorem isDigit_digit (c : Char) : Iban.isDigit c = true ↔ Spec.ibanDigit c := by
+theorem isDigit_digit (c : Char) : Iban.isDigit c = true ↔ Codec.Spec.ibanDigit c := by
   rw [isDigit_iff, ibanDigit_iff]
 
-theorem isUpper_letter (c : Char) : Iban.isUpper c = true ↔ Spec.ibanLetter c := by
+theorem isUpper_letter (c : Char) : Iban.isUpper c = true ↔ Codec.Spec.ibanLetter c := by
   rw [isUpper_iff, ibanLetter_iff]
 
-theorem ibanValue_eq (c : Char) : Spec.ibanValue c = Iban.value c := by
-  simp [Spec.ibanValue, Iban.value, Iban.isDigit]
+theorem ibanValue_eq (c : Char) : Codec.Spec.ibanValue c = Iban.value c := by
+  simp [Codec.Spec.ibanValue, Iban.value, Iban.isDigit]
 
 theorem not_digit_of_upper (c : Char) (h : Iban.isUpper c = true) : Iban.isDigit c = false := by
   have := (isUpper_iff c).mp h
@@ -162,7 +162,7 @@ theorem wellShaped_cons4 (c0 c1 k0 k1 : Char) (bban : List Char) :
   simp only [Iban.wellShaped, Bool.and_eq_true, decide_eq_true_eq, List.all_eq_true,
     Bool.or_eq_true, and_assoc]
 
-theorem shape_iff (s : List Char) : Iban.wellShaped s = true ↔ Spec.IbanShape s := by
+theorem shape_iff (s : List Char) : Iban.wellShaped s = true ↔ Codec.Spec.IbanShape s := by
   constructor
   · intro hs
     match s, hs with
@@ -197,8 +197,8 @@ theorem rot_ok (s : List Char) (hs : Iban.wellShaped s = true) :
   | [], hs | [_], hs | [_, _], hs | [_, _, _], hs => simp [Iban.wellShaped] at hs
 
 theorem digits_step (c : Char) (hc : Iban.isDigit c = true ∨ Iban.isUpper c = true) (n : Nat) :
-    (Spec.ibanDigits c).foldl (fun n d => 10 * n + d) n = step n c := by
-  simp only [Spec.ibanDigits, ibanValue_eq, step]
+    (Codec.Spec.ibanDigits c).foldl (fun n d => 10 * n + d) n = step n c := by
+  simp only [Codec.Spec.ibanDigits, ibanValue_eq, step]
   rcases hc with hc | hc
   · have := (isDigit_iff c).mp hc
     rw [pw_of_digit c hc, value_of_digit c hc, ite_eq_left (by omega)]
@@ -212,10 +212,10 @@ theorem digits_step (c : Char) (hc : Iban.isDigit c = true ∨ Iban.isUpper c =
 
 theorem ibanNumber_eq (cs : List Char)
     (h : ∀ c ∈ cs, Iban.isDigit c = true ∨ Iban.isUpper c = true) :
-    Spec.ibanNumber cs = num cs := by
-  unfold Spec.ibanNumber Spec.decimal num
+    Codec.Spec.ibanNumber cs = num cs := by
+  unfold Codec.Spec.ibanNumber Codec.Spec.decimal num
   rw [List.foldl_flatMap]
-  suffices ∀ n, cs.foldl (fun acc x => (Spec.ibanDigits x).foldl (fun n d => 10 * n + d) acc) n =
+  suffices ∀ n, cs.foldl (fun acc x => (Codec.Spec.ibanDigits x).foldl (fun n d => 10 * n + d) acc) n =
       cs.foldl step n from this 0
   induction cs with
   | nil => intro n; rfl
@@ -250,7 +250,7 @@ theorem rot_block (l m r : List Char) (h : l.length + m.length ≤ 4 ∨ 4 ≤ l
 
 /-- Characters of the same kind that differ: equal shift, different values. -/
 theorem kind_cases (a b : Char) (hab : a ≠ b)
-    (hkind : (Spec.ibanDigit a ∧ Spec.ibanDigit b) ∨ (Spec.ibanLetter a ∧ Spec.ibanLetter b)) :
+    (hkind : (Codec.Spec.ibanDigit a ∧ Codec.Spec.ibanDigit b) ∨ (Codec.Spec.ibanLetter a ∧ Codec.Spec.ibanLetter b)) :
     ((pw a = 10 ∧ pw b = 10 ∧ Iban.value a < 10 ∧ Iban.value b < 10) ∨
       (pw a = 100 ∧ pw b = 100)) ∧
       Iban.value a ≠ Iban.value b ∧ Iban.value a < 36 ∧ Iban.value b < 36 := by
@@ -268,9 +268,9 @@ theorem kind_cases (a b : Char) (hab : a ≠ b)
       value_of_not_digit b db]
     omega
 
-theorem valid_spec (s : List Char) : Iban.valid s = true ↔ Spec.IbanValid s := by
+theorem valid_spec (s : List Char) : Iban.valid s = true ↔ Codec.Spec.IbanValid s := by
   rw [valid_iff_num]
-  unfold Spec.IbanValid
+  unfold Codec.Spec.IbanValid
   rw [← shape_iff]
   constructor
   · rintro ⟨hs, hm⟩
@@ -291,12 +291,12 @@ theorem num_two (d1 d2 : Char) (h1 : Iban.isDigit d1 = true) (h2 : Iban.isDigit
 
 theorem zz_digit : Iban.isDigit '0' = true := by decide
 
-/-- `Spec.iban_checkDigits_iff` for a country code of two characters. -/
+/-- `Codec.Spec.iban_checkDigits_iff` for a country code of two characters. -/
 theorem checkDigits_iff_of_length (country bban ck : List Char) (hc : country.length = 2) :
     Iban.checkDigits country bban = some ck ↔
-      ck.length = 2 ∧ (∀ c ∈ ck, Spec.ibanDigit c) ∧
-        2 ≤ Spec.ibanNumber ck ∧ Spec.ibanNumber ck ≤ 98 ∧
-          Spec.IbanValid (country ++ ck ++ bban) := by
+      ck.length = 2 ∧ (∀ c ∈ ck, Codec.Spec.ibanDigit c) ∧
+        2 ≤ Codec.Spec.ibanNumber ck ∧ Codec.Spec.ibanNumber ck ≤ 98 ∧
+          Codec.Spec.IbanValid (country ++ ck ++ bban) := by
   match country, hc with
   | [c0, c1], _ =>
   have h00 : num (bban ++ [c0, c1] ++ ['0', '0']) = num (bban ++ [c0, c1]) * 100 := by
@@ -333,7 +333,7 @@ theorem checkDigits_iff_of_length (country bban ck : List Char) (hc : country.le
         · exact dq
         · exact dt
       obtain ⟨n2, p2⟩ := num_two _ _ dq dt
-      have hn : Spec.ibanNumber [Char.ofNat (48 + (98 - num (bban ++ [c0, c1]) * 100 % 97) / 10),
+      have hn : Codec.Spec.ibanNumber [Char.ofNat (48 + (98 - num (bban ++ [c0, c1]) * 100 % 97) / 10),
           Char.ofNat (48 + (98 - num (bban ++ [c0, c1]) * 100 % 97) % 10)] =
           98 - num (bban ++ [c0, c1]) * 100 % 97 := by
         rw [ibanNumber_eq _ (fun c hc => Or.inl (hok c hc)), n2, value_of_digit _ dq,
@@ -376,14 +376,14 @@ end Codec.Proofs.Iban
 
 open Codec.Proofs.Iban
 
-theorem Spec.iban_valid_iff (s : List Char) : Iban.valid s = true ↔ Spec.IbanValid s :=
+theorem Codec.Spec.iban_valid_iff (s : List Char) : Iban.valid s = true ↔ Codec.Spec.IbanValid s :=
   valid_spec s
 
-theorem Spec.iban_checkDigits_iff (country bban ck : List Char) :
+theorem Codec.Spec.iban_checkDigits_iff (country bban ck : List Char) :
     Iban.checkDigits country bban = some ck ↔
-      country.length = 2 ∧ ck.length = 2 ∧ (∀ c ∈ ck, Spec.ibanDigit c) ∧
-        2 ≤ Spec.ibanNumber ck ∧ Spec.ibanNumber ck ≤ 98 ∧
-          Spec.IbanValid (country ++ ck ++ bban) := by
+      country.length = 2 ∧ ck.length = 2 ∧ (∀ c ∈ ck, Codec.Spec.ibanDigit c) ∧
+        2 ≤ Codec.Spec.ibanNumber ck ∧ Codec.Spec.ibanNumber ck ≤ 98 ∧
+          Codec.Spec.IbanValid (country ++ ck ++ bban) := by
   by_cases hc : country.length = 2
   · simp only [hc, true_and]
     exact checkDigits_iff_of_length country bban ck hc
@@ -391,9 +391,9 @@ theorem Spec.iban_checkDigits_iff (country bban ck : List Char) :
     unfold Iban.checkDigits
     simp [hc]
 
-theorem Spec.iban_substitution (l r : List Char) (a b : Char)
+theorem Codec.Spec.iban_substitution (l r : List Char) (a b : Char)
     (h : Iban.valid (l ++ a :: r) = true) (hab : a ≠ b)
-    (hkind : (Spec.ibanDigit a ∧ Spec.ibanDigit b) ∨ (Spec.ibanLetter a ∧ Spec.ibanLetter b)) :
+    (hkind : (Codec.Spec.ibanDigit a ∧ Codec.Spec.ibanDigit b) ∨ (Codec.Spec.ibanLetter a ∧ Codec.Spec.ibanLetter b)) :
     Iban.valid (l ++ b :: r) = false := by
   obtain ⟨_, h1⟩ := (valid_iff_num _).mp h
   obtain ⟨hp, hv, ha, hb⟩ := kind_cases a b hab hkind
@@ -410,9 +410,9 @@ theorem Spec.iban_substitution (l r : List Char) (a b : Char)
   have h4 := cancel_pws R _ _ h3
   omega
 
-theorem Spec.iban_adjacent_swap (l r : List Char) (a b : Char)
+theorem Codec.Spec.iban_adjacent_swap (l r : List Char) (a b : Char)
     (h : Iban.valid (l ++ a :: b :: r) = true) (hab : a ≠ b)
-    (hkind : (Spec.ibanDigit a ∧ Spec.ibanDigit b) ∨ (Spec.ibanLetter a ∧ Spec.ibanLetter b)) :
+    (hkind : (Codec.Spec.ibanDigit a ∧ Codec.Spec.ibanDigit b) ∨ (Codec.Spec.ibanLetter a ∧ Codec.Spec.ibanLetter b)) :
     Iban.valid (l ++ b :: a :: r) = false := by
   obtain ⟨hs, h1⟩ := (valid_iff_num _).mp h
   obtain ⟨hp, hv, ha, hb⟩ := kind_cases a b hab hkind
@@ -473,7 +473,7 @@ theorem Spec.iban_adjacent_swap (l r : List Char) (a b : Char)
       have h4 := cancel_pws R _ _ h3
       omega
 
-theorem Spec.iban_vectors :
+theorem Codec.Spec.iban_vectors :
     Iban.valid "GB29NWBK60161331926819".toList = true ∧
     Iban.valid "DE89370400440532013000".toList = true ∧
     Iban.valid "FR1420041010050500013M02606".toList = true ∧
diff --git a/Proofs/Luhn.lean b/Codec/Proofs/Luhn.lean
similarity index 90%
rename from Proofs/Luhn.lean
rename to Codec/Proofs/Luhn.lean
index 9903332..d362810 100644
--- a/Proofs/Luhn.lean
+++ b/Codec/Proofs/Luhn.lean
@@ -1,10 +1,10 @@
 /-
-  Proofs of the Luhn statements in `Spec.lean`, under the same names. The
+  Proofs of the Luhn statements in `Codec/Spec.lean`, under the same names. The
   helper lemmas live in `Codec.Proofs.Luhn`.
 -/
 
 import Codec
-import Spec.Defs
+import Codec.Spec.Defs
 
 open Codec
 
@@ -72,15 +72,15 @@ theorem sumFromRight_range (k : Nat) (L : List Nat) :
     rw [hf]
     simp only [Nat.add_zero, List.getD_cons_zero]
 
-theorem sum_eq_luhnSum (ds : List Nat) : Luhn.sum ds = Spec.luhnSum ds := by
+theorem sum_eq_luhnSum (ds : List Nat) : Luhn.sum ds = Codec.Spec.luhnSum ds := by
   have h := sumFromRight_range 0 ds.reverse
   simp only [Nat.zero_mod, Nat.zero_add, List.length_reverse] at h
-  rw [Luhn.sum, Spec.luhnSum]
+  rw [Luhn.sum, Codec.Spec.luhnSum]
   refine Eq.trans h ?_
   congr 1
   apply List.map_congr_left
   intro i _
-  simp [Spec.luhnShare, Luhn.weigh]
+  simp [Codec.Spec.luhnShare, Luhn.weigh]
 
 /-- Changing one digit, at place `k` from the start of the list, changes
     its share only. -/
@@ -124,11 +124,11 @@ end Codec.Proofs.Luhn
 
 open Codec.Proofs.Luhn
 
-theorem Spec.luhn_valid_iff (ds : List Nat) :
-    Luhn.valid ds = true ↔ (∀ d ∈ ds, d ≤ 9) ∧ Spec.luhnSum ds % 10 = 0 := by
+theorem Codec.Spec.luhn_valid_iff (ds : List Nat) :
+    Luhn.valid ds = true ↔ (∀ d ∈ ds, d ≤ 9) ∧ Codec.Spec.luhnSum ds % 10 = 0 := by
   rw [valid_eq, sum_eq_luhnSum]
 
-theorem Spec.luhn_checkDigit (ds : List Nat) (h : ∀ d ∈ ds, d ≤ 9) :
+theorem Codec.Spec.luhn_checkDigit (ds : List Nat) (h : ∀ d ∈ ds, d ≤ 9) :
     Luhn.checkDigit ds ≤ 9 ∧
       ∀ c, c ≤ 9 → (Luhn.valid (ds ++ [c]) = true ↔ c = Luhn.checkDigit ds) := by
   constructor
@@ -152,7 +152,7 @@ theorem Spec.luhn_checkDigit (ds : List Nat) (h : ∀ d ∈ ds, d ≤ 9) :
     · intro h2
       exact ⟨hall, by omega⟩
 
-theorem Spec.luhn_single_error (l r : List Nat) (a b : Nat)
+theorem Codec.Spec.luhn_single_error (l r : List Nat) (a b : Nat)
     (h : Luhn.valid (l ++ a :: r) = true) (hb : b ≤ 9) (hab : a ≠ b) :
     Luhn.valid (l ++ b :: r) = false := by
   rw [valid_eq] at h
@@ -169,7 +169,7 @@ theorem Spec.luhn_single_error (l r : List Nat) (a b : Nat)
     have := weigh_inj (decide (r.length % 2 = 1)) a b ha hb
     omega
 
-theorem Spec.luhn_adjacent_swap (l r : List Nat) (a b : Nat)
+theorem Codec.Spec.luhn_adjacent_swap (l r : List Nat) (a b : Nat)
     (h : Luhn.valid (l ++ a :: b :: r) = true) (hab : a ≠ b)
     (h09 : ¬ (a = 0 ∧ b = 9)) (h90 : ¬ (a = 9 ∧ b = 0)) :
     Luhn.valid (l ++ b :: a :: r) = false := by
@@ -186,13 +186,13 @@ theorem Spec.luhn_adjacent_swap (l r : List Nat) (a b : Nat)
     have hm := swap_digits _ _ (parity_succ_ne r.length) a b ha hb (by omega)
     omega
 
-theorem Spec.luhn_swap_09 (l r : List Nat) :
+theorem Codec.Spec.luhn_swap_09 (l r : List Nat) :
     Luhn.valid (l ++ 0 :: 9 :: r) = Luhn.valid (l ++ 9 :: 0 :: r) := by
   have hs : Luhn.sum (l ++ 0 :: 9 :: r) = Luhn.sum (l ++ 9 :: 0 :: r) := by
     rw [sum_pair, sum_pair l r 9 0, weigh_zero, weigh_zero, weigh_nine, weigh_nine]
   simp [Luhn.valid, hs]
 
-theorem Spec.luhn_vectors :
+theorem Codec.Spec.luhn_vectors :
     Luhn.valid [7, 9, 9, 2, 7, 3, 9, 8, 7, 1, 3] = true ∧
     Luhn.checkDigit [7, 9, 9, 2, 7, 3, 9, 8, 7, 1] = 3 ∧
     Luhn.valid [7, 9, 9, 2, 7, 3, 9, 8, 7, 1, 4] = false ∧
diff --git a/Proofs/Pem.lean b/Codec/Proofs/Pem.lean
similarity index 76%
rename from Proofs/Pem.lean
rename to Codec/Proofs/Pem.lean
index 93da08d..3750bb3 100644
--- a/Proofs/Pem.lean
+++ b/Codec/Proofs/Pem.lean
@@ -1,26 +1,26 @@
 /-
-  Proofs of the PEM statements in `Spec.lean`, under the same names, from
-  the lemmas in `Proofs/Pem/` and the base 64 statements. The vectors are
+  Proofs of the PEM statements in `Codec/Spec.lean`, under the same names, from
+  the lemmas in `Codec/Proofs/Pem/` and the base 64 statements. The vectors are
   checked by evaluation in the kernel.
 -/
 
 import Codec
-import Spec.Defs
-import Proofs.Base64
-import Proofs.Pem.Lines
-import Proofs.Pem.Parts
+import Codec.Spec.Defs
+import Codec.Proofs.Base64
+import Codec.Proofs.Pem.Lines
+import Codec.Proofs.Pem.Parts
 
 open Codec
 
 namespace Codec.Proofs.Pem
 
 theorem pm_text_eq (label : List Char) (data : List UInt8) :
-    (Pem.lines label data).flatMap (· ++ ['\n']) = Spec.pemText label data := by
-  rw [lines_eq, Spec.pemText, List.flatMap_def]
+    (Pem.lines label data).flatMap (· ++ ['\n']) = Codec.Spec.pemText label data := by
+  rw [lines_eq, Codec.Spec.pemText, List.flatMap_def]
 
-theorem pm_mem_lines64 {s l : List Char} {c : Char} (hl : l ∈ Spec.lines64 s) (hc : c ∈ l) :
+theorem pm_mem_lines64 {s l : List Char} {c : Char} (hl : l ∈ Codec.Spec.lines64 s) (hc : c ∈ l) :
     c ∈ s := by
-  unfold Spec.lines64 at hl
+  unfold Codec.Spec.lines64 at hl
   obtain ⟨i, -, rfl⟩ := List.mem_map.mp hl
   exact List.mem_of_mem_drop (List.mem_of_mem_take hc)
 
@@ -59,11 +59,11 @@ theorem pm_encode_ok (bs : List UInt8) : ∀ c ∈ Base64.encode bs, c ≠ '\r'
     intro x hx
     cases hx
 
-theorem pm_labelChar_ok {c : Char} (h : Spec.labelChar c) : c ≠ '\r' ∧ c ≠ '\n' := by
-  unfold Spec.labelChar at h
+theorem pm_labelChar_ok {c : Char} (h : Codec.Spec.labelChar c) : c ≠ '\r' ∧ c ≠ '\n' := by
+  unfold Codec.Spec.labelChar at h
   constructor <;> rintro rfl <;> revert h <;> decide
 
-theorem pm_labelTail_ok {l : List Char} (h : Spec.LabelTail l) :
+theorem pm_labelTail_ok {l : List Char} (h : Codec.Spec.LabelTail l) :
     ∀ c ∈ l, c ≠ '\r' ∧ c ≠ '\n' := by
   induction h with
   | nil => intro x hx; cases hx
@@ -81,7 +81,7 @@ theorem pm_labelTail_ok {l : List Char} (h : Spec.LabelTail l) :
       | head => exact pm_labelChar_ok hc
       | tail _ hx => exact ih x hx
 
-theorem pm_label_ok {l : List Char} (h : Spec.Label l) : ∀ c ∈ l, c ≠ '\r' ∧ c ≠ '\n' := by
+theorem pm_label_ok {l : List Char} (h : Codec.Spec.Label l) : ∀ c ∈ l, c ≠ '\r' ∧ c ≠ '\n' := by
   rcases h with rfl | ⟨c, rest, rfl, hc, ht⟩
   · intro x hx; cases hx
   · intro x hx
@@ -89,11 +89,11 @@ theorem pm_label_ok {l : List Char} (h : Spec.Label l) : ∀ c ∈ l, c ≠ '\r'
     | head => exact pm_labelChar_ok hc
     | tail _ hx => exact pm_labelTail_ok ht x hx
 
-theorem pm_pemLines_ok (label : List Char) (data : List UInt8) (hl : Spec.Label label) :
-    ∀ l ∈ Spec.pemLines label data, '\r' ∉ l ∧ '\n' ∉ l := by
-  have key : ∀ l ∈ Spec.pemLines label data, ∀ c ∈ l, c ≠ '\r' ∧ c ≠ '\n' := by
+theorem pm_pemLines_ok (label : List Char) (data : List UInt8) (hl : Codec.Spec.Label label) :
+    ∀ l ∈ Codec.Spec.pemLines label data, '\r' ∉ l ∧ '\n' ∉ l := by
+  have key : ∀ l ∈ Codec.Spec.pemLines label data, ∀ c ∈ l, c ≠ '\r' ∧ c ≠ '\n' := by
     intro l hl' c hc
-    simp only [Spec.pemLines, List.mem_append, List.mem_singleton] at hl'
+    simp only [Codec.Spec.pemLines, List.mem_append, List.mem_singleton] at hl'
     rcases hl' with (rfl | hl') | rfl
     · simp only [List.mem_append] at hc
       rcases hc with (hc | hc) | hc
@@ -110,21 +110,21 @@ theorem pm_pemLines_ok (label : List Char) (data : List UInt8) (hl : Spec.Label
   exact ⟨fun h => (key l hl' _ h).1 rfl, fun h => (key l hl' _ h).2 rfl⟩
 
 theorem pm_pemLines_ne_nil (label : List Char) (data : List UInt8) :
-    ∀ l ∈ Spec.pemLines label data, l ≠ [] := by
+    ∀ l ∈ Codec.Spec.pemLines label data, l ≠ [] := by
   intro l hl'
-  simp only [Spec.pemLines, List.mem_append, List.mem_singleton] at hl'
+  simp only [Codec.Spec.pemLines, List.mem_append, List.mem_singleton] at hl'
   rcases hl' with (rfl | hl') | rfl
   · simp
   · exact lines64_ne_nil _ l hl'
   · simp
 
 theorem pm_linesEol_lf (ls : List (List Char)) (h : ∀ l ∈ ls, '\r' ∉ l ∧ '\n' ∉ l) :
-    Spec.LinesEol ((ls.map (· ++ ['\n'])).flatten) ls := by
+    Codec.Spec.LinesEol ((ls.map (· ++ ['\n'])).flatten) ls := by
   induction ls with
-  | nil => exact Spec.LinesEol.nil
+  | nil => exact Codec.Spec.LinesEol.nil
   | cons l ls ih =>
     have hl := h l (List.mem_cons_self ..)
-    have := Spec.LinesEol.cons (e := ['\n']) hl.1 hl.2 (Or.inr (Or.inr rfl))
+    have := Codec.Spec.LinesEol.cons (e := ['\n']) hl.1 hl.2 (Or.inr (Or.inr rfl))
       (ih fun l' hl' => h l' (List.mem_cons_of_mem _ hl'))
     simpa only [List.map_cons, List.flatten_cons, List.append_assoc] using this
 
@@ -132,8 +132,8 @@ end Codec.Proofs.Pem
 
 open Codec.Proofs.Pem
 
-theorem Spec.pem_encode_iff (label : List Char) (data : List UInt8) (text : List Char) :
-    Pem.encode label data = some text ↔ Spec.Label label ∧ text = Spec.pemText label data := by
+theorem Codec.Spec.pem_encode_iff (label : List Char) (data : List UInt8) (text : List Char) :
+    Pem.encode label data = some text ↔ Codec.Spec.Label label ∧ text = Codec.Spec.pemText label data := by
   unfold Pem.encode
   rw [← validLabel_iff, pm_text_eq]
   constructor
@@ -146,8 +146,8 @@ theorem Spec.pem_encode_iff (label : List Char) (data : List UInt8) (text : List
   · rintro ⟨hv, rfl⟩
     simp [hv]
 
-theorem Spec.pem_decode_iff (text label : List Char) (data : List UInt8) :
-    Pem.decode text = some (label, data) ↔ Spec.StrictPem text label data := by
+theorem Codec.Spec.pem_decode_iff (text label : List Char) (data : List UInt8) :
+    Pem.decode text = some (label, data) ↔ Codec.Spec.StrictPem text label data := by
   constructor
   · intro h
     cases hs : Pem.splitLines text.length text with
@@ -186,7 +186,7 @@ theorem Spec.pem_decode_iff (text label : List Char) (data : List UInt8) :
                   obtain ⟨rfl, hv, hbody⟩ := hc
                   simp only [Option.some.injEq, Prod.mk.injEq] at h
                   obtain ⟨rfl, rfl⟩ := h
-                  have hflat := Spec.base64_encode_decode _ _ hd
+                  have hflat := Codec.Spec.base64_encode_decode _ _ hd
                   rw [lines64_eq, ← hflat] at hbody
                   rw [labelOf_some _ _ _ hb, labelOf_some _ _ _ he, hbody] at hle
                   exact ⟨(validLabel_iff _).mp hv, hle⟩
@@ -197,24 +197,24 @@ theorem Spec.pem_decode_iff (text label : List Char) (data : List UInt8) :
     unfold Pem.decode
     rw [hs]
     simp only [Option.bind_eq_bind, Option.bind_some]
-    simp only [Spec.pemLines, List.cons_append, List.nil_append, List.getLast?_concat,
+    simp only [Codec.Spec.pemLines, List.cons_append, List.nil_append, List.getLast?_concat,
       List.dropLast_concat, labelOf_append, Option.bind_some, flatten_lines64,
-      Spec.base64_decode_encode, lines64_eq]
+      Codec.Spec.base64_decode_encode, lines64_eq]
     simp only [(validLabel_iff label).mpr hl, and_self, ite_true]
 
-theorem Spec.pem_decode_encode (label : List Char) (data : List UInt8) (text : List Char) :
+theorem Codec.Spec.pem_decode_encode (label : List Char) (data : List UInt8) (text : List Char) :
     Pem.encode label data = some text → Pem.decode text = some (label, data) := by
   intro h
-  obtain ⟨hl, rfl⟩ := (Spec.pem_encode_iff label data text).mp h
-  exact (Spec.pem_decode_iff _ _ _).mpr ⟨hl, pm_linesEol_lf _ (pm_pemLines_ok label data hl)⟩
+  obtain ⟨hl, rfl⟩ := (Codec.Spec.pem_encode_iff label data text).mp h
+  exact (Codec.Spec.pem_decode_iff _ _ _).mpr ⟨hl, pm_linesEol_lf _ (pm_pemLines_ok label data hl)⟩
 
-theorem Spec.pem_vectors :
-    Pem.encode "PUBLIC KEY".toList Spec.figure15 = some
+theorem Codec.Spec.pem_vectors :
+    Pem.encode "PUBLIC KEY".toList Codec.Spec.figure15 = some
       ("-----BEGIN PUBLIC KEY-----\nMHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEn1LlwLN/KBYQRVH6HfIMTzfEqJOVztLe\n".toList ++
        "kLchp2hi78cCaMY81FBlYs8J9l7krc+M4aBeCGYFjba+hiXttJWPL7ydlE+5UG4U\nNkn3Eos8EiZByi9DVsyfy9eejh+8AXgp\n-----END PUBLIC KEY-----\n".toList) ∧
     Pem.decode ("-----BEGIN PUBLIC KEY-----\r\nMHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEn1LlwLN/KBYQRVH6HfIMTzfEqJOVztLe\r\n".toList ++
        "kLchp2hi78cCaMY81FBlYs8J9l7krc+M4aBeCGYFjba+hiXttJWPL7ydlE+5UG4U\r\nNkn3Eos8EiZByi9DVsyfy9eejh+8AXgp\r\n-----END PUBLIC KEY-----\r\n".toList) =
-      some ("PUBLIC KEY".toList, Spec.figure15) ∧
+      some ("PUBLIC KEY".toList, Codec.Spec.figure15) ∧
     Pem.encode "X".toList [] = some "-----BEGIN X-----\n-----END X-----\n".toList ∧
     Pem.decode "-----BEGIN X-----\n-----END X-----\n".toList = some ("X".toList, []) ∧
     Pem.decode "-----BEGIN -----\rAA==\r-----END -----\r".toList = some ([], [0]) ∧
diff --git a/Proofs/Pem/Lines.lean b/Codec/Proofs/Pem/Lines.lean
similarity index 86%
rename from Proofs/Pem/Lines.lean
rename to Codec/Proofs/Pem/Lines.lean
index 1c6d47d..1bc79e9 100644
--- a/Proofs/Pem/Lines.lean
+++ b/Codec/Proofs/Pem/Lines.lean
@@ -1,5 +1,5 @@
 /-
-  Splitting text into lines: `Pem.splitLines` against `Spec.LinesEol`.
+  Splitting text into lines: `Pem.splitLines` against `Codec.Spec.LinesEol`.
 
   `eol` allows CR LF, CR, or LF, so "a" CR LF "b" LF also reads as the
   lines "a", "", "b". `splitLines` takes CR LF as one line end, which is
@@ -8,14 +8,14 @@
 -/
 
 import Codec
-import Spec.Defs
+import Codec.Spec.Defs
 
 open Codec
 
 namespace Codec.Proofs.Pem
 
 theorem ln_takeLine_sound (text l rest : List Char) (h : Pem.takeLine text = some (l, rest)) :
-    ∃ e, Spec.Eol e ∧ text = l ++ e ++ rest ∧ '\r' ∉ l ∧ '\n' ∉ l ∧ rest.length < text.length := by
+    ∃ e, Codec.Spec.Eol e ∧ text = l ++ e ++ rest ∧ '\r' ∉ l ∧ '\n' ∉ l ∧ rest.length < text.length := by
   induction text using Pem.takeLine.induct generalizing l rest with
   | case1 => simp [Pem.takeLine] at h
   | case2 t =>
@@ -48,15 +48,15 @@ theorem ln_takeLine_sound (text l rest : List Char) (h : Pem.takeLine text = som
       · simp only [List.length_cons] at h6 ⊢; omega
 
 theorem splitLines_sound (fuel : Nat) (text : List Char) (ls : List (List Char))
-    (h : Pem.splitLines fuel text = some ls) : Spec.LinesEol text ls := by
+    (h : Pem.splitLines fuel text = some ls) : Codec.Spec.LinesEol text ls := by
   induction fuel generalizing text ls with
   | zero =>
     cases text with
-    | nil => simp [Pem.splitLines] at h; subst h; exact Spec.LinesEol.nil
+    | nil => simp [Pem.splitLines] at h; subst h; exact Codec.Spec.LinesEol.nil
     | cons c t => simp [Pem.splitLines] at h
   | succ f ih =>
     cases text with
-    | nil => simp [Pem.splitLines] at h; subst h; exact Spec.LinesEol.nil
+    | nil => simp [Pem.splitLines] at h; subst h; exact Codec.Spec.LinesEol.nil
     | cons c t =>
       rw [Pem.splitLines.eq_3 _ _ (by simp)] at h
       cases ht : Pem.takeLine (c :: t) with
@@ -71,10 +71,10 @@ theorem splitLines_sound (fuel : Nat) (text : List Char) (ls : List (List Char))
           subst h
           obtain ⟨e, he, heq, h1, h2, _⟩ := ln_takeLine_sound _ _ _ ht
           rw [heq]
-          exact Spec.LinesEol.cons h1 h2 he (ih r ls' hs)
+          exact Codec.Spec.LinesEol.cons h1 h2 he (ih r ls' hs)
 
 theorem ln_takeLine_complete (l e rest : List Char) (h1 : '\r' ∉ l) (h2 : '\n' ∉ l)
-    (he : Spec.Eol e) (hcr : e = ['\r'] → rest.head? ≠ some '\n') :
+    (he : Codec.Spec.Eol e) (hcr : e = ['\r'] → rest.head? ≠ some '\n') :
     Pem.takeLine (l ++ e ++ rest) = some (l, rest) := by
   induction l with
   | nil =>
@@ -93,7 +93,7 @@ theorem ln_takeLine_complete (l e rest : List Char) (h1 : '\r' ∉ l) (h2 : '\n'
     rw [Pem.takeLine.eq_5 _ _ (fun _ h _ => hc1 h) hc1 hc2, ih h1.2 h2.2]
     rfl
 
-theorem ln_linesEol_head (rest : List Char) (ls : List (List Char)) (h : Spec.LinesEol rest ls)
+theorem ln_linesEol_head (rest : List Char) (ls : List (List Char)) (h : Codec.Spec.LinesEol rest ls)
     (hne : ∀ l ∈ ls, l ≠ []) : rest.head? ≠ some '\n' := by
   cases h with
   | nil => simp
@@ -108,7 +108,7 @@ theorem ln_linesEol_head (rest : List Char) (ls : List (List Char)) (h : Spec.Li
       exact h2 (by simp)
 
 theorem splitLines_complete (fuel : Nat) (text : List Char) (ls : List (List Char))
-    (hfuel : text.length ≤ fuel) (h : Spec.LinesEol text ls) (hne : ∀ l ∈ ls, l ≠ []) :
+    (hfuel : text.length ≤ fuel) (h : Codec.Spec.LinesEol text ls) (hne : ∀ l ∈ ls, l ≠ []) :
     Pem.splitLines fuel text = some ls := by
   induction h generalizing fuel with
   | nil => cases fuel <;> simp [Pem.splitLines]
diff --git a/Proofs/Pem/Parts.lean b/Codec/Proofs/Pem/Parts.lean
similarity index 82%
rename from Proofs/Pem/Parts.lean
rename to Codec/Proofs/Pem/Parts.lean
index a6e7712..395d1dc 100644
--- a/Proofs/Pem/Parts.lean
+++ b/Codec/Proofs/Pem/Parts.lean
@@ -4,14 +4,14 @@
 -/
 
 import Codec
-import Spec.Defs
+import Codec.Spec.Defs
 
 open Codec
 
 namespace Codec.Proofs.Pem
 
-theorem pt_isLabelChar_iff (c : Char) : Pem.isLabelChar c = true ↔ Spec.labelChar c := by
-  simp [Pem.isLabelChar, Spec.labelChar]
+theorem pt_isLabelChar_iff (c : Char) : Pem.isLabelChar c = true ↔ Codec.Spec.labelChar c := by
+  simp [Pem.isLabelChar, Codec.Spec.labelChar]
 
 private theorem pt_labelRest_cons (c : Char) (rest : List Char) :
     Pem.labelRest (c :: rest) =
@@ -23,15 +23,15 @@ private theorem pt_labelRest_cons (c : Char) (rest : List Char) :
       else false := by
   rw [Pem.labelRest.eq_def]; rfl
 
-theorem pt_labelRest_iff : ∀ (r : List Char), Pem.labelRest r = true ↔ Spec.LabelTail r
-  | [] => by simp [Pem.labelRest, Spec.LabelTail.nil]
+theorem pt_labelRest_iff : ∀ (r : List Char), Pem.labelRest r = true ↔ Codec.Spec.LabelTail r
+  | [] => by simp [Pem.labelRest, Codec.Spec.LabelTail.nil]
   | c :: rest => by
     have ih := pt_labelRest_iff rest
     rw [pt_labelRest_cons]
     by_cases hc : Pem.isLabelChar c = true
     · rw [ite_eq_left hc, ih]
       constructor
-      · intro h; exact Spec.LabelTail.char ((pt_isLabelChar_iff c).1 hc) h
+      · intro h; exact Codec.Spec.LabelTail.char ((pt_isLabelChar_iff c).1 hc) h
       · intro h
         cases h with
         | char _ h => exact h
@@ -51,7 +51,7 @@ theorem pt_labelRest_iff : ∀ (r : List Char), Pem.labelRest r = true ↔ Spec.
           simp only [Bool.and_eq_true]
           rw [ih', pt_isLabelChar_iff]
           constructor
-          · rintro ⟨h1, h2⟩; exact Spec.LabelTail.sep hs h1 h2
+          · rintro ⟨h1, h2⟩; exact Codec.Spec.LabelTail.sep hs h1 h2
           · intro h
             cases h with
             | char h _ => exact absurd ((pt_isLabelChar_iff c).2 h) hc
@@ -63,26 +63,26 @@ theorem pt_labelRest_iff : ∀ (r : List Char), Pem.labelRest r = true ↔ Spec.
         | char h _ => exact hc ((pt_isLabelChar_iff c).2 h)
         | sep h _ _ => exact hs h
 
-theorem validLabel_iff (l : List Char) : Pem.validLabel l = true ↔ Spec.Label l := by
+theorem validLabel_iff (l : List Char) : Pem.validLabel l = true ↔ Codec.Spec.Label l := by
   cases l with
-  | nil => simp [Pem.validLabel, Spec.Label]
+  | nil => simp [Pem.validLabel, Codec.Spec.Label]
   | cons c rest =>
-    simp only [Pem.validLabel, Bool.and_eq_true, pt_isLabelChar_iff, pt_labelRest_iff, Spec.Label]
+    simp only [Pem.validLabel, Bool.and_eq_true, pt_isLabelChar_iff, pt_labelRest_iff, Codec.Spec.Label]
     constructor
     · intro h; exact Or.inr ⟨c, rest, rfl, h⟩
     · rintro (h | ⟨c', rest', h, h1, h2⟩)
       · cases h
       · cases h; exact ⟨h1, h2⟩
 
-theorem pt_spec_lines64_nil : Spec.lines64 [] = [] := by
-  simp [Spec.lines64]
+theorem pt_spec_lines64_nil : Codec.Spec.lines64 [] = [] := by
+  simp [Codec.Spec.lines64]
 
 theorem pt_spec_lines64_cons (s : List Char) (h : s ≠ []) :
-    Spec.lines64 s = s.take 64 :: Spec.lines64 (s.drop 64) := by
+    Codec.Spec.lines64 s = s.take 64 :: Codec.Spec.lines64 (s.drop 64) := by
   have hlen : 0 < s.length := List.length_pos_iff.2 h
   have hk : (s.length + 63) / 64 = ((s.drop 64).length + 63) / 64 + 1 := by
     rw [List.length_drop]; omega
-  unfold Spec.lines64
+  unfold Codec.Spec.lines64
   rw [hk, List.range_succ_eq_map]
   simp only [List.map_cons, List.map_map, Nat.mul_zero, List.drop_zero]
   congr 1
@@ -93,7 +93,7 @@ theorem pt_spec_lines64_cons (s : List Char) (h : s ≠ []) :
   omega
 
 theorem pt_lines64_fuel : ∀ (fuel : Nat) (s : List Char), s.length ≤ fuel →
-    Pem.lines64 fuel s = Spec.lines64 s
+    Pem.lines64 fuel s = Codec.Spec.lines64 s
   | _, [], _ => by simp [Pem.lines64, pt_spec_lines64_nil]
   | 0, _ :: _, h => by simp at h
   | fuel + 1, c :: cs, h => by
@@ -101,11 +101,11 @@ theorem pt_lines64_fuel : ∀ (fuel : Nat) (s : List Char), s.length ≤ fuel 
     · rw [pt_lines64_fuel fuel _ (by simp at h ⊢; omega)]
     · exact List.cons_ne_nil c cs
 
-theorem lines64_eq (s : List Char) : Pem.lines64 s.length s = Spec.lines64 s :=
+theorem lines64_eq (s : List Char) : Pem.lines64 s.length s = Codec.Spec.lines64 s :=
   pt_lines64_fuel _ _ (Nat.le_refl _)
 
 theorem pt_lines64_fuel_props : ∀ (fuel : Nat) (s : List Char), s.length ≤ fuel →
-    (Spec.lines64 s).flatten = s ∧ ∀ l ∈ Spec.lines64 s, l ≠ []
+    (Codec.Spec.lines64 s).flatten = s ∧ ∀ l ∈ Codec.Spec.lines64 s, l ≠ []
   | _, [], _ => by simp [pt_spec_lines64_nil]
   | 0, _ :: _, h => by simp at h
   | fuel + 1, c :: cs, h => by
@@ -118,15 +118,15 @@ theorem pt_lines64_fuel_props : ∀ (fuel : Nat) (s : List Char), s.length ≤ f
       · subst hl; simp
       · exact ih.2 l hl
 
-theorem flatten_lines64 (s : List Char) : (Spec.lines64 s).flatten = s :=
+theorem flatten_lines64 (s : List Char) : (Codec.Spec.lines64 s).flatten = s :=
   (pt_lines64_fuel_props s.length s (Nat.le_refl _)).1
 
-theorem lines64_ne_nil (s : List Char) : ∀ l ∈ Spec.lines64 s, l ≠ [] :=
+theorem lines64_ne_nil (s : List Char) : ∀ l ∈ Codec.Spec.lines64 s, l ≠ [] :=
   (pt_lines64_fuel_props s.length s (Nat.le_refl _)).2
 
 theorem lines_eq (label : List Char) (data : List UInt8) :
-    Pem.lines label data = Spec.pemLines label data := by
-  unfold Pem.lines Pem.beginLine Pem.endLine Spec.pemLines
+    Pem.lines label data = Codec.Spec.pemLines label data := by
+  unfold Pem.lines Pem.beginLine Pem.endLine Codec.Spec.pemLines
   dsimp only
   rw [lines64_eq]
   rfl
diff --git a/Proofs/Percent.lean b/Codec/Proofs/Percent.lean
similarity index 65%
rename from Proofs/Percent.lean
rename to Codec/Proofs/Percent.lean
index 5786e07..0034e4c 100644
--- a/Proofs/Percent.lean
+++ b/Codec/Proofs/Percent.lean
@@ -1,11 +1,11 @@
 /-
-  Proofs of the percent-encoding statements in `Spec.lean`, under the
+  Proofs of the percent-encoding statements in `Codec/Spec.lean`, under the
   same names. The helper lemmas live in `Codec.Proofs.Percent`.
 -/
 
 import Codec
-import Spec.Defs
-import Proofs.Hex
+import Codec.Spec.Defs
+import Codec.Proofs.Hex
 
 open Codec
 
@@ -14,9 +14,9 @@ namespace Codec.Proofs.Percent
 open Codec.Proofs.Hex
 
 /-- `Percent.unreserved` picks out exactly the characters of
-    `Spec.unreservedChars`. -/
+    `Codec.Spec.unreservedChars`. -/
 theorem unreserved_fin : ∀ b : Fin 256,
-    Percent.unreserved b.val.toUInt8 = true ↔ Char.ofNat b.val ∈ Spec.unreservedChars := by
+    Percent.unreserved b.val.toUInt8 = true ↔ Char.ofNat b.val ∈ Codec.Spec.unreservedChars := by
   decide +kernel
 
 /-- An unreserved byte is an ASCII character other than `%`, whose code is the byte. -/
@@ -25,14 +25,14 @@ theorem unreserved_char_fin : ∀ b : Fin 256, Percent.unreserved b.val.toUInt8
       (Char.ofNat b.val).toNat.toUInt8 = b.val.toUInt8 := by
   decide +kernel
 
-theorem upper_fin : ∀ n : Fin 16, Percent.upper n.val = Spec.upperHexDigits.getD n.val '?' := by
+theorem upper_fin : ∀ n : Fin 16, Percent.upper n.val = Codec.Spec.upperHexDigits.getD n.val '?' := by
   decide
 
-theorem lower_upper_fin : ∀ n : Fin 16, Spec.asciiLower (Percent.upper n.val) = Spec.hexDigit n.val := by
+theorem lower_upper_fin : ∀ n : Fin 16, Codec.Spec.asciiLower (Percent.upper n.val) = Codec.Spec.hexDigit n.val := by
   decide
 
 theorem unreserved_iff (b : UInt8) :
-    Percent.unreserved b = true ↔ Char.ofNat b.toNat ∈ Spec.unreservedChars := by
+    Percent.unreserved b = true ↔ Char.ofNat b.toNat ∈ Codec.Spec.unreservedChars := by
   have := unreserved_fin ⟨b.toNat, b.toNat_lt⟩
   simpa using this
 
@@ -43,17 +43,17 @@ theorem unreserved_char (b : UInt8) (h : Percent.unreserved b = true) :
   simp only [Nat.toUInt8_eq, UInt8.ofNat_toNat] at this
   simpa using this h
 
-theorem upper_eq (n : Nat) (h : n < 16) : Percent.upper n = Spec.upperHexDigits.getD n '?' :=
+theorem upper_eq (n : Nat) (h : n < 16) : Percent.upper n = Codec.Spec.upperHexDigits.getD n '?' :=
   upper_fin ⟨n, h⟩
 
-theorem lower_upper (n : Nat) (h : n < 16) : Spec.asciiLower (Percent.upper n) = Spec.hexDigit n :=
+theorem lower_upper (n : Nat) (h : n < 16) : Codec.Spec.asciiLower (Percent.upper n) = Codec.Spec.hexDigit n :=
   lower_upper_fin ⟨n, h⟩
 
 theorem encode_cons (b : UInt8) (bs : List UInt8) :
-    Percent.encode (b :: bs) = Spec.pctByte b ++ Percent.encode bs := by
+    Percent.encode (b :: bs) = Codec.Spec.pctByte b ++ Percent.encode bs := by
   have h1 : b.toNat / 16 < 16 := by have := b.toNat_lt; omega
   have h2 : b.toNat % 16 < 16 := Nat.mod_lt _ (by decide)
-  rw [Percent.encode, Spec.pctByte]
+  rw [Percent.encode, Codec.Spec.pctByte]
   by_cases hu : Percent.unreserved b = true
   · rw [ite_eq_left hu, ite_eq_left ((unreserved_iff b).mp hu)]
     rfl
@@ -61,13 +61,13 @@ theorem encode_cons (b : UInt8) (bs : List UInt8) :
     rfl
 
 theorem decode_reads (cs : List Char) (bs : List UInt8) :
-    Percent.decode cs = some bs → Spec.PctReads cs bs := by
+    Percent.decode cs = some bs → Codec.Spec.PctReads cs bs := by
   induction cs using Percent.decode.induct generalizing bs with
   | case1 =>
     intro hd
     rw [Percent.decode.eq_1] at hd
     cases hd
-    exact Spec.PctReads.nil
+    exact Codec.Spec.PctReads.nil
   | case2 hi lo rest h l tail hrest hl hh ih =>
     intro hd
     rw [Percent.decode.eq_2, hh, hl, hrest] at hd
@@ -79,7 +79,7 @@ theorem decode_reads (cs : List Char) (bs : List UInt8) :
       rw [byte_toNat h l h16 l16]; omega
     have e2 : (h * 16 + l).toUInt8.toNat % 16 = l := by
       rw [byte_toNat h l h16 l16]; omega
-    refine Spec.PctReads.escape ?_ ?_ (ih tail hrest)
+    refine Codec.Spec.PctReads.escape ?_ ?_ (ih tail hrest)
     · rw [e1, eh, digit_hexDigit h h16]
     · rw [e2, el, digit_hexDigit l l16]
   | case3 hi lo rest hne ih =>
@@ -101,13 +101,13 @@ theorem decode_reads (cs : List Char) (bs : List UInt8) :
       rw [hr] at hd
       injection hd with hd
       subst hd
-      exact Spec.PctReads.char hne2 hlt (ih tail hr)
+      exact Codec.Spec.PctReads.char hne2 hlt (ih tail hr)
   | case6 c rest hne1 hne2 hlt =>
     intro hd
     rw [Percent.decode.eq_4 c rest hne1 hne2, ite_eq_right hlt] at hd
     cases hd
 
-theorem reads_decode (cs : List Char) (bs : List UInt8) (h : Spec.PctReads cs bs) :
+theorem reads_decode (cs : List Char) (bs : List UInt8) (h : Codec.Spec.PctReads cs bs) :
     Percent.decode cs = some bs := by
   induction h with
   | nil => rw [Percent.decode.eq_1]
@@ -124,57 +124,57 @@ theorem reads_decode (cs : List Char) (bs : List UInt8) (h : Spec.PctReads cs bs
     rw [Percent.decode.eq_4 c rest (fun _ _ _ h _ => hne h) hne, ite_eq_left hlt, ih]
     rfl
 
-theorem encode_reads (bs : List UInt8) : Spec.PctReads (Percent.encode bs) bs := by
+theorem encode_reads (bs : List UInt8) : Codec.Spec.PctReads (Percent.encode bs) bs := by
   induction bs with
-  | nil => exact Spec.PctReads.nil
+  | nil => exact Codec.Spec.PctReads.nil
   | cons b bs ih =>
     rw [Percent.encode]
     by_cases hu : Percent.unreserved b = true
     · rw [ite_eq_left hu]
       obtain ⟨hne, hlt, hb⟩ := unreserved_char b hu
-      have := Spec.PctReads.char hne hlt ih
+      have := Codec.Spec.PctReads.char hne hlt ih
       rwa [hb] at this
     · rw [ite_eq_right hu]
       have h1 : b.toNat / 16 < 16 := by have := b.toNat_lt; omega
       have h2 : b.toNat % 16 < 16 := Nat.mod_lt _ (by decide)
-      exact Spec.PctReads.escape (lower_upper _ h1) (lower_upper _ h2) ih
+      exact Codec.Spec.PctReads.escape (lower_upper _ h1) (lower_upper _ h2) ih
 
 end Codec.Proofs.Percent
 
 open Codec.Proofs.Percent
 
-theorem Spec.percent_encode_eq (bs : List UInt8) :
-    Percent.encode bs = Spec.pctEncode bs := by
+theorem Codec.Spec.percent_encode_eq (bs : List UInt8) :
+    Percent.encode bs = Codec.Spec.pctEncode bs := by
   induction bs with
   | nil => rfl
   | cons b bs ih =>
-    rw [encode_cons, ih, Spec.pctEncode, Spec.pctEncode, List.map_cons, List.flatten_cons]
+    rw [encode_cons, ih, Codec.Spec.pctEncode, Codec.Spec.pctEncode, List.map_cons, List.flatten_cons]
 
-theorem Spec.percent_decode_iff (cs : List Char) (bs : List UInt8) :
-    Percent.decode cs = some bs ↔ Spec.PctReads cs bs :=
+theorem Codec.Spec.percent_decode_iff (cs : List Char) (bs : List UInt8) :
+    Percent.decode cs = some bs ↔ Codec.Spec.PctReads cs bs :=
   ⟨decode_reads cs bs, reads_decode cs bs⟩
 
-theorem Spec.percent_decode_encode (bs : List UInt8) :
+theorem Codec.Spec.percent_decode_encode (bs : List UInt8) :
     Percent.decode (Percent.encode bs) = some bs :=
   reads_decode _ _ (encode_reads bs)
 
-theorem Spec.percent_vectors :
+theorem Codec.Spec.percent_vectors :
     Percent.encode [0x20] = "%20".toList ∧
-    Percent.encode (Spec.ascii "A") = "A".toList ∧
+    Percent.encode (Codec.Spec.ascii "A") = "A".toList ∧
     Percent.encode [0xC3, 0x80] = "%C3%80".toList ∧
     Percent.encode [0xE3, 0x82, 0xA2] = "%E3%82%A2".toList ∧
-    Percent.encode (Spec.ascii "-._~") = "-._~".toList ∧
-    Percent.encode (Spec.ascii "Laguna Beach") = "Laguna%20Beach".toList ∧
-    Percent.encode (Spec.ascii "%:/?#[]@!$&'()*+,;=") =
+    Percent.encode (Codec.Spec.ascii "-._~") = "-._~".toList ∧
+    Percent.encode (Codec.Spec.ascii "Laguna Beach") = "Laguna%20Beach".toList ∧
+    Percent.encode (Codec.Spec.ascii "%:/?#[]@!$&'()*+,;=") =
       "%25%3A%2F%3F%23%5B%5D%40%21%24%26%27%28%29%2A%2B%2C%3B%3D".toList ∧
     Percent.decode "%C3%80".toList = some [0xC3, 0x80] ∧
     Percent.decode "%e3%82%a2".toList = some [0xE3, 0x82, 0xA2] ∧
-    Percent.decode "%7E".toList = some (Spec.ascii "~") ∧
-    Percent.decode "%63/%7bfoo%7d".toList = some (Spec.ascii "c/{foo}") ∧
-    Percent.decode "%3a".toList = some (Spec.ascii ":") ∧
-    Percent.decode "%3A".toList = some (Spec.ascii ":") ∧
-    Percent.decode "a+b c".toList = some (Spec.ascii "a+b c") ∧
-    Percent.decode "%252E".toList = some (Spec.ascii "%2E") ∧
+    Percent.decode "%7E".toList = some (Codec.Spec.ascii "~") ∧
+    Percent.decode "%63/%7bfoo%7d".toList = some (Codec.Spec.ascii "c/{foo}") ∧
+    Percent.decode "%3a".toList = some (Codec.Spec.ascii ":") ∧
+    Percent.decode "%3A".toList = some (Codec.Spec.ascii ":") ∧
+    Percent.decode "a+b c".toList = some (Codec.Spec.ascii "a+b c") ∧
+    Percent.decode "%252E".toList = some (Codec.Spec.ascii "%2E") ∧
     Percent.decode "%".toList = none ∧
     Percent.decode "%2".toList = none ∧
     Percent.decode "%zz".toList = none ∧
diff --git a/Spec.lean b/Codec/Spec.lean
similarity index 61%
rename from Spec.lean
rename to Codec/Spec.lean
index 69a60bd..0d4292f 100644
--- a/Spec.lean
+++ b/Codec/Spec.lean
@@ -2,7 +2,7 @@
   The specification as Lean statements: the challenge file.
 
   A reviewer who did not write this file approves it, and `bar.toml`
-  records the hash it had then. The proofs live in `Proofs.lean`, under
+  records the hash it had then. The proofs live in `Codec/Proofs.lean`, under
   the same names; `lake comparator` checks that each one proves exactly
   the statement written here. The `sorry` below is expected in this file
   only.
@@ -12,7 +12,7 @@
 -/
 
 import Codec
-import Spec.Defs
+import Codec.Spec.Defs
 
 open Codec
 
@@ -23,108 +23,108 @@ first, as Python's `bytes.hex()` writes it: RFC 4648 base 16 in
 lowercase. Decoding reads digits in either case and accepts nothing
 else. -/
 
-theorem Spec.hex_encode_nil : Hex.encode [] = [] := sorry
+theorem Codec.Spec.hex_encode_nil : Hex.encode [] = [] := sorry
 
 /-- Each byte is two digits, high half first. -/
-theorem Spec.hex_encode_cons (b : UInt8) (bs : List UInt8) :
+theorem Codec.Spec.hex_encode_cons (b : UInt8) (bs : List UInt8) :
     Hex.encode (b :: bs) =
-      Spec.hexDigit (b.toNat / 16) :: Spec.hexDigit (b.toNat % 16) :: Hex.encode bs := sorry
+      Codec.Spec.hexDigit (b.toNat / 16) :: Codec.Spec.hexDigit (b.toNat % 16) :: Hex.encode bs := sorry
 
 /-- Decoding gives back what was encoded. -/
-theorem Spec.hex_decode_encode (bs : List UInt8) :
+theorem Codec.Spec.hex_decode_encode (bs : List UInt8) :
     Hex.decode (Hex.encode bs) = some bs := sorry
 
 /-- Decoding accepts any mix of upper and lower case. -/
-theorem Spec.hex_decode_any_case (cs : List Char) (bs : List UInt8) :
-    cs.map Spec.asciiLower = Hex.encode bs → Hex.decode cs = some bs := sorry
+theorem Codec.Spec.hex_decode_any_case (cs : List Char) (bs : List UInt8) :
+    cs.map Codec.Spec.asciiLower = Hex.encode bs → Hex.decode cs = some bs := sorry
 
 /-- Decoding accepts nothing else: whatever it accepts is an encoding,
     up to case. -/
-theorem Spec.hex_encode_decode (cs : List Char) (bs : List UInt8) :
-    Hex.decode cs = some bs → Hex.encode bs = cs.map Spec.asciiLower := sorry
+theorem Codec.Spec.hex_encode_decode (cs : List Char) (bs : List UInt8) :
+    Hex.decode cs = some bs → Hex.encode bs = cs.map Codec.Spec.asciiLower := sorry
 
 /-- The test vectors of RFC 4648, section 10. The RFC writes them in
     uppercase: encoding gives them in lowercase, and decoding reads them
     as the RFC writes them. -/
-theorem Spec.hex_rfc4648_vectors :
-    Hex.encode (Spec.ascii "") = "".toList ∧
-    Hex.encode (Spec.ascii "f") = "66".toList ∧
-    Hex.encode (Spec.ascii "fo") = "666f".toList ∧
-    Hex.encode (Spec.ascii "foo") = "666f6f".toList ∧
-    Hex.encode (Spec.ascii "foob") = "666f6f62".toList ∧
-    Hex.encode (Spec.ascii "fooba") = "666f6f6261".toList ∧
-    Hex.encode (Spec.ascii "foobar") = "666f6f626172".toList ∧
-    Hex.decode "".toList = some (Spec.ascii "") ∧
-    Hex.decode "66".toList = some (Spec.ascii "f") ∧
-    Hex.decode "666F".toList = some (Spec.ascii "fo") ∧
-    Hex.decode "666F6F".toList = some (Spec.ascii "foo") ∧
-    Hex.decode "666F6F62".toList = some (Spec.ascii "foob") ∧
-    Hex.decode "666F6F6261".toList = some (Spec.ascii "fooba") ∧
-    Hex.decode "666F6F626172".toList = some (Spec.ascii "foobar") := sorry
+theorem Codec.Spec.hex_rfc4648_vectors :
+    Hex.encode (Codec.Spec.ascii "") = "".toList ∧
+    Hex.encode (Codec.Spec.ascii "f") = "66".toList ∧
+    Hex.encode (Codec.Spec.ascii "fo") = "666f".toList ∧
+    Hex.encode (Codec.Spec.ascii "foo") = "666f6f".toList ∧
+    Hex.encode (Codec.Spec.ascii "foob") = "666f6f62".toList ∧
+    Hex.encode (Codec.Spec.ascii "fooba") = "666f6f6261".toList ∧
+    Hex.encode (Codec.Spec.ascii "foobar") = "666f6f626172".toList ∧
+    Hex.decode "".toList = some (Codec.Spec.ascii "") ∧
+    Hex.decode "66".toList = some (Codec.Spec.ascii "f") ∧
+    Hex.decode "666F".toList = some (Codec.Spec.ascii "fo") ∧
+    Hex.decode "666F6F".toList = some (Codec.Spec.ascii "foo") ∧
+    Hex.decode "666F6F62".toList = some (Codec.Spec.ascii "foob") ∧
+    Hex.decode "666F6F6261".toList = some (Codec.Spec.ascii "fooba") ∧
+    Hex.decode "666F6F626172".toList = some (Codec.Spec.ascii "foobar") := sorry
 
 /-! ## Base 64
 
 RFC 4648, section 4. -/
 
-theorem Spec.base64_encode_nil : Base64.encode [] = [] := sorry
+theorem Codec.Spec.base64_encode_nil : Base64.encode [] = [] := sorry
 
 /-- Three bytes, the first in the high bits, form one group. -/
-theorem Spec.base64_encode_three (a b c : UInt8) (rest : List UInt8) :
+theorem Codec.Spec.base64_encode_three (a b c : UInt8) (rest : List UInt8) :
     Base64.encode (a :: b :: c :: rest) =
-      Spec.base64Group (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8 + c.toNat) ++
+      Codec.Spec.base64Group (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8 + c.toNat) ++
         Base64.encode rest := sorry
 
 /-- Two final bytes: zero bits fill the group, which is cut to three
     characters and padded with one `=`. -/
-theorem Spec.base64_encode_two (a b : UInt8) :
+theorem Codec.Spec.base64_encode_two (a b : UInt8) :
     Base64.encode [a, b] =
-      (Spec.base64Group (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8)).take 3 ++ ['='] := sorry
+      (Codec.Spec.base64Group (a.toNat * 2 ^ 16 + b.toNat * 2 ^ 8)).take 3 ++ ['='] := sorry
 
 /-- One final byte: the group is cut to two characters and padded with
     `==`. -/
-theorem Spec.base64_encode_one (a : UInt8) :
-    Base64.encode [a] = (Spec.base64Group (a.toNat * 2 ^ 16)).take 2 ++ ['=', '='] := sorry
+theorem Codec.Spec.base64_encode_one (a : UInt8) :
+    Base64.encode [a] = (Codec.Spec.base64Group (a.toNat * 2 ^ 16)).take 2 ++ ['=', '='] := sorry
 
 /-- Decoding gives back what was encoded. -/
-theorem Spec.base64_decode_encode (bs : List UInt8) :
+theorem Codec.Spec.base64_decode_encode (bs : List UInt8) :
     Base64.decode (Base64.encode bs) = some bs := sorry
 
 /-- Decoding is strict: whatever it accepts is exactly an encoding. -/
-theorem Spec.base64_encode_decode (cs : List Char) (bs : List UInt8) :
+theorem Codec.Spec.base64_encode_decode (cs : List Char) (bs : List UInt8) :
     Base64.decode cs = some bs → Base64.encode bs = cs := sorry
 
 /-- The test vectors of RFC 4648, section 10. -/
-theorem Spec.base64_rfc4648_vectors :
-    Base64.encode (Spec.ascii "") = "".toList ∧
-    Base64.encode (Spec.ascii "f") = "Zg==".toList ∧
-    Base64.encode (Spec.ascii "fo") = "Zm8=".toList ∧
-    Base64.encode (Spec.ascii "foo") = "Zm9v".toList ∧
-    Base64.encode (Spec.ascii "foob") = "Zm9vYg==".toList ∧
-    Base64.encode (Spec.ascii "fooba") = "Zm9vYmE=".toList ∧
-    Base64.encode (Spec.ascii "foobar") = "Zm9vYmFy".toList := sorry
+theorem Codec.Spec.base64_rfc4648_vectors :
+    Base64.encode (Codec.Spec.ascii "") = "".toList ∧
+    Base64.encode (Codec.Spec.ascii "f") = "Zg==".toList ∧
+    Base64.encode (Codec.Spec.ascii "fo") = "Zm8=".toList ∧
+    Base64.encode (Codec.Spec.ascii "foo") = "Zm9v".toList ∧
+    Base64.encode (Codec.Spec.ascii "foob") = "Zm9vYg==".toList ∧
+    Base64.encode (Codec.Spec.ascii "fooba") = "Zm9vYmE=".toList ∧
+    Base64.encode (Codec.Spec.ascii "foobar") = "Zm9vYmFy".toList := sorry
 
 /-! ## CRC-32
 
 The CRC-32 of ISO 3309, ITU-T V.42, and RFC 1952 (gzip), defined one bit
 at a time. -/
 
-/-- The table-driven code computes `Spec.crc32`, the CRC-32 defined one
+/-- The table-driven code computes `Codec.Spec.crc32`, the CRC-32 defined one
     bit at a time in `Spec/Defs.lean`. -/
-theorem Spec.crc32_eq (bs : List UInt8) : Crc32.crc32 bs = Spec.crc32 bs := sorry
+theorem Codec.Spec.crc32_eq (bs : List UInt8) : Crc32.crc32 bs = Codec.Spec.crc32 bs := sorry
 
 /-- The code gives the standard check value. -/
-theorem Spec.crc32_check : Crc32.crc32 (Spec.ascii "123456789") = 0xCBF43926 := sorry
+theorem Codec.Spec.crc32_check : Crc32.crc32 (Codec.Spec.ascii "123456789") = 0xCBF43926 := sorry
 
 /-- A frame is the message followed by its CRC-32, low byte first. -/
-theorem Spec.frame_layout (bs : List UInt8) :
-    Crc32.frame bs = bs ++ Spec.le32 (Spec.crc32 bs) := sorry
+theorem Codec.Spec.frame_layout (bs : List UInt8) :
+    Crc32.frame bs = bs ++ Codec.Spec.le32 (Codec.Spec.crc32 bs) := sorry
 
 /-- Unframing a frame gives back the message. -/
-theorem Spec.unframe_frame (bs : List UInt8) :
+theorem Codec.Spec.unframe_frame (bs : List UInt8) :
     Crc32.unframe (Crc32.frame bs) = some bs := sorry
 
 /-- Unframing accepts nothing else: whatever it accepts is a frame. -/
-theorem Spec.frame_unframe (fr bs : List UInt8) :
+theorem Codec.Spec.frame_unframe (fr bs : List UInt8) :
     Crc32.unframe fr = some bs → Crc32.frame bs = fr := sorry
 
 /-! ## Percent-encoding
@@ -137,17 +137,17 @@ case, and decodes once. -/
 /-- The encoder writes each byte as sections 2.1 and 2.3 tell producers
     to: an unreserved character as itself, any other byte as `%` and
     two uppercase digits. -/
-theorem Spec.percent_encode_eq (bs : List UInt8) :
-    Percent.encode bs = Spec.pctEncode bs := sorry
+theorem Codec.Spec.percent_encode_eq (bs : List UInt8) :
+    Percent.encode bs = Codec.Spec.pctEncode bs := sorry
 
-/-- The decoder reads exactly the text that `Spec.PctReads` allows, and
-    reads it as `Spec.PctReads` says. So it refuses a `%` without two
+/-- The decoder reads exactly the text that `Codec.Spec.PctReads` allows, and
+    reads it as `Codec.Spec.PctReads` says. So it refuses a `%` without two
     hex digits after it, and any character outside US-ASCII. -/
-theorem Spec.percent_decode_iff (cs : List Char) (bs : List UInt8) :
-    Percent.decode cs = some bs ↔ Spec.PctReads cs bs := sorry
+theorem Codec.Spec.percent_decode_iff (cs : List Char) (bs : List UInt8) :
+    Percent.decode cs = some bs ↔ Codec.Spec.PctReads cs bs := sorry
 
 /-- Decoding what the encoder wrote gives the bytes back. -/
-theorem Spec.percent_decode_encode (bs : List UInt8) :
+theorem Codec.Spec.percent_decode_encode (bs : List UInt8) :
     Percent.decode (Percent.encode bs) = some bs := sorry
 
 /-- The examples of RFC 3986, sections 2.1, 2.3, 2.5 and 6.2.2 (with
@@ -155,23 +155,23 @@ theorem Spec.percent_decode_encode (bs : List UInt8) :
     2.2 and the unreserved punctuation of section 2.3; decoding once
     (`%252E` is the text `%2E`, not a dot); and text the decoder
     refuses. -/
-theorem Spec.percent_vectors :
+theorem Codec.Spec.percent_vectors :
     Percent.encode [0x20] = "%20".toList ∧
-    Percent.encode (Spec.ascii "A") = "A".toList ∧
+    Percent.encode (Codec.Spec.ascii "A") = "A".toList ∧
     Percent.encode [0xC3, 0x80] = "%C3%80".toList ∧
     Percent.encode [0xE3, 0x82, 0xA2] = "%E3%82%A2".toList ∧
-    Percent.encode (Spec.ascii "-._~") = "-._~".toList ∧
-    Percent.encode (Spec.ascii "Laguna Beach") = "Laguna%20Beach".toList ∧
-    Percent.encode (Spec.ascii "%:/?#[]@!$&'()*+,;=") =
+    Percent.encode (Codec.Spec.ascii "-._~") = "-._~".toList ∧
+    Percent.encode (Codec.Spec.ascii "Laguna Beach") = "Laguna%20Beach".toList ∧
+    Percent.encode (Codec.Spec.ascii "%:/?#[]@!$&'()*+,;=") =
       "%25%3A%2F%3F%23%5B%5D%40%21%24%26%27%28%29%2A%2B%2C%3B%3D".toList ∧
     Percent.decode "%C3%80".toList = some [0xC3, 0x80] ∧
     Percent.decode "%e3%82%a2".toList = some [0xE3, 0x82, 0xA2] ∧
-    Percent.decode "%7E".toList = some (Spec.ascii "~") ∧
-    Percent.decode "%63/%7bfoo%7d".toList = some (Spec.ascii "c/{foo}") ∧
-    Percent.decode "%3a".toList = some (Spec.ascii ":") ∧
-    Percent.decode "%3A".toList = some (Spec.ascii ":") ∧
-    Percent.decode "a+b c".toList = some (Spec.ascii "a+b c") ∧
-    Percent.decode "%252E".toList = some (Spec.ascii "%2E") ∧
+    Percent.decode "%7E".toList = some (Codec.Spec.ascii "~") ∧
+    Percent.decode "%63/%7bfoo%7d".toList = some (Codec.Spec.ascii "c/{foo}") ∧
+    Percent.decode "%3a".toList = some (Codec.Spec.ascii ":") ∧
+    Percent.decode "%3A".toList = some (Codec.Spec.ascii ":") ∧
+    Percent.decode "a+b c".toList = some (Codec.Spec.ascii "a+b c") ∧
+    Percent.decode "%252E".toList = some (Codec.Spec.ascii "%2E") ∧
     Percent.decode "%".toList = none ∧
     Percent.decode "%2".toList = none ∧
     Percent.decode "%zz".toList = none ∧
@@ -187,8 +187,8 @@ and an END line with the same label. -/
 /-- The encoder writes the strict form, each line ending in LF, and for
     empty data the BEGIN and END lines alone; it fails on a label the
     `label` rule does not allow. -/
-theorem Spec.pem_encode_iff (label : List Char) (data : List UInt8) (text : List Char) :
-    Pem.encode label data = some text ↔ Spec.Label label ∧ text = Spec.pemText label data :=
+theorem Codec.Spec.pem_encode_iff (label : List Char) (data : List UInt8) (text : List Char) :
+    Pem.encode label data = some text ↔ Codec.Spec.Label label ∧ text = Codec.Spec.pemText label data :=
   sorry
 
 /-- The decoder reads exactly the messages in the strict form, and for
@@ -197,23 +197,23 @@ theorem Spec.pem_encode_iff (label : List Char) (data : List UInt8) (text : List
     it refuses a different label on the END line, blanks, headers, text
     before or after the message, lines of another length, and base 64
     that is not exactly the encoding of the data. -/
-theorem Spec.pem_decode_iff (text label : List Char) (data : List UInt8) :
-    Pem.decode text = some (label, data) ↔ Spec.StrictPem text label data := sorry
+theorem Codec.Spec.pem_decode_iff (text label : List Char) (data : List UInt8) :
+    Pem.decode text = some (label, data) ↔ Codec.Spec.StrictPem text label data := sorry
 
 /-- Decoding what the encoder wrote gives the label and the data back. -/
-theorem Spec.pem_decode_encode (label : List Char) (data : List UInt8) (text : List Char) :
+theorem Codec.Spec.pem_decode_encode (label : List Char) (data : List UInt8) (text : List Char) :
     Pem.encode label data = some text → Pem.decode text = some (label, data) := sorry
 
 /-- RFC 7468, Figure 15, written exactly as the RFC prints it and read
     back with CR LF line ends; empty data and an empty label; labels the
     `label` rule refuses; and texts the decoder refuses. -/
-theorem Spec.pem_vectors :
-    Pem.encode "PUBLIC KEY".toList Spec.figure15 = some
+theorem Codec.Spec.pem_vectors :
+    Pem.encode "PUBLIC KEY".toList Codec.Spec.figure15 = some
       ("-----BEGIN PUBLIC KEY-----\nMHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEn1LlwLN/KBYQRVH6HfIMTzfEqJOVztLe\n".toList ++
        "kLchp2hi78cCaMY81FBlYs8J9l7krc+M4aBeCGYFjba+hiXttJWPL7ydlE+5UG4U\nNkn3Eos8EiZByi9DVsyfy9eejh+8AXgp\n-----END PUBLIC KEY-----\n".toList) ∧
     Pem.decode ("-----BEGIN PUBLIC KEY-----\r\nMHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEn1LlwLN/KBYQRVH6HfIMTzfEqJOVztLe\r\n".toList ++
        "kLchp2hi78cCaMY81FBlYs8J9l7krc+M4aBeCGYFjba+hiXttJWPL7ydlE+5UG4U\r\nNkn3Eos8EiZByi9DVsyfy9eejh+8AXgp\r\n-----END PUBLIC KEY-----\r\n".toList) =
-      some ("PUBLIC KEY".toList, Spec.figure15) ∧
+      some ("PUBLIC KEY".toList, Codec.Spec.figure15) ∧
     Pem.encode "X".toList [] = some "-----BEGIN X-----\n-----END X-----\n".toList ∧
     Pem.decode "-----BEGIN X-----\n-----END X-----\n".toList = some ("X".toList, []) ∧
     Pem.decode "-----BEGIN -----\rAA==\r-----END -----\r".toList = some ([], [0]) ∧
@@ -244,33 +244,33 @@ theorem Spec.pem_vectors :
 
 /-- `valid` decides the Luhn rule: every digit is 0 to 9, and the Luhn
     sum is a multiple of 10. -/
-theorem Spec.luhn_valid_iff (ds : List Nat) :
-    Luhn.valid ds = true ↔ (∀ d ∈ ds, d ≤ 9) ∧ Spec.luhnSum ds % 10 = 0 := sorry
+theorem Codec.Spec.luhn_valid_iff (ds : List Nat) :
+    Luhn.valid ds = true ↔ (∀ d ∈ ds, d ≤ 9) ∧ Codec.Spec.luhnSum ds % 10 = 0 := sorry
 
 /-- The check digit is a digit, and it is the one digit that makes the
     payload with it valid. -/
-theorem Spec.luhn_checkDigit (ds : List Nat) (h : ∀ d ∈ ds, d ≤ 9) :
+theorem Codec.Spec.luhn_checkDigit (ds : List Nat) (h : ∀ d ∈ ds, d ≤ 9) :
     Luhn.checkDigit ds ≤ 9 ∧
       ∀ c, c ≤ 9 → (Luhn.valid (ds ++ [c]) = true ↔ c = Luhn.checkDigit ds) := sorry
 
 /-- A single digit typed wrong is caught. -/
-theorem Spec.luhn_single_error (l r : List Nat) (a b : Nat)
+theorem Codec.Spec.luhn_single_error (l r : List Nat) (a b : Nat)
     (h : Luhn.valid (l ++ a :: r) = true) (hb : b ≤ 9) (hab : a ≠ b) :
     Luhn.valid (l ++ b :: r) = false := sorry
 
 /-- Two adjacent digits typed in the wrong order are caught, unless they
     are 0 and 9. -/
-theorem Spec.luhn_adjacent_swap (l r : List Nat) (a b : Nat)
+theorem Codec.Spec.luhn_adjacent_swap (l r : List Nat) (a b : Nat)
     (h : Luhn.valid (l ++ a :: b :: r) = true) (hab : a ≠ b)
     (h09 : ¬ (a = 0 ∧ b = 9)) (h90 : ¬ (a = 9 ∧ b = 0)) :
     Luhn.valid (l ++ b :: a :: r) = false := sorry
 
 /-- The blind spot: swapping an adjacent 0 and 9 is never caught. -/
-theorem Spec.luhn_swap_09 (l r : List Nat) :
+theorem Codec.Spec.luhn_swap_09 (l r : List Nat) :
     Luhn.valid (l ++ 0 :: 9 :: r) = Luhn.valid (l ++ 9 :: 0 :: r) := sorry
 
 /-- The common worked example, 79927398713, and a test card number. -/
-theorem Spec.luhn_vectors :
+theorem Codec.Spec.luhn_vectors :
     Luhn.valid [7, 9, 9, 2, 7, 3, 9, 8, 7, 1, 3] = true ∧
     Luhn.checkDigit [7, 9, 9, 2, 7, 3, 9, 8, 7, 1] = 3 ∧
     Luhn.valid [7, 9, 9, 2, 7, 3, 9, 8, 7, 1, 4] = false ∧
@@ -280,35 +280,35 @@ theorem Spec.luhn_vectors :
 /-! ## IBAN -/
 
 /-- `valid` decides the IBAN check: the shape, and the number mod 97. -/
-theorem Spec.iban_valid_iff (s : List Char) : Iban.valid s = true ↔ Spec.IbanValid s := sorry
+theorem Codec.Spec.iban_valid_iff (s : List Char) : Iban.valid s = true ↔ Codec.Spec.IbanValid s := sorry
 
 /-- `checkDigits` gives exactly the two digits from 02 to 98 that make
     the IBAN pass the check, for a country code of two characters; there
     is never more than one. -/
-theorem Spec.iban_checkDigits_iff (country bban ck : List Char) :
+theorem Codec.Spec.iban_checkDigits_iff (country bban ck : List Char) :
     Iban.checkDigits country bban = some ck ↔
-      country.length = 2 ∧ ck.length = 2 ∧ (∀ c ∈ ck, Spec.ibanDigit c) ∧
-        2 ≤ Spec.ibanNumber ck ∧ Spec.ibanNumber ck ≤ 98 ∧
-          Spec.IbanValid (country ++ ck ++ bban) := sorry
+      country.length = 2 ∧ ck.length = 2 ∧ (∀ c ∈ ck, Codec.Spec.ibanDigit c) ∧
+        2 ≤ Codec.Spec.ibanNumber ck ∧ Codec.Spec.ibanNumber ck ≤ 98 ∧
+          Codec.Spec.IbanValid (country ++ ck ++ bban) := sorry
 
 /-- One digit typed for another, or one letter for another, is caught. -/
-theorem Spec.iban_substitution (l r : List Char) (a b : Char)
+theorem Codec.Spec.iban_substitution (l r : List Char) (a b : Char)
     (h : Iban.valid (l ++ a :: r) = true) (hab : a ≠ b)
-    (hkind : (Spec.ibanDigit a ∧ Spec.ibanDigit b) ∨ (Spec.ibanLetter a ∧ Spec.ibanLetter b)) :
+    (hkind : (Codec.Spec.ibanDigit a ∧ Codec.Spec.ibanDigit b) ∨ (Codec.Spec.ibanLetter a ∧ Codec.Spec.ibanLetter b)) :
     Iban.valid (l ++ b :: r) = false := sorry
 
 /-- Two adjacent digits, or two adjacent letters, typed in the wrong
     order are caught. -/
-theorem Spec.iban_adjacent_swap (l r : List Char) (a b : Char)
+theorem Codec.Spec.iban_adjacent_swap (l r : List Char) (a b : Char)
     (h : Iban.valid (l ++ a :: b :: r) = true) (hab : a ≠ b)
-    (hkind : (Spec.ibanDigit a ∧ Spec.ibanDigit b) ∨ (Spec.ibanLetter a ∧ Spec.ibanLetter b)) :
+    (hkind : (Codec.Spec.ibanDigit a ∧ Codec.Spec.ibanDigit b) ∨ (Codec.Spec.ibanLetter a ∧ Codec.Spec.ibanLetter b)) :
     Iban.valid (l ++ b :: a :: r) = false := sorry
 
 /-- Example IBANs: the United Kingdom's from the SWIFT IBAN Registry,
     and Germany's, France's and Norway's; their check digits; one digit
     wrong. And the blind spot: a letter and a digit swapped, `4B1` for
     `41B`, gives another IBAN that passes, since B is 11. -/
-theorem Spec.iban_vectors :
+theorem Codec.Spec.iban_vectors :
     Iban.valid "GB29NWBK60161331926819".toList = true ∧
     Iban.valid "DE89370400440532013000".toList = true ∧
     Iban.valid "FR1420041010050500013M02606".toList = true ∧
diff --git a/Spec/Defs.lean b/Codec/Spec/Defs.lean
similarity index 64%
rename from Spec/Defs.lean
rename to Codec/Spec/Defs.lean
index 7b0d3f8..9552c49 100644
--- a/Spec/Defs.lean
+++ b/Codec/Spec/Defs.lean
@@ -2,15 +2,15 @@
   The definitions the specification uses, written from the standards,
   independently of the code in `Codec/`, with one exception: the PEM
   definitions take their base 64 from `Base64.encode`, which the base 64
-  statements in `Spec.lean` pin down exactly. Part of the approved
-  specification, with `Spec.lean`.
+  statements in `Codec/Spec.lean` pin down exactly. Part of the approved
+  specification, with `Codec/Spec.lean`.
 
   Both the challenge file and the proofs import this file, so each
   statement means the same thing on both sides. The `example`s pin each
   table character by character, by code point, and check the
   definitions against the examples of RFC 4648, section 9, and the
   CRC-32 check value. A mistake in either fails the build. The test
-  vectors of RFC 4648, section 10, are theorems in `Spec.lean`.
+  vectors of RFC 4648, section 10, are theorems in `Codec/Spec.lean`.
 -/
 
 import Codec
@@ -20,14 +20,14 @@ open Codec
 /-! ## Shared -/
 
 /-- The bytes of an ASCII string, for test vectors. -/
-def Spec.ascii (s : String) : List UInt8 :=
+def Codec.Spec.ascii (s : String) : List UInt8 :=
   s.toList.map fun c => c.toNat.toUInt8
 
 /-- ASCII lowercase: `A` to `Z` become `a` to `z`; nothing else changes. -/
-def Spec.asciiLower (c : Char) : Char :=
+def Codec.Spec.asciiLower (c : Char) : Char :=
   if 'A' ≤ c ∧ c ≤ 'Z' then Char.ofNat (c.toNat + 32) else c
 
-example : "AZaz09@[`{".toList.map Spec.asciiLower = "azaz09@[`{".toList := by decide
+example : "AZaz09@[`{".toList.map Codec.Spec.asciiLower = "azaz09@[`{".toList := by decide
 
 /-! ## Hex
 
@@ -35,12 +35,12 @@ Each byte becomes two digits from `0123456789abcdef`, the high half
 first. Decoding reads digits in either case and accepts nothing else. -/
 
 /-- The hex digits, lowercase, as Python's `bytes.hex()` writes them. -/
-def Spec.hexDigits : List Char := "0123456789abcdef".toList
+def Codec.Spec.hexDigits : List Char := "0123456789abcdef".toList
 
-def Spec.hexDigit (n : Nat) : Char := Spec.hexDigits.getD n '?'
+def Codec.Spec.hexDigit (n : Nat) : Char := Codec.Spec.hexDigits.getD n '?'
 
 -- Digits 0 to 9, then a to f, by code point.
-example : Spec.hexDigits.map Char.toNat =
+example : Codec.Spec.hexDigits.map Char.toNat =
     (List.range 10).map (· + 48) ++ (List.range 6).map (· + 97) := by decide
 
 /-! ## Base 64
@@ -48,29 +48,29 @@ example : Spec.hexDigits.map Char.toNat =
 RFC 4648, section 4. -/
 
 /-- RFC 4648, Table 1: the base 64 alphabet, values 0 to 63. -/
-def Spec.base64Table : List Char :=
+def Codec.Spec.base64Table : List Char :=
   "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/".toList
 
-def Spec.base64Char (n : Nat) : Char := Spec.base64Table.getD n '?'
+def Codec.Spec.base64Char (n : Nat) : Char := Codec.Spec.base64Table.getD n '?'
 
 /-- RFC 4648, section 4: a 24-bit group, high bit first, read as four
     6-bit values, each written as its character in Table 1. -/
-def Spec.base64Group (n : Nat) : List Char :=
-  [Spec.base64Char (n / 2 ^ 18 % 64), Spec.base64Char (n / 2 ^ 12 % 64),
-   Spec.base64Char (n / 2 ^ 6 % 64), Spec.base64Char (n % 64)]
+def Codec.Spec.base64Group (n : Nat) : List Char :=
+  [Codec.Spec.base64Char (n / 2 ^ 18 % 64), Codec.Spec.base64Char (n / 2 ^ 12 % 64),
+   Codec.Spec.base64Char (n / 2 ^ 6 % 64), Codec.Spec.base64Char (n % 64)]
 
 -- RFC 4648, Table 1, by code point: A to Z, a to z, 0 to 9, then + and /.
-example : Spec.base64Table.map Char.toNat =
+example : Codec.Spec.base64Table.map Char.toNat =
     (List.range 26).map (· + 65) ++ (List.range 26).map (· + 97) ++
       (List.range 10).map (· + 48) ++ [43, 47] := by decide
 
 -- RFC 4648, section 9: the bytes 14 fb 9c 03 d9 7e are "FPucA9l+",
 -- 14 fb 9c 03 d9 are "FPucA9k=", and 14 fb 9c 03 are "FPucAw==".
-example : Spec.base64Group 0x14fb9c ++ Spec.base64Group 0x03d97e = "FPucA9l+".toList := by
+example : Codec.Spec.base64Group 0x14fb9c ++ Codec.Spec.base64Group 0x03d97e = "FPucA9l+".toList := by
   decide
-example : Spec.base64Group 0x14fb9c ++ (Spec.base64Group 0x03d900).take 3 ++ ['='] =
+example : Codec.Spec.base64Group 0x14fb9c ++ (Codec.Spec.base64Group 0x03d900).take 3 ++ ['='] =
     "FPucA9k=".toList := by decide
-example : Spec.base64Group 0x14fb9c ++ (Spec.base64Group 0x030000).take 2 ++ ['=', '='] =
+example : Codec.Spec.base64Group 0x14fb9c ++ (Codec.Spec.base64Group 0x030000).take 2 ++ ['=', '='] =
     "FPucAw==".toList := by decide
 
 /-! ## CRC-32
@@ -80,27 +80,27 @@ at a time. -/
 
 /-- One bit: if the low bit is one, shift right and xor in the reflected
     polynomial 0xEDB88320; otherwise just shift right. -/
-def Spec.crcBit (c : UInt32) : UInt32 :=
+def Codec.Spec.crcBit (c : UInt32) : UInt32 :=
   if c % 2 = 1 then c / 2 ^^^ 0xEDB88320 else c / 2
 
 /-- One byte: xor it into the low end of the register, then eight bits. -/
-def Spec.crcByte (c : UInt32) (b : UInt8) : UInt32 :=
-  Nat.repeat Spec.crcBit 8 (c ^^^ b.toUInt32)
+def Codec.Spec.crcByte (c : UInt32) (b : UInt8) : UInt32 :=
+  Nat.repeat Codec.Spec.crcBit 8 (c ^^^ b.toUInt32)
 
 /-- The register starts as all ones, takes each byte in order, and is
     inverted at the end. -/
-def Spec.crc32 (bs : List UInt8) : UInt32 :=
-  bs.foldl Spec.crcByte 0xFFFFFFFF ^^^ 0xFFFFFFFF
+def Codec.Spec.crc32 (bs : List UInt8) : UInt32 :=
+  bs.foldl Codec.Spec.crcByte 0xFFFFFFFF ^^^ 0xFFFFFFFF
 
 -- The standard check value: the CRC-32 of "123456789" is 0xCBF43926.
-example : Spec.crc32 (Spec.ascii "123456789") = 0xCBF43926 := by decide +kernel
+example : Codec.Spec.crc32 (Codec.Spec.ascii "123456789") = 0xCBF43926 := by decide +kernel
 
 /-- Four bytes, low byte first, as gzip stores its CRC. -/
-def Spec.le32 (x : UInt32) : List UInt8 :=
+def Codec.Spec.le32 (x : UInt32) : List UInt8 :=
   [(x.toNat % 2 ^ 8).toUInt8, (x.toNat / 2 ^ 8 % 2 ^ 8).toUInt8,
    (x.toNat / 2 ^ 16 % 2 ^ 8).toUInt8, (x.toNat / 2 ^ 24).toUInt8]
 
-example : Spec.le32 0xCBF43926 = [0x26, 0x39, 0xF4, 0xCB] := by decide
+example : Codec.Spec.le32 0xCBF43926 = [0x26, 0x39, 0xF4, 0xCB] := by decide
 
 /-! ## Percent-encoding
 
@@ -129,57 +129,57 @@ Section 2.4: "Implementations must not percent-encode or decode the same
 string more than once". -/
 
 /-- The unreserved characters of section 2.3. -/
-def Spec.unreservedChars : List Char :=
+def Codec.Spec.unreservedChars : List Char :=
   "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-._~".toList
 
 -- `A` to `Z`, `a` to `z`, `0` to `9`, then `-`, `.`, `_` and `~`, by code point.
-example : Spec.unreservedChars.map Char.toNat =
+example : Codec.Spec.unreservedChars.map Char.toNat =
     (List.range 26).map (· + 65) ++ (List.range 26).map (· + 97) ++
       (List.range 10).map (· + 48) ++ [45, 46, 95, 126] := by decide
 
 /-- The hex digits, uppercase, as section 2.1 recommends producers write
     them. -/
-def Spec.upperHexDigits : List Char := "0123456789ABCDEF".toList
+def Codec.Spec.upperHexDigits : List Char := "0123456789ABCDEF".toList
 
 -- Digits 0 to 9, then A to F, by code point.
-example : Spec.upperHexDigits.map Char.toNat =
+example : Codec.Spec.upperHexDigits.map Char.toNat =
     (List.range 10).map (· + 48) ++ (List.range 6).map (· + 65) := by decide
 
 /-- How a producer writes one byte: an unreserved character as itself,
     and any other byte as `%` and two uppercase digits, the high half
     first. -/
-def Spec.pctByte (b : UInt8) : List Char :=
-  if Char.ofNat b.toNat ∈ Spec.unreservedChars then [Char.ofNat b.toNat]
-  else ['%', Spec.upperHexDigits.getD (b.toNat / 16) '?',
-    Spec.upperHexDigits.getD (b.toNat % 16) '?']
+def Codec.Spec.pctByte (b : UInt8) : List Char :=
+  if Char.ofNat b.toNat ∈ Codec.Spec.unreservedChars then [Char.ofNat b.toNat]
+  else ['%', Codec.Spec.upperHexDigits.getD (b.toNat / 16) '?',
+    Codec.Spec.upperHexDigits.getD (b.toNat % 16) '?']
 
 /-- The percent-encoding of a byte string, byte by byte. -/
-def Spec.pctEncode (bs : List UInt8) : List Char :=
-  (bs.map Spec.pctByte).flatten
+def Codec.Spec.pctEncode (bs : List UInt8) : List Char :=
+  (bs.map Codec.Spec.pctByte).flatten
 
 -- The examples of sections 2.1 and 2.5: the space, "A", LATIN CAPITAL
 -- LETTER A WITH GRAVE (C3 80 in UTF-8) and KATAKANA LETTER A (E3 82 A2).
-example : Spec.pctEncode [0x20] = "%20".toList := by decide
-example : Spec.pctEncode (Spec.ascii "A") = "A".toList := by decide
-example : Spec.pctEncode [0xC3, 0x80] = "%C3%80".toList := by decide
-example : Spec.pctEncode [0xE3, 0x82, 0xA2] = "%E3%82%A2".toList := by decide
+example : Codec.Spec.pctEncode [0x20] = "%20".toList := by decide
+example : Codec.Spec.pctEncode (Codec.Spec.ascii "A") = "A".toList := by decide
+example : Codec.Spec.pctEncode [0xC3, 0x80] = "%C3%80".toList := by decide
+example : Codec.Spec.pctEncode [0xE3, 0x82, 0xA2] = "%E3%82%A2".toList := by decide
 
-/-- How percent-encoded text reads: `Spec.PctReads cs bs` says the text
+/-- How percent-encoded text reads: `Codec.Spec.PctReads cs bs` says the text
     `cs` reads as the bytes `bs`. A `%` and two hex digits, in either
     case, read as the byte they spell, the high half first. Any other
     US-ASCII character but `%` reads as its own code. Nothing else
     reads: not a `%` without two hex digits after it, and not a
     character outside US-ASCII. What a `%` and its digits spell is never
     read again. -/
-inductive Spec.PctReads : List Char → List UInt8 → Prop where
-  | nil : Spec.PctReads [] []
+inductive Codec.Spec.PctReads : List Char → List UInt8 → Prop where
+  | nil : Codec.Spec.PctReads [] []
   | escape {hi lo : Char} {b : UInt8} {rest : List Char} {bs : List UInt8} :
-      Spec.asciiLower hi = Spec.hexDigit (b.toNat / 16) →
-      Spec.asciiLower lo = Spec.hexDigit (b.toNat % 16) →
-      Spec.PctReads rest bs → Spec.PctReads ('%' :: hi :: lo :: rest) (b :: bs)
+      Codec.Spec.asciiLower hi = Codec.Spec.hexDigit (b.toNat / 16) →
+      Codec.Spec.asciiLower lo = Codec.Spec.hexDigit (b.toNat % 16) →
+      Codec.Spec.PctReads rest bs → Codec.Spec.PctReads ('%' :: hi :: lo :: rest) (b :: bs)
   | char {c : Char} {rest : List Char} {bs : List UInt8} :
       c ≠ '%' → c.toNat < 0x80 →
-      Spec.PctReads rest bs → Spec.PctReads (c :: rest) (c.toNat.toUInt8 :: bs)
+      Codec.Spec.PctReads rest bs → Codec.Spec.PctReads (c :: rest) (c.toNat.toUInt8 :: bs)
 
 /-! ## PEM
 
@@ -220,65 +220,65 @@ unused bits are not zero, which strict base 64 refuses: here the base 64
 is exactly `Base64.encode` of the data. -/
 
 /-- `labelchar`: printable US-ASCII, `!` to `~`, except `-`. -/
-def Spec.labelChar (c : Char) : Prop :=
+def Codec.Spec.labelChar (c : Char) : Prop :=
   (0x21 ≤ c.toNat ∧ c.toNat ≤ 0x2C) ∨ (0x2E ≤ c.toNat ∧ c.toNat ≤ 0x7E)
 
 /-- `*( ["-" / SP] labelchar )`: label characters, each of which may
     follow one `-` or space. -/
-inductive Spec.LabelTail : List Char → Prop where
-  | nil : Spec.LabelTail []
+inductive Codec.Spec.LabelTail : List Char → Prop where
+  | nil : Codec.Spec.LabelTail []
   | char {c : Char} {rest : List Char} :
-      Spec.labelChar c → Spec.LabelTail rest → Spec.LabelTail (c :: rest)
+      Codec.Spec.labelChar c → Codec.Spec.LabelTail rest → Codec.Spec.LabelTail (c :: rest)
   | sep {s c : Char} {rest : List Char} :
-      (s = '-' ∨ s = ' ') → Spec.labelChar c → Spec.LabelTail rest →
-      Spec.LabelTail (s :: c :: rest)
+      (s = '-' ∨ s = ' ') → Codec.Spec.labelChar c → Codec.Spec.LabelTail rest →
+      Codec.Spec.LabelTail (s :: c :: rest)
 
 /-- `label = [ labelchar *( ["-" / SP] labelchar ) ]`. -/
-def Spec.Label (l : List Char) : Prop :=
-  l = [] ∨ ∃ c rest, l = c :: rest ∧ Spec.labelChar c ∧ Spec.LabelTail rest
+def Codec.Spec.Label (l : List Char) : Prop :=
+  l = [] ∨ ∃ c rest, l = c :: rest ∧ Codec.Spec.labelChar c ∧ Codec.Spec.LabelTail rest
 
 /-- `eol = CRLF / CR / LF`. -/
-def Spec.Eol (e : List Char) : Prop :=
+def Codec.Spec.Eol (e : List Char) : Prop :=
   e = ['\r', '\n'] ∨ e = ['\r'] ∨ e = ['\n']
 
 /-- The text `text` is the lines `ls`, each followed by an `eol`. No
     line holds a CR or an LF. -/
-inductive Spec.LinesEol : List Char → List (List Char) → Prop where
-  | nil : Spec.LinesEol [] []
+inductive Codec.Spec.LinesEol : List Char → List (List Char) → Prop where
+  | nil : Codec.Spec.LinesEol [] []
   | cons {l e rest : List Char} {ls : List (List Char)} :
-      '\r' ∉ l → '\n' ∉ l → Spec.Eol e → Spec.LinesEol rest ls →
-      Spec.LinesEol (l ++ e ++ rest) (l :: ls)
+      '\r' ∉ l → '\n' ∉ l → Codec.Spec.Eol e → Codec.Spec.LinesEol rest ls →
+      Codec.Spec.LinesEol (l ++ e ++ rest) (l :: ls)
 
 /-- `*base64fullline strictbase64finl`, without the line ends: the base
     64 text cut into lines of 64 characters, the last one at most 64. -/
-def Spec.lines64 (s : List Char) : List (List Char) :=
+def Codec.Spec.lines64 (s : List Char) : List (List Char) :=
   (List.range ((s.length + 63) / 64)).map fun i => (s.drop (64 * i)).take 64
 
 /-- The lines of the message for `label` and `data`, without their line
     ends: `preeb`, the base 64 of the data, `posteb`. The END line has
     the same label as the BEGIN line. -/
-def Spec.pemLines (label : List Char) (data : List UInt8) : List (List Char) :=
-  ["-----BEGIN ".toList ++ label ++ "-----".toList] ++ Spec.lines64 (Base64.encode data) ++
+def Codec.Spec.pemLines (label : List Char) (data : List UInt8) : List (List Char) :=
+  ["-----BEGIN ".toList ++ label ++ "-----".toList] ++ Codec.Spec.lines64 (Base64.encode data) ++
     ["-----END ".toList ++ label ++ "-----".toList]
 
 /-- What a generator writes: each line, then LF. -/
-def Spec.pemText (label : List Char) (data : List UInt8) : List Char :=
-  ((Spec.pemLines label data).map (· ++ ['\n'])).flatten
+def Codec.Spec.pemText (label : List Char) (data : List UInt8) : List Char :=
+  ((Codec.Spec.pemLines label data).map (· ++ ['\n'])).flatten
 
 /-- `text` is a message in the strict form, for this label and data:
     the label is a `label`, and the text is the message's lines, each
     followed by any `eol`. -/
-def Spec.StrictPem (text label : List Char) (data : List UInt8) : Prop :=
-  Spec.Label label ∧ Spec.LinesEol text (Spec.pemLines label data)
+def Codec.Spec.StrictPem (text label : List Char) (data : List UInt8) : Prop :=
+  Codec.Spec.Label label ∧ Codec.Spec.LinesEol text (Codec.Spec.pemLines label data)
 
 -- 48 bytes are one full line of 64 characters; 49 bytes need a second.
-example : (Spec.lines64 (List.replicate 64 'A')).map List.length = [64] := by decide
-example : (Spec.lines64 (List.replicate 68 'A')).map List.length = [64, 4] := by decide
-example : Spec.lines64 [] = [] := by decide
+example : (Codec.Spec.lines64 (List.replicate 64 'A')).map List.length = [64] := by decide
+example : (Codec.Spec.lines64 (List.replicate 68 'A')).map List.length = [64, 4] := by decide
+example : Codec.Spec.lines64 [] = [] := by decide
 
 /-- The data of RFC 7468, Figure 15 (a subject public key info), as the
     base 64 there spells it. -/
-def Spec.figure15 : List UInt8 := [
+def Codec.Spec.figure15 : List UInt8 := [
     0x30, 0x76, 0x30, 0x10, 0x06, 0x07, 0x2A, 0x86, 0x48, 0xCE, 0x3D, 0x02,
     0x01, 0x06, 0x05, 0x2B, 0x81, 0x04, 0x00, 0x22, 0x03, 0x62, 0x00, 0x04,
     0x9F, 0x52, 0xE5, 0xC0, 0xB3, 0x7F, 0x28, 0x16, 0x10, 0x45, 0x51, 0xFA,
@@ -301,16 +301,16 @@ sum of the results is a multiple of 10. -/
 /-- The share of digit `d` at place `i` from the right, the check digit
     being place 0: as it is at an even place; doubled at an odd place,
     less 9 when the double is above 9. -/
-def Spec.luhnShare (i d : Nat) : Nat :=
+def Codec.Spec.luhnShare (i d : Nat) : Nat :=
   if i % 2 = 1 then (if 2 * d > 9 then 2 * d - 9 else 2 * d) else d
 
 /-- The Luhn sum: the shares of all the digits. -/
-def Spec.luhnSum (ds : List Nat) : Nat :=
-  ((List.range ds.length).map fun i => Spec.luhnShare i (ds.reverse.getD i 0)).sum
+def Codec.Spec.luhnSum (ds : List Nat) : Nat :=
+  ((List.range ds.length).map fun i => Codec.Spec.luhnShare i (ds.reverse.getD i 0)).sum
 
 -- 79927398713: 3 + 2 + 7 + 7 + 7 + 6 + 2 + 9 + 9 + 9 + 7 (from the
 -- right; 1 8 3 2 9 doubled are 2 16 6 4 18, less 9 above 9: 2 7 6 4 9).
-example : Spec.luhnSum [7, 9, 9, 2, 7, 3, 9, 8, 7, 1, 3] = 70 := by decide
+example : Codec.Spec.luhnSum [7, 9, 9, 2, 7, 3, 9, 8, 7, 1, 3] = 70 := by decide
 
 /-! ## IBAN
 
@@ -324,39 +324,39 @@ are computed with 00 in their place, as 98 less that remainder, so they
 run from 02 to 98. The lengths and formats of each country's BBAN, in
 the SWIFT IBAN Registry, are not checked. -/
 
-def Spec.ibanDigit (c : Char) : Prop := '0' ≤ c ∧ c ≤ '9'
+def Codec.Spec.ibanDigit (c : Char) : Prop := '0' ≤ c ∧ c ≤ '9'
 
-def Spec.ibanLetter (c : Char) : Prop := 'A' ≤ c ∧ c ≤ 'Z'
+def Codec.Spec.ibanLetter (c : Char) : Prop := 'A' ≤ c ∧ c ≤ 'Z'
 
 /-- A digit's value, or a letter's: A = 10 to Z = 35. -/
-def Spec.ibanValue (c : Char) : Nat :=
+def Codec.Spec.ibanValue (c : Char) : Nat :=
   if '0' ≤ c ∧ c ≤ '9' then c.toNat - 48 else c.toNat - 55
 
 /-- The decimal digits a character becomes: one for a digit, two for a
     letter. -/
-def Spec.ibanDigits (c : Char) : List Nat :=
-  if Spec.ibanValue c < 10 then [Spec.ibanValue c] else [Spec.ibanValue c / 10, Spec.ibanValue c % 10]
+def Codec.Spec.ibanDigits (c : Char) : List Nat :=
+  if Codec.Spec.ibanValue c < 10 then [Codec.Spec.ibanValue c] else [Codec.Spec.ibanValue c / 10, Codec.Spec.ibanValue c % 10]
 
 /-- The number decimal digits write, most significant first. -/
-def Spec.decimal (ds : List Nat) : Nat :=
+def Codec.Spec.decimal (ds : List Nat) : Nat :=
   ds.foldl (fun n d => 10 * n + d) 0
 
 /-- The number a string of letters and digits becomes. -/
-def Spec.ibanNumber (cs : List Char) : Nat :=
-  Spec.decimal (cs.flatMap Spec.ibanDigits)
+def Codec.Spec.ibanNumber (cs : List Char) : Nat :=
+  Codec.Spec.decimal (cs.flatMap Codec.Spec.ibanDigits)
 
 /-- Two letters, two digits, then a BBAN of 1 to 30 letters and digits. -/
-def Spec.IbanShape (s : List Char) : Prop :=
+def Codec.Spec.IbanShape (s : List Char) : Prop :=
   ∃ c0 c1 k0 k1 bban, s = c0 :: c1 :: k0 :: k1 :: bban ∧
-    Spec.ibanLetter c0 ∧ Spec.ibanLetter c1 ∧ Spec.ibanDigit k0 ∧ Spec.ibanDigit k1 ∧
-    1 ≤ bban.length ∧ bban.length ≤ 30 ∧ ∀ c ∈ bban, Spec.ibanDigit c ∨ Spec.ibanLetter c
+    Codec.Spec.ibanLetter c0 ∧ Codec.Spec.ibanLetter c1 ∧ Codec.Spec.ibanDigit k0 ∧ Codec.Spec.ibanDigit k1 ∧
+    1 ≤ bban.length ∧ bban.length ≤ 30 ∧ ∀ c ∈ bban, Codec.Spec.ibanDigit c ∨ Codec.Spec.ibanLetter c
 
 /-- An IBAN that passes the check: the right shape, and the number of
     the string with its first four characters moved to the end leaves 1
     when divided by 97. -/
-def Spec.IbanValid (s : List Char) : Prop :=
-  Spec.IbanShape s ∧ Spec.ibanNumber (s.drop 4 ++ s.take 4) % 97 = 1
+def Codec.Spec.IbanValid (s : List Char) : Prop :=
+  Codec.Spec.IbanShape s ∧ Codec.Spec.ibanNumber (s.drop 4 ++ s.take 4) % 97 = 1
 
 -- The letters become 10 to 35, and "WEST" becomes 32 14 28 29.
-example : ("AZWEST".toList.flatMap Spec.ibanDigits) =
+example : ("AZWEST".toList.flatMap Codec.Spec.ibanDigits) =
     [1, 0, 3, 5, 3, 2, 1, 4, 2, 8, 2, 9] := by decide
diff --git a/Proofs.lean b/Proofs.lean
deleted file mode 100644
index 1a7183c..0000000
--- a/Proofs.lean
+++ /dev/null
@@ -1,12 +0,0 @@
-/-
-  The proofs, one file per codec.
--/
-
-import Proofs.Hex
-import Proofs.Base64
-import Proofs.Base32
-import Proofs.Crc32
-import Proofs.Percent
-import Proofs.Pem
-import Proofs.Luhn
-import Proofs.Iban
diff --git a/README.md b/README.md
index 848354e..f156567 100644
--- a/README.md
+++ b/README.md
@@ -6,40 +6,40 @@ Status: in progress. The specification has not yet been approved by a reviewer a
 
 ## What is proved
 
-The statements are in `Spec.lean`, the definitions they use in `Spec/Defs.lean`, and the proofs in `Proofs/`. Together they fix every output: the encoders and the checksum are given exactly. The hex and base 64 decoders and unframing accept exactly the outputs of their encoder or of framing (for hex, up to ASCII case) and return the matching input. The percent-decoder accepts more than the encoder writes, such as reserved characters as they are and escapes in lowercase, and `Spec.PctReads` gives exactly what it accepts and what each text reads as. The PEM decoder accepts what the PEM encoder writes, with any of the line ends LF, CR, and CR LF, and `Spec.StrictPem` gives exactly what it accepts. `Luhn.valid` and `Iban.valid` are decided exactly, and `Iban.checkDigits` is given exactly. `Luhn.checkDigit` is given exactly for a payload of digits 0 to 9; on a payload with a value above 9, no statement says what it gives.
+The statements are in `Codec/Spec.lean`, the definitions they use in `Codec/Spec/Defs.lean`, and the proofs in `Codec/Proofs/`. Together they fix every output: the encoders and the checksum are given exactly. The hex and base 64 decoders and unframing accept exactly the outputs of their encoder or of framing (for hex, up to ASCII case) and return the matching input. The percent-decoder accepts more than the encoder writes, such as reserved characters as they are and escapes in lowercase, and `Codec.Spec.PctReads` gives exactly what it accepts and what each text reads as. The PEM decoder accepts what the PEM encoder writes, with any of the line ends LF, CR, and CR LF, and `Codec.Spec.StrictPem` gives exactly what it accepts. `Luhn.valid` and `Iban.valid` are decided exactly, and `Iban.checkDigits` is given exactly. `Luhn.checkDigit` is given exactly for a payload of digits 0 to 9; on a payload with a value above 9, no statement says what it gives.
 
 | Claim | Theorem |
 |-------|---------|
-| Hex writes each byte as two digits, high half first, from `0123456789abcdef`. | `Spec.hex_encode_nil`, `Spec.hex_encode_cons` |
-| Hex decoding gives back what was encoded. | `Spec.hex_decode_encode` |
-| Hex decoding accepts any mix of upper and lower case. | `Spec.hex_decode_any_case` |
-| Hex decoding accepts nothing that is not an encoding, up to case. | `Spec.hex_encode_decode` |
-| Hex matches the test vectors of RFC 4648, section 10: encoding gives them in lowercase, and decoding reads them as the RFC writes them, in uppercase. | `Spec.hex_rfc4648_vectors` |
-| Base 64 writes three bytes as one group of four characters from RFC 4648, Table 1. | `Spec.base64_encode_nil`, `Spec.base64_encode_three` |
-| Base 64 writes a final one or two bytes with zero fill and `==` or `=` padding, as RFC 4648 section 4 says. | `Spec.base64_encode_one`, `Spec.base64_encode_two` |
-| Base 64 decoding gives back what was encoded. | `Spec.base64_decode_encode` |
-| Base 64 decoding accepts exactly the encodings and nothing else. | `Spec.base64_encode_decode` |
-| Base 64 matches the test vectors of RFC 4648, section 10. | `Spec.base64_rfc4648_vectors` |
-| The table-driven CRC-32 equals the CRC-32 defined one bit at a time. | `Spec.crc32_eq` |
-| The CRC-32 of `123456789` is the standard check value `0xCBF43926`. | `Spec.crc32_check` |
-| A frame is the message followed by its CRC-32, low byte first. | `Spec.frame_layout` |
-| Unframing a frame gives back the message. | `Spec.unframe_frame` |
-| Unframing accepts nothing that is not a frame. | `Spec.frame_unframe` |
-| Percent-encoding keeps the unreserved characters of RFC 3986, section 2.3, and writes every other byte as `%` and two uppercase digits, as section 2.1 recommends. | `Spec.percent_encode_eq` |
-| Percent-decoding reads `%` and two hex digits (the `pct-encoded` rule of section 2.1), in either case, as one byte, and any other US-ASCII character but `%` as itself. It does not check which characters a URI allows, so a space or a control character reads as itself. It refuses a `%` without two hex digits after it, and any character outside US-ASCII, rather than passing them through. | `Spec.percent_decode_iff` |
-| Percent-decoding gives back what was encoded. | `Spec.percent_decode_encode` |
-| Percent-encoding matches the examples of RFC 3986, sections 2.1, 2.3, 2.5 and 6.2.2, and decodes once: `%252E` decodes to the text `%2E`, not to a dot. | `Spec.percent_vectors` |
-| PEM encoding writes the strict form of RFC 7468 (Figure 3): `-----BEGIN label-----`, the base 64 of the data in lines of 64 characters with the last at most 64, and `-----END label-----`, each line ending in LF. For empty data, which that form cannot express, it writes the BEGIN and END lines alone (see What is not proved). It refuses a label that the `label` rule of section 3 does not allow. | `Spec.pem_encode_iff` |
-| PEM decoding reads exactly one message in the strict form, or for empty data the BEGIN and END lines alone, with each line ending in LF, CR, or CR LF, and gives its label and data. So it refuses a different label on the END line, blanks, headers, text before or after the message, lines of another length, and base 64 that is not exactly the encoding of the data. | `Spec.pem_decode_iff` |
-| PEM decoding gives back the label and data that were encoded. | `Spec.pem_decode_encode` |
-| Luhn: `valid` decides the rule (every second digit from the right doubled, less 9 above 9, the sum a multiple of 10), and, for a payload of digits, the check digit is the one digit that makes it valid. | `Spec.luhn_valid_iff`, `Spec.luhn_checkDigit` |
-| Luhn catches any one digit typed wrong, and any two adjacent different digits typed in the wrong order, except 0 and 9. | `Spec.luhn_single_error`, `Spec.luhn_adjacent_swap` |
-| Among adjacent swaps, Luhn misses only one: an adjacent 0 and 9 swapped is never caught. | `Spec.luhn_swap_09` |
-| Luhn gives the common worked example, 79927398713, and a test card number. | `Spec.luhn_vectors` |
-| IBAN: `valid` decides the check of ISO 13616 by ISO 7064 MOD 97-10 (the shape, and the rearranged number mod 97), and `checkDigits` gives exactly the two digits from 02 to 98 that make an IBAN pass. | `Spec.iban_valid_iff`, `Spec.iban_checkDigits_iff` |
-| IBAN catches one digit typed for another or one letter for another, and two adjacent digits or two adjacent letters typed in the wrong order. | `Spec.iban_substitution`, `Spec.iban_adjacent_swap` |
-| IBAN gives the SWIFT registry's UK example and Germany's, France's and Norway's, and their check digits; and its blind spot: a letter and a digit swapped, `4B1` for `41B`, gives another IBAN that passes. | `Spec.iban_vectors` |
-| PEM encoding writes RFC 7468's Figure 15 exactly as the RFC prints it, and decoding reads it back with CR LF line ends; empty data, an empty label, labels the rule refuses, and texts the decoder refuses. | `Spec.pem_vectors` |
+| Hex writes each byte as two digits, high half first, from `0123456789abcdef`. | `Codec.Spec.hex_encode_nil`, `Codec.Spec.hex_encode_cons` |
+| Hex decoding gives back what was encoded. | `Codec.Spec.hex_decode_encode` |
+| Hex decoding accepts any mix of upper and lower case. | `Codec.Spec.hex_decode_any_case` |
+| Hex decoding accepts nothing that is not an encoding, up to case. | `Codec.Spec.hex_encode_decode` |
+| Hex matches the test vectors of RFC 4648, section 10: encoding gives them in lowercase, and decoding reads them as the RFC writes them, in uppercase. | `Codec.Spec.hex_rfc4648_vectors` |
+| Base 64 writes three bytes as one group of four characters from RFC 4648, Table 1. | `Codec.Spec.base64_encode_nil`, `Codec.Spec.base64_encode_three` |
+| Base 64 writes a final one or two bytes with zero fill and `==` or `=` padding, as RFC 4648 section 4 says. | `Codec.Spec.base64_encode_one`, `Codec.Spec.base64_encode_two` |
+| Base 64 decoding gives back what was encoded. | `Codec.Spec.base64_decode_encode` |
+| Base 64 decoding accepts exactly the encodings and nothing else. | `Codec.Spec.base64_encode_decode` |
+| Base 64 matches the test vectors of RFC 4648, section 10. | `Codec.Spec.base64_rfc4648_vectors` |
+| The table-driven CRC-32 equals the CRC-32 defined one bit at a time. | `Codec.Spec.crc32_eq` |
+| The CRC-32 of `123456789` is the standard check value `0xCBF43926`. | `Codec.Spec.crc32_check` |
+| A frame is the message followed by its CRC-32, low byte first. | `Codec.Spec.frame_layout` |
+| Unframing a frame gives back the message. | `Codec.Spec.unframe_frame` |
+| Unframing accepts nothing that is not a frame. | `Codec.Spec.frame_unframe` |
+| Percent-encoding keeps the unreserved characters of RFC 3986, section 2.3, and writes every other byte as `%` and two uppercase digits, as section 2.1 recommends. | `Codec.Spec.percent_encode_eq` |
+| Percent-decoding reads `%` and two hex digits (the `pct-encoded` rule of section 2.1), in either case, as one byte, and any other US-ASCII character but `%` as itself. It does not check which characters a URI allows, so a space or a control character reads as itself. It refuses a `%` without two hex digits after it, and any character outside US-ASCII, rather than passing them through. | `Codec.Spec.percent_decode_iff` |
+| Percent-decoding gives back what was encoded. | `Codec.Spec.percent_decode_encode` |
+| Percent-encoding matches the examples of RFC 3986, sections 2.1, 2.3, 2.5 and 6.2.2, and decodes once: `%252E` decodes to the text `%2E`, not to a dot. | `Codec.Spec.percent_vectors` |
+| PEM encoding writes the strict form of RFC 7468 (Figure 3): `-----BEGIN label-----`, the base 64 of the data in lines of 64 characters with the last at most 64, and `-----END label-----`, each line ending in LF. For empty data, which that form cannot express, it writes the BEGIN and END lines alone (see What is not proved). It refuses a label that the `label` rule of section 3 does not allow. | `Codec.Spec.pem_encode_iff` |
+| PEM decoding reads exactly one message in the strict form, or for empty data the BEGIN and END lines alone, with each line ending in LF, CR, or CR LF, and gives its label and data. So it refuses a different label on the END line, blanks, headers, text before or after the message, lines of another length, and base 64 that is not exactly the encoding of the data. | `Codec.Spec.pem_decode_iff` |
+| PEM decoding gives back the label and data that were encoded. | `Codec.Spec.pem_decode_encode` |
+| Luhn: `valid` decides the rule (every second digit from the right doubled, less 9 above 9, the sum a multiple of 10), and, for a payload of digits, the check digit is the one digit that makes it valid. | `Codec.Spec.luhn_valid_iff`, `Codec.Spec.luhn_checkDigit` |
+| Luhn catches any one digit typed wrong, and any two adjacent different digits typed in the wrong order, except 0 and 9. | `Codec.Spec.luhn_single_error`, `Codec.Spec.luhn_adjacent_swap` |
+| Among adjacent swaps, Luhn misses only one: an adjacent 0 and 9 swapped is never caught. | `Codec.Spec.luhn_swap_09` |
+| Luhn gives the common worked example, 79927398713, and a test card number. | `Codec.Spec.luhn_vectors` |
+| IBAN: `valid` decides the check of ISO 13616 by ISO 7064 MOD 97-10 (the shape, and the rearranged number mod 97), and `checkDigits` gives exactly the two digits from 02 to 98 that make an IBAN pass. | `Codec.Spec.iban_valid_iff`, `Codec.Spec.iban_checkDigits_iff` |
+| IBAN catches one digit typed for another or one letter for another, and two adjacent digits or two adjacent letters typed in the wrong order. | `Codec.Spec.iban_substitution`, `Codec.Spec.iban_adjacent_swap` |
+| IBAN gives the SWIFT registry's UK example and Germany's, France's and Norway's, and their check digits; and its blind spot: a letter and a digit swapped, `4B1` for `41B`, gives another IBAN that passes. | `Codec.Spec.iban_vectors` |
+| PEM encoding writes RFC 7468's Figure 15 exactly as the RFC prints it, and decoding reads it back with CR LF line ends; empty data, an empty label, labels the rule refuses, and texts the decoder refuses. | `Codec.Spec.pem_vectors` |
 
 The command-line tool in `Main.lean` calls these functions directly.
 
@@ -88,14 +88,14 @@ lake comparator --paranoid
 python3 tests/run_tests.py
 ```
 
-`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. The test script compares the tool with Python's standard library, for PEM with an encoder and strict parser written in the script, and for Luhn and IBAN with the rules written in the script, on a million inputs in all, from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. Frames are compared with messages framed by `zlib.crc32`. Python 3.11.17, 3.12.3, and 3.13.17 give the same seed, count, and failures; they differ only in how many strict rejections each kind accounts for.
+`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Codec/Proofs/` proves exactly the statement in `Codec/Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. The test script compares the tool with Python's standard library, for PEM with an encoder and strict parser written in the script, and for Luhn and IBAN with the rules written in the script, on a million inputs in all, from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. Frames are compared with messages framed by `zlib.crc32`. Python 3.11.17, 3.12.3, and 3.13.17 give the same seed, count, and failures; they differ only in how many strict rejections each kind accounts for.
 
 ## Layout
 
 - `Codec/Hex.lean`, `Codec/Base64.lean`, `Codec/Crc32.lean`, `Codec/Percent.lean`, `Codec/Pem.lean`, `Codec/Luhn.lean`, `Codec/Iban.lean`: the code under proof.
-- `Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file.
-- `Spec/Defs.lean`: the definitions the statements use, written from the standards, with checks against their test values.
-- `Proofs.lean` and `Proofs/`: the proofs, under the same names.
+- `Codec/Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file.
+- `Codec/Spec/Defs.lean`: the definitions the statements use, written from the standards, with checks against their test values.
+- `Codec/Proofs.lean` and `Codec/Proofs/`: the proofs, under the same names.
 - `Main.lean`: the command-line tool the tests drive.
 - `lakefile.toml`: the build. It names the package and its version, its libraries and executable, and the default targets, and sets nothing else.
 - `comparator.json`: which theorems `lake comparator` checks, and which axioms it allows.
diff --git a/SPEC.md b/SPEC.md
index d148ac9..5fdac69 100644
--- a/SPEC.md
+++ b/SPEC.md
@@ -1,6 +1,6 @@
 # Specification: codec
 
-Five small codecs: hex, base 64, CRC-32 with a frame around a message, percent-encoding, and PEM; and two check digits, Luhn and IBAN. A reviewer who did not write this specification approves it, together with `Spec.lean`, `Spec/Defs.lean`, and the other files `bar.toml` lists.
+Five small codecs: hex, base 64, CRC-32 with a frame around a message, percent-encoding, and PEM; and two check digits, Luhn and IBAN. A reviewer who did not write this specification approves it, together with `Codec/Spec.lean`, `Codec/Spec/Defs.lean`, and the other files `bar.toml` lists.
 
 Bytes are `List UInt8` and text is `List Char`. The command-line tool converts at the edges.
 
@@ -73,47 +73,47 @@ The command-line tool in `Main.lean` reads one request per line and prints one a
 
 ## What must always hold
 
-Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use, written from the standards and checked against their test values, are in `Spec/Defs.lean`.
+Each property is a theorem in `Codec/Spec.lean`, under the name given. The definitions the statements use, written from the standards and checked against their test values, are in `Codec/Spec/Defs.lean`.
 
 | Property | Theorem |
 |----------|---------|
-| Hex encodes each byte as two digits, high half first, from `0123456789abcdef`. | `Spec.hex_encode_nil`, `Spec.hex_encode_cons` |
-| Hex decoding gives back what was encoded. | `Spec.hex_decode_encode` |
-| Hex decoding accepts any mix of upper and lower case. | `Spec.hex_decode_any_case` |
-| Hex decoding accepts nothing that is not an encoding, up to case. | `Spec.hex_encode_decode` |
-| Hex matches the test vectors of RFC 4648, section 10, in lowercase, and decodes them as the RFC writes them. | `Spec.hex_rfc4648_vectors` |
-| Base 64 encodes three bytes as one group of four characters from RFC 4648 Table 1. | `Spec.base64_encode_nil`, `Spec.base64_encode_three` |
-| Base 64 encodes a final one or two bytes with zero fill and `==` or `=` padding. | `Spec.base64_encode_one`, `Spec.base64_encode_two` |
-| Base 64 decoding gives back what was encoded. | `Spec.base64_decode_encode` |
-| Base 64 decoding accepts exactly the encodings and nothing else. | `Spec.base64_encode_decode` |
-| Base 64 encoding matches the test vectors of RFC 4648, section 10. | `Spec.base64_rfc4648_vectors` |
-| The table-driven CRC-32 equals the bit-at-a-time definition. | `Spec.crc32_eq` |
-| The CRC-32 of `123456789` is the standard check value `0xCBF43926`. | `Spec.crc32_check` |
-| A frame is the message followed by its CRC-32, low byte first. | `Spec.frame_layout` |
-| Unframing a frame gives back the message. | `Spec.unframe_frame` |
-| Unframing accepts nothing that is not a frame. | `Spec.frame_unframe` |
-| Percent-encoding writes each byte as `Spec.pctByte` says: an unreserved character as itself, any other byte as `%` and two uppercase digits. | `Spec.percent_encode_eq` |
-| Percent-decoding reads exactly what `Spec.PctReads` allows, as it says. | `Spec.percent_decode_iff` |
-| Percent-decoding gives back what was encoded. | `Spec.percent_decode_encode` |
-| The examples of RFC 3986, sections 2.1, 2.3, 2.5 and 6.2.2; the reserved and unreserved characters; decoding once; and text the decoder refuses. | `Spec.percent_vectors` |
-| PEM encoding gives `Spec.pemText` for a label the `label` rule allows, and fails on any other label. | `Spec.pem_encode_iff` |
-| PEM decoding gives a label and data exactly when `Spec.StrictPem` holds: the text is the message's lines, each followed by any `eol`. | `Spec.pem_decode_iff` |
-| PEM decoding gives back what was encoded. | `Spec.pem_decode_encode` |
-| `Luhn.valid` decides the Luhn sum's rule. | `Spec.luhn_valid_iff` |
-| The check digit is a digit, and the only one that makes the payload valid. | `Spec.luhn_checkDigit` |
-| One digit typed wrong is caught. | `Spec.luhn_single_error` |
-| Two adjacent different digits swapped are caught, unless they are 0 and 9. | `Spec.luhn_adjacent_swap` |
-| An adjacent 0 and 9 swapped is never caught. | `Spec.luhn_swap_09` |
-| 79927398713, its check digit, a wrong check digit, a test card number, and `10`. | `Spec.luhn_vectors` |
-| `Iban.valid` decides `Spec.IbanValid`: the shape, and the rearranged number mod 97 is 1. | `Spec.iban_valid_iff` |
-| `checkDigits` gives exactly the two digits from 02 to 98 that make the IBAN pass. | `Spec.iban_checkDigits_iff` |
-| One digit for another, or one letter for another, is caught. | `Spec.iban_substitution` |
-| Two adjacent digits, or two adjacent letters, swapped are caught. | `Spec.iban_adjacent_swap` |
-| Example IBANs and their check digits; a digit wrong; lower case refused; a letter and a digit swapped, both passing. | `Spec.iban_vectors` |
-| RFC 7468's Figure 15, written exactly as the RFC prints it and read back with CR LF; empty data and an empty label; labels the rule refuses; texts the decoder refuses. | `Spec.pem_vectors` |
-
-Together these fix every output but one, named at the end of this paragraph. The encoders, `crc32`, and `frame` are given exactly. Each of the hex and base 64 decoders and `unframe` accepts exactly the outputs of its encoder or `frame` (for hex, up to ASCII case), and returns the matching input. The percent-decoder accepts more than the encoder writes, since text may carry reserved characters as they are and escapes in lowercase: `Spec.PctReads` gives what it accepts and what each text reads as. The PEM decoder accepts what the PEM encoder writes, with any `eol` in place of each LF: `Spec.StrictPem` gives what it accepts. `Luhn.valid` and `Iban.valid` are decided exactly, `Iban.checkDigits` is given exactly, and `Luhn.checkDigit` is given exactly for a payload of digits; on a payload with a value above 9 it is the one output not fixed. A function that did nothing, or that accepted too much, would fail at least one of them.
+| Hex encodes each byte as two digits, high half first, from `0123456789abcdef`. | `Codec.Spec.hex_encode_nil`, `Codec.Spec.hex_encode_cons` |
+| Hex decoding gives back what was encoded. | `Codec.Spec.hex_decode_encode` |
+| Hex decoding accepts any mix of upper and lower case. | `Codec.Spec.hex_decode_any_case` |
+| Hex decoding accepts nothing that is not an encoding, up to case. | `Codec.Spec.hex_encode_decode` |
+| Hex matches the test vectors of RFC 4648, section 10, in lowercase, and decodes them as the RFC writes them. | `Codec.Spec.hex_rfc4648_vectors` |
+| Base 64 encodes three bytes as one group of four characters from RFC 4648 Table 1. | `Codec.Spec.base64_encode_nil`, `Codec.Spec.base64_encode_three` |
+| Base 64 encodes a final one or two bytes with zero fill and `==` or `=` padding. | `Codec.Spec.base64_encode_one`, `Codec.Spec.base64_encode_two` |
+| Base 64 decoding gives back what was encoded. | `Codec.Spec.base64_decode_encode` |
+| Base 64 decoding accepts exactly the encodings and nothing else. | `Codec.Spec.base64_encode_decode` |
+| Base 64 encoding matches the test vectors of RFC 4648, section 10. | `Codec.Spec.base64_rfc4648_vectors` |
+| The table-driven CRC-32 equals the bit-at-a-time definition. | `Codec.Spec.crc32_eq` |
+| The CRC-32 of `123456789` is the standard check value `0xCBF43926`. | `Codec.Spec.crc32_check` |
+| A frame is the message followed by its CRC-32, low byte first. | `Codec.Spec.frame_layout` |
+| Unframing a frame gives back the message. | `Codec.Spec.unframe_frame` |
+| Unframing accepts nothing that is not a frame. | `Codec.Spec.frame_unframe` |
+| Percent-encoding writes each byte as `Codec.Spec.pctByte` says: an unreserved character as itself, any other byte as `%` and two uppercase digits. | `Codec.Spec.percent_encode_eq` |
+| Percent-decoding reads exactly what `Codec.Spec.PctReads` allows, as it says. | `Codec.Spec.percent_decode_iff` |
+| Percent-decoding gives back what was encoded. | `Codec.Spec.percent_decode_encode` |
+| The examples of RFC 3986, sections 2.1, 2.3, 2.5 and 6.2.2; the reserved and unreserved characters; decoding once; and text the decoder refuses. | `Codec.Spec.percent_vectors` |
+| PEM encoding gives `Codec.Spec.pemText` for a label the `label` rule allows, and fails on any other label. | `Codec.Spec.pem_encode_iff` |
+| PEM decoding gives a label and data exactly when `Codec.Spec.StrictPem` holds: the text is the message's lines, each followed by any `eol`. | `Codec.Spec.pem_decode_iff` |
+| PEM decoding gives back what was encoded. | `Codec.Spec.pem_decode_encode` |
+| `Luhn.valid` decides the Luhn sum's rule. | `Codec.Spec.luhn_valid_iff` |
+| The check digit is a digit, and the only one that makes the payload valid. | `Codec.Spec.luhn_checkDigit` |
+| One digit typed wrong is caught. | `Codec.Spec.luhn_single_error` |
+| Two adjacent different digits swapped are caught, unless they are 0 and 9. | `Codec.Spec.luhn_adjacent_swap` |
+| An adjacent 0 and 9 swapped is never caught. | `Codec.Spec.luhn_swap_09` |
+| 79927398713, its check digit, a wrong check digit, a test card number, and `10`. | `Codec.Spec.luhn_vectors` |
+| `Iban.valid` decides `Codec.Spec.IbanValid`: the shape, and the rearranged number mod 97 is 1. | `Codec.Spec.iban_valid_iff` |
+| `checkDigits` gives exactly the two digits from 02 to 98 that make the IBAN pass. | `Codec.Spec.iban_checkDigits_iff` |
+| One digit for another, or one letter for another, is caught. | `Codec.Spec.iban_substitution` |
+| Two adjacent digits, or two adjacent letters, swapped are caught. | `Codec.Spec.iban_adjacent_swap` |
+| Example IBANs and their check digits; a digit wrong; lower case refused; a letter and a digit swapped, both passing. | `Codec.Spec.iban_vectors` |
+| RFC 7468's Figure 15, written exactly as the RFC prints it and read back with CR LF; empty data and an empty label; labels the rule refuses; texts the decoder refuses. | `Codec.Spec.pem_vectors` |
+
+Together these fix every output but one, named at the end of this paragraph. The encoders, `crc32`, and `frame` are given exactly. Each of the hex and base 64 decoders and `unframe` accepts exactly the outputs of its encoder or `frame` (for hex, up to ASCII case), and returns the matching input. The percent-decoder accepts more than the encoder writes, since text may carry reserved characters as they are and escapes in lowercase: `Codec.Spec.PctReads` gives what it accepts and what each text reads as. The PEM decoder accepts what the PEM encoder writes, with any `eol` in place of each LF: `Codec.Spec.StrictPem` gives what it accepts. `Luhn.valid` and `Iban.valid` are decided exactly, `Iban.checkDigits` is given exactly, and `Luhn.checkDigit` is given exactly for a payload of digits; on a payload with a value above 9 it is the one output not fixed. A function that did nothing, or that accepted too much, would fail at least one of them.
 
 ## Oracle
 
-Python's `binascii.hexlify` and `binascii.unhexlify`, `base64.b64encode` and `binascii.a2b_base64(strict_mode=True)`, `zlib.crc32`, and `urllib.parse.quote(safe="")` and `urllib.parse.unquote_to_bytes`. `unquote_to_bytes` passes a bad escape through, so the tests give it only text that `Spec.PctReads` accepts, checked with a regular expression; the decoder must refuse the rest. For PEM, a strict parser written in the tests from the ABNF of RFC 7468 decides every decoding, with the base 64 checked by strict `binascii.a2b_base64` and by encoding it again; where it accepts a text with the `CERTIFICATE` label, Python's `ssl.PEM_cert_to_DER_cert` must read the same data. Encoding is checked against `ssl.DER_cert_to_PEM_cert` for the `CERTIFICATE` label and against an encoder written in the tests for the others. For Luhn and IBAN, the oracle is the rules written in the tests: the Luhn sum, the IBAN shape as a regular expression, and the IBAN number mod 97 computed with Python's integers. A one-off cross-check with python-stdnum, in `tests/CROSS-CHECK.md`, compares them with an independent implementation.
+Python's `binascii.hexlify` and `binascii.unhexlify`, `base64.b64encode` and `binascii.a2b_base64(strict_mode=True)`, `zlib.crc32`, and `urllib.parse.quote(safe="")` and `urllib.parse.unquote_to_bytes`. `unquote_to_bytes` passes a bad escape through, so the tests give it only text that `Codec.Spec.PctReads` accepts, checked with a regular expression; the decoder must refuse the rest. For PEM, a strict parser written in the tests from the ABNF of RFC 7468 decides every decoding, with the base 64 checked by strict `binascii.a2b_base64` and by encoding it again; where it accepts a text with the `CERTIFICATE` label, Python's `ssl.PEM_cert_to_DER_cert` must read the same data. Encoding is checked against `ssl.DER_cert_to_PEM_cert` for the `CERTIFICATE` label and against an encoder written in the tests for the others. For Luhn and IBAN, the oracle is the rules written in the tests: the Luhn sum, the IBAN shape as a regular expression, and the IBAN number mod 97 computed with Python's integers. A one-off cross-check with python-stdnum, in `tests/CROSS-CHECK.md`, compares them with an independent implementation.
diff --git a/bar.toml b/bar.toml
index 5f3405f..4466900 100644
--- a/bar.toml
+++ b/bar.toml
@@ -13,7 +13,7 @@ spec_authors = ["claude"]
 entry_points = ["Main.lean"]
 
 [spec]
-files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean"]
+files = ["SPEC.md", "Codec/Spec.lean", "Codec/Spec/Defs.lean"]
 # The code under proof: the functions the statements are about.
 code = [
   "Codec.Hex.encode", "Codec.Hex.decode",
diff --git a/comparator.json b/comparator.json
index bd48adc..ff71b1a 100644
--- a/comparator.json
+++ b/comparator.json
@@ -1,44 +1,44 @@
 {
-  "challenge_module": "Spec",
-  "solution_module": "Proofs",
+  "challenge_module": "Codec.Spec",
+  "solution_module": "Codec.Proofs",
   "theorem_names": [
-    "Spec.hex_encode_nil",
-    "Spec.hex_encode_cons",
-    "Spec.hex_decode_encode",
-    "Spec.hex_decode_any_case",
-    "Spec.hex_encode_decode",
-    "Spec.hex_rfc4648_vectors",
-    "Spec.base64_encode_nil",
-    "Spec.base64_encode_three",
-    "Spec.base64_encode_two",
-    "Spec.base64_encode_one",
-    "Spec.base64_decode_encode",
-    "Spec.base64_encode_decode",
-    "Spec.base64_rfc4648_vectors",
-    "Spec.crc32_eq",
-    "Spec.crc32_check",
-    "Spec.frame_layout",
-    "Spec.unframe_frame",
-    "Spec.frame_unframe",
-    "Spec.percent_encode_eq",
-    "Spec.percent_decode_iff",
-    "Spec.percent_decode_encode",
-    "Spec.percent_vectors",
-    "Spec.pem_encode_iff",
-    "Spec.pem_decode_iff",
-    "Spec.pem_decode_encode",
-    "Spec.pem_vectors",
-    "Spec.luhn_valid_iff",
-    "Spec.luhn_checkDigit",
-    "Spec.luhn_single_error",
-    "Spec.luhn_adjacent_swap",
-    "Spec.luhn_swap_09",
-    "Spec.luhn_vectors",
-    "Spec.iban_valid_iff",
-    "Spec.iban_checkDigits_iff",
-    "Spec.iban_substitution",
-    "Spec.iban_adjacent_swap",
-    "Spec.iban_vectors"
+    "Codec.Spec.hex_encode_nil",
+    "Codec.Spec.hex_encode_cons",
+    "Codec.Spec.hex_decode_encode",
+    "Codec.Spec.hex_decode_any_case",
+    "Codec.Spec.hex_encode_decode",
+    "Codec.Spec.hex_rfc4648_vectors",
+    "Codec.Spec.base64_encode_nil",
+    "Codec.Spec.base64_encode_three",
+    "Codec.Spec.base64_encode_two",
+    "Codec.Spec.base64_encode_one",
+    "Codec.Spec.base64_decode_encode",
+    "Codec.Spec.base64_encode_decode",
+    "Codec.Spec.base64_rfc4648_vectors",
+    "Codec.Spec.crc32_eq",
+    "Codec.Spec.crc32_check",
+    "Codec.Spec.frame_layout",
+    "Codec.Spec.unframe_frame",
+    "Codec.Spec.frame_unframe",
+    "Codec.Spec.percent_encode_eq",
+    "Codec.Spec.percent_decode_iff",
+    "Codec.Spec.percent_decode_encode",
+    "Codec.Spec.percent_vectors",
+    "Codec.Spec.pem_encode_iff",
+    "Codec.Spec.pem_decode_iff",
+    "Codec.Spec.pem_decode_encode",
+    "Codec.Spec.pem_vectors",
+    "Codec.Spec.luhn_valid_iff",
+    "Codec.Spec.luhn_checkDigit",
+    "Codec.Spec.luhn_single_error",
+    "Codec.Spec.luhn_adjacent_swap",
+    "Codec.Spec.luhn_swap_09",
+    "Codec.Spec.luhn_vectors",
+    "Codec.Spec.iban_valid_iff",
+    "Codec.Spec.iban_checkDigits_iff",
+    "Codec.Spec.iban_substitution",
+    "Codec.Spec.iban_adjacent_swap",
+    "Codec.Spec.iban_vectors"
   ],
   "permitted_axioms": [
     "propext",
diff --git a/lakefile.toml b/lakefile.toml
index f9e0588..8aabce3 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,16 +1,18 @@
 name = "codec"
 version = "0.1.0"
 license = "Apache-2.0"
-defaultTargets = ["Codec", "Spec", "Proofs", "codec"]
+defaultTargets = ["Codec", "CodecSpec", "CodecProofs", "codec"]
 
 [[lean_lib]]
 name = "Codec"
 
 [[lean_lib]]
-name = "Spec"
+name = "CodecSpec"
+roots = ["Codec.Spec"]
 
 [[lean_lib]]
-name = "Proofs"
+name = "CodecProofs"
+roots = ["Codec.Proofs"]
 
 [[lean_exe]]
 name = "codec"
diff --git a/tests/run_tests.py b/tests/run_tests.py
index 311dcef..7246adc 100644
--- a/tests/run_tests.py
+++ b/tests/run_tests.py
@@ -11,7 +11,7 @@
 parser written here from the ABNF of RFC 7468, section 3, with the base
 64 checked by strict `binascii.a2b_base64`. `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
+against what `Codec.Spec.PctReads` accepts, as a regular expression, and only
 text that matches is given to it; the rest must be refused. Inputs come from
 a recorded seed:
 
@@ -224,7 +224,7 @@ def oracle_b64decode(text):
         return None
 
 
-# What `Spec.PctReads` accepts, as a regular expression: each piece is `%`
+# What `Codec.Spec.PctReads` accepts, as a regular expression: each piece is `%`
 # and two hex digits (the `pct-encoded` rule of RFC 3986, section 2.1),
 # or a US-ASCII character other than `%`.
 PCT_TEXT = re.compile(r"(?:%[0-9A-Fa-f]{2}|[\x00-\x24\x26-\x7f])*")