First slice: SemVer 2.0.0 parser, printer and precedence, proved

.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

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

Main.lean

@@ -0,0 +1,118 @@
+/-
+  Command line front end.
+
+    semver check VERSION...
+
+  prints, for each version, its printed form, or `invalid`, and exits
+  with 1 when any is invalid.
+
+    semver serve
+
+  answers requests on standard input, one per line, for the
+  differential tests. A string is sent as the hex digits of its UTF-8
+  bytes, so that any character, a line break included, can be sent.
+
+    parse HEX         prints  OK, then tab-separated: the printed form,
+                      major, minor, patch, the pre-release identifiers
+                      and the build identifiers; or REJECT. Each
+                      pre-release identifier is `n:` and its number or
+                      `a:` and its text, joined by `,`; the build
+                      identifiers are joined by `,`.
+    compare HEX HEX   prints  <, = or >, or REJECT when either string
+                      is not a version
+
+  A malformed request prints `error`: an unknown operation, hex digits
+  that are not in pairs, or bytes that are not UTF-8. A request line
+  may end in LF or CR LF.
+
+  Every answer comes from the proved functions in `SemVer/`: `parse`,
+  `Version.print` and `Version.compare`. The hex decoding and the
+  request handling here are covered by the tests, not by a proof.
+-/
+
+import SemVer
+
+open SemVer
+
+def hexValue (c : Char) : Option Nat :=
+  if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - '0'.toNat)
+  else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 'a'.toNat + 10)
+  else none
+
+def hexBytes : List Char → Option (List UInt8)
+  | [] => some []
+  | a :: b :: rest => do
+    let hi ← hexValue a
+    let lo ← hexValue b
+    let bs ← hexBytes rest
+    pure ((hi * 16 + lo).toUInt8 :: bs)
+  | [_] => none
+
+/-- The string whose UTF-8 bytes the hex digits give. -/
+def fromHex (h : String) : Option String := do
+  let bs ← hexBytes h.toList
+  String.fromUTF8? ⟨bs.toArray⟩
+
+def identField : Ident → String
+  | .num n => "n:" ++ toString n
+  | .alnum s => "a:" ++ s
+
+def fields (v : Version) : List String :=
+  [v.print, toString v.major, toString v.minor, toString v.patch,
+   ",".intercalate (v.pre.map identField), ",".intercalate v.build]
+
+def showOrdering : Ordering → String
+  | .lt => "<"
+  | .eq => "="
+  | .gt => ">"
+
+/-- The answer to one request line, or `none` when it is malformed. -/
+def request (line : String) : Option String :=
+  match line.splitOn " " with
+  | ["parse", h] => do
+    let s ← fromHex h
+    pure <| match parse s with
+      | some v => "\t".intercalate ("OK" :: fields v)
+      | none => "REJECT"
+  | ["compare", ha, hb] => do
+    let a ← fromHex ha
+    let b ← fromHex hb
+    pure <| match parse a, parse b with
+      | some va, some vb => showOrdering (va.compare vb)
+      | _, _ => "REJECT"
+  | _ => 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 serve : IO Unit := do
+  let stdin ← IO.getStdin
+  let stdout ← IO.getStdout
+  repeat
+    let line ← stdin.getLine
+    if line.isEmpty then break
+    stdout.putStrLn ((request (chomp line)).getD "error")
+
+def check (args : List String) : IO UInt32 := do
+  let mut code : UInt32 := 0
+  for s in args do
+    match parse s with
+    | some v => IO.println v.print
+    | none =>
+      IO.println s!"invalid\t{s}"
+      code := 1
+  return code
+
+def usage : String :=
+  "usage: semver check VERSION...\n       semver serve"
+
+def main (args : List String) : IO UInt32 := do
+  match args with
+  | "check" :: rest@(_ :: _) => check rest
+  | ["serve"] => serve; return 0
+  | _ => IO.eprintln usage; return 2

Proofs.lean

