Bring PEM and check digits onto main

Codec.lean

@@ -3,3 +3,6 @@ import Codec.Base64
 import Codec.Base32
 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

Codec/Pem.lean

@@ -0,0 +1,105 @@
+/-
+  PEM, the textual encoding of RFC 7468, in its strict form (Figure 3):
+
+    -----BEGIN label-----
+    the base 64 of the data, in lines of 64 characters, the last at most 64
+    -----END label-----
+
+  `encode` writes each line ending in LF, and fails on a label that the
+  `label` rule of section 3 does not allow. `decode` reads exactly one
+  message in this form, with each line ending in LF, CR, or CR LF. It
+  fails on anything else: a different label on the END line, blanks,
+  headers, text before or after the message, a short line before the
+  last, and base 64 that `Base64.decode` refuses. Empty data has no line
+  of base 64.
+-/
+
+import Codec.Base64
+
+namespace Codec.Pem
+
+/-- `labelchar`: a printable US-ASCII character other than `-`. -/
+def isLabelChar (c : Char) : Bool :=
+  let n := c.toNat
+  (0x21 ≤ n && n ≤ 0x2C) || (0x2E ≤ n && n ≤ 0x7E)
+
+/-- After the first character of a label: label characters, each of
+    which may follow one `-` or space. -/
+def labelRest : List Char → Bool
+  | [] => true
+  | c :: rest =>
+    if isLabelChar c then labelRest rest
+    else if c = '-' ∨ c = ' ' then
+      match rest with
+      | d :: rest' => isLabelChar d && labelRest rest'
+      | [] => false
+    else false
+
+/-- A label: empty, or a label character and then `labelRest`. -/
+def validLabel : List Char → Bool
+  | [] => true
+  | c :: rest => isLabelChar c && labelRest rest
+
+/-- Cut text into lines of 64 characters, the last one at most 64. `fuel`
+    equal to the text's length is enough. -/
+def lines64 : Nat → List Char → List (List Char)
+  | _, [] => []
+  | 0, _ :: _ => []
+  | fuel + 1, cs => cs.take 64 :: lines64 fuel (cs.drop 64)
+
+def beginLine (label : List Char) : List Char := "-----BEGIN ".toList ++ label ++ "-----".toList
+
+def endLine (label : List Char) : List Char := "-----END ".toList ++ label ++ "-----".toList
+
+/-- The lines of a message: BEGIN, the base 64, END. -/
+def lines (label : List Char) (data : List UInt8) : List (List Char) :=
+  let b64 := Base64.encode data
+  beginLine label :: lines64 b64.length b64 ++ [endLine label]
+
+/-- Encode data under a label, each line ending in LF. -/
+def encode (label : List Char) (data : List UInt8) : Option (List Char) :=
+  if validLabel label then some ((lines label data).flatMap (· ++ ['\n'])) else none
+
+/-- The first line of `text` and the text after its line end (LF, CR,
+    or CR LF), or `none` when no line end follows. -/
+def takeLine : List Char → Option (List Char × List Char)
+  | [] => none
+  | '\r' :: '\n' :: rest => some ([], rest)
+  | '\r' :: rest => some ([], rest)
+  | '\n' :: rest => some ([], rest)
+  | c :: rest => (takeLine rest).map fun (l, r) => (c :: l, r)
+
+/-- Split text into lines, each of which must end in a line end. `fuel`
+    equal to the text's length is enough. -/
+def splitLines : Nat → List Char → Option (List (List Char))
+  | _, [] => some []
+  | 0, _ :: _ => none
+  | fuel + 1, text => do
+    let (l, rest) ← takeLine text
+    let ls ← splitLines fuel rest
+    pure (l :: ls)
+
+/-- The label of a BEGIN line, or of an END line. -/
+def labelOf (pre : List Char) (line : List Char) : Option (List Char) :=
+  if pre.isPrefixOf line ∧ "-----".toList.isSuffixOf line ∧ pre.length + 5 ≤ line.length then
+    some ((line.drop pre.length).take (line.length - pre.length - 5))
+  else none
+
+/-- Decode one message in the strict form: its label and its data. -/
+def decode (text : List Char) : Option (List Char × List UInt8) := do
+  let ls ← splitLines text.length text
+  match ls with
+  | first :: rest =>
+    match rest.getLast? with
+    | some last =>
+      let body := rest.dropLast
+      let label ← labelOf "-----BEGIN ".toList first
+      let label' ← labelOf "-----END ".toList last
+      let data ← Base64.decode body.flatten
+      if label = label' ∧ validLabel label ∧ body = lines64 body.flatten.length body.flatten then
+        some (label, data)
+      else none
+    | none => none
+  | [] => none
+
+end Codec.Pem

Main.lean

@@ -16,9 +16,29 @@
     unframe 1,2,3,4,5     prints  ok:... (or none)
     pctenc 32,65          prints  %20A
     pctdec 37,50,48,65    prints  ok:32,65   (or none)
+    pemenc 88;0           prints  ok: and the character codes of the PEM
+                                  text for label "X" and the byte 0
+                                  (or none, for a label the rule refuses)
+    pemdec 45,45,...      prints  ok:88;0, the label's character codes and
+                                  the data (or none)
+
+    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. 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
@@ -53,6 +73,31 @@ def toChars (ns : List Nat) : Option (List Char) :=
 def showBytes (bs : List UInt8) : String :=
   ",".intercalate (bs.map fun b => toString b.toNat)
 
+def showChars (cs : List Char) : String :=
+  ",".intercalate (cs.map fun c => toString c.toNat)
+
+/-- `pemenc`: the label's character codes, `;`, and the bytes. -/
+def pemEncode (arg : String) : Option String :=
+  match arg.splitOn ";" with
+  | [l, d] => do
+    let label ← toChars (← numbers l)
+    let data ← toBytes (← numbers d)
+    return match Pem.encode label data with
+      | some text => "ok:" ++ showChars text
+      | none => "none"
+  | _ => none
+
+/-- `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
@@ -70,12 +115,23 @@ 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
+      | none => "none"
   | _ => none
 
 /-- The answer to one line: an operation, then optionally one space and
     its numbers. -/
 def request (line : String) : Option String :=
   match line.splitOn " " with
+  | ["pemenc", arg] => pemEncode arg
+  | ["pemenc"] => none
+  | ["ibancheck", arg] => ibanCheck arg
+  | ["ibancheck"] => none
   | [op] => answer op []
   | [op, arg] => numbers arg >>= answer op
   | _ => none

Proofs.lean

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