diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml new file mode 100644 index 0000000..32457ed --- /dev/null +++ b/.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 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..b913bf2 --- /dev/null +++ b/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 diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..6a6e36c --- /dev/null +++ b/Proofs.lean @@ -0,0 +1 @@ +import Proofs.Main diff --git a/Proofs/Chars.lean b/Proofs/Chars.lean new file mode 100644 index 0000000..bbf6623 --- /dev/null +++ b/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 diff --git a/Proofs/Format.lean b/Proofs/Format.lean new file mode 100644 index 0000000..fff5292 --- /dev/null +++ b/Proofs/Format.lean @@ -0,0 +1,189 @@ +/- + Printing and parsing: `Version.print` writes `Spec.render`, and + `parseChars` accepts a list of characters exactly when it is how a + well formed version is written. +-/ + +import Proofs.Ident + +open SemVer + +namespace SemVer.Proofs + +/-! ## Printing -/ + +theorem toList_toString (n : Nat) : (toString n).toList = Nat.toDigits 10 n := by + rw [Nat.toString_eq_repr, Nat.toList_repr] + +theorem identPrint_toList (i : Ident) : i.print.toList = Spec.identChars i := by + cases i <;> simp [Ident.print, Spec.identChars, Spec.decimal] + +theorem print_toList (v : Version) : v.print.toList = Spec.render v := by + simp [Version.print, Spec.render, Spec.core, String.toList_append, Spec.decimal] + split <;> split <;> simp [List.map_map, Function.comp_def, identPrint_toList] + +/-! ## The parts of a rendered version -/ + +/-- The pre-release identifiers as written, if there are any. -/ +def prePart (pre : List Ident) : Option (List Char) := + if pre = [] then none else some (['.'].intercalate (pre.map Spec.identChars)) + +/-- The build identifiers as written, if there are any. -/ +def buildPart (build : List String) : Option (List Char) := + if build = [] then none else some (['.'].intercalate (build.map String.toList)) + +theorem core_eq (a b c : List Char) : Spec.core a b c = ['.'].intercalate [a, b, c] := by + simp [Spec.core, List.intercalate_cons_cons] + +theorem render_eq (v : Version) : + Spec.render v = + (Spec.core (Spec.decimal v.major) (Spec.decimal v.minor) (Spec.decimal v.patch) ++ + after '-' (prePart v.pre)) ++ after '+' (buildPart v.build) := by + simp only [Spec.render, prePart, buildPart] + split <;> split <;> simp [after] + +theorem dot_not_mem_decimal (n : Nat) : '.' ∉ Spec.decimal n := not_mem_toDigits not_digit_dot n +theorem plus_not_mem_decimal (n : Nat) : '+' ∉ Spec.decimal n := + not_mem_toDigits not_digit_plus n +theorem hyphen_not_mem_decimal (n : Nat) : '-' ∉ Spec.decimal n := + not_mem_toDigits not_digit_hyphen n + +theorem not_mem_core {c : Char} (hc : c ≠ '.') (a b d : Nat) + (h : ∀ n, c ∉ Spec.decimal n) : + c ∉ Spec.core (Spec.decimal a) (Spec.decimal b) (Spec.decimal d) := by + simp only [Spec.core, List.mem_append, List.mem_singleton, not_or] + exact ⟨⟨⟨⟨h a, hc⟩, h b⟩, hc⟩, h d⟩ + +theorem plus_not_mem_after_pre {pre : List Ident} (h : ∀ i ∈ pre, Spec.ValidIdent i) : + '+' ∉ after '-' (prePart pre) := by + unfold prePart + split + · simp [after] + · simp only [after, List.mem_cons, not_or] + refine ⟨by decide, not_mem_intercalate (by decide) ?_⟩ + intro l hl + simp only [List.mem_map] at hl + obtain ⟨i, hi, rfl⟩ := hl + exact plus_not_mem_identChars (h i hi) + +/-! ## Parsing -/ + +theorem parsePre_iff {p : List Char} {xs : List Ident} : + parseEach parsePreIdent (p.splitOn '.') = some xs ↔ + xs ≠ [] ∧ (∀ x ∈ xs, Spec.ValidIdent x) ∧ p = ['.'].intercalate (xs.map Spec.identChars) := + parseDotted_iff (fun _ _ => parsePreIdent_eq_some) (fun _ h => dot_not_mem_identChars h) + +theorem parseBuild_iff {p : List Char} {xs : List String} : + parseEach parseBuildIdent (p.splitOn '.') = some xs ↔ + xs ≠ [] ∧ (∀ x ∈ xs, Spec.BuildIdent x.toList) ∧ + p = ['.'].intercalate (xs.map String.toList) := + parseDotted_iff (fun _ _ => parseBuildIdent_eq_some) (fun _ h => dot_not_mem_build h) + +theorem parsePrePart_iff {r : Option (List Char)} {xs : List Ident} : + parseDotted parsePreIdent r = some xs ↔ (∀ x ∈ xs, Spec.ValidIdent x) ∧ r = prePart xs := by + cases r with + | none => + simp only [parseDotted, Option.some.injEq, prePart] + constructor + · rintro rfl; simp + · rintro ⟨-, h⟩ + split at h + · rename_i hx; exact hx.symm + · cases h + | some p => + simp only [parseDotted, parsePre_iff, prePart] + constructor + · rintro ⟨hne, hv, rfl⟩ + exact ⟨hv, by simp [hne]⟩ + · rintro ⟨hv, h⟩ + split at h + · cases h + · rename_i hne + simp only [Option.some.injEq] at h + exact ⟨hne, hv, h⟩ + +theorem parseBuildPart_iff {r : Option (List Char)} {xs : List String} : + parseDotted parseBuildIdent r = some xs ↔ (∀ x ∈ xs, Spec.BuildIdent x.toList) ∧ r = buildPart xs := by + cases r with + | none => + simp only [parseDotted, Option.some.injEq, buildPart] + constructor + · rintro rfl; simp + · rintro ⟨-, h⟩ + split at h + · rename_i hx; exact hx.symm + · cases h + | some p => + simp only [parseDotted, parseBuild_iff, buildPart] + constructor + · rintro ⟨hne, hv, rfl⟩ + exact ⟨hv, by simp [hne]⟩ + · rintro ⟨hv, h⟩ + split at h + · cases h + · rename_i hne + simp only [Option.some.injEq] at h + exact ⟨hne, hv, h⟩ + +/-- `parseChars`, with the steps named. -/ +theorem parseChars_eq (cs : List Char) : + parseChars cs = + match (breakAt '-' (breakAt '+' cs).1).1.splitOn '.' with + | [a, b, c] => do + let major ← parseNumeric a + let minor ← parseNumeric b + let patch ← parseNumeric c + let pre ← parseDotted parsePreIdent (breakAt '-' (breakAt '+' cs).1).2 + let build ← parseDotted parseBuildIdent (breakAt '+' cs).2 + pure { major, minor, patch, pre, build } + | _ => none := by + unfold parseChars + rfl + +theorem parseChars_eq_some {cs : List Char} {v : Version} : + parseChars cs = some v ↔ Spec.Valid v ∧ cs = Spec.render v := by + rw [parseChars_eq] + generalize hb : breakAt '+' cs = rb + obtain ⟨main, bp⟩ := rb + generalize hp : breakAt '-' main = rp + obtain ⟨core, pp⟩ := rp + obtain ⟨hb1, hb2⟩ := breakAt_spec hb + obtain ⟨hp1, hp2⟩ := breakAt_spec hp + simp only + constructor + · intro h + split at h + · rename_i a b c hs + simp only [Option.bind_eq_bind, Option.bind_eq_some_iff, Option.pure_def, + Option.some.injEq] at h + obtain ⟨major, hma, minor, hmi, patch, hpa, pre, hpre, build, hbuild, rfl⟩ := h + rw [parseNumeric_eq_some] at hma hmi hpa + obtain ⟨hvp, rfl⟩ := parsePrePart_iff.mp hpre + obtain ⟨hvb, rfl⟩ := parseBuildPart_iff.mp hbuild + refine ⟨⟨hvp, hvb⟩, ?_⟩ + rw [render_eq, hb2, hp2, core_eq] + have hcore := List.intercalate_splitOn (xs := core) '.' + rw [hs] at hcore + rw [← hcore, hma, hmi, hpa] + rfl + · cases h + · rintro ⟨⟨hvp, hvb⟩, rfl⟩ + rw [render_eq] at hb + rw [breakAt_append _ (by + simp only [List.mem_append, not_or] + exact ⟨not_mem_core (by decide) _ _ _ plus_not_mem_decimal, plus_not_mem_after_pre hvp⟩), + Prod.mk.injEq] at hb + obtain ⟨rfl, rfl⟩ := hb + rw [breakAt_append _ (not_mem_core (by decide) _ _ _ hyphen_not_mem_decimal), + Prod.mk.injEq] at hp + obtain ⟨rfl, rfl⟩ := hp + rw [core_eq, List.splitOn_intercalate] + · rw [(parsePrePart_iff (xs := v.pre)).mpr ⟨hvp, rfl⟩, + (parseBuildPart_iff (xs := v.build)).mpr ⟨hvb, rfl⟩] + simp only [Spec.decimal, parseNumeric_toDigits, Option.bind_eq_bind, Option.bind_some, + Option.pure_def] + · simp only [List.mem_cons, List.not_mem_nil, or_false, forall_eq_or_imp, forall_eq] + exact ⟨dot_not_mem_decimal _, dot_not_mem_decimal _, dot_not_mem_decimal _⟩ + · simp + +end SemVer.Proofs diff --git a/Proofs/Grammar.lean b/Proofs/Grammar.lean new file mode 100644 index 0000000..6c4e195 --- /dev/null +++ b/Proofs/Grammar.lean @@ -0,0 +1,92 @@ +/- + The grammar: a list of characters is a `` exactly when + it is how some well formed version is written. +-/ + +import Proofs.Format + +open SemVer + +namespace SemVer.Proofs + +theorem preReleaseIdent_iff {q : List Char} : + Spec.PreReleaseIdent q ↔ ∃ i, Spec.ValidIdent i ∧ q = Spec.identChars i := by + constructor + · rintro (h | h) + · refine ⟨.alnum (String.ofList q), ?_, ?_⟩ + · simpa [Spec.ValidIdent, String.toList_ofList] using h + · simp [Spec.identChars, String.toList_ofList] + · obtain ⟨n, rfl⟩ := numericIdent_iff.mp h + exact ⟨.num n, trivial, rfl⟩ + · rintro ⟨i, hi, rfl⟩ + cases i with + | num n => exact Or.inr (numericIdent_toDigits n) + | alnum s => exact Or.inl hi + +theorem buildIdent_iff_exists {q : List Char} : + Spec.BuildIdent q ↔ ∃ s : String, Spec.BuildIdent s.toList ∧ q = s.toList := by + constructor + · intro h + exact ⟨String.ofList q, by rwa [String.toList_ofList], by rw [String.toList_ofList]⟩ + · rintro ⟨s, hs, rfl⟩ + exact hs + +theorem dotSeparated_iff {α : Type} {P : List Char → Prop} {V : α → Prop} {g : α → List Char} + (hP : ∀ q, P q ↔ ∃ x, V x ∧ q = g x) {p : List Char} : + Spec.DotSeparated P p ↔ + ∃ xs : List α, xs ≠ [] ∧ (∀ x ∈ xs, V x) ∧ p = ['.'].intercalate (xs.map g) := by + constructor + · rintro ⟨parts, hne, hparts, rfl⟩ + obtain ⟨xs, hxs, rfl⟩ := exists_map_of_forall (fun q hq => (hP q).mp (hparts q hq)) + exact ⟨xs, by simpa using hne, hxs, rfl⟩ + · rintro ⟨xs, hne, hxs, rfl⟩ + refine ⟨xs.map g, by simpa using hne, ?_, rfl⟩ + intro q hq + simp only [List.mem_map] at hq + obtain ⟨x, hx, rfl⟩ := hq + exact (hP _).mpr ⟨x, hxs x hx, rfl⟩ + +theorem dotSeparated_pre_iff {p : List Char} : + Spec.DotSeparated Spec.PreReleaseIdent p ↔ + ∃ xs : List Ident, xs ≠ [] ∧ (∀ x ∈ xs, Spec.ValidIdent x) ∧ + p = ['.'].intercalate (xs.map Spec.identChars) := + dotSeparated_iff (fun _ => preReleaseIdent_iff) + +theorem dotSeparated_build_iff {p : List Char} : + Spec.DotSeparated Spec.BuildIdent p ↔ + ∃ xs : List String, xs ≠ [] ∧ (∀ x ∈ xs, Spec.BuildIdent x.toList) ∧ + p = ['.'].intercalate (xs.map String.toList) := + dotSeparated_iff (fun _ => buildIdent_iff_exists) + +theorem validSemVer_iff {cs : List Char} : + Spec.ValidSemVer cs ↔ ∃ v, Spec.Valid v ∧ cs = Spec.render v := by + constructor + · rintro ⟨ma, mi, pa, hma, hmi, hpa, h⟩ + obtain ⟨a, rfl⟩ := numericIdent_iff.mp hma + obtain ⟨b, rfl⟩ := numericIdent_iff.mp hmi + obtain ⟨c, rfl⟩ := numericIdent_iff.mp hpa + rcases h with rfl | ⟨pre, hpre, rfl⟩ | ⟨build, hbuild, rfl⟩ | ⟨pre, build, hpre, hbuild, rfl⟩ + · exact ⟨⟨a, b, c, [], []⟩, ⟨by simp, by simp⟩, by simp [Spec.render, Spec.decimal]⟩ + · obtain ⟨xs, hne, hxs, rfl⟩ := dotSeparated_pre_iff.mp hpre + exact ⟨⟨a, b, c, xs, []⟩, ⟨hxs, by simp⟩, by simp [Spec.render, Spec.decimal, hne]⟩ + · obtain ⟨ys, hne, hys, rfl⟩ := dotSeparated_build_iff.mp hbuild + exact ⟨⟨a, b, c, [], ys⟩, ⟨by simp, hys⟩, by simp [Spec.render, Spec.decimal, hne]⟩ + · obtain ⟨xs, hne, hxs, rfl⟩ := dotSeparated_pre_iff.mp hpre + obtain ⟨ys, hne', hys, rfl⟩ := dotSeparated_build_iff.mp hbuild + exact ⟨⟨a, b, c, xs, ys⟩, ⟨hxs, hys⟩, by simp [Spec.render, Spec.decimal, hne, hne']⟩ + · rintro ⟨⟨a, b, c, pre, build⟩, ⟨hvp, hvb⟩, rfl⟩ + refine ⟨Spec.decimal a, Spec.decimal b, Spec.decimal c, numericIdent_toDigits a, + numericIdent_toDigits b, numericIdent_toDigits c, ?_⟩ + by_cases hp : pre = [] <;> by_cases hb : build = [] + · subst hp hb + exact Or.inl (by simp [Spec.render]) + · subst hp + exact Or.inr (Or.inr (Or.inl ⟨_, dotSeparated_build_iff.mpr ⟨build, hb, hvb, rfl⟩, + by simp [Spec.render, hb]⟩)) + · subst hb + exact Or.inr (Or.inl ⟨_, dotSeparated_pre_iff.mpr ⟨pre, hp, hvp, rfl⟩, + by simp [Spec.render, hp]⟩) + · exact Or.inr (Or.inr (Or.inr ⟨_, _, dotSeparated_pre_iff.mpr ⟨pre, hp, hvp, rfl⟩, + dotSeparated_build_iff.mpr ⟨build, hb, hvb, rfl⟩, by simp [Spec.render, hp, hb]⟩)) + +end SemVer.Proofs diff --git a/Proofs/Ident.lean b/Proofs/Ident.lean new file mode 100644 index 0000000..5a2fabd --- /dev/null +++ b/Proofs/Ident.lean @@ -0,0 +1,143 @@ +/- + Identifiers: `parsePreIdent` and `parseBuildIdent` against the + grammar's `` and ``. +-/ + +import Proofs.Numeric +import Proofs.Lists + +open SemVer + +namespace SemVer.Proofs + +theorem all_isIdentChar_iff {cs : List Char} : + cs.all isIdentChar = true ↔ ∀ d ∈ cs, Spec.IdentChar d := by + simp [List.all_eq_true, isIdentChar_iff] + +/-- ``: identifier characters, not all of them + digits. -/ +theorem alnumIdent_iff {cs : List Char} : + Spec.AlnumIdent cs ↔ (∀ d ∈ cs, Spec.IdentChar d) ∧ ¬ ∀ d ∈ cs, Spec.Digit d := by + constructor + · rintro ⟨xs, c, ys, rfl, hc, hxs, hys⟩ + have hc' := (nonDigit_iff c).mp hc + refine ⟨?_, fun h => hc'.2 (h c (by simp))⟩ + intro d hd + simp only [List.mem_append, List.mem_cons] at hd + rcases hd with hd | rfl | hd + · exact hxs d hd + · exact hc'.1 + · exact hys d hd + · rintro ⟨hi, hd⟩ + simp only [Classical.not_forall, exists_prop] at hd + obtain ⟨c, hc, hnd⟩ := hd + obtain ⟨xs, ys, rfl⟩ := List.append_of_mem hc + refine ⟨xs, c, ys, rfl, (nonDigit_iff c).mpr ⟨hi c hc, hnd⟩, ?_, ?_⟩ + · exact fun d hd => hi d (by simp [hd]) + · exact fun d hd => hi d (by simp [hd]) + +/-- ``: one or more identifier characters. -/ +theorem buildIdent_iff {cs : List Char} : + Spec.BuildIdent cs ↔ cs ≠ [] ∧ ∀ d ∈ cs, Spec.IdentChar d := by + constructor + · rintro (h | ⟨hne, hd⟩) + · refine ⟨?_, (alnumIdent_iff.mp h).1⟩ + obtain ⟨xs, c, ys, rfl, -, -, -⟩ := h + simp + · exact ⟨hne, fun d h => digit_identChar (hd d h)⟩ + · rintro ⟨hne, hi⟩ + by_cases hd : ∀ d ∈ cs, Spec.Digit d + · exact Or.inr ⟨hne, hd⟩ + · exact Or.inl (alnumIdent_iff.mpr ⟨hi, hd⟩) + +theorem identChar_of_validIdent {i : Ident} (h : Spec.ValidIdent i) : + ∀ d ∈ Spec.identChars i, Spec.IdentChar d := by + cases i with + | num n => exact fun d hd => digit_identChar (digit_of_mem_toDigits hd) + | alnum s => exact (alnumIdent_iff.mp h).1 + +theorem parsePreIdent_eq_some {cs : List Char} {i : Ident} : + parsePreIdent cs = some i ↔ Spec.ValidIdent i ∧ cs = Spec.identChars i := by + unfold parsePreIdent + split + · rename_i hd + rw [all_isDigit_iff] at hd + cases i with + | num n => + simp only [Option.map_eq_some_iff, Ident.num.injEq, exists_eq_right, Spec.ValidIdent, + true_and, Spec.identChars, Spec.decimal] + exact parseNumeric_eq_some + | alnum s => + simp only [Option.map_eq_some_iff, reduceCtorEq, and_false, exists_false, false_iff, + not_and, Spec.ValidIdent, Spec.identChars] + rintro h rfl + exact (alnumIdent_iff.mp h).2 hd + · rename_i hd + rw [all_isDigit_iff] at hd + split + · rename_i hi + rw [all_isIdentChar_iff] at hi + cases i with + | num n => + simp only [Option.some.injEq, reduceCtorEq, Spec.ValidIdent, Spec.identChars, + Spec.decimal, true_and, false_iff] + rintro rfl + exact hd (fun d h => digit_of_mem_toDigits h) + | alnum s => + simp only [Option.some.injEq, Ident.alnum.injEq, Spec.ValidIdent, Spec.identChars] + constructor + · rintro rfl + rw [String.toList_ofList] + exact ⟨alnumIdent_iff.mpr ⟨hi, hd⟩, rfl⟩ + · rintro ⟨-, rfl⟩ + exact String.ofList_toList + · rename_i hi + rw [all_isIdentChar_iff] at hi + simp only [reduceCtorEq, false_iff, not_and] + rintro hv rfl + exact hi (identChar_of_validIdent hv) + +theorem parseBuildIdent_eq_some {cs : List Char} {s : String} : + parseBuildIdent cs = some s ↔ Spec.BuildIdent s.toList ∧ cs = s.toList := by + unfold parseBuildIdent + split + · rename_i h + simp only [Bool.and_eq_true, Bool.not_eq_true', List.isEmpty_eq_false_iff, + all_isIdentChar_iff] at h + simp only [Option.some.injEq] + constructor + · rintro rfl + rw [String.toList_ofList] + exact ⟨buildIdent_iff.mpr h, rfl⟩ + · rintro ⟨-, rfl⟩ + exact String.ofList_toList + · rename_i h + simp only [reduceCtorEq, false_iff, not_and] + rintro hb rfl + apply h + simp only [Bool.and_eq_true, Bool.not_eq_true', List.isEmpty_eq_false_iff, + all_isIdentChar_iff] + exact buildIdent_iff.mp hb + +/-! ## Separators inside identifiers -/ + +theorem not_mem_of_identChar {c : Char} (hc : ¬ Spec.IdentChar c) {cs : List Char} + (h : ∀ d ∈ cs, Spec.IdentChar d) : c ∉ cs := + fun hm => hc (h c hm) + +theorem dot_not_mem_identChars {i : Ident} (h : Spec.ValidIdent i) : '.' ∉ Spec.identChars i := + not_mem_of_identChar not_identChar_dot (identChar_of_validIdent h) + +theorem plus_not_mem_identChars {i : Ident} (h : Spec.ValidIdent i) : '+' ∉ Spec.identChars i := + not_mem_of_identChar not_identChar_plus (identChar_of_validIdent h) + +theorem dot_not_mem_build {s : String} (h : Spec.BuildIdent s.toList) : '.' ∉ s.toList := + not_mem_of_identChar not_identChar_dot (buildIdent_iff.mp h).2 + +theorem plus_not_mem_build {s : String} (h : Spec.BuildIdent s.toList) : '+' ∉ s.toList := + not_mem_of_identChar not_identChar_plus (buildIdent_iff.mp h).2 + +theorem not_mem_toDigits {c : Char} (hc : ¬ Spec.Digit c) (n : Nat) : c ∉ Nat.toDigits 10 n := + fun hm => hc (digit_of_mem_toDigits hm) + +end SemVer.Proofs diff --git a/Proofs/Lists.lean b/Proofs/Lists.lean new file mode 100644 index 0000000..2a1b23f --- /dev/null +++ b/Proofs/Lists.lean @@ -0,0 +1,133 @@ +/- + The list functions the parser uses: `breakAt`, `parseEach`, and + `List.splitOn` with `List.intercalate` from Lean core. +-/ + +import SemVer + +open SemVer + +namespace SemVer.Proofs + +/-- The text after a separator, with the separator, when there is one. -/ +def after (sep : Char) : Option (List Char) → List Char + | none => [] + | some b => sep :: b + +theorem breakAt_spec {sep : Char} {cs a : List Char} {r : Option (List Char)} + (h : breakAt sep cs = (a, r)) : sep ∉ a ∧ cs = a ++ after sep r := by + induction cs generalizing a r with + | nil => + simp only [breakAt, Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + simp [after] + | cons c cs ih => + simp only [breakAt] at h + split at h + · rename_i hc + simp only [Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + subst hc + simp [after] + · rename_i hc + obtain ⟨h1, h2⟩ := ih (a := (breakAt sep cs).1) (r := (breakAt sep cs).2) rfl + simp only [Prod.mk.injEq] at h + obtain ⟨rfl, rfl⟩ := h + refine ⟨?_, ?_⟩ + · simp only [List.mem_cons, not_or] + exact ⟨fun e => hc e.symm, h1⟩ + · rw [List.cons_append] + exact congrArg (c :: ·) h2 + +theorem breakAt_append {sep : Char} {a : List Char} (r : Option (List Char)) (h : sep ∉ a) : + breakAt sep (a ++ after sep r) = (a, r) := by + induction a with + | nil => cases r <;> simp [after, breakAt] + | cons c a ih => + simp only [List.mem_cons, not_or] at h + simp only [List.cons_append, breakAt, Ne.symm h.1, ite_false, ih h.2] + +theorem parseEach_cons_eq_some {α : Type} {f : List Char → Option α} {p : List Char} + {ps : List (List Char)} {ys : List α} : + parseEach f (p :: ps) = some ys ↔ + ∃ x xs, ys = x :: xs ∧ f p = some x ∧ parseEach f ps = some xs := by + simp only [parseEach, Option.bind_eq_bind, Option.bind_eq_some_iff, Option.pure_def, + Option.some.injEq] + constructor + · rintro ⟨x, hx, xs, hxs, rfl⟩ + exact ⟨x, xs, rfl, hx, hxs⟩ + · rintro ⟨x, xs, rfl, hx, hxs⟩ + exact ⟨x, hx, xs, hxs, rfl⟩ + +theorem parseEach_eq_some_iff {α : Type} {f : List Char → Option α} {g : α → List Char} + {V : α → Prop} (hf : ∀ p x, f p = some x ↔ V x ∧ p = g x) {ps : List (List Char)} + {ys : List α} : parseEach f ps = some ys ↔ (∀ x ∈ ys, V x) ∧ ps = ys.map g := by + induction ps generalizing ys with + | nil => cases ys <;> simp [parseEach] + | cons p ps ih => + rw [parseEach_cons_eq_some] + cases ys with + | nil => simp + | cons y ys => + simp only [List.cons.injEq, List.forall_mem_cons, List.map_cons, hf, ih] + constructor + · rintro ⟨x, xs, ⟨rfl, rfl⟩, ⟨hy, hp⟩, hys, hps⟩ + exact ⟨⟨hy, hys⟩, hp, hps⟩ + · rintro ⟨⟨hy, hys⟩, hp, hps⟩ + exact ⟨y, ys, ⟨rfl, rfl⟩, ⟨hy, hp⟩, hys, hps⟩ + +/-- Parsing a list of parts joined by dots. -/ +theorem parseDotted_iff {α : Type} {f : List Char → Option α} {g : α → List Char} + {V : α → Prop} (hf : ∀ p x, f p = some x ↔ V x ∧ p = g x) + (hdot : ∀ x, V x → '.' ∉ g x) {p : List Char} {xs : List α} : + parseEach f (p.splitOn '.') = some xs ↔ + xs ≠ [] ∧ (∀ x ∈ xs, V x) ∧ p = ['.'].intercalate (xs.map g) := by + rw [parseEach_eq_some_iff hf] + constructor + · rintro ⟨hv, he⟩ + refine ⟨?_, hv, ?_⟩ + · rintro rfl + exact List.splitOn_ne_nil _ _ he + · rw [← he, List.intercalate_splitOn] + · rintro ⟨hne, hv, rfl⟩ + refine ⟨hv, ?_⟩ + rw [List.splitOn_intercalate] + · intro l hl + simp only [List.mem_map] at hl + obtain ⟨x, hx, rfl⟩ := hl + exact hdot x (hv x hx) + · simpa using hne + +/-- Every part has the form `g x` for some `x` meeting `V`, so the list + of parts does too. -/ +theorem exists_map_of_forall {α : Type} {g : α → List Char} {V : α → Prop} : + ∀ {parts : List (List Char)}, (∀ q ∈ parts, ∃ x, V x ∧ q = g x) → + ∃ xs : List α, (∀ x ∈ xs, V x) ∧ parts = xs.map g + | [], _ => ⟨[], by simp, rfl⟩ + | q :: qs, h => by + obtain ⟨x, hx, rfl⟩ := h q (by simp) + obtain ⟨xs, hxs, rfl⟩ := exists_map_of_forall (parts := qs) (fun q hq => h q (by simp [hq])) + refine ⟨x :: xs, ?_, rfl⟩ + intro y hy + simp only [List.mem_cons] at hy + rcases hy with rfl | hy + · exact hx + · exact hxs y hy + +theorem not_mem_intercalate {c : Char} {ls : List (List Char)} (hc : c ≠ '.') + (h : ∀ l ∈ ls, c ∉ l) : c ∉ ['.'].intercalate ls := by + induction ls with + | nil => simp + | cons l ls ih => + cases ls with + | nil => simpa using h + | cons l' ls => + rw [List.intercalate_cons_cons] + intro hm + simp only [List.mem_append, List.mem_cons, List.not_mem_nil, or_false] at hm + rcases hm with (hm | hm) | hm + · exact h l (by simp) hm + · exact hc hm + · exact ih (fun l hl => h l (by simp_all)) hm + +end SemVer.Proofs diff --git a/Proofs/Main.lean b/Proofs/Main.lean new file mode 100644 index 0000000..b3534de --- /dev/null +++ b/Proofs/Main.lean @@ -0,0 +1,146 @@ +/- + The statements of `Spec.lean`, under the same names, from the lemmas + in the other files of `Proofs/`. The test vectors are checked by + evaluation in the kernel. +-/ + +import SemVer +import Spec.Defs +import Proofs.Grammar +import Proofs.Order + +open SemVer +open SemVer.Proofs + +/-! ## Printing -/ + +theorem Spec.print_eq (v : Version) : v.print.toList = Spec.render v := + print_toList v + +/-! ## Parsing -/ + +theorem Spec.parse_iff (s : String) (v : Version) : + parse s = some v ↔ Spec.Valid v ∧ s.toList = Spec.render v := + parseChars_eq_some + +theorem Spec.parse_isSome_iff (s : String) : + (parse s).isSome ↔ Spec.ValidSemVer s.toList := by + rw [validSemVer_iff, Option.isSome_iff_exists] + exact exists_congr fun v => Spec.parse_iff s v + +theorem Spec.parse_valid (s : String) (v : Version) (h : parse s = some v) : + Spec.Valid v := + ((Spec.parse_iff s v).mp h).1 + +theorem Spec.parse_print (v : Version) (h : Spec.Valid v) : parse v.print = some v := + (Spec.parse_iff _ _).mpr ⟨h, Spec.print_eq v⟩ + +theorem Spec.print_parse (s : String) (v : Version) (h : parse s = some v) : + v.print = s := by + obtain ⟨-, hs⟩ := (Spec.parse_iff s v).mp h + apply String.toList_injective + rw [Spec.print_eq, hs] + +/-! ## Precedence -/ + +theorem Spec.compare_eq (a b : Version) : a.compare b = Spec.precedence a b := + versionCompare_eq a b + +theorem Spec.compare_build (a b : Version) (x y : List String) : + ({ a with build := x } : Version).compare { b with build := y } = a.compare b := + rfl + +theorem Spec.compare_eq_eq_iff (a b : Version) : + a.compare b = .eq ↔ + a.major = b.major ∧ a.minor = b.minor ∧ a.patch = b.patch ∧ a.pre = b.pre := by + rw [compare_key, lawful_key.eq_iff] + simp [key] + +theorem Spec.compare_swap (a b : Version) : (a.compare b).swap = b.compare a := by + rw [compare_key, compare_key, lawful_key.swap] + +theorem Spec.compare_trans (a b c : Version) (hab : a.compare b ≠ .gt) + (hbc : b.compare c ≠ .gt) : a.compare c ≠ .gt := by + rw [compare_key] at hab hbc ⊢ + exact lawful_key.le_trans hab hbc + +theorem Spec.compare_lt_trans (a b c : Version) (hab : a.compare b = .lt) + (hbc : b.compare c = .lt) : a.compare c = .lt := by + rw [compare_key] at hab hbc ⊢ + exact lawful_key.lt_trans _ _ _ hab hbc + +/-! ## Test vectors -/ + +/-- The examples of sections 9 and 10, with the parts they are read + as. -/ +theorem Spec.semver_examples : + parse "1.0.0-alpha" = some ⟨1, 0, 0, [.alnum "alpha"], []⟩ ∧ + parse "1.0.0-alpha.1" = some ⟨1, 0, 0, [.alnum "alpha", .num 1], []⟩ ∧ + parse "1.0.0-0.3.7" = some ⟨1, 0, 0, [.num 0, .num 3, .num 7], []⟩ ∧ + parse "1.0.0-x.7.z.92" = some ⟨1, 0, 0, [.alnum "x", .num 7, .alnum "z", .num 92], []⟩ ∧ + parse "1.0.0-x-y-z.--" = some ⟨1, 0, 0, [.alnum "x-y-z", .alnum "--"], []⟩ ∧ + parse "1.0.0-alpha+001" = some ⟨1, 0, 0, [.alnum "alpha"], ["001"]⟩ ∧ + parse "1.0.0+20130313144700" = some ⟨1, 0, 0, [], ["20130313144700"]⟩ ∧ + parse "1.0.0-beta+exp.sha.5114f85" = + some ⟨1, 0, 0, [.alnum "beta"], ["exp", "sha", "5114f85"]⟩ ∧ + parse "1.0.0+21AF26D3----117B344092BD" = some ⟨1, 0, 0, [], ["21AF26D3----117B344092BD"]⟩ := by + decide + +/-- The examples of section 11, each list in rising order: every + version in it has lower precedence than every later one. And two + versions that differ only in build metadata have the same + precedence (section 10). -/ +theorem Spec.precedence_examples : + ["1.0.0", "2.0.0", "2.1.0", "2.1.1"].Pairwise + (fun s t => Spec.compareStrings s t = some .lt) ∧ + ["1.0.0-alpha", "1.0.0"].Pairwise (fun s t => Spec.compareStrings s t = some .lt) ∧ + ["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"].Pairwise + (fun s t => Spec.compareStrings s t = some .lt) ∧ + Spec.compareStrings "1.0.0-alpha+001" "1.0.0-alpha" = some .eq ∧ + Spec.compareStrings "1.0.0+20130313144700" "1.0.0+21AF26D3----117B344092BD" = some .eq := by + decide + +/-- Strings outside the grammar: leading zeros in numbers, missing or + extra parts, empty identifiers, characters outside ASCII letters, + digits and hyphens, and anything before or after the version. -/ +theorem Spec.reject_vectors : + parse "01.0.0" = none ∧ + parse "1.02.0" = none ∧ + parse "1.0.00" = none ∧ + parse "1.0.0-01" = none ∧ + parse "1.0" = none ∧ + parse "1.0.0.0" = none ∧ + parse "1.0.0-" = none ∧ + parse "1.0.0+" = none ∧ + parse "1.0.0-alpha..1" = none ∧ + parse "1.0.0-alpha." = none ∧ + parse "1.0.0+build..1" = none ∧ + parse "1.0.0+a+b" = none ∧ + parse "1.0.0-alpha_beta" = none ∧ + parse "1.0.0-alpha.é" = none ∧ + parse "1.0.0-١" = none ∧ + parse "１.0.0" = none ∧ + parse "v1.0.0" = none ∧ + parse "=1.0.0" = none ∧ + parse " 1.0.0" = none ∧ + parse "1.0.0 " = none ∧ + parse "1.0.0\n" = none ∧ + parse "-1.0.0" = none ∧ + parse "1.0.0-+" = none ∧ + parse "" = none := by + decide + +/-- Strings inside the grammar that loose parsers often get wrong: a + pre-release identifier may have leading zeros when it is not all + digits, a build identifier may have them always, and a hyphen may + start an identifier. -/ +theorem Spec.accept_vectors : + parse "1.0.0-0a" = some ⟨1, 0, 0, [.alnum "0a"], []⟩ ∧ + parse "1.0.0-0" = some ⟨1, 0, 0, [.num 0], []⟩ ∧ + parse "1.0.0+001" = some ⟨1, 0, 0, [], ["001"]⟩ ∧ + parse "1.0.0--" = some ⟨1, 0, 0, [.alnum "-"], []⟩ ∧ + parse "1.0.0-a-+b-" = some ⟨1, 0, 0, [.alnum "a-"], ["b-"]⟩ ∧ + parse "0.0.0" = some ⟨0, 0, 0, [], []⟩ ∧ + parse "18446744073709551616.0.0" = some ⟨18446744073709551616, 0, 0, [], []⟩ := by + decide diff --git a/Proofs/Numeric.lean b/Proofs/Numeric.lean new file mode 100644 index 0000000..8104e89 --- /dev/null +++ b/Proofs/Numeric.lean @@ -0,0 +1,143 @@ +/- + Numbers: `Nat.toDigits 10`, which `Spec.decimal` uses, writes exactly + the numeric identifiers of the grammar, and `parseNumeric` reads them + back. +-/ + +import Proofs.Chars + +open SemVer + +namespace SemVer.Proofs + +theorem digit_of_mem_toDigits {n : Nat} {c : Char} (h : c ∈ Nat.toDigits 10 n) : Spec.Digit c := by + have := Nat.isDigit_of_mem_toDigits (by decide) (by decide) h + rw [Char.isDigit_iff_toNat] at this + exact (digit_iff c).mpr this + +/-- A positive number is written with a first digit other than `0`. -/ +theorem toDigits_head {n : Nat} (hn : 0 < n) : + ∃ c rest, Nat.toDigits 10 n = c :: rest ∧ c ≠ '0' := by + induction n using Nat.strongRecOn with + | ind n ih => + rw [Nat.toDigits_eq_ite (by decide)] + split + · exact ⟨_, [], rfl, by simp only [ne_eq, Nat.digitChar_eq_zero]; omega⟩ + · obtain ⟨c, rest, h, hc⟩ := ih (n / 10) (by omega) (by omega) + exact ⟨c, rest ++ _, by rw [h]; rfl, hc⟩ + +theorem numericIdent_cons {c : Char} {cs : List Char} : + Spec.NumericIdent (c :: cs) ↔ (∀ d ∈ c :: cs, Spec.Digit d) ∧ (c ≠ '0' ∨ cs = []) := by + constructor + · rintro (h | ⟨c', rest, h, hc, hr⟩) + · simp only [List.cons.injEq] at h + obtain ⟨rfl, rfl⟩ := h + exact ⟨by decide, Or.inr rfl⟩ + · simp only [List.cons.injEq] at h + obtain ⟨rfl, rfl⟩ := h + rw [positiveDigit_iff_digit] at hc + exact ⟨List.forall_mem_cons.mpr ⟨hc.1, hr⟩, Or.inl hc.2⟩ + · rintro ⟨hd, h0 | rfl⟩ + · rw [List.forall_mem_cons] at hd + exact Or.inr ⟨c, cs, rfl, (positiveDigit_iff_digit c).mpr ⟨hd.1, h0⟩, hd.2⟩ + · by_cases hc : c = '0' + · exact Or.inl (by rw [hc]) + · exact Or.inr ⟨c, [], rfl, (positiveDigit_iff_digit c).mpr ⟨hd c (by simp), hc⟩, + by simp⟩ + +theorem numericIdent_toDigits (n : Nat) : Spec.NumericIdent (Nat.toDigits 10 n) := by + rcases Nat.eq_zero_or_pos n with rfl | hn + · exact Or.inl rfl + · obtain ⟨c, rest, h, hc⟩ := toDigits_head hn + rw [h, numericIdent_cons] + exact ⟨fun d hd => digit_of_mem_toDigits (h ▸ hd), Or.inl hc⟩ + +theorem numericIdent_ne_nil {cs : List Char} (h : Spec.NumericIdent cs) : cs ≠ [] := by + rcases h with rfl | ⟨c, rest, rfl, _, _⟩ <;> simp + +theorem numericIdent_digits {cs : List Char} (h : Spec.NumericIdent cs) : ∀ d ∈ cs, Spec.Digit d := by + rcases h with rfl | ⟨c, rest, rfl, hc, hr⟩ + · decide + · exact List.forall_mem_cons.mpr ⟨⟨by + have := (positiveDigit_iff c).mp hc + rw [le_iff_toNat]; exact Nat.le_trans (by decide) this.1, hc.2⟩, hr⟩ + +/-- Induction from the end of a list. -/ +theorem snoc_induction {α : Type} {P : List α → Prop} (nil : P []) + (snoc : ∀ r x, P r → P (r ++ [x])) (l : List α) : P l := by + rw [← List.reverse_reverse l] + induction l.reverse with + | nil => exact nil + | cons x t ih => rw [List.reverse_cons]; exact snoc _ _ ih + +theorem ofDigitChars_ge (cs : List Char) (init : Nat) : init ≤ Nat.ofDigitChars 10 cs init := by + rw [Nat.ofDigitChars_eq_ofDigitChars_zero] + have : 0 < 10 ^ cs.length := Nat.pow_pos_iff.mpr (Or.inl (by decide)) + have : init ≤ 10 ^ cs.length * init := Nat.le_mul_of_pos_left init this + omega + +/-- Digits with a first digit other than `0` are how their value is + written. -/ +theorem toDigits_ofDigitChars_cons {c : Char} {rest : List Char} (hc : Spec.PositiveDigit c) + (hr : ∀ d ∈ rest, Spec.Digit d) : + Nat.toDigits 10 (Nat.ofDigitChars 10 (c :: rest) 0) = c :: rest := by + have hc' := (positiveDigit_iff c).mp hc + induction rest using snoc_induction with + | nil => + rw [Nat.ofDigitChars_cons, Nat.ofDigitChars_nil, show '0'.toNat = 48 from rfl, + Nat.mul_zero, Nat.zero_add, Nat.toDigits_of_lt_base (by omega), + digitChar_toNat ((positiveDigit_iff_digit c).mp hc).1] + | snoc r x ih => + have hx := hr x (by simp) + have ih := ih (fun d hd => hr d (by simp [hd])) + have hpos : 0 < Nat.ofDigitChars 10 (c :: r) 0 := by + rw [Nat.ofDigitChars_cons] + have := ofDigitChars_ge r (10 * 0 + (c.toNat - '0'.toNat)) + have : '0'.toNat = 48 := rfl + omega + have hx' := (digit_iff x).mp hx + rw [← List.cons_append, Nat.ofDigitChars_append, Nat.ofDigitChars_cons, Nat.ofDigitChars_nil, + ← Nat.toDigits_append_toDigits (by decide) hpos (by show x.toNat - 48 < 10; omega), ih, + Nat.toDigits_of_lt_base (by show x.toNat - 48 < 10; omega)] + show _ ++ [Nat.digitChar (x.toNat - 48)] = _ + rw [digitChar_toNat hx] + +theorem toDigits_ofDigitChars {cs : List Char} (h : Spec.NumericIdent cs) : + Nat.toDigits 10 (Nat.ofDigitChars 10 cs 0) = cs := by + rcases h with rfl | ⟨c, rest, rfl, hc, hr⟩ + · decide + · exact toDigits_ofDigitChars_cons hc hr + +theorem numericIdent_iff {cs : List Char} : + Spec.NumericIdent cs ↔ ∃ n, cs = Nat.toDigits 10 n := + ⟨fun h => ⟨_, (toDigits_ofDigitChars h).symm⟩, fun ⟨n, h⟩ => h ▸ numericIdent_toDigits n⟩ + +theorem all_isDigit_iff {cs : List Char} : cs.all isDigit = true ↔ ∀ d ∈ cs, Spec.Digit d := by + simp [List.all_eq_true, isDigit_iff] + +theorem parseNumeric_eq_some {cs : List Char} {n : Nat} : + parseNumeric cs = some n ↔ cs = Nat.toDigits 10 n := by + cases cs with + | nil => simp [parseNumeric, (Nat.toDigits_ne_nil).symm] + | cons c cs => + have key : ((c :: cs).all isDigit && (c != '0' || cs.isEmpty)) = true ↔ + Spec.NumericIdent (c :: cs) := by + rw [numericIdent_cons, Bool.and_eq_true, all_isDigit_iff, Bool.or_eq_true, bne_iff_ne, + List.isEmpty_iff] + rw [parseNumeric] + split + · rename_i h + have hn := key.mp h + simp only [Option.some.injEq] + constructor + · rintro rfl; exact (toDigits_ofDigitChars hn).symm + · intro h; rw [h, Nat.ofDigitChars_ten_toDigits] + · rename_i h + simp only [reduceCtorEq, false_iff] + intro he + exact h (key.mpr (he ▸ numericIdent_toDigits n)) + +theorem parseNumeric_toDigits (n : Nat) : parseNumeric (Nat.toDigits 10 n) = some n := + parseNumeric_eq_some.mpr rfl + +end SemVer.Proofs diff --git a/Proofs/Order.lean b/Proofs/Order.lean new file mode 100644 index 0000000..7b38a1b --- /dev/null +++ b/Proofs/Order.lean @@ -0,0 +1,229 @@ +/- + Precedence: `Version.compare` against `Spec.precedence`, and the laws + that make it an order: swapping the sides swaps the answer, it is + transitive, and `.eq` means the same numbers and pre-release + identifiers. +-/ + +import Proofs.Chars + +open SemVer + +namespace SemVer.Proofs + +/-! ## Against the specification -/ + +theorem compare_nat (a b : Nat) : compare a b = Spec.numOrder a b := by + unfold Spec.numOrder + split + · exact Nat.compare_eq_lt.mpr ‹_› + · split + · exact Nat.compare_eq_gt.mpr ‹_› + · exact Nat.compare_eq_eq.mpr (by omega) + +theorem compareAscii_eq : ∀ a b : List Char, compareAscii a b = Spec.asciiOrder a b + | [], [] => rfl + | [], _ :: _ => rfl + | _ :: _, [] => rfl + | x :: xs, y :: ys => by + simp only [compareAscii, Spec.asciiOrder, compare_nat, Spec.numOrder, compareAscii_eq xs ys] + split + · rfl + · split + · rfl + · rfl + +theorem identCompare_eq (a b : Ident) : a.compare b = Spec.identOrder a b := by + cases a <;> cases b <;> simp [Ident.compare, Spec.identOrder, compare_nat, compareAscii_eq] + +theorem compareIdents_eq : ∀ a b : List Ident, compareIdents a b = Spec.preOrder a b + | [], [] => rfl + | [], _ :: _ => rfl + | _ :: _, [] => rfl + | x :: xs, y :: ys => by + simp only [compareIdents, Spec.preOrder, identCompare_eq, compareIdents_eq xs ys] + cases Spec.identOrder x y <;> rfl + +theorem then_numOrder (a b : Nat) (r : Ordering) : + (compare a b).then r = if a ≠ b then Spec.numOrder a b else r := by + split + · rename_i h + have : compare a b ≠ .eq := fun e => h (Nat.compare_eq_eq.mp e) + rw [compare_nat] at this ⊢ + revert this + cases Spec.numOrder a b <;> simp + · rename_i h + rw [Nat.compare_eq_eq.mpr (Classical.not_not.mp h)] + rfl + +theorem versionCompare_eq (a b : Version) : a.compare b = Spec.precedence a b := by + simp only [Version.compare, Spec.precedence, then_numOrder] + split + · rfl + · split + · rfl + · split + · rfl + · cases ha : a.pre <;> cases hb : b.pre <;> + simp [comparePre, compareIdents_eq] + +/-! ## Orders in which `.eq` means equal -/ + +/-- `o` orders `α`: swapping the sides swaps the answer, `.lt` is + transitive, and `.eq` means the two are equal. -/ +structure LawfulOrder {α : Type} (o : α → α → Ordering) : Prop where + eq_iff : ∀ a b, o a b = .eq ↔ a = b + swap : ∀ a b, (o a b).swap = o b a + lt_trans : ∀ a b c, o a b = .lt → o b c = .lt → o a c = .lt + +theorem LawfulOrder.le_trans {α : Type} {o : α → α → Ordering} (h : LawfulOrder o) + {a b c : α} (hab : o a b ≠ .gt) (hbc : o b c ≠ .gt) : o a c ≠ .gt := by + cases e1 : o a b + · cases e2 : o b c + · rw [h.lt_trans a b c e1 e2]; decide + · rw [← (h.eq_iff b c).mp e2, e1]; decide + · exact absurd e2 hbc + · rw [(h.eq_iff a b).mp e1]; exact hbc + · exact absurd e1 hab + +theorem lawful_nat : LawfulOrder (fun a b : Nat => compare a b) where + eq_iff _ _ := Nat.compare_eq_eq + swap a b := Nat.compare_swap a b + lt_trans _ _ _ h1 h2 := Nat.compare_eq_lt.mpr + (Nat.lt_trans (Nat.compare_eq_lt.mp h1) (Nat.compare_eq_lt.mp h2)) + +theorem lawful_char : LawfulOrder (fun a b : Char => compare a.toNat b.toNat) where + eq_iff a b := by simp only [Nat.compare_eq_eq, Char.toNat_inj] + swap a b := Nat.compare_swap _ _ + lt_trans _ _ _ h1 h2 := Nat.compare_eq_lt.mpr + (Nat.lt_trans (Nat.compare_eq_lt.mp h1) (Nat.compare_eq_lt.mp h2)) + +/-- Lists by the first element that differs; a list before any longer + list it starts. -/ +def listOrder {α : Type} (o : α → α → Ordering) : List α → List α → Ordering + | [], [] => .eq + | [], _ :: _ => .lt + | _ :: _, [] => .gt + | a :: as, b :: bs => (o a b).then (listOrder o as bs) + +theorem lawful_list {α : Type} {o : α → α → Ordering} (h : LawfulOrder o) : + LawfulOrder (listOrder o) where + eq_iff := by + intro as bs + induction as generalizing bs with + | nil => cases bs <;> simp [listOrder] + | cons a as ih => + cases bs with + | nil => simp [listOrder] + | cons b bs => simp [listOrder, h.eq_iff, ih] + swap := by + intro as bs + induction as generalizing bs with + | nil => cases bs <;> rfl + | cons a as ih => + cases bs with + | nil => rfl + | cons b bs => simp [listOrder, Ordering.swap_then, h.swap, ih] + lt_trans := by + intro as bs cs + induction as generalizing bs cs with + | nil => + cases bs <;> cases cs <;> simp [listOrder] + | cons a as ih => + cases bs with + | nil => simp [listOrder] + | cons b bs => + cases cs with + | nil => simp [listOrder] + | cons c cs => + simp only [listOrder, Ordering.then_eq_lt] + rintro (h1 | ⟨h1, h1'⟩) (h2 | ⟨h2, h2'⟩) + · exact Or.inl (h.lt_trans a b c h1 h2) + · rw [← (h.eq_iff b c).mp h2]; exact Or.inl h1 + · rw [(h.eq_iff a b).mp h1]; exact Or.inl h2 + · rw [(h.eq_iff a b).mp h1] + exact Or.inr ⟨h2, ih bs cs h1' h2'⟩ + +theorem compareAscii_eq_listOrder : + ∀ a b : List Char, compareAscii a b = listOrder (fun a b : Char => compare a.toNat b.toNat) a b + | [], [] => rfl + | [], _ :: _ => rfl + | _ :: _, [] => rfl + | x :: xs, y :: ys => by + simp only [compareAscii, listOrder, compareAscii_eq_listOrder xs ys] + +theorem lawful_ascii : LawfulOrder compareAscii := by + have h := lawful_list lawful_char + have e : compareAscii = listOrder (fun a b : Char => compare a.toNat b.toNat) := + funext fun a => funext fun b => compareAscii_eq_listOrder a b + rw [e]; exact h + +theorem lawful_ident : LawfulOrder Ident.compare where + eq_iff a b := by + cases a <;> cases b <;> + simp [Ident.compare, lawful_ascii.eq_iff, String.toList_inj] + swap a b := by + cases a <;> cases b <;> simp [Ident.compare, Nat.compare_swap, lawful_ascii.swap] + lt_trans a b c := by + cases a <;> cases b <;> cases c <;> simp only [Ident.compare, reduceCtorEq, imp_self, + implies_true, false_implies] + · exact lawful_nat.lt_trans _ _ _ + · exact lawful_ascii.lt_trans _ _ _ + +theorem compareIdents_eq_listOrder : + ∀ a b : List Ident, compareIdents a b = listOrder Ident.compare a b + | [], [] => rfl + | [], _ :: _ => rfl + | _ :: _, [] => rfl + | x :: xs, y :: ys => by + simp only [compareIdents, listOrder, compareIdents_eq_listOrder xs ys] + +theorem lawful_idents : LawfulOrder compareIdents := by + have e : compareIdents = listOrder Ident.compare := + funext fun a => funext fun b => compareIdents_eq_listOrder a b + rw [e]; exact lawful_list lawful_ident + +theorem lawful_pre : LawfulOrder comparePre where + eq_iff a b := by + cases a <;> cases b <;> simp [comparePre, lawful_idents.eq_iff] + swap a b := by + cases a <;> cases b <;> simp [comparePre, lawful_idents.swap] + lt_trans a b c := by + cases a <;> cases b <;> cases c <;> simp only [comparePre, reduceCtorEq, imp_self, + implies_true, false_implies] + exact lawful_idents.lt_trans _ _ _ + +/-- Pairs, by the first part and then the second. -/ +def pairOrder {α β : Type} (o₁ : α → α → Ordering) (o₂ : β → β → Ordering) : + α × β → α × β → Ordering := + fun x y => (o₁ x.1 y.1).then (o₂ x.2 y.2) + +theorem lawful_pair {α β : Type} {o₁ : α → α → Ordering} {o₂ : β → β → Ordering} + (h₁ : LawfulOrder o₁) (h₂ : LawfulOrder o₂) : LawfulOrder (pairOrder o₁ o₂) where + eq_iff x y := by + simp [pairOrder, h₁.eq_iff, h₂.eq_iff, Prod.ext_iff] + swap x y := by + simp [pairOrder, Ordering.swap_then, h₁.swap, h₂.swap] + lt_trans x y z := by + simp only [pairOrder, Ordering.then_eq_lt] + rintro (h1 | ⟨h1, h1'⟩) (h2 | ⟨h2, h2'⟩) + · exact Or.inl (h₁.lt_trans _ _ _ h1 h2) + · rw [← (h₁.eq_iff _ _).mp h2]; exact Or.inl h1 + · rw [(h₁.eq_iff _ _).mp h1]; exact Or.inl h2 + · rw [(h₁.eq_iff _ _).mp h1] + exact Or.inr ⟨h2, h₂.lt_trans _ _ _ h1' h2'⟩ + +/-- What precedence reads of a version. -/ +def key (v : Version) : Nat × Nat × Nat × List Ident := (v.major, v.minor, v.patch, v.pre) + +/-- The order on keys. -/ +def keyOrder : Nat × Nat × Nat × List Ident → Nat × Nat × Nat × List Ident → Ordering := + pairOrder (fun a b : Nat => compare a b) + (pairOrder (fun a b : Nat => compare a b) (pairOrder (fun a b : Nat => compare a b) comparePre)) + +theorem lawful_key : LawfulOrder keyOrder := + lawful_pair lawful_nat (lawful_pair lawful_nat (lawful_pair lawful_nat lawful_pre)) + +theorem compare_key (a b : Version) : a.compare b = keyOrder (key a) (key b) := rfl + +end SemVer.Proofs diff --git a/README.md b/README.md index 0c6c680..c508a02 100644 --- a/README.md +++ b/README.md @@ -1,2 +1,93 @@ -# semver -lean semver +# semver: Semantic Versioning, proved + +This library reads and writes Semantic Versioning 2.0.0 strings in Lean, and gives the precedence of two versions. Machine-checked proofs show four things: + +- The parser accepts exactly the strings of the grammar on semver.org, and nothing else. +- It returns each part as written, and printing what it returns gives the string back. +- `compare` follows the precedence rules of section 11, as `Spec/Defs.lean` states them. +- That order is consistent: swapping the sides swaps the answer, it is transitive, and two versions tie exactly when they differ in build metadata at most. + +So `01.0.0`, `1.0.0-01`, `v1.0.0`, `1.0` and `1.0.0 ` are rejected, `1.0.0-0a` and `1.0.0+001` are accepted, and numbers have no upper limit. + +It is tested against python-semver, with the regular expression semver.org gives as a second check; `tests/TEST-RESULTS.md` has the record. It is a project of [Proven Commons](https://github.com/Proven-Commons/mission), built to the verified bar published there. + +Status: in progress. The specification has not yet been approved by a reviewer apart from its author, so this is not verified. + +## Use it + +From Lean: + +- `SemVer.parse : String → Option SemVer.Version` +- `SemVer.Version.print : SemVer.Version → String` +- `SemVer.Version.compare : SemVer.Version → SemVer.Version → Ordering` + +`SPEC.md` says what each one does. + +## What is proved + +The statements are in `Spec.lean`, the definitions they use in `Spec/Defs.lean`, and the proofs in `Proofs/`. + +| Claim | Theorem | +|-------|---------| +| `print` writes the three numbers in decimal, then the pre-release and build identifiers, each part left out when it is empty. | `Spec.print_eq` | +| `parse` returns a version exactly when the version is well formed and the string is how it is written. So it returns the parts as written, and there is one way to write each version. | `Spec.parse_iff` | +| `parse` accepts exactly the strings of the grammar on semver.org, as `Spec/Defs.lean` writes it out. It rejects leading zeros in numbers and in numeric pre-release identifiers, empty identifiers, characters other than ASCII letters, digits and hyphens, and anything before or after the version. | `Spec.parse_isSome_iff` | +| What `parse` returns is well formed. | `Spec.parse_valid` | +| Printing a well formed version and parsing the result gives it back. | `Spec.parse_print` | +| Parsing a string and printing the result gives the string back. | `Spec.print_parse` | +| `compare` follows section 11: major, minor and patch as numbers, then a version with a pre-release part below one without, then the pre-release identifiers from the left, numbers as numbers and below other identifiers, other identifiers in ASCII order, and a shorter list first when it runs out. | `Spec.compare_eq` | +| Build metadata plays no part: changing it on either side changes no answer. | `Spec.compare_build` | +| Two versions have the same precedence exactly when they differ in build metadata at most. | `Spec.compare_eq_eq_iff` | +| Swapping the two versions swaps the answer, and precedence is transitive. So sorting by it is consistent. | `Spec.compare_swap`, `Spec.compare_trans`, `Spec.compare_lt_trans` | +| The examples of sections 9 to 11, both ways; a selection of strings outside the grammar; and strings inside it that loose parsers get wrong. | `Spec.semver_examples`, `Spec.precedence_examples`, `Spec.reject_vectors`, `Spec.accept_vectors` | + +The command-line tool in `Main.lean` answers `parse` and `compare` requests with these functions directly. + +## What is not proved + +- Reading requests and printing answers in `Main.lean`: the hex parsing and printing, and the request format. The differential tests cover them, with malformed requests and CR LF line endings. +- Whether a project followed the rules of sections 1 to 8, on when to change which number. Those rules are about people's choices, not strings. +- Anything outside section 11's precedence. Build metadata has no order here, though some libraries order it to break ties. There are no version ranges, such as `^1.2.3` or `>=1.0.0 <2.0.0`, and no loose forms, such as `v1.2.3` or `1.2`. +- Speed and size. The code works on lists and recurses once per character, which suits proofs, not bulk data. With an 8 MB stack, a string of 4 million characters is answered, but one of 16 million runs out of stack. The program then stops, with the answers before it already written, and never gives a wrong answer. Reading and printing a number takes time that grows with the square of its length: a number of 100,000 digits takes seconds. +- Numbers with more than 4,300 digits are outside the tests. Python refuses to read them by default, so the oracle cannot answer. + +## What you must trust + +- The Lean kernel and the five external kernels shipped with Lean, which all check the proofs. +- `lake comparator`, which builds the statements and the proofs in a sandbox, exports them, and checks that each proof proves exactly its statement. +- bubblewrap and the Linux kernel's namespaces, which keep the untrusted build from tampering with that check. +- 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 (by `implemented_by` and `extern`), such as the arithmetic on natural numbers, `Nat.repr`, which `print` uses to write numbers, and the conversion between strings and lists. +- The operating system and hardware it runs on. +- python-semver 3.1.0, as the oracle in the differential tests. The record names its version. + +This project has no dependencies beyond Lean itself. + +## Re-check it + +Needs Linux, [elan](https://github.com/leanprover/elan), bubblewrap (`apt install bubblewrap`), and Python 3. + +``` +lake build +lake comparator --paranoid +python3 tests/run_tests.py +``` + +`lake comparator --paranoid` builds the statements and the proofs in a sandbox. It checks that each theorem in `Proofs/` proves exactly the statement in `Spec.lean`, using only the axioms `propext`, `Classical.choice`, and `Quot.sound`, and replays it through every kernel shipped with Lean. + +The test script compares the tool with python-semver. It runs every string of up to eight characters over `0`, `1`, `.`, `-`, `+` and `a`, the examples of the specification, and random and mutated versions from a recorded seed, then compares pairs of versions. It then rewrites `tests/TEST-RESULTS.md`. When Python lacks python-semver 3.1.0, it installs it into `.lake/oracle-venv`, checked against the hashes in `tests/oracle-requirements.txt`. + +## Layout + +- `SemVer/Types.lean`: the `Version` and `Ident` types. +- `SemVer/Basic.lean`: the code under proof. +- `Spec.lean`: the statements, with `sorry` for proofs. A reviewer approves this file. +- `Spec/Defs.lean`: the definitions the statements use, written from the grammar and section 11, with checks against the specification's examples. +- `Proofs.lean` and `Proofs/`: the proofs, under the same names. +- `Main.lean`: the command-line tool the tests drive. +- `lakefile.toml`: the build. It names the package and its version, its libraries and executable, and the default targets, and sets nothing else. +- `comparator.json`: which theorems `lake comparator` checks, and which axioms it allows. +- `bar.toml`: the record for the bar check: status, authors, approvals, and where things are. +- `SPEC.md`: the specification in plain words. +- `tests/run_tests.py`: the differential tests. +- `tests/oracle-requirements.txt`: the oracle's version, pinned by hash. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..e1447c1 --- /dev/null +++ b/SPEC.md @@ -0,0 +1,96 @@ +# Specification: semver + +This library reads and writes version strings in the form Semantic Versioning 2.0.0 sets out (https://semver.org/spec/v2.0.0.html), such as `1.0.0-beta.11+exp.sha.5114f85`. It also gives the precedence of two versions, as section 11 of that specification defines it. A reviewer who did not write this specification approves it. The approval also covers `Spec.lean`, `Spec/Defs.lean`, `SemVer/Types.lean`, and the other files `bar.toml` lists. + +## The format + +The scope is the `` rule of the Backus–Naur form grammar on semver.org: + +``` + ::= + | "-" + | "+" + | "-" "+" + ::= "." "." +``` + +`Spec/Defs.lean` writes out each rule of the grammar. In plain words: + +- The major, minor and patch numbers are numeric identifiers: `0`, or ASCII digits that do not start with `0` (section 2). There is no upper limit on their size. +- The pre-release part follows a `-`. It is one or more identifiers joined by `.`. Each is a numeric identifier, which has no leading zero, or an alphanumeric identifier. An alphanumeric identifier is ASCII letters, digits and hyphens, with at least one letter or hyphen. So `0a` and `--` are identifiers, and `01` is not (section 9). +- The build part follows a `+`. It is one or more identifiers joined by `.`. Each is one or more ASCII letters, digits and hyphens, and may start with `0` (section 10). +- No identifier is empty. +- The parser reads nothing else. That includes: + - a `v` or `=` before the version; + - spaces or a line break before or after it; + - a version with fewer or more than three numbers; + - digits and letters outside ASCII, such as `١` and `１`; + - the ranges and shorthands that package managers accept, such as `^1.2` or `1.x`. + +## The value + +`parse` returns a `Version`: the three numbers, the list of pre-release identifiers, and the list of build identifiers. Each pre-release identifier is a number (`num`) when it is all digits, and its text (`alnum`) otherwise. Each build identifier is its text. A list is empty when its part is absent. `Spec.Valid` says which values are well formed: every `alnum` identifier is an alphanumeric identifier, and every build identifier is one or more identifier characters. + +`Version.print` writes a version: the three numbers in decimal, then `-` and the pre-release identifiers, then `+` and the build identifiers. Each list is joined by `.` and left out, with its sign, when it is empty. + +## Precedence + +`Version.compare` gives the precedence of `a` against `b`: `.lt` when `a` has lower precedence, `.eq` when the two have the same precedence, and `.gt` otherwise. It follows section 11: + +1. Build identifiers play no part. +2. Major, minor and patch are compared as numbers, in that order. The first difference decides. +3. With the same three numbers, a version with a pre-release part comes before one without. +4. Two pre-release parts are compared identifier by identifier, from the left, until one differs: + 1. Two numbers are compared as numbers. + 2. Two other identifiers are compared in ASCII order, character by character. When one runs out first, it comes first. + 3. A number comes before any other identifier. + 4. When one list runs out first, all its identifiers being equal to the other's, it comes first. + +So two versions have the same precedence exactly when they differ in build identifiers at most. `Spec.precedence` in `Spec/Defs.lean` states these rules as written. + +## Errors + +`parse` returns `none` for any string it does not accept. No function can fail any other way. + +## The command-line tool + +The command-line tool in `Main.lean` has two modes: + +- `semver check VERSION...` prints each version's printed form, or `invalid`. It exits with 1 when any version is invalid. +- `semver serve` answers requests from the differential tests, one per line. Each string is sent as the hex digits of its UTF-8 bytes. The header comment of `Main.lean` gives the protocol. + +Every answer comes from `parse`, `Version.print` and `Version.compare`. + +## What must always hold + +Each property is a theorem in `Spec.lean`, under the name given. The definitions the statements use are in `Spec/Defs.lean`. They are written from the specification and checked against its examples. + +| Property | Theorem | +|----------|---------| +| `print` writes a version as `Spec.render` sets out. | `Spec.print_eq` | +| `parse` returns `v` exactly when `v` is well formed and the string is how `v` is written. | `Spec.parse_iff` | +| `parse` accepts exactly the strings of the grammar on semver.org. | `Spec.parse_isSome_iff` | +| What `parse` returns is well formed. | `Spec.parse_valid` | +| Printing then parsing gives a well formed version back. | `Spec.parse_print` | +| Parsing then printing gives the string back. | `Spec.print_parse` | +| `compare` gives the precedence of section 11, as `Spec.precedence` states it. | `Spec.compare_eq` | +| Changing the build identifiers of either version changes no answer of `compare`. | `Spec.compare_build` | +| `compare` gives `.eq` exactly when the numbers and the pre-release identifiers are the same. | `Spec.compare_eq_eq_iff` | +| Swapping the two versions swaps the answer. | `Spec.compare_swap` | +| Precedence is transitive, both "at most" and "lower". | `Spec.compare_trans`, `Spec.compare_lt_trans` | +| The examples of sections 9 and 10 parse to the parts the specification reads them as. | `Spec.semver_examples` | +| The example lists of section 11 are in rising order, every version below every later one. Two versions that differ only in build metadata have the same precedence. | `Spec.precedence_examples` | +| Leading zeros, missing and extra parts, empty identifiers, characters outside the grammar, and text around the version are rejected. | `Spec.reject_vectors` | +| Leading zeros in alphanumeric and build identifiers, an identifier of hyphens, and numbers past 64 bits are accepted. | `Spec.accept_vectors` | + +Together, these fix every output. + +- `parse` is fixed for every string by `Spec.parse_iff`. +- `print` is fixed for every version by `Spec.print_eq`. +- `compare` is fixed for every pair of versions by `Spec.compare_eq`. +- A parser that accepted nothing would meet `Spec.parse_valid`, but it would fail `Spec.parse_iff`, `Spec.parse_isSome_iff` and `Spec.parse_print`. +- A parser that accepted too much would fail `Spec.parse_iff` and `Spec.parse_isSome_iff`. + +## Oracle + +The differential tests compare the tool with python-semver 3.1.0, `semver.Version.parse` and `Version.compare`. Every string python-semver accepts must also match, in full, the regular expression semver.org gives in its FAQ, and every string it rejects must not. diff --git a/SemVer.lean b/SemVer.lean new file mode 100644 index 0000000..fa61b23 --- /dev/null +++ b/SemVer.lean @@ -0,0 +1,2 @@ +import SemVer.Types +import SemVer.Basic diff --git a/SemVer/Basic.lean b/SemVer/Basic.lean new file mode 100644 index 0000000..8315eee --- /dev/null +++ b/SemVer/Basic.lean @@ -0,0 +1,142 @@ +/- + Reading and writing Semantic Versioning 2.0.0 strings, and the + precedence of section 11. +-/ + +import SemVer.Types + +namespace SemVer + +/-! ## Printing -/ + +/-- A pre-release identifier as written: a number in decimal, or the + identifier itself. -/ +def Ident.print : Ident → String + | .num n => toString n + | .alnum s => s + +/-- The version as SemVer 2.0.0 writes it: the three numbers in decimal, + then `-` and the pre-release identifiers, then `+` and the build + identifiers, each list joined by `.` and left out when empty. -/ +def Version.print (v : Version) : String := + toString v.major ++ "." ++ toString v.minor ++ "." ++ toString v.patch ++ + (if v.pre.isEmpty then "" else "-" ++ ".".intercalate (v.pre.map Ident.print)) ++ + (if v.build.isEmpty then "" else "+" ++ ".".intercalate v.build) + +/-! ## Parsing -/ + +/-- ``: `0` to `9`. -/ +def isDigit (c : Char) : Bool := '0' ≤ c && c ≤ '9' + +/-- ``: an ASCII digit, letter or hyphen. -/ +def isIdentChar (c : Char) : Bool := + isDigit c || ('A' ≤ c && c ≤ 'Z') || ('a' ≤ c && c ≤ 'z') || c == '-' + +/-- The characters before the first `sep`, and the characters after it + when there is one. -/ +def breakAt (sep : Char) : List Char → List Char × Option (List Char) + | [] => ([], none) + | c :: cs => + if c = sep then ([], some cs) + else + let r := breakAt sep cs + (c :: r.1, r.2) + +/-- ``: `0`, or digits with no leading zero. -/ +def parseNumeric : List Char → Option Nat + | [] => none + | c :: cs => + if (c :: cs).all isDigit && (c != '0' || cs.isEmpty) then + some (Nat.ofDigitChars 10 (c :: cs) 0) + else none + +/-- ``: a numeric identifier, or an alphanumeric + one, which has a character other than a digit. -/ +def parsePreIdent (cs : List Char) : Option Ident := + if cs.all isDigit then (parseNumeric cs).map .num + else if cs.all isIdentChar then some (.alnum (String.ofList cs)) + else none + +/-- ``: one or more identifier characters. Leading + zeros are allowed here. -/ +def parseBuildIdent (cs : List Char) : Option String := + if !cs.isEmpty && cs.all isIdentChar then some (String.ofList cs) else none + +/-- Applies `f` to each part, and fails if it fails on any. -/ +def parseEach (f : List Char → Option α) : List (List Char) → Option (List α) + | [] => some [] + | p :: ps => do + let a ← f p + let as ← parseEach f ps + pure (a :: as) + +/-- The identifiers after a separator, joined by `.`: none when the + separator is absent, and at least one when it is present. -/ +def parseDotted (f : List Char → Option α) : Option (List Char) → Option (List α) + | none => some [] + | some p => parseEach f (p.splitOn '.') + +/-- ``, as a list of characters. -/ +def parseChars (cs : List Char) : Option Version := + -- `+` appears in no identifier, so the first one starts the build + -- part; `-` appears in no number, so the first one before it starts + -- the pre-release part. + let (main, buildPart) := breakAt '+' cs + let (core, prePart) := breakAt '-' main + match core.splitOn '.' with + | [a, b, c] => do + let major ← parseNumeric a + let minor ← parseNumeric b + let patch ← parseNumeric c + let pre ← parseDotted parsePreIdent prePart + let build ← parseDotted parseBuildIdent buildPart + pure { major, minor, patch, pre, build } + | _ => none + +/-- Reads a Semantic Versioning 2.0.0 string. The whole string must be + the version: no `v` before it and no space around it. -/ +def parse (s : String) : Option Version := parseChars s.toList + +/-! ## Precedence -/ + +/-- Two lists of characters in ASCII order: by the first character that + differs, and a list before any longer list it starts. -/ +def compareAscii : List Char → List Char → Ordering + | [], [] => .eq + | [], _ :: _ => .lt + | _ :: _, [] => .gt + | a :: as, b :: bs => (compare a.toNat b.toNat).then (compareAscii as bs) + +/-- Two pre-release identifiers: numbers by value, other identifiers in + ASCII order, and a number before any other identifier. -/ +def Ident.compare : Ident → Ident → Ordering + | .num a, .num b => Ord.compare a b + | .num _, .alnum _ => .lt + | .alnum _, .num _ => .gt + | .alnum a, .alnum b => compareAscii a.toList b.toList + +/-- Two lists of pre-release identifiers: by the first identifier that + differs, and a list before any longer list it starts. -/ +def compareIdents : List Ident → List Ident → Ordering + | [], [] => .eq + | [], _ :: _ => .lt + | _ :: _, [] => .gt + | a :: as, b :: bs => (a.compare b).then (compareIdents as bs) + +/-- The pre-release parts of two versions with the same numbers: a + version with no pre-release part comes after one with a pre-release + part. -/ +def comparePre : List Ident → List Ident → Ordering + | [], [] => .eq + | [], _ :: _ => .gt + | _ :: _, [] => .lt + | as, bs => compareIdents as bs + +/-- The precedence of section 11: major, minor and patch by value, then + the pre-release part. Build identifiers play no part. -/ +def Version.compare (a b : Version) : Ordering := + (Ord.compare a.major b.major).then <| + (Ord.compare a.minor b.minor).then <| + (Ord.compare a.patch b.patch).then (comparePre a.pre b.pre) + +end SemVer diff --git a/SemVer/Types.lean b/SemVer/Types.lean new file mode 100644 index 0000000..dc370cd --- /dev/null +++ b/SemVer/Types.lean @@ -0,0 +1,32 @@ +/- + What a version is: the values the parser produces and the printer + takes. Part of the approved specification, with `Spec.lean` and + `Spec/Defs.lean`, since every statement is about these types. + + A value holds each part of a Semantic Versioning 2.0.0 string as + written. Which values are valid is `Spec.Valid`, in `Spec/Defs.lean`. +-/ + +namespace SemVer + +/-- A pre-release identifier, section 9 of SemVer 2.0.0. -/ +inductive Ident where + /-- A numeric identifier: digits only, read as a number. -/ + | num (n : Nat) + /-- An alphanumeric identifier: ASCII letters, digits and hyphens, + with at least one letter or hyphen. -/ + | alnum (s : String) + deriving DecidableEq, Repr + +/-- A version: `major.minor.patch`, then the pre-release identifiers + after `-`, then the build identifiers after `+`. Either list is + empty when its part is absent. -/ +structure Version where + major : Nat + minor : Nat + patch : Nat + pre : List Ident + build : List String + deriving DecidableEq, Repr + +end SemVer diff --git a/Spec.lean b/Spec.lean new file mode 100644 index 0000000..4bea671 --- /dev/null +++ b/Spec.lean @@ -0,0 +1,154 @@ +/- + The specification as Lean statements: the challenge file. + + A reviewer who did not write this file approves it, and `bar.toml` + records the hash it had then. The proofs live in `Proofs.lean`, under + the same names; `lake comparator` checks that each one proves exactly + the statement written here. The `sorry`s below are expected in this + file only. + + The definitions the statements use, written from Semantic Versioning + 2.0.0, are in `Spec/Defs.lean`, and the types in `SemVer/Types.lean`. + Both are part of the specification too. +-/ + +import SemVer +import Spec.Defs + +open SemVer + +/-! ## Printing -/ + +/-- `print` writes a version as `Spec.render` sets out: the numbers in + decimal, then the pre-release and build parts, each left out when + empty. -/ +theorem Spec.print_eq (v : Version) : v.print.toList = Spec.render v := sorry + +/-! ## Parsing -/ + +/-- `parse` returns `v` exactly when `v` is well formed and the string + is how `v` is written. So it returns the parts as written, accepts + no other spelling of them, and rejects every string that is not how + some well formed version is written. -/ +theorem Spec.parse_iff (s : String) (v : Version) : + parse s = some v ↔ Spec.Valid v ∧ s.toList = Spec.render v := sorry + +/-- `parse` accepts exactly the strings of the grammar on semver.org. -/ +theorem Spec.parse_isSome_iff (s : String) : + (parse s).isSome ↔ Spec.ValidSemVer s.toList := sorry + +/-- What `parse` returns is well formed. -/ +theorem Spec.parse_valid (s : String) (v : Version) (h : parse s = some v) : + Spec.Valid v := sorry + +/-- Round trip: printing a well formed version and parsing the result + gives it back. -/ +theorem Spec.parse_print (v : Version) (h : Spec.Valid v) : parse v.print = some v := sorry + +/-- Round trip: parsing a string and printing the result gives the + string back. -/ +theorem Spec.print_parse (s : String) (v : Version) (h : parse s = some v) : + v.print = s := sorry + +/-! ## Precedence -/ + +/-- `compare` gives the precedence of section 11. -/ +theorem Spec.compare_eq (a b : Version) : a.compare b = Spec.precedence a b := sorry + +/-- Build identifiers play no part in precedence (11.1): changing them + on either side changes nothing. -/ +theorem Spec.compare_build (a b : Version) (x y : List String) : + ({ a with build := x } : Version).compare { b with build := y } = a.compare b := sorry + +/-- Two versions have the same precedence exactly when they differ in + build identifiers at most. -/ +theorem Spec.compare_eq_eq_iff (a b : Version) : + a.compare b = .eq ↔ + a.major = b.major ∧ a.minor = b.minor ∧ a.patch = b.patch ∧ a.pre = b.pre := sorry + +/-- Swapping the two sides swaps the answer. -/ +theorem Spec.compare_swap (a b : Version) : (a.compare b).swap = b.compare a := sorry + +/-- Precedence is transitive, so sorting by it is consistent. -/ +theorem Spec.compare_trans (a b c : Version) (hab : a.compare b ≠ .gt) + (hbc : b.compare c ≠ .gt) : a.compare c ≠ .gt := sorry + +/-- Strict precedence is transitive too. -/ +theorem Spec.compare_lt_trans (a b c : Version) (hab : a.compare b = .lt) + (hbc : b.compare c = .lt) : a.compare c = .lt := sorry + +/-! ## Test vectors -/ + +/-- The examples of sections 9 and 10, with the parts they are read + as. -/ +theorem Spec.semver_examples : + parse "1.0.0-alpha" = some ⟨1, 0, 0, [.alnum "alpha"], []⟩ ∧ + parse "1.0.0-alpha.1" = some ⟨1, 0, 0, [.alnum "alpha", .num 1], []⟩ ∧ + parse "1.0.0-0.3.7" = some ⟨1, 0, 0, [.num 0, .num 3, .num 7], []⟩ ∧ + parse "1.0.0-x.7.z.92" = some ⟨1, 0, 0, [.alnum "x", .num 7, .alnum "z", .num 92], []⟩ ∧ + parse "1.0.0-x-y-z.--" = some ⟨1, 0, 0, [.alnum "x-y-z", .alnum "--"], []⟩ ∧ + parse "1.0.0-alpha+001" = some ⟨1, 0, 0, [.alnum "alpha"], ["001"]⟩ ∧ + parse "1.0.0+20130313144700" = some ⟨1, 0, 0, [], ["20130313144700"]⟩ ∧ + parse "1.0.0-beta+exp.sha.5114f85" = + some ⟨1, 0, 0, [.alnum "beta"], ["exp", "sha", "5114f85"]⟩ ∧ + parse "1.0.0+21AF26D3----117B344092BD" = some ⟨1, 0, 0, [], ["21AF26D3----117B344092BD"]⟩ := + sorry + +/-- The examples of section 11, each list in rising order: every + version in it has lower precedence than every later one. And two + versions that differ only in build metadata have the same + precedence (section 10). -/ +theorem Spec.precedence_examples : + ["1.0.0", "2.0.0", "2.1.0", "2.1.1"].Pairwise + (fun s t => Spec.compareStrings s t = some .lt) ∧ + ["1.0.0-alpha", "1.0.0"].Pairwise (fun s t => Spec.compareStrings s t = some .lt) ∧ + ["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"].Pairwise + (fun s t => Spec.compareStrings s t = some .lt) ∧ + Spec.compareStrings "1.0.0-alpha+001" "1.0.0-alpha" = some .eq ∧ + Spec.compareStrings "1.0.0+20130313144700" "1.0.0+21AF26D3----117B344092BD" = some .eq := + sorry + +/-- Strings outside the grammar: leading zeros in numbers, missing or + extra parts, empty identifiers, characters outside ASCII letters, + digits and hyphens, and anything before or after the version. -/ +theorem Spec.reject_vectors : + parse "01.0.0" = none ∧ + parse "1.02.0" = none ∧ + parse "1.0.00" = none ∧ + parse "1.0.0-01" = none ∧ + parse "1.0" = none ∧ + parse "1.0.0.0" = none ∧ + parse "1.0.0-" = none ∧ + parse "1.0.0+" = none ∧ + parse "1.0.0-alpha..1" = none ∧ + parse "1.0.0-alpha." = none ∧ + parse "1.0.0+build..1" = none ∧ + parse "1.0.0+a+b" = none ∧ + parse "1.0.0-alpha_beta" = none ∧ + parse "1.0.0-alpha.é" = none ∧ + parse "1.0.0-١" = none ∧ + parse "１.0.0" = none ∧ + parse "v1.0.0" = none ∧ + parse "=1.0.0" = none ∧ + parse " 1.0.0" = none ∧ + parse "1.0.0 " = none ∧ + parse "1.0.0\n" = none ∧ + parse "-1.0.0" = none ∧ + parse "1.0.0-+" = none ∧ + parse "" = none := + sorry + +/-- Strings inside the grammar that loose parsers often get wrong: a + pre-release identifier may have leading zeros when it is not all + digits, a build identifier may have them always, and a hyphen may + start an identifier. -/ +theorem Spec.accept_vectors : + parse "1.0.0-0a" = some ⟨1, 0, 0, [.alnum "0a"], []⟩ ∧ + parse "1.0.0-0" = some ⟨1, 0, 0, [.num 0], []⟩ ∧ + parse "1.0.0+001" = some ⟨1, 0, 0, [], ["001"]⟩ ∧ + parse "1.0.0--" = some ⟨1, 0, 0, [.alnum "-"], []⟩ ∧ + parse "1.0.0-a-+b-" = some ⟨1, 0, 0, [.alnum "a-"], ["b-"]⟩ ∧ + parse "0.0.0" = some ⟨0, 0, 0, [], []⟩ ∧ + parse "18446744073709551616.0.0" = some ⟨18446744073709551616, 0, 0, [], []⟩ := + sorry diff --git a/Spec/Defs.lean b/Spec/Defs.lean new file mode 100644 index 0000000..e2056e2 --- /dev/null +++ b/Spec/Defs.lean @@ -0,0 +1,256 @@ +/- + The definitions the specification uses, written from Semantic + Versioning 2.0.0 (https://semver.org/spec/v2.0.0.html) independently + of the code in `SemVer/`. Part of the approved specification, with + `Spec.lean` and `SemVer/Types.lean`. + + Both the challenge file and the proofs import this file, so each + statement means the same thing on both sides. The `example`s check + the definitions against the specification's own examples. A mistake + in either fails the build. +-/ + +import SemVer + +open SemVer + +/-! ## Characters + +From the Backus–Naur form grammar on semver.org: + +``` + ::= "0" | + ::= "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9" + ::= "A" | "B" | ... | "Z" | "a" | "b" | ... | "z" + ::= | "-" + ::= | +``` +-/ + +/-- ``. -/ +abbrev Spec.Digit (c : Char) : Prop := '0' ≤ c ∧ c ≤ '9' + +/-- ``. -/ +abbrev Spec.PositiveDigit (c : Char) : Prop := '1' ≤ c ∧ c ≤ '9' + +/-- ``: ASCII letters only. -/ +abbrev Spec.Letter (c : Char) : Prop := ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') + +/-- ``. -/ +abbrev Spec.NonDigit (c : Char) : Prop := Spec.Letter c ∨ c = '-' + +/-- ``. -/ +abbrev Spec.IdentChar (c : Char) : Prop := Spec.Digit c ∨ Spec.NonDigit c + +example : "0123456789".toList.all (fun c => decide (Spec.Digit c)) := by decide +example : "123456789".toList.all (fun c => decide (Spec.PositiveDigit c)) := by decide +example : ¬ Spec.PositiveDigit '0' := by decide +example : ("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz-".toList.all fun c => + decide (Spec.NonDigit c)) := by decide +-- The neighbours of each range, and characters people mistake for +-- them, are not identifier characters. +example : ("/:@[`{.+_ \n٣０éα".toList.all fun c => !decide (Spec.IdentChar c)) := by decide + +/-! ## The grammar + +``` + ::= + | "-" + | "+" + | "-" "+" + ::= "." "." + ::= + ::= + ::= + ::= + ::= + | "." + ::= + ::= + | "." + ::= | + ::= | + ::= + | + | + | + ::= "0" | | + ::= + | + ::= | +``` + +Each rule below is one of these, over lists of characters. +-/ + +/-- ``: one or more digits. -/ +def Spec.Digits (cs : List Char) : Prop := cs ≠ [] ∧ ∀ c ∈ cs, Spec.Digit c + +/-- ``: `0`, or a positive digit followed by any + number of digits. So no leading zero. -/ +def Spec.NumericIdent (cs : List Char) : Prop := + cs = ['0'] ∨ ∃ c rest, cs = c :: rest ∧ Spec.PositiveDigit c ∧ ∀ d ∈ rest, Spec.Digit d + +/-- ``: the four forms of the rule together are + a non-digit with any identifier characters, possibly none, before + and after it. -/ +def Spec.AlnumIdent (cs : List Char) : Prop := + ∃ xs c ys, cs = xs ++ c :: ys ∧ Spec.NonDigit c ∧ + (∀ d ∈ xs, Spec.IdentChar d) ∧ ∀ d ∈ ys, Spec.IdentChar d + +/-- ``. -/ +def Spec.PreReleaseIdent (cs : List Char) : Prop := + Spec.AlnumIdent cs ∨ Spec.NumericIdent cs + +/-- ``. -/ +def Spec.BuildIdent (cs : List Char) : Prop := + Spec.AlnumIdent cs ∨ Spec.Digits cs + +/-- ``: one or more parts, each of them + meeting `P`, with `.` between each two. -/ +def Spec.DotSeparated (P : List Char → Prop) (cs : List Char) : Prop := + ∃ parts, parts ≠ [] ∧ (∀ p ∈ parts, P p) ∧ cs = ['.'].intercalate parts + +/-- ``, from its three parts. -/ +def Spec.core (major minor patch : List Char) : List Char := + major ++ ['.'] ++ minor ++ ['.'] ++ patch + +/-- ``: the four forms of the rule. -/ +def Spec.ValidSemVer (cs : List Char) : Prop := + ∃ major minor patch, + Spec.NumericIdent major ∧ Spec.NumericIdent minor ∧ Spec.NumericIdent patch ∧ + (cs = Spec.core major minor patch ∨ + (∃ pre, Spec.DotSeparated Spec.PreReleaseIdent pre ∧ + cs = Spec.core major minor patch ++ ['-'] ++ pre) ∨ + (∃ build, Spec.DotSeparated Spec.BuildIdent build ∧ + cs = Spec.core major minor patch ++ ['+'] ++ build) ∨ + (∃ pre build, Spec.DotSeparated Spec.PreReleaseIdent pre ∧ + Spec.DotSeparated Spec.BuildIdent build ∧ + cs = Spec.core major minor patch ++ ['-'] ++ pre ++ ['+'] ++ build)) + +/-! ## Values -/ + +/-- A natural number in decimal, as Lean's `Nat.repr` writes it: no + leading zero, and `0` for zero. -/ +def Spec.decimal (n : Nat) : List Char := Nat.toDigits 10 n + +example : Spec.decimal 0 = ['0'] := by decide +example : Spec.decimal 7 = ['7'] := by decide +example : Spec.decimal 1985 = "1985".toList := by decide + +/-- A pre-release identifier as written. -/ +def Spec.identChars : Ident → List Char + | .num n => Spec.decimal n + | .alnum s => s.toList + +/-- The string a version stands for: the three numbers, the pre-release + identifiers after `-` and the build identifiers after `+`, each list + joined by `.` and left out with its sign when it is empty. -/ +def Spec.render (v : Version) : List Char := + Spec.core (Spec.decimal v.major) (Spec.decimal v.minor) (Spec.decimal v.patch) ++ + (if v.pre = [] then [] else ['-'] ++ ['.'].intercalate (v.pre.map Spec.identChars)) ++ + (if v.build = [] then [] else ['+'] ++ ['.'].intercalate (v.build.map String.toList)) + +example : Spec.render ⟨1, 0, 0, [.alnum "alpha", .num 1], []⟩ = "1.0.0-alpha.1".toList := by + decide +example : Spec.render ⟨1, 0, 0, [.alnum "beta"], ["exp", "sha", "5114f85"]⟩ = + "1.0.0-beta+exp.sha.5114f85".toList := by decide +example : Spec.render ⟨1, 0, 0, [], ["20130313144700"]⟩ = "1.0.0+20130313144700".toList := by + decide + +/-- A pre-release identifier is well formed when, as a number, it is any + natural number, and otherwise when it is an alphanumeric identifier. + An `alnum` of digits only is not well formed: those digits are a + numeric identifier. -/ +def Spec.ValidIdent : Ident → Prop + | .num _ => True + | .alnum s => Spec.AlnumIdent s.toList + +/-- A version is well formed when each of its identifiers is. The three + numbers may be any natural numbers: SemVer sets no upper limit. -/ +def Spec.Valid (v : Version) : Prop := + (∀ i ∈ v.pre, Spec.ValidIdent i) ∧ ∀ b ∈ v.build, Spec.BuildIdent b.toList + +/-! ## Precedence: section 11 + +``` +1. Precedence MUST be calculated by separating the version into major, + minor, patch and pre-release identifiers in that order (Build + metadata does not figure into precedence). +2. Precedence is determined by the first difference when comparing + each of these identifiers from left to right as follows: Major, + minor, and patch versions are always compared numerically. +3. When major, minor, and patch are equal, a pre-release version has + lower precedence than a normal version. +4. Precedence for two pre-release versions with the same major, minor, + and patch version MUST be determined by comparing each dot separated + identifier from left to right until a difference is found as + follows: + 1. Identifiers consisting of only digits are compared numerically. + 2. Identifiers with letters or hyphens are compared lexically in + ASCII sort order. + 3. Numeric identifiers always have lower precedence than + non-numeric identifiers. + 4. A larger set of pre-release fields has a higher precedence than + a smaller set, if all of the preceding identifiers are equal. +``` +-/ + +/-- Two numbers, compared numerically (11.2 and 11.4.1). -/ +def Spec.numOrder (a b : Nat) : Ordering := + if a < b then .lt else if b < a then .gt else .eq + +/-- ASCII sort order (11.4.2): by the code of the first character that + differs; when one string runs out first, it comes first. -/ +def Spec.asciiOrder : List Char → List Char → Ordering + | [], [] => .eq + | [], _ :: _ => .lt + | _ :: _, [] => .gt + | a :: as, b :: bs => + if a.toNat < b.toNat then .lt else if b.toNat < a.toNat then .gt else Spec.asciiOrder as bs + +example : Spec.asciiOrder "alpha".toList "beta".toList = .lt := by decide +example : Spec.asciiOrder "Z".toList "a".toList = .lt := by decide +example : Spec.asciiOrder "-".toList "0a".toList = .lt := by decide +example : Spec.asciiOrder "rc".toList "rc1".toList = .lt := by decide + +/-- Two pre-release identifiers: 11.4.1 to 11.4.3. -/ +def Spec.identOrder : Ident → Ident → Ordering + | .num a, .num b => Spec.numOrder a b + | .alnum a, .alnum b => Spec.asciiOrder a.toList b.toList + | .num _, .alnum _ => .lt + | .alnum _, .num _ => .gt + +/-- Two lists of pre-release identifiers, from left to right until a + difference is found (11.4); when one list runs out first, all of its + identifiers being equal to the other's, it comes first (11.4.4). -/ +def Spec.preOrder : List Ident → List Ident → Ordering + | [], [] => .eq + | [], _ :: _ => .lt + | _ :: _, [] => .gt + | a :: as, b :: bs => + match Spec.identOrder a b with + | .eq => Spec.preOrder as bs + | o => o + +/-- The precedence of `a` against `b`: `.lt` when `a` has lower + precedence. Major, minor and patch first (11.2), then a version + without a pre-release part above one with it (11.3), then the + pre-release identifiers (11.4). Build identifiers are not read + (11.1). -/ +def Spec.precedence (a b : Version) : Ordering := + if a.major ≠ b.major then Spec.numOrder a.major b.major + else if a.minor ≠ b.minor then Spec.numOrder a.minor b.minor + else if a.patch ≠ b.patch then Spec.numOrder a.patch b.patch + else if a.pre = [] ∧ b.pre = [] then .eq + else if a.pre = [] then .gt + else if b.pre = [] then .lt + else Spec.preOrder a.pre b.pre + +/-! ## Helpers for the test vectors -/ + +/-- The precedence of two strings, when both parse. -/ +def Spec.compareStrings (s t : String) : Option Ordering := do + let a ← parse s + let b ← parse t + pure (a.compare b) diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..77cf39d --- /dev/null +++ b/bar.toml @@ -0,0 +1,32 @@ +# Read by bar/check.py in Proven-Commons/mission. +# See playbook/verified-bar.md there for what each field means. + +[project] +name = "semver" +# "in-progress" until every bar item passes, then "verified". +status = "in-progress" +page = "README.md" +# GitHub handles of everyone who wrote the specification. It was drafted +# by Claude, an AI agent, for the org, from the fdn-0 account. +spec_authors = ["claude", "fdn-0"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +# SemVer/Types.lean holds the types every statement is about, so it is +# part of the specification. +files = ["SPEC.md", "Spec.lean", "Spec/Defs.lean", "SemVer/Types.lean"] +# The code under proof: the functions the statements are about. +code = ["SemVer.parse", "SemVer.Version.print", "SemVer.Version.compare"] + +# One entry per approval, added in a pull request the reviewer approves. +# [[spec.approval]] +# reviewer = "github-handle" +# date = "2026-11-02" +# sha256 = "..." +# record = "https://github.com/Proven-Commons/semver/pull/" + +[tests] +results = "tests/TEST-RESULTS.md" +command = "python3 tests/run_tests.py" +files = ["tests/run_tests.py", "tests/oracle-requirements.txt"] diff --git a/comparator.json b/comparator.json new file mode 100644 index 0000000..b2c2048 --- /dev/null +++ b/comparator.json @@ -0,0 +1,12 @@ +{ + "challenge_module": "Spec", + "solution_module": "Proofs", + "theorem_names": [ + "Spec.print_eq", "Spec.parse_iff", "Spec.parse_isSome_iff", "Spec.parse_valid", + "Spec.parse_print", "Spec.print_parse", "Spec.compare_eq", "Spec.compare_build", + "Spec.compare_eq_eq_iff", "Spec.compare_swap", "Spec.compare_trans", "Spec.compare_lt_trans", + "Spec.semver_examples", "Spec.precedence_examples", "Spec.reject_vectors", + "Spec.accept_vectors" + ], + "permitted_axioms": ["propext", "Quot.sound", "Classical.choice"] +} 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..52eb2e9 --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,16 @@ +name = "semver" +version = "0.1.0" +defaultTargets = ["SemVer", "Spec", "Proofs", "semver"] + +[[lean_lib]] +name = "SemVer" + +[[lean_lib]] +name = "Spec" + +[[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..d102248 --- /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: python-semver 3.1.0 on Python 3.13.17, with the semver.org FAQ regular expression as a second check on acceptance +- Lean: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) +- Seed: 20261025 +- Inputs: 3021721 +- Mutated: 449861 of the inputs are mutated versions +- By kind: compare 150022, compare pool 6084, error 13, examples 85, grid 2015539, mutated 449861, random 100539, valid 299578 +- Strings parsed: 2865602, of which 442325 accepted and 2423277 rejected +- Accepted versions with a number of 2**64 or more: 72009 +- Pairs compared: 156106: < 66963, = 27956, > 61187, REJECT 0 +- Malformed requests answered `error`: 13 of 13 +- Requests ending in CR LF: every seventh, 431674 +- Last lines sent alone, with no LF or with CR LF, answered right: 3 of 3 +- Failures: 0 diff --git a/tests/oracle-requirements.txt b/tests/oracle-requirements.txt new file mode 100644 index 0000000..a2ad78d --- /dev/null +++ b/tests/oracle-requirements.txt @@ -0,0 +1,5 @@ +# The oracle for tests/run_tests.py, pinned by hash. The hashes are the +# ones PyPI publishes for semver 3.1.0. +semver==3.1.0 \ + --hash=sha256:6e4998f8b4762acdfea85f9bfd5b4032e0bb50038dc04bf82011b42d5d1145c5 \ + --hash=sha256:14bc073439513d7773662a338f4db9829cf16c12b74b9568e2d2689975fbd7fc diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..68c780a --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,556 @@ +#!/usr/bin/env python3 +"""Differential tests: the Lean SemVer parser and precedence against +python-semver. + +The oracle is python-semver 3.1.0 (https://pypi.org/project/semver/): +`semver.Version.parse`, which raises on any string outside the +SemVer 2.0.0 grammar, and `Version.compare`, which gives section 11 +precedence. Every accepted string must also match, in full, the +regular expression semver.org gives in its FAQ, compiled with +`re.ASCII`; a string where the two oracles disagree is a failure too. + +For `parse`, the expected answer is python-semver's version: its +printed form, its three numbers, its pre-release identifiers, each +tagged as a number (digits only) or not, and its build identifiers. +For `compare`, it is python-semver's answer, or REJECT when either +string is not a version. + +Inputs come from a recorded seed, after fixed sets: + +- every string of up to eight characters over `0`, `1`, `.`, `-`, + `+` and `a`, which reaches every arrangement of parts and + separators with short parts; +- the examples of sections 9 to 11 of the specification, and strings + outside the grammar that loose parsers accept; +- random versions with numbers up to 2**200, pre-release identifiers + that are numbers, letters, hyphens and mixtures (`0a`, `--`), and + build identifiers with leading zeros; +- mutations of those: a character changed, dropped, added or + doubled, a leading zero put in front of a number, the string cut + short, a prefix such as `v` or a space or line break around it, + and digits from other scripts put in; +- random short strings; +- comparisons: every pair from a pool of versions built to differ in + one place at a time, and random pairs of random versions; +- malformed requests, which the tool must answer with `error`. + +Every seventh request ends in CR LF. + +When this Python lacks python-semver 3.1.0, the script creates a +virtual environment in `.lake/oracle-venv`, installs it there, checked +against the hashes in `tests/oracle-requirements.txt`, and runs itself +again with it. + + python3 tests/run_tests.py [--seed N] [--count N] + +`--count` is the number of random inputs after the fixed sets. The +script builds the executable first, writes tests/TEST-RESULTS.md, and +exits non-zero if any input disagrees. +""" + +import argparse +import itertools +import os +import platform +import random +import re +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" +REQUIREMENTS = ROOT / "tests" / "oracle-requirements.txt" +VENV = ROOT / ".lake" / "oracle-venv" +PKGS = ROOT / ".lake" / "oracle-packages" +PIN = "3.1.0" +TIMEOUT = 1800 +BUILD_TIMEOUT = 3600 + + +def oracle_ready(): + """Whether the pinned python-semver imports.""" + try: + import semver + except ImportError: + return False + return semver.__version__ == PIN + + +def ensure_oracle(): + """Import the oracle. When this Python lacks the pinned version, + install it, checked against the hashes in + tests/oracle-requirements.txt, into a virtual environment and run + again with it; where a virtual environment cannot be made, install + it into a folder instead and import it from there.""" + if oracle_ready(): + return + if os.environ.get("SEMVER_ORACLE_VENV"): + sys.exit(f"python-semver {PIN} is not usable even in .lake/oracle-venv") + pip = ["-m", "pip", "install", "--quiet", "--require-hashes", "-r", str(REQUIREMENTS)] + python = VENV / "bin" / "python" + made = python.exists() or subprocess.run( + [sys.executable, "-m", "venv", str(VENV)], capture_output=True).returncode == 0 + if made: + subprocess.run([str(python), *pip], check=True) + env = dict(os.environ, SEMVER_ORACLE_VENV="1") + os.execve(str(python), [str(python), *sys.argv], env) + subprocess.run([sys.executable, *pip, "--break-system-packages", "--target", str(PKGS)], + check=True) + sys.path.insert(0, str(PKGS)) + sys.modules.pop("semver", None) + if not oracle_ready(): + sys.exit(f"python-semver {PIN} is not usable") + + +ensure_oracle() +import semver # noqa: E402 + +# The regular expression of the semver.org FAQ, "Is there a suggested +# regular expression (RegEx) to check a SemVer string?", as written +# there. `re.ASCII` keeps `\d` to ASCII digits, and `fullmatch` keeps +# `$` from matching before a final line break. +SEMVER_ORG_REGEX = re.compile( + r"^(0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)" + r"(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?" + r"(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?$", + re.ASCII, +) + + +def oracle_version(s): + """python-semver's reading of `s`, or None. Raises when the two + oracles disagree.""" + try: + v = semver.Version.parse(s) + except (ValueError, TypeError): + v = None + if (v is not None) != (SEMVER_ORG_REGEX.fullmatch(s) is not None): + raise OracleDisagree(s) + return v + + +class OracleDisagree(Exception): + pass + + +def ident_field(x): + return f"n:{int(x)}" if x.isascii() and x.isdigit() else f"a:{x}" + + +def oracle_parse(s): + v = oracle_version(s) + if v is None: + return "REJECT" + pre = ",".join(ident_field(x) for x in v.prerelease.split(".")) if v.prerelease else "" + build = ",".join(v.build.split(".")) if v.build else "" + return "\t".join(["OK", str(v), str(v.major), str(v.minor), str(v.patch), pre, build]) + + +def oracle_compare(a, b): + va, vb = oracle_version(a), oracle_version(b) + if va is None or vb is None: + return "REJECT" + return {-1: "<", 0: "=", 1: ">"}[va.compare(vb)] + + +# The fixed sets. + +GRID_ALPHABET = "01.-+a" +GRID_LENGTH = 8 + + +def grid(): + for n in range(GRID_LENGTH + 1): + for t in itertools.product(GRID_ALPHABET, repeat=n): + yield "".join(t) + + +EXAMPLES = [ + # Sections 9 and 10. + "1.0.0-alpha", "1.0.0-alpha.1", "1.0.0-0.3.7", "1.0.0-x.7.z.92", "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+21AF26D3----117B344092BD", + # Section 11. + "1.0.0", "2.0.0", "2.1.0", "2.1.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", + # Inside the grammar, often got wrong. + "0.0.0", "0.0.0-0", "1.0.0-0a", "1.0.0-00a", "1.0.0--", "1.0.0---", "1.0.0-a-+b-", + "1.0.0+001", "1.0.0+0", "1.0.0+-", "1.0.0-0.0.0", "1.0.0-alpha.0valid", + "1.0.0-alpha-a.b-c-somethinglong+build.1-aef.1-its-okay", "1.0.0-rc.1+build.123", + "10.20.30", "99999999999999999999999.999999999999999999.99999999999999999", + "18446744073709551616.0.0", "1.2.3----RC-SNAPSHOT.12.9.1--.12+788", + "1.2.3----R-S.12.9.1--.12+meta", "1.0.0-0A.is.legal", "2.0.0+build.1848", + # Outside the grammar. + "", "1", "1.2", "1.2.3.4", "01.1.1", "1.01.1", "1.1.01", "1.2.3-01", "1.2.3-0123", + "1.2.3-0123.0123", "1.2.3-", "1.2.3+", "1.2.3-+", "1.2.3-+123", "1.2-SNAPSHOT", + "1.2.31.2.3----RC-SNAPSHOT.12.09.1--..12+788", "-1.0.3-gamma+b7718", "+justmeta", + "9.8.7+meta+meta", "9.8.7-whatever+meta+meta", "1.2.3.DEV", "1.2.3-alpha..1", + "1.2.3-alpha.", "1.2.3+build..1", "1.2.3-alpha_beta", "1.2.3-alpha.é", "v1.2.3", + "=1.2.3", " 1.2.3", "1.2.3 ", "1.2.3\n", "\n1.2.3", "1.2.3\t", "1٣.2.3", + "1.2.3-١", "１.2.3", "1.2.3-a ", "1.2.3+٣", "1.2.3-K", + "1.2.3-İ", "1.2.3\x00", "1..2.3", ".1.2.3", "1.2.3.", "a.b.c", "1.2.3-α", +] + +ASCII_PRINTABLE = [chr(c) for c in range(32, 127)] +OTHER_CHARS = ["٣", "０", "１", "०", "é", "K", "İ", + " ", "\t", "\n", "\r", "\x00", "‐", "−", "﹣", "．"] + + +def random_number(rng): + r = rng.random() + if r < 0.3: + return rng.randint(0, 9) + if r < 0.6: + return rng.randint(10, 999) + if r < 0.8: + return rng.randint(1000, 2 ** 32) + if r < 0.95: + return rng.randint(2 ** 63 - 2, 2 ** 64 + 2) + return rng.randint(0, 2 ** 200) + + +def random_ident_text(rng, alphabet, n): + return "".join(rng.choice(alphabet) for _ in range(n)) + + +ALNUM = "0123456789abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ-" + + +def random_pre_ident(rng): + r = rng.random() + if r < 0.4: + return str(random_number(rng)) + if r < 0.5: + return rng.choice(["alpha", "beta", "rc", "pre", "SNAPSHOT", "-", "--", "0a", "a0"]) + while True: + s = random_ident_text(rng, ALNUM, rng.randint(1, 8)) + if not s.isdigit(): + return s + + +def random_build_ident(rng): + r = rng.random() + if r < 0.3: + return "".join(rng.choice("0123456789") for _ in range(rng.randint(1, 6))) + return random_ident_text(rng, ALNUM, rng.randint(1, 8)) + + +def random_version(rng): + s = ".".join(str(random_number(rng)) for _ in range(3)) + if rng.random() < 0.6: + s += "-" + ".".join(random_pre_ident(rng) for _ in range(rng.randint(1, 4))) + if rng.random() < 0.4: + s += "+" + ".".join(random_build_ident(rng) for _ in range(rng.randint(1, 3))) + return s + + +def mutate(rng, s): + cs = list(s) + op = rng.randrange(10) + if op == 0 and cs: + cs[rng.randrange(len(cs))] = rng.choice(ASCII_PRINTABLE + list("0.-+")) + elif op == 1 and cs: + del cs[rng.randrange(len(cs))] + elif op == 2: + cs.insert(rng.randint(0, len(cs)), rng.choice(list("0123456789.-+aZ") + ASCII_PRINTABLE)) + elif op == 3 and cs: + i = rng.randrange(len(cs)) + cs.insert(i, cs[i]) + elif op == 4: + # A leading zero in front of a number or an identifier. + starts = [i for i in range(len(cs)) if i == 0 or cs[i - 1] in ".-+"] + cs.insert(rng.choice(starts) if starts else 0, "0") + elif op == 5 and cs: + cs = cs[: rng.randrange(len(cs))] + elif op == 6: + cs = list(rng.choice(["v", "V", "=", " ", "\n", "\t", "~", "^"])) + cs + elif op == 7: + cs += list(rng.choice([" ", "\n", "\r\n", "\t", ".", "-", "+", "\x00"])) + elif op == 8 and cs: + cs[rng.randrange(len(cs))] = rng.choice(OTHER_CHARS) + else: + cs.insert(rng.randint(0, len(cs)), rng.choice(OTHER_CHARS)) + return "".join(cs) + + +def compare_pool(): + """Versions built to differ from each other in one place at a time: + each number, the presence of a pre-release part, each identifier's + kind and value, the number of identifiers, and build metadata.""" + cores = ["0.0.0", "0.0.1", "0.1.0", "1.0.0", "1.0.1", "1.1.0", "2.0.0", "10.0.0", + "1.10.0", "1.2.10", "18446744073709551616.0.0"] + pres = ["", "-0", "-1", "-2", "-10", "-11", "-a", "-b", "-A", "-Z", "-z", "-0a", "-1a", "--", + "-a-", "-alpha", "-alpha.1", "-alpha.beta", "-alpha.1.1", "-alpha.0", "-alpha.a", + "-beta", "-beta.2", "-beta.11", "-rc.1", "-1.a", "-a.1", "-18446744073709551616"] + builds = ["", "+b", "+001"] + pool = [] + for c in ["1.0.0", "1.0.1"]: + for p in pres: + pool.append(c + p) + for c in cores: + pool.append(c) + pool.append(c + "-alpha") + for b in builds: + pool.append("1.0.0-alpha" + b) + pool.append("1.0.0" + b) + return list(dict.fromkeys(pool)) + + +def hexs(s): + return s.encode("utf-8").hex() + + +MALFORMED = [ + ("frob 30", "unknown operation"), + ("PARSE 30", "operations are lower case"), + ("parse", "no argument"), + ("parse 3", "an odd number of hex digits"), + ("parse 3G", "not a hex digit"), + ("parse 3A", "hex digits are lower case"), + ("parse ff", "bytes that are not UTF-8"), + ("parse 30 30", "two arguments"), + ("compare 30", "one argument"), + ("compare 30 30 30", "three arguments"), + ("compare 3 30", "an odd number of hex digits"), + ("", "an empty line"), + (" parse 30", "a leading space"), +] + +AT_EOF = [ + ("parse " + hexs("1.2.3"), oracle_parse("1.2.3")), + ("compare " + hexs("1.0.0") + " " + hexs("2.0.0"), "<"), + ("parse " + hexs("1.2.3") + "\r\n", oracle_parse("1.2.3")), +] + + +def parse_case(label, s, mutated=False): + return (label, f"parse {hexs(s)}", oracle_parse(s), mutated) + + +def cases(seed, count): + """(label, request, expected answer, mutated) for each input.""" + for req, _ in MALFORMED: + yield ("error", req, "error", False) + for s in EXAMPLES: + yield parse_case("examples", s) + for s in grid(): + yield parse_case("grid", s) + pool = compare_pool() + for a in pool: + for b in pool: + yield ("compare pool", f"compare {hexs(a)} {hexs(b)}", oracle_compare(a, b), False) + rng = random.Random(seed) + for _ in range(count): + r = rng.random() + if r < 0.3: + yield parse_case("valid", random_version(rng)) + elif r < 0.75: + base = random_version(rng) + s = mutate(rng, base) + while s == base: + s = mutate(rng, base) + yield parse_case("mutated", s, True) + elif r < 0.85: + n = rng.randint(0, 12) + yield parse_case("random", "".join(rng.choice("0123456789.-+aZ" + "".join(OTHER_CHARS[:3])) + for _ in range(n))) + else: + a = random_version(rng) + b = random_version(rng) if rng.random() < 0.5 else mutate_compare(rng, a) + yield ("compare", f"compare {hexs(a)} {hexs(b)}", oracle_compare(a, b), False) + + +def mutate_compare(rng, a): + """A version near `a`: one identifier or number changed, or only the + build metadata.""" + v = semver.Version.parse(a) + op = rng.randrange(4) + if op == 0: + return str(v.replace(build=random_build_ident(rng))) + if op == 1: + return str(v.replace(patch=v.patch + rng.choice([0, 1]))) + if op == 2 and v.prerelease: + parts = v.prerelease.split(".") + parts[rng.randrange(len(parts))] = random_pre_ident(rng) + return str(v.replace(prerelease=".".join(parts))) + parts = v.prerelease.split(".") if v.prerelease else [] + parts.append(random_pre_ident(rng)) + return str(v.replace(prerelease=".".join(parts))) + + +def run_tool(data, timeout=TIMEOUT): + """The tool's answer lines for `data`, and a note on how the run + failed, or None.""" + raw = data.encode("utf-8") + limit = 4 * len(raw) + 256 * (data.count("\n") + 1) + try: + proc = subprocess.Popen([str(EXE), "serve"], stdin=subprocess.PIPE, + stdout=subprocess.PIPE, stderr=subprocess.PIPE) + except OSError as e: + return [], f"could not run {EXE.relative_to(ROOT)}: {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(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" + lines = text.split("\n") + if lines and lines[-1] == "": + lines.pop() + return lines, problem + + +def oracle(): + return (f"python-semver {semver.__version__} on Python {platform.python_version()}, " + "with the semver.org FAQ regular expression as a second check on acceptance") + + +def lean_version(): + try: + out = subprocess.run(["lake", "env", "lean", "--version"], cwd=ROOT, + capture_output=True, text=True, errors="backslashreplace", + timeout=300) + first = out.stdout.strip().splitlines()[:1] + return first[0] if first else "unknown" + except (OSError, subprocess.TimeoutExpired): + return "unknown" + + +def count(text): + n = int(text) + if n < 1: + raise argparse.ArgumentTypeError("the count must be at least 1") + return n + + +def write(lines): + RESULTS.write_text("\n".join(lines), encoding="utf-8") + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--seed", type=int, default=20261025) + ap.add_argument("--count", type=count, default=1_000_000) + args = ap.parse_args() + + try: + build = subprocess.run(["lake", "build", "semver"], cwd=ROOT, capture_output=True, + text=True, errors="backslashreplace", timeout=BUILD_TIMEOUT) + built, log = build.returncode == 0, build.stdout + build.stderr + except (OSError, subprocess.TimeoutExpired) as e: + built, log = False, str(e) + if not built: + write(["# Test results", "", f"- Oracle: {oracle()}", f"- Seed: {args.seed}", + "- Inputs: 0", "- Failures: 1 (`lake build semver` failed)", ""]) + sys.exit("lake build semver failed:\n" + log) + + try: + items = list(cases(args.seed, args.count)) + except OracleDisagree as e: + write(["# Test results", "", f"- Oracle: {oracle()}", f"- Seed: {args.seed}", + "- Inputs: 0", + f"- Failures: 1 (python-semver and the semver.org regex disagree on {e.args[0]!r})", + ""]) + sys.exit(f"the two oracles disagree on {e.args[0]!r}") + # Every seventh request ends in CR LF, which the tool must take as LF. + out, problem = run_tool("".join(req + ("\r\n" if i % 7 == 6 else "\n") + for i, (_, req, _, _) in enumerate(items))) + failures = [("(whole run)", "a clean run", problem)] if problem else [] + for item, got in itertools.zip_longest(items, out): + if item is None: + failures.append(("(no request)", "nothing", got)) + elif got != item[2]: + failures.append((item[1], item[2], "(no answer)" if got is None else got)) + eof_right = 0 + for req, want in AT_EOF: + got, problem = run_tool(req, timeout=60) + if got == [want] and not problem: + eof_right += 1 + else: + failures.append((req + " (at end of input)", want, f"{got} {problem or ''}".strip())) + + by_label = {} + for label, _, _, _ in items: + by_label[label] = by_label.get(label, 0) + 1 + parses = [want for label, req, want, _ in items if req.startswith("parse ") + and label != "error"] + accepted = sum(1 for w in parses if w.startswith("OK")) + compares = [want for label, req, want, _ in items if req.startswith("compare ") + and label != "error"] + mutated = sum(1 for item in items if item[3]) + malformed = [got for item, got in zip(items, out) if item[0] == "error"] + big = sum(1 for w in parses if w.startswith("OK") and + any(int(x) >= 2 ** 64 for x in w.split("\t")[2:5])) + + lines = [ + "# Test results", + "", + "Written by `tests/run_tests.py`. Rerun it to check these numbers.", + "", + f"- Oracle: {oracle()}", + f"- Lean: {lean_version()}", + f"- Seed: {args.seed}", + f"- Inputs: {len(items)}", + f"- Mutated: {mutated} of the inputs are mutated versions", + "- By kind: " + ", ".join(f"{k} {v}" for k, v in sorted(by_label.items())), + f"- Strings parsed: {len(parses)}, of which {accepted} accepted and " + f"{len(parses) - accepted} rejected", + f"- Accepted versions with a number of 2**64 or more: {big}", + f"- Pairs compared: {len(compares)}: " + + ", ".join(f"{k} {compares.count(k)}" for k in ["<", "=", ">", "REJECT"]), + f"- Malformed requests answered `error`: {malformed.count('error')} of " + f"{by_label.get('error', 0)}", + f"- Requests ending in CR LF: every seventh, {len(items) // 7}", + f"- Last lines sent alone, with no LF or with CR LF, answered right: {eof_right} of " + f"{len(AT_EOF)}", + f"- Failures: {len(failures)}", + "", + ] + if failures: + lines += ["## Failures", ""] + lines += [f"- `{req[:160]!r}`: expected `{want[:120]!r}`, got `{got[:120]!r}`" + for req, want, got in failures[:50]] + lines.append("") + write(lines) + agree = sum(1 for item, got in zip(items, out) if got == item[2]) + print(f"{agree}/{len(items)} requests agree, {len(failures)} failures; results in {RESULTS}") + return 1 if failures else 0 + + +if __name__ == "__main__": + sys.exit(main())