From e55d41217009465c444dbf4e7214150fc66b6f32 Mon Sep 17 00:00:00 2001
From: ahrazzle <38987266+ahrazzle@users.noreply.github.com>
Date: Tue, 27 Oct 2026 22:51:02 -0500
Subject: [PATCH 1/2] Move proof modules and spec names under Protobuf

---
 Proofs.lean                              |  7 --
 Protobuf/Proofs.lean                     |  7 ++
 {Proofs => Protobuf/Proofs}/Fixed.lean   | 34 +++++-----
 {Proofs => Protobuf/Proofs}/Main.lean    | 40 +++++------
 {Proofs => Protobuf/Proofs}/Message.lean | 78 ++++++++++-----------
 {Proofs => Protobuf/Proofs}/Varint.lean  | 80 +++++++++++-----------
 Spec.lean => Protobuf/Spec.lean          | 36 +++++-----
 {Spec => Protobuf/Spec}/Defs.lean        | 86 ++++++++++++------------
 Protobuf/Types.lean                      |  4 +-
 README.md                                | 30 ++++-----
 SPEC.md                                  | 30 ++++-----
 bar.toml                                 |  2 +-
 comparator.json                          | 24 +++++--
 lakefile.toml                            |  8 ++-
 tests/PLANTED-BUGS.md                    |  2 +-
 tests/planted_bugs.py                    |  2 +-
 16 files changed, 242 insertions(+), 228 deletions(-)
 delete mode 100644 Proofs.lean
 create mode 100644 Protobuf/Proofs.lean
 rename {Proofs => Protobuf/Proofs}/Fixed.lean (64%)
 rename {Proofs => Protobuf/Proofs}/Main.lean (68%)
 rename {Proofs => Protobuf/Proofs}/Message.lean (78%)
 rename {Proofs => Protobuf/Proofs}/Varint.lean (74%)
 rename Spec.lean => Protobuf/Spec.lean (79%)
 rename {Spec => Protobuf/Spec}/Defs.lean (60%)

diff --git a/Proofs.lean b/Proofs.lean
deleted file mode 100644
index a0c5328..0000000
--- a/Proofs.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-/-
-  The proofs, under the names the challenge file gives them. The
-  theorems themselves are in `Proofs/Main.lean`, from the lemmas in the
-  other files.
--/
-
-import Proofs.Main
diff --git a/Protobuf/Proofs.lean b/Protobuf/Proofs.lean
new file mode 100644
index 0000000..82715f3
--- /dev/null
+++ b/Protobuf/Proofs.lean
@@ -0,0 +1,7 @@
+/-
+  The proofs, under the names the challenge file gives them. The
+  theorems themselves are in `Protobuf/Proofs/Main.lean`, from the lemmas in the
+  other files.
+-/
+
+import Protobuf.Proofs.Main
diff --git a/Proofs/Fixed.lean b/Protobuf/Proofs/Fixed.lean
similarity index 64%
rename from Proofs/Fixed.lean
rename to Protobuf/Proofs/Fixed.lean
index 6a186d8..c0cb3c8 100644
--- a/Proofs/Fixed.lean
+++ b/Protobuf/Proofs/Fixed.lean
@@ -1,13 +1,13 @@
 /-
   Fixed-width values: `leValue` and `leBytes` in `Protobuf/Wire.lean`
-  are `Spec.leValue` and `Spec.leBytes`, `Spec.leBytes k n` has `k`
+  are `Protobuf.Spec.leValue` and `Protobuf.Spec.leBytes`, `Protobuf.Spec.leBytes k n` has `k`
   bytes, and the two are inverse: reading back `k` bytes of a number
   below 256^k gives the number, and writing the value of a list of bytes
   in as many bytes gives the list.
 -/
 
 import Protobuf
-import Spec.Defs
+import Protobuf.Spec.Defs
 
 namespace Protobuf.Proofs.Fixed
 
@@ -21,11 +21,11 @@ theorem sum_map_mul_left (l : List Nat) (g : Nat → Nat) (c : Nat) :
   | nil => simp
   | cons x xs ih => simp [List.sum_cons, ih, Nat.mul_add]
 
-theorem spec_leValue_nil : Spec.leValue [] = 0 := rfl
+theorem spec_leValue_nil : Protobuf.Spec.leValue [] = 0 := rfl
 
 theorem spec_leValue_cons (b : UInt8) (bs : List UInt8) :
-    Spec.leValue (b :: bs) = b.toNat + 256 * Spec.leValue bs := by
-  unfold Spec.leValue
+    Protobuf.Spec.leValue (b :: bs) = b.toNat + 256 * Protobuf.Spec.leValue bs := by
+  unfold Protobuf.Spec.leValue
   rw [List.length_cons, List.range_succ_eq_map, List.map_cons, List.sum_cons, List.map_map]
   have : ((fun i => ((b :: bs).getD i 0).toNat * 256 ^ i) ∘ Nat.succ) =
       fun i => 256 * ((bs.getD i 0).toNat * 256 ^ i) := by
@@ -34,11 +34,11 @@ theorem spec_leValue_cons (b : UInt8) (bs : List UInt8) :
   rw [this, sum_map_mul_left]
   simp
 
-theorem spec_leBytes_zero (n : Nat) : Spec.leBytes 0 n = [] := rfl
+theorem spec_leBytes_zero (n : Nat) : Protobuf.Spec.leBytes 0 n = [] := rfl
 
 theorem spec_leBytes_succ (k n : Nat) :
-    Spec.leBytes (k + 1) n = (n % 256).toUInt8 :: Spec.leBytes k (n / 256) := by
-  unfold Spec.leBytes
+    Protobuf.Spec.leBytes (k + 1) n = (n % 256).toUInt8 :: Protobuf.Spec.leBytes k (n / 256) := by
+  unfold Protobuf.Spec.leBytes
   rw [List.range_succ_eq_map, List.map_cons, List.map_map]
   congr 1
   · simp
@@ -51,24 +51,24 @@ theorem spec_leBytes_succ (k n : Nat) :
 theorem leValue_cons (b : UInt8) (bs : List UInt8) :
     leValue (b :: bs) = b.toNat + 256 * leValue bs := rfl
 
-theorem leValue_eq (bs : List UInt8) : leValue bs = Spec.leValue bs := by
+theorem leValue_eq (bs : List UInt8) : leValue bs = Protobuf.Spec.leValue bs := by
   induction bs with
   | nil => rfl
   | cons b bs ih => rw [leValue_cons, spec_leValue_cons, ih]
 
-theorem leBytes_eq (k n : Nat) : leBytes k n = Spec.leBytes k n := by
+theorem leBytes_eq (k n : Nat) : leBytes k n = Protobuf.Spec.leBytes k n := by
   induction k generalizing n with
   | zero => rfl
   | succ k ih => rw [spec_leBytes_succ, ← ih]; rfl
 
 /-! ## Length, bounds and inverses -/
 
-theorem leBytes_length (k n : Nat) : (Spec.leBytes k n).length = k := by
-  simp [Spec.leBytes]
+theorem leBytes_length (k n : Nat) : (Protobuf.Spec.leBytes k n).length = k := by
+  simp [Protobuf.Spec.leBytes]
 
 theorem toNat_lt (b : UInt8) : b.toNat < 256 := UInt8.toNat_lt b
 
-theorem leValue_leBytes (k n : Nat) (h : n < 256 ^ k) : Spec.leValue (Spec.leBytes k n) = n := by
+theorem leValue_leBytes (k n : Nat) (h : n < 256 ^ k) : Protobuf.Spec.leValue (Protobuf.Spec.leBytes k n) = n := by
   induction k generalizing n with
   | zero =>
     simp at h
@@ -83,7 +83,7 @@ theorem leValue_leBytes (k n : Nat) (h : n < 256 ^ k) : Spec.leValue (Spec.leByt
     rw [this]
     exact Nat.mod_add_div n 256
 
-theorem leValue_lt (bs : List UInt8) : Spec.leValue bs < 256 ^ bs.length := by
+theorem leValue_lt (bs : List UInt8) : Protobuf.Spec.leValue bs < 256 ^ bs.length := by
   induction bs with
   | nil => simp [spec_leValue_nil]
   | cons b bs ih =>
@@ -91,14 +91,14 @@ theorem leValue_lt (bs : List UInt8) : Spec.leValue bs < 256 ^ bs.length := by
     have := toNat_lt b
     omega
 
-theorem leBytes_leValue (bs : List UInt8) : Spec.leBytes bs.length (Spec.leValue bs) = bs := by
+theorem leBytes_leValue (bs : List UInt8) : Protobuf.Spec.leBytes bs.length (Protobuf.Spec.leValue bs) = bs := by
   induction bs with
   | nil => rfl
   | cons b bs ih =>
     have hb := toNat_lt b
     rw [List.length_cons, spec_leBytes_succ, spec_leValue_cons]
-    have hm : (b.toNat + 256 * Spec.leValue bs) % 256 = b.toNat := by omega
-    have hd : (b.toNat + 256 * Spec.leValue bs) / 256 = Spec.leValue bs := by omega
+    have hm : (b.toNat + 256 * Protobuf.Spec.leValue bs) % 256 = b.toNat := by omega
+    have hd : (b.toNat + 256 * Protobuf.Spec.leValue bs) / 256 = Protobuf.Spec.leValue bs := by omega
     rw [hm, hd, ih]
     simp
 
diff --git a/Proofs/Main.lean b/Protobuf/Proofs/Main.lean
similarity index 68%
rename from Proofs/Main.lean
rename to Protobuf/Proofs/Main.lean
index e68bf18..4cd96c6 100644
--- a/Proofs/Main.lean
+++ b/Protobuf/Proofs/Main.lean
@@ -1,48 +1,48 @@
 /-
-  The statements of `Spec.lean`, under the same names, from the lemmas
-  in the other files of `Proofs/`. The test vectors are checked by
+  The statements of `Protobuf/Spec.lean`, under the same names, from the lemmas
+  in the other files of `Protobuf/Proofs/`. The test vectors are checked by
   evaluation.
 -/
 
 import Protobuf
-import Spec.Defs
-import Proofs.Varint
-import Proofs.Message
+import Protobuf.Spec.Defs
+import Protobuf.Proofs.Varint
+import Protobuf.Proofs.Message
 
 open Protobuf
 open Protobuf.Proofs
 
-theorem Spec.varint_encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Spec.varint n :=
+theorem Protobuf.Spec.varint_encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Protobuf.Spec.varint n :=
   Protobuf.Proofs.Varint.encode_eq n h
 
-theorem Spec.varint_decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) :
-    Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Spec.IsVarint pre v :=
+theorem Protobuf.Spec.varint_decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) :
+    Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Protobuf.Spec.IsVarint pre v :=
   Protobuf.Proofs.Varint.decode_iff bs v rest
 
