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..aeec2c0 --- /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 is not two letters or the BBAN has the wrong shape. -/ +def checkDigits (country bban : List Char) : Option (List Char) := + 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 + +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..be06ca5 --- /dev/null +++ b/Proofs/Iban.lean @@ -0,0 +1,489 @@ +/- + 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 + +/-! ### 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 + +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 ↔ + country.length = 2 ∧ ck.length = 2 ∧ (∀ c ∈ ck, Spec.ibanDigit c) ∧ + 2 ≤ Spec.ibanNumber ck ∧ Spec.ibanNumber ck ≤ 98 ∧ + Spec.IbanValid (country ++ ck ++ bban) := by + 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 := 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 := 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 ∧ + 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 "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 ∧ + 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..b202b90 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,12 @@ -# 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, 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,18 +32,29 @@ 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, for a payload of digits, the check digit is the one digit that makes it valid. | `Spec.luhn_valid_iff`, `Spec.luhn_checkDigit` | +| Luhn catches any one digit typed wrong, and any two adjacent different digits typed in the wrong order, except 0 and 9. | `Spec.luhn_single_error`, `Spec.luhn_adjacent_swap` | +| Among adjacent swaps, Luhn misses only one: an adjacent 0 and 9 swapped is never caught. | `Spec.luhn_swap_09` | +| Luhn gives the common worked example, 79927398713, and a test card number. | `Spec.luhn_vectors` | +| IBAN: `valid` decides the check of ISO 13616 by ISO 7064 MOD 97-10 (the shape, and the rearranged number mod 97), and `checkDigits` gives exactly the two digits from 02 to 98 that make an IBAN pass. | `Spec.iban_valid_iff`, `Spec.iban_checkDigits_iff` | +| IBAN catches one digit typed for another or one letter for another, and two adjacent digits or two adjacent letters typed in the wrong order. | `Spec.iban_substitution`, `Spec.iban_adjacent_swap` | +| IBAN gives the SWIFT registry's UK example and Germany's, France's and Norway's, and their check digits; and its blind spot: a letter and a digit swapped, `4B1` for `41B`, gives another IBAN that passes. | `Spec.iban_vectors` | | PEM encoding writes RFC 7468's Figure 15 exactly as the RFC prints it, and decoding reads it back with CR LF line ends; empty data, an empty label, labels the rule refuses, and texts the decoder refuses. | `Spec.pem_vectors` | 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. - 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. @@ -55,13 +66,15 @@ 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. ## 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 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. @@ -75,11 +88,11 @@ 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 -- `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 +102,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..d148ac9 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,11 +48,28 @@ 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, 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 + +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 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. + ## 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. +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 @@ -82,10 +99,21 @@ 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 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 230e314..0e837e3 100644 --- a/Spec.lean +++ b/Spec.lean @@ -236,3 +236,85 @@ 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, 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 ↔ + 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 + +/-- 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 "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 ∧ + 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..5b693c6 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: 180363, of which 154476 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: 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: 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: 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. 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 1df57e8..cb995ab 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`; 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: 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: 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: 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: 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 f434ad0..d0ac6d5 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,124 @@ 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 = ("".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, "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 "" + 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 + 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 + 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, "same_true": 0, "registry": 0, "national": 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 + full["same_true"] += t == "true" + elif o == "true" and why in ("InvalidComponent", "InvalidFormat", "InvalidLength"): + # 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: + 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. 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 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`, 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}`" + 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 +293,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..b8a957a 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,14 @@ 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 `;`"), + ("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"), ("pemenc 88;1;2", "two `;`"), @@ -333,6 +342,134 @@ 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 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}") + + +IBAN_CHARS = "ABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789" +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 + + +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; 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_check("GB", "A1", "NWBK1234"), forged_check("GB", "1A", "NWBK1234"), + forged_check("GB", "AB", "NWBK1234"), forged_check("GB", "ZZ", "")] + + +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 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) + 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 +559,32 @@ 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)) + # 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"), ("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)) + 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: @@ -487,6 +650,25 @@ 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), + ("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)}", @@ -566,7 +748,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():