SemVer parser, printer, and section 11 precedence

.gitignore

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

Main.lean

@@ -0,0 +1,116 @@
+/-
+  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 49,46,48,46,48        prints  ok:49,46,48,46,48
+    parse 48,49,46,50,46,51      prints  none
+    cmp 49,46,48,46,48,59,50,46,48,46,48   prints  lt
+
+  The operations are `parse` and `cmp`.
+
+  `parse` takes the character codes of one version text. Its
+  answer is `ok:` and the character codes of the canonical print
+  of the parsed version, or `none` when the text is rejected.
+
+  `cmp` takes the codes of two version texts split by one code
+  59, the semicolon, which cannot appear in a version text. Its
+  answer is `lt`, `eq`, or `gt` for the precedence of the first
+  text against the second, or `none` when either 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, a
+  character code that is not a Unicode scalar value, or a `cmp`
+  request with no semicolon code in it. A line may end in LF or
+  CR LF; nothing else around a request is ignored.
+
+  The parsing, printing, and comparing here call `Semver.parse`,
+  `Semver.print`, and `Semver.compare` directly. The line
+  handling is covered by the tests, not by a proof.
+-/
+
+import Semver
+
+open Semver
+
+/-- 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)
+
+/-- Split a character list at its first semicolon. -/
+def splitSemi : List Char → Option (List Char × List Char)
+  | [] => none
+  | c :: cs =>
+    if c = ';' then some ([], cs)
+    else (splitSemi cs).map fun (a, b) => (c :: a, b)
+
+/-- 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 v => some ("ok:" ++ showCodes (print v))
+      | none => some "none"
+  | "cmp" =>
+    match toChars ns with
+    | none => none
+    | some cs =>
+      match splitSemi cs with
+      | none => none
+      | some (a, b) =>
+        match parse a, parse b with
+        | some x, some y =>
+          some (match compare x y with
+            | Ordering.lt => "lt"
+            | Ordering.eq => "eq"
+            | Ordering.gt => "gt")
+        | _, _ => 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,3 @@
+import Proofs.RoundTrip
+import Proofs.Compare
+import Proofs.Examples

Proofs/Compare.lean

@@ -0,0 +1,78 @@
+/-
+  What is proved about precedence: a version compares equal to
+  itself, and two versions that agree on the three numbers and
+  the prerelease compare equal, whatever their build metadata.
+  The second claim is the one the specification makes about build
+  metadata: it takes no part in precedence.
+
+  No claim is made here that the comparison is a full order on
+  all versions. That would take transitivity and totality proofs,
+  which this slice does not attempt.
+-/
+
+import Semver
+
+namespace Semver.Proofs
+
+open Semver
+
+theorem cmpNat_self (a : Nat) : cmpNat a a = Ordering.eq := by
+  simp [cmpNat]
+
+theorem cmpChar_self (c : Char) : cmpChar c c = Ordering.eq := by
+  simp [cmpChar]
+
+theorem cmpChars_self : ∀ (cs : List Char), cmpChars cs cs = Ordering.eq := by
+  intro cs
+  induction cs with
+  | nil => rfl
+  | cons c cs ih => simp [cmpChars, cmpChar_self, ih]
+
+theorem cmpPreId_self (id : PreId) : cmpPreId id id = Ordering.eq := by
+  cases id with
+  | num n => exact cmpNat_self n
+  | alpha cs => exact cmpChars_self cs
+
+theorem cmpPreList_self : ∀ (ids : List PreId),
+    cmpPreList ids ids = Ordering.eq := by
+  intro ids
+  induction ids with
+  | nil => rfl
+  | cons id ids ih => simp [cmpPreList, cmpPreId_self, ih]
+
+theorem cmpPre_self (ids : List PreId) : cmpPre ids ids = Ordering.eq := by
+  cases ids with
+  | nil => rfl
+  | cons id ids => exact cmpPreList_self (id :: ids)
+
+/-- A version compares equal to itself. -/
+theorem compare_self (v : Version) : compare v v = Ordering.eq := by
+  obtain ⟨M, m, p, pre, build⟩ := v
+  simp [compare, cmpNat_self, cmpPre_self]
+
+/-- Two versions that agree on the three numbers and the
+    prerelease compare equal. Build metadata is not consulted,
+    so it may differ freely. -/
+theorem compare_eq_of_fields {v w : Version}
+    (hM : v.major = w.major) (hm : v.minor = w.minor)
+    (hp : v.patch = w.patch) (hpre : v.pre = w.pre) :
+    compare v w = Ordering.eq := by
+  obtain ⟨M₁, m₁, p₁, pre₁, b₁⟩ := v
+  obtain ⟨M₂, m₂, p₂, pre₂, b₂⟩ := w
+  change M₁ = M₂ at hM
+  change m₁ = m₂ at hm
+  change p₁ = p₂ at hp
+  change pre₁ = pre₂ at hpre
+  subst hM
+  subst hm
+  subst hp
+  subst hpre
+  simp [compare, cmpNat_self, cmpPre_self]
+
+/-- Changing only the build metadata of a version leaves it
+    comparing equal to the original. -/
+theorem compare_build_irrel (v : Version) (b : List (List Char)) :
+    compare v { v with build := b } = Ordering.eq :=
+  compare_eq_of_fields rfl rfl rfl rfl
+
+end Semver.Proofs

Proofs/Examples.lean