-theorem Spec.varint_decode_encode (n : Nat) (rest : List UInt8) (h : n < 2 ^ 64) :
+theorem Protobuf.Spec.varint_decode_encode (n : Nat) (rest : List UInt8) (h : n < 2 ^ 64) :
     Varint.decode (Varint.encode n ++ rest) = some (n, rest) :=
   Protobuf.Proofs.Varint.decode_encode n rest h
 
-theorem Spec.isValid_iff (f : Field) : f.isValid = true ↔ Spec.ValidField f :=
+theorem Protobuf.Spec.isValid_iff (f : Field) : f.isValid = true ↔ Protobuf.Spec.ValidField f :=
   Protobuf.Proofs.Message.isValid_iff f
 
-theorem Spec.encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
-    Protobuf.encode fs = Spec.encode fs :=
+theorem Protobuf.Spec.encode_eq (fs : List Field) (h : ∀ f ∈ fs, Protobuf.Spec.ValidField f) :
+    Protobuf.encode fs = Protobuf.Spec.encode fs :=
   Protobuf.Proofs.Message.encode_eq fs h
 
-theorem Spec.decode_iff (bs : List UInt8) (fs : List Field) :
-    decode bs = some fs ↔ Spec.Message bs fs :=
+theorem Protobuf.Spec.decode_iff (bs : List UInt8) (fs : List Field) :
+    decode bs = some fs ↔ Protobuf.Spec.Message bs fs :=
   Protobuf.Proofs.Message.decode_iff bs fs
 
-theorem Spec.decode_encode (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+theorem Protobuf.Spec.decode_encode (fs : List Field) (h : ∀ f ∈ fs, Protobuf.Spec.ValidField f) :
     decode (Protobuf.encode fs) = some fs :=
   Protobuf.Proofs.Message.decode_encode fs h
 
-theorem Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) :
-    ∀ f ∈ fs, Spec.ValidField f :=
+theorem Protobuf.Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) :
+    ∀ f ∈ fs, Protobuf.Spec.ValidField f :=
   Protobuf.Proofs.Message.decode_valid bs fs h
 
-theorem Spec.guide_vectors :
+theorem Protobuf.Spec.guide_vectors :
     Varint.encode 1 = [0x01] ∧
     Varint.encode 150 = [0x96, 0x01] ∧
     Varint.encode (2 ^ 64 - 2) = [0xfe, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
@@ -56,7 +56,7 @@ theorem Spec.guide_vectors :
       [0x08, 0x96, 0x01, 0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] := by
   decide
 
-theorem Spec.edge_vectors :
+theorem Protobuf.Spec.edge_vectors :
     Varint.encode (2 ^ 64 - 1) = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
     decode [0x0d, 0x01, 0x02, 0x03, 0x04] = some [⟨1, .i32 0x04030201⟩] ∧
     decode [0x09, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, 0x08] =
@@ -68,7 +68,7 @@ theorem Spec.edge_vectors :
     decode [] = some [] := by
   decide
 
-theorem Spec.reject_vectors :
+theorem Protobuf.Spec.reject_vectors :
     decode [0x08] = none ∧
     decode [0x08, 0x80] = none ∧
     decode [0x08, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x00] = none ∧
diff --git a/Proofs/Message.lean b/Protobuf/Proofs/Message.lean
similarity index 78%
rename from Proofs/Message.lean
rename to Protobuf/Proofs/Message.lean
index cb65b96..1c36d9c 100644
--- a/Proofs/Message.lean
+++ b/Protobuf/Proofs/Message.lean
@@ -1,16 +1,16 @@
 /-
   Fields and messages against the spec: `Field.isValid` decides
-  `Spec.ValidField`, the encoder writes `Spec.encode`, `decodeField`
-  reads exactly one record (`Spec.FieldBytes`) from the front of its
-  input, `decode` reads exactly a `Spec.Message`, decoding what the
+  `Protobuf.Spec.ValidField`, the encoder writes `Protobuf.Spec.encode`, `decodeField`
+  reads exactly one record (`Protobuf.Spec.FieldBytes`) from the front of its
+  input, `decode` reads exactly a `Protobuf.Spec.Message`, decoding what the
   encoder wrote gives the fields back, and every field the decoder
   returns is valid.
 -/
 
 import Protobuf
-import Spec.Defs
-import Proofs.Varint
-import Proofs.Fixed
+import Protobuf.Spec.Defs
+import Protobuf.Proofs.Varint
+import Protobuf.Proofs.Fixed
 
 namespace Protobuf.Proofs.Message
 
@@ -18,13 +18,13 @@ open Protobuf
 
 /-! ## Validity -/
 
-theorem isValid_iff (f : Field) : f.isValid = true ↔ Spec.ValidField f := by
+theorem isValid_iff (f : Field) : f.isValid = true ↔ Protobuf.Spec.ValidField f := by
   obtain ⟨n, v⟩ := f
-  cases v <;> simp [Field.isValid, Spec.ValidField, and_assoc]
+  cases v <;> simp [Field.isValid, Protobuf.Spec.ValidField, and_assoc]
 
 /-! ## The encoder -/
 
-theorem field_encode_eq (f : Field) (h : Spec.ValidField f) : f.encode = Spec.fieldBytes f := by
+theorem field_encode_eq (f : Field) (h : Protobuf.Spec.ValidField f) : f.encode = Protobuf.Spec.fieldBytes f := by
   obtain ⟨n, v⟩ := f
   obtain ⟨h1, h2, h3⟩ := h
   have h2 : n < 2 ^ 29 := h2
@@ -32,29 +32,29 @@ theorem field_encode_eq (f : Field) (h : Spec.ValidField f) : f.encode = Spec.fi
   cases v with
   | varint v =>
     have h3 : v < 2 ^ 64 := h3
-    show Varint.encode (n * 8 + 0) ++ Varint.encode v = Spec.varint (n * 8 + 0) ++ Spec.varint v
+    show Varint.encode (n * 8 + 0) ++ Varint.encode v = Protobuf.Spec.varint (n * 8 + 0) ++ Protobuf.Spec.varint v
     rw [Proofs.Varint.encode_eq _ (hn 0 (by decide)), Proofs.Varint.encode_eq _ h3]
   | i64 v =>
-    show Varint.encode (n * 8 + 1) ++ leBytes 8 v = Spec.varint (n * 8 + 1) ++ Spec.leBytes 8 v
+    show Varint.encode (n * 8 + 1) ++ leBytes 8 v = Protobuf.Spec.varint (n * 8 + 1) ++ Protobuf.Spec.leBytes 8 v
     rw [Proofs.Varint.encode_eq _ (hn 1 (by decide)), Proofs.Fixed.leBytes_eq]
   | len d =>
     have h3 : d.length < 2 ^ 31 - 16 := h3
     show Varint.encode (n * 8 + 2) ++ (Varint.encode d.length ++ d) =
-      Spec.varint (n * 8 + 2) ++ Spec.varint d.length ++ d
+      Protobuf.Spec.varint (n * 8 + 2) ++ Protobuf.Spec.varint d.length ++ d
     rw [Proofs.Varint.encode_eq _ (hn 2 (by decide)), Proofs.Varint.encode_eq _ (by omega),
       List.append_assoc]
   | i32 v =>
-    show Varint.encode (n * 8 + 5) ++ leBytes 4 v = Spec.varint (n * 8 + 5) ++ Spec.leBytes 4 v
+    show Varint.encode (n * 8 + 5) ++ leBytes 4 v = Protobuf.Spec.varint (n * 8 + 5) ++ Protobuf.Spec.leBytes 4 v
     rw [Proofs.Varint.encode_eq _ (hn 5 (by decide)), Proofs.Fixed.leBytes_eq]
 
 theorem encode_cons (f : Field) (fs : List Field) : encode (f :: fs) = f.encode ++ encode fs := by
   simp [encode]
 
 theorem spec_encode_cons (f : Field) (fs : List Field) :
-    Spec.encode (f :: fs) = Spec.fieldBytes f ++ Spec.encode fs := by
-  simp [Spec.encode]
+    Protobuf.Spec.encode (f :: fs) = Protobuf.Spec.fieldBytes f ++ Protobuf.Spec.encode fs := by
+  simp [Protobuf.Spec.encode]
 
-theorem encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) : encode fs = Spec.encode fs := by
+theorem encode_eq (fs : List Field) (h : ∀ f ∈ fs, Protobuf.Spec.ValidField f) : encode fs = Protobuf.Spec.encode fs := by
   induction fs with
   | nil => rfl
   | cons f fs ih =>
