Add Luhn and IBAN check digits, proved and tested

Codec.lean

@@ -3,3 +3,5 @@ import Codec.Base64
 import Codec.Crc32
 import Codec.Percent
 import Codec.Pem
+import Codec.Luhn
+import Codec.Iban

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

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

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

Proofs.lean

@@ -7,3 +7,5 @@ import Proofs.Base64
 import Proofs.Crc32
 import Proofs.Percent
 import Proofs.Pem
+import Proofs.Luhn
+import Proofs.Iban