XML safe subset parser and printer, with a proved round trip

.github/workflows/bar.yml

@@ -0,0 +1,21 @@
+name: verified bar
+
+on:
+  push:
+  pull_request:
+  # Rerun when the spec reviewer approves, or an approval is dismissed.
+  pull_request_review:
+    types: [submitted, dismissed]
+
+jobs:
+  bar:
+    # pull-requests: read lets the check confirm the spec approval on GitHub.
+    permissions:
+      contents: read
+      pull-requests: read
+    # Both lines pin the same commit of Proven-Commons/mission: bar v2, as
+    # proposed in its pull request #2. Move both to a release tag once
+    # mission publishes one.
+    uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2
+    with:
+      bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2

.gitignore

@@ -1 +1,2 @@
 .lake/
+__pycache__/

Main.lean

@@ -0,0 +1,87 @@
+/-
+  Command line front end, used by the tests.
+
+  Reads one request per line and prints one answer per line. A
+  request is an operation and its input as comma-separated decimal
+  character codes.
+
+    parse 60,97,62,120,60,47,97,62   prints  ok:60,97,62,120,60,47,97,62
+    parse 60,97,47,62                prints  ok:60,97,47,62
+    parse 120                        prints  none
+
+  The one operation is `parse`. Its input is the character codes of
+  an XML text in the safe subset. Its answer is `ok:` and the
+  character codes of the canonical print of the parsed document,
+  or `none` when the text is rejected.
+
+  A request is an operation, then optionally one space and its
+  numbers; with no numbers after the space, the input is empty. A
+  malformed request prints `error`: any other line, an unknown
+  operation, a number that is not plain decimal digits, 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 parsing and printing here call `Xml.parse` and `Xml.print`
+  directly. The line handling is covered by the tests, not by a
+  proof.
+-/
+
+import Xml
+
+open Xml
+
+/-- A number in plain decimal digits. Longer numbers than any
+    character code are refused before they are converted, since
+    that takes time quadratic in their length. -/
+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?
+
+/-- The comma-separated numbers in `s`. -/
+def numbers (s : String) : Option (List Nat) :=
+  if s.isEmpty then some [] else (s.splitOn ",").mapM number
+
+def toChars (ns : List Nat) : Option (List Char) :=
+  ns.mapM fun n => if n.isValidChar then some (Char.ofNat n) else none
+
+def showCodes (cs : List Char) : String :=
+  ",".intercalate (cs.map fun c => toString c.toNat)
+
+/-- The answer to one request, or `none` when the request is
+    malformed. -/
+def answer (op : String) (ns : List Nat) : Option String :=
+  match op with
+  | "parse" =>
+    match toChars ns with
+    | none => none
+    | some cs =>
+      match parse cs with
+      | some d => some ("ok:" ++ showCodes (print d))
+      | none => some "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
+  | [op] => answer op []
+  | [op, arg] => numbers arg >>= answer op
+  | _ => none
+
+/-- The line without its line ending: LF, or CR LF. -/
+def chomp (line : String) : String :=
+  let cs := line.toList
+  if cs.getLast? = some '\n' then
+    let cs := cs.dropLast
+    String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs)
+  else line
+
+def main : IO Unit := do
+  let stdin ← IO.getStdin
+  let stdout ← IO.getStdout
+  repeat
+    let line ← stdin.getLine
+    if line.isEmpty then break
+    let line := chomp line
+    stdout.putStrLn ((request line).getD "error")

Proofs.lean

@@ -0,0 +1,2 @@
+import Proofs.RoundTrip
+import Proofs.SpecProofs