@@ -71,7 +71,7 @@ theorem take_short (l : List UInt8) (k : Nat) : ((l.take k).length < k) = (l.len
 
 theorem decodeField_iff (bs : List UInt8) (f : Field) (rest : List UInt8) :
     decodeField bs = some (f, rest) ↔
-      ∃ tag payload, bs = tag ++ payload ++ rest ∧ Spec.FieldBytes tag payload f := by
+      ∃ tag payload, bs = tag ++ payload ++ rest ∧ Protobuf.Spec.FieldBytes tag payload f := by
   constructor
   · intro h
     unfold decodeField at h
@@ -141,12 +141,12 @@ theorem decodeField_iff (bs : List UInt8) (f : Field) (rest : List UInt8) :
   · rintro ⟨tag, payload, rfl, hshape, ht32, hnum, hn, hm⟩
     obtain ⟨num, val⟩ := f
     have hd : Varint.decodeAux 5 (tag ++ payload ++ rest) =
-        some (Spec.groupsValue tag, payload ++ rest) :=
+        some (Protobuf.Spec.groupsValue tag, payload ++ rest) :=
       (Proofs.Varint.decodeAux_iff 5 _ _ _).mpr ⟨tag, List.append_assoc _ _ _, hshape, rfl⟩
-    have hc : ¬(2 ^ 32 ≤ Spec.groupsValue tag ∨ Spec.groupsValue tag / 8 = 0) := by
+    have hc : ¬(2 ^ 32 ≤ Protobuf.Spec.groupsValue tag ∨ Protobuf.Spec.groupsValue tag / 8 = 0) := by
       simp only at hnum hn
       omega
-    have hnum' : num = Spec.groupsValue tag / 8 := hnum
+    have hnum' : num = Protobuf.Spec.groupsValue tag / 8 := hnum
     unfold decodeField
     simp only [take_short]
     rw [hd]
@@ -185,7 +185,7 @@ theorem decodeField_iff (bs : List UInt8) (f : Field) (rest : List UInt8) :
 
 /-- Whatever `decodeAux` returns, with any fuel, is a message. -/
 theorem decodeAux_sound (fuel : Nat) :
-    ∀ bs fs, decodeAux fuel bs = some fs → Spec.Message bs fs := by
+    ∀ bs fs, decodeAux fuel bs = some fs → Protobuf.Spec.Message bs fs := by
   induction fuel with
   | zero =>
     intro bs fs h
@@ -218,7 +218,7 @@ theorem decodeAux_sound (fuel : Nat) :
 
 /-- A message is read whole by `decodeAux` with fuel at least its length:
     each record takes at least one byte, since its tag does. -/
-theorem decodeAux_complete {bs : List UInt8} {fs : List Field} (h : Spec.Message bs fs) :
+theorem decodeAux_complete {bs : List UInt8} {fs : List Field} (h : Protobuf.Spec.Message bs fs) :
     ∀ fuel, bs.length ≤ fuel → decodeAux fuel bs = some fs := by
   induction h with
   | nil => intro fuel _; cases fuel <;> rfl
@@ -235,13 +235,13 @@ theorem decodeAux_complete {bs : List UInt8} {fs : List Field} (h : Spec.Message
     simp only [decodeAux, hd]
     rw [ih fuel' (by omega)]
 
-theorem decode_iff (bs : List UInt8) (fs : List Field) : decode bs = some fs ↔ Spec.Message bs fs :=
+theorem decode_iff (bs : List UInt8) (fs : List Field) : decode bs = some fs ↔ Protobuf.Spec.Message bs fs :=
   ⟨decodeAux_sound bs.length bs fs, fun h => decodeAux_complete h bs.length (Nat.le_refl _)⟩
 
 /-! ## Decoded fields are valid -/
 
-theorem fieldBytes_valid {tag payload : List UInt8} {f : Field} (h : Spec.FieldBytes tag payload f) :
-    Spec.ValidField f := by
+theorem fieldBytes_valid {tag payload : List UInt8} {f : Field} (h : Protobuf.Spec.FieldBytes tag payload f) :
+    Protobuf.Spec.ValidField f := by
   obtain ⟨num, val⟩ := f
   obtain ⟨_, ht, hnum, hn, hm⟩ := h
   simp only at hnum hn hm
@@ -262,8 +262,8 @@ theorem fieldBytes_valid {tag payload : List UInt8} {f : Field} (h : Spec.FieldB
     exact this
   · exact hm.elim
 
-theorem message_valid {bs : List UInt8} {fs : List Field} (h : Spec.Message bs fs) :
-    ∀ f ∈ fs, Spec.ValidField f := by
+theorem message_valid {bs : List UInt8} {fs : List Field} (h : Protobuf.Spec.Message bs fs) :
+    ∀ f ∈ fs, Protobuf.Spec.ValidField f := by
   induction h with
   | nil => simp
   | cons hfb _ ih =>
@@ -273,21 +273,21 @@ theorem message_valid {bs : List UInt8} {fs : List Field} (h : Spec.Message bs f
     · exact ih g hg
 
 theorem decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) :
-    ∀ f ∈ fs, Spec.ValidField f :=
+    ∀ f ∈ fs, Protobuf.Spec.ValidField f :=
   message_valid ((decode_iff bs fs).mp h)
 
 /-! ## Round trip -/
 
 /-- The shortest varint of a valid tag has at most five bytes. -/
 theorem tag_bytes (n w : Nat) (hn : n < 2 ^ 29) (hw : w < 8) :
-    Spec.VarintShape 5 (Spec.varint (n * 8 + w)) ∧ Spec.groupsValue (Spec.varint (n * 8 + w)) = n * 8 + w := by
+    Protobuf.Spec.VarintShape 5 (Protobuf.Spec.varint (n * 8 + w)) ∧ Protobuf.Spec.groupsValue (Protobuf.Spec.varint (n * 8 + w)) = n * 8 + w := by
   have hs := Proofs.Varint.varint_shape (n * 8 + w)
   have h5 : (2 : Nat) ^ 32 ≤ 128 ^ 5 := by decide
   exact ⟨Proofs.Varint.shape_mono hs.1 (Proofs.Varint.varint_length _ 5 (by decide) (by omega)), hs.2⟩
 
 /-- The bytes the encoder writes for a valid field are one record. -/
-theorem fieldBytes_split (f : Field) (h : Spec.ValidField f) :
-    ∃ tag payload, Spec.fieldBytes f = tag ++ payload ∧ Spec.FieldBytes tag payload f := by
+theorem fieldBytes_split (f : Field) (h : Protobuf.Spec.ValidField f) :
+    ∃ tag payload, Protobuf.Spec.fieldBytes f = tag ++ payload ∧ Protobuf.Spec.FieldBytes tag payload f := by
   obtain ⟨n, val⟩ := f
   obtain ⟨h1, h2, h3⟩ := h
   have h1 : 1 ≤ n := h1
@@ -296,7 +296,7 @@ theorem fieldBytes_split (f : Field) (h : Spec.ValidField f) :
   | varint v =>
     have h3 : v < 2 ^ 64 := h3
     obtain ⟨hs, hg⟩ := tag_bytes n 0 h2 (by decide)
-    refine ⟨Spec.varint (n * 8 + 0), Spec.varint v, rfl, hs, by rw [hg]; omega,
+    refine ⟨Protobuf.Spec.varint (n * 8 + 0), Protobuf.Spec.varint v, rfl, hs, by rw [hg]; omega,
       show n = _ by rw [hg]; omega, h1, ?_⟩
     rw [hg, show (n * 8 + 0) % 8 = 0 by omega]
     have hv := Proofs.Varint.varint_shape v
@@ -306,7 +306,7 @@ theorem fieldBytes_split (f : Field) (h : Spec.ValidField f) :
   | i64 v =>
     have h3 : v < 2 ^ 64 := h3
     obtain ⟨hs, hg⟩ := tag_bytes n 1 h2 (by decide)
-    refine ⟨Spec.varint (n * 8 + 1), Spec.leBytes 8 v, rfl, hs, by rw [hg]; omega,
+    refine ⟨Protobuf.Spec.varint (n * 8 + 1), Protobuf.Spec.leBytes 8 v, rfl, hs, by rw [hg]; omega,
       show n = _ by rw [hg]; omega, h1, ?_⟩
     rw [hg, show (n * 8 + 1) % 8 = 1 by omega]
     exact ⟨Proofs.Fixed.leBytes_length 8 v,
@@ -314,25 +314,25 @@ theorem fieldBytes_split (f : Field) (h : Spec.ValidField f) :
   | len d =>
     have h3 : d.length < 2 ^ 31 - 16 := h3
     obtain ⟨hs, hg⟩ := tag_bytes n 2 h2 (by decide)
-    refine ⟨Spec.varint (n * 8 + 2), Spec.varint d.length ++ d, List.append_assoc _ _ _, hs,
+    refine ⟨Protobuf.Spec.varint (n * 8 + 2), Protobuf.Spec.varint d.length ++ d, List.append_assoc _ _ _, hs,
       by rw [hg]; omega, show n = _ by rw [hg]; omega, h1, ?_⟩
     rw [hg, show (n * 8 + 2) % 8 = 2 by omega]
     have hv := Proofs.Varint.varint_shape d.length
     have h5 : (2 : Nat) ^ 31 ≤ 128 ^ 5 := by decide
-    exact ⟨Spec.varint d.length, rfl,
+    exact ⟨Protobuf.Spec.varint d.length, rfl,
       Proofs.Varint.shape_mono hv.1 (Proofs.Varint.varint_length _ 5 (by decide) (by omega)),
       hv.2, h3⟩
   | i32 v =>
     have h3 : v < 2 ^ 32 := h3
     obtain ⟨hs, hg⟩ := tag_bytes n 5 h2 (by decide)
-    refine ⟨Spec.varint (n * 8 + 5), Spec.leBytes 4 v, rfl, hs, by rw [hg]; omega,
+    refine ⟨Protobuf.Spec.varint (n * 8 + 5), Protobuf.Spec.leBytes 4 v, rfl, hs, by rw [hg]; omega,
       show n = _ by rw [hg]; omega, h1, ?_⟩
     rw [hg, show (n * 8 + 5) % 8 = 5 by omega]
     exact ⟨Proofs.Fixed.leBytes_length 4 v,
       (Proofs.Fixed.leValue_leBytes 4 v (by simpa using h3)).symm⟩
 
-theorem encode_message (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
-    Spec.Message (Spec.encode fs) fs := by
+theorem encode_message (fs : List Field) (h : ∀ f ∈ fs, Protobuf.Spec.ValidField f) :
+    Protobuf.Spec.Message (Protobuf.Spec.encode fs) fs := by
   induction fs with
   | nil => exact .nil
   | cons f fs ih =>
@@ -340,7 +340,7 @@ theorem encode_message (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
     rw [spec_encode_cons, he]
     exact .cons hfb (ih fun g hg => h g (by simp [hg]))
 
-theorem decode_encode (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+theorem decode_encode (fs : List Field) (h : ∀ f ∈ fs, Protobuf.Spec.ValidField f) :
     decode (encode fs) = some fs := by
   rw [encode_eq fs h]
   exact (decode_iff _ _).mpr (encode_message fs h)
diff --git a/Proofs/Varint.lean b/Protobuf/Proofs/Varint.lean
similarity index 74%
rename from Proofs/Varint.lean
rename to Protobuf/Proofs/Varint.lean
index 19655d5..1f59fea 100644
--- a/Proofs/Varint.lean
+++ b/Protobuf/Proofs/Varint.lean
@@ -1,13 +1,13 @@
 /-
   The varint encoder and decoder of `Protobuf/Varint.lean` against the
-  spec: `encode` writes `Spec.varint`, `decodeAux k` reads exactly one
-  varint of at most `k` bytes (shape `Spec.VarintShape k`, value
-  `Spec.groupsValue`), `decode` reads exactly a `Spec.IsVarint`, and
+  spec: `encode` writes `Protobuf.Spec.varint`, `decodeAux k` reads exactly one
+  varint of at most `k` bytes (shape `Protobuf.Spec.VarintShape k`, value
+  `Protobuf.Spec.groupsValue`), `decode` reads exactly a `Protobuf.Spec.IsVarint`, and
   decoding what the encoder wrote gives the number back.
 -/
 
 import Protobuf
-import Spec.Defs
+import Protobuf.Spec.Defs
 
 namespace Protobuf.Proofs.Varint
 
@@ -21,11 +21,11 @@ theorem sum_map_mul (c : Nat) (g : Nat → Nat) (l : List Nat) :
   | nil => simp
   | cons a l ih => simp [List.sum_cons, ih, Nat.mul_add]
 
-theorem groupsValue_nil : Spec.groupsValue [] = 0 := rfl
+theorem groupsValue_nil : Protobuf.Spec.groupsValue [] = 0 := rfl
 
 theorem groupsValue_cons (b : UInt8) (bs : List UInt8) :
-    Spec.groupsValue (b :: bs) = b.toNat % 128 + 128 * Spec.groupsValue bs := by
-  unfold Spec.groupsValue
+    Protobuf.Spec.groupsValue (b :: bs) = b.toNat % 128 + 128 * Protobuf.Spec.groupsValue bs := by
+  unfold Protobuf.Spec.groupsValue
   rw [List.length_cons, List.range_succ_eq_map, List.map_cons, List.sum_cons, List.map_map,
     ← sum_map_mul]
   congr 1
@@ -36,20 +36,20 @@ theorem groupsValue_cons (b : UInt8) (bs : List UInt8) :
     simp only [Function.comp, Nat.succ_eq_add_one, List.getD_cons_succ, Nat.pow_succ]
     rw [Nat.mul_comm (128 ^ i) 128, Nat.mul_left_comm]
 
-theorem shape_zero (bs : List UInt8) : ¬ Spec.VarintShape 0 bs := by
+theorem shape_zero (bs : List UInt8) : ¬ Protobuf.Spec.VarintShape 0 bs := by
   intro ⟨h1, h2, _⟩
   exact h1 (List.eq_nil_of_length_eq_zero (Nat.le_zero.mp h2))
 
-theorem shape_nil (k : Nat) : ¬ Spec.VarintShape k [] := fun h => h.1 rfl
+theorem shape_nil (k : Nat) : ¬ Protobuf.Spec.VarintShape k [] := fun h => h.1 rfl
 
 theorem shape_cons (k : Nat) (b : UInt8) (bs : List UInt8) :
-    Spec.VarintShape (k + 1) (b :: bs) ↔
-      (b.toNat < 128 ∧ bs = []) ∨ (128 ≤ b.toNat ∧ Spec.VarintShape k bs) := by
+    Protobuf.Spec.VarintShape (k + 1) (b :: bs) ↔
+      (b.toNat < 128 ∧ bs = []) ∨ (128 ≤ b.toNat ∧ Protobuf.Spec.VarintShape k bs) := by
   cases bs with
   | nil =>
-    simp [Spec.VarintShape]
+    simp [Protobuf.Spec.VarintShape]
   | cons c cs =>
-    simp [Spec.VarintShape, List.dropLast_cons_cons, List.getLast?_cons_cons]
+    simp [Protobuf.Spec.VarintShape, List.dropLast_cons_cons, List.getLast?_cons_cons]
     exact ⟨fun ⟨h1, ⟨h2, h3⟩, h4⟩ => ⟨h2, h1, h3, h4⟩, fun ⟨h2, h1, h3, h4⟩ => ⟨h1, ⟨h2, h3⟩, h4⟩⟩
 
 
@@ -57,10 +57,10 @@ theorem shape_cons (k : Nat) (b : UInt8) (bs : List UInt8) :
 
 /-- The right-hand side of `decodeAux_iff` at `k + 1`, one byte at a time. -/
 theorem split_cons (k : Nat) (b : UInt8) (bs : List UInt8) (v : Nat) (rest : List UInt8) :
-    (∃ pre, b :: bs = pre ++ rest ∧ Spec.VarintShape (k + 1) pre ∧ v = Spec.groupsValue pre) ↔
+    (∃ pre, b :: bs = pre ++ rest ∧ Protobuf.Spec.VarintShape (k + 1) pre ∧ v = Protobuf.Spec.groupsValue pre) ↔
       (b.toNat < 128 ∧ bs = rest ∧ v = b.toNat) ∨
-      (128 ≤ b.toNat ∧ ∃ v', (∃ pre, bs = pre ++ rest ∧ Spec.VarintShape k pre ∧
-        v' = Spec.groupsValue pre) ∧ v = b.toNat % 128 + 128 * v') := by
+      (128 ≤ b.toNat ∧ ∃ v', (∃ pre, bs = pre ++ rest ∧ Protobuf.Spec.VarintShape k pre ∧
+        v' = Protobuf.Spec.groupsValue pre) ∧ v = b.toNat % 128 + 128 * v') := by
   constructor
   · rintro ⟨pre, h, hs, hv⟩
     cases pre with
@@ -84,7 +84,7 @@ theorem split_cons (k : Nat) (b : UInt8) (bs : List UInt8) (v : Nat) (rest : Lis
 
 theorem decodeAux_iff (k : Nat) (bs : List UInt8) (v : Nat) (rest : List UInt8) :
     Varint.decodeAux k bs = some (v, rest) ↔
-      ∃ pre, bs = pre ++ rest ∧ Spec.VarintShape k pre ∧ v = Spec.groupsValue pre := by
+      ∃ pre, bs = pre ++ rest ∧ Protobuf.Spec.VarintShape k pre ∧ v = Protobuf.Spec.groupsValue pre := by
   induction k generalizing bs v with
   | zero =>
     simp only [Varint.decodeAux, reduceCtorEq, false_iff, not_exists, not_and]
@@ -123,7 +123,7 @@ theorem decodeAux_iff (k : Nat) (bs : List UInt8) (v : Nat) (rest : List UInt8)
 
 
 theorem decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) :
-    Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Spec.IsVarint pre v := by
+    Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Protobuf.Spec.IsVarint pre v := by
   unfold Varint.decode
   cases h : Varint.decodeAux 10 bs with
   | none =>
@@ -152,8 +152,8 @@ theorem toUInt8_toNat_of_lt (n : Nat) (h : n < 256) : n.toUInt8.toNat = n := by
   omega
 
 theorem varintAux_succ (f n : Nat) :
-    Spec.varintAux (f + 1) n =
-      if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: Spec.varintAux f (n / 128) :=
+    Protobuf.Spec.varintAux (f + 1) n =
+      if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: Protobuf.Spec.varintAux f (n / 128) :=
   rfl
 
 theorem div_lt (n f : Nat) (h : n < 128 ^ (f + 1)) : n / 128 < 128 ^ f :=
@@ -163,24 +163,24 @@ theorem lt_pow (n : Nat) : n < 128 ^ (n + 1) :=
   Nat.lt_of_lt_of_le (Nat.lt_pow_self (by decide)) (Nat.pow_le_pow_right (by decide) (by omega))
 
 theorem single_shape (n : Nat) (h : n < 128) :
-    Spec.VarintShape [n.toUInt8].length [n.toUInt8] ∧ Spec.groupsValue [n.toUInt8] = n := by
+    Protobuf.Spec.VarintShape [n.toUInt8].length [n.toUInt8] ∧ Protobuf.Spec.groupsValue [n.toUInt8] = n := by
   have h1 : n.toUInt8.toNat = n := toUInt8_toNat_of_lt n (by omega)
   refine ⟨(shape_cons 0 _ []).mpr (Or.inl ⟨by omega, rfl⟩), ?_⟩
   rw [groupsValue_cons, groupsValue_nil, h1]
   omega
 
 theorem cons_shape (n : Nat) (rest : List UInt8)
-    (hr : Spec.VarintShape rest.length rest ∧ Spec.groupsValue rest = n / 128) :
-    Spec.VarintShape ((n % 128 + 128).toUInt8 :: rest).length ((n % 128 + 128).toUInt8 :: rest) ∧
-      Spec.groupsValue ((n % 128 + 128).toUInt8 :: rest) = n := by
+    (hr : Protobuf.Spec.VarintShape rest.length rest ∧ Protobuf.Spec.groupsValue rest = n / 128) :
+    Protobuf.Spec.VarintShape ((n % 128 + 128).toUInt8 :: rest).length ((n % 128 + 128).toUInt8 :: rest) ∧
+      Protobuf.Spec.groupsValue ((n % 128 + 128).toUInt8 :: rest) = n := by
   have h1 : (n % 128 + 128).toUInt8.toNat = n % 128 + 128 := toUInt8_toNat_of_lt _ (by omega)
   refine ⟨(shape_cons rest.length _ rest).mpr (Or.inr ⟨by omega, hr.1⟩), ?_⟩
   rw [groupsValue_cons, hr.2, h1]
   omega
 
 theorem varintAux_shape (f : Nat) : ∀ n, n < 128 ^ (f + 1) →
-    Spec.VarintShape (Spec.varintAux (f + 1) n).length (Spec.varintAux (f + 1) n) ∧
-      Spec.groupsValue (Spec.varintAux (f + 1) n) = n := by
+    Protobuf.Spec.VarintShape (Protobuf.Spec.varintAux (f + 1) n).length (Protobuf.Spec.varintAux (f + 1) n) ∧
+      Protobuf.Spec.groupsValue (Protobuf.Spec.varintAux (f + 1) n) = n := by
   induction f with
   | zero =>
     intro n hn
@@ -198,15 +198,15 @@ theorem varintAux_shape (f : Nat) : ∀ n, n < 128 ^ (f + 1) →
       exact cons_shape n _ (ih (n / 128) (div_lt n (f + 1) hn))
 
 theorem varint_shape (n : Nat) :
-    Spec.VarintShape (Spec.varint n).length (Spec.varint n) ∧ Spec.groupsValue (Spec.varint n) = n :=
+    Protobuf.Spec.VarintShape (Protobuf.Spec.varint n).length (Protobuf.Spec.varint n) ∧ Protobuf.Spec.groupsValue (Protobuf.Spec.varint n) = n :=
   varintAux_shape n n (lt_pow n)
 
 theorem varintAux_length (f : Nat) :
-    ∀ n k, 1 ≤ k → n < 128 ^ k → (Spec.varintAux f n).length ≤ k := by
+    ∀ n k, 1 ≤ k → n < 128 ^ k → (Protobuf.Spec.varintAux f n).length ≤ k := by
   induction f with
   | zero =>
     intro n k _ _
-    simp [Spec.varintAux]
+    simp [Protobuf.Spec.varintAux]
   | succ f ih =>
     intro n k hk hn
     rw [varintAux_succ]
@@ -223,29 +223,29 @@ theorem varintAux_length (f : Nat) :
       have := ih (n / 128) j hj (div_lt n j hn)
       omega
 
-theorem varint_length (n k : Nat) (hk : 1 ≤ k) (h : n < 128 ^ k) : (Spec.varint n).length ≤ k :=
+theorem varint_length (n k : Nat) (hk : 1 ≤ k) (h : n < 128 ^ k) : (Protobuf.Spec.varint n).length ≤ k :=
   varintAux_length (n + 1) n k hk h
 
-theorem shape_mono {k k' : Nat} {bs : List UInt8} (h : Spec.VarintShape k bs) (hk : k ≤ k') :
-    Spec.VarintShape k' bs :=
+theorem shape_mono {k k' : Nat} {bs : List UInt8} (h : Protobuf.Spec.VarintShape k bs) (hk : k ≤ k') :
+    Protobuf.Spec.VarintShape k' bs :=
   ⟨h.1, Nat.le_trans h.2.1 hk, h.2.2⟩
 
 theorem decodeAux_varint (n k : Nat) (rest : List UInt8) (hk : 1 ≤ k) (h : n < 128 ^ k) :
-    Varint.decodeAux k (Spec.varint n ++ rest) = some (n, rest) := by
+    Varint.decodeAux k (Protobuf.Spec.varint n ++ rest) = some (n, rest) := by
   have hs := varint_shape n
   exact (decodeAux_iff k _ n rest).mpr
-    ⟨Spec.varint n, rfl, shape_mono hs.1 (varint_length n k hk h), hs.2.symm⟩
+    ⟨Protobuf.Spec.varint n, rfl, shape_mono hs.1 (varint_length n k hk h), hs.2.symm⟩
 
 /-! ## The encoder -/
 
-theorem encodeAux_eq (f n : Nat) : Varint.encodeAux f n = Spec.varintAux f n := by
+theorem encodeAux_eq (f n : Nat) : Varint.encodeAux f n = Protobuf.Spec.varintAux f n := by
   induction f generalizing n with
   | zero => rfl
-  | succ f ih => simp only [Varint.encodeAux, Spec.varintAux, ih]
+  | succ f ih => simp only [Varint.encodeAux, Protobuf.Spec.varintAux, ih]
 
 /-- More fuel than the digits need changes nothing. -/
 theorem varintAux_add (f g : Nat) :
-    ∀ n, n < 128 ^ (f + 1) → Spec.varintAux (f + g + 1) n = Spec.varintAux (f + 1) n := by
+    ∀ n, n < 128 ^ (f + 1) → Protobuf.Spec.varintAux (f + g + 1) n = Protobuf.Spec.varintAux (f + 1) n := by
   induction f with
   | zero =>
     intro n hn
@@ -261,8 +261,8 @@ theorem varintAux_add (f g : Nat) :
       rw [Nat.add_right_comm f 1 g, ih (n / 128) (div_lt n (f + 1) hn)]
 
 theorem varintAux_eq_varint (f n : Nat) (hf : 1 ≤ f) (h : n < 128 ^ f) :
-    Spec.varintAux f n = Spec.varint n := by
-  unfold Spec.varint
+    Protobuf.Spec.varintAux f n = Protobuf.Spec.varint n := by
+  unfold Protobuf.Spec.varint
   obtain ⟨f, rfl⟩ : ∃ j, f = j + 1 := ⟨f - 1, by omega⟩
   rcases Nat.le_total f n with hle | hle
   · have := varintAux_add f (n - f) n h
@@ -274,7 +274,7 @@ theorem varintAux_eq_varint (f n : Nat) (hf : 1 ≤ f) (h : n < 128 ^ f) :
 
 theorem two_pow_le : 2 ^ 64 ≤ 128 ^ 10 := by decide
 
-theorem encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Spec.varint n := by
+theorem encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Protobuf.Spec.varint n := by
   unfold Varint.encode
   rw [encodeAux_eq]
   exact varintAux_eq_varint 10 n (by decide) (Nat.lt_of_lt_of_le h two_pow_le)
diff --git a/Spec.lean b/Protobuf/Spec.lean
similarity index 79%
rename from Spec.lean
rename to Protobuf/Spec.lean
index 135ee17..00a6701 100644
--- a/Spec.lean
+++ b/Protobuf/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 `Protobuf/Proofs.lean`, under
   the same names; `lake comparator` checks that each one proves exactly
   the statement written here. The `sorry`s below are expected in this
   file only.
@@ -13,55 +13,55 @@
 -/
 
 import Protobuf
-import Spec.Defs
+import Protobuf.Spec.Defs
 
 open Protobuf
 
 /-! ## Varints -/
 
 /-- The encoder writes the shortest varint. -/
-theorem Spec.varint_encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Spec.varint n := sorry
+theorem Protobuf.Spec.varint_encode_eq (n : Nat) (h : n < 2 ^ 64) : Varint.encode n = Protobuf.Spec.varint n := sorry
 
 /-- The decoder reads exactly one varint from the front of its input:
     up to ten bytes, the last without its high bit, and returns its
     value and the rest of the input untouched. Anything else, including
     input that ends inside the varint and an eleventh byte, is
     refused. -/
-theorem Spec.varint_decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) :
-    Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Spec.IsVarint pre v := sorry
+theorem Protobuf.Spec.varint_decode_iff (bs : List UInt8) (v : Nat) (rest : List UInt8) :
+    Varint.decode bs = some (v, rest) ↔ ∃ pre, bs = pre ++ rest ∧ Protobuf.Spec.IsVarint pre v := sorry
 
 /-- Round trip: decoding what the encoder wrote gives the number back,
     and leaves what follows untouched. -/
-theorem Spec.varint_decode_encode (n : Nat) (rest : List UInt8) (h : n < 2 ^ 64) :
+theorem Protobuf.Spec.varint_decode_encode (n : Nat) (rest : List UInt8) (h : n < 2 ^ 64) :
     Varint.decode (Varint.encode n ++ rest) = some (n, rest) := sorry
 
 /-! ## Messages -/
 
 /-- `isValid` decides exactly which fields can be written. -/
-theorem Spec.isValid_iff (f : Field) : f.isValid = true ↔ Spec.ValidField f := sorry
+theorem Protobuf.Spec.isValid_iff (f : Field) : f.isValid = true ↔ Protobuf.Spec.ValidField f := sorry
 
 /-- The encoder writes each field as the encoding guide describes, with
     every varint in its shortest form. -/
-theorem Spec.encode_eq (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
-    Protobuf.encode fs = Spec.encode fs := sorry
+theorem Protobuf.Spec.encode_eq (fs : List Field) (h : ∀ f ∈ fs, Protobuf.Spec.ValidField f) :
+    Protobuf.encode fs = Protobuf.Spec.encode fs := sorry
 
 /-- `decode` returns `fs` exactly when the bytes split into records, one
-    per field of `fs`, in order, by the rules of `Spec.FieldBytes`. So it
+    per field of `fs`, in order, by the rules of `Protobuf.Spec.FieldBytes`. So it
     reads every message made of `VARINT`, `I64`, `LEN` and `I32` records
     with field numbers from 1 to 2^29 - 1, refuses everything else (a
     record cut short, a length past the end, field number 0, a group, an
     unknown wire type, an oversized tag or length), and returns the
     fields as written. -/
-theorem Spec.decode_iff (bs : List UInt8) (fs : List Field) :
-    decode bs = some fs ↔ Spec.Message bs fs := sorry
+theorem Protobuf.Spec.decode_iff (bs : List UInt8) (fs : List Field) :
+    decode bs = some fs ↔ Protobuf.Spec.Message bs fs := sorry
 
 /-- Round trip: decoding what the encoder wrote gives the fields back. -/
-theorem Spec.decode_encode (fs : List Field) (h : ∀ f ∈ fs, Spec.ValidField f) :
+theorem Protobuf.Spec.decode_encode (fs : List Field) (h : ∀ f ∈ fs, Protobuf.Spec.ValidField f) :
     decode (Protobuf.encode fs) = some fs := sorry
 
 /-- Every field the decoder returns can be written again. -/
-theorem Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) :
-    ∀ f ∈ fs, Spec.ValidField f := sorry
+theorem Protobuf.Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = some fs) :
+    ∀ f ∈ fs, Protobuf.Spec.ValidField f := sorry
 
 /-! ## Test vectors -/
 
@@ -70,7 +70,7 @@ theorem Spec.decode_valid (bs : List UInt8) (fs : List Field) (h : decode bs = s
     field 1 set to 150, `Test2` with field 2 set to "testing", `Test3`
     holding the first message in field 3, and `Test4` with field 4 set
     to "hello" and field 5 packed with 1, 2 and 3. -/
-theorem Spec.guide_vectors :
+theorem Protobuf.Spec.guide_vectors :
     Varint.encode 1 = [0x01] ∧
     Varint.encode 150 = [0x96, 0x01] ∧
     Varint.encode (2 ^ 64 - 2) = [0xfe, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
@@ -88,7 +88,7 @@ theorem Spec.guide_vectors :
     parsers' readings of unusual varints, not in shortest form, and ten
     bytes with bits past the 64th; the largest field number; and the
     empty message. -/
-theorem Spec.edge_vectors :
+theorem Protobuf.Spec.edge_vectors :
     Varint.encode (2 ^ 64 - 1) = [0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0xff, 0x01] ∧
     decode [0x0d, 0x01, 0x02, 0x03, 0x04] = some [⟨1, .i32 0x04030201⟩] ∧
     decode [0x09, 0x01, 0x02, 0x03, 0x04, 0x05, 0x06, 0x07, 0x08] =
@@ -104,7 +104,7 @@ theorem Spec.edge_vectors :
     short, a group start and a group end, wire types 6 and 7, a tag of
     2^32 or more (from exactly 2^32, which would be field number 2^29),
     and a tag or length longer than five bytes. -/
-theorem Spec.reject_vectors :
+theorem Protobuf.Spec.reject_vectors :
     decode [0x08] = none ∧
     decode [0x08, 0x80] = none ∧
     decode [0x08, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x80, 0x00] = none ∧
diff --git a/Spec/Defs.lean b/Protobuf/Spec/Defs.lean
similarity index 60%
rename from Spec/Defs.lean
rename to Protobuf/Spec/Defs.lean
index b7c213b..052486c 100644
--- a/Spec/Defs.lean
+++ b/Protobuf/Spec/Defs.lean
@@ -2,7 +2,7 @@
   The definitions the specification uses, written from the Protobuf
   encoding guide (https://protobuf.dev/programming-guides/encoding/)
   independently of the code in `Protobuf/`. Part of the approved
-  specification, with `Spec.lean` and `Protobuf/Types.lean`.
+  specification, with `Protobuf/Spec.lean` and `Protobuf/Types.lean`.
 
   Both the challenge file and the proofs import this file, so each
   statement means the same thing on both sides. The `example`s check the
@@ -24,12 +24,12 @@ one to ten bytes. -/
 
 /-- The number the low seven bits of each byte make, least significant
     group first. -/
-def Spec.groupsValue (bs : List UInt8) : Nat :=
+def Protobuf.Spec.groupsValue (bs : List UInt8) : Nat :=
   ((List.range bs.length).map fun i => (bs.getD i 0).toNat % 128 * 128 ^ i).sum
 
 /-- The shape of a varint of at most `k` bytes: at least one byte, every
     byte but the last with its high bit set, the last without it. -/
-def Spec.VarintShape (k : Nat) (bs : List UInt8) : Prop :=
+def Protobuf.Spec.VarintShape (k : Nat) (bs : List UInt8) : Prop :=
   bs ≠ [] ∧ bs.length ≤ k ∧
     (∀ b ∈ bs.dropLast, 128 ≤ b.toNat) ∧ (∀ b ∈ bs.getLast?, b.toNat < 128)
 
@@ -37,25 +37,25 @@ def Spec.VarintShape (k : Nat) (bs : List UInt8) : Prop :=
     bytes and drop any bits above the 64th, so a value is its groups
     modulo 2^64. A varint need not be in its shortest form: the
     reference parsers read `80 00` as 0. -/
-def Spec.IsVarint (bs : List UInt8) (v : Nat) : Prop :=
-  Spec.VarintShape 10 bs ∧ v = Spec.groupsValue bs % 2 ^ 64
+def Protobuf.Spec.IsVarint (bs : List UInt8) (v : Nat) : Prop :=
+  Protobuf.Spec.VarintShape 10 bs ∧ v = Protobuf.Spec.groupsValue bs % 2 ^ 64
 
 /-- The shortest varint for `n`, as an encoder writes it: seven bits at
     a time, least significant first, with the high bit set on every
     byte but the last. `fuel` bounds the number of bytes; `n + 1` is
     always enough. -/
-def Spec.varintAux : Nat → Nat → List UInt8
+def Protobuf.Spec.varintAux : Nat → Nat → List UInt8
   | 0, _ => []
   | fuel + 1, n =>
-    if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: Spec.varintAux fuel (n / 128)
+    if n < 128 then [n.toUInt8] else (n % 128 + 128).toUInt8 :: Protobuf.Spec.varintAux fuel (n / 128)
 
-def Spec.varint (n : Nat) : List UInt8 := Spec.varintAux (n + 1) n
+def Protobuf.Spec.varint (n : Nat) : List UInt8 := Protobuf.Spec.varintAux (n + 1) n
 
 -- The guide's examples: 1 is `01`, and 150 is `96 01`.
-example : Spec.varint 1 = [0x01] := by decide
-example : Spec.varint 150 = [0x96, 0x01] := by decide
-example : Spec.groupsValue [0x96, 0x01] = 150 := by decide
-example : Spec.VarintShape 10 [0x96, 0x01] := by unfold Spec.VarintShape; decide
+example : Protobuf.Spec.varint 1 = [0x01] := by decide
+example : Protobuf.Spec.varint 150 = [0x96, 0x01] := by decide
+example : Protobuf.Spec.groupsValue [0x96, 0x01] = 150 := by decide
+example : Protobuf.Spec.VarintShape 10 [0x96, 0x01] := by unfold Protobuf.Spec.VarintShape; decide
 
 /-! ## Fixed-width values
 
@@ -65,15 +65,15 @@ data. ... Similarly `float` and `fixed32` have wire type `I32`, which
 tells it to expect four bytes instead." The bytes are little-endian. -/
 
 /-- The bytes read as a number, least significant first. -/
-def Spec.leValue (bs : List UInt8) : Nat :=
+def Protobuf.Spec.leValue (bs : List UInt8) : Nat :=
   ((List.range bs.length).map fun i => (bs.getD i 0).toNat * 256 ^ i).sum
 
 /-- `n` in `k` bytes, least significant first. -/
-def Spec.leBytes (k n : Nat) : List UInt8 :=
+def Protobuf.Spec.leBytes (k n : Nat) : List UInt8 :=
   (List.range k).map fun i => (n / 256 ^ i % 256).toUInt8
 
-example : Spec.leValue [0x01, 0x02, 0x03, 0x04] = 0x04030201 := by decide
-example : Spec.leBytes 4 0x04030201 = [0x01, 0x02, 0x03, 0x04] := by decide
+example : Protobuf.Spec.leValue [0x01, 0x02, 0x03, 0x04] = 0x04030201 := by decide
+example : Protobuf.Spec.leBytes 4 0x04030201 = [0x01, 0x02, 0x03, 0x04] := by decide
 
 /-! ## Fields and messages
 
@@ -98,7 +98,7 @@ outside this library; wire types 6 and 7 do not exist. -/
 /-- A field the encoder can write: a field number from 1 to 2^29 - 1,
     and a value that fits its wire type, with bytes the C++ parser
     reads. -/
-def Spec.ValidField (f : Field) : Prop :=
+def Protobuf.Spec.ValidField (f : Field) : Prop :=
   1 ≤ f.number ∧ f.number < 2 ^ 29 ∧
   match f.value with
   | .varint v => v < 2 ^ 64
@@ -107,47 +107,47 @@ def Spec.ValidField (f : Field) : Prop :=
   | .i32 v => v < 2 ^ 32
 
 /-- `tag` then `payload` are the bytes of field `f`. -/
-def Spec.FieldBytes (tag payload : List UInt8) (f : Field) : Prop :=
-  Spec.VarintShape 5 tag ∧ Spec.groupsValue tag < 2 ^ 32 ∧
-  f.number = Spec.groupsValue tag / 8 ∧ 1 ≤ f.number ∧
-  match Spec.groupsValue tag % 8, f.value with
-  | 0, .varint v => Spec.IsVarint payload v
-  | 1, .i64 v => payload.length = 8 ∧ v = Spec.leValue payload
+def Protobuf.Spec.FieldBytes (tag payload : List UInt8) (f : Field) : Prop :=
+  Protobuf.Spec.VarintShape 5 tag ∧ Protobuf.Spec.groupsValue tag < 2 ^ 32 ∧
+  f.number = Protobuf.Spec.groupsValue tag / 8 ∧ 1 ≤ f.number ∧
+  match Protobuf.Spec.groupsValue tag % 8, f.value with
+  | 0, .varint v => Protobuf.Spec.IsVarint payload v
+  | 1, .i64 v => payload.length = 8 ∧ v = Protobuf.Spec.leValue payload
   | 2, .len d =>
-    ∃ pre, payload = pre ++ d ∧ Spec.VarintShape 5 pre ∧ Spec.groupsValue pre = d.length ∧
+    ∃ pre, payload = pre ++ d ∧ Protobuf.Spec.VarintShape 5 pre ∧ Protobuf.Spec.groupsValue pre = d.length ∧
       d.length < 2 ^ 31 - 16
-  | 5, .i32 v => payload.length = 4 ∧ v = Spec.leValue payload
+  | 5, .i32 v => payload.length = 4 ∧ v = Protobuf.Spec.leValue payload
   | _, _ => False
 
 /-- `bs` is a message whose fields, in order, are `fs`: the bytes split
     into records, one per field. -/
-inductive Spec.Message : List UInt8 → List Field → Prop where
-  | nil : Spec.Message [] []
+inductive Protobuf.Spec.Message : List UInt8 → List Field → Prop where
+  | nil : Protobuf.Spec.Message [] []
   | cons {tag payload rest : List UInt8} {f : Field} {fs : List Field} :
-      Spec.FieldBytes tag payload f → Spec.Message rest fs →
-      Spec.Message (tag ++ payload ++ rest) (f :: fs)
+      Protobuf.Spec.FieldBytes tag payload f → Protobuf.Spec.Message rest fs →
+      Protobuf.Spec.Message (tag ++ payload ++ rest) (f :: fs)
 
 /-- The bytes an encoder writes for a field: the shortest varint for
     the tag, then the payload, with any varint in its shortest form. -/
-def Spec.fieldBytes (f : Field) : List UInt8 :=
+def Protobuf.Spec.fieldBytes (f : Field) : List UInt8 :=
   match f.value with
-  | .varint v => Spec.varint (f.number * 8 + 0) ++ Spec.varint v
-  | .i64 v => Spec.varint (f.number * 8 + 1) ++ Spec.leBytes 8 v
-  | .len d => Spec.varint (f.number * 8 + 2) ++ Spec.varint d.length ++ d
-  | .i32 v => Spec.varint (f.number * 8 + 5) ++ Spec.leBytes 4 v
+  | .varint v => Protobuf.Spec.varint (f.number * 8 + 0) ++ Protobuf.Spec.varint v
+  | .i64 v => Protobuf.Spec.varint (f.number * 8 + 1) ++ Protobuf.Spec.leBytes 8 v
+  | .len d => Protobuf.Spec.varint (f.number * 8 + 2) ++ Protobuf.Spec.varint d.length ++ d
+  | .i32 v => Protobuf.Spec.varint (f.number * 8 + 5) ++ Protobuf.Spec.leBytes 4 v
 
 /-- The bytes an encoder writes for a message: its fields in order. -/
-def Spec.encode (fs : List Field) : List UInt8 :=
-  (fs.map Spec.fieldBytes).flatten
+def Protobuf.Spec.encode (fs : List Field) : List UInt8 :=
+  (fs.map Protobuf.Spec.fieldBytes).flatten
 
 -- The guide's examples: field 1 set to 150 is `08 96 01`, field 2 set
 -- to "testing" is `12 07 74 65 73 74 69 6e 67`, and field 3 holding the
 -- first message is `1a 03 08 96 01`.
-example : Spec.encode [⟨1, .varint 150⟩] = [0x08, 0x96, 0x01] := by decide
-example : Spec.encode [⟨2, .len [0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67]⟩] =
+example : Protobuf.Spec.encode [⟨1, .varint 150⟩] = [0x08, 0x96, 0x01] := by decide
+example : Protobuf.Spec.encode [⟨2, .len [0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67]⟩] =
     [0x12, 0x07, 0x74, 0x65, 0x73, 0x74, 0x69, 0x6e, 0x67] := by decide
-example : Spec.encode [⟨3, .len [0x08, 0x96, 0x01]⟩] = [0x1a, 0x03, 0x08, 0x96, 0x01] := by decide
-example : Spec.FieldBytes [0x08] [0x96, 0x01] ⟨1, .varint 150⟩ := by
-  refine ⟨by unfold Spec.VarintShape; decide, by decide, by decide, by decide, ?_⟩
-  show Spec.IsVarint [0x96, 0x01] 150
-  exact ⟨by unfold Spec.VarintShape; decide, by decide⟩
+example : Protobuf.Spec.encode [⟨3, .len [0x08, 0x96, 0x01]⟩] = [0x1a, 0x03, 0x08, 0x96, 0x01] := by decide
+example : Protobuf.Spec.FieldBytes [0x08] [0x96, 0x01] ⟨1, .varint 150⟩ := by
+  refine ⟨by unfold Protobuf.Spec.VarintShape; decide, by decide, by decide, by decide, ?_⟩
+  show Protobuf.Spec.IsVarint [0x96, 0x01] 150
+  exact ⟨by unfold Protobuf.Spec.VarintShape; decide, by decide⟩
diff --git a/Protobuf/Types.lean b/Protobuf/Types.lean
index dd42d06..11b4c47 100644
--- a/Protobuf/Types.lean
+++ b/Protobuf/Types.lean
@@ -1,10 +1,10 @@
 /-
   What a message is on the wire: a list of fields, each a field number
   and a raw value of one of four wire types. Part of the approved
-  specification, with `Spec.lean` and `Spec/Defs.lean`, since every
+  specification, with `Protobuf/Spec.lean` and `Spec/Defs.lean`, since every
   statement is about these types.
 
-  Which values are in range is `Spec.ValidField`, in `Spec/Defs.lean`.
+  Which values are in range is `Protobuf.Spec.ValidField`, in `Spec/Defs.lean`.
 -/
 
 namespace Protobuf
diff --git a/README.md b/README.md
index 4c3886f..ef9b648 100644
--- a/README.md
+++ b/README.md
@@ -25,19 +25,19 @@ From Lean:
 
 ## What is proved
 
-The statements are in `Spec.lean`. The definitions they use, written from the encoding guide, are in `Spec/Defs.lean`, and the types are in `Protobuf/Types.lean`. The proofs are in `Proofs/`.
+The statements are in `Protobuf/Spec.lean`. The definitions they use, written from the encoding guide, are in `Protobuf/Spec/Defs.lean`, and the types are in `Protobuf/Types.lean`. The proofs are in `Protobuf/Proofs/`.
 
 | Claim | Theorem |
 |-------|---------|
-| For numbers below 2^64, the encoder writes the shortest varint. | `Spec.varint_encode_eq` |
-| The varint decoder reads exactly one varint of up to ten bytes from the front of its input, leaves the rest untouched, and refuses everything else. That includes input that ends inside the varint, and an eleventh byte. | `Spec.varint_decode_iff` |
-| For numbers below 2^64, decoding a varint the encoder wrote gives the number back. | `Spec.varint_decode_encode` |
-| `isValid` decides exactly which fields can be written: field numbers 1 to 2^29 - 1, values that fit their wire type, and bytes shorter than 2^31 - 16. | `Spec.isValid_iff` |
-| For valid fields, the encoder writes each field as the guide describes: the tag, then the payload, every varint in its shortest form. | `Spec.encode_eq` |
-| `decode` returns a field list exactly when the bytes split into records, one per field, in order, by the rules in `SPEC.md`. So it reads every message made of `VARINT`, `I64`, `LEN` and `I32` records with field numbers from 1 to 2^29 - 1, and returns the fields as written. It refuses everything else: a record cut short, a length past the end, field number 0, a group, an unknown wire type, and an oversized tag or length. | `Spec.decode_iff` |
-| For valid fields, decoding what the encoder wrote gives the fields back. | `Spec.decode_encode` |
-| Every field the decoder returns can be written again. | `Spec.decode_valid` |
-| The guide's worked bytes (1, 150 and -2 as varints, and its messages `Test1` to `Test4`), and the edge and refusal cases listed in `SPEC.md`. | `Spec.guide_vectors`, `Spec.edge_vectors`, `Spec.reject_vectors` |
+| For numbers below 2^64, the encoder writes the shortest varint. | `Protobuf.Spec.varint_encode_eq` |
+| The varint decoder reads exactly one varint of up to ten bytes from the front of its input, leaves the rest untouched, and refuses everything else. That includes input that ends inside the varint, and an eleventh byte. | `Protobuf.Spec.varint_decode_iff` |
+| For numbers below 2^64, decoding a varint the encoder wrote gives the number back. | `Protobuf.Spec.varint_decode_encode` |
+| `isValid` decides exactly which fields can be written: field numbers 1 to 2^29 - 1, values that fit their wire type, and bytes shorter than 2^31 - 16. | `Protobuf.Spec.isValid_iff` |
+| For valid fields, the encoder writes each field as the guide describes: the tag, then the payload, every varint in its shortest form. | `Protobuf.Spec.encode_eq` |
+| `decode` returns a field list exactly when the bytes split into records, one per field, in order, by the rules in `SPEC.md`. So it reads every message made of `VARINT`, `I64`, `LEN` and `I32` records with field numbers from 1 to 2^29 - 1, and returns the fields as written. It refuses everything else: a record cut short, a length past the end, field number 0, a group, an unknown wire type, and an oversized tag or length. | `Protobuf.Spec.decode_iff` |
+| For valid fields, decoding what the encoder wrote gives the fields back. | `Protobuf.Spec.decode_encode` |
+| Every field the decoder returns can be written again. | `Protobuf.Spec.decode_valid` |
+| The guide's worked bytes (1, 150 and -2 as varints, and its messages `Test1` to `Test4`), and the edge and refusal cases listed in `SPEC.md`. | `Protobuf.Spec.guide_vectors`, `Protobuf.Spec.edge_vectors`, `Protobuf.Spec.reject_vectors` |
 
 The command-line tool in `Main.lean` calls these functions directly.
 
@@ -75,17 +75,17 @@ 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.
+`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Protobuf/Proofs/` proves exactly the statement in `Protobuf/Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean.
 
-The test script installs the pinned oracle packages into `.lake/oracle-venv` when they are missing. It then compares the tool with upb and with the C++ parser on inputs from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. `tests/planted_bugs.py` plants ten small bugs in a copy of the code, and `tests/PLANTED-BUGS.md` records that the tests catch nine; the tenth, a missing `LEN` length limit, needs a 2 GiB input to show, so it rests on `Spec.decode_iff`.
+The test script installs the pinned oracle packages into `.lake/oracle-venv` when they are missing. It then compares the tool with upb and with the C++ parser on inputs from a recorded seed, and rewrites `tests/TEST-RESULTS.md`. `tests/planted_bugs.py` plants ten small bugs in a copy of the code, and `tests/PLANTED-BUGS.md` records that the tests catch nine; the tenth, a missing `LEN` length limit, needs a 2 GiB input to show, so it rests on `Protobuf.Spec.decode_iff`.
 
 ## Layout
 
 - `Protobuf/Types.lean`: the field and value types. It is part of the specification.
 - `Protobuf/Varint.lean`, `Protobuf/Wire.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 encoding guide, with checks against its worked bytes.
-- `Proofs.lean` and `Proofs/`: the proofs, under the same names.
+- `Protobuf/Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file.
+- `Protobuf/Spec/Defs.lean`: the definitions the statements use, written from the encoding guide, with checks against its worked bytes.
+- `Protobuf/Proofs.lean` and `Protobuf/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 0ed95f4..4ca8788 100644
--- a/SPEC.md
+++ b/SPEC.md
@@ -1,6 +1,6 @@
 # Specification: protobuf
 
-This library implements the Protobuf wire format: varints, field tags, and messages as lists of raw fields. It is the layer under every `.proto` schema. It reads and writes the bytes without knowing what the fields mean. A reviewer who did not write this specification approves it. The approval also covers `Spec.lean`, `Spec/Defs.lean`, `Protobuf/Types.lean`, and the other files `bar.toml` lists.
+This library implements the Protobuf wire format: varints, field tags, and messages as lists of raw fields. It is the layer under every `.proto` schema. It reads and writes the bytes without knowing what the fields mean. A reviewer who did not write this specification approves it. The approval also covers `Protobuf/Spec.lean`, `Protobuf/Spec/Defs.lean`, `Protobuf/Types.lean`, and the other files `bar.toml` lists.
 
 The source is the Protobuf encoding guide, <https://protobuf.dev/programming-guides/encoding/>. Where the guide leaves a choice, the source is the behaviour of Google's two parsers: upb, which Python's `protobuf` package uses, and the C++ parser behind `protoc --decode_raw`.
 
@@ -66,29 +66,29 @@ The two reference parsers differ in three places, and this library takes the str
 
 ## What must always hold
 
-Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use are in `Spec/Defs.lean`. They are written from the encoding guide and checked against its worked bytes.
+Each property is a theorem in `Protobuf/Spec.lean`, under the name given. The definitions the statements use are in `Protobuf/Spec/Defs.lean`. They are written from the encoding guide and checked against its worked bytes.
 
 | Property | Theorem |
 |----------|---------|
-| For numbers below 2^64, the encoder writes the shortest varint. | `Spec.varint_encode_eq` |
-| The varint decoder reads exactly one varint of up to ten bytes from the front of its input, keeps the rest untouched, and refuses everything else. | `Spec.varint_decode_iff` |
-| For numbers below 2^64, decoding a varint the encoder wrote gives the number back. | `Spec.varint_decode_encode` |
-| `isValid` decides exactly which fields can be written. | `Spec.isValid_iff` |
-| For valid fields, the encoder writes each field as the guide describes. | `Spec.encode_eq` |
-| `decode` returns a field list exactly when the bytes split into records, one per field, in order, by the rules above. | `Spec.decode_iff` |
-| For valid fields, decoding what the encoder wrote gives the fields back. | `Spec.decode_encode` |
-| Every field the decoder returns can be written again. | `Spec.decode_valid` |
-| The guide's worked bytes: 1, 150 and -2 as varints, and its messages `Test1` to `Test4`. | `Spec.guide_vectors` |
-| 2^64 - 1 is ten bytes, fixed-width values are little-endian, varints need not be in shortest form, ten-byte varints drop bits past the 64th, the largest field number reads, and so does the empty message. | `Spec.edge_vectors` |
-| The decoder refuses each kind of malformed input listed above, except a length of 2^31 - 16 or more, which needs a 2 GiB input; `Spec.decode_iff` covers it. | `Spec.reject_vectors` |
+| For numbers below 2^64, the encoder writes the shortest varint. | `Protobuf.Spec.varint_encode_eq` |
+| The varint decoder reads exactly one varint of up to ten bytes from the front of its input, keeps the rest untouched, and refuses everything else. | `Protobuf.Spec.varint_decode_iff` |
+| For numbers below 2^64, decoding a varint the encoder wrote gives the number back. | `Protobuf.Spec.varint_decode_encode` |
+| `isValid` decides exactly which fields can be written. | `Protobuf.Spec.isValid_iff` |
+| For valid fields, the encoder writes each field as the guide describes. | `Protobuf.Spec.encode_eq` |
+| `decode` returns a field list exactly when the bytes split into records, one per field, in order, by the rules above. | `Protobuf.Spec.decode_iff` |
+| For valid fields, decoding what the encoder wrote gives the fields back. | `Protobuf.Spec.decode_encode` |
+| Every field the decoder returns can be written again. | `Protobuf.Spec.decode_valid` |
+| The guide's worked bytes: 1, 150 and -2 as varints, and its messages `Test1` to `Test4`. | `Protobuf.Spec.guide_vectors` |
+| 2^64 - 1 is ten bytes, fixed-width values are little-endian, varints need not be in shortest form, ten-byte varints drop bits past the 64th, the largest field number reads, and so does the empty message. | `Protobuf.Spec.edge_vectors` |
+| The decoder refuses each kind of malformed input listed above, except a length of 2^31 - 16 or more, which needs a 2 GiB input; `Protobuf.Spec.decode_iff` covers it. | `Protobuf.Spec.reject_vectors` |
 
 Together, these fix every output.
 
 - `decode` is fixed for every input.
 - `encode` and `Varint.encode` are fixed for every valid input.
-- A decoder that accepted nothing would meet `Spec.decode_valid`, but it would fail `Spec.decode_iff` and `Spec.decode_encode`.
+- A decoder that accepted nothing would meet `Protobuf.Spec.decode_valid`, but it would fail `Protobuf.Spec.decode_iff` and `Protobuf.Spec.decode_encode`.
 - `encode` is not fixed for fields that are not valid.
-- A decoder that accepted too much would fail `Spec.decode_iff`.
+- A decoder that accepted too much would fail `Protobuf.Spec.decode_iff`.
 
 ## Oracle
 
diff --git a/bar.toml b/bar.toml
index 44efda4..45d1916 100644
--- a/bar.toml
+++ b/bar.toml
@@ -18,7 +18,7 @@ entry_points = ["Main.lean"]
 [spec]
 # Protobuf/Types.lean holds the types every statement is about, so it
 # is part of the specification.
-files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean", "Protobuf/Types.lean"]
+files = ["SPEC.md", "Protobuf/Spec.lean", "Protobuf/Spec/Defs.lean", "Protobuf/Types.lean"]
 # The code under proof: the functions the statements are about.
 code = [
   "Protobuf.Varint.encode", "Protobuf.Varint.decode",
diff --git a/comparator.json b/comparator.json
index da878b7..13c7a7f 100644
--- a/comparator.json
+++ b/comparator.json
@@ -1,10 +1,22 @@
 {
-  "challenge_module": "Spec",
-  "solution_module": "Proofs",
+  "challenge_module": "Protobuf.Spec",
+  "solution_module": "Protobuf.Proofs",
   "theorem_names": [
-    "Spec.varint_encode_eq", "Spec.varint_decode_iff", "Spec.varint_decode_encode",
-    "Spec.isValid_iff", "Spec.encode_eq", "Spec.decode_iff", "Spec.decode_encode",
-    "Spec.decode_valid", "Spec.guide_vectors", "Spec.edge_vectors", "Spec.reject_vectors"
+    "Protobuf.Spec.varint_encode_eq",
+    "Protobuf.Spec.varint_decode_iff",
+    "Protobuf.Spec.varint_decode_encode",
+    "Protobuf.Spec.isValid_iff",
+    "Protobuf.Spec.encode_eq",
+    "Protobuf.Spec.decode_iff",
+    "Protobuf.Spec.decode_encode",
+    "Protobuf.Spec.decode_valid",
+    "Protobuf.Spec.guide_vectors",
+    "Protobuf.Spec.edge_vectors",
+    "Protobuf.Spec.reject_vectors"
   ],
-  "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"]
+  "permitted_axioms": [
+    "propext",
+    "Quot.sound",
+    "Classical.choice"
+  ]
 }
diff --git a/lakefile.toml b/lakefile.toml
index 4f53683..10e1e60 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -1,16 +1,18 @@
 name = "protobuf"
 version = "0.1.0"
 license = "Apache-2.0"
-defaultTargets = ["Protobuf", "Spec", "Proofs", "protowire"]
+defaultTargets = ["Protobuf", "ProtobufSpec", "ProtobufProofs", "protowire"]
 
 [[lean_lib]]
 name = "Protobuf"
 
 [[lean_lib]]
-name = "Spec"
+name = "ProtobufSpec"
+roots = ["Protobuf.Spec"]
 
 [[lean_lib]]
-name = "Proofs"
+name = "ProtobufProofs"
+roots = ["Protobuf.Proofs"]
 
 [[lean_exe]]
 name = "protowire"
diff --git a/tests/PLANTED-BUGS.md b/tests/PLANTED-BUGS.md
index 3cdb2e0..c003f53 100644
--- a/tests/PLANTED-BUGS.md
+++ b/tests/PLANTED-BUGS.md
@@ -12,7 +12,7 @@ against the changed tool. A bug is caught when they report failures.
 | Six-byte tags read | `Protobuf/Wire.lean` | 133 |
 | Eleven-byte varints read | `Protobuf/Varint.lean` | 70 |
 | Bits past the 64th kept | `Protobuf/Varint.lean` | 23 |
-| No LEN length limit | `Protobuf/Wire.lean` | 0, not caught by the tests: it shows only when a length of 2^31 - 16 or more is followed by that many bytes, an input of about 2 GiB; a shorter input with such a length is refused for running out of input either way. `Spec.decode_iff` covers the limit. |
+| No LEN length limit | `Protobuf/Wire.lean` | 0, not caught by the tests: it shows only when a length of 2^31 - 16 or more is followed by that many bytes, an input of about 2 GiB; a shorter input with such a length is refused for running out of input either way. `Protobuf.Spec.decode_iff` covers the limit. |
 | A group start tag read as an empty LEN field | `Protobuf/Wire.lean` | 150 |
 | isValid takes field number 2^29 | `Protobuf/Wire.lean` | 90 |
 | CR kept at the end of a CR LF request | `Main.lean` | 2856 |
diff --git a/tests/planted_bugs.py b/tests/planted_bugs.py
index 00431ee..6b74a60 100644
--- a/tests/planted_bugs.py
+++ b/tests/planted_bugs.py
@@ -57,7 +57,7 @@
      "if (rest.take len).length < len then none",
      "it shows only when a length of 2^31 - 16 or more is followed by that many bytes, "
      "an input of about 2 GiB; a shorter input with such a length is refused for running "
-     "out of input either way. `Spec.decode_iff` covers the limit."),
+     "out of input either way. `Protobuf.Spec.decode_iff` covers the limit."),
     ("A group start tag read as an empty LEN field", "Protobuf/Wire.lean",
      "      | _ => none",
      "      | 3 => some (⟨n, .len []⟩, rest)\n      | _ => none", None),

From c61f11f76a03811c6d33b3d1ace0687a724b1783 Mon Sep 17 00:00:00 2001
From: orda-aska <orda-aska@users.noreply.github.com>
Date: Thu, 29 Oct 2026 20:03:59 +0000
Subject: [PATCH 2/2] Point the remaining Spec/Defs.lean references at
 Protobuf/Spec/Defs.lean

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01QwrvNdsMA6RtgKxXn1Pmhf
---
 Protobuf/Spec.lean  | 2 +-
 Protobuf/Types.lean | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Protobuf/Spec.lean b/Protobuf/Spec.lean
index 00a6701..42a6030 100644
--- a/Protobuf/Spec.lean
+++ b/Protobuf/Spec.lean
@@ -8,7 +8,7 @@
   file only.
 
   The definitions the statements use, written from the Protobuf encoding
-  guide, are in `Spec/Defs.lean`, and the types in `Protobuf/Types.lean`.
+  guide, are in `Protobuf/Spec/Defs.lean`, and the types in `Protobuf/Types.lean`.
   Both are part of the specification too.
 -/
 
diff --git a/Protobuf/Types.lean b/Protobuf/Types.lean
index 11b4c47..b603cc0 100644
--- a/Protobuf/Types.lean
+++ b/Protobuf/Types.lean
@@ -1,10 +1,10 @@
 /-
   What a message is on the wire: a list of fields, each a field number
   and a raw value of one of four wire types. Part of the approved
-  specification, with `Protobuf/Spec.lean` and `Spec/Defs.lean`, since every
+  specification, with `Protobuf/Spec.lean` and `Protobuf/Spec/Defs.lean`, since every
   statement is about these types.
 
-  Which values are in range is `Protobuf.Spec.ValidField`, in `Spec/Defs.lean`.
+  Which values are in range is `Protobuf.Spec.ValidField`, in `Protobuf/Spec/Defs.lean`.
 -/
 
 namespace Protobuf