@@ -0,0 +1 @@
+import Proofs.Main

Proofs/Chars.lean

@@ -0,0 +1,66 @@
+/-
+  Character classes: the code's `isDigit` and `isIdentChar` against the
+  specification's `Spec.Digit` and `Spec.IdentChar`, and the digit
+  characters against their values.
+-/
+
+import SemVer
+import Spec.Defs
+
+open SemVer
+
+namespace SemVer.Proofs
+
+theorem le_iff_toNat {a b : Char} : a ≤ b ↔ a.toNat ≤ b.toNat := by
+  rw [Char.le_def, UInt32.le_iff_toNat_le]; rfl
+
+theorem digit_iff (c : Char) : Spec.Digit c ↔ 48 ≤ c.toNat ∧ c.toNat ≤ 57 := by
+  simp only [Spec.Digit, le_iff_toNat]; rfl
+
+theorem positiveDigit_iff (c : Char) : Spec.PositiveDigit c ↔ 49 ≤ c.toNat ∧ c.toNat ≤ 57 := by
+  simp only [Spec.PositiveDigit, le_iff_toNat]; rfl
+
+theorem letter_iff (c : Char) :
+    Spec.Letter c ↔ (65 ≤ c.toNat ∧ c.toNat ≤ 90) ∨ (97 ≤ c.toNat ∧ c.toNat ≤ 122) := by
+  simp only [Spec.Letter, le_iff_toNat]; rfl
+
+theorem eq_hyphen_iff (c : Char) : c = '-' ↔ c.toNat = 45 := by
+  rw [← Char.toNat_inj]; rfl
+
+theorem isDigit_iff (c : Char) : isDigit c = true ↔ Spec.Digit c := by
+  simp [isDigit, Spec.Digit]
+
+theorem isIdentChar_iff (c : Char) : isIdentChar c = true ↔ Spec.IdentChar c := by
+  simp only [isIdentChar, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq, beq_iff_eq,
+    isDigit_iff, Spec.IdentChar, Spec.NonDigit, Spec.Letter, or_assoc]
+
+theorem nonDigit_iff (c : Char) : Spec.NonDigit c ↔ Spec.IdentChar c ∧ ¬ Spec.Digit c := by
+  simp only [Spec.IdentChar, Spec.NonDigit, letter_iff, digit_iff, eq_hyphen_iff]
+  omega
+
+theorem positiveDigit_iff_digit (c : Char) :
+    Spec.PositiveDigit c ↔ Spec.Digit c ∧ c ≠ '0' := by
+  rw [positiveDigit_iff, digit_iff, Ne, ← Char.toNat_inj]
+  show _ ↔ _ ∧ ¬ c.toNat = 48
+  omega
+
+theorem digit_identChar {c : Char} (h : Spec.Digit c) : Spec.IdentChar c := Or.inl h
+
+/-- A digit character is the character for its value. -/
+theorem digitChar_toNat {c : Char} (h : Spec.Digit c) : Nat.digitChar (c.toNat - 48) = c := by
+  rw [digit_iff] at h
+  rw [← Char.toNat_inj, Nat.toNat_digitChar_of_lt_ten (by omega)]
+  omega
+
+theorem digit_digitChar {n : Nat} (h : n < 10) : Spec.Digit (Nat.digitChar n) := by
+  rw [digit_iff, Nat.toNat_digitChar_of_lt_ten h]; omega
+
+/-- Characters the separators of the format use are not identifier
+    characters. -/
+theorem not_identChar_dot : ¬ Spec.IdentChar '.' := by decide
+theorem not_identChar_plus : ¬ Spec.IdentChar '+' := by decide
+theorem not_digit_hyphen : ¬ Spec.Digit '-' := by decide
+theorem not_digit_dot : ¬ Spec.Digit '.' := by decide
+theorem not_digit_plus : ¬ Spec.Digit '+' := by decide
+
+end SemVer.Proofs