Bound decimal conversion and cover PEM refusal cases

Main.lean

@@ -52,13 +52,15 @@ import Codec
 
 open Codec
 
-/-- A number in plain decimal digits. Longer numbers than any byte or
-    character code are refused before they are converted, since that
-    takes time quadratic in their length. -/
+/-- A number in plain decimal digits. Leading zeros are accepted and
+    removed before conversion. At most seven significant digits are
+    converted, bounding the quadratic decimal conversion cost. -/
 def number (t : String) : Option Nat :=
   let ds := t.toList
-  if ds.isEmpty || !ds.all Char.isDigit || (ds.dropWhile (· = '0')).length > 7 then none
-  else t.toNat?
+  let significant := ds.dropWhile (· = '0')
+  if ds.isEmpty || !ds.all Char.isDigit || significant.length > 7 then none
+  else if significant.isEmpty then some 0
+  else (String.ofList significant).toNat?
 
 /-- The comma-separated numbers in `s`. -/
 def numbers (s : String) : Option (List Nat) :=

Proofs/Pem.lean

@@ -226,6 +226,9 @@ theorem Spec.pem_vectors :
     Pem.encode " A".toList [] = none ∧
     Pem.encode "A-".toList [] = none ∧
     Pem.encode "\u00c9".toList [] = none ∧
+    Pem.decode "-----BEGIN X-----\n\n-----END X-----\n".toList = none ∧
+    Pem.decode ("-----BEGIN X-----\nAA==\n-----END X-----\n" ++
+      "-----BEGIN X-----\nAA==\n-----END X-----\n").toList = none ∧
     Pem.decode "-----BEGIN X-----\nAA==\n-----END Y-----\n".toList = none ∧
     Pem.decode "-----BEGIN X-----\nAA==\n-----END X-----".toList = none ∧
     Pem.decode "-----BEGIN X-----\nAA== \n-----END X-----\n".toList = none ∧

README.md

@@ -76,7 +76,7 @@ This project has no dependencies beyond Lean itself.
 
 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.
+For PEM, Go writes the same text for every allowed label tried in the cross-check, empty data included; it also writes labels the rule refuses. Go reads PEM laxly: it skips text around a block and takes headers and blanks, which this decoder refuses. And it ends lines at LF only, so it refuses most text with a CR alone as a line end, which RFC 7468 allows and this decoder reads. Go also refuses a message with empty data whose label holds a `:`, such as `-----BEGIN A:B-----` then `-----END A:B-----`, which Go itself writes: it takes the END line for an RFC 1421 header. Apart from those, on every text the cross-check gives this decoder and it accepts, Go reads the same label and data.
 
 ## Re-check it
 

Spec.lean

@@ -225,6 +225,9 @@ theorem Spec.pem_vectors :
     Pem.encode " A".toList [] = none ∧
     Pem.encode "A-".toList [] = none ∧
     Pem.encode "\u00c9".toList [] = none ∧
+    Pem.decode "-----BEGIN X-----\n\n-----END X-----\n".toList = none ∧
+    Pem.decode ("-----BEGIN X-----\nAA==\n-----END X-----\n" ++
+      "-----BEGIN X-----\nAA==\n-----END X-----\n").toList = none ∧
     Pem.decode "-----BEGIN X-----\nAA==\n-----END Y-----\n".toList = none ∧
     Pem.decode "-----BEGIN X-----\nAA==\n-----END X-----".toList = none ∧
     Pem.decode "-----BEGIN X-----\nAA== \n-----END X-----\n".toList = none ∧

tests/TEST-RESULTS.md

@@ -6,8 +6,8 @@ Written by `tests/run_tests.py`. Rerun it to check these numbers.
 - Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release)
 - Seed: 20261024
 - Inputs: 1000000
-- Mutated: 319603 of the inputs are mutated encodings or frames
-- By operation: b32dec 64902, b32enc 32444, b64dec 64902, b64enc 32444, crc 32446, error 89, frame 32444, hexdec 97348, hexenc 32447, iban 64914, ibancheck 64930, luhn 98450, luhncheck 33554, pctdec 162787, pctenc 32699, pemdec 55550, pemenc 32763, unframe 64887
+- Mutated: 319602 of the inputs are mutated encodings or frames
+- By operation: b32dec 64902, b32enc 32444, b64dec 64902, b64enc 32444, crc 32445, error 89, frame 32443, hexdec 97347, hexenc 32447, iban 64914, ibancheck 64930, leading zeros 2, luhn 98450, luhncheck 33554, pctdec 162787, pctenc 32699, pemdec 55550, pemdec refusal 2, pemenc 32763, unframe 64886
 - Malformed requests answered `error`: 89 of 89
 - Last lines with no LF, sent alone, answered right: 6 of 6
 - Strict base 64 rejections where Python decodes: 7290 (5796 with unused bits before the padding not zero, 1494 with padding after a whole group, which Python 3.11 and 3.12 before 3.12.4 decode)

tests/run_tests.py

@@ -423,9 +423,10 @@ def forged_check(country, check, bban):
             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.
+# Shape and BBAN length edges, including lowercase text and letters in
+# the check-digit places. `forged` uses Python base-36 conversion, which
+# folds lowercase; those lowercase strings need not have remainder 1
+# under Lean's uppercase-only value function.
 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),
@@ -655,6 +656,13 @@ def fixed_cases():
                           pem_encoded(label, data), None, False))
             text = oracle_pem_encode(label, data) or f"-----BEGIN {label}-----\n-----END {label}-----\n"
             items.append(("pemdec", f"pemdec {text_nums(text)}", pem_decoded(text), None, False))
+    # Standard-form empty payload and concatenated messages are outside
+    # this decoder's single-message strict form.
+    for text in ("-----BEGIN X-----\n\n-----END X-----\n",
+                 "-----BEGIN X-----\nAA==\n-----END X-----\n" * 2):
+        items.append(("pemdec refusal", f"pemdec {text_nums(text)}", "none", None, False))
+    for digits, answer in (("0" * 1000 + "1", "01"), ("0" * 1000, "00")):
+        items.append(("leading zeros", f"hexenc {digits}", answer, None, False))
     for c in range(128):
         text = chr(c)
         items.append(("pctdec", f"pctdec {text_nums(text)}", decoded(oracle_pctdec(text)), None, False))