@@ -0,0 +1,125 @@
+/-
+  Proved example cases, each closed by `decide`: the parser and
+  the comparison are programs, so a claim about two concrete
+  texts is a computation the kernel can check.
+
+  The first block is the precedence chain from section 11 of the
+  specification, step by step. The second block checks that the
+  valid example texts from the specification parse and print back
+  word for word. The third block checks that texts the grammar
+  forbids are rejected.
+-/
+
+import Semver
+
+namespace Semver.Examples
+
+open Semver
+
+/-- Compare two texts: parse both, then compare. -/
+def cmpTexts (a b : String) : Option Ordering :=
+  (parse a.toList).bind fun x => (parse b.toList).map (compare x)
+
+/-! ## The section 11 chain, step by step -/
+
+theorem chain_1 : cmpTexts "1.0.0-alpha" "1.0.0-alpha.1" = some Ordering.lt := by
+  decide
+
+theorem chain_2 : cmpTexts "1.0.0-alpha.1" "1.0.0-alpha.beta" = some Ordering.lt := by
+  decide
+
+theorem chain_3 : cmpTexts "1.0.0-alpha.beta" "1.0.0-beta" = some Ordering.lt := by
+  decide
+
+theorem chain_4 : cmpTexts "1.0.0-beta" "1.0.0-beta.2" = some Ordering.lt := by
+  decide
+
+theorem chain_5 : cmpTexts "1.0.0-beta.2" "1.0.0-beta.11" = some Ordering.lt := by
+  decide
+
+theorem chain_6 : cmpTexts "1.0.0-beta.11" "1.0.0-rc.1" = some Ordering.lt := by
+  decide
+
+theorem chain_7 : cmpTexts "1.0.0-rc.1" "1.0.0" = some Ordering.lt := by
+  decide
+
+/-- The ends of the chain, compared directly. -/
+theorem chain_ends : cmpTexts "1.0.0-alpha" "1.0.0" = some Ordering.lt := by
+  decide
+
+/-- A prerelease is lower than the release, read in the other
+    direction as well. -/
+theorem chain_back : cmpTexts "1.0.0" "1.0.0-rc.1" = some Ordering.gt := by
+  decide
+
+/-- Numbers compare by value, not by text: 11 is above 2. -/
+theorem numeric_by_value : cmpTexts "1.0.0-beta.11" "1.0.0-beta.2" =
+    some Ordering.gt := by
+  decide
+
+/-- The core numbers decide first: a higher patch wins over any
+    prerelease question. -/
+theorem core_first : cmpTexts "2.1.1" "2.1.0" = some Ordering.gt := by
+  decide
+
+/-- Build metadata changes nothing in a comparison of two parsed
+    texts. -/
+theorem build_ignored : cmpTexts "1.0.0+build.1" "1.0.0+other.2" =
+    some Ordering.eq := by
+  decide
+
+/-! ## Valid texts from the specification parse and print back -/
+
+theorem valid_alpha : (parse "1.0.0-alpha".toList).map print =
+    some "1.0.0-alpha".toList := by decide
+
+theorem valid_alpha_1 : (parse "1.0.0-alpha.1".toList).map print =
+    some "1.0.0-alpha.1".toList := by decide
+
+theorem valid_037 : (parse "1.0.0-0.3.7".toList).map print =
+    some "1.0.0-0.3.7".toList := by decide
+
+theorem valid_xyz : (parse "1.0.0-x-y-z.-".toList).map print =
+    some "1.0.0-x-y-z.-".toList := by decide
+
+theorem valid_build_001 : (parse "1.0.0-alpha+001".toList).map print =
+    some "1.0.0-alpha+001".toList := by decide
+
+theorem valid_build_time : (parse "1.0.0+20130313144700".toList).map print =
+    some "1.0.0+20130313144700".toList := by decide
+
+theorem valid_build_sha : (parse "1.0.0-beta+exp.sha.5114f85".toList).map print =
+    some "1.0.0-beta+exp.sha.5114f85".toList := by decide
+
+theorem valid_plain : (parse "1.0.0".toList).map print =
+    some "1.0.0".toList := by decide
+
+/-! ## Texts the grammar forbids are rejected -/
+
+theorem invalid_leading_zero_major : parse "01.2.3".toList = none := by decide
+
+theorem invalid_leading_zero_minor : parse "1.02.3".toList = none := by decide
+
+theorem invalid_leading_zero_pre : parse "1.0.0-01".toList = none := by decide
+
+theorem invalid_empty_pre_id : parse "1.0.0-alpha..1".toList = none := by decide
+
+theorem invalid_empty_pre_and_build : parse "1.0.0-+".toList = none := by decide
+
+theorem invalid_empty_build : parse "1.0.0+".toList = none := by decide
+
+theorem invalid_empty_pre : parse "1.0.0-".toList = none := by decide
+
+theorem invalid_missing_patch : parse "1.0".toList = none := by decide
+
+theorem invalid_extra_part : parse "1.0.0.0".toList = none := by decide
+
+theorem invalid_letter_prefix : parse "v1.2.3".toList = none := by decide
+
+theorem invalid_underscore : parse "1.0.0-alpha_beta".toList = none := by decide
+
+theorem invalid_empty : parse "".toList = none := by decide
+
+theorem invalid_empty_core_part : parse "1..2".toList = none := by decide
+
+end Semver.Examples