Move proof modules under Codec

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

Proofs/Base32.lean → 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

Proofs/Base64.lean → 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

Proofs/Crc32.lean → 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