From 33a588befcde025952ac60134755f7436794c867 Mon Sep 17 00:00:00 2001 From: shah Date: Sun, 25 Oct 2026 11:14:01 -0500 Subject: [PATCH] Add SemVer parser, printer, and precedence, with proved round trip and chain --- .gitignore | 2 + Main.lean | 116 +++++++ Proofs.lean | 3 + Proofs/Compare.lean | 78 +++++ Proofs/Examples.lean | 125 +++++++ Proofs/RoundTrip.lean | 768 ++++++++++++++++++++++++++++++++++++++++++ README.md | 63 +++- SPEC.md | 62 ++++ Semver.lean | 2 + Semver/Parse.lean | 139 ++++++++ Semver/Verify.lean | 23 ++ Semver/Version.lean | 216 ++++++++++++ lake-manifest.json | 6 + lakefile.toml | 13 + lean-toolchain | 1 + tests/TEST-RESULTS.md | 17 + tests/run_tests.py | 485 ++++++++++++++++++++++++++ 17 files changed, 2118 insertions(+), 1 deletion(-) create mode 100644 .gitignore create mode 100644 Main.lean create mode 100644 Proofs.lean create mode 100644 Proofs/Compare.lean create mode 100644 Proofs/Examples.lean create mode 100644 Proofs/RoundTrip.lean create mode 100644 SPEC.md create mode 100644 Semver.lean create mode 100644 Semver/Parse.lean create mode 100644 Semver/Verify.lean create mode 100644 Semver/Version.lean create mode 100644 lake-manifest.json create mode 100644 lakefile.toml create mode 100644 lean-toolchain create mode 100644 tests/TEST-RESULTS.md create mode 100644 tests/run_tests.py diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..ae73679 --- /dev/null +++ b/.gitignore @@ -0,0 +1,2 @@ +.lake/ +__pycache__/ diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..4a3c0ee --- /dev/null +++ b/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") diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..da6738a --- /dev/null +++ b/Proofs.lean @@ -0,0 +1,3 @@ +import Proofs.RoundTrip +import Proofs.Compare +import Proofs.Examples diff --git a/Proofs/Compare.lean b/Proofs/Compare.lean new file mode 100644 index 0000000..b4ebfdf --- /dev/null +++ b/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 diff --git a/Proofs/Examples.lean b/Proofs/Examples.lean new file mode 100644 index 0000000..992ff56 --- /dev/null +++ b/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 diff --git a/Proofs/RoundTrip.lean b/Proofs/RoundTrip.lean new file mode 100644 index 0000000..bcdb7f8 --- /dev/null +++ b/Proofs/RoundTrip.lean @@ -0,0 +1,768 @@ +/- + The round trip: parsing the printed form of a well formed + version gives the version back. + + The proof follows the shape of the printer. Numbers first: the + digits the printer writes read back to the same number. Then one + prerelease identifier, then a dot separated list of them, then + build identifiers the same way, then the whole version. +-/ + +import Semver + +namespace Semver.Proofs + +open Semver + +/-! ## Digit characters -/ + +theorem digitChar_toNat {d : Nat} (h : d < 10) : (digitChar d).toNat = d + 48 := by + have h9 : d = 0 ∨ d = 1 ∨ d = 2 ∨ d = 3 ∨ d = 4 ∨ d = 5 ∨ d = 6 ∨ d = 7 ∨ + d = 8 ∨ d = 9 := by omega + rcases h9 with rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> rfl + +theorem isDigit_digitChar {d : Nat} (h : d < 10) : isDigit (digitChar d) = true := by + rw [isDigit_iff] + show 48 ≤ (digitChar d).toNat ∧ (digitChar d).toNat ≤ 57 + rw [digitChar_toNat h] + constructor <;> omega + +theorem digitChar_ne_zero {d : Nat} (h : d < 10) (hd : d ≠ 0) : digitChar d ≠ '0' := by + intro hcon + have h1 : (digitChar d).toNat = ('0').toNat := congrArg Char.toNat hcon + rw [digitChar_toNat h] at h1 + simp at h1 + omega + +/-! ## The digits of a number -/ + +/-- The value of a list of digits, least significant first. -/ +def digitsVal (ds : List Nat) : Nat := ds.foldr (fun d acc => d + 10 * acc) 0 + +theorem digitsRevAux_zero (f : Nat) : digitsRevAux f 0 = [] := by + cases f <;> rfl + +/-- Everything the printer needs to know about the digit builder, + in one induction on the fuel: the digits read back to the + number, every digit is below 10, and a positive number ends + (at the most significant side) in a nonzero digit. -/ +theorem digitsRevAux_spec : ∀ (f n : Nat), n < f → + digitsVal (digitsRevAux f n) = n ∧ + (∀ d ∈ digitsRevAux f n, d < 10) ∧ + (n = 0 ∨ ∃ ds d, digitsRevAux f n = ds ++ [d] ∧ d ≠ 0) := by + intro f + induction f with + | zero => intro n hn; omega + | succ f ih => + intro n hn + cases n with + | zero => + have hz : digitsRevAux (f + 1) 0 = [] := digitsRevAux_zero _ + refine ⟨?_, ?_, Or.inl rfl⟩ + · rw [hz] + rfl + · intro d hd + rw [hz] at hd + simp at hd + | succ n => + have hlt : (n + 1) / 10 < f := by + by_cases h0 : (n + 1) / 10 = 0 + · omega + · have h2 : (n + 1) / 10 < n + 1 := Nat.div_lt_self (by omega) (by omega) + omega + obtain ⟨hval, hmem, hform⟩ := ih ((n + 1) / 10) hlt + have hmod : (n + 1) % 10 < 10 := Nat.mod_lt _ (by omega) + refine ⟨?_, ?_, ?_⟩ + · show digitsVal ((n + 1) % 10 :: digitsRevAux f ((n + 1) / 10)) = n + 1 + show (n + 1) % 10 + 10 * digitsVal (digitsRevAux f ((n + 1) / 10)) = n + 1 + rw [hval] + have := Nat.div_add_mod (n + 1) 10 + omega + · intro d hd + have hd' : d ∈ (n + 1) % 10 :: digitsRevAux f ((n + 1) / 10) := hd + rcases List.mem_cons.mp hd' with rfl | hd'' + · exact hmod + · exact hmem d hd'' + · by_cases h0 : (n + 1) / 10 = 0 + · refine Or.inr ⟨[], (n + 1) % 10, ?_, ?_⟩ + · show digitsRevAux (f + 1) (n + 1) = [] ++ [(n + 1) % 10] + show (n + 1) % 10 :: digitsRevAux f ((n + 1) / 10) = [(n + 1) % 10] + rw [h0, digitsRevAux_zero] + · have hlt10 : n + 1 < 10 := by + rcases Nat.lt_or_ge (n + 1) 10 with hlt | hge + · exact hlt + · have hpos := Nat.div_pos hge (by omega : 0 < 10) + omega + rw [Nat.mod_eq_of_lt hlt10] + omega + · rcases hform with h | ⟨ds, d, hds, hd⟩ + · exact absurd h h0 + · refine Or.inr ⟨(n + 1) % 10 :: ds, d, ?_, hd⟩ + show (n + 1) % 10 :: digitsRevAux f ((n + 1) / 10) = + ((n + 1) % 10 :: ds) ++ [d] + rw [hds] + rfl + +/-- The specification of `digitsRev`, from the fuelled builder. -/ +theorem digitsRev_spec (n : Nat) : + digitsVal (digitsRev n) = n ∧ + (∀ d ∈ digitsRev n, d < 10) ∧ + (n = 0 ∨ ∃ ds d, digitsRev n = ds ++ [d] ∧ d ≠ 0) := + digitsRevAux_spec (n + 1) n (Nat.lt_succ_self n) + +/-! ## Reading digits back -/ + +/-- Reading a digit list with one more digit at the end: the + fold multiplies what it had and adds the digit. -/ +theorem digitsValue_append_single (ds : List Char) (c : Char) : + digitsValue (ds ++ [c]) = digitsValue ds * 10 + (c.toNat - 48) := by + unfold digitsValue + rw [List.foldl_append] + rfl + +/-- Reading the printed digits of a digit list gives the value of + the list. Induction on the digit list, least significant + first: the reversed print puts the head digit last, and the + fold that reads digits most significant first turns appending + one digit into a multiply and an add. -/ +theorem digitsValue_printDigits : ∀ (ds : List Nat), (∀ d ∈ ds, d < 10) → + digitsValue (ds.reverse.map digitChar) = digitsVal ds := by + intro ds + induction ds with + | nil => intro _; rfl + | cons d ds ih => + intro hmem + have hd : d < 10 := hmem d (by simp) + have hds : ∀ d' ∈ ds, d' < 10 := fun d' hd' => hmem d' (by simp [hd']) + rw [List.reverse_cons] + show digitsValue ((ds.reverse ++ [d]).map digitChar) = digitsVal (d :: ds) + rw [List.map_append, List.map_singleton, digitsValue_append_single, ih hds] + show digitsVal ds * 10 + ((digitChar d).toNat - 48) = d + 10 * digitsVal ds + rw [digitChar_toNat hd] + have h48 : d + 48 - 48 = d := by omega + rw [h48] + omega + +/-- The printed form of a number reads back to the number. -/ +theorem digitsValue_printNat (n : Nat) : digitsValue (printNat n) = n := by + by_cases h0 : n = 0 + · subst h0 + rfl + · obtain ⟨hval, hmem, _⟩ := digitsRev_spec n + have hprint : printNat n = (digitsRev n).reverse.map digitChar := by + unfold printNat + rw [if_neg h0] + rw [hprint, digitsValue_printDigits (digitsRev n) hmem, hval] + +/-- Every character the printer writes for a number is a digit. -/ +theorem printNat_isDigit {n : Nat} : ∀ c ∈ printNat n, isDigit c = true := by + by_cases h0 : n = 0 + · subst h0 + intro c hc + simp [printNat] at hc + subst hc + decide + · obtain ⟨_, hmem, _⟩ := digitsRev_spec n + intro c hc + simp [printNat, h0] at hc + obtain ⟨d, hd, rfl⟩ := hc + exact isDigit_digitChar (hmem d hd) + +/-- Every character the printer writes for a number is an + identifier character. -/ +theorem printNat_isIdChar {n : Nat} : ∀ c ∈ printNat n, isIdChar c = true := by + intro c hc + rw [isIdChar_iff] + exact Or.inl (isDigit_iff.mp (printNat_isDigit c hc)) + +/-- The number text check passes on any nonempty digit text + whose first character is not 0, and on the text 0 itself. + Stated for a text that does not start with 0. -/ +theorem numTextOk_of_head {ds : List Char} (hne : ds ≠ []) + (h : ds.head? ≠ some '0') : numTextOk ds = true := by + cases hds : ds with + | nil => exact absurd hds hne + | cons c cs => + subst hds + have hne' : (c :: cs).isEmpty = false := rfl + have hhead : (c :: cs).head? = some c := rfl + rw [hhead] at h + have hbeq : ((c :: cs).head? == some '0') = false := by + rw [hhead] + cases hcc : (some c == some '0') with + | false => rfl + | true => + simp only [beq_iff_eq] at hcc + exact absurd hcc h + show numTextOk (c :: cs) = true + show (!(c :: cs).isEmpty && (((c :: cs).length == 1) || + !((c :: cs).head? == some '0'))) = true + rw [hne', hbeq] + simp + +/-- The print of a number is never empty. -/ +theorem printNat_ne_nil (n : Nat) : printNat n ≠ [] := by + by_cases h0 : n = 0 + · subst h0 + simp [printNat] + · obtain ⟨_, _, hform⟩ := digitsRev_spec n + rcases hform with h | ⟨ds, d, hds, _⟩ + · omega + · have hprint : printNat n = digitChar d :: (ds.reverse.map digitChar) := by + unfold printNat + rw [if_neg h0, hds] + simp [List.reverse_append] + rw [hprint] + simp + +/-- The number text check passes on a printed number. -/ +theorem numTextOk_printNat (n : Nat) : numTextOk (printNat n) = true := by + by_cases h0 : n = 0 + · subst h0 + rfl + · obtain ⟨_, hmem, hform⟩ := digitsRev_spec n + rcases hform with h | ⟨ds, d, hds, hd⟩ + · omega + · have hprint : printNat n = digitChar d :: (ds.reverse.map digitChar) := by + unfold printNat + rw [if_neg h0, hds] + simp [List.reverse_append] + have hlt : d < 10 := hmem d (by rw [hds]; simp) + have hhead : (printNat n).head? ≠ some '0' := by + rw [hprint] + simp [digitChar_ne_zero hlt hd] + exact numTextOk_of_head (printNat_ne_nil n) hhead + +/-! ## Taking runs from the front -/ + +/-- A condition on what follows a printed part: nothing, or a + character that ends the run. -/ +def HeadOk (test : Char → Bool) (rest : List Char) : Prop := + match rest with + | [] => True + | c :: _ => test c = false + +theorem takeDigits_append (ds rest : List Char) (hall : ∀ c ∈ ds, isDigit c = true) + (h : HeadOk isDigit rest) : takeDigits (ds ++ rest) = (ds, rest) := by + induction ds with + | nil => + cases rest with + | nil => rfl + | cons c cs => + have hc : isDigit c = false := h + show takeDigits (c :: cs) = ([], c :: cs) + simp [takeDigits, hc] + | cons d ds ih => + have hd : isDigit d = true := hall d (by simp) + have hds : ∀ c ∈ ds, isDigit c = true := fun c hc => hall c (by simp [hc]) + show takeDigits (d :: (ds ++ rest)) = (d :: ds, rest) + simp [takeDigits, hd, ih hds] + +theorem takeIdChars_append (ds rest : List Char) (hall : ∀ c ∈ ds, isIdChar c = true) + (h : HeadOk isIdChar rest) : takeIdChars (ds ++ rest) = (ds, rest) := by + induction ds with + | nil => + cases rest with + | nil => rfl + | cons c cs => + have hc : isIdChar c = false := h + show takeIdChars (c :: cs) = ([], c :: cs) + simp [takeIdChars, hc] + | cons d ds ih => + have hd : isIdChar d = true := hall d (by simp) + have hds : ∀ c ∈ ds, isIdChar c = true := fun c hc => hall c (by simp [hc]) + show takeIdChars (d :: (ds ++ rest)) = (d :: ds, rest) + simp [takeIdChars, hd, ih hds] + +/-! ## Reading the printed parts back -/ + +/-- A printed number reads back as the number, over any tail that + does not start with a digit. -/ +theorem parseCoreNum_printNat (n : Nat) (rest : List Char) (h : HeadOk isDigit rest) : + parseCoreNum (printNat n ++ rest) = some (n, rest) := by + simp [parseCoreNum, takeDigits_append (printNat n) rest printNat_isDigit h, + numTextOk_printNat, digitsValue_printNat] + +/-- The text of a numeric identifier reads back as that + identifier. -/ +theorem classifyPreId_printNat (n : Nat) : classifyPreId (printNat n) = some (.num n) := by + have hall : (printNat n).all isDigit = true := by + rw [List.all_eq_true] + exact printNat_isDigit + simp [classifyPreId, hall, numTextOk_printNat, digitsValue_printNat] + +/-- The text of an alphanumeric identifier reads back as that + identifier. -/ +theorem classifyPreId_alpha (cs : List Char) (h : WFAlpha cs) : + classifyPreId cs = some (.alpha cs) := by + obtain ⟨hne, hchars, ⟨c, hc, hcd⟩⟩ := h + unfold classifyPreId + have hnotall : cs.all isDigit = false := by + cases hall : cs.all isDigit with + | false => rfl + | true => + rw [List.all_eq_true] at hall + exact absurd (isDigit_iff.mp (hall c hc)) hcd + simp [hnotall] + +/-- A printed prerelease identifier reads back, over a tail that + does not start with an identifier character. -/ +theorem parsePreId_printPreId (id : PreId) (h : WFPreId id) (rest : List Char) + (hr : HeadOk isIdChar rest) : + parsePreId (printPreId id ++ rest) = some (id, rest) := by + cases id with + | num n => + show parsePreId (printNat n ++ rest) = some (PreId.num n, rest) + simp [parsePreId, takeIdChars_append (printNat n) rest printNat_isIdChar hr, + classifyPreId_printNat, printNat_ne_nil] + | alpha cs => + show parsePreId (cs ++ rest) = some (PreId.alpha cs, rest) + simp [parsePreId, takeIdChars_append cs rest + (fun c hc => isIdChar_iff.mpr (h.2.1 c hc)) hr, classifyPreId_alpha cs h, h.1] + +/-- A printed build identifier reads back, over a tail that does + not start with an identifier character. -/ +theorem parseBuildId_print (cs : List Char) (h : WFBuildId cs) (rest : List Char) + (hr : HeadOk isIdChar rest) : + parseBuildId (cs ++ rest) = some (cs, rest) := by + simp [parseBuildId, takeIdChars_append cs rest + (fun c hc => isIdChar_iff.mpr (h.2 c hc)) hr, h.1] + +/-! ## The delimiter characters end every run -/ + +theorem headOk_dot_digit (r : List Char) : HeadOk isDigit ('.' :: r) := by + show isDigit '.' = false + decide + +theorem headOk_minus_digit (r : List Char) : HeadOk isDigit ('-' :: r) := by + show isDigit '-' = false + decide + +theorem headOk_plus_digit (r : List Char) : HeadOk isDigit ('+' :: r) := by + show isDigit '+' = false + decide + +theorem headOk_nil (test : Char → Bool) : HeadOk test [] := trivial + +theorem headOk_dot_idChar (r : List Char) : HeadOk isIdChar ('.' :: r) := by + show isIdChar '.' = false + decide + +theorem headOk_plus_idChar (r : List Char) : HeadOk isIdChar ('+' :: r) := by + show isIdChar '+' = false + decide + +/-- A tail that starts with an appended hyphen part still starts + with the hyphen. -/ +theorem headOk_minus_append (J X : List Char) : + HeadOk isDigit (('-' :: J) ++ X) := by + show isDigit '-' = false + decide + +/-! ## Lengths of joined prints -/ + +/-- A joined list of nonempty parts is at least as long as the + number of parts, less the dots it saves at the end: the length + of the join plus one is at least the number of parts. -/ +theorem joinDots_length : ∀ (ps : List (List Char)), (∀ p ∈ ps, p ≠ []) → + ps.length ≤ (joinDots ps).length + 1 := by + intro ps + induction ps with + | nil => intro _; exact Nat.zero_le _ + | cons p ps ih => + intro hne + cases ps with + | nil => + show 1 ≤ (joinDots [p]).length + 1 + show 1 ≤ p.length + 1 + omega + | cons q qs => + have ih' := ih (fun x hx => hne x (by simp [hx])) + have hp : 0 < p.length := by + cases p with + | nil => exact absurd rfl (hne _ (by simp)) + | cons c cs => simp + show (p :: q :: qs).length ≤ (joinDots (p :: q :: qs)).length + 1 + show (q :: qs).length + 1 ≤ (p ++ '.' :: joinDots (q :: qs)).length + 1 + rw [List.length_append] + simp only [List.length_cons] at ih' ⊢ + omega + +/-- A printed prerelease identifier is never empty. -/ +theorem printPreId_ne_nil (id : PreId) (h : WFPreId id) : printPreId id ≠ [] := by + cases id with + | num n => exact printNat_ne_nil n + | alpha cs => exact h.1 + +/-- The tail after a printed list must not start with a dot: a + dot would open another identifier. Named so that statements + share one form. -/ +def NotDotHead (rest : List Char) : Prop := + match rest with + | [] => True + | c :: _ => c ≠ '.' + +/-! ## Reading printed lists back -/ + +/-- A printed list of prerelease identifiers reads back. The tail + after the list must not start with an identifier character, + and must not start with a dot either: a dot would open another + identifier. Induction on the fuel. -/ +theorem parsePreIdsGo_print : ∀ (fuel : Nat) (ids : List PreId) (rest : List Char), + ids ≠ [] → (∀ id ∈ ids, WFPreId id) → HeadOk isIdChar rest → + NotDotHead rest → + ids.length ≤ fuel → + parsePreIdsGo fuel (joinDots (ids.map printPreId) ++ rest) = some (ids, rest) := by + intro fuel + induction fuel with + | zero => + intro ids rest hne _ _ _ hlen + cases ids with + | nil => exact absurd rfl hne + | cons id ids => simp at hlen + | succ f ih => + intro ids rest hne hwf hr hrd hlen + cases ids with + | nil => exact absurd rfl hne + | cons id ids' => + have hid : WFPreId id := hwf id (by simp) + have hwf' : ∀ x ∈ ids', WFPreId x := fun x hx => hwf x (by simp [hx]) + cases ids' with + | nil => + show parsePreIdsGo (f + 1) (printPreId id ++ rest) = some ([id], rest) + show (match parsePreId (printPreId id ++ rest) with + | none => none + | some (x, rest') => + if rest'.head? = some '.' then + match parsePreIdsGo f rest'.tail with + | some (ids, rest'') => some (x :: ids, rest'') + | none => none + else some ([x], rest')) = some ([id], rest) + rw [parsePreId_printPreId id hid rest hr] + cases rest with + | nil => rfl + | cons c cs => + have hc : c ≠ '.' := hrd + show (if (c :: cs).head? = some '.' then + match parsePreIdsGo f (c :: cs).tail with + | some (ids, rest'') => some (id :: ids, rest'') + | none => none + else some ([id], c :: cs)) = some ([id], c :: cs) + rw [if_neg (by simp [hc])] + | cons id₂ ids'' => + have hwf'' : ∀ x ∈ (id₂ :: ids''), WFPreId x := hwf' + show parsePreIdsGo (f + 1) + ((printPreId id ++ '.' :: joinDots ((id₂ :: ids'').map printPreId)) ++ rest) = + some (id :: id₂ :: ids'', rest) + rw [List.append_assoc] + show (match parsePreId + (printPreId id ++ ('.' :: (joinDots ((id₂ :: ids'').map printPreId) ++ rest))) with + | none => none + | some (x, rest') => + if rest'.head? = some '.' then + match parsePreIdsGo f rest'.tail with + | some (ids, rest'') => some (x :: ids, rest'') + | none => none + else some ([x], rest')) = some (id :: id₂ :: ids'', rest) + rw [parsePreId_printPreId id hid _ (headOk_dot_idChar _)] + show (if ('.' :: (joinDots ((id₂ :: ids'').map printPreId) ++ rest)).head? = + some '.' then + match parsePreIdsGo f + ('.' :: (joinDots ((id₂ :: ids'').map printPreId) ++ rest)).tail with + | some (ids, rest'') => some (id :: ids, rest'') + | none => none + else some ([id], '.' :: (joinDots ((id₂ :: ids'').map printPreId) ++ rest))) = + some (id :: id₂ :: ids'', rest) + rw [if_pos (by rfl : List.head? + ('.' :: (joinDots ((id₂ :: ids'').map printPreId) ++ rest)) = some '.')] + show (match parsePreIdsGo f (joinDots ((id₂ :: ids'').map printPreId) ++ rest) with + | some (ids, rest'') => some (id :: ids, rest'') + | none => none) = some (id :: id₂ :: ids'', rest) + rw [ih (id₂ :: ids'') rest (by simp) hwf'' hr hrd (by + simp at hlen + omega)] + +/-- A printed list of build identifiers reads back. The same + shape as the prerelease list. -/ +theorem parseBuildIdsGo_print : ∀ (fuel : Nat) (ids : List (List Char)) + (rest : List Char), + ids ≠ [] → (∀ b ∈ ids, WFBuildId b) → HeadOk isIdChar rest → + NotDotHead rest → + ids.length ≤ fuel → + parseBuildIdsGo fuel (joinDots ids ++ rest) = some (ids, rest) := by + intro fuel + induction fuel with + | zero => + intro ids rest hne _ _ _ hlen + cases ids with + | nil => exact absurd rfl hne + | cons id ids => simp at hlen + | succ f ih => + intro ids rest hne hwf hr hrd hlen + cases ids with + | nil => exact absurd rfl hne + | cons id ids' => + have hid : WFBuildId id := hwf id (by simp) + have hwf' : ∀ x ∈ ids', WFBuildId x := fun x hx => hwf x (by simp [hx]) + cases ids' with + | nil => + show parseBuildIdsGo (f + 1) (id ++ rest) = some ([id], rest) + show (match parseBuildId (id ++ rest) with + | none => none + | some (x, rest') => + if rest'.head? = some '.' then + match parseBuildIdsGo f rest'.tail with + | some (ids, rest'') => some (x :: ids, rest'') + | none => none + else some ([x], rest')) = some ([id], rest) + rw [parseBuildId_print id hid rest hr] + cases rest with + | nil => rfl + | cons c cs => + have hc : c ≠ '.' := hrd + show (if (c :: cs).head? = some '.' then + match parseBuildIdsGo f (c :: cs).tail with + | some (ids, rest'') => some (id :: ids, rest'') + | none => none + else some ([id], c :: cs)) = some ([id], c :: cs) + rw [if_neg (by simp [hc])] + | cons id₂ ids'' => + show parseBuildIdsGo (f + 1) + ((id ++ '.' :: joinDots (id₂ :: ids'')) ++ rest) = + some (id :: id₂ :: ids'', rest) + rw [List.append_assoc] + show (match parseBuildId + (id ++ ('.' :: (joinDots (id₂ :: ids'') ++ rest))) with + | none => none + | some (x, rest') => + if rest'.head? = some '.' then + match parseBuildIdsGo f rest'.tail with + | some (ids, rest'') => some (x :: ids, rest'') + | none => none + else some ([x], rest')) = some (id :: id₂ :: ids'', rest) + rw [parseBuildId_print id hid _ (headOk_dot_idChar _)] + show (if ('.' :: (joinDots (id₂ :: ids'') ++ rest)).head? = some '.' then + match parseBuildIdsGo f ('.' :: (joinDots (id₂ :: ids'') ++ rest)).tail with + | some (ids, rest'') => some (id :: ids, rest'') + | none => none + else some ([id], '.' :: (joinDots (id₂ :: ids'') ++ rest))) = + some (id :: id₂ :: ids'', rest) + rw [if_pos (by rfl : List.head? + ('.' :: (joinDots (id₂ :: ids'') ++ rest)) = some '.')] + show (match parseBuildIdsGo f (joinDots (id₂ :: ids'') ++ rest) with + | some (ids, rest'') => some (id :: ids, rest'') + | none => none) = some (id :: id₂ :: ids'', rest) + rw [ih (id₂ :: ids'') rest (by simp) hwf' hr hrd (by + simp at hlen + omega)] + +/-! ## The whole version -/ + +/-- The fuel the identifier readers get from the printed text is + always enough: the number of identifiers is at most the length + of their joined print, plus the tail. -/ +theorem ids_length_le (ids : List PreId) (hwf : ∀ id ∈ ids, WFPreId id) + (tail : List Char) : + ids.length ≤ (joinDots (ids.map printPreId) ++ tail).length + 1 := by + rw [List.length_append] + have h := joinDots_length (ids.map printPreId) (by + intro p hp + obtain ⟨id, hid, rfl⟩ := List.mem_map.mp hp + exact printPreId_ne_nil id (hwf id hid)) + simp at h + omega + +/-- The build side of the same fuel fact. -/ +theorem build_length_le (ids : List (List Char)) + (hwf : ∀ b ∈ ids, WFBuildId b) (tail : List Char) : + ids.length ≤ (joinDots ids ++ tail).length + 1 := by + rw [List.length_append] + have h := joinDots_length ids (fun b hb => (hwf b hb).1) + omega + +/-- A printed number at the very end reads back, with nothing + left over. -/ +theorem parseCoreNum_printNat_last (n : Nat) : + parseCoreNum (printNat n) = some (n, []) := by + have h := parseCoreNum_printNat n [] (headOk_nil _) + simpa using h + +/-- A dot at the front is read, and the rest returned. -/ +theorem expectDot_cons (rest : List Char) : expectDot ('.' :: rest) = some rest := by + simp [expectDot] + +/-- The prerelease reader on a printed prerelease part, with a + tail behind it. -/ +theorem parseOptPre_printPre (ids : List PreId) (hne : ids ≠ []) + (hwf : ∀ id ∈ ids, WFPreId id) (tail : List Char) + (hr : HeadOk isIdChar tail) + (hrd : NotDotHead tail) : + parseOptPre (('-' :: joinDots (ids.map printPreId)) ++ tail) = + some (ids, tail) := by + show parsePreIdsGo ((joinDots (ids.map printPreId) ++ tail).length + 1) + (joinDots (ids.map printPreId) ++ tail) = some (ids, tail) + exact parsePreIdsGo_print _ _ _ hne hwf hr hrd (ids_length_le ids hwf tail) + +/-- The prerelease reader on a printed prerelease part with + nothing behind it. -/ +theorem parseOptPre_printPre_last (ids : List PreId) (hne : ids ≠ []) + (hwf : ∀ id ∈ ids, WFPreId id) : + parseOptPre ('-' :: joinDots (ids.map printPreId)) = some (ids, []) := by + show parsePreIdsGo ((joinDots (ids.map printPreId)).length + 1) + (joinDots (ids.map printPreId)) = some (ids, []) + have h := parsePreIdsGo_print ((joinDots (ids.map printPreId) ++ []).length + 1) + ids [] hne hwf (headOk_nil _) True.intro (ids_length_le ids hwf []) + simpa using h + +/-- With a plus sign at the front, the prerelease reader reads + nothing. -/ +theorem parseOptPre_plus (rest : List Char) : + parseOptPre ('+' :: rest) = some ([], '+' :: rest) := by + simp [parseOptPre] + +/-- With nothing at the front, the prerelease reader reads + nothing. -/ +theorem parseOptPre_nil : parseOptPre [] = some ([], []) := by + simp [parseOptPre] + +/-- The build reader on a printed build part. -/ +theorem parseOptBuild_printBuild (ids : List (List Char)) (hne : ids ≠ []) + (hwf : ∀ b ∈ ids, WFBuildId b) : + parseOptBuild ('+' :: joinDots ids) = some (ids, []) := by + show parseBuildIdsGo ((joinDots ids).length + 1) (joinDots ids) = some (ids, []) + have h := parseBuildIdsGo_print ((joinDots ids ++ []).length + 1) ids [] + hne hwf (headOk_nil _) True.intro (build_length_le ids hwf []) + simpa using h + +/-- With nothing at the front, the build reader reads nothing. -/ +theorem parseOptBuild_nil : parseOptBuild [] = some ([], []) := by + simp [parseOptBuild] + +/-- Parsing the printed form of a version gives the version and + nothing left over. The four shapes of the optional parts are + handled by the cases on the prerelease and build lists. Each + case rewrites the readers one by one and then collapses the + chain of binds over `some`. -/ +theorem parseVersion_print (v : Version) (h : WF v) : + parseVersion (print v) = some (v, []) := by + obtain ⟨M, m, p, pre, build⟩ := v + obtain ⟨hwfpre, hwfbuild⟩ := h + cases pre with + | nil => + cases build with + | nil => + show parseVersion (printNat M ++ ('.' :: (printNat m ++ ('.' :: + (printNat p ++ []))))) = some (⟨M, m, p, [], []⟩, []) + unfold parseVersion + rw [parseCoreNum_printNat M _ (headOk_dot_digit _)] + simp only [Option.bind_some] + try dsimp only + rw [expectDot_cons] + simp only [Option.bind_some] + try dsimp only + rw [parseCoreNum_printNat m _ (headOk_dot_digit _)] + simp only [Option.bind_some] + try dsimp only + rw [expectDot_cons] + simp only [Option.bind_some] + try dsimp only + rw [parseCoreNum_printNat p _ (headOk_nil _)] + simp only [Option.bind_some] + try dsimp only + rw [parseOptPre_nil] + simp only [Option.bind_some] + try dsimp only + rw [parseOptBuild_nil] + simp only [Option.bind_some] + try dsimp only + | cons b bs => + show parseVersion (printNat M ++ ('.' :: (printNat m ++ ('.' :: + (printNat p ++ ('+' :: joinDots (b :: bs))))))) = + some (⟨M, m, p, [], b :: bs⟩, []) + unfold parseVersion + rw [parseCoreNum_printNat M _ (headOk_dot_digit _)] + simp only [Option.bind_some] + try dsimp only + rw [expectDot_cons] + simp only [Option.bind_some] + try dsimp only + rw [parseCoreNum_printNat m _ (headOk_dot_digit _)] + simp only [Option.bind_some] + try dsimp only + rw [expectDot_cons] + simp only [Option.bind_some] + try dsimp only + rw [parseCoreNum_printNat p _ (headOk_plus_digit _)] + simp only [Option.bind_some] + try dsimp only + rw [parseOptPre_plus] + simp only [Option.bind_some] + try dsimp only + rw [parseOptBuild_printBuild (b :: bs) (by simp) hwfbuild] + simp only [Option.bind_some] + try dsimp only + | cons id ids => + cases build with + | nil => + show parseVersion (printNat M ++ ('.' :: (printNat m ++ ('.' :: + (printNat p ++ ('-' :: joinDots ((id :: ids).map printPreId))))))) = + some (⟨M, m, p, id :: ids, []⟩, []) + unfold parseVersion + rw [parseCoreNum_printNat M _ (headOk_dot_digit _)] + simp only [Option.bind_some] + try dsimp only + rw [expectDot_cons] + simp only [Option.bind_some] + try dsimp only + rw [parseCoreNum_printNat m _ (headOk_dot_digit _)] + simp only [Option.bind_some] + try dsimp only + rw [expectDot_cons] + simp only [Option.bind_some] + try dsimp only + rw [parseCoreNum_printNat p _ (headOk_minus_digit _)] + simp only [Option.bind_some] + try dsimp only + rw [parseOptPre_printPre_last (id :: ids) (by simp) hwfpre] + simp only [Option.bind_some] + try dsimp only + rw [parseOptBuild_nil] + simp only [Option.bind_some] + try dsimp only + | cons b bs => + show parseVersion (printNat M ++ ('.' :: (printNat m ++ ('.' :: + (printNat p ++ (('-' :: joinDots ((id :: ids).map printPreId)) ++ + ('+' :: joinDots (b :: bs)))))))) = + some (⟨M, m, p, id :: ids, b :: bs⟩, []) + unfold parseVersion + rw [parseCoreNum_printNat M _ (headOk_dot_digit _)] + simp only [Option.bind_some] + try dsimp only + rw [expectDot_cons] + simp only [Option.bind_some] + try dsimp only + rw [parseCoreNum_printNat m _ (headOk_dot_digit _)] + simp only [Option.bind_some] + try dsimp only + rw [expectDot_cons] + simp only [Option.bind_some] + try dsimp only + rw [parseCoreNum_printNat p _ (headOk_minus_append _ _)] + simp only [Option.bind_some] + try dsimp only + rw [parseOptPre_printPre (id :: ids) (by simp) hwfpre + ('+' :: joinDots (b :: bs)) (headOk_plus_idChar _) + (show ('+' : Char) ≠ '.' by decide)] + simp only [Option.bind_some] + try dsimp only + rw [parseOptBuild_printBuild (b :: bs) (by simp) hwfbuild] + simp only [Option.bind_some] + try dsimp only + +/-- The round trip: parsing the printed form of a well formed + version gives the version back. -/ +theorem parse_print (v : Version) (h : WF v) : parse (print v) = some v := by + unfold parse + rw [parseVersion_print v h] + +end Semver.Proofs diff --git a/README.md b/README.md index 0c6c680..70e5dec 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,63 @@ # semver -lean semver + +A Semantic Versioning 2.0.0 parser, printer, and precedence comparison in Lean, with the round trip proved: parsing the printed form of a well formed version gives the version back. + +The specification this follows is Semantic Versioning 2.0.0 at semver.org. `SPEC.md` states its rules as this library applies them. + +## What it does + +`Semver/Version.lean` holds the value type, the well-formedness rules, the printer, and the comparison. A version is three numbers, a list of prerelease identifiers, and a list of build identifiers held as text. A prerelease identifier is a number or a text. `Semver/Parse.lean` holds the parser. `Main.lean` is a small command-line front end the tests drive. + +## What is proved + +The definitions are in `Semver/Version.lean` and `Semver/Parse.lean`. The proofs are in `Proofs/`. + +| Claim | Theorem | +|-------|---------| +| Parsing the printed form of a well formed version gives the version back. | `Semver.Proofs.parse_print` | +| A version compares equal to itself. | `Semver.Proofs.compare_self` | +| Two versions that agree on the numbers and the prerelease compare equal, whatever their build metadata. | `Semver.Proofs.compare_eq_of_fields` | +| Changing only the build metadata leaves a version comparing equal to the original. | `Semver.Proofs.compare_build_irrel` | +| Each step of the section 11 example chain: 1.0.0-alpha < 1.0.0-alpha.1 < 1.0.0-alpha.beta < 1.0.0-beta < 1.0.0-beta.2 < 1.0.0-beta.11 < 1.0.0-rc.1 < 1.0.0. | `Semver.Examples.chain_1` to `chain_7` | + +A version is well formed when each alphanumeric prerelease identifier is nonempty, holds only digits, ASCII letters, and hyphens, and holds at least one character that is not a digit, and each build identifier is nonempty and holds only those characters. The last rule for alphanumeric identifiers is what the type needs: an all-digit text is a number in this library, never an alphanumeric identifier, so a printed identifier reads back as the same kind. + +The proved theorems check against the standard axioms only (`propext`, `Classical.choice`, `Quot.sound`), which a reader can confirm with the prints in `Semver/Verify.lean`. + +## What is not proved + +- That the parser accepts every text the grammar allows, and rejects every text it forbids. The round trip does not need either, so neither is proved. The test harness checks that behaviour against a Python oracle written from the specification text, and the results file records the outcome, including any failure. +- That `compare` is a full order. Reflexivity of equality under `compare` is proved, and build metadata is proved irrelevant. Transitivity and totality are not proved, so no claim is made that any two versions compare consistently across a chain of comparisons, beyond the proved example chain. +- Anything about version ranges, sorting lists of versions, or picking a version. +- Reading requests and printing answers in `Main.lean`: splitting lines, the decimal parser, the semicolon split, and the check that a code is a Unicode scalar value. The tests cover them, malformed requests included. +- Speed. The code works on lists of characters, which suits proofs, not large data. + +## What you must trust + +- The Lean kernel, which checks the proofs. +- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. +- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about. +- The operating system and hardware it runs on. +- The Python oracle in the test harness, written from the specification text, and the reader's own reading of Semantic Versioning 2.0.0, which the oracle and this code both follow. + +This project has no dependencies beyond Lean itself. + +## Run it + +Needs Linux and [elan](https://github.com/leanprover/elan). Build, then feed request lines to the tool: + +``` +lake build +echo "parse 49,46,50,46,51" | .lake/build/bin/semver +``` + +That request is the text `1.2.3` as character codes, and the answer is `ok:49,46,50,46,51`. A text the parser rejects, such as the codes for `01.2.3`, answers `none`. A comparison request puts code 59 between the two texts and answers `lt`, `eq`, or `gt`. A malformed request answers `error`. See `SPEC.md` for the full protocol. + +## Re-check it + +``` +lake build +python3 tests/run_tests.py +``` + +The test script rebuilds, reruns the fixed specification cases and the differential run against the oracle, and rewrites `tests/TEST-RESULTS.md`. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..4f30134 --- /dev/null +++ b/SPEC.md @@ -0,0 +1,62 @@ +# Specification: semver + +A Semantic Versioning 2.0.0 parser, printer, and precedence comparison in Lean, following the specification at semver.org. A reviewer who did not write this specification approves it, together with any statement file a reviewer adds later. No such file exists yet, so nothing here counts toward the verified bar yet. + +Text is `List Char`. A Lean `Char` is one Unicode scalar value. + +## Values + +One value type, `Version`: + +- `major`, `minor`, `patch`: natural numbers. +- `pre`: a list of prerelease identifiers. Each identifier is `num n`, a number held as the number itself, or `alpha cs`, a text held as its characters. +- `build`: a list of build identifiers, each a list of characters held as text. + +Two choices in this shape carry weight: + +- A numeric prerelease identifier is held as a number, never as text. So the type cannot hold a numeric identifier with a leading zero, and cannot hold an alphanumeric identifier whose text is all digits: such a text is a number here. An `alpha` identifier is only well formed when its text holds at least one character that is not a digit. That rule is what lets a printed identifier always read back as the same kind. +- Build identifiers are held as text and never turned into numbers. Leading zeros in build metadata are part of the text, and build metadata takes no part in precedence, so nothing is gained by reading it as a number. + +## The grammar + +A version text is the core, then an optional prerelease part, then an optional build part. Anything after the build part, and any input that ends early, is rejected. + +- The core is three numbers split by dots. A number is a run of digits with no leading zero: the text `0` is fine, the text `01` is not. An empty part and a part with a non-digit are rejected. +- The prerelease part opens with a hyphen. It is a list of identifiers split by dots. An identifier is a nonempty run of digits, ASCII letters, and hyphens. An identifier made only of digits is numeric and must pass the same no-leading-zero rule. Any other identifier is alphanumeric. +- The build part opens with a plus sign. It is a list of identifiers split by dots, of the same character set. Identifiers must not be empty. Leading zeros are allowed. + +## The printer + +The printer writes the canonical text: numbers in decimal with no leading zeros, prerelease identifiers as their number or their text, build identifiers as their text, parts joined by dots, a hyphen before the prerelease part when there is one, a plus sign before the build part when there is one. + +## Precedence + +`compare` follows section 11 of the specification: + +1. Compare major, then minor, then patch, by value. +2. When the cores are equal, a version with a prerelease is lower than the same version without one. +3. Two prereleases compare identifier by identifier. Numeric identifiers compare by value. Alphanumeric identifiers compare in ASCII order. A numeric identifier is lower than an alphanumeric one. When every shared identifier is equal, the shorter list is lower. +4. Build metadata takes no part. + +## The claims + +Three claims are proved, for the value type as defined here: + +- The round trip: for every well formed version, parsing its printed form gives the version back. Well formed means each `alpha` identifier is nonempty, holds only identifier characters, and holds a character that is not a digit, and each build identifier is nonempty and holds only identifier characters. Numbers and numeric identifiers need no condition: a natural number prints canonically by construction. +- A version compares equal to itself. +- Two versions that agree on the three numbers and the prerelease compare equal, whatever their build metadata. In particular, changing only the build metadata of a version leaves it comparing equal to the original. + +The section 11 example chain is also proved, step by step, as example cases: + +1.0.0-alpha < 1.0.0-alpha.1 < 1.0.0-alpha.beta < 1.0.0-beta < 1.0.0-beta.2 < 1.0.0-beta.11 < 1.0.0-rc.1 < 1.0.0 + +No claim is made that the parser accepts every text the grammar allows, or rejects every text it forbids, beyond what the round trip needs. The test harness checks that behaviour against an oracle written from this specification's source text, Semantic Versioning 2.0.0, and the results file records the outcome. No claim is made that `compare` is a full order on all versions: transitivity and totality are not proved. Nothing here speaks of version ranges, sorting, or choosing among versions. + +## The command-line tool + +`Main.lean` reads one request per line and prints one answer per line. A request is an operation word, then optionally one space and comma-separated decimal character codes. + +- `parse` takes the codes of one version text. The answer is `ok:` followed by the codes of the canonical print of the parsed version, or `none` when the text is rejected. With no codes, the input is empty and the answer is `none`. +- `cmp` takes the codes of two version texts split by one code 59, the semicolon, which cannot appear in a version text. The split is at the first code 59; a second one lands in the second text and makes it rejected. The answer is `lt`, `eq`, or `gt`, or `none` when either text is rejected. A `cmp` request with no code 59 in it is malformed. + +A malformed request prints `error`: an unknown operation, numbers that are not plain decimal digits, a code that is not a Unicode scalar value, more than one space in the line, or the `cmp` case above. A line may end in LF or CR LF; nothing else around a request is ignored. diff --git a/Semver.lean b/Semver.lean new file mode 100644 index 0000000..515ef2c --- /dev/null +++ b/Semver.lean @@ -0,0 +1,2 @@ +import Semver.Version +import Semver.Parse diff --git a/Semver/Parse.lean b/Semver/Parse.lean new file mode 100644 index 0000000..e00d051 --- /dev/null +++ b/Semver/Parse.lean @@ -0,0 +1,139 @@ +/- + The parser, reading a semantic version from a list of + characters. Each reader returns the value it read and the + characters left over, or `none` when the text breaks the + grammar. The reader never reads past the end of its input. +-/ + +import Semver.Version + +namespace Semver + +/-- The longest run of digit characters at the front of the + input, and what is left. -/ +def takeDigits : List Char → List Char × List Char + | [] => ([], []) + | c :: cs => + if isDigit c then + let (a, b) := takeDigits cs + (c :: a, b) + else ([], c :: cs) + +/-- The longest run of identifier characters at the front of the + input, and what is left. -/ +def takeIdChars : List Char → List Char × List Char + | [] => ([], []) + | c :: cs => + if isIdChar c then + let (a, b) := takeIdChars cs + (c :: a, b) + else ([], c :: cs) + +/-- The value of a list of digit characters, most significant + first. The caller checks that every character is a digit. -/ +def digitsValue (ds : List Char) : Nat := + ds.foldl (fun a c => a * 10 + (c.toNat - 48)) 0 + +/-- The text of a number in the grammar: at least one digit, and + no leading zero unless the text is the single digit 0. -/ +def numTextOk (ds : List Char) : Bool := + !ds.isEmpty && ((ds.length == 1) || !(ds.head? == some '0')) + +/-- Read one number of the grammar: a run of digits that passes + the number text check. -/ +def parseCoreNum (cs : List Char) : Option (Nat × List Char) := + let (ds, rest) := takeDigits cs + if numTextOk ds then some (digitsValue ds, rest) else none + +/-- Turn the text of one prerelease identifier into a value. A + text of digits alone is a number, and must pass the number + text check. Any other text is alphanumeric, as it stands. The + caller checks that the text is not empty and holds only + identifier characters. -/ +def classifyPreId (ds : List Char) : Option PreId := + if ds.all isDigit then + if numTextOk ds then some (.num (digitsValue ds)) else none + else some (.alpha ds) + +/-- Read one prerelease identifier: a nonempty run of identifier + characters, classified by its text. -/ +def parsePreId (cs : List Char) : Option (PreId × List Char) := + let (ds, rest) := takeIdChars cs + if ds.isEmpty then none + else match classifyPreId ds with + | some id => some (id, rest) + | none => none + +/-- Read one build identifier: a nonempty run of identifier + characters, held as text. Leading zeros are fine here. -/ +def parseBuildId (cs : List Char) : Option (List Char × List Char) := + let (ds, rest) := takeIdChars cs + if ds.isEmpty then none else some (ds, rest) + +/-- Read a dot separated list of prerelease identifiers. The fuel + is the length of the input plus one, which bounds the number + of identifiers. After each identifier, a dot opens the next + one; anything else ends the list. -/ +def parsePreIdsGo : Nat → List Char → Option (List PreId × List Char) + | 0, _ => none + | fuel + 1, cs => + match parsePreId cs with + | none => none + | some (id, rest) => + if rest.head? = some '.' then + match parsePreIdsGo fuel rest.tail with + | some (ids, rest') => some (id :: ids, rest') + | none => none + else some ([id], rest) + +/-- Read a dot separated list of build identifiers. -/ +def parseBuildIdsGo : Nat → List Char → Option (List (List Char) × List Char) + | 0, _ => none + | fuel + 1, cs => + match parseBuildId cs with + | none => none + | some (id, rest) => + if rest.head? = some '.' then + match parseBuildIdsGo fuel rest.tail with + | some (ids, rest') => some (id :: ids, rest') + | none => none + else some ([id], rest) + +/-- Read the prerelease part when a hyphen opens it. With no + hyphen, the part is empty and nothing is read. -/ +def parseOptPre (cs : List Char) : Option (List PreId × List Char) := + if cs.head? = some '-' then parsePreIdsGo (cs.tail.length + 1) cs.tail + else some ([], cs) + +/-- Read the build part when a plus sign opens it. -/ +def parseOptBuild (cs : List Char) : Option (List (List Char) × List Char) := + if cs.head? = some '+' then parseBuildIdsGo (cs.tail.length + 1) cs.tail + else some ([], cs) + +/-- Read a dot where the grammar asks for one, returning what + follows it. -/ +def expectDot (cs : List Char) : Option (List Char) := + if cs.head? = some '.' then some cs.tail else none + +/-- Read a whole version, returning the version and the characters + left over. Three numbers split by dots, then the prerelease + part, then the build part. -/ +def parseVersion (cs : List Char) : Option (Version × List Char) := + (parseCoreNum cs).bind fun r₁ => + (expectDot r₁.2).bind fun rest₂ => + (parseCoreNum rest₂).bind fun r₂ => + (expectDot r₂.2).bind fun rest₄ => + (parseCoreNum rest₄).bind fun r₃ => + (parseOptPre r₃.2).bind fun r₄ => + (parseOptBuild r₄.2).bind fun r₅ => + some ({ major := r₁.1, minor := r₂.1, patch := r₃.1, pre := r₄.1, + build := r₅.1 }, r₅.2) + +/-- Parse a version from a character list. Anything after the + version makes the text rejected, as does any grammar break. -/ +def parse (cs : List Char) : Option Version := + match parseVersion cs with + | some (v, []) => some v + | _ => none + +end Semver diff --git a/Semver/Verify.lean b/Semver/Verify.lean new file mode 100644 index 0000000..17f942a --- /dev/null +++ b/Semver/Verify.lean @@ -0,0 +1,23 @@ +/- + Axiom check for the claims this package makes. Run with: + + lake env lean Semver/Verify.lean + + Every claim should list only the standard axioms (propext, + Classical.choice, Quot.sound). A line naming sorryAx would mean + a proof rests on an admitted gap, and the claim is not proved. +-/ + +import Proofs +import Proofs.Examples + +open Semver.Proofs Semver.Examples + +#print axioms parse_print +#print axioms compare_self +#print axioms compare_eq_of_fields +#print axioms compare_build_irrel +#print axioms chain_1 +#print axioms chain_7 +#print axioms valid_xyz +#print axioms invalid_empty_pre_and_build diff --git a/Semver/Version.lean b/Semver/Version.lean new file mode 100644 index 0000000..922a3b4 --- /dev/null +++ b/Semver/Version.lean @@ -0,0 +1,216 @@ +/- + The version value type, the well-formedness rules, the printer, + and the precedence comparison, for Semantic Versioning 2.0.0. + + A version holds three numbers, a list of prerelease identifiers, + and a list of build metadata identifiers. A prerelease identifier + is either numeric, held as the number itself, or alphanumeric, + held as its characters. Build identifiers are held as text, + because build metadata is never compared and leading zeros in it + carry meaning as text, not as numbers. +-/ + +namespace Semver + +/-- A prerelease identifier: a number, or a text with at least one + character that is not a digit. -/ +inductive PreId where + | num (n : Nat) + | alpha (cs : List Char) + deriving DecidableEq, Repr + +/-- A semantic version. Build identifiers are lists of characters. -/ +structure Version where + major : Nat + minor : Nat + patch : Nat + pre : List PreId + build : List (List Char) + deriving DecidableEq, Repr + +/-- A digit character, as a proposition. -/ +def IsDigit (c : Char) : Prop := 48 ≤ c.toNat ∧ c.toNat ≤ 57 + +/-- A digit character, as a test. -/ +def isDigit (c : Char) : Bool := 48 ≤ c.toNat && c.toNat ≤ 57 + +/-- The characters an identifier may hold: digits, ASCII letters, + and the hyphen. -/ +def IsIdChar (c : Char) : Prop := + IsDigit c ∨ (65 ≤ c.toNat ∧ c.toNat ≤ 90) ∨ + (97 ≤ c.toNat ∧ c.toNat ≤ 122) ∨ c = '-' + +/-- The identifier character test. -/ +def isIdChar (c : Char) : Bool := + isDigit c || (65 ≤ c.toNat && c.toNat ≤ 90) || + (97 ≤ c.toNat && c.toNat ≤ 122) || c = '-' + +theorem isDigit_iff {c : Char} : isDigit c = true ↔ IsDigit c := by + simp [isDigit, IsDigit, Bool.and_eq_true] + +theorem isIdChar_iff {c : Char} : isIdChar c = true ↔ IsIdChar c := by + unfold isIdChar IsIdChar + simp only [isDigit_iff, Bool.or_eq_true, Bool.and_eq_true, decide_eq_true_eq] + constructor + · rintro (((h | h) | h) | h) + · exact Or.inl h + · exact Or.inr (Or.inl h) + · exact Or.inr (Or.inr (Or.inl h)) + · exact Or.inr (Or.inr (Or.inr h)) + · rintro (h | (h | (h | h))) + · exact Or.inl (Or.inl (Or.inl h)) + · exact Or.inl (Or.inl (Or.inr h)) + · exact Or.inl (Or.inr h) + · exact Or.inr h + +/-- An alphanumeric prerelease identifier is well formed when it is + not empty, holds only identifier characters, and holds at least + one character that is not a digit. The last rule is what makes + the type honest: a text of digits alone is a number here, never + an alphanumeric identifier, so a printed identifier reads back + as the same kind. -/ +def WFAlpha (cs : List Char) : Prop := + cs ≠ [] ∧ (∀ c ∈ cs, IsIdChar c) ∧ (∃ c ∈ cs, ¬ IsDigit c) + +/-- A build identifier is well formed when it is not empty and + holds only identifier characters. Leading zeros are fine. -/ +def WFBuildId (cs : List Char) : Prop := + cs ≠ [] ∧ ∀ c ∈ cs, IsIdChar c + +/-- Well-formedness of one prerelease identifier. A numeric + identifier needs nothing: a natural number prints with no + leading zeros by construction. -/ +def WFPreId : PreId → Prop + | .num _ => True + | .alpha cs => WFAlpha cs + +/-- A version is well formed when each prerelease identifier and + each build identifier is well formed. The three numbers need + nothing. -/ +def WF (v : Version) : Prop := + (∀ id ∈ v.pre, WFPreId id) ∧ ∀ b ∈ v.build, WFBuildId b + +/-! ## Printing -/ + +/-- The character for a digit value below 10. Any other value + gives '0'; the lemmas about this function all ask for a value + below 10. -/ +def digitChar : Nat → Char + | 0 => '0' + | 1 => '1' + | 2 => '2' + | 3 => '3' + | 4 => '4' + | 5 => '5' + | 6 => '6' + | 7 => '7' + | 8 => '8' + | 9 => '9' + | _ => '0' + +/-- The digits of a number, least significant first, built with + fuel so the definition is structural. The top level call gives + one more fuel than the number, which is always enough: each + step divides by 10. -/ +def digitsRevAux : Nat → Nat → List Nat + | 0, _ => [] + | _ + 1, 0 => [] + | fuel + 1, n + 1 => (n + 1) % 10 :: digitsRevAux fuel ((n + 1) / 10) + +/-- The digits of a number, least significant first. The digits of + 0 are the empty list; `printNat` handles 0 on its own. -/ +def digitsRev (n : Nat) : List Nat := digitsRevAux (n + 1) n + +/-- The printed form of a natural number: decimal digits, no + leading zeros. -/ +def printNat (n : Nat) : List Char := + if n = 0 then ['0'] else (digitsRev n).reverse.map digitChar + +/-- One prerelease identifier, printed. -/ +def printPreId : PreId → List Char + | .num n => printNat n + | .alpha cs => cs + +/-- A list of printed parts joined by dots. -/ +def joinDots : List (List Char) → List Char + | [] => [] + | [p] => p + | p :: ps => p ++ '.' :: joinDots ps + +/-- The canonical text of a version: the three numbers split by + dots, then the prerelease part behind a hyphen when there is + one, then the build part behind a plus sign when there is + one. -/ +def print (v : Version) : List Char := + printNat v.major ++ ('.' :: (printNat v.minor ++ ('.' :: (printNat v.patch ++ + (match v.pre, v.build with + | [], [] => [] + | ids, [] => '-' :: joinDots (ids.map printPreId) + | [], bs => '+' :: joinDots bs + | ids, bs => ('-' :: joinDots (ids.map printPreId)) ++ + ('+' :: joinDots bs)))))) + +/-! ## Precedence, section 11 of the specification -/ + +/-- Three-way comparison of two numbers. -/ +def cmpNat (a b : Nat) : Ordering := + if a < b then .lt else if b < a then .gt else .eq + +/-- Three-way comparison of two characters, by code point. For + identifier characters this is ASCII order. -/ +def cmpChar (a b : Char) : Ordering := + if a.toNat < b.toNat then .lt else if b.toNat < a.toNat then .gt else .eq + +/-- Lexicographic comparison of two character lists. When one is + a prefix of the other, the shorter one is lower. -/ +def cmpChars : List Char → List Char → Ordering + | [], [] => .eq + | [], _ :: _ => .lt + | _ :: _, [] => .gt + | a :: as, b :: bs => + match cmpChar a b with + | .eq => cmpChars as bs + | o => o + +/-- Two prerelease identifiers: numbers compare by value, texts + compare in ASCII order, and a number is lower than a text. -/ +def cmpPreId : PreId → PreId → Ordering + | .num a, .num b => cmpNat a b + | .num _, .alpha _ => .lt + | .alpha _, .num _ => .gt + | .alpha a, .alpha b => cmpChars a b + +/-- Two prerelease lists, identifier by identifier. When every + shared identifier is equal, the shorter list is lower. -/ +def cmpPreList : List PreId → List PreId → Ordering + | [], [] => .eq + | [], _ :: _ => .lt + | _ :: _, [] => .gt + | a :: as, b :: bs => + match cmpPreId a b with + | .eq => cmpPreList as bs + | o => o + +/-- The prerelease step of section 11: a version with a + prerelease is lower than the same version without one. -/ +def cmpPre : List PreId → List PreId → Ordering + | [], [] => .eq + | [], _ :: _ => .gt + | _ :: _, [] => .lt + | ids₁, ids₂ => cmpPreList ids₁ ids₂ + +/-- Precedence, as section 11 of the specification states it: + major, then minor, then patch, then the prerelease rules. + Build metadata takes no part. -/ +def compare (v w : Version) : Ordering := + match cmpNat v.major w.major with + | .eq => + match cmpNat v.minor w.minor with + | .eq => + match cmpNat v.patch w.patch with + | .eq => cmpPre v.pre w.pre + | o => o + | o => o + | o => o + +end Semver diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..7c127af --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "semver", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..bea1a00 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,13 @@ +name = "semver" +version = "0.1.0" +defaultTargets = ["Semver", "Proofs", "semver"] + +[[lean_lib]] +name = "Semver" + +[[lean_lib]] +name = "Proofs" + +[[lean_exe]] +name = "semver" +root = "Main" diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..a6aff06 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.35.0 diff --git a/tests/TEST-RESULTS.md b/tests/TEST-RESULTS.md new file mode 100644 index 0000000..a9a1396 --- /dev/null +++ b/tests/TEST-RESULTS.md @@ -0,0 +1,17 @@ +# Test results + +Written by `tests/run_tests.py`. Rerun it to check these numbers. + +- Oracle: a Python oracle written from the specification text in `tests/run_tests.py` (Python 3.12.3) +- Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) +- Seed: 20261025 + +- fixed parse cases: 31 inputs, 31 agreements +- fixed cmp cases: 19 inputs, 19 agreements +- random valid versions, parse: 3000 inputs, 3000 agreements +- random version pairs, cmp: 3000 inputs, 3000 agreements +- mutated texts, parse: 3000 inputs, 3000 agreements +- soup texts, parse: 1500 inputs, 1500 agreements +- malformed requests: 12 inputs, 12 agreements +- Total: 10562 inputs, 10562 agreements +- Failures: 0 diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..3190797 --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,485 @@ +#!/usr/bin/env python3 +"""Tests for the Lean SemVer parser, printer, and precedence. + +Three parts. + +1. Fixed cases. The precedence chain from section 11 of the + specification as `cmp` requests, the valid example texts from + the specification as `parse` requests (each must answer with + its own text back, since each is already canonical), and + texts the grammar forbids (each must be rejected). + +2. A differential run against a Python oracle written from the + specification text with plain string code. Python's standard + library has no semver module, and `packaging` is not semver, + so neither is used. Random valid versions are built from + parts; random pairs are compared; random text mutations and + random soup texts must be read alike by both sides, as a + canonical print or as a rejection. + +3. Malformed request lines must be answered `error`. + +The oracle and the generator share no code with the Lean side. +The seed is recorded in the results file. + + python3 tests/run_tests.py [--seed N] [--count N] + +The tool is driven one batch process per chunk of requests: +input written and closed, output drained until the process +exits. The harness builds the executable first, writes +tests/TEST-RESULTS.md, and exits non-zero if any check fails. +It needs Python 3.11 or later. +""" + +import argparse +import random +import subprocess +import sys +import threading +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +EXE = ROOT / ".lake" / "build" / "bin" / "semver" +RESULTS = ROOT / "tests" / "TEST-RESULTS.md" +TIMEOUT = 900 +BUILD_TIMEOUT = 3600 +CHUNK = 2000 + +SEED_DEFAULT = 20261025 + +DIGITS = "0123456789" +IDCHARS = set(DIGITS + "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz-") + + +def codes(text): + return ",".join(str(ord(c)) for c in text) + + +def parse_request(text): + return "parse " + codes(text) + + +def cmp_request(a, b): + return "cmp " + codes(a) + ",59," + codes(b) + + +def run_tool(lines, timeout=TIMEOUT): + """Run the tool on a batch of request lines. + + Returns (answers, problem). No right answer is longer than + its request plus a small constant, so output past twice the + input plus 64 bytes a line is stopped, not read until memory + runs out. + """ + data = "".join(line + "\n" for line in lines) + raw = data.encode("utf-8") + limit = 2 * len(raw) + 64 * (len(lines) + 1) + try: + proc = subprocess.Popen( + [str(EXE)], + stdin=subprocess.PIPE, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + ) + except OSError as e: + return [], f"could not run {EXE}: {e.strerror or e}" + out, err = bytearray(), bytearray() + + def feed(): + try: + proc.stdin.write(raw) + proc.stdin.close() + except (BrokenPipeError, ValueError): + pass + + def drain(stream, buf, cap): + while chunk := stream.read1(1 << 16): + buf += chunk + if len(buf) > cap: + proc.kill() + return + + threads = [ + threading.Thread(target=feed), + threading.Thread(target=drain, args=(proc.stdout, out, limit)), + threading.Thread(target=drain, args=(proc.stderr, err, 1 << 20)), + ] + for t in threads: + t.start() + problem = None + try: + proc.wait(timeout=timeout) + except subprocess.TimeoutExpired: + proc.kill() + problem = f"no end after {timeout} seconds" + for t in threads: + t.join() + proc.wait() + if len(out) > limit: + problem = problem or f"more than {limit} bytes of output, stopped" + elif proc.returncode != 0 and not problem: + tail = " / ".join( + bytes(err).decode("utf-8", "backslashreplace").splitlines()[-3:] + ) + problem = f"exit status {proc.returncode}: {tail}" + text = bytes(out).decode("utf-8", "backslashreplace") + if text and not text.endswith("\n"): + problem = problem or "the last answer has no LF" + answers = text.split("\n") + if answers and answers[-1] == "": + answers.pop() + if len(answers) != len(lines) and not problem: + problem = f"{len(lines)} requests but {len(answers)} answers" + return answers, problem + + +# ------------------------------------------------------------------ +# The oracle, written from the specification text. +# +# A parsed version is (numbers, prerelease identifiers, build +# identifiers): numbers is a list of three ints; a prerelease +# identifier is ("n", int) or ("a", text); build identifiers are +# text. Parsing returns None for a text the grammar forbids. + + +def is_digits(s): + return s != "" and all(c in DIGITS for c in s) + + +def num_ok(s): + return is_digits(s) and (s == "0" or not s.startswith("0")) + + +def id_ok(s): + return s != "" and all(c in IDCHARS for c in s) + + +def oracle_parse(text): + if text == "": + return None + if "+" in text: + core_pre, build = text.split("+", 1) + else: + core_pre, build = text, None + if "-" in core_pre: + core, pre = core_pre.split("-", 1) + else: + core, pre = core_pre, None + parts = core.split(".") + if len(parts) != 3 or not all(num_ok(p) for p in parts): + return None + numbers = [int(p) for p in parts] + pre_ids = [] + if pre is not None: + for ident in pre.split("."): + if not id_ok(ident): + return None + if is_digits(ident): + if not num_ok(ident): + return None + pre_ids.append(("n", int(ident))) + else: + pre_ids.append(("a", ident)) + build_ids = [] + if build is not None: + for ident in build.split("."): + if not id_ok(ident): + return None + build_ids.append(ident) + return numbers, pre_ids, build_ids + + +def oracle_print(parsed): + numbers, pre_ids, build_ids = parsed + out = ".".join(str(n) for n in numbers) + if pre_ids: + out += "-" + ".".join( + str(v) if kind == "n" else v for kind, v in pre_ids + ) + if build_ids: + out += "+" + ".".join(build_ids) + return out + + +def expected_parse_answer(text): + parsed = oracle_parse(text) + if parsed is None: + return "none" + return "ok:" + codes(oracle_print(parsed)) + + +def cmp_id(x, y): + if x[0] == "n" and y[0] == "n": + if x[1] == y[1]: + return "eq" + return "lt" if x[1] < y[1] else "gt" + if x[0] == "n": + return "lt" + if y[0] == "n": + return "gt" + if x[1] == y[1]: + return "eq" + return "lt" if x[1] < y[1] else "gt" + + +def oracle_cmp(a_text, b_text): + pa = oracle_parse(a_text) + pb = oracle_parse(b_text) + if pa is None or pb is None: + return "none" + if pa[0] != pb[0]: + return "lt" if pa[0] < pb[0] else "gt" + a, b = pa[1], pb[1] + if not a and not b: + return "eq" + if not a: + return "gt" + if not b: + return "lt" + for x, y in zip(a, b): + c = cmp_id(x, y) + if c != "eq": + return c + if len(a) == len(b): + return "eq" + return "lt" if len(a) < len(b) else "gt" + + +# ------------------------------------------------------------------ +# Fixed cases. + +CHAIN = [ + "1.0.0-alpha", + "1.0.0-alpha.1", + "1.0.0-alpha.beta", + "1.0.0-beta", + "1.0.0-beta.2", + "1.0.0-beta.11", + "1.0.0-rc.1", + "1.0.0", +] + +VALID = [ + "1.0.0-alpha", + "1.0.0-alpha.1", + "1.0.0-0.3.7", + "1.0.0-x-y-z.-", + "1.0.0-alpha+001", + "1.0.0+20130313144700", + "1.0.0-beta+exp.sha.5114f85", + "1.0.0", + "0.0.0", + "999999.8888.7777-rc.99+build.01", +] + +INVALID = [ + "01.2.3", + "1.02.3", + "1.0.0-01", + "1.0.0-alpha..1", + "1.0.0-+", + "1.0.0+", + "1.0.0-", + "1.0", + "1.0.0.0", + "v1.2.3", + "1.0.0-alpha_beta", + "", + "1..2", + "1.0.0-alpha.01", + "1.0.0++1", + "-1.0.0", + "1.0.0 ", + " 1.0.0", + "1.0.0-rc.1+build+more", +] + +MALFORMED = [ + " ", + "parse 1,,2", + "parse 12a", + "cmp", + "cmp 49,50", + "cmp ;", + "bogus 1,2", + "parse 55296", + "parse 1114112", + "parse 49 50", + " parse 49", + "parse 49,", +] + + +def random_version(rng): + def core_num(): + return rng.choice([0, 1, 2, 9, 10, 42, 999, rng.randrange(0, 10**9)]) + + def pre_id(): + if rng.random() < 0.5: + return ("n", rng.choice([0, 1, 7, 11, 99, rng.randrange(0, 10**6)])) + n = rng.randrange(1, 7) + chars = [] + for _ in range(n): + chars.append(rng.choice("abcdefghijklmnopqrstuvwxyzABCZ0123456789-")) + text = "".join(chars) + if all(c in DIGITS for c in text): + text += rng.choice("aZ-") + return ("a", text) + + def build_id(): + n = rng.randrange(1, 7) + return "".join(rng.choice("0123456789abcXYZ-") for _ in range(n)) + + numbers = [core_num(), core_num(), core_num()] + pre_ids = [pre_id() for _ in range(rng.randrange(0, 4))] + build_ids = [build_id() for _ in range(rng.randrange(0, 3))] + return numbers, pre_ids, build_ids + + +def mutate(rng, text): + chars = list(text) + alphabet = "0123456789aZ-.+_;vx " + for _ in range(rng.randrange(1, 4)): + if not chars: + break + op = rng.choice(["replace", "insert", "delete", "swap"]) + i = rng.randrange(0, len(chars)) + if op == "replace": + chars[i] = rng.choice(alphabet) + elif op == "insert": + chars.insert(i, rng.choice(alphabet)) + elif op == "delete": + del chars[i] + elif i + 1 < len(chars): + chars[i], chars[i + 1] = chars[i + 1], chars[i] + return "".join(chars) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--seed", type=int, default=SEED_DEFAULT) + ap.add_argument("--count", type=int, default=3000) + args = ap.parse_args() + rng = random.Random(args.seed) + + print("building...", flush=True) + build = subprocess.run( + ["lake", "build"], cwd=ROOT, capture_output=True, text=True, + timeout=BUILD_TIMEOUT, + ) + if build.returncode != 0: + print(build.stdout[-3000:]) + print(build.stderr[-3000:]) + return 1 + + sections = [] # (name, requests, expected) + failures = [] + problems = [] + + def section(name, pairs): + sections.append((name, [r for r, _ in pairs], [e for _, e in pairs])) + + fixed_parse = [(parse_request(t), expected_parse_answer(t)) for t in VALID + INVALID] + fixed_parse.append(("parse", "none")) + fixed_parse.append(("parse ", "none")) + section("fixed parse cases", fixed_parse) + + fixed_cmp = [] + for a, b in zip(CHAIN, CHAIN[1:]): + fixed_cmp.append((cmp_request(a, b), "lt")) + fixed_cmp.append((cmp_request(b, a), "gt")) + fixed_cmp.append((cmp_request(CHAIN[0], CHAIN[-1]), "lt")) + fixed_cmp.append((cmp_request("1.0.0+build.1", "1.0.0+other.2"), "eq")) + fixed_cmp.append((cmp_request("2.1.1", "2.1.0"), "gt")) + fixed_cmp.append((cmp_request("1.0", "1.0.0"), "none")) + fixed_cmp.append(("cmp 49,59", "none")) + section("fixed cmp cases", fixed_cmp) + + rand_parse = [] + texts = [] + for _ in range(args.count): + v = random_version(rng) + text = oracle_print(v) + texts.append(text) + rand_parse.append((parse_request(text), "ok:" + codes(text))) + section("random valid versions, parse", rand_parse) + + rand_cmp = [] + for _ in range(args.count): + a = oracle_print(random_version(rng)) + b = oracle_print(random_version(rng)) + rand_cmp.append((cmp_request(a, b), oracle_cmp(a, b))) + section("random version pairs, cmp", rand_cmp) + + mutated = [] + for text in texts: + m = mutate(rng, text) + mutated.append((parse_request(m), expected_parse_answer(m))) + section("mutated texts, parse", mutated) + + soup = [] + soup_alphabet = "01.-+aZ; " + for _ in range(args.count // 2): + n = rng.randrange(0, 15) + text = "".join(rng.choice(soup_alphabet) for _ in range(n)) + soup.append((parse_request(text), expected_parse_answer(text))) + section("soup texts, parse", soup) + + section("malformed requests", [(line, "error") for line in MALFORMED]) + + lines_out = [] + lines_out.append("# Test results") + lines_out.append("") + lines_out.append( + "Written by `tests/run_tests.py`. Rerun it to check these numbers." + ) + lines_out.append("") + import platform + + lean_version = subprocess.run( + ["lake", "env", "lean", "--version"], cwd=ROOT, + capture_output=True, text=True, + ).stdout.strip() + lines_out.append(f"- Oracle: a Python oracle written from the specification text in `tests/run_tests.py` (Python {platform.python_version()})") + lines_out.append(f"- Lean: {lean_version}") + lines_out.append(f"- Seed: {args.seed}") + lines_out.append("") + + total_inputs = 0 + total_agree = 0 + for name, requests, expected in sections: + answers = [] + for i in range(0, len(requests), CHUNK): + chunk_answers, problem = run_tool(requests[i:i + CHUNK]) + if problem: + problems.append(f"{name}: {problem}") + chunk_answers = [""] * (len(requests[i:i + CHUNK])) + answers.extend(chunk_answers) + agree = 0 + for req, exp, ans in zip(requests, expected, answers): + total_inputs += 1 + if ans == exp: + agree += 1 + total_agree += 1 + elif len(failures) < 25: + failures.append(f"{name}: request {req!r}: expected {exp!r}, got {ans!r}") + lines_out.append(f"- {name}: {len(requests)} inputs, {agree} agreements") + lines_out.append(f"- Total: {total_inputs} inputs, {total_agree} agreements") + fail_count = total_inputs - total_agree + lines_out.append(f"- Failures: {fail_count}") + if problems: + lines_out.append(f"- Tool problems: {len(problems)}") + if failures or problems: + lines_out.append("") + lines_out.append("## Failures and problems") + lines_out.append("") + for f in (problems + failures)[:25]: + lines_out.append(f"- {f}") + lines_out.append("") + RESULTS.write_text("\n".join(lines_out), encoding="utf-8") + print("\n".join(lines_out)) + return 0 if fail_count == 0 and not problems else 1 + + +if __name__ == "__main__": + sys.exit(main())