From f149621971b3b32d8ae077810fdccdb6734ca41c Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 25 Oct 2026 23:01:31 +0000 Subject: [PATCH 1/5] Add PEM (RFC 7468, strict form), proved and tested Codec.Pem.encode writes the strict form of RFC 7468 (Figure 3): the BEGIN line, the base 64 of the data in lines of 64 characters, the END line with the same label, each line ending in LF. It refuses a label the `label` rule does not allow. Codec.Pem.decode reads exactly one message in that form, with each line ending in LF, CR or CR LF, and refuses anything else: a different END label, blanks, headers, text around the message, other line lengths, and base 64 that is not exactly the encoding of the data. The spec writes the label rule, `eol`, the lines of a message and the strict form from the RFC's ABNF, and settles two points it leaves open: empty data is the two boundary lines alone, as Go and Python write it, and the base 64 is exactly codec's. Four statements, all proved: Spec.pem_encode_iff, Spec.pem_decode_iff, Spec.pem_decode_encode, and Spec.pem_vectors, which includes RFC 7468's Figure 15 written exactly as the RFC prints it. lake comparator --paranoid accepts all 26 theorems. The differential tests run 1,000,000 inputs, 135,034 of them PEM, with 0 failures, against ssl.DER_cert_to_PEM_cert and an encoder and strict parser written from the ABNF; eight planted bugs each make them fail. A one-off check against Go's encoding/pem finds no difference beyond Go's lax reading, its writing of any label, and its not taking a CR alone as a line end. Plan and claim: #5. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Codec.lean | 1 + Codec/Pem.lean | 105 +++++++++++++++++ Main.lean | 29 +++++ Proofs.lean | 1 + Proofs/Pem.lean | 239 +++++++++++++++++++++++++++++++++++++++ Proofs/Pem/Lines.lean | 133 ++++++++++++++++++++++ Proofs/Pem/Parts.lean | 171 ++++++++++++++++++++++++++++ README.md | 18 ++- SPEC.md | 23 +++- Spec.lean | 56 +++++++++ Spec/Defs.lean | 106 +++++++++++++++++ bar.toml | 1 + comparator.json | 6 +- tests/CROSS-CHECK.md | 13 ++- tests/TEST-RESULTS.md | 10 +- tests/cross_check.py | 78 ++++++++++++- tests/cross_check/pem.go | 92 +++++++++++++++ tests/run_tests.py | 119 ++++++++++++++++++- 18 files changed, 1180 insertions(+), 21 deletions(-) create mode 100644 Codec/Pem.lean create mode 100644 Proofs/Pem.lean create mode 100644 Proofs/Pem/Lines.lean create mode 100644 Proofs/Pem/Parts.lean create mode 100644 tests/cross_check/pem.go diff --git a/Codec.lean b/Codec.lean index 2aa7de4..e3f1353 100644 --- a/Codec.lean +++ b/Codec.lean @@ -2,3 +2,4 @@ import Codec.Hex import Codec.Base64 import Codec.Crc32 import Codec.Percent +import Codec.Pem diff --git a/Codec/Pem.lean b/Codec/Pem.lean new file mode 100644 index 0000000..6651ba4 --- /dev/null +++ b/Codec/Pem.lean @@ -0,0 +1,105 @@ +/- + PEM, the textual encoding of RFC 7468, in its strict form (Figure 3): + + -----BEGIN label----- + the base 64 of the data, in lines of 64 characters, the last shorter + -----END label----- + + `encode` writes each line ending in LF, and fails on a label that the + `label` rule of section 3 does not allow. `decode` reads exactly one + message in this form, with each line ending in LF, CR, or CR LF. It + fails on anything else: a different label on the END line, blanks, + headers, text before or after the message, a short line before the + last, and base 64 that `Base64.decode` refuses. Empty data has no line + of base 64. +-/ + +import Codec.Base64 + +namespace Codec.Pem + +/-- `labelchar`: a printable US-ASCII character other than `-`. -/ +def isLabelChar (c : Char) : Bool := + let n := c.toNat + (0x21 ≤ n && n ≤ 0x2C) || (0x2E ≤ n && n ≤ 0x7E) + +/-- After the first character of a label: label characters, each of + which may follow one `-` or space. -/ +def labelRest : List Char → Bool + | [] => true + | c :: rest => + if isLabelChar c then labelRest rest + else if c = '-' ∨ c = ' ' then + match rest with + | d :: rest' => isLabelChar d && labelRest rest' + | [] => false + else false + +/-- A label: empty, or a label character and then `labelRest`. -/ +def validLabel : List Char → Bool + | [] => true + | c :: rest => isLabelChar c && labelRest rest + +/-- Cut text into lines of 64 characters, the last one shorter. `fuel` + equal to the text's length is enough. -/ +def lines64 : Nat → List Char → List (List Char) + | _, [] => [] + | 0, _ :: _ => [] + | fuel + 1, cs => cs.take 64 :: lines64 fuel (cs.drop 64) + +def beginLine (label : List Char) : List Char := "-----BEGIN ".toList ++ label ++ "-----".toList + +def endLine (label : List Char) : List Char := "-----END ".toList ++ label ++ "-----".toList + +/-- The lines of a message: BEGIN, the base 64, END. -/ +def lines (label : List Char) (data : List UInt8) : List (List Char) := + let b64 := Base64.encode data + beginLine label :: lines64 b64.length b64 ++ [endLine label] + +/-- Encode data under a label, each line ending in LF. -/ +def encode (label : List Char) (data : List UInt8) : Option (List Char) := + if validLabel label then some ((lines label data).flatMap (· ++ ['\n'])) else none + +/-- The first line of `text` and the text after its line end (LF, CR, + or CR LF), or `none` when no line end follows. -/ +def takeLine : List Char → Option (List Char × List Char) + | [] => none + | '\r' :: '\n' :: rest => some ([], rest) + | '\r' :: rest => some ([], rest) + | '\n' :: rest => some ([], rest) + | c :: rest => (takeLine rest).map fun (l, r) => (c :: l, r) + +/-- Split text into lines, each of which must end in a line end. `fuel` + equal to the text's length is enough. -/ +def splitLines : Nat → List Char → Option (List (List Char)) + | _, [] => some [] + | 0, _ :: _ => none + | fuel + 1, text => do + let (l, rest) ← takeLine text + let ls ← splitLines fuel rest + pure (l :: ls) + +/-- The label of a BEGIN line, or of an END line. -/ +def labelOf (pre : List Char) (line : List Char) : Option (List Char) := + if pre.isPrefixOf line ∧ "-----".toList.isSuffixOf line ∧ pre.length + 5 ≤ line.length then + some ((line.drop pre.length).take (line.length - pre.length - 5)) + else none + +/-- Decode one message in the strict form: its label and its data. -/ +def decode (text : List Char) : Option (List Char × List UInt8) := do + let ls ← splitLines text.length text + match ls with + | first :: rest => + match rest.getLast? with + | some last => + let body := rest.dropLast + let label ← labelOf "-----BEGIN ".toList first + let label' ← labelOf "-----END ".toList last + let data ← Base64.decode body.flatten + if label = label' ∧ validLabel label ∧ body = lines64 body.flatten.length body.flatten then + some (label, data) + else none + | none => none + | [] => none + +end Codec.Pem diff --git a/Main.lean b/Main.lean index f47c182..8e9d59c 100644 --- a/Main.lean +++ b/Main.lean @@ -14,6 +14,15 @@ unframe 1,2,3,4,5 prints ok:... (or none) pctenc 32,65 prints %20A pctdec 37,50,48,65 prints ok:32,65 (or none) + pemenc 88;0 prints ok: and the character codes of the PEM + text for label "X" and the byte 0 + (or none, for a label the rule refuses) + pemdec 45,45,... prints ok:88;0, the label's character codes and + the data (or none) + + `pemenc` takes two lists, the label's character codes and the bytes, + separated by `;`. PEM text holds line ends, so it goes in and out as + character codes. A request is an operation, then optionally one space and its numbers; with no numbers after the space, the input is empty. A malformed @@ -51,6 +60,20 @@ def toChars (ns : List Nat) : Option (List Char) := def showBytes (bs : List UInt8) : String := ",".intercalate (bs.map fun b => toString b.toNat) +def showChars (cs : List Char) : String := + ",".intercalate (cs.map fun c => toString c.toNat) + +/-- `pemenc`: the label's character codes, `;`, and the bytes. -/ +def pemEncode (arg : String) : Option String := + match arg.splitOn ";" with + | [l, d] => do + let label ← toChars (← numbers l) + let data ← toBytes (← numbers d) + return match Pem.encode label data with + | some text => "ok:" ++ showChars text + | none => "none" + | _ => none + /-- The answer to one request, or `none` when the request is malformed. -/ def answer (op : String) (ns : List Nat) : Option String := do let result : Option (List UInt8) → String @@ -66,12 +89,18 @@ def answer (op : String) (ns : List Nat) : Option String := do | "unframe" => return result (Crc32.unframe (← toBytes ns)) | "pctenc" => return String.ofList (Percent.encode (← toBytes ns)) | "pctdec" => return result (Percent.decode (← toChars ns)) + | "pemdec" => + return match Pem.decode (← toChars ns) with + | some (label, data) => "ok:" ++ showChars label ++ ";" ++ showBytes data + | none => "none" | _ => none /-- The answer to one line: an operation, then optionally one space and its numbers. -/ def request (line : String) : Option String := match line.splitOn " " with + | ["pemenc", arg] => pemEncode arg + | ["pemenc"] => none | [op] => answer op [] | [op, arg] => numbers arg >>= answer op | _ => none diff --git a/Proofs.lean b/Proofs.lean index 694b150..6287cbd 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -6,3 +6,4 @@ import Proofs.Hex import Proofs.Base64 import Proofs.Crc32 import Proofs.Percent +import Proofs.Pem diff --git a/Proofs/Pem.lean b/Proofs/Pem.lean new file mode 100644 index 0000000..d093536 --- /dev/null +++ b/Proofs/Pem.lean @@ -0,0 +1,239 @@ +/- + 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 + checked by evaluation in the kernel. +-/ + +import Codec +import Spec.Defs +import Proofs.Base64 +import Proofs.Pem.Lines +import 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] + +theorem pm_mem_lines64 {s l : List Char} {c : Char} (hl : l ∈ Spec.lines64 s) (hc : c ∈ l) : + c ∈ s := by + unfold Spec.lines64 at hl + obtain ⟨i, -, rfl⟩ := List.mem_map.mp hl + exact List.mem_of_mem_drop (List.mem_of_mem_take hc) + +theorem pm_char_ok (n : Nat) : Base64.char n ≠ '\r' ∧ Base64.char n ≠ '\n' := by + unfold Base64.char + rw [List.getD_eq_getElem?_getD] + cases h : Base64.alphabet[n]? with + | none => decide + | some x => + have hx : x ∈ Base64.alphabet := List.mem_of_getElem? h + have hall : ∀ y ∈ Base64.alphabet, y ≠ '\r' ∧ y ≠ '\n' := by decide + exact hall x hx + +theorem pm_encode_ok (bs : List UInt8) : ∀ c ∈ Base64.encode bs, c ≠ '\r' ∧ c ≠ '\n' := by + induction bs using Base64.encode.induct with + | case1 a b c rest ih => + rw [Base64.encode.eq_1] + intro x hx + simp only [List.mem_cons] at hx + rcases hx with rfl | rfl | rfl | rfl | hx + all_goals first | exact pm_char_ok _ | exact ih x hx + | case2 a b => + rw [Base64.encode.eq_2] + intro x hx + simp only [List.mem_cons, List.not_mem_nil, or_false] at hx + rcases hx with rfl | rfl | rfl | rfl + all_goals first | exact pm_char_ok _ | decide + | case3 a => + rw [Base64.encode.eq_3] + intro x hx + simp only [List.mem_cons, List.not_mem_nil, or_false] at hx + rcases hx with rfl | rfl | rfl | rfl + all_goals first | exact pm_char_ok _ | decide + | case4 => + rw [Base64.encode.eq_4] + 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 + constructor <;> rintro rfl <;> revert h <;> decide + +theorem pm_labelTail_ok {l : List Char} (h : Spec.LabelTail l) : + ∀ c ∈ l, c ≠ '\r' ∧ c ≠ '\n' := by + induction h with + | nil => intro x hx; cases hx + | char hc _ ih => + intro x hx + cases hx with + | head => exact pm_labelChar_ok hc + | tail _ hx => exact ih x hx + | sep hs hc _ ih => + intro x hx + cases hx with + | head => rcases hs with rfl | rfl <;> decide + | tail _ hx => + cases hx with + | 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 + rcases h with rfl | ⟨c, rest, rfl, hc, ht⟩ + · intro x hx; cases hx + · intro x hx + cases hx with + | 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 + intro l hl' c hc + simp only [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 + · revert c; decide + · exact pm_label_ok hl c hc + · revert c; decide + · exact pm_encode_ok data c (pm_mem_lines64 hl' hc) + · simp only [List.mem_append] at hc + rcases hc with (hc | hc) | hc + · revert c; decide + · exact pm_label_ok hl c hc + · revert c; decide + intro l hl' + 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 + intro l hl' + simp only [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 + induction ls with + | nil => exact 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)) + (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 + +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 + unfold Pem.encode + rw [← validLabel_iff, pm_text_eq] + constructor + · intro h + split at h + · rename_i hv + cases h + exact ⟨hv, rfl⟩ + · cases h + · 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 + constructor + · intro h + cases hs : Pem.splitLines text.length text with + | none => + unfold Pem.decode at h + rw [hs] at h + cases h + | some ls => + have hle := splitLines_sound _ _ _ hs + unfold Pem.decode at h + rw [hs] at h + simp only [Option.bind_eq_bind, Option.bind_some] at h + match ls, h with + | first :: rest, h => + simp only at h + cases hlast : rest.getLast? with + | none => rw [hlast] at h; cases h + | some last => + rw [hlast] at h + simp only at h + obtain ⟨body, rfl⟩ := List.getLast?_eq_some_iff.mp hlast + simp only [List.dropLast_concat] at h + cases hb : Pem.labelOf "-----BEGIN ".toList first with + | none => rw [hb] at h; cases h + | some lb => + cases he : Pem.labelOf "-----END ".toList last with + | none => rw [hb, he] at h; cases h + | some le => + cases hd : Base64.decode body.flatten with + | none => rw [hb, he, hd] at h; cases h + | some d => + rw [hb, he, hd] at h + simp only [Option.bind_some] at h + split at h + · rename_i hc + 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 + rw [lines64_eq, ← hflat] at hbody + rw [labelOf_some _ _ _ hb, labelOf_some _ _ _ he, hbody] at hle + exact ⟨(validLabel_iff _).mp hv, hle⟩ + · cases h + · rintro ⟨hl, hle⟩ + have hs := splitLines_complete text.length text _ (Nat.le_refl _) hle + (pm_pemLines_ne_nil label data) + 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, + List.dropLast_concat, labelOf_append, Option.bind_some, flatten_lines64, + 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) : + 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)⟩ + +theorem Spec.pem_vectors : + Pem.encode "PUBLIC KEY".toList 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) ∧ + 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]) ∧ + Pem.encode "RSA PRIVATE KEY".toList [0] = + some "-----BEGIN RSA PRIVATE KEY-----\nAA==\n-----END RSA PRIVATE KEY-----\n".toList ∧ + Pem.encode "A--B".toList [] = none ∧ + Pem.encode "A B".toList [] = none ∧ + Pem.encode " A".toList [] = none ∧ + Pem.encode "A-".toList [] = none ∧ + Pem.encode "\u00c9".toList [] = none ∧ + Pem.decode "-----BEGIN X-----\nAA==\n-----END Y-----\n".toList = none ∧ + Pem.decode "-----BEGIN X-----\nAA==\n-----END X-----".toList = none ∧ + Pem.decode "-----BEGIN X-----\nAA== \n-----END X-----\n".toList = none ∧ + Pem.decode "-----BEGIN X----- \nAA==\n-----END X-----\n".toList = none ∧ + Pem.decode "-----BEGIN X-----\n\nAA==\n-----END X-----\n".toList = none ∧ + Pem.decode "-----BEGIN X-----\nProc-Type: 4,ENCRYPTED\nAA==\n-----END X-----\n".toList = none ∧ + Pem.decode "text\n-----BEGIN X-----\nAA==\n-----END X-----\n".toList = none ∧ + Pem.decode "-----BEGIN X-----\nAA==\n-----END X-----\n\n".toList = none ∧ + Pem.decode "-----BEGIN X-----\nAB==\n-----END X-----\n".toList = none ∧ + Pem.decode ("-----BEGIN X-----\nAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA\nAAAAAAAA\n".toList ++ + "-----END X-----\n".toList) = none := by + and_intros <;> decide +kernel diff --git a/Proofs/Pem/Lines.lean b/Proofs/Pem/Lines.lean new file mode 100644 index 0000000..1c6d47d --- /dev/null +++ b/Proofs/Pem/Lines.lean @@ -0,0 +1,133 @@ +/- + Splitting text into lines: `Pem.splitLines` against `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 + the only reading with no empty line, and no line of a PEM message is + empty. +-/ + +import Codec +import 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 + induction text using Pem.takeLine.induct generalizing l rest with + | case1 => simp [Pem.takeLine] at h + | case2 t => + rw [Pem.takeLine.eq_2] at h + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + exact ⟨['\r', '\n'], Or.inl rfl, by simp, by simp, by simp, by simp only [List.length_cons]; omega⟩ + | case3 t ht => + rw [Pem.takeLine.eq_3 _ ht] at h + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + exact ⟨['\r'], Or.inr (Or.inl rfl), by simp, by simp, by simp, by simp only [List.length_cons]; omega⟩ + | case4 t => + rw [Pem.takeLine.eq_4] at h + simp only [Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + exact ⟨['\n'], Or.inr (Or.inr rfl), by simp, by simp, by simp, by simp only [List.length_cons]; omega⟩ + | case5 c t h1 h2 h3 ih => + rw [Pem.takeLine.eq_5 _ _ h1 h2 h3] at h + cases ht : Pem.takeLine t with + | none => simp [ht] at h + | some p => + obtain ⟨l', r'⟩ := p + simp only [ht, Option.map_some, Option.some.injEq, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + obtain ⟨e, he, rfl, h4, h5, h6⟩ := ih l' r' ht + refine ⟨e, he, by simp, ?_, ?_, ?_⟩ + · simp only [List.mem_cons, not_or]; exact ⟨fun h => h2 h.symm, h4⟩ + · simp only [List.mem_cons, not_or]; exact ⟨fun h => h3 h.symm, h5⟩ + · 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 + induction fuel generalizing text ls with + | zero => + cases text with + | nil => simp [Pem.splitLines] at h; subst h; exact 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 + | cons c t => + rw [Pem.splitLines.eq_3 _ _ (by simp)] at h + cases ht : Pem.takeLine (c :: t) with + | none => simp [ht] at h + | some p => + obtain ⟨l, r⟩ := p + cases hs : Pem.splitLines f r with + | none => simp [ht, hs] at h + | some ls' => + simp only [ht, hs, Option.bind_eq_bind, Option.bind_some, Option.pure_def, + Option.some.injEq] at h + 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) + +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') : + Pem.takeLine (l ++ e ++ rest) = some (l, rest) := by + induction l with + | nil => + rcases he with rfl | rfl | rfl + · exact Pem.takeLine.eq_2 rest + · apply Pem.takeLine.eq_3 + intro r hr + subst hr + exact hcr rfl rfl + · exact Pem.takeLine.eq_4 rest + | cons c l' ih => + simp only [List.mem_cons, not_or] at h1 h2 + have hc1 : c ≠ '\r' := fun h => h1.1 h.symm + have hc2 : c ≠ '\n' := fun h => h2.1 h.symm + show Pem.takeLine (c :: (l' ++ e ++ rest)) = _ + 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) + (hne : ∀ l ∈ ls, l ≠ []) : rest.head? ≠ some '\n' := by + cases h with + | nil => simp + | @cons l e r ls' h1 h2 he _ => + have hl : l ≠ [] := hne l (by simp) + cases l with + | nil => exact absurd rfl hl + | cons c l' => + simp only [List.cons_append, List.head?_cons, ne_eq, Option.some.injEq] + intro hc + subst hc + 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 ≠ []) : + Pem.splitLines fuel text = some ls := by + induction h generalizing fuel with + | nil => cases fuel <;> simp [Pem.splitLines] + | @cons l e rest ls h1 h2 he hrest ih => + have helen : e.length ≥ 1 := by rcases he with rfl | rfl | rfl <;> simp + simp only [List.length_append] at hfuel + obtain ⟨f, rfl⟩ : ∃ f, fuel = f + 1 := ⟨fuel - 1, by omega⟩ + have hne' : ∀ l ∈ ls, l ≠ [] := fun l' hl' => hne l' (List.mem_cons_of_mem _ hl') + have htext : l ++ e ++ rest ≠ [] := by + intro h0 + have := congrArg List.length h0 + simp only [List.length_append, List.length_nil] at this + omega + rw [Pem.splitLines.eq_3 _ _ htext] + have ht : Pem.takeLine (l ++ e ++ rest) = some (l, rest) := + ln_takeLine_complete l e rest h1 h2 he (fun _ => ln_linesEol_head rest ls hrest hne') + rw [ht] + simp only [Option.bind_eq_bind, Option.bind_some] + rw [ih f (by omega) hne'] + rfl + +end Codec.Proofs.Pem diff --git a/Proofs/Pem/Parts.lean b/Proofs/Pem/Parts.lean new file mode 100644 index 0000000..a6e7712 --- /dev/null +++ b/Proofs/Pem/Parts.lean @@ -0,0 +1,171 @@ +/- + The parts of a PEM message: labels, lines of 64 characters, and the + BEGIN and END lines, in the code against the spec. +-/ + +import Codec +import 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] + +private theorem pt_labelRest_cons (c : Char) (rest : List Char) : + Pem.labelRest (c :: rest) = + if Pem.isLabelChar c = true then Pem.labelRest rest + else if c = '-' ∨ c = ' ' then + (match rest with + | d :: rest' => Pem.isLabelChar d && Pem.labelRest rest' + | [] => false) + 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] + | 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 + cases h with + | char _ h => exact h + | sep hs _ _ => + rcases hs with hs | hs <;> subst hs <;> simp [Pem.isLabelChar] at hc + · rw [ite_eq_right hc] + by_cases hs : c = '-' ∨ c = ' ' + · rw [ite_eq_left hs] + cases rest with + | nil => + simp only [Bool.false_eq_true, false_iff] + intro h + cases h with + | char h _ => exact hc ((pt_isLabelChar_iff c).2 h) + | cons d rest' => + have ih' := pt_labelRest_iff rest' + simp only [Bool.and_eq_true] + rw [ih', pt_isLabelChar_iff] + constructor + · rintro ⟨h1, h2⟩; exact Spec.LabelTail.sep hs h1 h2 + · intro h + cases h with + | char h _ => exact absurd ((pt_isLabelChar_iff c).2 h) hc + | sep _ h1 h2 => exact ⟨h1, h2⟩ + · rw [ite_eq_right hs] + simp only [Bool.false_eq_true, false_iff] + intro h + cases h with + | 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 + cases l with + | nil => simp [Pem.validLabel, Spec.Label] + | cons c rest => + simp only [Pem.validLabel, Bool.and_eq_true, pt_isLabelChar_iff, pt_labelRest_iff, 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_cons (s : List Char) (h : s ≠ []) : + Spec.lines64 s = s.take 64 :: 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 + rw [hk, List.range_succ_eq_map] + simp only [List.map_cons, List.map_map, Nat.mul_zero, List.drop_zero] + congr 1 + apply List.map_congr_left + intro i _ + simp only [Function.comp, List.drop_drop, Nat.succ_eq_add_one] + congr 2 + omega + +theorem pt_lines64_fuel : ∀ (fuel : Nat) (s : List Char), s.length ≤ fuel → + Pem.lines64 fuel s = Spec.lines64 s + | _, [], _ => by simp [Pem.lines64, pt_spec_lines64_nil] + | 0, _ :: _, h => by simp at h + | fuel + 1, c :: cs, h => by + rw [Pem.lines64, pt_spec_lines64_cons _ (List.cons_ne_nil c cs)] + · 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 := + 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 ≠ [] + | _, [], _ => by simp [pt_spec_lines64_nil] + | 0, _ :: _, h => by simp at h + | fuel + 1, c :: cs, h => by + rw [pt_spec_lines64_cons _ (List.cons_ne_nil c cs)] + have ih := pt_lines64_fuel_props fuel ((c :: cs).drop 64) (by simp at h ⊢; omega) + refine ⟨?_, ?_⟩ + · rw [List.flatten_cons, ih.1, List.take_append_drop] + · intro l hl + rcases List.mem_cons.1 hl with hl | hl + · subst hl; simp + · exact ih.2 l hl + +theorem flatten_lines64 (s : List Char) : (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 ≠ [] := + (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 + dsimp only + rw [lines64_eq] + rfl + +theorem labelOf_append (pre l : List Char) : + Pem.labelOf pre (pre ++ l ++ "-----".toList) = some l := by + unfold Pem.labelOf + have h1 : pre.isPrefixOf (pre ++ l ++ "-----".toList) = true := by + rw [List.isPrefixOf_iff_prefix, List.append_assoc]; exact List.prefix_append _ _ + have h2 : "-----".toList.isSuffixOf (pre ++ l ++ "-----".toList) = true := by + rw [List.isSuffixOf_iff_suffix]; exact List.suffix_append _ _ + have h5 : "-----".toList.length = 5 := rfl + have h3 : pre.length + 5 ≤ (pre ++ l ++ "-----".toList).length := by + simp only [List.length_append, h5]; omega + rw [ite_eq_left ⟨h1, h2, h3⟩] + congr 1 + rw [List.append_assoc, List.drop_left] + have : (pre ++ (l ++ "-----".toList)).length - pre.length - 5 = l.length := by + simp only [List.length_append, h5]; omega + rw [this, List.take_left] + +theorem labelOf_some (pre line l : List Char) (h : Pem.labelOf pre line = some l) : + line = pre ++ l ++ "-----".toList := by + unfold Pem.labelOf at h + split at h + · rename_i hc + obtain ⟨h1, h2, h3⟩ := hc + cases h + rw [List.isPrefixOf_iff_prefix, List.prefix_iff_eq_take] at h1 + rw [List.isSuffixOf_iff_suffix, List.suffix_iff_eq_drop] at h2 + have h5 : "-----".toList.length = 5 := rfl + rw [h5] at h2 + have e1 := List.take_append_drop pre.length line + have e2 := List.take_append_drop (line.length - pre.length - 5) (line.drop pre.length) + rw [List.drop_drop] at e2 + have : pre.length + (line.length - pre.length - 5) = line.length - 5 := by omega + rw [this, ← h2] at e2 + rw [List.append_assoc, e2] + exact e1.symm.trans (by rw [← h1]) + · cases h + +end Codec.Proofs.Pem diff --git a/README.md b/README.md index 2192bc6..012bbc6 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,12 @@ -# codec: hex, base 64, CRC-32 and percent-encoding, proved +# codec: hex, base 64, CRC-32, percent-encoding and PEM, proved -Four small codecs in Lean, each with machine-checked proofs that it does exactly what its specification says, and tested against Python's standard library on a million inputs in all (see `tests/TEST-RESULTS.md`). Hex is written as Python's `bytes.hex()` writes it, base 64 follows RFC 4648, the CRC-32 is the one in gzip, zip, and PNG, and percent-encoding follows RFC 3986. They are also the material for Level 0 of the [Proven Commons academy](https://github.com/Proven-Commons/mission): a first proof, read and then written, on code small enough to hold in your head. +Five small codecs in Lean, each with machine-checked proofs that it does exactly what its specification says, and tested against Python's standard library on a million inputs in all (see `tests/TEST-RESULTS.md`). Hex is written as Python's `bytes.hex()` writes it, base 64 follows RFC 4648, the CRC-32 is the one in gzip, zip, and PNG, percent-encoding follows RFC 3986, and PEM is the strict form of RFC 7468, the text that wraps certificates and keys. They are also the material for Level 0 of the [Proven Commons academy](https://github.com/Proven-Commons/mission): a first proof, read and then written, on code small enough to hold in your head. Status: in progress. The specification has not yet been approved by a reviewer apart from its author, so this is not verified. ## 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 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. | Claim | Theorem | |-------|---------| @@ -29,6 +29,10 @@ The statements are in `Spec.lean`, the definitions they use in `Spec/Defs.lean`, | 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 exactly the strict form of RFC 7468 (Figure 3): `-----BEGIN label-----`, the base 64 of the data in lines of 64 characters with the last shorter, and `-----END label-----`, each line ending in LF. 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, 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` | +| 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` | The command-line tool in `Main.lean` calls these functions directly. @@ -38,6 +42,8 @@ The command-line tool in `Main.lean` calls these functions directly. - Speed. The code works on lists, which suits proofs, not large data. - Base 64 variants: the URL-safe alphabet, line breaks, and unpadded text are not supported. Strict decoding also rejects two kinds of text that Python's strict mode decodes: unused bits before the padding that are not zero, and, in Python 3.11 and in 3.12 before 3.12.4, padding after a whole group, such as `Zm9v=`. The tests count both. - Percent-encoding with another set of characters left as they are, such as the `+` for a space of HTML forms or the wider sets of JavaScript's `encodeURIComponent`. Which characters a URI component allows, and whether text is decoded at the right layer, are for a URI parser. This codec decodes what it is given, once, and does not check that it is URI text: it reads any US-ASCII character but `%` as itself, and reads `%00` as a NUL byte. Section 7.3 of RFC 3986 says `%00` should be rejected where an application does not expect raw data in a component; that check is the caller's. +- PEM in any form but the strict one. The lax forms of RFC 7468 (Figures 1 and 2), which allow blanks, empty lines, and other line lengths, are refused, as are the headers of older PEM (RFC 1421), text around the message, and a file of several messages. Which label goes with which kind of data, and what that data means, is for the caller: a label is any text the `label` rule allows. +- Two points the strict form leaves open, settled here. It has no text for empty data, since its last line of base 64 needs four characters: here empty data is the BEGIN and END lines alone, as Go's `encoding/pem` and Python's `ssl` write it. And it allows a last group whose unused bits are not zero, which this codec's strict base 64 refuses. - Hex with spaces, line breaks, or a `0x` prefix, which decoding rejects. Hex is RFC 4648 base 16 up to case: it writes lowercase, as Python does, where the RFC's alphabet is uppercase. - Other checksums, such as CRC-32C. A frame is this library's own layout, a message and its CRC-32, not a gzip or zip file. @@ -55,7 +61,9 @@ This project has no dependencies beyond Lean itself. ## Other decoders -`tests/CROSS-CHECK.md` records a one-off comparison of the percent-decoder with Go's `net/url.PathUnescape`. It is not part of the verified bar. On every text in US-ASCII that the tests give the decoder, Go gives the same answer, bad escapes included. Go reads a character outside US-ASCII as its UTF-8 bytes, where this decoder refuses it. +`tests/CROSS-CHECK.md` records a one-off comparison of the percent-decoder with Go's `net/url.PathUnescape`, and of PEM with Go's `encoding/pem`. It is not part of the verified bar. On every text in US-ASCII that the tests give the decoder, Go gives the same answer, bad escapes included. Go reads a character outside US-ASCII as its UTF-8 bytes, where this decoder refuses it. + +For PEM, Go writes the same text for every label the RFC's `label` rule allows, empty data included; it also writes labels the rule refuses. Go reads PEM laxly: it skips text around a block and takes headers and blanks, which this decoder refuses. And it ends lines at LF only, so it does not read text with a CR alone as a line end, which RFC 7468 allows and this decoder reads. Apart from those, on every text this decoder accepts, Go reads the same label and data. ## Re-check it @@ -71,7 +79,7 @@ python3 tests/run_tests.py ## Layout -- `Codec/Hex.lean`, `Codec/Base64.lean`, `Codec/Crc32.lean`, `Codec/Percent.lean`: the code under proof. +- `Codec/Hex.lean`, `Codec/Base64.lean`, `Codec/Crc32.lean`, `Codec/Percent.lean`, `Codec/Pem.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. diff --git a/SPEC.md b/SPEC.md index 70cc7ee..368744e 100644 --- a/SPEC.md +++ b/SPEC.md @@ -1,6 +1,6 @@ # Specification: codec -Four small codecs: hex, base 64, CRC-32 with a frame around a message, and percent-encoding. 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. A reviewer who did not write this specification approves it, together with `Spec.lean`, `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. @@ -35,6 +35,19 @@ Scope: RFC 3986, section 2.1: a byte written as `%` and two hex digits. Decoders differ on bad escapes. Go's `url.PathUnescape` returns an error, as this one does. Python's `urllib.parse.unquote` passes them through as text. +## PEM + +Scope: RFC 7468, the textual encoding of PKIX, PKCS, and CMS structures, in its strict form (section 3, Figure 3). One message: a BEGIN line with a label, the base 64 of the data (RFC 4648, section 4, as the base 64 codec above writes it), and an END line with the same label. + +- Encoding writes `-----BEGIN label-----`, the base 64 in lines of exactly 64 characters with the last line shorter, and `-----END label-----`, each line ending in LF. It fails on a label that the `label` rule does not allow: `label = [ labelchar *( ["-" / SP] labelchar ) ]`, where a `labelchar` is printable US-ASCII except `-`. So a label is empty, or has no `-` or space at either end and never two in a row. +- Decoding reads exactly one message in that form. Each line may end in LF, CR, or CR LF, as the `eol` rule allows; CR LF is one line end. It fails on everything else, including: + - a different label on the END line, which the RFC lets parsers ignore but this one does not; + - blanks, empty lines, headers, and text before or after the message; + - a base 64 line of another length; + - base 64 that is not exactly the encoding of the data, such as a last group whose unused bits are not zero. + +The strict form has no text for empty data, since its last line of base 64 needs four characters. Here empty data is the BEGIN and END lines with nothing between, as Go's `encoding/pem` and Python's `ssl.DER_cert_to_PEM_cert` write it. + ## Valid inputs and errors Every encoder input and every `crc32` and `frame` input is valid. The decoders and `unframe` return `none` for anything they do not accept. No function can fail any other way. @@ -66,9 +79,13 @@ Each property is a theorem in `Spec.lean`, under the name given. The definitions | 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` | +| 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. 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. A function that did nothing, or that accepted too much, would fail at least one of them. +Together these fix every output. 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. 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. +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, `ssl.DER_cert_to_PEM_cert` for the `CERTIFICATE` label, and for other labels an encoder and a strict parser written in the tests from the ABNF of RFC 7468, with the base 64 checked by strict `binascii.a2b_base64` and by encoding it again. diff --git a/Spec.lean b/Spec.lean index 5843803..5d2b00a 100644 --- a/Spec.lean +++ b/Spec.lean @@ -177,3 +177,59 @@ theorem Spec.percent_vectors : Percent.decode "%zz".toList = none ∧ Percent.decode "%%41".toList = none ∧ Percent.decode "café".toList = none := sorry + +/-! ## PEM + +RFC 7468, the strict form of the textual encoding (Figure 3): a BEGIN +line with a label, the base 64 of the data in lines of 64 characters, +and an END line with the same label. -/ + +/-- The encoder writes exactly the strict form, each line ending in LF, + and 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 := + sorry + +/-- The decoder reads exactly the messages in the strict form, with any + `eol` at the end of each line, and gives their 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. -/ +theorem Spec.pem_decode_iff (text label : List Char) (data : List UInt8) : + Pem.decode text = some (label, data) ↔ 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) : + 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 + ("-----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) ∧ + 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]) ∧ + Pem.encode "RSA PRIVATE KEY".toList [0] = + some "-----BEGIN RSA PRIVATE KEY-----\nAA==\n-----END RSA PRIVATE KEY-----\n".toList ∧ + Pem.encode "A--B".toList [] = none ∧ + Pem.encode "A B".toList [] = none ∧ + Pem.encode " A".toList [] = none ∧ + Pem.encode "A-".toList [] = none ∧ + Pem.encode "\u00c9".toList [] = none ∧ + Pem.decode "-----BEGIN X-----\nAA==\n-----END Y-----\n".toList = none ∧ + Pem.decode "-----BEGIN X-----\nAA==\n-----END X-----".toList = none ∧ + Pem.decode "-----BEGIN X-----\nAA== \n-----END X-----\n".toList = none ∧ + Pem.decode "-----BEGIN X----- \nAA==\n-----END X-----\n".toList = none ∧ + Pem.decode "-----BEGIN X-----\n\nAA==\n-----END X-----\n".toList = none ∧ + Pem.decode "-----BEGIN X-----\nProc-Type: 4,ENCRYPTED\nAA==\n-----END X-----\n".toList = none ∧ + Pem.decode "text\n-----BEGIN X-----\nAA==\n-----END X-----\n".toList = none ∧ + Pem.decode "-----BEGIN X-----\nAA==\n-----END X-----\n\n".toList = none ∧ + Pem.decode "-----BEGIN X-----\nAB==\n-----END X-----\n".toList = none ∧ + Pem.decode ("-----BEGIN X-----\nAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA\nAAAAAAAA\n".toList ++ + "-----END X-----\n".toList) = none := sorry diff --git a/Spec/Defs.lean b/Spec/Defs.lean index e7be4ce..7a9a02b 100644 --- a/Spec/Defs.lean +++ b/Spec/Defs.lean @@ -178,3 +178,109 @@ inductive Spec.PctReads : List Char → List UInt8 → Prop where | 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) + +/-! ## PEM + +RFC 7468, the textual encoding of PKIX, PKCS, and CMS structures, +section 3, the strict form (Figure 3) and the rules it uses (Figure 1): + +``` +stricttextualmsg = preeb eol + strictbase64text + posteb eol + +strictbase64finl = *15(4base64char) (4base64char / 3base64char + base64pad / 2base64char 2base64pad) eol +base64fullline = 64base64char eol +strictbase64text = *base64fullline strictbase64finl + +preeb = "-----BEGIN " label "-----" +posteb = "-----END " label "-----" +labelchar = %x21-2C / %x2E-7E ; any printable character, + ; except hyphen-minus +label = [ labelchar *( ["-" / SP] labelchar ) ] ; empty ok +eol = CRLF / CR / LF +``` + +Section 2: "Generators MUST put the same label on the "-----END " line +(post-encapsulation boundary) as the corresponding "-----BEGIN " line." +"Generators MUST wrap the base64-encoded lines so that each line consists +of exactly 64 characters except for the final line". + +The base 64 is RFC 4648, section 4, as `Base64.encode` writes it; its +statements above pin it down. Two points the strict form leaves open are +settled here. It has no text for empty data, since `strictbase64finl` +needs four characters: here empty data has no line of base 64. And it +allows a final group whose 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 := + (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 [] + | char {c : Char} {rest : List Char} : + Spec.labelChar c → Spec.LabelTail rest → Spec.LabelTail (c :: rest) + | sep {s c : Char} {rest : List Char} : + (s = '-' ∨ s = ' ') → Spec.labelChar c → Spec.LabelTail rest → + 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 + +/-- `eol = CRLF / CR / LF`. -/ +def 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 [] [] + | 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) + +/-- `*base64fullline strictbase64finl`, without the line ends: the base + 64 text cut into lines of 64 characters, the last one shorter. -/ +def 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) ++ + ["-----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 + +/-- `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) + +-- 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 + +/-- The data of RFC 7468, Figure 15 (a subject public key info), as the + base 64 there spells it. -/ +def 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, + 0x1D, 0xF2, 0x0C, 0x4F, 0x37, 0xC4, 0xA8, 0x93, 0x95, 0xCE, 0xD2, 0xDE, + 0x90, 0xB7, 0x21, 0xA7, 0x68, 0x62, 0xEF, 0xC7, 0x02, 0x68, 0xC6, 0x3C, + 0xD4, 0x50, 0x65, 0x62, 0xCF, 0x09, 0xF6, 0x5E, 0xE4, 0xAD, 0xCF, 0x8C, + 0xE1, 0xA0, 0x5E, 0x08, 0x66, 0x05, 0x8D, 0xB6, 0xBE, 0x86, 0x25, 0xED, + 0xB4, 0x95, 0x8F, 0x2F, 0xBC, 0x9D, 0x94, 0x4F, 0xB9, 0x50, 0x6E, 0x14, + 0x36, 0x49, 0xF7, 0x12, 0x8B, 0x3C, 0x12, 0x26, 0x41, 0xCA, 0x2F, 0x43, + 0x56, 0xCC, 0x9F, 0xCB, 0xD7, 0x9E, 0x8E, 0x1F, 0xBC, 0x01, 0x78, 0x29] diff --git a/bar.toml b/bar.toml index 65d8884..a1584b2 100644 --- a/bar.toml +++ b/bar.toml @@ -20,6 +20,7 @@ code = [ "Codec.Base64.encode", "Codec.Base64.decode", "Codec.Crc32.crc32", "Codec.Crc32.frame", "Codec.Crc32.unframe", "Codec.Percent.encode", "Codec.Percent.decode", + "Codec.Pem.encode", "Codec.Pem.decode", ] # One entry per approval, added in a pull request the reviewer approves. diff --git a/comparator.json b/comparator.json index ac97690..214a339 100644 --- a/comparator.json +++ b/comparator.json @@ -23,7 +23,11 @@ "Spec.percent_encode_eq", "Spec.percent_decode_iff", "Spec.percent_decode_encode", - "Spec.percent_vectors" + "Spec.percent_vectors", + "Spec.pem_encode_iff", + "Spec.pem_decode_iff", + "Spec.pem_decode_encode", + "Spec.pem_vectors" ], "permitted_axioms": [ "propext", diff --git a/tests/CROSS-CHECK.md b/tests/CROSS-CHECK.md index ef60584..d64890e 100644 --- a/tests/CROSS-CHECK.md +++ b/tests/CROSS-CHECK.md @@ -3,8 +3,15 @@ Written by `tests/cross_check.py`, once, by hand. It is not part of the verified bar. - Seed: 20261024 -- Texts given to the percent-decoder: 294412, of which 252015 it accepts +- Texts given to the percent-decoder: 254697, of which 218319 it accepts - Go: `net/url.PathUnescape`, go version go1.24.7 linux/amd64 -- Texts in US-ASCII: 272971, differences: 0 -- Texts with a character outside US-ASCII: 21441, of which this decoder accepts 0. Go reads such a character as its UTF-8 bytes, and gives the same answer on 5828 of them (where it finds a bad escape too) and a different one on 15613. +- Texts in US-ASCII: 236466, differences: 0 +- Texts with a character outside US-ASCII: 18231, of which this decoder accepts 0. Go reads such a character as its UTF-8 bytes, and gives the same answer on 4869 of them (where it finds a bad escape too) and a different one on 13362. + + +## PEM + +- Go: `encoding/pem`, go version go1.24.7 linux/amd64 +- Encoding requests: 51114. The same text from both: 41955. Go writes a label this encoder refuses: 9159. Other differences: 0. +- Decoding requests: 83920. The same answer from both, with nothing left over in Go: 50108. Go reads text this decoder refuses: 4721. This decoder accepts text with a CR alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines at LF only: 29091. Other differences, where this decoder accepts text that Go reads differently or not at all: 0. diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 333f6e2..73d0a54 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -2,13 +2,13 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. -- Oracle: Python 3.13.17 `binascii`, `base64`, `zlib` (zlib 1.3), `urllib.parse` +- Oracle: Python 3.13.17 `binascii`, `base64`, `zlib` (zlib 1.3), `urllib.parse`, `ssl.DER_cert_to_PEM_cert` - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261024 - Inputs: 1000000 -- Mutated: 235073 of the inputs are mutated encodings or frames -- By operation: b64dec 117552, b64enc 58769, crc 58771, error 71, frame 58769, hexdec 176323, hexenc 58772, pctdec 294412, pctenc 59024, unframe 117537 -- Malformed requests answered `error`: 71 of 71 +- Mutated: 245115 of the inputs are mutated encodings or frames +- By operation: b64dec 101665, b64enc 50825, crc 50827, error 77, frame 50825, hexdec 152491, hexenc 50828, pctdec 254697, pctenc 51081, pemdec 83920, pemenc 51114, unframe 101650 +- Malformed requests answered `error`: 77 of 77 - Last lines with no LF, sent alone, answered right: 6 of 6 -- Strict base 64 rejections where Python decodes: 10562 (10562 with unused bits before the padding not zero, 0 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) +- Strict base 64 rejections where Python decodes: 9256 (9256 with unused bits before the padding not zero, 0 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) - Failures: 0 diff --git a/tests/cross_check.py b/tests/cross_check.py index 59d9067..4511955 100644 --- a/tests/cross_check.py +++ b/tests/cross_check.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -"""A one-off comparison of the percent-decoder with Go's. +"""A one-off comparison of the percent-decoder and of PEM with Go's. Unlike tests/run_tests.py, this is not part of the verified bar and is not run in CI. It needs Go: @@ -11,11 +11,21 @@ `net/url.PathUnescape`. Go reads a character outside US-ASCII as its UTF-8 bytes, where this decoder refuses it, so texts with such a character are counted on their own. On every other text the two must -agree. The counts go to tests/CROSS-CHECK.md. +agree. + +Then each PEM request tests/run_tests.py makes goes to Go's +`encoding/pem`: `pemenc` to `pem.EncodeToMemory`, and `pemdec` to +`pem.Decode`. Go writes any label, where this encoder refuses one the +RFC's `label` rule does not allow, and Go reads PEM laxly, skipping text +around a block and taking headers and blanks. So each difference is +sorted by kind, and only text this decoder accepts and Go reads +differently, or not at all, counts against it. The counts go to +tests/CROSS-CHECK.md. """ import argparse import os +import re import subprocess import sys from pathlib import Path @@ -29,6 +39,69 @@ BUILD = ROOT / ".lake" / "cross_check" +def run_tests_nums(req): + arg = req.split(" ", 1)[1] if " " in req else "" + return [int(n) for n in arg.split(",") if n] + + +def pem_section(args, version): + items = [(label, req, want) for label, req, want, _, _ in run_tests.cases(args.seed, args.count) + if label in ("pemenc", "pemdec")] + ours, problem = run_tests.run_tool("".join(req + "\n" for _, req, _ in items)) + if problem or len(ours) != len(items): + sys.exit(f"the tool failed: {problem}") + subprocess.run(["go", "build", "-o", str(BUILD / "go-pem"), "pem.go"], cwd=HELPERS, + check=True, env={**os.environ, "GO111MODULE": "off"}) + go_reqs = [("enc " if label == "pemenc" else "dec ") + req.split(" ", 1)[1] + for label, req, _ in items] + go = subprocess.run([str(BUILD / "go-pem")], input="".join(r + "\n" for r in go_reqs), + capture_output=True, text=True, check=True).stdout.splitlines() + if len(go) != len(items): + sys.exit(f"Go gave {len(go)} answers for {len(items)} PEM requests") + enc = {"same": 0, "Go writes a label this encoder refuses": 0, "other": []} + dec = {"same": 0, "Go reads text this decoder refuses": 0, "lone CR": 0, "other": []} + for (label, req, _), o, g in zip(items, ours, go): + if label == "pemenc": + if o == g: + enc["same"] += 1 + elif o == "none" and g.startswith("ok:"): + enc["Go writes a label this encoder refuses"] += 1 + else: + enc["other"].append((req, o, g)) + else: + # Go's answer with nothing left over is the same block. + g_same = g.startswith("ok:") and g.rsplit(";", 1)[1] == "0" and o == g.rsplit(";", 1)[0] + if g_same or (o == "none" and g == "none"): + dec["same"] += 1 + elif o == "none": + dec["Go reads text this decoder refuses"] += 1 + elif re.search("\r(?!\n)", "".join(map(chr, run_tests_nums(req)))): + # RFC 7468 allows CR alone as a line end; Go splits lines + # at LF only. + dec["lone CR"] += 1 + else: + dec["other"].append((req, o, g)) + lines = [ + "", + "## PEM", + "", + f"- Go: `encoding/pem`, {version}", + f"- Encoding requests: {sum(1 for l, _, _ in items if l == 'pemenc')}. The same text from both: " + f"{enc['same']}. Go writes a label this encoder refuses: " + f"{enc['Go writes a label this encoder refuses']}. Other differences: {len(enc['other'])}.", + f"- Decoding requests: {sum(1 for l, _, _ in items if l == 'pemdec')}. The same answer from " + f"both, with nothing left over in Go: {dec['same']}. Go reads text this decoder refuses: " + f"{dec['Go reads text this decoder refuses']}. This decoder accepts text with a CR " + f"alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines " + f"at LF only: {dec['lone CR']}. Other differences, where this decoder accepts text that " + f"Go reads differently or not at all: {len(dec['other'])}.", + "", + ] + lines += [f"- `{r[:100]}`: this project `{o[:60]}`, Go `{g[:60]}`" + for r, o, g in (enc["other"] + dec["other"])[:10]] + return lines + + def main(): ap = argparse.ArgumentParser() ap.add_argument("--seed", type=int, default=20261024) @@ -82,6 +155,7 @@ def non_ascii(a): "", ] lines += [f"- `{a}`: this project `{o}`, Go `{g}`" for a, o, g in ascii_diffs[:10]] + lines += pem_section(args, version) REPORT.write_text("\n".join(lines) + "\n", encoding="utf-8") print(f"{len(reqs)} texts; report in {REPORT}") diff --git a/tests/cross_check/pem.go b/tests/cross_check/pem.go new file mode 100644 index 0000000..58784d6 --- /dev/null +++ b/tests/cross_check/pem.go @@ -0,0 +1,92 @@ +// Reads one request per line and prints what Go's encoding/pem makes of +// it. Used by tests/cross_check.py. +// +// enc LABEL;DATA the label's character codes and the bytes, as +// comma-separated decimal numbers; prints "ok:" and the +// character codes of pem.EncodeToMemory, or "none" on +// an error +// dec TEXT the text's character codes; prints "ok:", the type's +// character codes, ";", the bytes, ";", and the number +// of bytes pem.Decode left over; or "none" when it finds +// no block +package main + +import ( + "bufio" + "encoding/pem" + "fmt" + "os" + "strconv" + "strings" +) + +func numbers(s string) []int { + out := []int{} + if s == "" { + return out + } + for _, f := range strings.Split(s, ",") { + n, _ := strconv.Atoi(f) + out = append(out, n) + } + return out +} + +func text(ns []int) string { + var b strings.Builder + for _, n := range ns { + b.WriteRune(rune(n)) + } + return b.String() +} + +func codes(s string) string { + parts := []string{} + for _, r := range s { + parts = append(parts, strconv.Itoa(int(r))) + } + return strings.Join(parts, ",") +} + +func bytesOut(b []byte) string { + parts := make([]string, len(b)) + for i, x := range b { + parts[i] = strconv.Itoa(int(x)) + } + return strings.Join(parts, ",") +} + +func main() { + in := bufio.NewScanner(os.Stdin) + in.Buffer(make([]byte, 1<<20), 1<<26) + out := bufio.NewWriter(os.Stdout) + defer out.Flush() + for in.Scan() { + op, arg, _ := strings.Cut(in.Text(), " ") + switch op { + case "enc": + l, d, _ := strings.Cut(arg, ";") + data := []byte{} + for _, n := range numbers(d) { + data = append(data, byte(n)) + } + enc := pem.EncodeToMemory(&pem.Block{Type: text(numbers(l)), Bytes: data}) + if enc == nil { + fmt.Fprintln(out, "none") + } else { + fmt.Fprintln(out, "ok:"+codes(string(enc))) + } + case "dec": + block, rest := pem.Decode([]byte(text(numbers(arg)))) + if block == nil { + fmt.Fprintln(out, "none") + } else { + fmt.Fprintf(out, "ok:%s;%s;%d\n", codes(block.Type), bytesOut(block.Bytes), len(rest)) + } + } + } + if err := in.Err(); err != nil { + fmt.Fprintln(os.Stderr, err) + os.Exit(1) + } +} diff --git a/tests/run_tests.py b/tests/run_tests.py index a6b6440..678d80f 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -4,7 +4,10 @@ The oracles are Python's `binascii.hexlify` and `binascii.unhexlify`, `base64.b64encode` and strict `binascii.a2b_base64`, `zlib.crc32`, and for percent-encoding `urllib.parse.quote` with no safe characters and -`urllib.parse.unquote_to_bytes`. `unquote_to_bytes` passes a bad escape +`urllib.parse.unquote_to_bytes`; for PEM, `ssl.DER_cert_to_PEM_cert` +for the `CERTIFICATE` label, and for other labels an encoder and a strict +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 text that matches is given to it; the rest must be refused. Inputs come from @@ -41,6 +44,7 @@ import platform import random import re +import ssl import subprocess import sys import threading @@ -144,6 +148,12 @@ def decoded(result): ("hexdec 48,1114112", "beyond Unicode"), ("pctenc 37,256", "a byte above 255"), ("pctdec 37,55296", "a surrogate, not a character"), + ("pemenc", "no arguments"), + ("pemenc 88", "no `;` between the label and the data"), + ("pemenc 88;1;2", "two `;`"), + ("pemenc 88;256", "a byte above 255"), + ("pemenc 55296;1", "a surrogate in the label"), + ("pemdec 45,1114112", "beyond Unicode"), ("hexdec 48,2097201", "2^21 + 49, which wraps at 21 bits to a digit"), ("hexdec 55357,56385", "a UTF-16 surrogate pair, not a character"), ("b64dec 90,103,61,99999999999999999999", "beyond Unicode"), @@ -233,6 +243,92 @@ def mutate_pct(rng, text): return text[:i] + "".join(rng.choice(PCT_POOL) for _ in range(rng.randrange(1, 4))) + text[i:] +# RFC 7468, section 3: `label`, `eol`, and the strict form (Figure 3). +PEM_LABEL = r"(?:[\x21-\x2c\x2e-\x7e](?:[- ]?[\x21-\x2c\x2e-\x7e])*)?" +PEM_EOL = r"(?:\r\n|\r|\n)" +PEM_TEXT = re.compile(r"-----BEGIN (" + PEM_LABEL + r")-----" + PEM_EOL + + r"((?:[A-Za-z0-9+/=]+" + PEM_EOL + r")*)" + + r"-----END \1-----" + PEM_EOL) +PEM_LABELS = ["CERTIFICATE", "X509 CRL", "CERTIFICATE REQUEST", "PKCS7", "CMS", "PRIVATE KEY", + "ENCRYPTED PRIVATE KEY", "ATTRIBUTE CERTIFICATE", "PUBLIC KEY", "", "A", "a-b c", + "!~", "X.509 CERTIFICATE"] +BAD_PEM_LABELS = ["A--B", "A B", "A -B", " A", "A ", "-A", "A-", "-", " ", "\xe9", "\x7f", "A\tB", + "A\nB", "A-----", "\u0130"] +PEM_POOL = "\r\n -=+/AZaz09-!~\t\xe9" + + +def oracle_pem_encode(label, data): + if not re.fullmatch(PEM_LABEL, label): + return None + b64 = base64.b64encode(data).decode() + lines = [b64[i:i + 64] for i in range(0, len(b64), 64)] + return "".join(line + "\n" for line in + [f"-----BEGIN {label}-----"] + lines + [f"-----END {label}-----"]) + + +def pem_encoded(label, data): + """The expected `pemenc` answer: from Python's own `ssl` for + certificates, else from the encoder above.""" + text = (ssl.DER_cert_to_PEM_cert(data) if label == "CERTIFICATE" + else oracle_pem_encode(label, data)) + return "none" if text is None else "ok:" + text_nums(text) + + +def oracle_pem_decode(text): + m = PEM_TEXT.fullmatch(text) + if not m: + return None + label, body = m.group(1), m.group(2) + lines = re.split(PEM_EOL, body)[:-1] if body else [] + if any(len(line) != 64 for line in lines[:-1]) or (lines and len(lines[-1]) > 64): + return None + b64 = "".join(lines) + try: + data = binascii.a2b_base64(b64.encode(), strict_mode=True) + except binascii.Error: + return None + if base64.b64encode(data).decode() != b64: + return None + return label, data + + +def pem_decoded(text): + result = oracle_pem_decode(text) + return "none" if result is None else f"ok:{text_nums(result[0])};{nums(result[1])}" + + +def pem_eols(rng, text): + """`text`, each LF replaced by a line end drawn from LF, CR and CR LF.""" + return "".join(rng.choice(["\n", "\r", "\r\n"]) if c == "\n" else c for c in text) + + +def mutate_pem(rng, text): + """One random mutation of a PEM text.""" + kind = rng.randrange(8) + i = rng.randrange(len(text) + 1) + if kind == 0 and text: + return text[:i % len(text)] + rng.choice(PEM_POOL) + text[i % len(text) + 1:] + if kind == 1: + return text[:i] + rng.choice(PEM_POOL) + text[i:] + if kind == 2 and text: + return text[:i % len(text)] + text[i % len(text) + 1:] + if kind == 3: + return rng.choice(["x\n", "\n", " "]) + text + if kind == 4: + return text + rng.choice(["x", "\n", " ", "x\n"]) + if kind == 5: + return text.replace("-----END ", "-----END X", 1) + if kind == 6: + first = text.find("\n") + return text[:first + 1] + "Proc-Type: 4,ENCRYPTED\n" + text[first + 1:] + # Join two lines, or cut a line in two. + nl = [k for k, c in enumerate(text) if c == "\n"] + if len(nl) > 2 and rng.random() < 0.5: + k = rng.choice(nl[1:-1]) + return text[:k] + text[k + 1:] + return text[:i] + "\n" + text[i:] + + def oracle_unframe(fr): if len(fr) < 4: return None @@ -322,6 +418,15 @@ def fixed_cases(): # encoder's and the decoder's per-character rules. for b in range(256): items.append(("pctenc", f"pctenc {b}", oracle_pctenc(bytes([b])), None, False)) + # PEM: every label above with data at the line edges (48 bytes are + # one full line), and every bad label. + for label in PEM_LABELS + BAD_PEM_LABELS: + for n in (0, 1, 2, 3, 47, 48, 49, 95, 96, 97): + data = bytes((7 * k + n) % 256 for k in range(n)) + items.append(("pemenc", f"pemenc {text_nums(label)};{nums(data)}", + pem_encoded(label, data), None, False)) + text = oracle_pem_encode(label, data) or f"-----BEGIN {label}-----\n-----END {label}-----\n" + items.append(("pemdec", f"pemdec {text_nums(text)}", pem_decoded(text), None, False)) for c in range(128): text = chr(c) items.append(("pctdec", f"pctdec {text_nums(text)}", decoded(oracle_pctdec(text)), None, False)) @@ -378,6 +483,16 @@ def cases(seed, count): batch.append(("pctdec", f"pctdec {text_nums(bad_pct)}", decoded(oracle_pctdec(bad_pct)), None, True)) raw = "".join(rng.choice(PCT_POOL) for _ in range(rng.randrange(8))) batch.append(("pctdec", f"pctdec {text_nums(raw)}", decoded(oracle_pctdec(raw)), None, False)) + label = rng.choice(PEM_LABELS + BAD_PEM_LABELS[:3]) + pem_data = data[: rng.choice([0, 1, 47, 48, 49, 96, 97, 200, len(data)])] + batch.append(("pemenc", f"pemenc {text_nums(label)};{nums(pem_data)}", + pem_encoded(label, pem_data), None, False)) + pem_text = oracle_pem_encode(label, pem_data) + if pem_text is not None: + ends = pem_eols(rng, pem_text) + batch.append(("pemdec", f"pemdec {text_nums(ends)}", pem_decoded(ends), None, False)) + bad_pem = changed(mutate_pem, rng, ends) + batch.append(("pemdec", f"pemdec {text_nums(bad_pem)}", pem_decoded(bad_pem), None, True)) batch = batch[: count - made] yield from batch made += len(batch) @@ -445,7 +560,7 @@ def drain(stream, buf, cap): def oracle(): return (f"Python {platform.python_version()} `binascii`, `base64`, `zlib` " - f"(zlib {zlib.ZLIB_RUNTIME_VERSION}), `urllib.parse`") + f"(zlib {zlib.ZLIB_RUNTIME_VERSION}), `urllib.parse`, `ssl.DER_cert_to_PEM_cert`") def lean_version(): From ee826ec3c0e0699ef15ef683c0aa2681008cb085 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 03:35:47 +0000 Subject: [PATCH 2/5] Say where PEM departs from the strict form, and widen its tests From an independent pre-review: - The page said the encoder writes, and the decoder reads, "exactly the strict form". For empty data, which that form cannot express, both use the BEGIN and END lines alone; the claims and Spec.lean's docstrings now say so. The page also says that with LF line ends only the lax form allows that text, and that the standard form's text for empty data is refused. Figure 1 is the standard form, not a lax one. - The last line of base 64 is at most 64 characters, not always shorter. - SPEC.md's paragraph on valid inputs and its description of the tool now cover PEM, and Spec/Defs.lean's header names its one use of code, Base64.encode, which the base 64 statements pin down. - The page and the record name the PEM oracle as it is: an encoder and strict parser written in the tests from RFC 7468. Where that parser accepts a certificate, Python's ssl.PEM_cert_to_DER_cert must now read the same data. - The labels `,`, `A,B` and `A:B` join the tests, and `,` and `:` the mutations; Spec.pem_vectors gains `A,B`. An off-by-one at `,` in the label rule now fails both the tests and the proofs. - Go refuses a message with empty data under a label with `:`, taking the END line for a header; the cross-check counts it and the page names it, and its claim is scoped to the texts it tried. lake comparator --paranoid accepts all 26 theorems; 1,000,000 inputs, 0 failures. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Codec/Pem.lean | 4 ++-- Main.lean | 3 ++- Proofs/Pem.lean | 1 + README.md | 16 ++++++++-------- SPEC.md | 10 +++++----- Spec.lean | 11 +++++++---- Spec/Defs.lean | 19 ++++++++++++------- tests/CROSS-CHECK.md | 10 +++++----- tests/TEST-RESULTS.md | 8 ++++---- tests/cross_check.py | 11 +++++++++-- tests/run_tests.py | 12 +++++++++--- 11 files changed, 64 insertions(+), 41 deletions(-) diff --git a/Codec/Pem.lean b/Codec/Pem.lean index 6651ba4..e798c0d 100644 --- a/Codec/Pem.lean +++ b/Codec/Pem.lean @@ -2,7 +2,7 @@ PEM, the textual encoding of RFC 7468, in its strict form (Figure 3): -----BEGIN label----- - the base 64 of the data, in lines of 64 characters, the last shorter + the base 64 of the data, in lines of 64 characters, the last at most 64 -----END label----- `encode` writes each line ending in LF, and fails on a label that the @@ -40,7 +40,7 @@ def validLabel : List Char → Bool | [] => true | c :: rest => isLabelChar c && labelRest rest -/-- Cut text into lines of 64 characters, the last one shorter. `fuel` +/-- Cut text into lines of 64 characters, the last one at most 64. `fuel` equal to the text's length is enough. -/ def lines64 : Nat → List Char → List (List Char) | _, [] => [] diff --git a/Main.lean b/Main.lean index 8e9d59c..a9b2b13 100644 --- a/Main.lean +++ b/Main.lean @@ -25,7 +25,8 @@ character codes. A request is an operation, then optionally one space and its numbers; - with no numbers after the space, the input is empty. A malformed + with no numbers after the space, the input is empty. `pemenc` is the + exception: it needs its one space and one `;`. A malformed request prints `error`: any other line, an unknown operation, a number that is not plain decimal digits, a byte above 255, or a character code that is not a Unicode scalar value. A line may end in LF or diff --git a/Proofs/Pem.lean b/Proofs/Pem.lean index d093536..6e87340 100644 --- a/Proofs/Pem.lean +++ b/Proofs/Pem.lean @@ -220,6 +220,7 @@ theorem Spec.pem_vectors : Pem.decode "-----BEGIN -----\rAA==\r-----END -----\r".toList = some ([], [0]) ∧ Pem.encode "RSA PRIVATE KEY".toList [0] = some "-----BEGIN RSA PRIVATE KEY-----\nAA==\n-----END RSA PRIVATE KEY-----\n".toList ∧ + Pem.encode "A,B".toList [] = some "-----BEGIN A,B-----\n-----END A,B-----\n".toList ∧ Pem.encode "A--B".toList [] = none ∧ Pem.encode "A B".toList [] = none ∧ Pem.encode " A".toList [] = none ∧ diff --git a/README.md b/README.md index 012bbc6..8fe49a1 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # codec: hex, base 64, CRC-32, percent-encoding and PEM, proved -Five small codecs in Lean, each with machine-checked proofs that it does exactly what its specification says, and tested against Python's standard library on a million inputs in all (see `tests/TEST-RESULTS.md`). Hex is written as Python's `bytes.hex()` writes it, base 64 follows RFC 4648, the CRC-32 is the one in gzip, zip, and PNG, percent-encoding follows RFC 3986, and PEM is the strict form of RFC 7468, the text that wraps certificates and keys. They are also the material for Level 0 of the [Proven Commons academy](https://github.com/Proven-Commons/mission): a first proof, read and then written, on code small enough to hold in your head. +Five small codecs in Lean, each with machine-checked proofs that it does exactly what its specification says, and tested on a million inputs in all against Python's standard library and, for PEM, against an encoder and strict parser written in the tests from RFC 7468 (see `tests/TEST-RESULTS.md`). Hex is written as Python's `bytes.hex()` writes it, base 64 follows RFC 4648, the CRC-32 is the one in gzip, zip, and PNG, percent-encoding follows RFC 3986, and PEM is the strict form of RFC 7468, the text that wraps certificates and keys. They are also the material for Level 0 of the [Proven Commons academy](https://github.com/Proven-Commons/mission): a first proof, read and then written, on code small enough to hold in your head. Status: in progress. The specification has not yet been approved by a reviewer apart from its author, so this is not verified. @@ -29,8 +29,8 @@ The statements are in `Spec.lean`, the definitions they use in `Spec/Defs.lean`, | 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 exactly the strict form of RFC 7468 (Figure 3): `-----BEGIN label-----`, the base 64 of the data in lines of 64 characters with the last shorter, and `-----END label-----`, each line ending in LF. 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, 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 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` | | 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` | @@ -42,8 +42,8 @@ The command-line tool in `Main.lean` calls these functions directly. - Speed. The code works on lists, which suits proofs, not large data. - Base 64 variants: the URL-safe alphabet, line breaks, and unpadded text are not supported. Strict decoding also rejects two kinds of text that Python's strict mode decodes: unused bits before the padding that are not zero, and, in Python 3.11 and in 3.12 before 3.12.4, padding after a whole group, such as `Zm9v=`. The tests count both. - Percent-encoding with another set of characters left as they are, such as the `+` for a space of HTML forms or the wider sets of JavaScript's `encodeURIComponent`. Which characters a URI component allows, and whether text is decoded at the right layer, are for a URI parser. This codec decodes what it is given, once, and does not check that it is URI text: it reads any US-ASCII character but `%` as itself, and reads `%00` as a NUL byte. Section 7.3 of RFC 3986 says `%00` should be rejected where an application does not expect raw data in a component; that check is the caller's. -- PEM in any form but the strict one. The lax forms of RFC 7468 (Figures 1 and 2), which allow blanks, empty lines, and other line lengths, are refused, as are the headers of older PEM (RFC 1421), text around the message, and a file of several messages. Which label goes with which kind of data, and what that data means, is for the caller: a label is any text the `label` rule allows. -- Two points the strict form leaves open, settled here. It has no text for empty data, since its last line of base 64 needs four characters: here empty data is the BEGIN and END lines alone, as Go's `encoding/pem` and Python's `ssl` write it. And it allows a last group whose unused bits are not zero, which this codec's strict base 64 refuses. +- PEM in any form but the strict one. The standard and lax forms of RFC 7468 (Figures 1 and 2), which allow blanks, empty lines, and other line lengths, are refused, as are the headers of older PEM (RFC 1421), text around the message, and a file of several messages. Which label goes with which kind of data, and what that data means, is for the caller: a label is any text the `label` rule allows. +- Two points where this codec departs from the strict form. The strict form has no text for empty data, since its last line of base 64 needs four characters. Here empty data is the BEGIN and END lines alone, as Go's `encoding/pem` and Python's `ssl` write it. With LF line ends, only the lax form of RFC 7468 (Figure 2) allows that text; the text the standard form (Figure 1) gives empty data, with one empty line between BEGIN and END, is refused. And the strict form allows a last group whose unused bits are not zero, which this codec's strict base 64 refuses. - Hex with spaces, line breaks, or a `0x` prefix, which decoding rejects. Hex is RFC 4648 base 16 up to case: it writes lowercase, as Python does, where the RFC's alphabet is uppercase. - Other checksums, such as CRC-32C. A frame is this library's own layout, a message and its CRC-32, not a gzip or zip file. @@ -55,7 +55,7 @@ The command-line tool in `Main.lean` calls these functions directly. - The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. - Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about (by `implemented_by` and `extern`), such as the fixed-width integer operations in CRC-32 and the arithmetic on natural numbers. - The operating system and hardware it runs on. -- Python's standard library and zlib, as the oracle in the differential tests. The record names their versions. +- Python's standard library and zlib, and for PEM an encoder and strict parser written in `tests/run_tests.py` from RFC 7468, as the oracle in the differential tests. The record names their versions. This project has no dependencies beyond Lean itself. @@ -63,7 +63,7 @@ This project has no dependencies beyond Lean itself. `tests/CROSS-CHECK.md` records a one-off comparison of the percent-decoder with Go's `net/url.PathUnescape`, and of PEM with Go's `encoding/pem`. It is not part of the verified bar. On every text in US-ASCII that the tests give the decoder, Go gives the same answer, bad escapes included. Go reads a character outside US-ASCII as its UTF-8 bytes, where this decoder refuses it. -For PEM, Go writes the same text for every label the RFC's `label` rule allows, empty data included; it also writes labels the rule refuses. Go reads PEM laxly: it skips text around a block and takes headers and blanks, which this decoder refuses. And it ends lines at LF only, so it does not read text with a CR alone as a line end, which RFC 7468 allows and this decoder reads. Apart from those, on every text this decoder accepts, Go reads the same label and data. +For PEM, Go writes the same text for every label the RFC's `label` rule allows, empty data included; it also writes labels the rule refuses. Go reads PEM laxly: it skips text around a block and takes headers and blanks, which this decoder refuses. And it ends lines at LF only, so it refuses most text with a CR alone as a line end, which RFC 7468 allows and this decoder reads. Go also refuses a message with empty data whose label holds a `:`, such as `-----BEGIN A:B-----` then `-----END A:B-----`, which Go itself writes: it takes the END line for an RFC 1421 header. Apart from those, on every text the cross-check gives this decoder and it accepts, Go reads the same label and data. ## Re-check it @@ -75,7 +75,7 @@ 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 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 `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, and for PEM with an encoder and strict parser 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 diff --git a/SPEC.md b/SPEC.md index 368744e..1007653 100644 --- a/SPEC.md +++ b/SPEC.md @@ -39,20 +39,20 @@ Decoders differ on bad escapes. Go's `url.PathUnescape` returns an error, as thi Scope: RFC 7468, the textual encoding of PKIX, PKCS, and CMS structures, in its strict form (section 3, Figure 3). One message: a BEGIN line with a label, the base 64 of the data (RFC 4648, section 4, as the base 64 codec above writes it), and an END line with the same label. -- Encoding writes `-----BEGIN label-----`, the base 64 in lines of exactly 64 characters with the last line shorter, and `-----END label-----`, each line ending in LF. It fails on a label that the `label` rule does not allow: `label = [ labelchar *( ["-" / SP] labelchar ) ]`, where a `labelchar` is printable US-ASCII except `-`. So a label is empty, or has no `-` or space at either end and never two in a row. +- Encoding writes `-----BEGIN label-----`, the base 64 in lines of 64 characters with the last line at most 64, and `-----END label-----`, each line ending in LF. It fails on a label that the `label` rule does not allow: `label = [ labelchar *( ["-" / SP] labelchar ) ]`, where a `labelchar` is printable US-ASCII except `-`. So a label is empty, or has no `-` or space at either end and never two in a row. - Decoding reads exactly one message in that form. Each line may end in LF, CR, or CR LF, as the `eol` rule allows; CR LF is one line end. It fails on everything else, including: - a different label on the END line, which the RFC lets parsers ignore but this one does not; - blanks, empty lines, headers, and text before or after the message; - a base 64 line of another length; - base 64 that is not exactly the encoding of the data, such as a last group whose unused bits are not zero. -The strict form has no text for empty data, since its last line of base 64 needs four characters. Here empty data is the BEGIN and END lines with nothing between, as Go's `encoding/pem` and Python's `ssl.DER_cert_to_PEM_cert` write it. +The strict form has no text for empty data, since its last line of base 64 needs four characters. Here empty data is the BEGIN and END lines with nothing between, as Go's `encoding/pem` and Python's `ssl.DER_cert_to_PEM_cert` write it. With LF line ends, only the lax form (Figure 2) allows that text; the text the standard form (Figure 1) gives empty data, with one empty line between BEGIN and END, is refused. ## Valid inputs and errors -Every encoder input and every `crc32` and `frame` input is valid. The decoders and `unframe` return `none` for anything they do not accept. No function can fail any other way. +Every encoder input, except a PEM label that the `label` rule refuses, and every `crc32` and `frame` input is valid. The decoders and `unframe` return `none` for anything they do not accept, and PEM encoding returns `none` for such a label. No function can fail any other way. -The command-line tool in `Main.lean` reads one request per line and prints one answer per line. A request is an operation, then optionally one space and its comma-separated numbers; with no numbers after the space, the input is empty. The tool prints `error` for any other line, an unknown operation, a number that is not plain decimal digits, a byte above 255, or a character code that is not a Unicode scalar value. A line may end in LF or CR LF; nothing else around a request is ignored. +The command-line tool in `Main.lean` reads one request per line and prints one answer per line. A request is an operation, then optionally one space and its comma-separated numbers; with no numbers after the space, the input is empty. `pemenc` is the exception: after its one space come the label's character codes, `;`, and the bytes, each list possibly empty, and it answers `ok:` and the character codes of the PEM text, or `none`. `pemdec` answers `ok:`, the label's character codes, `;`, and the bytes, or `none`. The tool prints `error` for any other line, including `pemenc` without its space or its `;`, an unknown operation, a number that is not plain decimal digits, a byte above 255, or a character code that is not a Unicode scalar value. A line may end in LF or CR LF; nothing else around a request is ignored. ## What must always hold @@ -88,4 +88,4 @@ Together these fix every output. The encoders, `crc32`, and `frame` are given ex ## 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, `ssl.DER_cert_to_PEM_cert` for the `CERTIFICATE` label, and for other labels an encoder and a strict parser written in the tests from the ABNF of RFC 7468, with the base 64 checked by strict `binascii.a2b_base64` and by encoding it again. +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. diff --git a/Spec.lean b/Spec.lean index 5d2b00a..230e314 100644 --- a/Spec.lean +++ b/Spec.lean @@ -184,14 +184,16 @@ RFC 7468, the strict form of the textual encoding (Figure 3): a BEGIN line with a label, the base 64 of the data in lines of 64 characters, and an END line with the same label. -/ -/-- The encoder writes exactly the strict form, each line ending in LF, - and fails on a label the `label` rule does not allow. -/ +/-- 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 := sorry -/-- The decoder reads exactly the messages in the strict form, with any - `eol` at the end of each line, and gives their label and data. So +/-- The decoder reads exactly the messages in the strict form, and for + empty data the BEGIN and END lines alone, with any `eol` at the end + of each line, and gives their 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. -/ @@ -217,6 +219,7 @@ theorem Spec.pem_vectors : Pem.decode "-----BEGIN -----\rAA==\r-----END -----\r".toList = some ([], [0]) ∧ Pem.encode "RSA PRIVATE KEY".toList [0] = some "-----BEGIN RSA PRIVATE KEY-----\nAA==\n-----END RSA PRIVATE KEY-----\n".toList ∧ + Pem.encode "A,B".toList [] = some "-----BEGIN A,B-----\n-----END A,B-----\n".toList ∧ Pem.encode "A--B".toList [] = none ∧ Pem.encode "A B".toList [] = none ∧ Pem.encode " A".toList [] = none ∧ diff --git a/Spec/Defs.lean b/Spec/Defs.lean index 7a9a02b..7325ffd 100644 --- a/Spec/Defs.lean +++ b/Spec/Defs.lean @@ -1,6 +1,8 @@ /- The definitions the specification uses, written from the standards, - independently of the code in `Codec/`. Part of the approved + 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`. Both the challenge file and the proofs import this file, so each @@ -208,11 +210,14 @@ Section 2: "Generators MUST put the same label on the "-----END " line of exactly 64 characters except for the final line". The base 64 is RFC 4648, section 4, as `Base64.encode` writes it; its -statements above pin it down. Two points the strict form leaves open are -settled here. It has no text for empty data, since `strictbase64finl` -needs four characters: here empty data has no line of base 64. And it -allows a final group whose unused bits are not zero, which strict base 64 -refuses: here the base 64 is exactly `Base64.encode` of the data. -/ +statements pin it down. Two points depart from the strict form. It has +no text for empty data, since `strictbase64finl` needs four characters: +here empty data has no line of base 64, so its text is the BEGIN and END +lines alone. With LF line ends only the lax form (Figure 2) allows that +text, and the standard form's text for empty data (Figure 1), with one +empty line, is refused. And the strict form allows a final group whose +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 := @@ -245,7 +250,7 @@ inductive Spec.LinesEol : List Char → List (List Char) → Prop where 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 shorter. -/ + 64 text cut into lines of 64 characters, the last one at most 64. -/ def Spec.lines64 (s : List Char) : List (List Char) := (List.range ((s.length + 63) / 64)).map fun i => (s.drop (64 * i)).take 64 diff --git a/tests/CROSS-CHECK.md b/tests/CROSS-CHECK.md index d64890e..0cc33f9 100644 --- a/tests/CROSS-CHECK.md +++ b/tests/CROSS-CHECK.md @@ -3,15 +3,15 @@ Written by `tests/cross_check.py`, once, by hand. It is not part of the verified bar. - Seed: 20261024 -- Texts given to the percent-decoder: 254697, of which 218319 it accepts +- Texts given to the percent-decoder: 254047, of which 217736 it accepts - Go: `net/url.PathUnescape`, go version go1.24.7 linux/amd64 -- Texts in US-ASCII: 236466, differences: 0 -- Texts with a character outside US-ASCII: 18231, of which this decoder accepts 0. Go reads such a character as its UTF-8 bytes, and gives the same answer on 4869 of them (where it finds a bad escape too) and a different one on 13362. +- Texts in US-ASCII: 235889, differences: 0 +- Texts with a character outside US-ASCII: 18158, of which this decoder accepts 0. Go reads such a character as its UTF-8 bytes, and gives the same answer on 4877 of them (where it finds a bad escape too) and a different one on 13281. ## PEM - Go: `encoding/pem`, go version go1.24.7 linux/amd64 -- Encoding requests: 51114. The same text from both: 41955. Go writes a label this encoder refuses: 9159. Other differences: 0. -- Decoding requests: 83920. The same answer from both, with nothing left over in Go: 50108. Go reads text this decoder refuses: 4721. This decoder accepts text with a CR alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines at LF only: 29091. Other differences, where this decoder accepts text that Go reads differently or not at all: 0. +- Encoding requests: 51015. The same text from both: 43123. Go writes a label this encoder refuses: 7892. Other differences: 0. +- Decoding requests: 86226. The same answer from both, with nothing left over in Go: 51362. Go reads text this decoder refuses: 4794. This decoder accepts text with a CR alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines at LF only: 29531. This decoder reads empty data under a label with a `:`, and Go takes the END line for a header: 539. Other differences, where this decoder accepts text that Go reads differently or not at all: 0. diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 73d0a54..1df57e8 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -2,13 +2,13 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. -- Oracle: Python 3.13.17 `binascii`, `base64`, `zlib` (zlib 1.3), `urllib.parse`, `ssl.DER_cert_to_PEM_cert` +- Oracle: Python 3.13.17 `binascii`, `base64`, `zlib` (zlib 1.3), `urllib.parse`; for PEM, a strict encoder and parser written in tests/run_tests.py from RFC 7468, with `ssl.DER_cert_to_PEM_cert` and `ssl.PEM_cert_to_DER_cert` for the `CERTIFICATE` label - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261024 - Inputs: 1000000 -- Mutated: 245115 of the inputs are mutated encodings or frames -- By operation: b64dec 101665, b64enc 50825, crc 50827, error 77, frame 50825, hexdec 152491, hexenc 50828, pctdec 254697, pctenc 51081, pemdec 83920, pemenc 51114, unframe 101650 +- Mutated: 245733 of the inputs are mutated encodings or frames +- By operation: b64dec 101405, b64enc 50695, crc 50697, error 77, frame 50695, hexdec 152103, hexenc 50699, pctdec 254047, pctenc 50951, pemdec 86226, pemenc 51015, unframe 101390 - Malformed requests answered `error`: 77 of 77 - Last lines with no LF, sent alone, answered right: 6 of 6 -- Strict base 64 rejections where Python decodes: 9256 (9256 with unused bits before the padding not zero, 0 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) +- Strict base 64 rejections where Python decodes: 9024 (9024 with unused bits before the padding not zero, 0 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) - Failures: 0 diff --git a/tests/cross_check.py b/tests/cross_check.py index 4511955..f434ad0 100644 --- a/tests/cross_check.py +++ b/tests/cross_check.py @@ -59,7 +59,7 @@ def pem_section(args, version): if len(go) != len(items): sys.exit(f"Go gave {len(go)} answers for {len(items)} PEM requests") enc = {"same": 0, "Go writes a label this encoder refuses": 0, "other": []} - dec = {"same": 0, "Go reads text this decoder refuses": 0, "lone CR": 0, "other": []} + dec = {"same": 0, "Go reads text this decoder refuses": 0, "lone CR": 0, "colon": 0, "other": []} for (label, req, _), o, g in zip(items, ours, go): if label == "pemenc": if o == g: @@ -75,6 +75,11 @@ def pem_section(args, version): dec["same"] += 1 elif o == "none": dec["Go reads text this decoder refuses"] += 1 + elif o.endswith(";") and ":" in "".join(map(chr, run_tests_nums(req))).split("\n")[0] \ + and g == "none": + # Empty data under a label with `:`: Go takes the END line + # for an RFC 1421 header. + dec["colon"] += 1 elif re.search("\r(?!\n)", "".join(map(chr, run_tests_nums(req)))): # RFC 7468 allows CR alone as a line end; Go splits lines # at LF only. @@ -93,7 +98,9 @@ def pem_section(args, version): f"both, with nothing left over in Go: {dec['same']}. Go reads text this decoder refuses: " f"{dec['Go reads text this decoder refuses']}. This decoder accepts text with a CR " f"alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines " - f"at LF only: {dec['lone CR']}. Other differences, where this decoder accepts text that " + f"at LF only: {dec['lone CR']}. This decoder reads empty data under a label with a `:`, " + f"and Go takes the END line for a header: {dec['colon']}. Other differences, where this " + f"decoder accepts text that " f"Go reads differently or not at all: {len(dec['other'])}.", "", ] diff --git a/tests/run_tests.py b/tests/run_tests.py index 678d80f..f5fd769 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -251,10 +251,10 @@ def mutate_pct(rng, text): r"-----END \1-----" + PEM_EOL) PEM_LABELS = ["CERTIFICATE", "X509 CRL", "CERTIFICATE REQUEST", "PKCS7", "CMS", "PRIVATE KEY", "ENCRYPTED PRIVATE KEY", "ATTRIBUTE CERTIFICATE", "PUBLIC KEY", "", "A", "a-b c", - "!~", "X.509 CERTIFICATE"] + "!~", "X.509 CERTIFICATE", ",", "A,B", "A:B"] BAD_PEM_LABELS = ["A--B", "A B", "A -B", " A", "A ", "-A", "A-", "-", " ", "\xe9", "\x7f", "A\tB", "A\nB", "A-----", "\u0130"] -PEM_POOL = "\r\n -=+/AZaz09-!~\t\xe9" +PEM_POOL = "\r\n -=+/AZaz09-!~,:\t\xe9" def oracle_pem_encode(label, data): @@ -289,6 +289,10 @@ def oracle_pem_decode(text): return None if base64.b64encode(data).decode() != b64: return None + # Python's own reader, which is lax, must read an accepted certificate + # the same way. + if label == "CERTIFICATE" and ssl.PEM_cert_to_DER_cert(text) != data: + raise AssertionError(f"ssl.PEM_cert_to_DER_cert disagrees on {text!r}") return label, data @@ -560,7 +564,9 @@ def drain(stream, buf, cap): def oracle(): return (f"Python {platform.python_version()} `binascii`, `base64`, `zlib` " - f"(zlib {zlib.ZLIB_RUNTIME_VERSION}), `urllib.parse`, `ssl.DER_cert_to_PEM_cert`") + f"(zlib {zlib.ZLIB_RUNTIME_VERSION}), `urllib.parse`; for PEM, a strict encoder and " + "parser written in tests/run_tests.py from RFC 7468, with `ssl.DER_cert_to_PEM_cert` " + "and `ssl.PEM_cert_to_DER_cert` for the `CERTIFICATE` label") def lean_version(): From 2697cc511684346518370114095e1dc0a42fa40a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 04:24:17 +0000 Subject: [PATCH 3/5] Work in progress: Luhn and IBAN check digits (IBAN proofs still open) Codec.Luhn and Codec.Iban, their spec in Spec/Defs.lean, eleven statements in Spec.lean, the tool's luhn, luhncheck, iban and ibancheck requests, the tests (1,000,000 inputs, 0 failures), a cross-check with python-stdnum, and the page. The Luhn proofs are done. The IBAN statements other than the vectors still end in sorry, so lake comparator fails on this commit; the proofs are being written and land next. Plan and claim: #7. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Codec.lean | 2 + Codec/Iban.lean | 48 ++++++++++ Codec/Luhn.lean | 33 +++++++ Main.lean | 30 ++++++- Proofs.lean | 2 + Proofs/Iban.lean | 44 +++++++++ Proofs/Luhn.lean | 201 ++++++++++++++++++++++++++++++++++++++++++ README.md | 21 +++-- SPEC.md | 34 ++++++- Spec.lean | 79 +++++++++++++++++ Spec/Defs.lean | 71 +++++++++++++++ bar.toml | 2 + comparator.json | 13 ++- tests/CROSS-CHECK.md | 17 ++-- tests/TEST-RESULTS.md | 8 +- tests/cross_check.py | 110 ++++++++++++++++++++++- tests/run_tests.py | 123 +++++++++++++++++++++++++- 17 files changed, 815 insertions(+), 23 deletions(-) create mode 100644 Codec/Iban.lean create mode 100644 Codec/Luhn.lean create mode 100644 Proofs/Iban.lean create mode 100644 Proofs/Luhn.lean diff --git a/Codec.lean b/Codec.lean index e3f1353..e8fd2c3 100644 --- a/Codec.lean +++ b/Codec.lean @@ -3,3 +3,5 @@ import Codec.Base64 import Codec.Crc32 import Codec.Percent import Codec.Pem +import Codec.Luhn +import Codec.Iban diff --git a/Codec/Iban.lean b/Codec/Iban.lean new file mode 100644 index 0000000..219be5f --- /dev/null +++ b/Codec/Iban.lean @@ -0,0 +1,48 @@ +/- + IBAN check digits (ISO 13616), by ISO 7064 MOD 97-10. + + An IBAN in its electronic form is a country code of two letters, two + check digits, and a BBAN of 1 to 30 letters and digits, letters in + upper case. It passes the check when, with the first four characters + moved to the end and each letter written as 10 (A) to 35 (Z), the + digits read as a number are 1 more than a multiple of 97. +-/ + +namespace Codec.Iban + +def isDigit (c : Char) : Bool := '0' ≤ c && c ≤ '9' + +def isUpper (c : Char) : Bool := 'A' ≤ c && c ≤ 'Z' + +/-- A digit as its value, a letter as 10 to 35. -/ +def value (c : Char) : Nat := + if isDigit c then c.toNat - 48 else c.toNat - 55 + +/-- The remainder mod 97 of the number the characters write, each digit + as one decimal digit and each letter as two, computed one character + at a time so that the numbers stay small. -/ +def mod97 (cs : List Char) : Nat := + cs.foldl (fun r c => if isDigit c then (r * 10 + value c) % 97 else (r * 100 + value c) % 97) 0 + +/-- Two letters, two digits, then 1 to 30 letters or digits. -/ +def wellShaped (s : List Char) : Bool := + match s with + | c0 :: c1 :: k0 :: k1 :: bban => + isUpper c0 && isUpper c1 && isDigit k0 && isDigit k1 && + 1 ≤ bban.length && bban.length ≤ 30 && bban.all (fun c => isDigit c || isUpper c) + | _ => false + +/-- The IBAN passes the check. -/ +def valid (s : List Char) : Bool := + wellShaped s && mod97 (s.drop 4 ++ s.take 4) == 1 + +/-- The check digits, 02 to 98, for a country code and a BBAN: 98 less + the remainder of the BBAN, the country code and `00`. `none` when the + country code or the BBAN has the wrong shape. -/ +def checkDigits (country bban : List Char) : Option (List Char) := + if wellShaped (country ++ ['0', '0'] ++ bban) then + let c := 98 - mod97 (bban ++ country ++ ['0', '0']) + some [Char.ofNat (48 + c / 10), Char.ofNat (48 + c % 10)] + else none + +end Codec.Iban diff --git a/Codec/Luhn.lean b/Codec/Luhn.lean new file mode 100644 index 0000000..cf77fd7 --- /dev/null +++ b/Codec/Luhn.lean @@ -0,0 +1,33 @@ +/- + The Luhn check digit (ISO/IEC 7812-1, Annex B; US patent 2,950,048). + + Counting from the right, starting with the check digit, every second + digit is doubled, and 9 is taken off a doubled value above 9. A number + is valid when the sum is a multiple of 10. Digits are numbers 0 to 9, + most significant first. +-/ + +namespace Codec.Luhn + +/-- A digit's share of the sum: as it is, or doubled with 9 taken off a + result above 9. -/ +def weigh (double : Bool) (d : Nat) : Nat := + if double then (if 2 * d > 9 then 2 * d - 9 else 2 * d) else d + +/-- The sum of digits given right to left, the first not doubled. -/ +def sumFromRight : Bool → List Nat → Nat + | _, [] => 0 + | double, d :: rest => weigh double d + sumFromRight (!double) rest + +/-- The Luhn sum of a number. -/ +def sum (ds : List Nat) : Nat := sumFromRight false ds.reverse + +/-- Every digit is 0 to 9 and the Luhn sum is a multiple of 10. -/ +def valid (ds : List Nat) : Bool := + ds.all (· ≤ 9) && sum ds % 10 == 0 + +/-- The digit to put after a payload so that the whole is valid. -/ +def checkDigit (ds : List Nat) : Nat := + (10 - sum (ds ++ [0]) % 10) % 10 + +end Codec.Luhn diff --git a/Main.lean b/Main.lean index a9b2b13..b0dad40 100644 --- a/Main.lean +++ b/Main.lean @@ -20,13 +20,23 @@ pemdec 45,45,... prints ok:88;0, the label's character codes and the data (or none) + luhn 7,9,9,2,7,3 prints true or false: whether the digits pass + the Luhn check + luhncheck 7,9,9,2 prints the Luhn check digit for the digits + (error when a number is above 9) + iban 71,66,50,57,... prints true or false: whether the text, given as + character codes, passes the IBAN check + ibancheck 71,66;78,87 prints ok: and the character codes of the two + check digits for a country code and a + BBAN (or none) + `pemenc` takes two lists, the label's character codes and the bytes, separated by `;`. PEM text holds line ends, so it goes in and out as character codes. A request is an operation, then optionally one space and its numbers; - with no numbers after the space, the input is empty. `pemenc` is the - exception: it needs its one space and one `;`. A malformed + with no numbers after the space, the input is empty. `pemenc` and + `ibancheck` are the exceptions: each needs its one space and one `;`. A malformed request prints `error`: any other line, an unknown operation, a number that is not plain decimal digits, a byte above 255, or a character code that is not a Unicode scalar value. A line may end in LF or @@ -75,6 +85,17 @@ def pemEncode (arg : String) : Option String := | none => "none" | _ => none +/-- `ibancheck`: the country code's character codes, `;`, and the BBAN's. -/ +def ibanCheck (arg : String) : Option String := + match arg.splitOn ";" with + | [c, b] => do + let country ← toChars (← numbers c) + let bban ← toChars (← numbers b) + return match Iban.checkDigits country bban with + | some ck => "ok:" ++ showChars ck + | none => "none" + | _ => none + /-- The answer to one request, or `none` when the request is malformed. -/ def answer (op : String) (ns : List Nat) : Option String := do let result : Option (List UInt8) → String @@ -90,6 +111,9 @@ def answer (op : String) (ns : List Nat) : Option String := do | "unframe" => return result (Crc32.unframe (← toBytes ns)) | "pctenc" => return String.ofList (Percent.encode (← toBytes ns)) | "pctdec" => return result (Percent.decode (← toChars ns)) + | "luhn" => return toString (Luhn.valid ns) + | "luhncheck" => if ns.all (· ≤ 9) then return toString (Luhn.checkDigit ns) else none + | "iban" => return toString (Iban.valid (← toChars ns)) | "pemdec" => return match Pem.decode (← toChars ns) with | some (label, data) => "ok:" ++ showChars label ++ ";" ++ showBytes data @@ -102,6 +126,8 @@ def request (line : String) : Option String := match line.splitOn " " with | ["pemenc", arg] => pemEncode arg | ["pemenc"] => none + | ["ibancheck", arg] => ibanCheck arg + | ["ibancheck"] => none | [op] => answer op [] | [op, arg] => numbers arg >>= answer op | _ => none diff --git a/Proofs.lean b/Proofs.lean index 6287cbd..9515cc1 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -7,3 +7,5 @@ import Proofs.Base64 import Proofs.Crc32 import Proofs.Percent import Proofs.Pem +import Proofs.Luhn +import Proofs.Iban diff --git a/Proofs/Iban.lean b/Proofs/Iban.lean new file mode 100644 index 0000000..adabdb6 --- /dev/null +++ b/Proofs/Iban.lean @@ -0,0 +1,44 @@ +/- + Proofs of the Iban statements in `Spec.lean`, under the same names. The + helper lemmas live in `Codec.Proofs.Iban`. +-/ + +import Codec +import Spec.Defs + +open Codec + +namespace Codec.Proofs.Iban + +end Codec.Proofs.Iban + +theorem Spec.iban_valid_iff (s : List Char) : Iban.valid s = true ↔ Spec.IbanValid s := sorry + +theorem Spec.iban_checkDigits_iff (country bban ck : List Char) : + 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) := sorry + +theorem 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)) : + Iban.valid (l ++ b :: r) = false := sorry + +theorem 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)) : + Iban.valid (l ++ b :: a :: r) = false := sorry + +theorem Spec.iban_vectors : + Iban.valid "GB29NWBK60161331926819".toList = true ∧ + Iban.valid "DE89370400440532013000".toList = true ∧ + Iban.valid "FR1420041010050500013M02606".toList = true ∧ + Iban.valid "NO9386011117947".toList = true ∧ + Iban.checkDigits "GB".toList "NWBK60161331926819".toList = some "29".toList ∧ + Iban.checkDigits "NO".toList "86011117947".toList = some "93".toList ∧ + Iban.valid "GB29NWBK60161331926818".toList = false ∧ + Iban.valid "gb29NWBK60161331926819".toList = false ∧ + Iban.valid "FR2130006000010001234B15697".toList = true ∧ + Iban.valid "FR21300060000100012341B5697".toList = true := by + and_intros <;> decide +kernel diff --git a/Proofs/Luhn.lean b/Proofs/Luhn.lean new file mode 100644 index 0000000..9903332 --- /dev/null +++ b/Proofs/Luhn.lean @@ -0,0 +1,201 @@ +/- + Proofs of the Luhn statements in `Spec.lean`, under the same names. The + helper lemmas live in `Codec.Proofs.Luhn`. +-/ + +import Codec +import Spec.Defs + +open Codec + +namespace Codec.Proofs.Luhn + +/-! Facts about single digits, checked by `decide` over `Fin 10` and both + parities, then lifted to `Nat`. -/ + +theorem weigh_zero (p : Bool) : Luhn.weigh p 0 = 0 := by cases p <;> rfl + +theorem weigh_nine (p : Bool) : Luhn.weigh p 9 = 9 := by cases p <;> rfl + +theorem weigh_false (d : Nat) : Luhn.weigh false d = d := rfl + +theorem weigh_le_fin : ∀ p : Bool, ∀ a : Fin 10, Luhn.weigh p a.val ≤ 9 := by decide + +theorem weigh_inj_fin : ∀ p : Bool, ∀ a b : Fin 10, + Luhn.weigh p a.val = Luhn.weigh p b.val → a.val = b.val := by decide + +/-- Swapping two neighbouring digits leaves the sum unchanged modulo 10 + only when they are equal, or 0 and 9. -/ +theorem swap_fin : ∀ p q : Bool, p ≠ q → ∀ a b : Fin 10, + (Luhn.weigh q a.val + Luhn.weigh p b.val) % 10 = + (Luhn.weigh q b.val + Luhn.weigh p a.val) % 10 → + a.val = b.val ∨ (a.val = 0 ∧ b.val = 9) ∨ (a.val = 9 ∧ b.val = 0) := by decide + +theorem weigh_le (p : Bool) (a : Nat) (ha : a ≤ 9) : Luhn.weigh p a ≤ 9 := + weigh_le_fin p ⟨a, by omega⟩ + +theorem weigh_inj (p : Bool) (a b : Nat) (ha : a ≤ 9) (hb : b ≤ 9) + (h : Luhn.weigh p a = Luhn.weigh p b) : a = b := + weigh_inj_fin p ⟨a, by omega⟩ ⟨b, by omega⟩ h + +theorem swap_digits (p q : Bool) (hpq : p ≠ q) (a b : Nat) (ha : a ≤ 9) (hb : b ≤ 9) + (h : (Luhn.weigh q a + Luhn.weigh p b) % 10 = (Luhn.weigh q b + Luhn.weigh p a) % 10) : + a = b ∨ (a = 0 ∧ b = 9) ∨ (a = 9 ∧ b = 0) := + swap_fin p q hpq ⟨a, by omega⟩ ⟨b, by omega⟩ h + +/-! Parities. -/ + +theorem not_parity (k : Nat) : (!decide (k % 2 = 1)) = decide ((k + 1) % 2 = 1) := by + by_cases h : k % 2 = 1 <;> simp [h] <;> omega + +theorem parity_succ_ne (k : Nat) : decide (k % 2 = 1) ≠ decide ((k + 1) % 2 = 1) := by + rw [← not_parity] + cases decide (k % 2 = 1) <;> decide + +/-! The sum, place by place. -/ + +/-- `sumFromRight` from a place of parity `k`, written as the sum over the + places. -/ +theorem sumFromRight_range (k : Nat) (L : List Nat) : + Luhn.sumFromRight (decide (k % 2 = 1)) L = + ((List.range L.length).map fun i => Luhn.weigh (decide ((k + i) % 2 = 1)) (L.getD i 0)).sum := by + induction L generalizing k with + | nil => rfl + | cons y L ih => + rw [Luhn.sumFromRight, not_parity, ih (k + 1), List.length_cons, List.range_succ_eq_map, + List.map_cons, List.map_map, List.sum_cons] + have hf : ((fun i => Luhn.weigh (decide ((k + i) % 2 = 1)) ((y :: L).getD i 0)) ∘ Nat.succ) = + (fun i => Luhn.weigh (decide ((k + 1 + i) % 2 = 1)) (L.getD i 0)) := by + funext i + simp only [Function.comp, Nat.succ_eq_add_one, List.getD_cons_succ] + rw [show k + (i + 1) = k + 1 + i by omega] + 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 + 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] + refine Eq.trans h ?_ + congr 1 + apply List.map_congr_left + intro i _ + simp [Spec.luhnShare, Luhn.weigh] + +/-- Changing one digit, at place `k` from the start of the list, changes + its share only. -/ +theorem sumFromRight_mid (k : Nat) (r l : List Nat) (x : Nat) : + Luhn.sumFromRight (decide (k % 2 = 1)) (r ++ x :: l) = + Luhn.sumFromRight (decide (k % 2 = 1)) (r ++ 0 :: l) + + Luhn.weigh (decide ((k + r.length) % 2 = 1)) x := by + induction r generalizing k with + | nil => + simp only [List.nil_append, Luhn.sumFromRight, weigh_zero, List.length_nil, Nat.add_zero] + omega + | cons y r ih => + simp only [List.cons_append, Luhn.sumFromRight] + rw [not_parity, ih (k + 1), List.length_cons, show k + (r.length + 1) = k + 1 + r.length by omega] + omega + +/-- The normal form: the digit `x` adds its share at place `r.length`. -/ +theorem sum_mid (l r : List Nat) (x : Nat) : + Luhn.sum (l ++ x :: r) = + Luhn.sum (l ++ 0 :: r) + Luhn.weigh (decide (r.length % 2 = 1)) x := by + have h := sumFromRight_mid 0 r.reverse l.reverse x + simp only [Nat.zero_mod, Nat.zero_add, List.length_reverse] at h + simp only [Luhn.sum, List.reverse_append, List.reverse_cons, List.append_assoc, + List.singleton_append] + exact h + +theorem sum_pair (l r : List Nat) (a b : Nat) : + Luhn.sum (l ++ a :: b :: r) = + Luhn.sum (l ++ 0 :: 0 :: r) + Luhn.weigh (decide ((r.length + 1) % 2 = 1)) a + + Luhn.weigh (decide (r.length % 2 = 1)) b := by + have h1 := sum_mid (l ++ [a]) r b + have h2 := sum_mid l (0 :: r) a + simp only [List.append_assoc, List.singleton_append, List.length_cons] at h1 h2 + omega + +theorem valid_eq (ds : List Nat) : + Luhn.valid ds = true ↔ (∀ d ∈ ds, d ≤ 9) ∧ Luhn.sum ds % 10 = 0 := by + simp [Luhn.valid, List.all_eq_true] + +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 + rw [valid_eq, sum_eq_luhnSum] + +theorem 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 + · unfold Luhn.checkDigit + omega + · intro c hc + have hs := sum_mid ds [] c + simp only [List.length_nil, Nat.zero_mod] at hs + rw [valid_eq, hs] + have hall : ∀ d ∈ ds ++ [c], d ≤ 9 := by + intro d hd + simp only [List.mem_append, List.mem_singleton] at hd + rcases hd with hd | hd + · exact h d hd + · omega + unfold Luhn.checkDigit + simp only [weigh_false, Nat.zero_ne_one, decide_false] + constructor + · intro ⟨_, h2⟩ + omega + · intro h2 + exact ⟨hall, by omega⟩ + +theorem 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 + obtain ⟨hall, hs⟩ := h + have ha : a ≤ 9 := hall a (by simp) + cases hv : Luhn.valid (l ++ b :: r) with + | false => rfl + | true => + rw [valid_eq] at hv + obtain ⟨_, hs'⟩ := hv + rw [sum_mid] at hs hs' + have := weigh_le (decide (r.length % 2 = 1)) a ha + have := weigh_le (decide (r.length % 2 = 1)) b hb + 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) + (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 + rw [valid_eq] at h + obtain ⟨hall, hs⟩ := h + have ha : a ≤ 9 := hall a (by simp) + have hb : b ≤ 9 := hall b (by simp) + cases hv : Luhn.valid (l ++ b :: a :: r) with + | false => rfl + | true => + rw [valid_eq] at hv + obtain ⟨_, hs'⟩ := hv + rw [sum_pair] at hs hs' + 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) : + 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 : + 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 ∧ + Luhn.valid [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] = true ∧ + Luhn.valid [1, 0] = false := by + and_intros <;> decide +kernel diff --git a/README.md b/README.md index 8fe49a1..ca107d3 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ -# codec: hex, base 64, CRC-32, percent-encoding and PEM, proved +# codec: hex, base 64, CRC-32, percent-encoding, PEM and check digits, proved -Five small codecs in Lean, each with machine-checked proofs that it does exactly what its specification says, and tested on a million inputs in all against Python's standard library and, for PEM, against an encoder and strict parser written in the tests from RFC 7468 (see `tests/TEST-RESULTS.md`). Hex is written as Python's `bytes.hex()` writes it, base 64 follows RFC 4648, the CRC-32 is the one in gzip, zip, and PNG, percent-encoding follows RFC 3986, and PEM is the strict form of RFC 7468, the text that wraps certificates and keys. They are also the material for Level 0 of the [Proven Commons academy](https://github.com/Proven-Commons/mission): a first proof, read and then written, on code small enough to hold in your head. +Small codecs and check digits in Lean, each with machine-checked proofs that it does exactly what its specification says, and tested on a million inputs in all against Python's standard library and, for PEM, against an encoder and strict parser written in the tests from RFC 7468 (see `tests/TEST-RESULTS.md`). Hex is written as Python's `bytes.hex()` writes it, base 64 follows RFC 4648, the CRC-32 is the one in gzip, zip, and PNG, percent-encoding follows RFC 3986, PEM is the strict form of RFC 7468, the text that wraps certificates and keys, and the check digits are Luhn's, as on card numbers, and the IBAN's, by ISO 7064 MOD 97-10. The check digits come with what each catches and, as theorems too, what each misses. They are also the material for Level 0 of the [Proven Commons academy](https://github.com/Proven-Commons/mission): a first proof, read and then written, on code small enough to hold in your head. Status: in progress. The specification has not yet been approved by a reviewer apart from its author, so this is not verified. @@ -32,6 +32,13 @@ The statements are in `Spec.lean`, the definitions they use in `Spec/Defs.lean`, | 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 the check digit is the one digit that makes a number 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` | +| Luhn's blind spot: swapping an adjacent 0 and 9 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` | The command-line tool in `Main.lean` calls these functions directly. @@ -44,6 +51,8 @@ The command-line tool in `Main.lean` calls these functions directly. - Percent-encoding with another set of characters left as they are, such as the `+` for a space of HTML forms or the wider sets of JavaScript's `encodeURIComponent`. Which characters a URI component allows, and whether text is decoded at the right layer, are for a URI parser. This codec decodes what it is given, once, and does not check that it is URI text: it reads any US-ASCII character but `%` as itself, and reads `%00` as a NUL byte. Section 7.3 of RFC 3986 says `%00` should be rejected where an application does not expect raw data in a component; that check is the caller's. - PEM in any form but the strict one. The standard and lax forms of RFC 7468 (Figures 1 and 2), which allow blanks, empty lines, and other line lengths, are refused, as are the headers of older PEM (RFC 1421), text around the message, and a file of several messages. Which label goes with which kind of data, and what that data means, is for the caller: a label is any text the `label` rule allows. - Two points where this codec departs from the strict form. The strict form has no text for empty data, since its last line of base 64 needs four characters. Here empty data is the BEGIN and END lines alone, as Go's `encoding/pem` and Python's `ssl` write it. With LF line ends, only the lax form of RFC 7468 (Figure 2) allows that text; the text the standard form (Figure 1) gives empty data, with one empty line between BEGIN and END, is refused. And the strict form allows a last group whose unused bits are not zero, which this codec's strict base 64 refuses. +- The IBAN registry. The check is the shape and the mod-97 sum only: each country's BBAN length and format, in the SWIFT IBAN Registry, are not checked, and nor is whether the country code is one. An IBAN with spaces or lower-case letters, which many tools tidy first, is refused. Check digits 00, 01 and 99 never come from the computation, which gives 02 to 98, but an IBAN with them can still pass the check, as 01 and 98 are the same mod 97. +- Luhn on an empty number, which passes, since its sum is 0. Each digit is a number 0 to 9; there is no text form with spaces or dashes. - Hex with spaces, line breaks, or a `0x` prefix, which decoding rejects. Hex is RFC 4648 base 16 up to case: it writes lowercase, as Python does, where the RFC's alphabet is uppercase. - Other checksums, such as CRC-32C. A frame is this library's own layout, a message and its CRC-32, not a gzip or zip file. @@ -61,7 +70,9 @@ This project has no dependencies beyond Lean itself. ## Other decoders -`tests/CROSS-CHECK.md` records a one-off comparison of the percent-decoder with Go's `net/url.PathUnescape`, and of PEM with Go's `encoding/pem`. It is not part of the verified bar. On every text in US-ASCII that the tests give the decoder, Go gives the same answer, bad escapes included. Go reads a character outside US-ASCII as its UTF-8 bytes, where this decoder refuses it. +`tests/CROSS-CHECK.md` records a one-off comparison of the percent-decoder with Go's `net/url.PathUnescape`, of PEM with Go's `encoding/pem`, and of the check digits with python-stdnum. It is not part of the verified bar. On every text in US-ASCII that the tests give the decoder, Go gives the same answer, bad escapes included. Go reads a character outside US-ASCII as its UTF-8 bytes, where this decoder refuses it. + +For the check digits, python-stdnum 2.2 gives the same answers on every Luhn and IBAN request the tests make, apart from the empty Luhn number, which it refuses, IBAN text it tidies first, and IBANs its registry check refuses. For PEM, Go writes the same text for every label the RFC's `label` rule allows, empty data included; it also writes labels the rule refuses. Go reads PEM laxly: it skips text around a block and takes headers and blanks, which this decoder refuses. And it ends lines at LF only, so it refuses most text with a CR alone as a line end, which RFC 7468 allows and this decoder reads. Go also refuses a message with empty data whose label holds a `:`, such as `-----BEGIN A:B-----` then `-----END A:B-----`, which Go itself writes: it takes the END line for an RFC 1421 header. Apart from those, on every text the cross-check gives this decoder and it accepts, Go reads the same label and data. @@ -79,7 +90,7 @@ python3 tests/run_tests.py ## Layout -- `Codec/Hex.lean`, `Codec/Base64.lean`, `Codec/Crc32.lean`, `Codec/Percent.lean`, `Codec/Pem.lean`: the code under proof. +- `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. @@ -89,4 +100,4 @@ python3 tests/run_tests.py - `bar.toml`: the record for the bar check: status, authors, approvals, and where things are. - `SPEC.md`: the specification in plain words. - `tests/run_tests.py`: the differential tests. -- `tests/cross_check.py` and `tests/cross_check/`: the one-off comparison with Go. +- `tests/cross_check.py` and `tests/cross_check/`: the one-off comparison with Go and python-stdnum. diff --git a/SPEC.md b/SPEC.md index 1007653..a42d9ab 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. 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 `Spec.lean`, `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. @@ -48,9 +48,26 @@ Scope: RFC 7468, the textual encoding of PKIX, PKCS, and CMS structures, in its The strict form has no text for empty data, since its last line of base 64 needs four characters. Here empty data is the BEGIN and END lines with nothing between, as Go's `encoding/pem` and Python's `ssl.DER_cert_to_PEM_cert` write it. With LF line ends, only the lax form (Figure 2) allows that text; the text the standard form (Figure 1) gives empty data, with one empty line between BEGIN and END, is refused. +## Luhn + +Scope: the check digit of ISO/IEC 7812-1, Annex B, from H. P. Luhn's US patent 2,950,048. Numbers are lists of digits 0 to 9, most significant first. + +- `valid` holds when every digit is 0 to 9 and the Luhn sum is a multiple of 10. The sum counts from the right, starting with the check digit: every second digit is doubled, and 9 is taken off a doubled digit above 9. The empty number passes, since its sum is 0. +- `checkDigit` gives the digit to put after a payload so that the whole is valid; it is the only such digit. +- What the check catches is a theorem: any one digit typed wrong, and any two adjacent different digits typed in the wrong order, except 0 and 9. That exception is a theorem too. + +## IBAN + +Scope: the check digits of ISO 13616-1, by ISO 7064 MOD 97-10, on the electronic form: a country code of two upper-case letters, two check digits, and a BBAN of 1 to 30 upper-case letters and digits. + +- `valid` holds when the text has that shape and, with its first four characters moved to the end and each letter written as A = 10 to Z = 35, the digits read as one number leave 1 when divided by 97. +- `checkDigits` gives, for a country code and a BBAN of the right shape, the two digits from 02 to 98 that make the IBAN pass: 98 less the remainder of the BBAN, the country code and `00`. There is never more than one, and it fails on the wrong shape. +- What the check catches is a theorem: one digit typed for another or one letter for another, and two adjacent digits or two adjacent letters typed in the wrong order. Where the rearrangement splits an adjacent pair, the 4th and 5th characters, the swap is still caught, since 10 has order 96 mod 97. A letter and a digit swapped need not be caught: B is 11, so `4B1` and `41B` both read as `4111`, and a proved vector gives two IBANs that pass and differ only so. +- Not checked: each country's BBAN format and length, in the SWIFT IBAN Registry, and whether the country code is one. Check digits 00, 01 and 99 never come from the computation, but an IBAN with them can pass the check. + ## Valid inputs and errors -Every encoder input, except a PEM label that the `label` rule refuses, and every `crc32` and `frame` input is valid. The decoders and `unframe` return `none` for anything they do not accept, and PEM encoding returns `none` for such a label. No function can fail any other way. +Every encoder input, except a PEM label that the `label` rule refuses, and every `crc32` and `frame` input is valid. The decoders and `unframe` return `none` for anything they do not accept, PEM encoding returns `none` for such a label, and `Iban.checkDigits` returns `none` for a country code or BBAN of the wrong shape. No function can fail any other way. The command-line tool in `Main.lean` reads one request per line and prints one answer per line. A request is an operation, then optionally one space and its comma-separated numbers; with no numbers after the space, the input is empty. `pemenc` is the exception: after its one space come the label's character codes, `;`, and the bytes, each list possibly empty, and it answers `ok:` and the character codes of the PEM text, or `none`. `pemdec` answers `ok:`, the label's character codes, `;`, and the bytes, or `none`. The tool prints `error` for any other line, including `pemenc` without its space or its `;`, an unknown operation, a number that is not plain decimal digits, a byte above 255, or a character code that is not a Unicode scalar value. A line may end in LF or CR LF; nothing else around a request is ignored. @@ -82,9 +99,20 @@ Each property is a theorem in `Spec.lean`, under the name given. The definitions | 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. 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. A function that did nothing, or that accepted too much, would fail at least one of them. +Together these fix every output. 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. A function that did nothing, or that accepted too much, would fail at least one of them. ## Oracle diff --git a/Spec.lean b/Spec.lean index 230e314..0e9897d 100644 --- a/Spec.lean +++ b/Spec.lean @@ -236,3 +236,82 @@ theorem Spec.pem_vectors : Pem.decode "-----BEGIN X-----\nAB==\n-----END X-----\n".toList = none ∧ Pem.decode ("-----BEGIN X-----\nAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAAA\nAAAAAAAA\n".toList ++ "-----END X-----\n".toList) = none := sorry + +/-! ## Luhn -/ + +/-- `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 + +/-- 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) : + 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) + (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) + (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) : + 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 : + 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 ∧ + Luhn.valid [4, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1] = true ∧ + Luhn.valid [1, 0] = false := sorry + +/-! ## 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 + +/-- `checkDigits` gives exactly the two digits from 02 to 98 that make + the IBAN pass the check; there is never more than one. -/ +theorem Spec.iban_checkDigits_iff (country bban ck : List Char) : + 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) := sorry + +/-- One digit typed for another, or one letter for another, is caught. -/ +theorem 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)) : + 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) + (h : Iban.valid (l ++ a :: b :: r) = true) (hab : a ≠ b) + (hkind : (Spec.ibanDigit a ∧ Spec.ibanDigit b) ∨ (Spec.ibanLetter a ∧ 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 : + Iban.valid "GB29NWBK60161331926819".toList = true ∧ + Iban.valid "DE89370400440532013000".toList = true ∧ + Iban.valid "FR1420041010050500013M02606".toList = true ∧ + Iban.valid "NO9386011117947".toList = true ∧ + Iban.checkDigits "GB".toList "NWBK60161331926819".toList = some "29".toList ∧ + Iban.checkDigits "NO".toList "86011117947".toList = some "93".toList ∧ + Iban.valid "GB29NWBK60161331926818".toList = false ∧ + Iban.valid "gb29NWBK60161331926819".toList = false ∧ + Iban.valid "FR2130006000010001234B15697".toList = true ∧ + Iban.valid "FR21300060000100012341B5697".toList = true := sorry diff --git a/Spec/Defs.lean b/Spec/Defs.lean index 7325ffd..7b0d3f8 100644 --- a/Spec/Defs.lean +++ b/Spec/Defs.lean @@ -289,3 +289,74 @@ def Spec.figure15 : List UInt8 := [ 0xB4, 0x95, 0x8F, 0x2F, 0xBC, 0x9D, 0x94, 0x4F, 0xB9, 0x50, 0x6E, 0x14, 0x36, 0x49, 0xF7, 0x12, 0x8B, 0x3C, 0x12, 0x26, 0x41, 0xCA, 0x2F, 0x43, 0x56, 0xCC, 0x9F, 0xCB, 0xD7, 0x9E, 0x8E, 0x1F, 0xBC, 0x01, 0x78, 0x29] + +/-! ## Luhn + +The check digit of ISO/IEC 7812-1, Annex B, from H. P. Luhn's US patent +2,950,048: counting from the right, starting with the check digit, every +second digit is doubled, and when a doubled digit is above 9, 9 is taken +off it (the same as adding its two digits). The number is valid when the +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 := + 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 + +-- 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 + +/-! ## IBAN + +ISO 13616-1, with the check digits of ISO 7064 MOD 97-10. In its +electronic form an IBAN is a country code of two letters, two check +digits, and a BBAN of up to 30 letters and digits, letters in upper +case. To check it, the first four characters move to the end, each +letter is replaced by its number, A = 10 to Z = 35, and the digits are +read as one number, which must leave 1 when divided by 97. Check digits +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 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 := + 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] + +/-- The number decimal digits write, most significant first. -/ +def 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) + +/-- Two letters, two digits, then a BBAN of 1 to 30 letters and digits. -/ +def 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 + +/-- 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 + +-- The letters become 10 to 35, and "WEST" becomes 32 14 28 29. +example : ("AZWEST".toList.flatMap Spec.ibanDigits) = + [1, 0, 3, 5, 3, 2, 1, 4, 2, 8, 2, 9] := by decide diff --git a/bar.toml b/bar.toml index a1584b2..5f3405f 100644 --- a/bar.toml +++ b/bar.toml @@ -21,6 +21,8 @@ code = [ "Codec.Crc32.crc32", "Codec.Crc32.frame", "Codec.Crc32.unframe", "Codec.Percent.encode", "Codec.Percent.decode", "Codec.Pem.encode", "Codec.Pem.decode", + "Codec.Luhn.valid", "Codec.Luhn.checkDigit", + "Codec.Iban.valid", "Codec.Iban.checkDigits", ] # One entry per approval, added in a pull request the reviewer approves. diff --git a/comparator.json b/comparator.json index 214a339..bd48adc 100644 --- a/comparator.json +++ b/comparator.json @@ -27,7 +27,18 @@ "Spec.pem_encode_iff", "Spec.pem_decode_iff", "Spec.pem_decode_encode", - "Spec.pem_vectors" + "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" ], "permitted_axioms": [ "propext", diff --git a/tests/CROSS-CHECK.md b/tests/CROSS-CHECK.md index 0cc33f9..419845f 100644 --- a/tests/CROSS-CHECK.md +++ b/tests/CROSS-CHECK.md @@ -3,15 +3,22 @@ Written by `tests/cross_check.py`, once, by hand. It is not part of the verified bar. - Seed: 20261024 -- Texts given to the percent-decoder: 254047, of which 217736 it accepts +- Texts given to the percent-decoder: 194412, of which 166412 it accepts - Go: `net/url.PathUnescape`, go version go1.24.7 linux/amd64 -- Texts in US-ASCII: 235889, differences: 0 -- Texts with a character outside US-ASCII: 18158, of which this decoder accepts 0. Go reads such a character as its UTF-8 bytes, and gives the same answer on 4877 of them (where it finds a bad escape too) and a different one on 13281. +- Texts in US-ASCII: 180340, differences: 0 +- Texts with a character outside US-ASCII: 14072, of which this decoder accepts 0. Go reads such a character as its UTF-8 bytes, and gives the same answer on 3917 of them (where it finds a bad escape too) and a different one on 10155. ## PEM - Go: `encoding/pem`, go version go1.24.7 linux/amd64 -- Encoding requests: 51015. The same text from both: 43123. Go writes a label this encoder refuses: 7892. Other differences: 0. -- Decoding requests: 86226. The same answer from both, with nothing left over in Go: 51362. Go reads text this decoder refuses: 4794. This decoder accepts text with a CR alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines at LF only: 29531. This decoder reads empty data under a label with a `:`, and Go takes the END line for a header: 539. Other differences, where this decoder accepts text that Go reads differently or not at all: 0. +- Encoding requests: 39088. The same text from both: 33035. Go writes a label this encoder refuses: 6053. Other differences: 0. +- Decoding requests: 66050. The same answer from both, with nothing left over in Go: 39312. Go reads text this decoder refuses: 3619. This decoder accepts text with a CR alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines at LF only: 22677. This decoder reads empty data under a label with a `:`, and Go takes the END line for a header: 442. Other differences, where this decoder accepts text that Go reads differently or not at all: 0. + + +## Luhn and IBAN + +- python-stdnum 2.2: `luhn.is_valid`, `luhn.calc_check_digit`, `iban.calc_check_digits`, and `iso7064.mod_97_10.is_valid` for the IBAN check +- Requests: 234856. The same answer: 234855. An empty Luhn number, which this codec passes and stdnum refuses: 1. IBAN text with a space, a dash, a dot or a lower-case letter, which stdnum removes or upper-cases first and this codec refuses: 0. Other differences: 0. +- The same IBANs given to stdnum's whole `iban.validate`: the same answer on 38564. It refuses, for a country code or BBAN format not in the SWIFT registry, 38983 that pass this codec's check, which does not use the registry. Read after stdnum's normalizing: 2. Other differences: 0. diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 1df57e8..1ec35e4 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -6,9 +6,9 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261024 - Inputs: 1000000 -- Mutated: 245733 of the inputs are mutated encodings or frames -- By operation: b64dec 101405, b64enc 50695, crc 50697, error 77, frame 50695, hexdec 152103, hexenc 50699, pctdec 254047, pctenc 50951, pemdec 86226, pemenc 51015, unframe 101390 -- Malformed requests answered `error`: 77 of 77 +- Mutated: 265473 of the inputs are mutated encodings or frames +- By operation: b64dec 77551, b64enc 38769, crc 38770, error 82, frame 38768, hexdec 116322, hexenc 38772, iban 77549, ibancheck 38781, luhn 78647, luhncheck 39879, pctdec 194412, pctenc 39024, pemdec 66050, pemenc 39088, unframe 77536 +- Malformed requests answered `error`: 82 of 82 - Last lines with no LF, sent alone, answered right: 6 of 6 -- Strict base 64 rejections where Python decodes: 9024 (9024 with unused bits before the padding not zero, 0 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) +- Strict base 64 rejections where Python decodes: 7102 (7102 with unused bits before the padding not zero, 0 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) - Failures: 0 diff --git a/tests/cross_check.py b/tests/cross_check.py index f434ad0..22f0d1b 100644 --- a/tests/cross_check.py +++ b/tests/cross_check.py @@ -1,5 +1,6 @@ #!/usr/bin/env python3 -"""A one-off comparison of the percent-decoder and of PEM with Go's. +"""A one-off comparison of the percent-decoder and of PEM with Go's, and +of the check digits with python-stdnum. Unlike tests/run_tests.py, this is not part of the verified bar and is not run in CI. It needs Go: @@ -21,6 +22,17 @@ sorted by kind, and only text this decoder accepts and Go reads differently, or not at all, counts against it. The counts go to tests/CROSS-CHECK.md. + +Last, each Luhn and IBAN request goes to python-stdnum 2.2, installed +into .lake/oracle-packages if it is not there: `luhn.is_valid` and +`luhn.calc_check_digit`, `iban.calc_check_digits`, and for the IBAN +check `iso7064.mod_97_10.is_valid` on the rearranged text, with the +shape checked as this codec does. Then each IBAN goes to `iban.validate` +too, which also checks each country's BBAN format in the SWIFT +registry, as this codec does not: those refusals are counted on their +own, as are the IBANs stdnum reads after removing spaces and dashes and +upper-casing, and the empty Luhn number, which stdnum refuses. +(stdnum removes spaces, dashes and dots.) """ import argparse @@ -39,6 +51,101 @@ BUILD = ROOT / ".lake" / "cross_check" +def stdnum(): + """python-stdnum 2.2, from .lake/oracle-packages, installed there if + needed.""" + target = ROOT / ".lake" / "oracle-packages" + sys.path.insert(0, str(target)) + try: + import stdnum as module + except ImportError: + subprocess.run([sys.executable, "-m", "pip", "install", "--quiet", "--target", str(target), + "python-stdnum==2.2"], check=True) + import stdnum as module + if module.__version__ != "2.2": + sys.exit(f"python-stdnum {module.__version__} found, 2.2 wanted") + return module + + +def check_digit_section(args): + stdnum() + from stdnum import iban, luhn + from stdnum.iso7064 import mod_97_10 + items = [(label, req) for label, req, _, _, _ in run_tests.cases(args.seed, args.count) + if label in ("luhn", "luhncheck", "iban", "ibancheck")] + ours, problem = run_tests.run_tool("".join(req + "\n" for _, req in items)) + if problem or len(ours) != len(items): + sys.exit(f"the tool failed: {problem}") + + def theirs(label, req): + arg = req.split(" ", 1)[1] if " " in req else "" + if label == "luhn": + return str(luhn.is_valid("".join(str(int(n)) for n in arg.split(",") if n))).lower() + if label == "luhncheck": + return luhn.calc_check_digit("".join(str(int(n)) for n in arg.split(",") if n)) + if label == "iban": + text = "".join(map(chr, run_tests_nums(req))) + return str(bool(run_tests.IBAN_SHAPE.fullmatch(text)) + and mod_97_10.is_valid(text[4:] + text[:4])).lower() + country, bban = (bytes(int(n) for n in part.split(",") if n).decode() for part in arg.split(";")) + try: + return "ok:" + run_tests.text_nums(iban.calc_check_digits(country + "00" + bban)) + except Exception: + return "none" + + counts = {"same": 0, "empty": 0, "normalized": 0, "other": []} + for (label, req), o in zip(items, ours): + t = theirs(label, req) + arg = req.split(" ", 1)[1] if " " in req else "" + if o == t: + counts["same"] += 1 + elif label == "luhn" and arg == "": + counts["empty"] += 1 + elif label in ("iban", "ibancheck") and any(chr(n) in " -." or 97 <= n <= 122 + for n in run_tests_nums(req.replace(";", ","))): + counts["normalized"] += 1 + else: + counts["other"].append((req, o, t)) + # The whole of stdnum's IBAN check, with the SWIFT registry. + full = {"same": 0, "registry": 0, "normalized": 0, "other": []} + for (label, req), o in zip(items, ours): + if label != "iban": + continue + text = "".join(map(chr, run_tests_nums(req))) + try: + iban.validate(text) + t, why = "true", None + except Exception as e: + t, why = "false", type(e).__name__ + if o == t: + full["same"] += 1 + elif o == "true" and why in ("InvalidComponent", "InvalidFormat", "InvalidLength"): + full["registry"] += 1 + elif any(c in " -." or c.islower() for c in text): + full["normalized"] += 1 + else: + full["other"].append((req, o, t)) + lines = [ + "", + "## Luhn and IBAN", + "", + "- python-stdnum 2.2: `luhn.is_valid`, `luhn.calc_check_digit`, " + "`iban.calc_check_digits`, and `iso7064.mod_97_10.is_valid` for the IBAN check", + f"- Requests: {len(items)}. The same answer: {counts['same']}. An empty Luhn number, " + f"which this codec passes and stdnum refuses: {counts['empty']}. IBAN text with a space, " + f"a dash, a dot or a lower-case letter, which stdnum removes or upper-cases first and this codec " + f"refuses: {counts['normalized']}. Other differences: {len(counts['other'])}.", + f"- The same IBANs given to stdnum's whole `iban.validate`: the same answer on " + f"{full['same']}. It refuses, for a country code or BBAN format not in the SWIFT registry, " + f"{full['registry']} that pass this codec's check, which does not use the registry. Read " + f"after stdnum's normalizing: {full['normalized']}. Other differences: {len(full['other'])}.", + "", + ] + lines += [f"- `{r[:100]}`: this project `{o}`, stdnum `{t}`" + for r, o, t in (counts["other"] + full["other"])[:10]] + return lines + + def run_tests_nums(req): arg = req.split(" ", 1)[1] if " " in req else "" return [int(n) for n in arg.split(",") if n] @@ -163,6 +270,7 @@ def non_ascii(a): ] lines += [f"- `{a}`: this project `{o}`, Go `{g}`" for a, o, g in ascii_diffs[:10]] lines += pem_section(args, version) + lines += check_digit_section(args) REPORT.write_text("\n".join(lines) + "\n", encoding="utf-8") print(f"{len(reqs)} texts; report in {REPORT}") diff --git a/tests/run_tests.py b/tests/run_tests.py index f5fd769..d9c4cc0 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -4,7 +4,8 @@ The oracles are Python's `binascii.hexlify` and `binascii.unhexlify`, `base64.b64encode` and strict `binascii.a2b_base64`, `zlib.crc32`, and for percent-encoding `urllib.parse.quote` with no safe characters and -`urllib.parse.unquote_to_bytes`; for PEM, `ssl.DER_cert_to_PEM_cert` +`urllib.parse.unquote_to_bytes`; for Luhn and IBAN, the rules written +here, with Python's own integers for the IBAN number mod 97; for PEM, `ssl.DER_cert_to_PEM_cert` for the `CERTIFICATE` label, and for other labels an encoder and a strict 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 @@ -148,6 +149,11 @@ def decoded(result): ("hexdec 48,1114112", "beyond Unicode"), ("pctenc 37,256", "a byte above 255"), ("pctdec 37,55296", "a surrogate, not a character"), + ("luhncheck 1,10", "a number above 9"), + ("ibancheck", "no arguments"), + ("ibancheck 71,66", "no `;`"), + ("ibancheck 71;66;1", "two `;`"), + ("iban 71,55296", "a surrogate, not a character"), ("pemenc", "no arguments"), ("pemenc 88", "no `;` between the label and the data"), ("pemenc 88;1;2", "two `;`"), @@ -333,6 +339,94 @@ def mutate_pem(rng, text): return text[:i] + "\n" + text[i:] +def luhn_sum(ds): + """The Luhn sum: from the right, every second digit doubled, less 9 + when the double is above 9.""" + total = 0 + for i, d in enumerate(reversed(ds)): + if i % 2 == 1: + d = 2 * d - 9 if 2 * d > 9 else 2 * d + total += d + return total + + +def oracle_luhn(ds): + return str(all(d <= 9 for d in ds) and luhn_sum(ds) % 10 == 0).lower() + + +def oracle_luhn_check(ds): + return str((10 - luhn_sum(ds + [0]) % 10) % 10) + + +IBAN_SHAPE = re.compile(r"[A-Z]{2}[0-9]{2}[A-Z0-9]{1,30}") +# Example IBANs, for the SWIFT IBAN Registry's countries among them. +IBAN_EXAMPLES = ["GB29NWBK60161331926819", "DE89370400440532013000", "FR1420041010050500013M02606", + "NO9386011117947", "MT84MALT011000012345MTLCAST001S", "NL91ABNA0417164300", + "BE68539007547034", "CH9300762011623852957", "ES9121000418450200051332", + "IT60X0542811101000000123456", "LC55HEMM000100010012001200023015", + "FR2130006000010001234B15697", "FR21300060000100012341B5697"] + + +def iban_number(text): + return int("".join(str(int(c, 36)) for c in text)) + + +def oracle_iban(text): + ok = bool(IBAN_SHAPE.fullmatch(text)) and iban_number(text[4:] + text[:4]) % 97 == 1 + return str(ok).lower() + + +def oracle_iban_check(country, bban): + if not IBAN_SHAPE.fullmatch(country + "00" + bban): + return "none" + return "ok:" + text_nums(f"{98 - iban_number(bban + country + '00') % 97:02d}") + + +IBAN_CHARS = "ABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789" +IBAN_POOL = IBAN_CHARS + "az -.\xe9" + + +def random_iban(rng): + country = "".join(rng.choice(IBAN_CHARS[:26]) for _ in range(2)) + bban = "".join(rng.choice(rng.choice([IBAN_CHARS, IBAN_CHARS[26:]])) + for _ in range(rng.randint(1, 30))) + check = f"{98 - iban_number(bban + country + '00') % 97:02d}" + return country, bban, country + check + bban + + +def mutate_iban(rng, text): + kind = rng.randrange(6) + i = rng.randrange(len(text)) + if kind == 0: + # A character of the same kind in its place. + pool = IBAN_CHARS[26:] if text[i].isdigit() else IBAN_CHARS[:26] + return text[:i] + rng.choice(pool) + text[i + 1:] + if kind == 1 and len(text) > 1: + j = rng.randrange(len(text) - 1) + return text[:j] + text[j + 1] + text[j] + text[j + 2:] + if kind == 2: + return text[:i] + rng.choice(IBAN_POOL) + text[i + 1:] + if kind == 3: + return text[:i] + text[i + 1:] + if kind == 4: + return text[:i] + rng.choice(IBAN_POOL) + text[i:] + return text.lower() if rng.random() < 0.5 else text + rng.choice(IBAN_CHARS) + + +def mutate_digits(rng, ds): + out = list(ds) + kind = rng.randrange(3) + if kind == 0 and out: + i = rng.randrange(len(out)) + out[i] = rng.randrange(10) + elif kind == 1 and len(out) > 1: + i = rng.randrange(len(out) - 1) + out[i], out[i + 1] = out[i + 1], out[i] + else: + out.insert(rng.randint(0, len(out)), rng.randrange(10)) + return out + + def oracle_unframe(fr): if len(fr) < 4: return None @@ -422,6 +516,16 @@ def fixed_cases(): # encoder's and the decoder's per-character rules. for b in range(256): items.append(("pctenc", f"pctenc {b}", oracle_pctenc(bytes([b])), None, False)) + # Luhn: every number of up to three digits; IBAN: the examples. + for n in range(4): + for ds in itertools.product(range(10), repeat=n): + ds = list(ds) + items.append(("luhn", f"luhn {nums(ds)}", oracle_luhn(ds), None, False)) + items.append(("luhncheck", f"luhncheck {nums(ds)}", oracle_luhn_check(ds), None, False)) + for text in IBAN_EXAMPLES: + items.append(("iban", f"iban {text_nums(text)}", oracle_iban(text), None, False)) + items.append(("ibancheck", f"ibancheck {text_nums(text[:2])};{text_nums(text[4:])}", + oracle_iban_check(text[:2], text[4:]), None, False)) # PEM: every label above with data at the line edges (48 bytes are # one full line), and every bad label. for label in PEM_LABELS + BAD_PEM_LABELS: @@ -487,6 +591,20 @@ def cases(seed, count): batch.append(("pctdec", f"pctdec {text_nums(bad_pct)}", decoded(oracle_pctdec(bad_pct)), None, True)) raw = "".join(rng.choice(PCT_POOL) for _ in range(rng.randrange(8))) batch.append(("pctdec", f"pctdec {text_nums(raw)}", decoded(oracle_pctdec(raw)), None, False)) + ds = [rng.randrange(10) for _ in range(rng.randint(0, 24))] + ds_valid = ds + [int(oracle_luhn_check(ds))] + country, bban, iban = random_iban(rng) + bad_iban = changed(mutate_iban, rng, iban) + bad_ds = changed(mutate_digits, rng, ds_valid) + batch += [ + ("luhncheck", f"luhncheck {nums(ds)}", oracle_luhn_check(ds), None, False), + ("luhn", f"luhn {nums(ds_valid)}", oracle_luhn(ds_valid), None, False), + ("luhn", f"luhn {nums(bad_ds)}", oracle_luhn(bad_ds), None, True), + ("ibancheck", f"ibancheck {text_nums(country)};{text_nums(bban)}", + oracle_iban_check(country, bban), None, False), + ("iban", f"iban {text_nums(iban)}", oracle_iban(iban), None, False), + ("iban", f"iban {text_nums(bad_iban)}", oracle_iban(bad_iban), None, True), + ] label = rng.choice(PEM_LABELS + BAD_PEM_LABELS[:3]) pem_data = data[: rng.choice([0, 1, 47, 48, 49, 96, 97, 200, len(data)])] batch.append(("pemenc", f"pemenc {text_nums(label)};{nums(pem_data)}", @@ -566,7 +684,8 @@ def oracle(): return (f"Python {platform.python_version()} `binascii`, `base64`, `zlib` " f"(zlib {zlib.ZLIB_RUNTIME_VERSION}), `urllib.parse`; for PEM, a strict encoder and " "parser written in tests/run_tests.py from RFC 7468, with `ssl.DER_cert_to_PEM_cert` " - "and `ssl.PEM_cert_to_DER_cert` for the `CERTIFICATE` label") + "and `ssl.PEM_cert_to_DER_cert` for the `CERTIFICATE` label; for Luhn and IBAN, the " + "rules written in tests/run_tests.py, with Python's integers for the IBAN number") def lean_version(): From 31cf549690040ed66881841514de5ec17fb35892 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 07:19:38 +0000 Subject: [PATCH 4/5] Prove the IBAN check digits, and test the shape's edges The IBAN statements are now proved, with no sorry left, and `lake comparator --paranoid` accepts all 37 theorems. Proving iban_checkDigits_iff found a bug: `checkDigits` checked the shape of country ++ "00" ++ bban, so a three-character country code whose third character is a digit passed, its digit read as the first of the check digits. `checkDigits` now requires a country code of two characters, and the statement says so. Planted bugs that the tests missed (digits above 9 in a Luhn number, a BBAN of 31 or of 0 characters, a second country character that is not a letter, BBAN characters not checked) are now caught: the tests add IBANs on the shape's edges whose mod-97 sum passes, so only the shape decides, and Luhn numbers with a value above 9. The cross-check counts the two kinds of request whose stdnum form is a different question. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Codec/Iban.lean | 4 +- Proofs/Iban.lean | 453 +++++++++++++++++++++++++++++++++++++++++- README.md | 2 +- SPEC.md | 2 +- Spec.lean | 5 +- tests/CROSS-CHECK.md | 12 +- tests/TEST-RESULTS.md | 6 +- tests/cross_check.py | 12 +- tests/run_tests.py | 27 ++- 9 files changed, 499 insertions(+), 24 deletions(-) diff --git a/Codec/Iban.lean b/Codec/Iban.lean index 219be5f..aeec2c0 100644 --- a/Codec/Iban.lean +++ b/Codec/Iban.lean @@ -38,9 +38,9 @@ def valid (s : List Char) : Bool := /-- The check digits, 02 to 98, for a country code and a BBAN: 98 less the remainder of the BBAN, the country code and `00`. `none` when the - country code or the BBAN has the wrong shape. -/ + country code is not two letters or the BBAN has the wrong shape. -/ def checkDigits (country bban : List Char) : Option (List Char) := - if wellShaped (country ++ ['0', '0'] ++ bban) then + if country.length = 2 ∧ wellShaped (country ++ ['0', '0'] ++ bban) then let c := 98 - mod97 (bban ++ country ++ ['0', '0']) some [Char.ofNat (48 + c / 10), Char.ofNat (48 + c % 10)] else none diff --git a/Proofs/Iban.lean b/Proofs/Iban.lean index adabdb6..035778d 100644 --- a/Proofs/Iban.lean +++ b/Proofs/Iban.lean @@ -10,25 +10,468 @@ open Codec namespace Codec.Proofs.Iban +/-! ### Characters, through their code points -/ + +theorem isDigit_iff (c : Char) : Iban.isDigit c = true ↔ 48 ≤ c.toNat ∧ c.toNat ≤ 57 := by + simp [Iban.isDigit, Char.le_def, UInt32.le_iff_toNat_le, Char.toNat_val] + +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 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 isDigit_digit (c : Char) : Iban.isDigit c = true ↔ Spec.ibanDigit c := by + rw [isDigit_iff, ibanDigit_iff] + +theorem isUpper_letter (c : Char) : Iban.isUpper c = true ↔ 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 not_digit_of_upper (c : Char) (h : Iban.isUpper c = true) : Iban.isDigit c = false := by + have := (isUpper_iff c).mp h + cases hd : Iban.isDigit c + · rfl + · have := (isDigit_iff c).mp hd; omega + +theorem value_of_digit (c : Char) (h : Iban.isDigit c = true) : Iban.value c = c.toNat - 48 := by + simp [Iban.value, h] + +theorem value_of_not_digit (c : Char) (h : Iban.isDigit c = false) : + Iban.value c = c.toNat - 55 := by + simp [Iban.value, h] + +/-! ### The number a string writes, one character at a time -/ + +/-- The factor a character shifts the number by: 10 for a digit, 100 otherwise. -/ +def pw (c : Char) : Nat := if Iban.isDigit c then 10 else 100 + +def step (n : Nat) (c : Char) : Nat := n * pw c + Iban.value c + +def num (cs : List Char) : Nat := cs.foldl step 0 + +def pws : List Char → Nat + | [] => 1 + | c :: cs => pw c * pws cs + +theorem foldl_step (n : Nat) (cs : List Char) : cs.foldl step n = n * pws cs + num cs := by + induction cs generalizing n with + | nil => simp [num, pws] + | cons c cs ih => + simp only [num, List.foldl_cons] + rw [ih, ih (step 0 c)] + simp only [step, pws, Nat.zero_mul, Nat.zero_add, Nat.add_mul, Nat.mul_assoc, Nat.add_assoc] + +theorem num_append (xs ys : List Char) : num (xs ++ ys) = num xs * pws ys + num ys := by + rw [num, List.foldl_append, foldl_step] + rfl + +theorem num_snoc (xs : List Char) (c : Char) : num (xs ++ [c]) = num xs * pw c + Iban.value c := by + rw [num_append] + simp [num, pws, step] + +theorem num_cons (c : Char) (cs : List Char) : num (c :: cs) = Iban.value c * pws cs + num cs := by + rw [show c :: cs = [c] ++ cs from rfl, num_append] + simp [num, step] + +theorem num_mid (L R : List Char) (c : Char) : + num (L ++ c :: R) = (num L * pw c + Iban.value c) * pws R + num R := by + rw [show L ++ c :: R = (L ++ [c]) ++ R by simp, num_append, num_snoc] + +theorem num_mid2 (L R : List Char) (c d : Char) : + num (L ++ c :: d :: R) = ((num L * pw c + Iban.value c) * pw d + Iban.value d) * pws R + num R := by + rw [show L ++ c :: d :: R = (L ++ [c]) ++ d :: R by simp, num_mid, num_snoc] + +theorem mod97_eq (cs : List Char) : Iban.mod97 cs = num cs % 97 := by + have key : ∀ (n : Nat) (cs : List Char), + cs.foldl (fun r c => if Iban.isDigit c then (r * 10 + Iban.value c) % 97 + else (r * 100 + Iban.value c) % 97) (n % 97) = cs.foldl step n % 97 := by + intro n cs + induction cs generalizing n with + | nil => rfl + | cons c cs ih => + simp only [List.foldl_cons] + rw [← ih] + congr 1 + simp only [step, pw] + split <;> omega + have := key 0 cs + simpa [Iban.mod97, num] using this + +theorem pw_of_digit (c : Char) (h : Iban.isDigit c = true) : pw c = 10 := by + simp [pw, h] + +theorem pw_of_not_digit (c : Char) (h : Iban.isDigit c = false) : pw c = 100 := by + simp [pw, h] + +theorem pws_append (xs ys : List Char) : pws (xs ++ ys) = pws xs * pws ys := by + induction xs with + | nil => simp [pws] + | cons c xs ih => simp only [List.cons_append, pws, ih, Nat.mul_assoc] + +theorem pws_pow (cs : List Char) : ∃ k, pws cs = 10 ^ k ∧ k ≤ 2 * cs.length := by + induction cs with + | nil => exact ⟨0, rfl, by simp⟩ + | cons c cs ih => + obtain ⟨k, hk, hl⟩ := ih + simp only [pws, pw, hk, List.length_cons] + split + · exact ⟨k + 1, by rw [Nat.pow_succ, Nat.mul_comm], by omega⟩ + · exact ⟨k + 2, by rw [Nat.pow_add]; simp [Nat.mul_comm], by omega⟩ + +theorem cancel_pow (k : Nat) : ∀ x y : Nat, (x * 10 ^ k) % 97 = (y * 10 ^ k) % 97 → x % 97 = y % 97 := by + induction k with + | zero => simp + | succ k ih => + intro x y h + have e : ∀ z : Nat, z * 10 ^ (k + 1) = (z * 10) * 10 ^ k := by + intro z + rw [Nat.pow_succ, Nat.mul_comm (10 ^ k) 10, Nat.mul_assoc] + rw [e, e] at h + have := ih _ _ h + omega + +theorem cancel_pws (R : List Char) (x y : Nat) (h : (x * pws R) % 97 = (y * pws R) % 97) : + x % 97 = y % 97 := by + obtain ⟨k, hk, _⟩ := pws_pow R + rw [hk] at h + exact cancel_pow k x y h + +/-- 10 has order 96 mod 97. -/ +theorem pow_ten_ne : ∀ K : Fin 96, 0 < K.val → 10 ^ K.val % 97 ≠ 1 := by decide +kernel + +/-- Two different digits swapped around a factor other than 1 change the remainder. -/ +theorem swap_fin : ∀ u : Fin 97, u.val ≠ 1 → ∀ x y : Fin 10, + (y.val * u.val + x.val) % 97 = (x.val * u.val + y.val) % 97 → x = y := by decide +kernel + +theorem mul_mod_right (x y : Nat) : (x * y) % 97 = (x * (y % 97)) % 97 := by + rw [Nat.mul_mod x (y % 97), Nat.mod_mod, ← Nat.mul_mod] + +/-! ### Shape, rotation, validity -/ + +theorem wellShaped_cons4 (c0 c1 k0 k1 : Char) (bban : List Char) : + Iban.wellShaped (c0 :: c1 :: k0 :: k1 :: bban) = true ↔ + Iban.isUpper c0 = true ∧ Iban.isUpper c1 = true ∧ Iban.isDigit k0 = true ∧ + Iban.isDigit k1 = true ∧ 1 ≤ bban.length ∧ bban.length ≤ 30 ∧ + ∀ c ∈ bban, Iban.isDigit c = true ∨ Iban.isUpper c = true := by + 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 + constructor + · intro hs + match s, hs with + | c0 :: c1 :: k0 :: k1 :: bban, hs => + rw [wellShaped_cons4] at hs + obtain ⟨u0, u1, d0, d1, l1, l2, hb⟩ := hs + exact ⟨c0, c1, k0, k1, bban, rfl, (isUpper_letter c0).mp u0, (isUpper_letter c1).mp u1, + (isDigit_digit k0).mp d0, (isDigit_digit k1).mp d1, l1, l2, + fun c hc => (hb c hc).imp (isDigit_digit c).mp (isUpper_letter c).mp⟩ + | [], hs | [_], hs | [_, _], hs | [_, _, _], hs => simp [Iban.wellShaped] at hs + · rintro ⟨c0, c1, k0, k1, bban, rfl, u0, u1, d0, d1, l1, l2, hb⟩ + rw [wellShaped_cons4] + exact ⟨(isUpper_letter c0).mpr u0, (isUpper_letter c1).mpr u1, + (isDigit_digit k0).mpr d0, (isDigit_digit k1).mpr d1, l1, l2, + fun c hc => (hb c hc).imp (isDigit_digit c).mpr (isUpper_letter c).mpr⟩ + +theorem rot_ok (s : List Char) (hs : Iban.wellShaped s = true) : + ∀ c ∈ s.drop 4 ++ s.take 4, Iban.isDigit c = true ∨ Iban.isUpper c = true := by + match s, hs with + | c0 :: c1 :: k0 :: k1 :: bban, hs => + rw [wellShaped_cons4] at hs + obtain ⟨u0, u1, d0, d1, _, _, hb⟩ := hs + intro c hc + simp only [List.drop_succ_cons, List.drop_zero, List.take_succ_cons, List.take_zero, + List.mem_append, List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with hc | hc | hc | hc | hc + · exact hb c hc + · subst hc; exact Or.inr u0 + · subst hc; exact Or.inr u1 + · subst hc; exact Or.inl d0 + · subst hc; exact Or.inl d1 + | [], 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] + 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)] + simp only [List.foldl_cons, List.foldl_nil] + omega + · have := (isUpper_iff c).mp hc + have hd := not_digit_of_upper c hc + rw [pw_of_not_digit c hd, value_of_not_digit c hd, ite_eq_right (by omega)] + simp only [List.foldl_cons, List.foldl_nil] + omega + +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 + rw [List.foldl_flatMap] + suffices ∀ n, cs.foldl (fun acc x => (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 + | cons c cs ih => + intro n + simp only [List.foldl_cons] + rw [digits_step c (h c (by simp)), ih (fun c hc => h c (by simp [hc]))] + +theorem valid_iff_num (s : List Char) : + Iban.valid s = true ↔ Iban.wellShaped s = true ∧ num (s.drop 4 ++ s.take 4) % 97 = 1 := by + simp [Iban.valid, mod97_eq] + +theorem valid_false (s : List Char) (h : num (s.drop 4 ++ s.take 4) % 97 ≠ 1) : + Iban.valid s = false := by + simp [Iban.valid, mod97_eq, h] + +/-- Moving the first four characters to the end keeps a block that lies + wholly before or wholly after the cut in one piece. -/ +theorem rot_block (l m r : List Char) (h : l.length + m.length ≤ 4 ∨ 4 ≤ l.length) : + ∃ L R : List Char, ∀ m' : List Char, m'.length = m.length → + (l ++ (m' ++ r)).drop 4 ++ (l ++ (m' ++ r)).take 4 = L ++ (m' ++ R) := by + rcases h with h | h + · refine ⟨r.drop (4 - l.length - m.length) ++ l, r.take (4 - l.length - m.length), ?_⟩ + intro m' hm + rw [← List.append_assoc, List.drop_append, List.take_append, + List.drop_eq_nil_of_le (by simp; omega), List.take_of_length_le (by simp; omega)] + simp [hm, Nat.sub_sub] + · refine ⟨l.drop 4, r ++ l.take 4, ?_⟩ + intro m' _ + rw [List.drop_append_of_le_length h, List.take_append_of_le_length h] + simp + +/-- 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)) : + ((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 + have hne : a.toNat ≠ b.toNat := fun h => hab (Char.toNat_inj.mp h) + rcases hkind with ⟨ha, hb⟩ | ⟨ha, hb⟩ + · have da : Iban.isDigit a = true := (isDigit_digit a).mpr ha + have db : Iban.isDigit b = true := (isDigit_digit b).mpr hb + rw [ibanDigit_iff] at ha hb + rw [pw_of_digit a da, pw_of_digit b db, value_of_digit a da, value_of_digit b db] + omega + · have da := not_digit_of_upper a ((isUpper_letter a).mpr ha) + have db := not_digit_of_upper b ((isUpper_letter b).mpr hb) + rw [ibanLetter_iff] at ha hb + rw [pw_of_not_digit a da, pw_of_not_digit b db, value_of_not_digit a da, + value_of_not_digit b db] + omega + +theorem valid_spec (s : List Char) : Iban.valid s = true ↔ Spec.IbanValid s := by + rw [valid_iff_num] + unfold Spec.IbanValid + rw [← shape_iff] + constructor + · rintro ⟨hs, hm⟩ + exact ⟨hs, by rw [ibanNumber_eq _ (rot_ok s hs)]; exact hm⟩ + · rintro ⟨hs, hm⟩ + exact ⟨hs, by rw [ibanNumber_eq _ (rot_ok s hs)] at hm; exact hm⟩ + +/-- The digit characters, as `checkDigits` writes them. -/ +theorem digitChar : ∀ d : Fin 10, Iban.isDigit (Char.ofNat (48 + d.val)) = true ∧ + (Char.ofNat (48 + d.val)).toNat = 48 + d.val := by decide + +theorem digitChar' (d : Nat) (h : d < 10) : Iban.isDigit (Char.ofNat (48 + d)) = true ∧ + (Char.ofNat (48 + d)).toNat = 48 + d := digitChar ⟨d, h⟩ + +theorem num_two (d1 d2 : Char) (h1 : Iban.isDigit d1 = true) (h2 : Iban.isDigit d2 = true) : + num [d1, d2] = Iban.value d1 * 10 + Iban.value d2 ∧ pws [d1, d2] = 100 := by + simp [pws, num, step, pw_of_digit _ h1, pw_of_digit _ h2] + +theorem zz_digit : Iban.isDigit '0' = true := by decide + +/-- `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 + match country, hc with + | [c0, c1], _ => + have h00 : num (bban ++ [c0, c1] ++ ['0', '0']) = num (bban ++ [c0, c1]) * 100 := by + rw [num_append, (num_two '0' '0' zz_digit zz_digit).2, (num_two '0' '0' zz_digit zz_digit).1] + simp [value_of_digit _ zz_digit] + have hrot : ∀ d1 d2 : Char, (c0 :: c1 :: d1 :: d2 :: bban).drop 4 ++ + (c0 :: c1 :: d1 :: d2 :: bban).take 4 = (bban ++ [c0, c1]) ++ [d1, d2] := by + intro d1 d2; simp + have hsh : ∀ d1 d2 : Char, Iban.isDigit d1 = true → Iban.isDigit d2 = true → + Iban.wellShaped (c0 :: c1 :: d1 :: d2 :: bban) = Iban.wellShaped (c0 :: c1 :: '0' :: '0' :: bban) := by + intro d1 d2 h1 h2 + apply Bool.eq_iff_iff.mpr + rw [wellShaped_cons4, wellShaped_cons4] + simp [h1, h2, zz_digit] + unfold Iban.checkDigits + rw [mod97_eq, h00] + constructor + · intro h + split at h + · rename_i hw' + have hw := hw'.2 + injection h with h + subst h + have hq : (98 - num (bban ++ [c0, c1]) * 100 % 97) / 10 < 10 := by omega + have ht : (98 - num (bban ++ [c0, c1]) * 100 % 97) % 10 < 10 := by omega + obtain ⟨dq, tq⟩ := digitChar' _ hq + obtain ⟨dt, tt⟩ := digitChar' _ ht + have hok : ∀ c ∈ [Char.ofNat (48 + (98 - num (bban ++ [c0, c1]) * 100 % 97) / 10), + Char.ofNat (48 + (98 - num (bban ++ [c0, c1]) * 100 % 97) % 10)], + Iban.isDigit c = true := by + intro c hc + simp only [List.mem_cons, List.not_mem_nil, or_false] at hc + rcases hc with rfl | rfl + · 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), + 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, + value_of_digit _ dt, tq, tt] + omega + refine ⟨rfl, fun c hc => (isDigit_digit c).mp (hok c hc), by omega, by omega, ?_⟩ + rw [← valid_spec, valid_iff_num] + refine ⟨?_, ?_⟩ + · rw [show [c0, c1] ++ _ ++ bban = c0 :: c1 :: _ :: _ :: bban from rfl, hsh _ _ dq dt] + exact hw + · rw [show [c0, c1] ++ _ ++ bban = c0 :: c1 :: _ :: _ :: bban from rfl, hrot, + num_append, n2, p2, value_of_digit _ dq, value_of_digit _ dt, tq, tt] + omega + · cases h + · rintro ⟨hl, hd, h2, h98, hv⟩ + match ck, hl with + | [d1, d2], _ => + have e1 := (isDigit_digit d1).mpr (hd d1 (by simp)) + have e2 := (isDigit_digit d2).mpr (hd d2 (by simp)) + rw [← valid_spec, valid_iff_num, + show [c0, c1] ++ [d1, d2] ++ bban = c0 :: c1 :: d1 :: d2 :: bban from rfl, + hsh _ _ e1 e2, hrot, num_append] at hv + obtain ⟨hw, hm⟩ := hv + obtain ⟨n2, p2⟩ := num_two _ _ e1 e2 + rw [n2, p2] at hm + rw [ibanNumber_eq _ (by simp [e1, e2]), n2] at h2 h98 + have v1 := value_of_digit _ e1 + have v2 := value_of_digit _ e2 + have b1 := (isDigit_iff d1).mp e1 + have b2 := (isDigit_iff d2).mp e2 + have hc : 98 - num (bban ++ [c0, c1]) * 100 % 97 = Iban.value d1 * 10 + Iban.value d2 := by + omega + rw [ite_eq_left (show [c0, c1].length = 2 ∧ Iban.wellShaped ([c0, c1] ++ ['0', '0'] ++ bban) = true + from ⟨rfl, hw⟩), hc] + have q1 : 48 + (Iban.value d1 * 10 + Iban.value d2) / 10 = d1.toNat := by omega + have q2 : 48 + (Iban.value d1 * 10 + Iban.value d2) % 10 = d2.toNat := by omega + simp only [q1, q2, Char.ofNat_toNat] + end Codec.Proofs.Iban -theorem Spec.iban_valid_iff (s : List Char) : Iban.valid s = true ↔ Spec.IbanValid s := sorry +open Codec.Proofs.Iban + +theorem Spec.iban_valid_iff (s : List Char) : Iban.valid s = true ↔ Spec.IbanValid s := + valid_spec s theorem Spec.iban_checkDigits_iff (country bban ck : List Char) : Iban.checkDigits country bban = some ck ↔ - ck.length = 2 ∧ (∀ c ∈ ck, Spec.ibanDigit c) ∧ + 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 + 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 + · simp only [hc, false_and, iff_false] + unfold Iban.checkDigits + simp [hc] theorem 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)) : - Iban.valid (l ++ b :: r) = false := sorry + 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 + have hpw : pw b = pw a := by omega + obtain ⟨L, R, hLR⟩ := rot_block l [a] r (by simp; omega) + have e1 : (l ++ a :: r).drop 4 ++ (l ++ a :: r).take 4 = L ++ a :: R := hLR [a] rfl + have e2 : (l ++ b :: r).drop 4 ++ (l ++ b :: r).take 4 = L ++ b :: R := hLR [b] rfl + apply valid_false + rw [e1, num_mid] at h1 + rw [e2, num_mid, hpw] + intro h2 + have h3 : ((num L * pw a + Iban.value a) * pws R) % 97 = + ((num L * pw a + Iban.value b) * pws R) % 97 := by omega + have h4 := cancel_pws R _ _ h3 + omega theorem 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)) : - Iban.valid (l ++ b :: a :: r) = false := sorry + 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 + apply valid_false + intro h2 + by_cases hl : l.length = 3 + · -- the pair straddles the cut: the last check digit and the first BBAN character + match l, hl with + | [c0, c1, c2], _ => + rw [show [c0, c1, c2] ++ a :: b :: r = c0 :: c1 :: c2 :: a :: b :: r from rfl, + wellShaped_cons4] at hs + obtain ⟨_, _, _, da, _, hlen, _⟩ := hs + have pa : pw a = 10 := pw_of_digit a da + have hp' : pw b = 10 ∧ Iban.value a < 10 ∧ Iban.value b < 10 := by + rcases hp with ⟨_, pb, va, vb⟩ | ⟨pa', _⟩ + · exact ⟨pb, va, vb⟩ + · omega + obtain ⟨pb, va, vb⟩ := hp' + have r1 : ([c0, c1, c2] ++ a :: b :: r).drop 4 ++ ([c0, c1, c2] ++ a :: b :: r).take 4 = + b :: ((r ++ [c0, c1, c2]) ++ [a]) := by simp + have r2 : ([c0, c1, c2] ++ b :: a :: r).drop 4 ++ ([c0, c1, c2] ++ b :: a :: r).take 4 = + a :: ((r ++ [c0, c1, c2]) ++ [b]) := by simp + rw [r1, num_cons, num_snoc, pws_append, pa] at h1 + rw [r2, num_cons, num_snoc, pws_append, pb] at h2 + obtain ⟨k, hk, hkl⟩ := pws_pow (r ++ [c0, c1, c2]) + simp only [List.length_append, List.length_cons, List.length_nil] at hkl hlen + have p1 : pws [a] = 10 := by simp [pws, pa] + have p2 : pws [b] = 10 := by simp [pws, pb] + rw [p1] at h1 + rw [p2] at h2 + have hu : (pws (r ++ [c0, c1, c2]) * 10) % 97 ≠ 1 := by + rw [hk, ← Nat.pow_succ] + exact pow_ten_ne ⟨k + 1, by omega⟩ (by simp) + have e1 := mul_mod_right (Iban.value b) (pws (r ++ [c0, c1, c2]) * 10) + have e2 := mul_mod_right (Iban.value a) (pws (r ++ [c0, c1, c2]) * 10) + have e3 : (Iban.value b * ((pws (r ++ [c0, c1, c2]) * 10) % 97) + Iban.value a) % 97 = + (Iban.value a * ((pws (r ++ [c0, c1, c2]) * 10) % 97) + Iban.value b) % 97 := by + omega + have := swap_fin ⟨_, Nat.mod_lt _ (by decide)⟩ hu ⟨_, va⟩ ⟨_, vb⟩ e3 + simp only [Fin.mk.injEq] at this + exact hv this + · obtain ⟨L, R, hLR⟩ := rot_block l [a, b] r (by simp; omega) + have e1 : (l ++ a :: b :: r).drop 4 ++ (l ++ a :: b :: r).take 4 = L ++ a :: b :: R := + hLR [a, b] rfl + have e2 : (l ++ b :: a :: r).drop 4 ++ (l ++ b :: a :: r).take 4 = L ++ b :: a :: R := + hLR [b, a] rfl + rw [e1, num_mid2] at h1 + rw [e2, num_mid2] at h2 + rcases hp with ⟨pa, pb, _, _⟩ | ⟨pa, pb⟩ + · rw [pa, pb] at h1 h2 + have h3 : (((num L * 10 + Iban.value a) * 10 + Iban.value b) * pws R) % 97 = + (((num L * 10 + Iban.value b) * 10 + Iban.value a) * pws R) % 97 := by omega + have h4 := cancel_pws R _ _ h3 + omega + · rw [pa, pb] at h1 h2 + have h3 : (((num L * 100 + Iban.value a) * 100 + Iban.value b) * pws R) % 97 = + (((num L * 100 + Iban.value b) * 100 + Iban.value a) * pws R) % 97 := by omega + have h4 := cancel_pws R _ _ h3 + omega theorem Spec.iban_vectors : Iban.valid "GB29NWBK60161331926819".toList = true ∧ diff --git a/README.md b/README.md index ca107d3..771fd6a 100644 --- a/README.md +++ b/README.md @@ -72,7 +72,7 @@ This project has no dependencies beyond Lean itself. `tests/CROSS-CHECK.md` records a one-off comparison of the percent-decoder with Go's `net/url.PathUnescape`, of PEM with Go's `encoding/pem`, and of the check digits with python-stdnum. It is not part of the verified bar. On every text in US-ASCII that the tests give the decoder, Go gives the same answer, bad escapes included. Go reads a character outside US-ASCII as its UTF-8 bytes, where this decoder refuses it. -For the check digits, python-stdnum 2.2 gives the same answers on every Luhn and IBAN request the tests make, apart from the empty Luhn number, which it refuses, IBAN text it tidies first, and IBANs its registry check refuses. +For the check digits, python-stdnum 2.2 gives the same answers on every Luhn and IBAN request the tests make, apart from the empty Luhn number, which it refuses, IBAN text it tidies first, IBANs its registry check refuses, and requests this tool refuses whose stdnum form is a different question: a country code that is not two characters, which stdnum's `calc_check_digits` does not check, and a Luhn value above 9, which becomes more than one digit when written out. For PEM, Go writes the same text for every label the RFC's `label` rule allows, empty data included; it also writes labels the rule refuses. Go reads PEM laxly: it skips text around a block and takes headers and blanks, which this decoder refuses. And it ends lines at LF only, so it refuses most text with a CR alone as a line end, which RFC 7468 allows and this decoder reads. Go also refuses a message with empty data whose label holds a `:`, such as `-----BEGIN A:B-----` then `-----END A:B-----`, which Go itself writes: it takes the END line for an RFC 1421 header. Apart from those, on every text the cross-check gives this decoder and it accepts, Go reads the same label and data. diff --git a/SPEC.md b/SPEC.md index a42d9ab..ad92361 100644 --- a/SPEC.md +++ b/SPEC.md @@ -61,7 +61,7 @@ Scope: the check digit of ISO/IEC 7812-1, Annex B, from H. P. Luhn's US patent 2 Scope: the check digits of ISO 13616-1, by ISO 7064 MOD 97-10, on the electronic form: a country code of two upper-case letters, two check digits, and a BBAN of 1 to 30 upper-case letters and digits. - `valid` holds when the text has that shape and, with its first four characters moved to the end and each letter written as A = 10 to Z = 35, the digits read as one number leave 1 when divided by 97. -- `checkDigits` gives, for a country code and a BBAN of the right shape, the two digits from 02 to 98 that make the IBAN pass: 98 less the remainder of the BBAN, the country code and `00`. There is never more than one, and it fails on the wrong shape. +- `checkDigits` gives, for a country code of two letters and a BBAN of the right shape, the two digits from 02 to 98 that make the IBAN pass: 98 less the remainder of the BBAN, the country code and `00`. There is never more than one, and it fails on the wrong shape, a country code of any other length included. - What the check catches is a theorem: one digit typed for another or one letter for another, and two adjacent digits or two adjacent letters typed in the wrong order. Where the rearrangement splits an adjacent pair, the 4th and 5th characters, the swap is still caught, since 10 has order 96 mod 97. A letter and a digit swapped need not be caught: B is 11, so `4B1` and `41B` both read as `4111`, and a proved vector gives two IBANs that pass and differ only so. - Not checked: each country's BBAN format and length, in the SWIFT IBAN Registry, and whether the country code is one. Check digits 00, 01 and 99 never come from the computation, but an IBAN with them can pass the check. diff --git a/Spec.lean b/Spec.lean index 0e9897d..d4a4fb1 100644 --- a/Spec.lean +++ b/Spec.lean @@ -280,10 +280,11 @@ theorem Spec.luhn_vectors : theorem Spec.iban_valid_iff (s : List Char) : Iban.valid s = true ↔ Spec.IbanValid s := sorry /-- `checkDigits` gives exactly the two digits from 02 to 98 that make - the IBAN pass the check; there is never more than one. -/ + 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) : Iban.checkDigits country bban = some ck ↔ - ck.length = 2 ∧ (∀ c ∈ ck, Spec.ibanDigit c) ∧ + 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 diff --git a/tests/CROSS-CHECK.md b/tests/CROSS-CHECK.md index 419845f..8b1da65 100644 --- a/tests/CROSS-CHECK.md +++ b/tests/CROSS-CHECK.md @@ -3,22 +3,22 @@ Written by `tests/cross_check.py`, once, by hand. It is not part of the verified bar. - Seed: 20261024 -- Texts given to the percent-decoder: 194412, of which 166412 it accepts +- Texts given to the percent-decoder: 194411, of which 166412 it accepts - Go: `net/url.PathUnescape`, go version go1.24.7 linux/amd64 -- Texts in US-ASCII: 180340, differences: 0 +- Texts in US-ASCII: 180339, differences: 0 - Texts with a character outside US-ASCII: 14072, of which this decoder accepts 0. Go reads such a character as its UTF-8 bytes, and gives the same answer on 3917 of them (where it finds a bad escape too) and a different one on 10155. ## PEM - Go: `encoding/pem`, go version go1.24.7 linux/amd64 -- Encoding requests: 39088. The same text from both: 33035. Go writes a label this encoder refuses: 6053. Other differences: 0. -- Decoding requests: 66050. The same answer from both, with nothing left over in Go: 39312. Go reads text this decoder refuses: 3619. This decoder accepts text with a CR alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines at LF only: 22677. This decoder reads empty data under a label with a `:`, and Go takes the END line for a header: 442. Other differences, where this decoder accepts text that Go reads differently or not at all: 0. +- Encoding requests: 39087. The same text from both: 33034. Go writes a label this encoder refuses: 6053. Other differences: 0. +- Decoding requests: 66048. The same answer from both, with nothing left over in Go: 39311. Go reads text this decoder refuses: 3619. This decoder accepts text with a CR alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines at LF only: 22676. This decoder reads empty data under a label with a `:`, and Go takes the END line for a header: 442. Other differences, where this decoder accepts text that Go reads differently or not at all: 0. ## Luhn and IBAN - python-stdnum 2.2: `luhn.is_valid`, `luhn.calc_check_digit`, `iban.calc_check_digits`, and `iso7064.mod_97_10.is_valid` for the IBAN check -- Requests: 234856. The same answer: 234855. An empty Luhn number, which this codec passes and stdnum refuses: 1. IBAN text with a space, a dash, a dot or a lower-case letter, which stdnum removes or upper-cases first and this codec refuses: 0. Other differences: 0. -- The same IBANs given to stdnum's whole `iban.validate`: the same answer on 38564. It refuses, for a country code or BBAN format not in the SWIFT registry, 38983 that pass this codec's check, which does not use the registry. Read after stdnum's normalizing: 2. Other differences: 0. +- Requests: 234864. The same answer: 234856. An empty Luhn number, which this codec passes and stdnum refuses: 1. IBAN text with a space, a dash, a dot or a lower-case letter, which stdnum removes or upper-cases first and this codec refuses: 0. A country code that is not two characters, which this codec refuses and stdnum's `calc_check_digits` takes, since it does not check the country code: 6. A Luhn number with a value above 9, which this codec refuses as not a digit and which, written out for stdnum, becomes more than one digit: 1. Other differences: 0. +- The same IBANs given to stdnum's whole `iban.validate`: the same answer on 38569. It refuses, for a country code or BBAN format not in the SWIFT registry, 38986 that pass this codec's check, which does not use the registry. Read after stdnum's normalizing: 3. Other differences: 0. diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 1ec35e4..638f4bc 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -2,12 +2,12 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. -- Oracle: Python 3.13.17 `binascii`, `base64`, `zlib` (zlib 1.3), `urllib.parse`; for PEM, a strict encoder and parser written in tests/run_tests.py from RFC 7468, with `ssl.DER_cert_to_PEM_cert` and `ssl.PEM_cert_to_DER_cert` for the `CERTIFICATE` label +- Oracle: Python 3.13.17 `binascii`, `base64`, `zlib` (zlib 1.3), `urllib.parse`; for PEM, a strict encoder and parser written in tests/run_tests.py from RFC 7468, with `ssl.DER_cert_to_PEM_cert` and `ssl.PEM_cert_to_DER_cert` for the `CERTIFICATE` label; for Luhn and IBAN, the rules written in tests/run_tests.py, with Python's integers for the IBAN number - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261024 - Inputs: 1000000 -- Mutated: 265473 of the inputs are mutated encodings or frames -- By operation: b64dec 77551, b64enc 38769, crc 38770, error 82, frame 38768, hexdec 116322, hexenc 38772, iban 77549, ibancheck 38781, luhn 78647, luhncheck 39879, pctdec 194412, pctenc 39024, pemdec 66050, pemenc 39088, unframe 77536 +- Mutated: 265470 of the inputs are mutated encodings or frames +- By operation: b64dec 77551, b64enc 38768, crc 38770, error 82, frame 38768, hexdec 116320, hexenc 38771, iban 77558, ibancheck 38778, luhn 78650, luhncheck 39878, pctdec 194411, pctenc 39024, pemdec 66048, pemenc 39087, unframe 77536 - Malformed requests answered `error`: 82 of 82 - Last lines with no LF, sent alone, answered right: 6 of 6 - Strict base 64 rejections where Python decodes: 7102 (7102 with unused bits before the padding not zero, 0 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) diff --git a/tests/cross_check.py b/tests/cross_check.py index 22f0d1b..d702fdd 100644 --- a/tests/cross_check.py +++ b/tests/cross_check.py @@ -93,7 +93,7 @@ def theirs(label, req): except Exception: return "none" - counts = {"same": 0, "empty": 0, "normalized": 0, "other": []} + counts = {"same": 0, "empty": 0, "normalized": 0, "country": 0, "nondigit": 0, "other": []} for (label, req), o in zip(items, ours): t = theirs(label, req) arg = req.split(" ", 1)[1] if " " in req else "" @@ -104,6 +104,10 @@ def theirs(label, req): elif label in ("iban", "ibancheck") and any(chr(n) in " -." or 97 <= n <= 122 for n in run_tests_nums(req.replace(";", ","))): counts["normalized"] += 1 + elif label == "luhn" and o == "false" and any(n > 9 for n in run_tests_nums(req)): + counts["nondigit"] += 1 + elif label == "ibancheck" and o == "none" and len(run_tests_nums(req.split(";")[0])) != 2: + counts["country"] += 1 else: counts["other"].append((req, o, t)) # The whole of stdnum's IBAN check, with the SWIFT registry. @@ -134,7 +138,11 @@ def theirs(label, req): f"- Requests: {len(items)}. The same answer: {counts['same']}. An empty Luhn number, " f"which this codec passes and stdnum refuses: {counts['empty']}. IBAN text with a space, " f"a dash, a dot or a lower-case letter, which stdnum removes or upper-cases first and this codec " - f"refuses: {counts['normalized']}. Other differences: {len(counts['other'])}.", + f"refuses: {counts['normalized']}. A country code that is not two characters, which this " + f"codec refuses and stdnum's `calc_check_digits` takes, since it does not check the " + f"country code: {counts['country']}. A Luhn number with a value above 9, which this codec refuses as " + f"not a digit and which, written out for stdnum, becomes more than one digit: " + f"{counts['nondigit']}. Other differences: {len(counts['other'])}.", f"- The same IBANs given to stdnum's whole `iban.validate`: the same answer on " f"{full['same']}. It refuses, for a country code or BBAN format not in the SWIFT registry, " f"{full['registry']} that pass this codec's check, which does not use the registry. Read " diff --git a/tests/run_tests.py b/tests/run_tests.py index d9c4cc0..0e1decc 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -377,7 +377,7 @@ def oracle_iban(text): def oracle_iban_check(country, bban): - if not IBAN_SHAPE.fullmatch(country + "00" + bban): + if len(country) != 2 or not IBAN_SHAPE.fullmatch(country + "00" + bban): return "none" return "ok:" + text_nums(f"{98 - iban_number(bban + country + '00') % 97:02d}") @@ -386,6 +386,20 @@ def oracle_iban_check(country, bban): IBAN_POOL = IBAN_CHARS + "az -.\xe9" +def forged(country, bban): + """country, check digits and BBAN, the check digits chosen so that + the mod-97 sum passes whatever the shape.""" + return country + f"{98 - iban_number(bban + country + '00') % 97:02d}" + bban + + +# Strings whose mod-97 sum passes but whose shape does not, and the +# edges of the BBAN's length, so only the shape decides. +IBAN_SHAPE_EDGES = [forged("G1", "2345"), forged("1B", "2345"), forged("gb", "NWBK60161331926819"), + forged("GB", "nwbk1234"), forged("GB", ""), forged("GB", "A"), + forged("GB", "A" * 30), forged("GB", "A" * 31), forged("GB", "1" * 30), + forged("GB", "1" * 31), forged("ZZ", "Z" * 30)] + + def random_iban(rng): country = "".join(rng.choice(IBAN_CHARS[:26]) for _ in range(2)) bban = "".join(rng.choice(rng.choice([IBAN_CHARS, IBAN_CHARS[26:]])) @@ -522,8 +536,17 @@ def fixed_cases(): ds = list(ds) items.append(("luhn", f"luhn {nums(ds)}", oracle_luhn(ds), None, False)) items.append(("luhncheck", f"luhncheck {nums(ds)}", oracle_luhn_check(ds), None, False)) - for text in IBAN_EXAMPLES: + # Country codes of the wrong length, which can still make a string of + # the right shape with the BBAN: "GB1" with "2345" is "GB1002345". + for country, bban in [("GB1", "2345"), ("AB1", "2345"), ("G", "B2345"), ("", "GB2345"), + ("GBR", "2345"), ("GB12", "345")]: + items.append(("ibancheck", f"ibancheck {text_nums(country)};{text_nums(bban)}", + oracle_iban_check(country, bban), None, False)) + for text in IBAN_EXAMPLES + IBAN_SHAPE_EDGES: items.append(("iban", f"iban {text_nums(text)}", oracle_iban(text), None, False)) + # Numbers above 9 are not digits, for `luhn`. + for ds in ([10], [1, 10], [5, 255, 0], [0, 0, 18], [9, 9, 10, 0]): + items.append(("luhn", f"luhn {nums(ds)}", oracle_luhn(ds), None, False)) items.append(("ibancheck", f"ibancheck {text_nums(text[:2])};{text_nums(text[4:])}", oracle_iban_check(text[:2], text[4:]), None, False)) # PEM: every label above with data at the line edges (48 bytes are From 151b995c93d7f3e50a14bbfe84dcff7f8a299044 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 08:04:01 +0000 Subject: [PATCH 5/5] Fix what the pre-review found: test gaps, the CLI protocol, the oracle An independent pre-review (spec, page, tests), each finding checked by a separate agent, found 16 real problems. None is in the proofs. Tests: - The `ibancheck` cases for each example and shape edge sat in the wrong loop, so `checkDigits` refusing a wrong shape was never tested. They now run, with an empty BBAN, one of 31 characters, lower case, and digits or a dash in the country code, and mutated IBANs go to `ibancheck` too. - Luhn values above 9 now also come where the sum still passes, at a place doubled and not, so only the digit rule decides. - IBAN shape edges now put letters in the check-digit places, and `ibancheck` has malformed and surrogate requests. Cross-check: stdnum's own national checks are counted apart from the SWIFT registry, `ibancheck` shapes stdnum does not check get their own count, and the page says what stdnum confirms and what it does not. Page and SPEC.md: the Luhn and IBAN oracle is named where the others are; SPEC.md's command-line paragraph covers `ibancheck`, `luhn`, `luhncheck` and `iban`; `Luhn.checkDigit` is pinned down only for a payload of digits, and both say so; Luhn's adjacent-swap blind spot is no longer called its only one, and the errors no theorem covers are listed. `Spec.iban_vectors` gains the check digits of the German and French examples. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01WWUFjVe6uzWVQGpyU113ow --- Proofs/Iban.lean | 2 ++ README.md | 18 ++++++++------- SPEC.md | 8 +++---- Spec.lean | 2 ++ tests/CROSS-CHECK.md | 16 ++++++------- tests/TEST-RESULTS.md | 8 +++---- tests/cross_check.py | 35 ++++++++++++++++++++-------- tests/run_tests.py | 53 ++++++++++++++++++++++++++++++++++++++----- 8 files changed, 102 insertions(+), 40 deletions(-) diff --git a/Proofs/Iban.lean b/Proofs/Iban.lean index 035778d..be06ca5 100644 --- a/Proofs/Iban.lean +++ b/Proofs/Iban.lean @@ -479,6 +479,8 @@ theorem Spec.iban_vectors : Iban.valid "FR1420041010050500013M02606".toList = true ∧ Iban.valid "NO9386011117947".toList = true ∧ Iban.checkDigits "GB".toList "NWBK60161331926819".toList = some "29".toList ∧ + Iban.checkDigits "DE".toList "370400440532013000".toList = some "89".toList ∧ + Iban.checkDigits "FR".toList "20041010050500013M02606".toList = some "14".toList ∧ Iban.checkDigits "NO".toList "86011117947".toList = some "93".toList ∧ Iban.valid "GB29NWBK60161331926818".toList = false ∧ Iban.valid "gb29NWBK60161331926819".toList = false ∧ diff --git a/README.md b/README.md index 771fd6a..b202b90 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,12 @@ # codec: hex, base 64, CRC-32, percent-encoding, PEM and check digits, proved -Small codecs and check digits in Lean, each with machine-checked proofs that it does exactly what its specification says, and tested on a million inputs in all against Python's standard library and, for PEM, against an encoder and strict parser written in the tests from RFC 7468 (see `tests/TEST-RESULTS.md`). Hex is written as Python's `bytes.hex()` writes it, base 64 follows RFC 4648, the CRC-32 is the one in gzip, zip, and PNG, percent-encoding follows RFC 3986, PEM is the strict form of RFC 7468, the text that wraps certificates and keys, and the check digits are Luhn's, as on card numbers, and the IBAN's, by ISO 7064 MOD 97-10. The check digits come with what each catches and, as theorems too, what each misses. They are also the material for Level 0 of the [Proven Commons academy](https://github.com/Proven-Commons/mission): a first proof, read and then written, on code small enough to hold in your head. +Small codecs and check digits in Lean, each with machine-checked proofs that it does exactly what its specification says, and tested on a million inputs in all against Python's standard library, for PEM against an encoder and strict parser written in the tests from RFC 7468, and for the check digits against the Luhn and IBAN rules written in the tests (see `tests/TEST-RESULTS.md`). Hex is written as Python's `bytes.hex()` writes it, base 64 follows RFC 4648, the CRC-32 is the one in gzip, zip, and PNG, percent-encoding follows RFC 3986, PEM is the strict form of RFC 7468, the text that wraps certificates and keys, and the check digits are Luhn's, as on card numbers, and the IBAN's, by ISO 7064 MOD 97-10. The check digits come with what each catches and, also as theorems, an error each misses. They are also the material for Level 0 of the [Proven Commons academy](https://github.com/Proven-Commons/mission): a first proof, read and then written, on code small enough to hold in your head. Status: in progress. The specification has not yet been approved by a reviewer apart from its author, so this is not verified. ## 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. +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. | Claim | Theorem | |-------|---------| @@ -32,9 +32,9 @@ The statements are in `Spec.lean`, the definitions they use in `Spec/Defs.lean`, | 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 the check digit is the one digit that makes a number valid. | `Spec.luhn_valid_iff`, `Spec.luhn_checkDigit` | +| 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` | -| Luhn's blind spot: swapping an adjacent 0 and 9 is never caught. | `Spec.luhn_swap_09` | +| 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` | @@ -45,7 +45,9 @@ The command-line tool in `Main.lean` calls these functions directly. ## What is not proved -- Reading requests and printing answers in `Main.lean`: splitting lines, the decimal parser, the checks that bytes are below 256 and character codes are Unicode scalar values, and the conversions `Nat.toUInt8`, `Char.ofNat`, and `String.ofList`. The differential tests cover them, malformed requests included. +- Reading requests and printing answers in `Main.lean`: splitting lines, the decimal parser, the checks that bytes are below 256 and character codes are Unicode scalar values, `luhncheck`'s check that every number is a digit, the `;` that splits `pemenc` and `ibancheck`, and the conversions `Nat.toUInt8`, `Char.ofNat`, and `String.ofList`. The differential tests cover them, malformed requests included. +- Other errors the check digits miss. Luhn never catches a jump transposition, `abc` for `cba`, since both outer digits are doubled or neither is, nor the twin errors `22` for `55`, `33` for `66` and `44` for `77`. IBAN can miss a letter and a digit swapped, or a letter typed for a digit. No theorem covers these, and the tests do not count them. +- `Luhn.checkDigit` on a payload with a value above 9. No statement says what it gives there; the tool's `luhncheck` answers `error`. - Speed. The code works on lists, which suits proofs, not large data. - Base 64 variants: the URL-safe alphabet, line breaks, and unpadded text are not supported. Strict decoding also rejects two kinds of text that Python's strict mode decodes: unused bits before the padding that are not zero, and, in Python 3.11 and in 3.12 before 3.12.4, padding after a whole group, such as `Zm9v=`. The tests count both. - Percent-encoding with another set of characters left as they are, such as the `+` for a space of HTML forms or the wider sets of JavaScript's `encodeURIComponent`. Which characters a URI component allows, and whether text is decoded at the right layer, are for a URI parser. This codec decodes what it is given, once, and does not check that it is URI text: it reads any US-ASCII character but `%` as itself, and reads `%00` as a NUL byte. Section 7.3 of RFC 3986 says `%00` should be rejected where an application does not expect raw data in a component; that check is the caller's. @@ -64,7 +66,7 @@ The command-line tool in `Main.lean` calls these functions directly. - The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. - Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about (by `implemented_by` and `extern`), such as the fixed-width integer operations in CRC-32 and the arithmetic on natural numbers. - The operating system and hardware it runs on. -- Python's standard library and zlib, and for PEM an encoder and strict parser written in `tests/run_tests.py` from RFC 7468, as the oracle in the differential tests. The record names their versions. +- Python's standard library and zlib, for PEM an encoder and strict parser written in `tests/run_tests.py` from RFC 7468, and for Luhn and IBAN the rules written in `tests/run_tests.py`, with Python's integers for the IBAN number, as the oracles in the differential tests. The record names their versions. This project has no dependencies beyond Lean itself. @@ -72,7 +74,7 @@ This project has no dependencies beyond Lean itself. `tests/CROSS-CHECK.md` records a one-off comparison of the percent-decoder with Go's `net/url.PathUnescape`, of PEM with Go's `encoding/pem`, and of the check digits with python-stdnum. It is not part of the verified bar. On every text in US-ASCII that the tests give the decoder, Go gives the same answer, bad escapes included. Go reads a character outside US-ASCII as its UTF-8 bytes, where this decoder refuses it. -For the check digits, python-stdnum 2.2 gives the same answers on every Luhn and IBAN request the tests make, apart from the empty Luhn number, which it refuses, IBAN text it tidies first, IBANs its registry check refuses, and requests this tool refuses whose stdnum form is a different question: a country code that is not two characters, which stdnum's `calc_check_digits` does not check, and a Luhn value above 9, which becomes more than one digit when written out. +For Luhn, python-stdnum 2.2 gives the same answer on every request the tests make, apart from the empty number, which it refuses, and a value above 9, which becomes more than one digit when written out for it. For IBAN, stdnum has no check of the shape on its own. Its mod 97-10 check gives the same answer on every IBAN request, with the shape taken from the tests' own rule. Its `calc_check_digits` gives the same check digits wherever the country code and BBAN have the IBAN's shape; it checks neither, and it removes spaces, dashes and dots and upper-cases letters first. Its whole `iban.validate` checks each country's format in the SWIFT registry. It never accepts an IBAN this codec refuses, apart from one it reads after that tidying. But it refuses almost every random IBAN this codec accepts, for a country code or format not in the registry, and one more for its own list of Belgian bank codes. 22 pass both. `tests/CROSS-CHECK.md` gives the counts. For PEM, Go writes the same text for every label the RFC's `label` rule allows, empty data included; it also writes labels the rule refuses. Go reads PEM laxly: it skips text around a block and takes headers and blanks, which this decoder refuses. And it ends lines at LF only, so it refuses most text with a CR alone as a line end, which RFC 7468 allows and this decoder reads. Go also refuses a message with empty data whose label holds a `:`, such as `-----BEGIN A:B-----` then `-----END A:B-----`, which Go itself writes: it takes the END line for an RFC 1421 header. Apart from those, on every text the cross-check gives this decoder and it accepts, Go reads the same label and data. @@ -86,7 +88,7 @@ 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, and for PEM with an encoder and strict parser 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 `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. ## Layout diff --git a/SPEC.md b/SPEC.md index ad92361..d148ac9 100644 --- a/SPEC.md +++ b/SPEC.md @@ -53,7 +53,7 @@ The strict form has no text for empty data, since its last line of base 64 needs Scope: the check digit of ISO/IEC 7812-1, Annex B, from H. P. Luhn's US patent 2,950,048. Numbers are lists of digits 0 to 9, most significant first. - `valid` holds when every digit is 0 to 9 and the Luhn sum is a multiple of 10. The sum counts from the right, starting with the check digit: every second digit is doubled, and 9 is taken off a doubled digit above 9. The empty number passes, since its sum is 0. -- `checkDigit` gives the digit to put after a payload so that the whole is valid; it is the only such digit. +- `checkDigit` gives, for a payload of digits 0 to 9, the digit to put after it so that the whole is valid; it is the only such digit. On a payload with a value above 9, what it gives is not specified. - What the check catches is a theorem: any one digit typed wrong, and any two adjacent different digits typed in the wrong order, except 0 and 9. That exception is a theorem too. ## IBAN @@ -69,7 +69,7 @@ Scope: the check digits of ISO 13616-1, by ISO 7064 MOD 97-10, on the electronic Every encoder input, except a PEM label that the `label` rule refuses, and every `crc32` and `frame` input is valid. The decoders and `unframe` return `none` for anything they do not accept, PEM encoding returns `none` for such a label, and `Iban.checkDigits` returns `none` for a country code or BBAN of the wrong shape. No function can fail any other way. -The command-line tool in `Main.lean` reads one request per line and prints one answer per line. A request is an operation, then optionally one space and its comma-separated numbers; with no numbers after the space, the input is empty. `pemenc` is the exception: after its one space come the label's character codes, `;`, and the bytes, each list possibly empty, and it answers `ok:` and the character codes of the PEM text, or `none`. `pemdec` answers `ok:`, the label's character codes, `;`, and the bytes, or `none`. The tool prints `error` for any other line, including `pemenc` without its space or its `;`, an unknown operation, a number that is not plain decimal digits, a byte above 255, or a character code that is not a Unicode scalar value. A line may end in LF or CR LF; nothing else around a request is ignored. +The command-line tool in `Main.lean` reads one request per line and prints one answer per line. A request is an operation, then optionally one space and its comma-separated numbers; with no numbers after the space, the input is empty. `pemenc` and `ibancheck` are the exceptions: after the one space come two lists separated by one `;`, each possibly empty. For `pemenc` they are the label's character codes and the bytes, and it answers `ok:` and the character codes of the PEM text, or `none`. For `ibancheck` they are the character codes of the country code and of the BBAN, and it answers `ok:` and the character codes of the two check digits, or `none`. `pemdec` answers `ok:`, the label's character codes, `;`, and the bytes, or `none`. `luhn` and `iban` answer `true` or `false`; `iban` takes the IBAN as character codes. `luhncheck` answers the check digit. The tool prints `error` for any other line, including `pemenc` or `ibancheck` without its space or its `;`, an unknown operation, a number that is not plain decimal digits, a byte above 255, a character code that is not a Unicode scalar value, or a `luhncheck` number above 9. A line may end in LF or CR LF; nothing else around a request is ignored. ## What must always hold @@ -112,8 +112,8 @@ Each property is a theorem in `Spec.lean`, under the name given. The definitions | 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. 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. A function that did nothing, or that accepted too much, would fail at least one of them. +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. ## 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. +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. diff --git a/Spec.lean b/Spec.lean index d4a4fb1..0e837e3 100644 --- a/Spec.lean +++ b/Spec.lean @@ -311,6 +311,8 @@ theorem Spec.iban_vectors : Iban.valid "FR1420041010050500013M02606".toList = true ∧ Iban.valid "NO9386011117947".toList = true ∧ Iban.checkDigits "GB".toList "NWBK60161331926819".toList = some "29".toList ∧ + Iban.checkDigits "DE".toList "370400440532013000".toList = some "89".toList ∧ + Iban.checkDigits "FR".toList "20041010050500013M02606".toList = some "14".toList ∧ Iban.checkDigits "NO".toList "86011117947".toList = some "93".toList ∧ Iban.valid "GB29NWBK60161331926818".toList = false ∧ Iban.valid "gb29NWBK60161331926819".toList = false ∧ diff --git a/tests/CROSS-CHECK.md b/tests/CROSS-CHECK.md index 8b1da65..5b693c6 100644 --- a/tests/CROSS-CHECK.md +++ b/tests/CROSS-CHECK.md @@ -3,22 +3,22 @@ Written by `tests/cross_check.py`, once, by hand. It is not part of the verified bar. - Seed: 20261024 -- Texts given to the percent-decoder: 194411, of which 166412 it accepts +- Texts given to the percent-decoder: 180363, of which 154476 it accepts - Go: `net/url.PathUnescape`, go version go1.24.7 linux/amd64 -- Texts in US-ASCII: 180339, differences: 0 -- Texts with a character outside US-ASCII: 14072, of which this decoder accepts 0. Go reads such a character as its UTF-8 bytes, and gives the same answer on 3917 of them (where it finds a bad escape too) and a different one on 10155. +- Texts in US-ASCII: 167344, differences: 0 +- Texts with a character outside US-ASCII: 13019, of which this decoder accepts 0. Go reads such a character as its UTF-8 bytes, and gives the same answer on 3452 of them (where it finds a bad escape too) and a different one on 9567. ## PEM - Go: `encoding/pem`, go version go1.24.7 linux/amd64 -- Encoding requests: 39087. The same text from both: 33034. Go writes a label this encoder refuses: 6053. Other differences: 0. -- Decoding requests: 66048. The same answer from both, with nothing left over in Go: 39311. Go reads text this decoder refuses: 3619. This decoder accepts text with a CR alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines at LF only: 22676. This decoder reads empty data under a label with a `:`, and Go takes the END line for a header: 442. Other differences, where this decoder accepts text that Go reads differently or not at all: 0. +- Encoding requests: 36278. The same text from both: 30763. Go writes a label this encoder refuses: 5515. Other differences: 0. +- Decoding requests: 61506. The same answer from both, with nothing left over in Go: 36549. Go reads text this decoder refuses: 3393. This decoder accepts text with a CR alone as a line end, as RFC 7468's `eol` allows, and Go does not, since it ends lines at LF only: 21118. This decoder reads empty data under a label with a `:`, and Go takes the END line for a header: 446. Other differences, where this decoder accepts text that Go reads differently or not at all: 0. ## Luhn and IBAN -- python-stdnum 2.2: `luhn.is_valid`, `luhn.calc_check_digit`, `iban.calc_check_digits`, and `iso7064.mod_97_10.is_valid` for the IBAN check -- Requests: 234864. The same answer: 234856. An empty Luhn number, which this codec passes and stdnum refuses: 1. IBAN text with a space, a dash, a dot or a lower-case letter, which stdnum removes or upper-cases first and this codec refuses: 0. A country code that is not two characters, which this codec refuses and stdnum's `calc_check_digits` takes, since it does not check the country code: 6. A Luhn number with a value above 9, which this codec refuses as not a digit and which, written out for stdnum, becomes more than one digit: 1. Other differences: 0. -- The same IBANs given to stdnum's whole `iban.validate`: the same answer on 38569. It refuses, for a country code or BBAN format not in the SWIFT registry, 38986 that pass this codec's check, which does not use the registry. Read after stdnum's normalizing: 3. Other differences: 0. +- python-stdnum 2.2: `luhn.is_valid`, `luhn.calc_check_digit`, `iban.calc_check_digits`, and `iso7064.mod_97_10.is_valid` for the IBAN check. stdnum has no check of the IBAN shape on its own, so for `iban` requests the shape comes from the tests' own regular expression and only the mod 97-10 check from stdnum +- Requests: 289968. The same answer: 280357. An empty Luhn number, which this codec passes and stdnum refuses: 1. IBAN text with a space, a dash, a dot or a lower-case letter, which stdnum removes or upper-cases first and this codec refuses: 4348. A country code that is not two characters, which this codec refuses and stdnum's `calc_check_digits` takes, since it does not check the country code: 6. A country code and BBAN that do not have the IBAN's shape, such as an empty BBAN or one of 31 characters, which this codec refuses and `calc_check_digits` takes, since it does not check the shape: 2117. A Luhn number with a value above 9, which this codec refuses as not a digit and which, written out for stdnum, becomes more than one digit: 3139. Other differences: 0. +- The same IBANs given to stdnum's whole `iban.validate`, which checks the shape itself: the same answer on 35815, of which 22 pass both. It refuses, for a country code or BBAN format not in the SWIFT registry, 36127 that pass this codec's check, which does not use the registry; and 1 for one of its own national checks, such as a bank code missing from its list. Read after stdnum's normalizing: 1. Other differences: 0. diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md index 638f4bc..cb995ab 100644 --- a/tests/TEST-RESULTS.md +++ b/tests/TEST-RESULTS.md @@ -6,9 +6,9 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers. - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) - Seed: 20261024 - Inputs: 1000000 -- Mutated: 265470 of the inputs are mutated encodings or frames -- By operation: b64dec 77551, b64enc 38768, crc 38770, error 82, frame 38768, hexdec 116320, hexenc 38771, iban 77558, ibancheck 38778, luhn 78650, luhncheck 39878, pctdec 194411, pctenc 39024, pemdec 66048, pemenc 39087, unframe 77536 -- Malformed requests answered `error`: 82 of 82 +- Mutated: 318260 of the inputs are mutated encodings or frames +- By operation: b64dec 71933, b64enc 35959, crc 35961, error 85, frame 35959, hexdec 107893, hexenc 35962, iban 71944, ibancheck 71960, luhn 108995, luhncheck 37069, pctdec 180363, pctenc 36215, pemdec 61506, pemenc 36278, unframe 71918 +- Malformed requests answered `error`: 85 of 85 - Last lines with no LF, sent alone, answered right: 6 of 6 -- Strict base 64 rejections where Python decodes: 7102 (7102 with unused bits before the padding not zero, 0 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) +- Strict base 64 rejections where Python decodes: 6450 (6450 with unused bits before the padding not zero, 0 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode) - Failures: 0 diff --git a/tests/cross_check.py b/tests/cross_check.py index d702fdd..d0ac6d5 100644 --- a/tests/cross_check.py +++ b/tests/cross_check.py @@ -87,13 +87,13 @@ def theirs(label, req): text = "".join(map(chr, run_tests_nums(req))) return str(bool(run_tests.IBAN_SHAPE.fullmatch(text)) and mod_97_10.is_valid(text[4:] + text[:4])).lower() - country, bban = (bytes(int(n) for n in part.split(",") if n).decode() for part in arg.split(";")) + country, bban = ("".join(chr(int(n)) for n in part.split(",") if n) for part in arg.split(";")) try: return "ok:" + run_tests.text_nums(iban.calc_check_digits(country + "00" + bban)) except Exception: return "none" - counts = {"same": 0, "empty": 0, "normalized": 0, "country": 0, "nondigit": 0, "other": []} + counts = {"same": 0, "empty": 0, "normalized": 0, "country": 0, "shape": 0, "nondigit": 0, "other": []} for (label, req), o in zip(items, ours): t = theirs(label, req) arg = req.split(" ", 1)[1] if " " in req else "" @@ -108,10 +108,12 @@ def theirs(label, req): counts["nondigit"] += 1 elif label == "ibancheck" and o == "none" and len(run_tests_nums(req.split(";")[0])) != 2: counts["country"] += 1 + elif label == "ibancheck" and o == "none": + counts["shape"] += 1 else: counts["other"].append((req, o, t)) # The whole of stdnum's IBAN check, with the SWIFT registry. - full = {"same": 0, "registry": 0, "normalized": 0, "other": []} + full = {"same": 0, "same_true": 0, "registry": 0, "national": 0, "normalized": 0, "other": []} for (label, req), o in zip(items, ours): if label != "iban": continue @@ -123,8 +125,15 @@ def theirs(label, req): t, why = "false", type(e).__name__ if o == t: full["same"] += 1 + full["same_true"] += t == "true" elif o == "true" and why in ("InvalidComponent", "InvalidFormat", "InvalidLength"): - full["registry"] += 1 + # stdnum also runs its own national checks (bank lists, national + # check digits); those refusals are not the registry's. + try: + iban.validate(text, check_country=False) + full["national"] += 1 + except Exception: + full["registry"] += 1 elif any(c in " -." or c.islower() for c in text): full["normalized"] += 1 else: @@ -134,19 +143,25 @@ def theirs(label, req): "## Luhn and IBAN", "", "- python-stdnum 2.2: `luhn.is_valid`, `luhn.calc_check_digit`, " - "`iban.calc_check_digits`, and `iso7064.mod_97_10.is_valid` for the IBAN check", + "`iban.calc_check_digits`, and `iso7064.mod_97_10.is_valid` for the IBAN check. stdnum " + "has no check of the IBAN shape on its own, so for `iban` requests the shape comes from " + "the tests' own regular expression and only the mod 97-10 check from stdnum", f"- Requests: {len(items)}. The same answer: {counts['same']}. An empty Luhn number, " f"which this codec passes and stdnum refuses: {counts['empty']}. IBAN text with a space, " f"a dash, a dot or a lower-case letter, which stdnum removes or upper-cases first and this codec " f"refuses: {counts['normalized']}. A country code that is not two characters, which this " f"codec refuses and stdnum's `calc_check_digits` takes, since it does not check the " - f"country code: {counts['country']}. A Luhn number with a value above 9, which this codec refuses as " + f"country code: {counts['country']}. A country code and BBAN that do not have the IBAN's shape, such as " + f"an empty BBAN or one of 31 characters, which this codec refuses and `calc_check_digits` " + f"takes, since it does not check the shape: {counts['shape']}. A Luhn number with a value above 9, which this codec refuses as " f"not a digit and which, written out for stdnum, becomes more than one digit: " f"{counts['nondigit']}. Other differences: {len(counts['other'])}.", - f"- The same IBANs given to stdnum's whole `iban.validate`: the same answer on " - f"{full['same']}. It refuses, for a country code or BBAN format not in the SWIFT registry, " - f"{full['registry']} that pass this codec's check, which does not use the registry. Read " - f"after stdnum's normalizing: {full['normalized']}. Other differences: {len(full['other'])}.", + f"- The same IBANs given to stdnum's whole `iban.validate`, which checks the shape itself: " + f"the same answer on {full['same']}, of which {full['same_true']} pass both. It refuses, for " + f"a country code or BBAN format not in the SWIFT registry, {full['registry']} that pass this " + f"codec's check, which does not use the registry; and {full['national']} for one of its own " + f"national checks, such as a bank code missing from its list. Read after stdnum's " + f"normalizing: {full['normalized']}. Other differences: {len(full['other'])}.", "", ] lines += [f"- `{r[:100]}`: this project `{o}`, stdnum `{t}`" diff --git a/tests/run_tests.py b/tests/run_tests.py index 0e1decc..b8a957a 100644 --- a/tests/run_tests.py +++ b/tests/run_tests.py @@ -153,6 +153,9 @@ def decoded(result): ("ibancheck", "no arguments"), ("ibancheck 71,66", "no `;`"), ("ibancheck 71;66;1", "two `;`"), + ("ibancheck 71,x;66", "a number that is not decimal"), + ("ibancheck 71,66;55296", "a surrogate in the BBAN"), + ("ibancheck 55296,66;49", "a surrogate in the country code"), ("iban 71,55296", "a surrogate, not a character"), ("pemenc", "no arguments"), ("pemenc 88", "no `;` between the label and the data"), @@ -392,12 +395,24 @@ def forged(country, bban): return country + f"{98 - iban_number(bban + country + '00') % 97:02d}" + bban +def forged_check(country, check, bban): + """country, `check` in the check-digit places, and the BBAN with the + two digits after it that make the mod-97 sum pass whatever the + shape.""" + for n in range(100): + if iban_number(bban + f"{n:02d}" + country + check) % 97 == 1: + return country + check + bban + f"{n:02d}" + + # Strings whose mod-97 sum passes but whose shape does not, and the -# edges of the BBAN's length, so only the shape decides. +# edges of the BBAN's length, so only the shape decides; and letters in +# the check-digit places. IBAN_SHAPE_EDGES = [forged("G1", "2345"), forged("1B", "2345"), forged("gb", "NWBK60161331926819"), forged("GB", "nwbk1234"), forged("GB", ""), forged("GB", "A"), forged("GB", "A" * 30), forged("GB", "A" * 31), forged("GB", "1" * 30), - forged("GB", "1" * 31), forged("ZZ", "Z" * 30)] + forged("GB", "1" * 31), forged("ZZ", "Z" * 30), + forged_check("GB", "A1", "NWBK1234"), forged_check("GB", "1A", "NWBK1234"), + forged_check("GB", "AB", "NWBK1234"), forged_check("GB", "ZZ", "")] def random_iban(rng): @@ -427,6 +442,20 @@ def mutate_iban(rng, text): return text.lower() if rng.random() < 0.5 else text + rng.choice(IBAN_CHARS) +def above_nine(rng, ds): + """`ds`, valid, with one digit d made d + 10 where the Luhn sum stays a + multiple of 10: at a place that is not doubled, or a doubled place + with d at least 5. So only the rule that every digit is 0 to 9 + decides. `None` when no place qualifies.""" + places = [i for i in range(len(ds)) + if (len(ds) - 1 - i) % 2 == 0 or ds[i] >= 5] + if not places: + return None + out = list(ds) + out[rng.choice(places)] += 10 + return out + + def mutate_digits(rng, ds): out = list(ds) kind = rng.randrange(3) @@ -538,17 +567,24 @@ def fixed_cases(): items.append(("luhncheck", f"luhncheck {nums(ds)}", oracle_luhn_check(ds), None, False)) # Country codes of the wrong length, which can still make a string of # the right shape with the BBAN: "GB1" with "2345" is "GB1002345". + # And country codes or BBANs of the wrong shape: an empty BBAN, one of + # 31 characters, lower case, a digit or a dash in the country code. for country, bban in [("GB1", "2345"), ("AB1", "2345"), ("G", "B2345"), ("", "GB2345"), - ("GBR", "2345"), ("GB12", "345")]: + ("GBR", "2345"), ("GB12", "345"), ("GB", ""), ("GB", "A" * 31), + ("GB", "A" * 30), ("GB", "1"), ("gb", "NWBK1234"), ("GB", "nwbk1234"), + ("G1", "2345"), ("1B", "2345"), ("G-", "2345"), ("GB", "NWBK-1234")]: items.append(("ibancheck", f"ibancheck {text_nums(country)};{text_nums(bban)}", oracle_iban_check(country, bban), None, False)) for text in IBAN_EXAMPLES + IBAN_SHAPE_EDGES: items.append(("iban", f"iban {text_nums(text)}", oracle_iban(text), None, False)) - # Numbers above 9 are not digits, for `luhn`. - for ds in ([10], [1, 10], [5, 255, 0], [0, 0, 18], [9, 9, 10, 0]): - items.append(("luhn", f"luhn {nums(ds)}", oracle_luhn(ds), None, False)) items.append(("ibancheck", f"ibancheck {text_nums(text[:2])};{text_nums(text[4:])}", oracle_iban_check(text[:2], text[4:]), None, False)) + # Numbers above 9 are not digits, for `luhn`; in the last five the sum + # is still a multiple of 10, at a place doubled and not. + for ds in ([10], [1, 10], [5, 255, 0], [0, 0, 18], [9, 9, 10, 0], [10, 9], [10, 0, 0], + [7, 9, 9, 2, 7, 3, 9, 8, 7, 1, 13], [7, 9, 9, 2, 7, 3, 9, 8, 17, 1, 3], + [7, 9, 9, 2, 7, 3, 9, 18, 7, 1, 3]): + items.append(("luhn", f"luhn {nums(ds)}", oracle_luhn(ds), None, False)) # PEM: every label above with data at the line edges (48 bytes are # one full line), and every bad label. for label in PEM_LABELS + BAD_PEM_LABELS: @@ -627,7 +663,12 @@ def cases(seed, count): oracle_iban_check(country, bban), None, False), ("iban", f"iban {text_nums(iban)}", oracle_iban(iban), None, False), ("iban", f"iban {text_nums(bad_iban)}", oracle_iban(bad_iban), None, True), + ("ibancheck", f"ibancheck {text_nums(bad_iban[:2])};{text_nums(bad_iban[4:])}", + oracle_iban_check(bad_iban[:2], bad_iban[4:]), None, True), ] + big = above_nine(rng, ds_valid) + if big is not None: + batch.append(("luhn", f"luhn {nums(big)}", oracle_luhn(big), None, True)) label = rng.choice(PEM_LABELS + BAD_PEM_LABELS[:3]) pem_data = data[: rng.choice([0, 1, 47, 48, 49, 96, 97, 200, len(data)])] batch.append(("pemenc", f"pemenc {text_nums(label)};{nums(pem_data)}",