From 9f65d441461c5d0ec2731917840007edfee0a92f Mon Sep 17 00:00:00 2001 From: shah Date: Tue, 27 Oct 2026 01:30:18 -0500 Subject: [PATCH 1/2] Add XML safe subset parser and printer, with proved round trip --- .gitignore | 1 + Main.lean | 87 +++ Proofs.lean | 1 + Proofs/RoundTrip.lean | 1636 +++++++++++++++++++++++++++++++++++++++++ README.md | 72 +- SPEC.md | 224 ++++++ Xml.lean | 2 + Xml/Parse.lean | 423 +++++++++++ Xml/Value.lean | 271 +++++++ lake-manifest.json | 6 + lakefile.toml | 13 + lean-toolchain | 1 + tests/TEST-RESULTS.md | 20 + tests/run_tests.py | 745 +++++++++++++++++++ 14 files changed, 3484 insertions(+), 18 deletions(-) create mode 100644 Main.lean create mode 100644 Proofs.lean create mode 100644 Proofs/RoundTrip.lean create mode 100644 SPEC.md create mode 100644 Xml.lean create mode 100644 Xml/Parse.lean create mode 100644 Xml/Value.lean create mode 100644 lake-manifest.json create mode 100644 lakefile.toml create mode 100644 lean-toolchain create mode 100644 tests/TEST-RESULTS.md create mode 100644 tests/run_tests.py diff --git a/.gitignore b/.gitignore index 01f8cdb..ae73679 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ .lake/ +__pycache__/ diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..d8bfd04 --- /dev/null +++ b/Main.lean @@ -0,0 +1,87 @@ +/- + Command line front end, used by the tests. + + Reads one request per line and prints one answer per line. A + request is an operation and its input as comma-separated decimal + character codes. + + parse 60,97,62,120,60,47,97,62 prints ok:60,97,62,120,60,47,97,62 + parse 60,97,47,62 prints ok:60,97,47,62 + parse 120 prints none + + The one operation is `parse`. Its input is the character codes of + an XML text in the safe subset. Its answer is `ok:` and the + character codes of the canonical print of the parsed document, + or `none` when the text is rejected. + + A request is an operation, then optionally one space and its + numbers; with no numbers after the space, the input is empty. A + malformed request prints `error`: any other line, an unknown + operation, a number that is not plain decimal digits, or a + character code that is not a Unicode scalar value. A line may end + in LF or CR LF; nothing else around a request is ignored. + + The parsing and printing here call `Xml.parse` and `Xml.print` + directly. The line handling is covered by the tests, not by a + proof. +-/ + +import Xml + +open Xml + +/-- A number in plain decimal digits. Longer numbers than any + character code are refused before they are converted, since + that takes time quadratic in their length. -/ +def number (t : String) : Option Nat := + let ds := t.toList + if ds.isEmpty || !ds.all Char.isDigit || (ds.dropWhile (· = '0')).length > 7 then none + else t.toNat? + +/-- The comma-separated numbers in `s`. -/ +def numbers (s : String) : Option (List Nat) := + if s.isEmpty then some [] else (s.splitOn ",").mapM number + +def toChars (ns : List Nat) : Option (List Char) := + ns.mapM fun n => if n.isValidChar then some (Char.ofNat n) else none + +def showCodes (cs : List Char) : String := + ",".intercalate (cs.map fun c => toString c.toNat) + +/-- The answer to one request, or `none` when the request is + malformed. -/ +def answer (op : String) (ns : List Nat) : Option String := + match op with + | "parse" => + match toChars ns with + | none => none + | some cs => + match parse cs with + | some d => some ("ok:" ++ showCodes (print d)) + | none => some "none" + | _ => none + +/-- The answer to one line: an operation, then optionally one space + and its numbers. -/ +def request (line : String) : Option String := + match line.splitOn " " with + | [op] => answer op [] + | [op, arg] => numbers arg >>= answer op + | _ => none + +/-- The line without its line ending: LF, or CR LF. -/ +def chomp (line : String) : String := + let cs := line.toList + if cs.getLast? = some '\n' then + let cs := cs.dropLast + String.ofList (if cs.getLast? = some '\r' then cs.dropLast else cs) + else line + +def main : IO Unit := do + let stdin ← IO.getStdin + let stdout ← IO.getStdout + repeat + let line ← stdin.getLine + if line.isEmpty then break + let line := chomp line + stdout.putStrLn ((request line).getD "error") diff --git a/Proofs.lean b/Proofs.lean new file mode 100644 index 0000000..1a31d95 --- /dev/null +++ b/Proofs.lean @@ -0,0 +1 @@ +import Proofs.RoundTrip diff --git a/Proofs/RoundTrip.lean b/Proofs/RoundTrip.lean new file mode 100644 index 0000000..377c90b --- /dev/null +++ b/Proofs/RoundTrip.lean @@ -0,0 +1,1636 @@ +/- + The round trip proof: for every well formed document, parsing + its printed form gives the document back. + + The statement proved here is `parse_print`. A matching statement + in a spec file still has to be added by a reviewer, so this file + builds on its own, in the same shape as the proofs of the other + slices. + + The proof goes layer by layer: references, text runs, attribute + values, character data, names, comment bodies, processing + instruction data, attributes, then elements and content together + by a strong induction on the length of the printed form, then + the prolog and epilog lists, and at last the document. +-/ + +import Xml + +namespace Xml.Proofs + +open Xml + +set_option maxRecDepth 10000 + +/-! ## Small facts -/ + +theorem isWs_of_ne {c : Char} (h1 : c ≠ ' ') (h2 : c ≠ '\t') + (h3 : c ≠ '\n') (h4 : c ≠ '\r') : isWs c = false := by + simp [isWs, h1, h2, h3, h4] + +theorem isWs_lt : isWs '<' = false := by decide +theorem isWs_slash : isWs '/' = false := by decide + +/-- Skipping whitespace over a list whose head is not whitespace + changes nothing. -/ +theorem skipWs_cons {c : Char} {cs : List Char} (h : isWs c = false) : + skipWs (c :: cs) = c :: cs := by + simp [skipWs, h] + +theorem isLegalChar_of {c : Char} (h : LegalChar c) : isLegalChar c = true := + isLegalChar_iff.mpr h + +theorem isNameStart_of {c : Char} (h : IsNameStart c) : isNameStart c = true := + isNameStart_iff.mpr h + +theorem isNameChar_of {c : Char} (h : IsNameChar c) : isNameChar c = true := + isNameChar_iff.mpr h + +theorem isNameChar_false_of {c : Char} (h : ¬ IsNameChar c) : + isNameChar c = false := by + cases hb : isNameChar c with + | true => exact absurd (isNameChar_iff.mp hb) h + | false => rfl + +/-- A name start character is a name character. -/ +theorem IsNameStart.toNameChar {c : Char} (h : IsNameStart c) : + IsNameChar c := + Or.inl h + +/-- A name start character differs from any character that fails + the name start test. -/ +theorem IsNameStart.ne_of_test {c d : Char} (h : IsNameStart c) + (hd : isNameStart d = false) : c ≠ d := by + intro e + subst e + have hb : isNameStart c = true := isNameStart_of h + rw [hb] at hd + exact Bool.false_ne_true hd.symm + +/-- A name start character is none of the marks that can follow a + name in a printed tag. -/ +theorem IsNameStart.ne_lt {c : Char} (h : IsNameStart c) : c ≠ '<' := + IsNameStart.ne_of_test h (by decide) + +theorem IsNameStart.ne_bang {c : Char} (h : IsNameStart c) : c ≠ '!' := + IsNameStart.ne_of_test h (by decide) + +theorem IsNameStart.ne_ws {c : Char} (h : IsNameStart c) : ¬ IsWs c := by + intro hw + rcases hw with e | e | e | e + · exact IsNameStart.ne_of_test h (by decide) e + · exact IsNameStart.ne_of_test h (by decide) e + · exact IsNameStart.ne_of_test h (by decide) e + · exact IsNameStart.ne_of_test h (by decide) e + +/-- A character that fails the name character test is not a name + character. -/ +theorem not_nameChar_of_test {c : Char} (h : isNameChar c = false) : + ¬ IsNameChar c := by + intro hc + have hb := isNameChar_iff.mpr hc + rw [h] at hb + exact Bool.false_ne_true hb + +/-- The marks that follow a name in a printed tag are not name + characters. -/ +theorem not_nameChar_slash : ¬ IsNameChar '/' := + not_nameChar_of_test (by decide) +theorem not_nameChar_gt : ¬ IsNameChar '>' := + not_nameChar_of_test (by decide) +theorem not_nameChar_eq : ¬ IsNameChar '=' := + not_nameChar_of_test (by decide) +theorem not_nameChar_quest : ¬ IsNameChar '?' := + not_nameChar_of_test (by decide) +theorem not_nameChar_space : ¬ IsNameChar ' ' := + not_nameChar_of_test (by decide) + +/-- The printed form of one character of character data: either + an escape, whose head is an ampersand, or the character + itself. -/ +theorem escapeTextChar_head (c : Char) : + (escapeTextChar c).head? = some '&' ∨ escapeTextChar c = [c] := by + unfold escapeTextChar + split + · simp + · split + · simp + · split + · simp + · split + · simp + · exact Or.inr rfl + +/-- An escaped character is never the empty list, and its head is + never a greater sign. The second fact is what keeps `]]>` from + ever forming in printed text: a greater sign only ever appears + inside `>`, behind an ampersand. -/ +theorem escapeTextChar_ne_nil (c : Char) : escapeTextChar c ≠ [] := by + intro he + rcases escapeTextChar_head c with h | h + · rw [he] at h + simp at h + · rw [he] at h + simp at h + +theorem escapeTextChar_head_ne_gt (c : Char) : + (escapeTextChar c).head? ≠ some '>' := by + rcases escapeTextChar_head c with h | h + · rw [h]; decide + · rw [h] + intro hcon + simp at hcon + subst hcon + have hgt : escapeTextChar '>' = ['&', 'g', 't', ';'] := by decide + rw [hgt] at h + simp at h + +/-- An escaped attribute character is never the empty list, and + its head is an ampersand when it is an escape. -/ +theorem escapeAttrChar_head (c : Char) : + (escapeAttrChar c).head? = some '&' ∨ escapeAttrChar c = [c] := by + unfold escapeAttrChar + split + · simp + · split + · simp + · split + · simp + · split + · simp + · split + · simp + · split + · simp + · exact Or.inr rfl + +theorem escapeAttrChar_ne_nil (c : Char) : escapeAttrChar c ≠ [] := by + intro he + rcases escapeAttrChar_head c with h | h + · rw [he] at h + simp at h + · rw [he] at h + simp at h + +/-- The head of a printed text run followed by more text: the + printed run of a nonempty list starts with the printed form of + its first character. -/ +theorem escapeText_head {c : Char} {cs : List Char} : + (escapeText (c :: cs)).head? = (escapeTextChar c).head? := by + have hne := escapeTextChar_ne_nil c + simp only [escapeText, List.flatMap_cons] + cases h : escapeTextChar c with + | nil => exact absurd h hne + | cons x xs => simp + +theorem escapeText_length_ge (cs : List Char) : + cs.length ≤ (escapeText cs).length := by + induction cs with + | nil => simp [escapeText] + | cons c cs ih => + have h1 : 1 ≤ (escapeTextChar c).length := by + cases h : escapeTextChar c with + | nil => exact absurd h (escapeTextChar_ne_nil c) + | cons x xs => simp + have hlen : (escapeText (c :: cs)).length = + (escapeTextChar c).length + (escapeText cs).length := by + have e1 : escapeText (c :: cs) = escapeTextChar c ++ escapeText cs := rfl + rw [e1, List.length_append] + rw [List.length_cons, hlen] + omega + +theorem escapeAttr_length_ge (cs : List Char) : + cs.length ≤ (escapeAttr cs).length := by + induction cs with + | nil => simp [escapeAttr] + | cons c cs ih => + have h1 : 1 ≤ (escapeAttrChar c).length := by + cases h : escapeAttrChar c with + | nil => exact absurd h (escapeAttrChar_ne_nil c) + | cons x xs => simp + have hlen : (escapeAttr (c :: cs)).length = + (escapeAttrChar c).length + (escapeAttr cs).length := by + have e1 : escapeAttr (c :: cs) = escapeAttrChar c ++ escapeAttr cs := rfl + rw [e1, List.length_append] + rw [List.length_cons, hlen] + omega + +/-! ## References -/ + +theorem parseRef_lt {rest : List Char} : + parseRef ('l' :: 't' :: ';' :: rest) = some ('<', rest) := rfl + +theorem parseRef_gt {rest : List Char} : + parseRef ('g' :: 't' :: ';' :: rest) = some ('>', rest) := rfl + +theorem parseRef_amp {rest : List Char} : + parseRef ('a' :: 'm' :: 'p' :: ';' :: rest) = some ('&', rest) := rfl + +theorem parseRef_quot {rest : List Char} : + parseRef ('q' :: 'u' :: 'o' :: 't' :: ';' :: rest) = some ('"', rest) := rfl + +/-- A run of digits at the head of a text is read whole: when the + text after the run does not start with a digit, the digit run + reader stops at the end of the run. -/ +theorem takeDigits_append {ds rest : List Char} + (hd : ∀ d ∈ ds, isDigit d = true) + (hr : ∀ c, rest.head? = some c → isDigit c = false) : + takeDigits (ds ++ rest) = (ds, rest) := by + induction ds generalizing rest with + | nil => + cases rest with + | nil => rfl + | cons c r => + have hc : isDigit c = false := hr c rfl + simp [takeDigits, hc] + | cons d ds ih => + have hdd : isDigit d = true := hd d (by simp) + have ih' := ih (fun x hx => hd x (List.mem_cons_of_mem d hx)) hr + simp [takeDigits, hdd, ih'] + +theorem parseRef_dec13 {rest : List Char} : + parseRef ('#' :: '1' :: '3' :: ';' :: rest) = some ('\r', rest) := by + have htake : takeDigits ('1' :: '3' :: ';' :: rest) = + (['1', '3'], ';' :: rest) := by + show takeDigits (['1', '3'] ++ (';' :: rest)) = (['1', '3'], ';' :: rest) + apply takeDigits_append + · decide + · intro c hc + have hcc : c = ';' := (Option.some.inj hc).symm + rw [hcc] + decide + have hval : digitsValue 10 (fun d => d.toNat - 48) ['1', '3'] = 13 := by + decide + have hchar : charRefChar 13 = some '\r' := by decide + simp [parseRef, htake, hval, hchar] + +theorem parseRef_dec9 {rest : List Char} : + parseRef ('#' :: '9' :: ';' :: rest) = some ('\t', rest) := by + have htake : takeDigits ('9' :: ';' :: rest) = (['9'], ';' :: rest) := by + show takeDigits (['9'] ++ (';' :: rest)) = (['9'], ';' :: rest) + apply takeDigits_append + · decide + · intro c hc + have hcc : c = ';' := (Option.some.inj hc).symm + rw [hcc] + decide + have hval : digitsValue 10 (fun d => d.toNat - 48) ['9'] = 9 := by decide + have hchar : charRefChar 9 = some '\t' := by decide + simp [parseRef, htake, hval, hchar] + +theorem parseRef_dec10 {rest : List Char} : + parseRef ('#' :: '1' :: '0' :: ';' :: rest) = some ('\n', rest) := by + have htake : takeDigits ('1' :: '0' :: ';' :: rest) = + (['1', '0'], ';' :: rest) := by + show takeDigits (['1', '0'] ++ (';' :: rest)) = (['1', '0'], ';' :: rest) + apply takeDigits_append + · decide + · intro c hc + have hcc : c = ';' := (Option.some.inj hc).symm + rw [hcc] + decide + have hval : digitsValue 10 (fun d => d.toNat - 48) ['1', '0'] = 10 := by + decide + have hchar : charRefChar 10 = some '\n' := by decide + simp [parseRef, htake, hval, hchar] + +/-! ## Text runs and attribute values -/ + +/-- The five shapes of a printed character of character data, with + the character each shape comes from. -/ +theorem escapeTextChar_cases (c : Char) : + (c = '&' ∧ escapeTextChar c = ['&', 'a', 'm', 'p', ';']) ∨ + (c = '<' ∧ escapeTextChar c = ['&', 'l', 't', ';']) ∨ + (c = '>' ∧ escapeTextChar c = ['&', 'g', 't', ';']) ∨ + (c = '\r' ∧ escapeTextChar c = ['&', '#', '1', '3', ';']) ∨ + (c ≠ '&' ∧ c ≠ '<' ∧ c ≠ '>' ∧ c ≠ '\r' ∧ escapeTextChar c = [c]) := by + by_cases h1 : c = '&' + · exact Or.inl ⟨h1, by simp [escapeTextChar, h1]⟩ + · by_cases h2 : c = '<' + · exact Or.inr (Or.inl ⟨h2, by simp [escapeTextChar, h1, h2]⟩) + · by_cases h3 : c = '>' + · exact Or.inr (Or.inr (Or.inl ⟨h3, by simp [escapeTextChar, h1, h2, h3]⟩)) + · by_cases h4 : c = '\r' + · exact Or.inr (Or.inr (Or.inr + (Or.inl ⟨h4, by simp [escapeTextChar, h1, h2, h3, h4]⟩))) + · exact Or.inr (Or.inr (Or.inr (Or.inr + ⟨h1, h2, h3, h4, by simp [escapeTextChar, h1, h2, h3, h4]⟩))) + +/-- The seven shapes of a printed character of an attribute + value. -/ +theorem escapeAttrChar_cases (c : Char) : + (c = '&' ∧ escapeAttrChar c = ['&', 'a', 'm', 'p', ';']) ∨ + (c = '<' ∧ escapeAttrChar c = ['&', 'l', 't', ';']) ∨ + (c = '"' ∧ escapeAttrChar c = ['&', 'q', 'u', 'o', 't', ';']) ∨ + (c = '\t' ∧ escapeAttrChar c = ['&', '#', '9', ';']) ∨ + (c = '\n' ∧ escapeAttrChar c = ['&', '#', '1', '0', ';']) ∨ + (c = '\r' ∧ escapeAttrChar c = ['&', '#', '1', '3', ';']) ∨ + (c ≠ '&' ∧ c ≠ '<' ∧ c ≠ '"' ∧ c ≠ '\t' ∧ c ≠ '\n' ∧ c ≠ '\r' ∧ + escapeAttrChar c = [c]) := by + by_cases h1 : c = '&' + · exact Or.inl ⟨h1, by simp [escapeAttrChar, h1]⟩ + · by_cases h2 : c = '<' + · exact Or.inr (Or.inl ⟨h2, by simp [escapeAttrChar, h1, h2]⟩) + · by_cases h3 : c = '"' + · exact Or.inr (Or.inr (Or.inl ⟨h3, by simp [escapeAttrChar, h1, h2, h3]⟩)) + · by_cases h4 : c = '\t' + · exact Or.inr (Or.inr (Or.inr + (Or.inl ⟨h4, by simp [escapeAttrChar, h1, h2, h3, h4]⟩))) + · by_cases h5 : c = '\n' + · exact Or.inr (Or.inr (Or.inr (Or.inr + (Or.inl ⟨h5, by simp [escapeAttrChar, h1, h2, h3, h4, h5]⟩)))) + · by_cases h6 : c = '\r' + · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr + (Or.inl ⟨h6, by simp [escapeAttrChar, h1, h2, h3, h4, h5, h6]⟩))))) + · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr + ⟨h1, h2, h3, h4, h5, h6, + by simp [escapeAttrChar, h1, h2, h3, h4, h5, h6]⟩))))) + +/-- A printed text run followed by the end of the text or by a + mark never holds the run `]]>` at the junction the text reader + is about to step over: the two characters the reader looks at + after a `]` it just read are never `]` and `>`. -/ +theorem escapeText_not_bracketGt {cs : List Char} {rest : List Char} + (hrest : rest = [] ∨ rest.head? = some '<') : + ¬ ((escapeText cs ++ rest).head? = some ']' ∧ + ((escapeText cs ++ rest).tail).head? = some '>') := by + intro hcon + obtain ⟨h1, h2⟩ := hcon + cases cs with + | nil => + simp only [escapeText, List.flatMap_nil, List.nil_append] at h1 + rcases hrest with h | h + · rw [h] at h1 + simp at h1 + · rw [h] at h1 + simp at h1 + | cons d ds => + have e1 : escapeText (d :: ds) ++ rest = + escapeTextChar d ++ (escapeText ds ++ rest) := by + have e0 : escapeText (d :: ds) = escapeTextChar d ++ escapeText ds := rfl + rw [e0, List.append_assoc] + rw [e1] at h1 h2 + rcases escapeTextChar_head d with hd | hd + · have hh : (escapeTextChar d ++ (escapeText ds ++ rest)).head? = + some '&' := by + cases hdd : escapeTextChar d with + | nil => exact absurd hdd (escapeTextChar_ne_nil d) + | cons x xs => + have hx : x = '&' := by + have h2' := hd + rw [hdd] at h2' + simp at h2' + exact h2' + simp [hdd, hx] + rw [hh] at h1 + simp at h1 + · rw [hd] at h2 + simp only [List.cons_append, List.tail_cons, List.nil_append] at h2 + cases ds with + | nil => + simp only [escapeText, List.flatMap_nil, List.nil_append] at h2 + rcases hrest with h | h + · rw [h] at h2 + simp at h2 + · rw [h] at h2 + simp at h2 + | cons e es => + have hgt := escapeTextChar_head_ne_gt e + have hh : (escapeText (e :: es) ++ rest).head? = + (escapeTextChar e).head? := by + have e2 : escapeText (e :: es) ++ rest = + escapeTextChar e ++ (escapeText es ++ rest) := by + have e0 : escapeText (e :: es) = + escapeTextChar e ++ escapeText es := rfl + rw [e0, List.append_assoc] + rw [e2] + cases hdd : escapeTextChar e with + | nil => exact absurd hdd (escapeTextChar_ne_nil e) + | cons x xs => simp [hdd] + rw [hh] at h2 + exact hgt h2 + +/-- Reading back a printed text run gives the run back, when the + text after it is empty or starts with a less sign (so the + reader stops there). -/ +theorem parseTextRun_escapeText : ∀ (cs : List Char) (rest : List Char), + (∀ c ∈ cs, LegalChar c) → + (rest = [] ∨ rest.head? = some '<') → + ∀ (f : Nat), cs.length + 1 ≤ f → + parseTextRun f (escapeText cs ++ rest) = some (cs, rest) := by + intro cs + induction cs with + | nil => + intro rest _ hrest f hf + cases f with + | zero => simp at hf + | succ f' => + cases rest with + | nil => simp [parseTextRun, escapeText] + | cons c t => + have hc : c = '<' := by + rcases hrest with h | h + · simp at h + · have h2 : (c :: t).head? = some c := rfl + rw [h2] at h + exact Option.some.inj h + subst hc + simp [parseTextRun, escapeText] + | cons c cs ih => + intro rest hlegal hrest f hf + have hlegal' : ∀ x ∈ cs, LegalChar x := + fun x hx => hlegal x (List.mem_cons_of_mem c hx) + have hclegal : LegalChar c := hlegal c (by simp) + cases f with + | zero => + simp only [List.length_cons] at hf + omega + | succ f' => + have hf' : cs.length + 1 ≤ f' := by + simp only [List.length_cons] at hf + omega + have ih' := ih rest hlegal' hrest f' hf' + have e0 : escapeText (c :: cs) = escapeTextChar c ++ escapeText cs := rfl + rw [e0, List.append_assoc] + rcases escapeTextChar_cases c with + ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2, h3, h4, h5⟩ + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + simp [parseTextRun, ih', parseRef_amp] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + simp [parseTextRun, ih', parseRef_lt] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + simp [parseTextRun, ih', parseRef_gt] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + simp [parseTextRun, ih', parseRef_dec13] + · rw [h5] + simp only [List.cons_append] + by_cases hc : c = ']' + · subst hc + have hnb := escapeText_not_bracketGt (cs := cs) (rest := rest) hrest + simp only [parseTextRun, List.nil_append] + rw [if_pos trivial, if_neg hnb, ih'] + simp + · simp [parseTextRun, ih', h1, h2, h3, h4, hc, + isLegalChar_of hclegal] + +/-- Reading back a printed attribute value gives the value back. + The printer uses double quotes, so the quote here is the + double quote. -/ +theorem parseAttrValue_escapeAttr : ∀ (cs : List Char) (rest : List Char), + (∀ c ∈ cs, LegalChar c) → + ∀ (f : Nat), cs.length + 1 ≤ f → + parseAttrValue '"' f (escapeAttr cs ++ '"' :: rest) = some (cs, rest) := by + intro cs + induction cs with + | nil => + intro rest _ f hf + cases f with + | zero => simp at hf + | succ f' => simp [parseAttrValue, escapeAttr] + | cons c cs ih => + intro rest hlegal f hf + have hlegal' : ∀ x ∈ cs, LegalChar x := + fun x hx => hlegal x (List.mem_cons_of_mem c hx) + have hclegal : LegalChar c := hlegal c (by simp) + cases f with + | zero => + simp only [List.length_cons] at hf + omega + | succ f' => + have hf' : cs.length + 1 ≤ f' := by + simp only [List.length_cons] at hf + omega + have ih' := ih rest hlegal' f' hf' + have e0 : escapeAttr (c :: cs) = escapeAttrChar c ++ escapeAttr cs := rfl + rw [e0, List.append_assoc] + rcases escapeAttrChar_cases c with + ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | + ⟨h1, h2, h3, h4, h5, h6, h7⟩ + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + simp [parseAttrValue, ih', parseRef_amp] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + simp [parseAttrValue, ih', parseRef_lt] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + simp [parseAttrValue, ih', parseRef_quot] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + simp [parseAttrValue, ih', parseRef_dec9] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + simp [parseAttrValue, ih', parseRef_dec10] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + simp [parseAttrValue, ih', parseRef_dec13] + · rw [h7] + simp only [List.cons_append] + simp [parseAttrValue, ih', h1, h2, h3, h4, h5, h6, + isLegalChar_of hclegal] + +/-- Reading back printed character data gives the data back, when + the reader stops at the text that follows. -/ +theorem parseCharData_escapeText (cs : List Char) (rest : List Char) + (hne : cs ≠ []) + (hlegal : ∀ c ∈ cs, LegalChar c) + (hrest : rest = [] ∨ rest.head? = some '<') + (hstop : ∀ f, 1 ≤ f → parseCharData f rest = some ([], rest)) + (f : Nat) (hf : cs.length + 2 ≤ f) : + parseCharData f (escapeText cs ++ rest) = some (cs, rest) := by + cases f with + | zero => omega + | succ f' => + have hf1 : cs.length + 1 ≤ f' := by omega + have htr := parseTextRun_escapeText cs rest hlegal hrest f' hf1 + have hst := hstop f' (by + have h1 : 1 ≤ cs.length := by + cases cs with + | nil => exact absurd rfl hne + | cons c cs' => simp + omega) + obtain ⟨c, cs', hcs⟩ : ∃ c cs', cs = c :: cs' := by + cases cs with + | nil => exact absurd rfl hne + | cons c cs' => exact ⟨c, cs', rfl⟩ + subst hcs + have e0 : escapeText (c :: cs') = escapeTextChar c ++ escapeText cs' := rfl + rw [e0, List.append_assoc] + rcases escapeTextChar_cases c with + ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2, h3, h4, h5⟩ + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + have htr2 : parseTextRun f' + ('&' :: 'a' :: 'm' :: 'p' :: ';' :: (escapeText cs' ++ rest)) = + some ('&' :: cs', rest) := htr + simp [parseCharData, htr2, hst] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + have htr2 : parseTextRun f' + ('&' :: 'l' :: 't' :: ';' :: (escapeText cs' ++ rest)) = + some ('<' :: cs', rest) := htr + simp [parseCharData, htr2, hst] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + have htr2 : parseTextRun f' + ('&' :: 'g' :: 't' :: ';' :: (escapeText cs' ++ rest)) = + some ('>' :: cs', rest) := htr + simp [parseCharData, htr2, hst] + · subst h1 + rw [h2] + simp only [List.cons_append, List.append_assoc] + have htr2 : parseTextRun f' + ('&' :: '#' :: '1' :: '3' :: ';' :: (escapeText cs' ++ rest)) = + some ('\r' :: cs', rest) := htr + simp [parseCharData, htr2, hst] + · rw [h5] + simp only [List.cons_append] + have htr2 : parseTextRun f' (c :: (escapeText cs' ++ rest)) = + some (c :: cs', rest) := by + have htr' := htr + rw [e0, h5] at htr' + simpa only [List.cons_append, List.append_assoc, List.nil_append] + using htr' + simp [parseCharData, htr2, hst, h2] + +/-! ## Names -/ + +theorem takeNameChars_append {ds rest : List Char} + (hd : ∀ d ∈ ds, isNameChar d = true) + (hr : ∀ c, rest.head? = some c → isNameChar c = false) : + takeNameChars (ds ++ rest) = (ds, rest) := by + induction ds generalizing rest with + | nil => + cases rest with + | nil => rfl + | cons c r => + have hc : isNameChar c = false := hr c rfl + simp [takeNameChars, hc] + | cons d ds ih => + have hdd : isNameChar d = true := hd d (by simp) + have ih' := ih (fun x hx => hd x (List.mem_cons_of_mem d hx)) hr + simp [takeNameChars, hdd, ih'] + +/-- A valid name at the head of a text is read whole, when the text + after it does not start with a name character. -/ +theorem parseName_append {cs rest : List Char} (hv : ValidName cs) + (hr : ∀ c, rest.head? = some c → isNameChar c = false) : + parseName (cs ++ rest) = some (cs, rest) := by + obtain ⟨c, ds, hcs, hstart, hchars⟩ := hv + subst hcs + have hsc : isNameStart c = true := isNameStart_of hstart + have htake := takeNameChars_append (ds := ds) (rest := rest) + (fun d hd => isNameChar_of (hchars d hd)) hr + simp [parseName, hsc, htake] + + +/-! ## Comments and processing instructions -/ + +/-- One step of the comment body reader over a dash that does not + close the comment. -/ +theorem parseCommentBody_dash_cons {d : Char} {xs : List Char} + (hd : d ≠ '-') : + parseCommentBody ('-' :: d :: xs) = + (parseCommentBody (d :: xs)).map fun (b, r) => ('-' :: b, r) := by + simp [parseCommentBody, hd] + +/-- Reading back a printed comment body gives the body back. -/ +theorem parseCommentBody_print : ∀ (cs : List Char) (rest : List Char), + NoDashDash cs → NotDashEnd cs → (∀ c ∈ cs, LegalChar c) → + parseCommentBody (cs ++ '-' :: '-' :: '>' :: rest) = some (cs, rest) := by + intro cs + induction cs with + | nil => + intro rest _ _ _ + simp [parseCommentBody] + | cons c cs ih => + intro rest hdd hde hlegal + have hlegal' : ∀ x ∈ cs, LegalChar x := + fun x hx => hlegal x (List.mem_cons_of_mem c hx) + have hclegal : LegalChar c := hlegal c (by simp) + have hdd' : NoDashDash cs := by + intro pre suf h + exact hdd (c :: pre) suf (by simp [h]) + have hde' : NotDashEnd cs := by + intro pre h + exact hde (c :: pre) (by simp [h]) + have ih' := ih rest hdd' hde' hlegal' + by_cases hc : c = '-' + · subst hc + cases cs with + | nil => + exfalso + exact hde [] (by simp) + | cons d ds => + have hd : d ≠ '-' := by + intro e + subst e + exact hdd [] ds (by simp) + have e1 : ('-' :: d :: ds) ++ '-' :: '-' :: '>' :: rest = + '-' :: d :: (ds ++ '-' :: '-' :: '>' :: rest) := by + simp [List.append_assoc] + rw [e1, parseCommentBody_dash_cons hd] + have ih2 : parseCommentBody (d :: (ds ++ '-' :: '-' :: '>' :: rest)) = + some (d :: ds, rest) := by + have := ih' + rwa [show (d :: ds) ++ '-' :: '-' :: '>' :: rest = + d :: (ds ++ '-' :: '-' :: '>' :: rest) by simp [List.append_assoc]] at this + rw [ih2] + rfl + · have e1 : (c :: cs) ++ '-' :: '-' :: '>' :: rest = + c :: (cs ++ '-' :: '-' :: '>' :: rest) := rfl + rw [e1] + simp [parseCommentBody, ih', hc, isLegalChar_of hclegal] + +/-- One step of the processing instruction data reader over a + question mark that does not close the instruction. -/ +theorem parsePIData_quest_cons {d : Char} {xs : List Char} + (hd : d ≠ '>') : + parsePIData ('?' :: d :: xs) = + (parsePIData (d :: xs)).map fun (b, r) => ('?' :: b, r) := by + simp [parsePIData, hd] + +/-- Reading back printed processing instruction data gives the + data back. -/ +theorem parsePIData_print : ∀ (d : List Char) (rest : List Char), + NoQClose d → (∀ c ∈ d, LegalChar c) → + parsePIData (d ++ '?' :: '>' :: rest) = some (d, rest) := by + intro d + induction d with + | nil => + intro rest _ _ + simp [parsePIData] + | cons c d ih => + intro rest hq hlegal + have hlegal' : ∀ x ∈ d, LegalChar x := + fun x hx => hlegal x (List.mem_cons_of_mem c hx) + have hclegal : LegalChar c := hlegal c (by simp) + have hq' : NoQClose d := by + intro pre suf h + exact hq (c :: pre) suf (by simp [h]) + have ih' := ih rest hq' hlegal' + by_cases hc : c = '?' + · subst hc + cases d with + | nil => + simp [parsePIData] + | cons e es => + have he : e ≠ '>' := by + intro hgt + subst hgt + exact hq [] es (by simp) + have e1 : ('?' :: e :: es) ++ '?' :: '>' :: rest = + '?' :: e :: (es ++ '?' :: '>' :: rest) := by + simp [List.append_assoc] + rw [e1, parsePIData_quest_cons he] + have ih2 : parsePIData (e :: (es ++ '?' :: '>' :: rest)) = + some (e :: es, rest) := ih' + rw [ih2] + rfl + · have e1 : (c :: d) ++ '?' :: '>' :: rest = + c :: (d ++ '?' :: '>' :: rest) := rfl + rw [e1] + simp [parsePIData, ih', hc, isLegalChar_of hclegal] + +/-- Whitespace, as the test the parser runs, is false of a + character that is no whitespace character. -/ +theorem isWs_false_of_not {c : Char} (h : ¬ IsWs c) : isWs c = false := by + have h1 : c ≠ ' ' := fun e => h (Or.inl e) + have h2 : c ≠ '\t' := fun e => h (Or.inr (Or.inl e)) + have h3 : c ≠ '\n' := fun e => h (Or.inr (Or.inr (Or.inl e))) + have h4 : c ≠ '\r' := fun e => h (Or.inr (Or.inr (Or.inr e))) + exact isWs_of_ne h1 h2 h3 h4 + +/-- Reading back a printed processing instruction gives the + instruction back. The input is the text after `'] else ' ' :: d ++ ['?', '>']) ++ + rest) = + some (.pi t d, rest) := by + have hres' : ¬ (t.map Char.toLower = ['x', 'm', 'l']) := hres + cases hd : d with + | nil => + subst hd + have hpn := parseName_append hname (rest := ['?', '>'] ++ rest) (by + intro c hc + simp at hc + rw [← hc] + exact isNameChar_false_of not_nameChar_quest) + rw [if_pos rfl, List.append_assoc] + simp only [parsePI] + rw [hpn] + simp [hres'] + | cons c0 d0 => + subst hd + have hpn := parseName_append hname + (rest := (' ' :: (c0 :: d0) ++ ['?', '>']) ++ rest) (by + intro c hc + simp at hc + rw [← hc] + exact isNameChar_false_of not_nameChar_space) + have hstart' : ¬ IsWs c0 := by + rcases hstart with h | h + · simp at h + · exact h c0 d0 rfl + have hsk : skipWs ((' ' :: (c0 :: d0) ++ ['?', '>']) ++ rest) = + (c0 :: d0) ++ '?' :: '>' :: rest := by + have e1 : (' ' :: (c0 :: d0) ++ ['?', '>']) ++ rest = + ' ' :: ((c0 :: d0) ++ '?' :: '>' :: rest) := by + simp [List.append_assoc] + rw [e1] + have hw : isWs ' ' = true := by decide + have hc0 : isWs c0 = false := isWs_false_of_not hstart' + simp [skipWs, hw, hc0] + have hpd := parsePIData_print (c0 :: d0) rest hq hlegal + rw [if_neg (by simp), List.append_assoc] + simp only [parsePI] + rw [hpn] + simp [hres', hsk, hpd, List.append_assoc, isWs] + have hsk2 : skipWs (' ' :: c0 :: (d0 ++ '?' :: '>' :: rest)) = + (c0 :: d0) ++ '?' :: '>' :: rest := by + have h1 : (' ' :: c0 :: (d0 ++ '?' :: '>' :: rest)) = + (' ' :: (c0 :: d0) ++ ['?', '>']) ++ rest := by + simp [List.append_assoc] + rw [h1] + exact hsk + rw [hsk2, hpd] + +/-! ## Printed lengths -/ + +/-- The printed attribute list is at least as long as the list of + attributes. -/ +theorem printAttrs_length_ge : ∀ (attrs : List (List Char × List Char)), + attrs.length ≤ (printAttrs attrs).length := by + intro attrs + induction attrs with + | nil => simp [printAttrs] + | cons kv rest ih => + have h2 := escapeAttr_length_ge kv.2 + simp only [printAttrs, List.length_append, List.length_cons] + omega + +/-- The printed attribute list is long enough to cover any one + value in it, plus one character per attribute. -/ +theorem printAttrs_length_ge_value : + ∀ (attrs : List (List Char × List Char)) (kv : List Char × List Char), + kv ∈ attrs → kv.2.length + attrs.length ≤ (printAttrs attrs).length := by + intro attrs + induction attrs with + | nil => intro kv h; simp at h + | cons kv0 rest ih => + intro kv h + have h3 := printAttrs_length_ge rest + rcases List.mem_cons.mp h with rfl | h' + · have h2 := escapeAttr_length_ge kv.2 + simp only [printAttrs, List.length_append, List.length_cons] + omega + · have h4 := ih kv h' + have h2 := escapeAttr_length_ge kv0.2 + simp only [printAttrs, List.length_append, List.length_cons] + omega + +/-! ## Stopping character data -/ + +/-- Character data stops at a less sign whose next character is + not the bang that would open a CDATA section. -/ +theorem parseCharData_stop_lt_cons {c : Char} {r : List Char} + (hc : c ≠ '!') : + ∀ f, 1 ≤ f → + parseCharData f ('<' :: c :: r) = some ([], '<' :: c :: r) := by + intro f hf + cases f with + | zero => simp at hf + | succ f' => simp [parseCharData, hc] + +/-- Character data stops at a less sign at the end of the text. -/ +theorem parseCharData_stop_lt_nil : + ∀ f, 1 ≤ f → parseCharData f ['<'] = some ([], ['<']) := by + intro f hf + cases f with + | zero => simp at hf + | succ f' => simp [parseCharData] + +/-- Character data stops at the marks that open a comment. -/ +theorem parseCharData_stop_comment {r : List Char} : + ∀ f, 1 ≤ f → + parseCharData f ('<' :: '!' :: '-' :: '-' :: r) = + some ([], '<' :: '!' :: '-' :: '-' :: r) := by + intro f hf + cases f with + | zero => simp at hf + | succ f' => simp [parseCharData] + +/-! ## Attributes -/ + +/-- Reading back a printed attribute list gives the attributes + back, on top of the ones already read. The end of the tag is + left to the caller: the statement ends in a hypothesis that + says what the reader does at the text that follows the printed + attributes. -/ +theorem parseAttrs_print : ∀ (attrs : List (List Char × List Char)) + (acc : List (List Char × List Char)) (tail : List Char) (f : Nat) + (res : Option (List (List Char × List Char) × List Char × Bool)), + AttrsOk attrs → + (∀ kv ∈ attrs, ¬ acc.any (fun p => p.1 = kv.1)) → + (∀ kv ∈ attrs, kv.2.length + attrs.length + 2 ≤ f) → + attrs.length + 1 ≤ f → + (∀ f', 1 ≤ f' → parseAttrs f' (acc ++ attrs) tail = res) → + parseAttrs f acc (printAttrs attrs ++ tail) = res := by + intro attrs + induction attrs with + | nil => + intro acc tail f res _ _ _ hf hfin + have h1 : parseAttrs f (acc ++ []) tail = res := hfin f (by + cases f with + | zero => simp at hf + | succ f' => omega) + simpa [printAttrs] using h1 + | cons kv attrs ih => + intro acc tail f res hok hdisj hfv hf hfin + obtain ⟨a, v⟩ := kv + have hname : ValidName a := hok.1 + have hval : ∀ c ∈ v, LegalChar c := hok.2.1 + have hnodup : ∀ kv2 ∈ attrs, kv2.1 ≠ a := hok.2.2.1 + have hok' : AttrsOk attrs := hok.2.2.2 + obtain ⟨c0, ds, ha, hc0, hds⟩ := hname + subst ha + cases f with + | zero => + simp only [List.length_cons] at hf + omega + | succ f' => + have hf' : attrs.length + 1 ≤ f' := by + simp only [List.length_cons] at hf + omega + have hfv' : ∀ kv2 ∈ attrs, kv2.2.length + attrs.length + 2 ≤ f' := by + intro kv2 h2 + have h3 := hfv kv2 (List.mem_cons_of_mem _ h2) + simp only [List.length_cons] at h3 + omega + have hdisj' : ∀ kv2 ∈ attrs, + ¬ (acc ++ [((c0 :: ds), v)]).any (fun p => p.1 = kv2.1) := by + intro kv2 h2 + rw [List.any_append] + simp only [List.any_cons, List.any_nil, Bool.or_eq_true, + Bool.or_false] + intro e + rcases e with e | e + · exact hdisj kv2 (List.mem_cons_of_mem _ h2) e + · exact hnodup kv2 h2 (of_decide_eq_true e).symm + have hfin' : ∀ f'', 1 ≤ f'' → + parseAttrs f'' ((acc ++ [((c0 :: ds), v)]) ++ attrs) tail = res := by + intro f'' hf'' + have h3 := hfin f'' hf'' + have e : (acc ++ [((c0 :: ds), v)]) ++ attrs = + acc ++ (((c0 :: ds), v) :: attrs) := by + simp [List.append_assoc] + rwa [← e] at h3 + have ih' := ih (acc ++ [((c0 :: ds), v)]) tail f' res hok' hdisj' + hfv' hf' hfin' + have hsk : skipWs (printAttrs (((c0 :: ds), v) :: attrs) ++ tail) = + (c0 :: ds) ++ + ('=' :: '"' :: escapeAttr v ++ '"' :: (printAttrs attrs ++ tail)) := by + have hws1 : isWs ' ' = true := by decide + have hws2 : isWs c0 = false := + isWs_false_of_not (IsNameStart.ne_ws hc0) + simp [printAttrs, skipWs, hws1, hws2, List.append_assoc] + have hpn : parseName + ((c0 :: ds) ++ + ('=' :: '"' :: escapeAttr v ++ '"' :: (printAttrs attrs ++ tail))) = + some ((c0 :: ds), + '=' :: '"' :: escapeAttr v ++ '"' :: (printAttrs attrs ++ tail)) := + parseName_append ⟨c0, ds, rfl, hc0, hds⟩ (by + intro c hc + simp only [List.head?] at hc + rw [← Option.some.inj hc] + exact isNameChar_false_of not_nameChar_eq) + have hpn2 : parseName + (c0 :: (ds ++ + ('=' :: '"' :: (escapeAttr v ++ '"' :: (printAttrs attrs ++ tail))))) = + some ((c0 :: ds), + '=' :: '"' :: (escapeAttr v ++ '"' :: (printAttrs attrs ++ tail))) := + hpn + have hval' : parseAttrValue '"' f' + (escapeAttr v ++ '"' :: (printAttrs attrs ++ tail)) = + some (v, printAttrs attrs ++ tail) := + parseAttrValue_escapeAttr v (printAttrs attrs ++ tail) hval f' (by + have h3 := hfv ((c0 :: ds), v) (by simp) + simp only [List.length_cons] at h3 + omega) + have hdup : acc.any (fun p => p.1 = (c0 :: ds)) = false := by + have h3 := hdisj ((c0 :: ds), v) (by simp) + cases h4 : acc.any (fun p => p.1 = (c0 :: ds)) with + | false => rfl + | true => exact absurd h4 (by exact h3) + have hc0ne1 : c0 ≠ '/' := by + intro e + subst e + have h5 : isNameStart '/' = true := isNameStart_of hc0 + have h6 : isNameStart '/' = false := by decide + rw [h6] at h5 + exact Bool.false_ne_true h5 + have hc0ne2 : c0 ≠ '>' := by + intro e + subst e + have h5 : isNameStart '>' = true := isNameStart_of hc0 + have h6 : isNameStart '>' = false := by decide + rw [h6] at h5 + exact Bool.false_ne_true h5 + have hstep : parseAttrs (f' + 1) acc + (printAttrs (((c0 :: ds), v) :: attrs) ++ tail) = + parseAttrs f' (acc ++ [((c0 :: ds), v)]) + (printAttrs attrs ++ tail) := by + simp [parseAttrs, hsk, hpn2, hval', hdup, hc0ne1, hc0ne2, + isNameStart_of hc0, List.cons_append, List.append_assoc, + skipWs_cons (by decide : isWs '=' = false), + skipWs_cons (by decide : isWs '"' = false)] + rwa [hstep] + +/-- Reading back a printed attribute list that ends a short form + tag. -/ +theorem parseAttrs_print_closed + (attrs : List (List Char × List Char)) + (acc : List (List Char × List Char)) (rest : List Char) (f : Nat) + (hok : AttrsOk attrs) + (hdisj : ∀ kv ∈ attrs, ¬ acc.any (fun p => p.1 = kv.1)) + (hfv : ∀ kv ∈ attrs, kv.2.length + attrs.length + 2 ≤ f) + (hf : attrs.length + 1 ≤ f) : + parseAttrs f acc (printAttrs attrs ++ '/' :: '>' :: rest) = + some (acc ++ attrs, rest, true) := by + apply parseAttrs_print attrs acc _ f _ hok hdisj hfv hf + intro f' hf' + cases f' with + | zero => simp at hf' + | succ f'' => + simp [parseAttrs, skipWs, isWs_slash, + (by decide : isWs '>' = false)] + +/-- Reading back a printed attribute list that ends a start tag. -/ +theorem parseAttrs_print_open + (attrs : List (List Char × List Char)) + (acc : List (List Char × List Char)) (rest : List Char) (f : Nat) + (hok : AttrsOk attrs) + (hdisj : ∀ kv ∈ attrs, ¬ acc.any (fun p => p.1 = kv.1)) + (hfv : ∀ kv ∈ attrs, kv.2.length + attrs.length + 2 ≤ f) + (hf : attrs.length + 1 ≤ f) : + parseAttrs f acc (printAttrs attrs ++ '>' :: rest) = + some (acc ++ attrs, rest, false) := by + apply parseAttrs_print attrs acc _ f _ hok hdisj hfv hf + intro f' hf' + cases f' with + | zero => simp at hf' + | succ f'' => + simp [parseAttrs, skipWs, (by decide : isWs '>' = false)] + +/-! ## Elements and content -/ + +/-- The element half of the round trip, at a bound on the length + of the printed element. -/ +abbrev ElemProp (n : Nat) : Prop := + ∀ (f : Nat), n + 1 ≤ f → ∀ (name : List Char) + (attrs : List (List Char × List Char)) (content : List Node) + (rest : List Char), + WFNode (.elem name attrs content) → + (printNode (.elem name attrs content)).length = n → + parseElement f (printNode (.elem name attrs content) ++ rest) = + some (.elem name attrs content, rest) + +/-- The content half of the round trip, at a bound two more than + the length of the printed content: the two end tag characters + that follow the content are part of the bound, which is what + makes the bound drop at an element inside the content. -/ +abbrev NodesProp (n : Nat) : Prop := + ∀ (f : Nat), n + 1 ≤ f → ∀ (nodes : List Node) (rest : List Char), + WFNodes nodes → + (printNodes nodes).length + 2 = n → + parseNodes f (printNodes nodes ++ '<' :: '/' :: rest) = + some (nodes, '<' :: '/' :: rest) + +/-- A name head is not any of the characters that would send the + content reader down another arm. -/ +theorem IsNameStart.ne_slash {c : Char} (h : IsNameStart c) : c ≠ '/' := by + intro e + subst e + have h5 : isNameStart '/' = true := isNameStart_of h + have h6 : isNameStart '/' = false := by decide + rw [h6] at h5 + exact Bool.false_ne_true h5 + +theorem IsNameStart.ne_quest {c : Char} (h : IsNameStart c) : c ≠ '?' := by + intro e + subst e + have h5 : isNameStart '?' = true := isNameStart_of h + have h6 : isNameStart '?' = false := by decide + rw [h6] at h5 + exact Bool.false_ne_true h5 + +/-- The two halves together, by strong induction on the bound. -/ +theorem elem_nodes : ∀ n, ElemProp n ∧ NodesProp n := by + have aux : ∀ k, ∀ n, n ≤ k → ElemProp n ∧ NodesProp n := by + intro k + induction k with + | zero => + intro n hn + have hn0 : n = 0 := by omega + subst hn0 + constructor + · intro f hf name attrs content rest hwf hlen + simp [printNode, printElem] at hlen + · intro f hf nodes rest hwf hlen + omega + | succ k ihk => + intro n hn + by_cases hn2 : n ≤ k + · exact ihk n hn2 + · have ih : ∀ m, m < n → ElemProp m ∧ NodesProp m := + fun m hm => ihk m (by omega) + constructor + · -- elements + intro f hf name attrs content rest hwf hlen + cases f with + | zero => simp at hf + | succ f' => + have hname : ValidName name := match hwf with + | .elem a _ _ => a + have hattrs : AttrsOk attrs := match hwf with + | .elem _ a _ => a + have hcontent : WFNodes content := match hwf with + | .elem _ _ a => a + obtain ⟨c0, ds, hnameq, hc0, hds⟩ := hname + subst hnameq + have hple : (printAttrs attrs).length + 4 ≤ + (printNode (.elem (c0 :: ds) attrs content)).length := by + by_cases hc : content = [] + · subst hc + simp [printNode, printElem, List.length_append] + · simp [printNode, printElem, hc, List.length_append] + omega + have hfv : ∀ kv ∈ attrs, kv.2.length + attrs.length + 2 ≤ f' := by + intro kv hkv + have h1 := printAttrs_length_ge_value attrs kv hkv + omega + have hfattrs : attrs.length + 1 ≤ f' := by + have h1 := printAttrs_length_ge attrs + omega + by_cases hc : content = [] + · subst hc + have hpn : parseName + ((c0 :: ds) ++ (printAttrs attrs ++ '/' :: '>' :: rest)) = + some ((c0 :: ds), printAttrs attrs ++ '/' :: '>' :: rest) := + parseName_append ⟨c0, ds, rfl, hc0, hds⟩ (by + intro c hc + have hc2 : ∀ x, (printAttrs attrs ++ '/' :: '>' :: rest).head? = + some x → isNameChar x = false := by + intro x hx + cases attrs with + | nil => + simp only [printAttrs, List.nil_append, + List.head?_cons] at hx + rw [← Option.some.inj hx] + exact isNameChar_false_of not_nameChar_slash + | cons kv as => + simp only [printAttrs, List.cons_append, + List.head?_cons] at hx + rw [← Option.some.inj hx] + exact isNameChar_false_of not_nameChar_space + exact hc2 c hc) + have hpn2 : parseName + (c0 :: (ds ++ (printAttrs attrs ++ '/' :: '>' :: rest))) = + some ((c0 :: ds), printAttrs attrs ++ '/' :: '>' :: rest) := + hpn + have hat : parseAttrs f' [] (printAttrs attrs ++ '/' :: '>' :: rest) = + some (attrs, rest, true) := by + have h := parseAttrs_print_closed attrs [] rest f' hattrs + (by intro kv _ e; simp at e) hfv hfattrs + simpa using h + simp [parseElement, printNode, printElem, hpn2, hat, + List.append_assoc] + · have hpn : parseName + ((c0 :: ds) ++ (printAttrs attrs ++ + ('>' :: (printNodes content ++ + '<' :: '/' :: ((c0 :: ds) ++ '>' :: rest))))) = + some ((c0 :: ds), printAttrs attrs ++ + ('>' :: (printNodes content ++ + '<' :: '/' :: ((c0 :: ds) ++ '>' :: rest)))) := + parseName_append ⟨c0, ds, rfl, hc0, hds⟩ (by + intro c hc + have hc2 : ∀ x, (printAttrs attrs ++ + ('>' :: (printNodes content ++ + '<' :: '/' :: ((c0 :: ds) ++ '>' :: rest)))).head? = + some x → isNameChar x = false := by + intro x hx + cases attrs with + | nil => + simp only [printAttrs, List.nil_append, + List.head?_cons] at hx + rw [← Option.some.inj hx] + exact isNameChar_false_of not_nameChar_gt + | cons kv as => + simp only [printAttrs, List.cons_append, + List.head?_cons] at hx + rw [← Option.some.inj hx] + exact isNameChar_false_of not_nameChar_space + exact hc2 c hc) + have hpn2 : parseName + (c0 :: (ds ++ (printAttrs attrs ++ + ('>' :: (printNodes content ++ + '<' :: '/' :: c0 :: (ds ++ '>' :: rest)))))) = + some ((c0 :: ds), printAttrs attrs ++ + ('>' :: (printNodes content ++ + '<' :: '/' :: c0 :: (ds ++ '>' :: rest)))) := + hpn + have hat : parseAttrs f' [] + (printAttrs attrs ++ + ('>' :: (printNodes content ++ + '<' :: '/' :: c0 :: (ds ++ '>' :: rest)))) = + some (attrs, printNodes content ++ + '<' :: '/' :: c0 :: (ds ++ '>' :: rest), false) := by + have h := parseAttrs_print_open attrs [] + (printNodes content ++ '<' :: '/' :: c0 :: (ds ++ '>' :: rest)) + f' hattrs (by intro kv _ e; simp at e) hfv hfattrs + simpa using h + have hm : (printNodes content).length + 2 < n := by + have hlb : (printNodes content).length + 3 ≤ + (printNode (.elem (c0 :: ds) attrs content)).length := by + simp [printNode, printElem, hc, List.length_append] + omega + omega + have hnodes : parseNodes f' + (printNodes content ++ '<' :: '/' :: c0 :: (ds ++ '>' :: rest)) = + some (content, '<' :: '/' :: c0 :: (ds ++ '>' :: rest)) := + (ih ((printNodes content).length + 2) hm).2 f' (by omega) + content (c0 :: (ds ++ '>' :: rest)) hcontent rfl + have hend2 : parseName (c0 :: (ds ++ '>' :: rest)) = + some ((c0 :: ds), '>' :: rest) := + parseName_append ⟨c0, ds, rfl, hc0, hds⟩ (by + intro c hc + simp only [List.head?_cons] at hc + rw [← Option.some.inj hc] + exact isNameChar_false_of not_nameChar_gt) + have hend : parseName ((c0 :: ds) ++ '>' :: rest) = + some ((c0 :: ds), '>' :: rest) := + parseName_append ⟨c0, ds, rfl, hc0, hds⟩ (by + intro c hc + simp only [List.head?_cons] at hc + rw [← Option.some.inj hc] + exact isNameChar_false_of not_nameChar_gt) + simp [parseElement, printNode, printElem, hc, hpn2, hat, hnodes, + hend2, skipWs_cons (by decide : isWs '>' = false), + List.append_assoc, List.cons_append] + · -- content lists + intro f hf nodes rest hwf hlen + cases f with + | zero => simp at hf + | succ f' => + cases nodes with + | nil => + simp [parseNodes, printNodes] + | cons n0 ns => + have hn0 : WFNode n0 := match hwf with + | .cons a _ _ => a + have hns : WFNodes ns := match hwf with + | .cons _ a _ => a + have hadj : (∃ cs, n0 = .text cs) → + ∀ cs, ns.head? ≠ some (.text cs) := match hwf with + | .cons _ _ a => a + have hlen2 : (printNode n0).length + (printNodes ns).length + 2 = + n := by + have h1 := hlen + simp only [printNodes, List.length_append] at h1 + omega + have hm : (printNodes ns).length + 2 < n := by + have hp : 1 ≤ (printNode n0).length := by + cases n0 with + | text cs => + cases hn0 with + | text hne hlegal => + have h1 := escapeText_length_ge cs + have h2 : 1 ≤ cs.length := by + cases cs with + | nil => exact absurd rfl hne + | cons c cs' => simp + simp only [printNode] + omega + | elem name attrs content => simp [printNode, printElem] + | comment cs => simp [printNode] + | pi t d => simp [printNode] + omega + have hIH : parseNodes f' (printNodes ns ++ '<' :: '/' :: rest) = + some (ns, '<' :: '/' :: rest) := + (ih ((printNodes ns).length + 2) hm).2 f' (by omega) ns rest + hns rfl + cases n0 with + | text t => + cases hn0 with + | text hne hlegal => + have hadj' : ∀ cs, ns.head? ≠ some (.text cs) := + hadj ⟨t, rfl⟩ + cases t with + | nil => exact absurd rfl hne + | cons c t' => + have hrest : (printNodes ns ++ '<' :: '/' :: rest) = [] ∨ + (printNodes ns ++ '<' :: '/' :: rest).head? = + some '<' := by + cases ns with + | nil => + right + simp [printNodes] + | cons n1 ns' => + right + cases n1 with + | text cs => + exfalso + exact hadj' cs rfl + | elem name attrs content => + simp [printNodes, printNode, printElem, List.cons_append] + | comment cs => + simp [printNodes, printNode, List.cons_append] + | pi t d => + simp [printNodes, printNode, List.cons_append] + have hstop : ∀ f, 1 ≤ f → + parseCharData f (printNodes ns ++ '<' :: '/' :: rest) = + some ([], printNodes ns ++ '<' :: '/' :: rest) := by + cases ns with + | nil => + intro f hf2 + simpa [printNodes] using + parseCharData_stop_lt_cons (c := '/') (by decide) f hf2 + | cons n1 ns' => + cases n1 with + | text cs => + intro f _ + exfalso + exact hadj' cs rfl + | elem name attrs content => + have hn1 : WFNode (.elem name attrs content) := + match hns with + | .cons a _ _ => a + cases hn1 with + | elem hname1 hattrs1 hcontent1 => + obtain ⟨c1, ds1, hq1, hc1, -⟩ := hname1 + intro f hf2 + cases f with + | zero => simp at hf2 + | succ f'' => + have hc1ne : c1 ≠ '!' := + IsNameStart.ne_bang hc1 + simp [parseCharData, printNodes, printNode, + printElem, hq1, hc1ne, List.append_assoc] + | comment cs => + intro f hf2 + simpa [printNodes, printNode] using + parseCharData_stop_comment + (r := (cs ++ '-' :: '-' :: '>' :: []) ++ + (printNodes ns' ++ '<' :: '/' :: rest)) f hf2 + | pi t d => + intro f hf2 + simpa [printNodes, printNode] using + parseCharData_stop_lt_cons (c := '?') (by decide) f hf2 + have hcd : parseCharData f' + (escapeText (c :: t') ++ + (printNodes ns ++ '<' :: '/' :: rest)) = + some (c :: t', printNodes ns ++ '<' :: '/' :: rest) := + parseCharData_escapeText (c :: t') _ (by simp) hlegal + hrest hstop f' (by + have h1 := escapeText_length_ge (c :: t') + have hlink : (printNode (.text (c :: t'))).length = + (escapeText (c :: t')).length := by + simp [printNode] + omega) + rcases escapeTextChar_cases c with + ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | ⟨h1, h2⟩ | + ⟨h1, h2, h3, h4, h5⟩ + · subst h1 + have hcdX : parseCharData f' + ('&' :: 'a' :: 'm' :: 'p' :: ';' :: (List.flatMap escapeTextChar t' ++ + (printNodes ns ++ '<' :: '/' :: rest))) = + some ('&' :: t', printNodes ns ++ '<' :: '/' :: rest) := + hcd + simp [parseNodes, printNodes, printNode, escapeText, h2, + List.append_assoc] + rw [hcdX] + simp [hIH] + · subst h1 + have hcdX : parseCharData f' + ('&' :: 'l' :: 't' :: ';' :: (List.flatMap escapeTextChar t' ++ + (printNodes ns ++ '<' :: '/' :: rest))) = + some ('<' :: t', printNodes ns ++ '<' :: '/' :: rest) := + hcd + simp [parseNodes, printNodes, printNode, escapeText, h2, + List.append_assoc] + rw [hcdX] + simp [hIH] + · subst h1 + have hcdX : parseCharData f' + ('&' :: 'g' :: 't' :: ';' :: (List.flatMap escapeTextChar t' ++ + (printNodes ns ++ '<' :: '/' :: rest))) = + some ('>' :: t', printNodes ns ++ '<' :: '/' :: rest) := + hcd + simp [parseNodes, printNodes, printNode, escapeText, h2, + List.append_assoc] + rw [hcdX] + simp [hIH] + · subst h1 + have hcdX : parseCharData f' + ('&' :: '#' :: '1' :: '3' :: ';' :: (List.flatMap escapeTextChar t' ++ + (printNodes ns ++ '<' :: '/' :: rest))) = + some ('\r' :: t', printNodes ns ++ '<' :: '/' :: rest) := + hcd + simp [parseNodes, printNodes, printNode, escapeText, h2, + List.append_assoc] + rw [hcdX] + simp [hIH] + · have hcdX : parseCharData f' + (c :: (List.flatMap escapeTextChar t' ++ + (printNodes ns ++ '<' :: '/' :: rest))) = + some (c :: t', printNodes ns ++ '<' :: '/' :: rest) := by + have h := hcd + rw [show escapeText (c :: t') = c :: escapeText t' by + simp [escapeText, h5]] at h + exact h + simp [parseNodes, printNodes, printNode, escapeText, + h5, h1, h2, List.append_assoc] + rw [hcdX] + simp [hIH] + | comment body => + cases hn0 with + | comment hdd hde hlegal => + have hcb : parseCommentBody + (body ++ '-' :: '-' :: '>' :: + (printNodes ns ++ '<' :: '/' :: rest)) = + some (body, printNodes ns ++ '<' :: '/' :: rest) := + parseCommentBody_print body _ hdd hde hlegal + simp [parseNodes, printNodes, printNode, hcb, hIH] + | pi t d => + cases hn0 with + | pi hname hres hq hlegal hstart => + have hpi : parsePI + (t ++ (if d = [] then ['?', '>'] + else ' ' :: d ++ ['?', '>']) ++ + (printNodes ns ++ '<' :: '/' :: rest)) = + some (.pi t d, printNodes ns ++ '<' :: '/' :: rest) := + parsePI_print t d _ hname hres hq hlegal hstart + have hpi2 := hpi + rw [List.append_assoc] at hpi2 + simp only [List.cons_append, List.nil_append] at hpi2 + simp [parseNodes, printNodes, printNode] + rw [hpi2] + simp [hIH] + | elem name attrs content => + cases hn0 with + | elem hname hattrs hcontent => + obtain ⟨c0, ds, hq0, hc0, hds⟩ := hname + have hmE : (printNode (.elem name attrs content)).length < + n := by + omega + have hE : parseElement f' + (printNode (.elem name attrs content) ++ + (printNodes ns ++ '<' :: '/' :: rest)) = + some (.elem name attrs content, + printNodes ns ++ '<' :: '/' :: rest) := + (ih (printNode (.elem name attrs content)).length hmE).1 + f' (by omega) name attrs content + (printNodes ns ++ '<' :: '/' :: rest) + (WFNode.elem ⟨c0, ds, hq0, hc0, hds⟩ hattrs hcontent) rfl + have hc0ne1 : c0 ≠ '/' := IsNameStart.ne_slash hc0 + have hc0ne2 : c0 ≠ '!' := IsNameStart.ne_bang hc0 + have hc0ne3 : c0 ≠ '?' := IsNameStart.ne_quest hc0 + simp only [printNode, printElem, hq0, List.append_assoc, + List.cons_append] at hE + simp [parseNodes, printNodes, printNode, printElem, hq0, + hc0ne1, hc0ne2, hc0ne3, isNameStart_of hc0, + List.append_assoc] + rw [hE] + simp [hIH] + + intro n + exact aux n n (Nat.le_refl n) + +/-- The misc parser stops at a tag whose second character starts + a name: that is an element start, not a comment or a + processing instruction. -/ +theorem parseMisc_stop {f : Nat} {c : Char} {cs : List Char} + (hc : IsNameStart c) : + parseMisc (f + 1) ('<' :: c :: cs) = some ([], '<' :: c :: cs) := by + have h1 : c ≠ '!' := IsNameStart.ne_bang hc + have h2 : c ≠ '?' := IsNameStart.ne_quest hc + have h3 : skipWs ('<' :: c :: cs) = '<' :: c :: cs := + skipWs_cons (by decide) + simp [parseMisc, h3, h1, h2] + +/-- Prologs and epilogs round trip: printing a list of comments + and processing instructions and parsing gives the list back, + with the continuation reached after it. -/ +theorem parseMisc_print : + ∀ (ms : List Node) (rest : List Char), + MiscOk ms → + (∀ f, 1 ≤ f → parseMisc f rest = some ([], skipWs rest)) → + ∀ f, (printNodes ms).length + 1 ≤ f → + parseMisc f (printNodes ms ++ rest) = some (ms, skipWs rest) := by + intro ms + induction ms with + | nil => + intro rest _ hstop f hf + simp only [printNodes, List.nil_append] + exact hstop f (by omega) + | cons n ms ih => + intro rest hok hstop f hf + have hokn : WFNode n ∧ + ((∃ cs, n = .comment cs) ∨ (∃ t d, n = .pi t d)) := + hok n (by simp) + have hoktail : MiscOk ms := + fun m hm => hok m (by simp [hm]) + cases f with + | zero => omega + | succ f' => + rcases hokn with ⟨hwf, hkind⟩ + rcases hkind with ⟨cs, rfl⟩ | ⟨t, d, rfl⟩ + · cases hwf with + | comment hdd hde hlegal => + have hcb : parseCommentBody + (cs ++ '-' :: '-' :: '>' :: (printNodes ms ++ rest)) = + some (cs, printNodes ms ++ rest) := + parseCommentBody_print cs _ hdd hde hlegal + have hlen : (printNodes ms).length + 1 ≤ f' := by + have h2 : (printNode (.comment cs)).length = cs.length + 7 := by + simp [printNode, List.length_append] + have h1 : (printNodes (.comment cs :: ms)).length = + (printNode (.comment cs)).length + + (printNodes ms).length := by + simp [printNodes, List.length_append] + omega + have hih := ih rest hoktail hstop f' hlen + simp [parseMisc, printNodes, printNode, skipWs, hcb, hih, + skipWs_cons (show isWs '<' = false by decide), + List.append_assoc] + · cases hwf with + | pi hname hres hq hlegal hstart => + have hpi : parsePI + (t ++ (if d = [] then ['?', '>'] + else ' ' :: d ++ ['?', '>']) ++ + (printNodes ms ++ rest)) = + some (.pi t d, printNodes ms ++ rest) := + parsePI_print t d _ hname hres hq hlegal hstart + have hlen : (printNodes ms).length + 1 ≤ f' := by + have h2 : 2 ≤ (printNode (.pi t d)).length := by + simp only [printNode, List.length_cons] + omega + have h1 : (printNodes (.pi t d :: ms)).length = + (printNode (.pi t d)).length + + (printNodes ms).length := by + simp [printNodes, List.length_append] + omega + have hpi2 := hpi + rw [List.append_assoc] at hpi2 + simp only [List.cons_append, List.nil_append] at hpi2 + have hih := ih rest hoktail hstop f' hlen + simp [parseMisc, printNodes, printNode, skipWs, hpi2, hih, + skipWs_cons (show isWs '<' = false by decide), + List.append_assoc] + +/-- The plan's claim: printing a well formed document and parsing + the print gives the same document back. -/ +theorem parse_print (d : Document) (hwf : WF d) : + parse (print d) = some d := by + obtain ⟨hpro, hroot, ⟨name, attrs, content, hreq⟩, hepi⟩ := hwf + rw [hreq] at hroot + cases hroot with + | elem hname hattrs hcontent => + obtain ⟨c0, ds, hq0, hc0, hds⟩ := hname + have harg : printNode d.root ++ printNodes d.epilog = + '<' :: c0 :: (ds ++ (printAttrs attrs ++ + (if content = [] then ['/', '>'] + else '>' :: (printNodes content ++ '<' :: '/' :: + ((c0 :: ds) ++ ['>'])))) ++ printNodes d.epilog) := by + rw [hreq, hq0] + simp [printNode, printElem, List.append_assoc, List.cons_append] + have hsw : skipWs (printNode d.root ++ printNodes d.epilog) = + printNode d.root ++ printNodes d.epilog := by + rw [harg] + exact skipWs_cons (by decide) + have hstoproot : ∀ f, 1 ≤ f → + parseMisc f (printNode d.root ++ printNodes d.epilog) = + some ([], skipWs (printNode d.root ++ printNodes d.epilog)) := by + intro f hf + cases f with + | zero => omega + | succ f' => + rw [harg, skipWs_cons (show isWs '<' = false by decide)] + exact parseMisc_stop hc0 + have hstopnil : ∀ f, 1 ≤ f → + parseMisc f [] = some ([], skipWs []) := by + intro f hf + cases f with + | zero => omega + | succ f' => simp [parseMisc, skipWs] + have hpro' : parseMisc ((printNodes d.prolog ++ + (printNode d.root ++ printNodes d.epilog)).length + 1) + (printNodes d.prolog ++ + (printNode d.root ++ printNodes d.epilog)) = + some (d.prolog, skipWs (printNode d.root ++ + printNodes d.epilog)) := + parseMisc_print d.prolog _ hpro hstoproot _ (by + simp only [List.length_append]; omega) + have hroot' : parseElement ((printNodes d.prolog ++ + (printNode d.root ++ printNodes d.epilog)).length + 1) + (printNode d.root ++ printNodes d.epilog) = + some (d.root, printNodes d.epilog) := by + rw [hreq] + exact (elem_nodes (printNode (.elem name attrs content)).length).1 + _ (by + have e : (printNode d.root).length = + (printNode (.elem name attrs content)).length := by + rw [hreq] + simp only [List.length_append]; omega) + name attrs content (printNodes d.epilog) + (WFNode.elem ⟨c0, ds, hq0, hc0, hds⟩ hattrs hcontent) rfl + have hepi' : parseMisc ((printNodes d.prolog ++ + (printNode d.root ++ printNodes d.epilog)).length + 1) (printNodes d.epilog) = + some (d.epilog, skipWs []) := by + have h := parseMisc_print d.epilog [] hepi hstopnil + ((printNodes d.prolog ++ + (printNode d.root ++ printNodes d.epilog)).length + 1) (by + simp only [List.length_append]; omega) + simpa using h + have hPd : print d = printNodes d.prolog ++ + (printNode d.root ++ printNodes d.epilog) := by + simp [print, List.append_assoc] + have hdoc : parseDocument ((printNodes d.prolog ++ + (printNode d.root ++ printNodes d.epilog)).length + 1) + (printNodes d.prolog ++ + (printNode d.root ++ printNodes d.epilog)) = some d := by + simp only [parseDocument, hpro', hsw, hroot', hepi', skipWs, + List.nil_append] + rfl + have hparse : parse (print d) = parseDocument ((printNodes d.prolog ++ + (printNode d.root ++ printNodes d.epilog)).length + 1) (print d) := by + have e : (printNodes d.prolog ++ + (printNode d.root ++ printNodes d.epilog)).length + 1 = (print d).length + 1 := by + simp only [print, List.length_append]; omega + rw [e] + rfl + rw [hparse, hPd] + exact hdoc + +end Xml.Proofs diff --git a/README.md b/README.md index 2a9ab1d..86ac722 100644 --- a/README.md +++ b/README.md @@ -1,32 +1,68 @@ -# xml +# xml: an XML safe-subset parser and printer, with a proved round trip -A Lean parser for a safe subset of XML. This is a Proven Commons project: it rebuilds a widely used format in Lean and proves the new code follows its written specification. It is not a full XML parser. It parses only the subset below. +A parser and printer in Lean for a safe subset of XML 1.0: elements, attributes, text, comments, processing instructions, character references, and CDATA sections, with one root element. There is no document type declaration, no entity declarations, no namespaces, and no XML declaration in the subset; a document with any of those is rejected, not parsed leniently. The printer writes one canonical form. The main claim is proved: printing a well formed document gives a text that parses to the same document. The tests run the parser against Python's `xml.etree.ElementTree` in subset mode; see `tests/TEST-RESULTS.md` for the counts. The full subset rules are in `SPEC.md`. -Status: not verified. No code has landed yet. Plan issue 1 holds the first slice, and it is unclaimed. The specification has not been approved by a reviewer, so do not call this verified. +Status: in progress. The specification has not yet been approved by a reviewer apart from its author, and no statement file (`Spec.lean`) has been added by a reviewer, so this is not verified. -## First slice +## What is proved -Elements, attributes, text, comments, processing instructions, character references, and CDATA sections. One root element. Attribute values are quoted. No document type declaration, no entity declarations, and no namespaces in this slice. A document containing a document type declaration is rejected, not parsed leniently. +The definitions are in `Xml/Value.lean` (the tree type, the printer, and the well-formedness rules) and `Xml/Parse.lean` (the parser). The proofs are in `Proofs/RoundTrip.lean`. -## Main claim +| Claim | Theorem | +|-------|---------| +| Parsing the printed form of a well formed document gives the document back. | `Xml.Proofs.parse_print` | +| The same for one element and for a list of content nodes, proved together by strong induction on the length of the printed form. | `Xml.Proofs.elem_nodes` | +| The same for a prolog or epilog list of comments and processing instructions. | `Xml.Proofs.parseMisc_print` | +| Reading back a printed comment body gives the body back. | `Xml.Proofs.parseCommentBody_print` | +| Reading back a printed processing instruction gives the instruction back. | `Xml.Proofs.parsePI_print` | +| Reading back escaped text and escaped attribute values gives the characters back. | `Xml.Proofs.parseCharData_escapeText`, `Xml.Proofs.parseAttrValue_escapeAttr` | -Printing a parsed document gives a document that parses to the same tree. A document with a document type declaration, an undefined entity reference, or mismatched tags is rejected. The parser never expands an entity, because no entities exist in the subset. +A document is well formed when its names match the subset's name rule, attribute names are unique per element, text holds only legal XML characters and no two text runs stand next to each other, comment bodies contain no `--` and do not end with `-`, processing instruction targets are valid and not the reserved word `xml`, and the prolog and epilog hold only comments and processing instructions. `SPEC.md` states the rules in full. `parse_print` checks against the standard axioms only (`propext`, `Classical.choice`, `Quot.sound`), which a reader can confirm with `#print axioms Xml.Proofs.parse_print`. -## Test oracles +The command-line tool in `Main.lean` calls these functions directly. -- Python ElementTree, Go encoding/xml, and Rust quick-xml, each in a strict subset mode. These parsers disagree outside the subset, on document type and entity handling. The differential harness counts out of subset cases separately, not as failures. +## What is not proved -## Score +- That the parser accepts every text the subset allows, and rejects every text it forbids. The round trip does not need either, so neither is proved. The differential tests check that behaviour instead, and the results file records the outcome, including any failure. +- Anything about documents outside the subset: documents with a document type declaration, entities beyond the five predefined ones, namespaces, an XML declaration, or non-ASCII names. The parser rejects them; whether a full XML parser would accept them is not a claim here. +- Reading requests and printing answers in `Main.lean`: splitting lines, the decimal parser, and the check that a code is a Unicode scalar value. The tests cover them, malformed requests included. +- Speed. The code works on lists of characters, which suits proofs, not large data. The parser's fuel is the length of the input text, which very deep inputs can reach. -14 out of 18, first pass score in mission issue 19, the round 4 sheet. Created at the org owner's direction on that sheet, on the judgement that the slice, claim, and oracles are sound and that it duplicates no existing repo. +Three deliberate choices, also stated in `SPEC.md`: -## What is not in this slice +- CDATA sections are a spelling, not a tree difference. CDATA content becomes ordinary character data in the same text node stream, and the printer never writes a CDATA section. The claim is at tree level, so this is sound. +- There is no line ending normalization in text, comments, processing instruction data, or CDATA: a literal carriage return reads as itself. Full XML normalizes it to a line feed. Inside attribute values both readings agree (either form reads as a space), and the printer always writes a carriage return as a character reference. +- The XML declaration is not in the model. A processing instruction target of `xml` in any letter case rejects everywhere, which keeps the declaration out. -- Document type declarations. -- Entities. -- Namespaces. -- Full XML 1.0. +## What you must trust -## Layout, when the first slice lands +- The Lean kernel, which checks the proofs. +- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. +- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about. +- The operating system and hardware it runs on. +- Python's standard library, as the oracle in the differential tests. The results file names the version used. The plan also names Go's encoding/xml and Rust's quick-xml as oracles; neither is wired in yet, and the harness says so rather than counting them. -The layout follows the Proven Commons template in the mission repo, under bar/template. Spec.lean holds the statements a reviewer approves. Proofs.lean holds the proofs under the same names. Main.lean holds the command line tool used by the tests. The bar check runs in CI on every change. +This project has no dependencies beyond Lean itself. + +## Run it + +Needs Linux and [elan](https://github.com/leanprover/elan). Build, then feed request lines to the tool: + +``` +lake build +echo "parse 60,97,47,62" | .lake/build/bin/xml +``` + +That request is the text `` as character codes, and the answer is `ok:60,97,47,62`. A text the parser rejects, such as the single code `120` (the letter `x`), answers `none`. A malformed request answers `error`. See `SPEC.md` for the full protocol. + +## Re-check it + +Needs Linux, elan, and Python 3.11 or later. + +``` +lake build +grep -rn "sorry" --include="*.lean" Xml Proofs Main.lean Xml.lean Proofs.lean +python3 tests/run_tests.py +``` + +The grep should print nothing: there is no `sorry` anywhere. The test script rebuilds the tool if needed, runs the fixed cases, runs the differential tests against Python's `xml.etree.ElementTree` with a fixed seed, and writes the counts to `tests/TEST-RESULTS.md`. diff --git a/SPEC.md b/SPEC.md new file mode 100644 index 0000000..2f71396 --- /dev/null +++ b/SPEC.md @@ -0,0 +1,224 @@ +# Specification: xml + +A parser and printer in Lean for a safe subset of XML 1.0 (Fifth +Edition), narrowed as stated here. A reviewer who did not write +this specification approves it, together with any statement file +a reviewer adds later. No such file exists yet, so nothing here +counts toward the verified bar yet. + +Text is `List Char`. A Lean `Char` is one Unicode scalar value. + +## The subset in one paragraph + +A document is a prolog of comments and processing instructions, +one root element, and an epilog of comments and processing +instructions. There is no XML declaration, no document type +declaration, no entity declarations, and no namespaces. The only +entity references are the five predefined ones, plus character +references. Anything outside the rules below is rejected, never +parsed leniently. + +## Documents + +- The prolog and the epilog hold only comments and processing + instructions, with whitespace allowed between them and around + the root. Any other text at the top level (character data, a + second element, a document type declaration, a CDATA section) + rejects. +- There is exactly one root element. +- The XML declaration is not part of this subset. A processing + instruction whose target is `xml`, in any letter case, rejects + everywhere, which keeps the declaration form (``) + out. A producer that writes a declaration can be asked for the + same document without it. Other targets that merely start with + the letters xml, such as `xml-stylesheet`, are ordinary + processing instructions. + +## Names + +- A name starts with an ASCII letter (A to Z, a to z) or an + underscore. +- Later characters may also be ASCII digits, a hyphen, or a dot. +- A colon is never allowed in a name in this subset. In XML a + colon signals namespace use, and namespaces are out. +- Non-ASCII names are out of the subset. XML 1.0 allows far + more; that is later work, not this slice. + +## Elements and attributes + +- An element is a name, attributes, and either an empty element + tag (``) or content and a matching end tag (`...`). + Mismatched tags reject. +- An attribute is a name, an equals sign, and a quoted value. + Single and double quotes are both read; the printer writes + double quotes. +- A duplicate attribute name on one element rejects. +- Whitespace may appear between attributes, around the equals + sign, and before the closing bracket of a start tag or an end + tag. +- In an attribute value: character references and the five + predefined entities are expanded on read. A raw `<` rejects. + A raw `&` that does not begin a valid reference rejects. +- Attribute value normalization: a literal tab or line feed in + a value reads as one space, and a literal carriage return or + carriage return with line feed reads as one space. This is + XML's rule for CDATA type attributes, and every attribute here + is CDATA type because there is no document type declaration + to say otherwise. A tab or line feed spelled as a character + reference is not normalized; it reads as itself. The model + holds the normalized value, so printing and reparsing is + stable. + +## Text + +- Character data runs between markup. A raw `<` begins markup, + never text. A raw `&` must begin a valid reference. +- The five predefined entities decode: `<`, `>`, `&`, + `'`, `"`. Any other entity reference rejects, + because no entities exist in the subset. +- A character reference (`A` decimal, `A` hex; the x is + lowercase only) decodes to its character. The value must be a + legal XML character: tab, line feed, carriage return, 0x20 to + 0xD7FF, 0xE000 to 0xFFFD, or 0x10000 to 0x10FFFF. Anything + else (zero, a control character, a surrogate value, a value + past 0x10FFFF) rejects. +- A raw character in text, a comment, a processing instruction, + a CDATA section, or an attribute value must also be a legal + XML character, or the text rejects. +- The sequence `]]>` inside text rejects, as XML requires + outside a CDATA section. +- Adjacent character data merges into one text node in the + model: plain text, character references, and CDATA sections + between two markup items form a single run. The printer + writes one run, and the round trip claim is about this merged + tree. + +## CDATA sections + +- A CDATA section (``) may appear inside + element content only, never in the prolog or the epilog. +- The text inside is literal. In the model it becomes ordinary + character data in the same text node stream as its neighbours. + CDATA is a spelling, not a tree difference, exactly as the + choice of quote in an attribute is a spelling. The printer + never writes a CDATA section. + +## Comments + +- A comment is ``. The body must not + contain `--` and must not end with `-`. Both are XML's rules, + and they keep the closing marks unambiguous. +- The body is carried as the characters between the marks. +- A comment may appear in the prolog, in content, or in the + epilog, and is a node in place. + +## Processing instructions + +- A processing instruction is `` at once, + or whitespace and data up to `?>`. +- The target `xml` in any letter case is reserved and rejects + (see Documents). +- The data is carried as text. It may be empty. It must not + contain `?>`, and in the model it never starts with + whitespace: the whitespace after the target is a separator, + not part of the data. + +## Document type declarations and other ``. An element read from `` has no content + and also prints as ``: same tree, different spelling. +- In text: `&` as `&`, `<` as `<`, `>` as `>` (always + escaping `>` keeps `]]>` from ever forming in printed text), + and carriage return as ` `. Every other character prints + as itself. +- In attribute values: `&` as `&`, `<` as `<`, `"` as + `"`, and tab, line feed, and carriage return as + ` `, ` `, ` `. A literal tab in a printed value + would read back as a space under normalization, so character + references are how those characters are kept. +- A processing instruction with no data prints as ``; + with data, as `` with one space. +- A document prints as its prolog, its root, and its epilog, + with nothing between them. + +## Well formed trees + +The round trip is claimed for trees that satisfy a well +formedness predicate (`WF` in `Xml/Value.lean`): + +- every name matches the name rule above; +- attribute names are unique per element, and attribute values + hold only legal XML characters; +- text nodes are not empty, hold only legal XML characters, + and two text nodes never stand next to each other (the + parser merges them, so an unmerged tree could not come + back); +- comment bodies hold only legal characters, contain no `--`, + and do not end with `-`; +- processing instruction targets are valid names and not the + reserved word, their data holds only legal characters, never + contains `?>`, and never starts with whitespace; +- the root is an element, and the prolog and epilog hold only + comments and processing instructions. + +## The claim + +Printing a well formed document gives a text that parses to +the same document: `parse (print d) = some d`. The theorem is +`Xml.Proofs.parse_print`. It checks against the standard axioms +only (`propext`, `Classical.choice`, `Quot.sound`), which a +reader can confirm with `#print axioms +Xml.Proofs.parse_print`. + +## Boundaries and named differences + +- No line ending normalization in text, comments, processing + instruction data, or CDATA sections: a literal carriage + return there reads as itself. Full XML normalizes carriage + return and carriage return with line feed to a line feed + before parsing, and Python's ElementTree does so. That is a + difference between this subset and full XML, stated plainly: + a text a full XML parser reads one way can read with a line + feed where this parser keeps a carriage return. Inside + attribute values both readings agree, because normalization + there sends either form to a space, and in printed form a + carriage return is always a character reference. +- No document type declaration, no entities beyond the five, + no namespaces, no XML declaration, ASCII names only. A full + XML parser may accept documents this slice rejects for + exactly those reasons; the test harness counts those as out + of subset disagreements, not failures. +- ElementTree, the one oracle wired into the tests, drops the + prolog and epilog when it reads a document, so the harness + compares ElementTree's tree for the root element and checks + the prolog and epilog through the canonical print. The plan + also names Go's encoding/xml and Rust's quick-xml as oracles; + neither is wired in yet, and the harness says so rather than + counting them. + +## The request protocol + +The command line tool in `Main.lean` reads one request per +line and prints one answer per line. A request is the operation +`parse`, then one space, then the input as comma-separated +decimal character codes. The answer is `ok:` and the character +codes of the canonical print, `none` when the text is +rejected, and `error` when the request itself is malformed (an +unknown operation, a number that is not plain decimal digits, +or a code that is not a Unicode scalar value). A request with +no codes is the empty input, which answers `none`. A line may +end in LF or CR LF. diff --git a/Xml.lean b/Xml.lean new file mode 100644 index 0000000..d2357ca --- /dev/null +++ b/Xml.lean @@ -0,0 +1,2 @@ +import Xml.Value +import Xml.Parse diff --git a/Xml/Parse.lean b/Xml/Parse.lean new file mode 100644 index 0000000..b8f8834 --- /dev/null +++ b/Xml/Parse.lean @@ -0,0 +1,423 @@ +/- + The XML parser for the safe subset. It reads a list of characters + and returns a document, or `none` when the text sits outside the + subset grammar `SPEC.md` states. + + Rules the parser follows: + + - Any ` [] + | c :: cs => if isWs c then skipWs cs else c :: cs + +/-- A digit, as a test. -/ +def isDigit (c : Char) : Bool := + decide ('0' ≤ c ∧ c ≤ '9') + +/-- The value of one hex digit, in either case. -/ +def hexVal (c : Char) : Option Nat := + if '0' ≤ c ∧ c ≤ '9' then some (c.toNat - 48) + else if 'a' ≤ c ∧ c ≤ 'f' then some (c.toNat - 87) + else if 'A' ≤ c ∧ c ≤ 'F' then some (c.toNat - 55) + else none + +/-- A hex digit, as a test. -/ +def isHexDigit (c : Char) : Bool := + (hexVal c).isSome + +/-- The longest run of decimal digits at the head of the text, and + the text after it. -/ +def takeDigits : List Char → List Char × List Char + | [] => ([], []) + | c :: rest => + if isDigit c then + let (ds, r) := takeDigits rest + (c :: ds, r) + else ([], c :: rest) + +/-- The longest run of hex digits at the head of the text, and the + text after it. -/ +def takeHexDigits : List Char → List Char × List Char + | [] => ([], []) + | c :: rest => + if isHexDigit c then + let (ds, r) := takeHexDigits rest + (c :: ds, r) + else ([], c :: rest) + +/-- The value of a run of digits in the given base, where `dv` + gives the value of one digit. An empty run has value zero, + which the character reference check then rejects, since zero + names no legal character. -/ +def digitsValue (base : Nat) (dv : Char → Nat) (ds : List Char) : Nat := + ds.foldl (fun acc d => acc * base + dv d) 0 + +/-- The character a character reference value names, when the + value is a legal XML character; otherwise rejection. -/ +def charRefChar (n : Nat) : Option Char := + if n = 9 ∨ n = 10 ∨ n = 13 ∨ (0x20 ≤ n ∧ n ≤ 0xD7FF) ∨ + (0xE000 ≤ n ∧ n ≤ 0xFFFD) ∨ (0x10000 ≤ n ∧ n ≤ 0x10FFFF) + then some (Char.ofNat n) + else none + +/-- Read a reference, at the text after the ampersand: one of the + five predefined entities, or a character reference. Returns + the character the reference stands for and the text after the + semicolon. -/ +def parseRef : List Char → Option (Char × List Char) + | 'l' :: 't' :: ';' :: rest => some ('<', rest) + | 'g' :: 't' :: ';' :: rest => some ('>', rest) + | 'a' :: 'm' :: 'p' :: ';' :: rest => some ('&', rest) + | 'a' :: 'p' :: 'o' :: 's' :: ';' :: rest => some ('\'', rest) + | 'q' :: 'u' :: 'o' :: 't' :: ';' :: rest => some ('"', rest) + | '#' :: rest => + if rest.head? = some 'x' then + let (ds, r) := takeHexDigits rest.tail + match r with + | ';' :: r2 => (charRefChar (digitsValue 16 (fun d => (hexVal d).getD 0) ds)).map + fun ch => (ch, r2) + | _ => none + else + let (ds, r) := takeDigits rest + match r with + | ';' :: r2 => (charRefChar (digitsValue 10 (fun d => d.toNat - 48) ds)).map + fun ch => (ch, r2) + | _ => none + | _ => none + +/-- The longest run of name characters at the head of the text, + and the text after it. -/ +def takeNameChars : List Char → List Char × List Char + | [] => ([], []) + | c :: rest => + if isNameChar c then + let (ds, r) := takeNameChars rest + (c :: ds, r) + else ([], c :: rest) + +/-- Read a name at the head of the text: a name start character, + then name characters. -/ +def parseName : List Char → Option (List Char × List Char) + | c :: rest => + if isNameStart c then + let (ds, r) := takeNameChars rest + some (c :: ds, r) + else none + | [] => none + +/-- Read character data up to the next less sign or the end of the + text: plain characters that are legal XML characters, and + references. The run `]]>` is rejected, as XML requires. The + fuel bounds the number of characters and references read, + since a reference can stand for one character while taking + several. -/ +def parseTextRun : Nat → List Char → Option (List Char × List Char) + | 0, _ => none + | _ + 1, [] => some ([], []) + | fuel + 1, c :: rest => + if c = '<' then some ([], c :: rest) + else if c = '&' then + match parseRef rest with + | some (ch, r) => (parseTextRun fuel r).map fun (t, r2) => (ch :: t, r2) + | none => none + else if c = ']' then + if rest.head? = some ']' ∧ (rest.tail).head? = some '>' then none + else (parseTextRun fuel rest).map fun (t, r) => (c :: t, r) + else if isLegalChar c then + (parseTextRun fuel rest).map fun (t, r) => (c :: t, r) + else none + +/-- Read the body of a CDATA section, up to the closing marks. The + characters are literal: no reference is read, and the run `]]>` + ends the section wherever it stands. -/ +def parseCDATABody : List Char → Option (List Char × List Char) + | [] => none + | ']' :: ']' :: '>' :: rest => some ([], rest) + | c :: rest => + if isLegalChar c then + (parseCDATABody rest).map fun (t, r) => (c :: t, r) + else none + +/-- Read the body of a comment, up to the closing marks. Two + dashes in a row inside the body are rejected, as XML requires, + so the first closing marks end the comment. -/ +def parseCommentBody : List Char → Option (List Char × List Char) + | [] => none + | c :: rest => + if c = '-' then + match rest with + | '-' :: '>' :: r => some ([], r) + | '-' :: _ => none + | _ => + (parseCommentBody rest).map fun (b, r) => (c :: b, r) + else if isLegalChar c then + (parseCommentBody rest).map fun (b, r) => (c :: b, r) + else none + +/-- Read the data of a processing instruction, up to the closing + marks. The data is literal. -/ +def parsePIData : List Char → Option (List Char × List Char) + | [] => none + | c :: rest => + if c = '?' then + match rest with + | '>' :: r => some ([], r) + | _ => + (parsePIData rest).map fun (d, r) => (c :: d, r) + else if isLegalChar c then + (parsePIData rest).map fun (d, r) => (c :: d, r) + else none + +/-- Read an attribute value, at the text after the opening quote + `q`. Returns the normalized value and the text after the + closing quote. A literal less sign is rejected; a literal tab + or line feed reads as a space; a literal carriage return reads + as one space, with a line feed right after it read as part of + the same return. References read as the characters they name, + with no normalization. The fuel bounds the number of + characters and references read, as in `parseTextRun`. -/ +def parseAttrValue (q : Char) : Nat → List Char → Option (List Char × List Char) + | 0, _ => none + | _ + 1, [] => none + | fuel + 1, c :: rest => + if c = q then some ([], rest) + else if c = '<' then none + else if c = '&' then + match parseRef rest with + | some (ch, r) => (parseAttrValue q fuel r).map fun (v, r2) => (ch :: v, r2) + | none => none + else if c = '\t' ∨ c = '\n' then + (parseAttrValue q fuel rest).map fun (v, r) => (' ' :: v, r) + else if c = '\r' then + match rest with + | '\n' :: rest2 => + (parseAttrValue q fuel rest2).map fun (v, r) => (' ' :: v, r) + | _ => + (parseAttrValue q fuel rest).map fun (v, r) => (' ' :: v, r) + else if isLegalChar c then + (parseAttrValue q fuel rest).map fun (v, r) => (c :: v, r) + else none + +/-- Read one processing instruction, at the text after ` + if target.map Char.toLower = ['x', 'm', 'l'] then none + else + match r1 with + | '?' :: '>' :: r2 => some (.pi target [], r2) + | c :: _ => + if isWs c then + match parsePIData (skipWs r1) with + | some (d, r2) => some (.pi target d, r2) + | none => none + else none + | [] => none + | none => none + +/-- Read character data at the head of the text: plain runs, + references, and CDATA sections, merged into one list of + characters. Stops before a less sign that does not open a CDATA + section, and at the end of the text. -/ +def parseCharData : Nat → List Char → Option (List Char × List Char) + | 0, _ => none + | _ + 1, [] => some ([], []) + | fuel + 1, '<' :: '!' :: '[' :: 'C' :: 'D' :: 'A' :: 'T' :: 'A' :: '[' :: rest => + match parseCDATABody rest with + | some (t, r) => (parseCharData fuel r).map fun (t2, r2) => (t ++ t2, r2) + | none => none + | fuel + 1, '<' :: rest => some ([], '<' :: rest) + | fuel + 1, cs => + match parseTextRun fuel cs with + | some (t, r) => (parseCharData fuel r).map fun (t2, r2) => (t ++ t2, r2) + | none => none + +/-- Read the attributes of a start tag, and how the tag ends. + Attributes read so far are in `acc`, in order. Returns the + attributes, the text after the tag, and whether the tag was + the empty form. A repeated attribute name is rejected. -/ +def parseAttrs : Nat → List (List Char × List Char) → List Char → + Option (List (List Char × List Char) × List Char × Bool) + | 0, _, _ => none + | fuel + 1, acc, cs => + match skipWs cs with + | '/' :: '>' :: rest => some (acc, rest, true) + | '>' :: rest => some (acc, rest, false) + | c :: _ => + if isNameStart c then + match parseName (skipWs cs) with + | some (aname, r1) => + match skipWs r1 with + | '=' :: r2 => + match skipWs r2 with + | '"' :: r3 => + match parseAttrValue '"' fuel r3 with + | some (v, r4) => + if acc.any (fun kv => kv.1 = aname) then none + else parseAttrs fuel (acc ++ [(aname, v)]) r4 + | none => none + | '\'' :: r3 => + match parseAttrValue '\'' fuel r3 with + | some (v, r4) => + if acc.any (fun kv => kv.1 = aname) then none + else parseAttrs fuel (acc ++ [(aname, v)]) r4 + | none => none + | _ => none + | _ => none + | none => none + else none + | [] => none + +mutual +/-- Read one element, at the less sign of its start tag. -/ +def parseElement : Nat → List Char → Option (Node × List Char) + | 0, _ => none + | fuel + 1, cs => + match cs with + | '<' :: rest => + match parseName rest with + | some (name, r1) => + match parseAttrs fuel [] r1 with + | some (attrs, r2, true) => some (.elem name attrs [], r2) + | some (attrs, r2, false) => + match parseNodes fuel r2 with + | some (content, r3) => + match r3 with + | '<' :: '/' :: r4 => + match parseName r4 with + | some (ename, r5) => + match skipWs r5 with + | '>' :: r6 => + if ename = name then some (.elem name attrs content, r6) + else none + | _ => none + | none => none + | _ => none + | none => none + | none => none + | none => none + | _ => none + +/-- Read the content of an element: nodes up to the end tag, which + is not consumed. Also returns at the end of the text. -/ +def parseNodes : Nat → List Char → Option (List Node × List Char) + | 0, _ => none + | fuel + 1, cs => + match cs with + | [] => some ([], []) + | '<' :: '/' :: _ => some ([], cs) + | '<' :: '!' :: '-' :: '-' :: rest => + match parseCommentBody rest with + | some (body, r) => + (parseNodes fuel r).map fun (ns, r2) => (.comment body :: ns, r2) + | none => none + | '<' :: '!' :: '[' :: 'C' :: 'D' :: 'A' :: 'T' :: 'A' :: '[' :: _ => + match parseCharData fuel cs with + | some (t, r) => + if t = [] then parseNodes fuel r + else (parseNodes fuel r).map fun (ns, r2) => (.text t :: ns, r2) + | none => none + | '<' :: '?' :: rest => + match parsePI rest with + | some (n, r) => + (parseNodes fuel r).map fun (ns, r2) => (n :: ns, r2) + | none => none + | '<' :: c :: _ => + if isNameStart c then + match parseElement fuel cs with + | some (n, r) => + (parseNodes fuel r).map fun (ns, r2) => (n :: ns, r2) + | none => none + else none + | '<' :: [] => none + | _ => + match parseCharData fuel cs with + | some (t, r) => + if t = [] then parseNodes fuel r + else (parseNodes fuel r).map fun (ns, r2) => (.text t :: ns, r2) + | none => none +end + +/-- Read the miscellany of a prolog or an epilog: comments and + processing instructions, with whitespace around them. Returns + the nodes and the text that follows, which starts at the first + character that is neither whitespace nor a comment or a + processing instruction. -/ +def parseMisc : Nat → List Char → Option (List Node × List Char) + | 0, _ => none + | fuel + 1, cs => + let s := skipWs cs + match s with + | '<' :: '!' :: '-' :: '-' :: rest => + match parseCommentBody rest with + | some (body, r) => + (parseMisc fuel r).map fun (ns, r2) => (.comment body :: ns, r2) + | none => none + | '<' :: '?' :: rest => + match parsePI rest with + | some (n, r) => + (parseMisc fuel r).map fun (ns, r2) => (n :: ns, r2) + | none => none + | _ => some ([], s) + +/-- Parse a whole text: a prolog, one root element, an epilog, and + nothing else. -/ +def parseDocument (fuel : Nat) (cs : List Char) : Option Document := + match parseMisc fuel cs with + | some (prolog, r1) => + match parseElement fuel r1 with + | some (root, r2) => + match parseMisc fuel r2 with + | some (epilog, r3) => if skipWs r3 = [] then some ⟨prolog, root, epilog⟩ else none + | none => none + | none => none + | none => none + +/-- Parse a whole text, with the fuel the length of the text + allows. -/ +def parse (cs : List Char) : Option Document := + parseDocument (cs.length + 1) cs + +end Xml diff --git a/Xml/Value.lean b/Xml/Value.lean new file mode 100644 index 0000000..650702b --- /dev/null +++ b/Xml/Value.lean @@ -0,0 +1,271 @@ +/- + The XML tree type for the safe subset, the canonical printer, and + the well formed predicate that the round trip proof in `Proofs` + uses. + + The subset is XML 1.0 narrowed as `SPEC.md` states: elements, + attributes, text, comments, and processing instructions, with + character references and CDATA sections read as character data. + There is no document type declaration, no entity beyond the five + predefined ones, no namespace, and no XML declaration. + + A node is one of: + + - `text`: a run of character data, held as a list of characters. + Text written as plain characters, as character references, and + as CDATA sections all lands here as one run: the three are + spellings of the same character data, not different trees. + - `elem`: an element: a name, a list of attribute name and value + pairs in the order held, and a list of content nodes. + - `comment`: a comment, held as the characters between the marks. + - `pi`: a processing instruction: a target name and the data + after it, held as characters. + + A document is a list of prolog nodes (comments and processing + instructions only), one root element, and a list of epilog nodes. + + Attribute values are held normalized, the way the parser reads + them: a literal tab or newline in the source is a space in the + value, and the five predefined entities and the character + references are the characters they stand for. +-/ + +namespace Xml + +/-- A node in a document or in element content. -/ +inductive Node where + | text (cs : List Char) + | elem (name : List Char) (attrs : List (List Char × List Char)) + (content : List Node) + | comment (cs : List Char) + | pi (target : List Char) (data : List Char) + +/-- A document: prolog, one root element, epilog. -/ +structure Document where + prolog : List Node + root : Node + epilog : List Node + +/-! ## Characters and names -/ + +/-- A legal XML character, as a proposition, in code points: tab, + line feed, carriage return, then the ranges of the XML 1.0 + character production. A Lean `Char` is a Unicode scalar value, + so no character here can be half of a surrogate pair; the + surrogate range is excluded all the same, since a character + reference can name it. -/ +def LegalChar (c : Char) : Prop := + c.toNat = 9 ∨ c.toNat = 10 ∨ c.toNat = 13 ∨ + (0x20 ≤ c.toNat ∧ c.toNat ≤ 0xD7FF) ∨ + (0xE000 ≤ c.toNat ∧ c.toNat ≤ 0xFFFD) ∨ + (0x10000 ≤ c.toNat ∧ c.toNat ≤ 0x10FFFF) + +/-- The legal character test the parser runs. -/ +def isLegalChar (c : Char) : Bool := + decide (c.toNat = 9 ∨ c.toNat = 10 ∨ c.toNat = 13 ∨ + (0x20 ≤ c.toNat ∧ c.toNat ≤ 0xD7FF) ∨ + (0xE000 ≤ c.toNat ∧ c.toNat ≤ 0xFFFD) ∨ + (0x10000 ≤ c.toNat ∧ c.toNat ≤ 0x10FFFF)) + +theorem isLegalChar_iff {c : Char} : isLegalChar c = true ↔ LegalChar c := by + simp only [isLegalChar, LegalChar, decide_eq_true_eq] + +/-- The first character of a name in the subset: an ASCII letter or + an underscore. The colon is not a name character in this + subset, since namespaces are out. -/ +def IsNameStart (c : Char) : Prop := + ('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') ∨ c = '_' + +/-- A later character of a name: a name start character, a digit, a + hyphen, or a point. -/ +def IsNameChar (c : Char) : Prop := + IsNameStart c ∨ ('0' ≤ c ∧ c ≤ '9') ∨ c = '-' ∨ c = '.' + +/-- The name start test the parser runs. -/ +def isNameStart (c : Char) : Bool := + decide (('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') ∨ c = '_') + +theorem isNameStart_iff {c : Char} : isNameStart c = true ↔ IsNameStart c := by + simp only [isNameStart, IsNameStart, decide_eq_true_eq] + +/-- The name character test the parser runs. -/ +def isNameChar (c : Char) : Bool := + decide ((('A' ≤ c ∧ c ≤ 'Z') ∨ ('a' ≤ c ∧ c ≤ 'z') ∨ c = '_') ∨ + ('0' ≤ c ∧ c ≤ '9') ∨ c = '-' ∨ c = '.') + +theorem isNameChar_iff {c : Char} : isNameChar c = true ↔ IsNameChar c := by + simp only [isNameChar, IsNameChar, IsNameStart, decide_eq_true_eq] + +/-- A name that follows the subset rule: a name start character, + then name characters. -/ +def ValidName (cs : List Char) : Prop := + ∃ c ds, cs = c :: ds ∧ IsNameStart c ∧ ∀ x ∈ ds, IsNameChar x + +/-- Whitespace in XML: space, tab, line feed, carriage return, as a + proposition. -/ +def IsWs (c : Char) : Prop := + c = ' ' ∨ c = '\t' ∨ c = '\n' ∨ c = '\r' + +/-- No two dashes in a row anywhere in the list, stated as: the + list is never a part, then two dashes, then a part. The body of + a comment must satisfy this. -/ +def NoDashDash (cs : List Char) : Prop := + ∀ pre suf, cs ≠ pre ++ '-' :: '-' :: suf + +/-- The list does not end with a dash. The body of a comment must + also satisfy this, or the closing marks run into the body. -/ +def NotDashEnd (cs : List Char) : Prop := + ∀ pre, cs ≠ pre ++ ['-'] + +/-- No `?>` anywhere in the list, stated as: the list is never a + part, then a question mark and a greater sign, then a part. + The data of a processing instruction must satisfy this. -/ +def NoQClose (cs : List Char) : Prop := + ∀ pre suf, cs ≠ pre ++ '?' :: '>' :: suf + +/-- A processing instruction target is reserved when it is the word + `xml`, in any case. A document whose first processing + instruction target is `xml` is the XML declaration form, which + this subset does not hold. -/ +def IsXmlTarget (t : List Char) : Prop := + t.map Char.toLower = ['x', 'm', 'l'] + +/-! ## The printer -/ + +/-- The printed form of one character of character data. The + ampersand, the less sign, and the greater sign are written as + the predefined entities, so a printed text can never hold the + forbidden `]]>` run. A carriage return is written as a + character reference, so it reads back as itself. Every other + character is written as it is. -/ +def escapeTextChar (c : Char) : List Char := + if c = '&' then ['&', 'a', 'm', 'p', ';'] + else if c = '<' then ['&', 'l', 't', ';'] + else if c = '>' then ['&', 'g', 't', ';'] + else if c = '\r' then ['&', '#', '1', '3', ';'] + else [c] + +/-- The printed form of a run of character data. -/ +def escapeText (cs : List Char) : List Char := + cs.flatMap escapeTextChar + +/-- The printed form of one character of an attribute value. The + ampersand and the less sign are written as entities, the quote + as an entity, and tab, line feed, and carriage return as + character references, because a literal one of those three + would read back as a space under the parser's normalization. + Every other character is written as it is. -/ +def escapeAttrChar (c : Char) : List Char := + if c = '&' then ['&', 'a', 'm', 'p', ';'] + else if c = '<' then ['&', 'l', 't', ';'] + else if c = '"' then ['&', 'q', 'u', 'o', 't', ';'] + else if c = '\t' then ['&', '#', '9', ';'] + else if c = '\n' then ['&', '#', '1', '0', ';'] + else if c = '\r' then ['&', '#', '1', '3', ';'] + else [c] + +/-- The printed form of an attribute value, without the quotes. -/ +def escapeAttr (cs : List Char) : List Char := + cs.flatMap escapeAttrChar + +/-- The printed form of the attribute list: each pair preceded by + one space, the name, an equals sign, and the value in double + quotes. -/ +def printAttrs : List (List Char × List Char) → List Char + | [] => [] + | (k, v) :: rest => + ' ' :: k ++ ('=' :: '"' :: (escapeAttr v ++ '"' :: printAttrs rest)) + +mutual +/-- The canonical printed form of a node. An element with no + content prints in the short form. A processing instruction with + no data prints with no space before the closing marks. -/ +def printNode : Node → List Char + | .text cs => escapeText cs + | .elem name attrs content => printElem name attrs content + | .comment cs => '<' :: '!' :: '-' :: '-' :: (cs ++ '-' :: '-' :: '>' :: []) + | .pi t d => + '<' :: '?' :: + (t ++ (if d = [] then ['?', '>'] else ' ' :: d ++ ['?', '>'])) + +/-- An element in its printed form: the start tag, then the + content and the end tag, or the short form when the content is + empty. -/ +def printElem (name : List Char) (attrs : List (List Char × List Char)) + (content : List Node) : List Char := + '<' :: (name ++ printAttrs attrs ++ + (if content = [] then ['/', '>'] + else '>' :: (printNodes content ++ '<' :: '/' :: (name ++ ['>'])))) + +/-- A list of nodes in its printed form, one after another. -/ +def printNodes : List Node → List Char + | [] => [] + | n :: ns => printNode n ++ printNodes ns +end + +/-- A document in its printed form. -/ +def print (d : Document) : List Char := + printNodes d.prolog ++ printNode d.root ++ printNodes d.epilog + +/-! ## Well formed trees -/ + +/-- Attribute lists the printer can write and the parser reads + back: each name is a valid name, each value holds only legal + characters, no name appears twice, and the rest of the list is + in order. -/ +def AttrsOk : List (List Char × List Char) → Prop + | [] => True + | kv :: rest => + ValidName kv.1 ∧ (∀ c ∈ kv.2, LegalChar c) ∧ + (∀ kv2 ∈ rest, kv2.1 ≠ kv.1) ∧ AttrsOk rest + +mutual +/-- A node the printer can write and the parser reads back as the + same node. A text run is not empty and holds only legal + characters. A comment body has no two dashes in a row, does not + end with a dash, and holds only legal characters. A processing + instruction has a valid target that is not the reserved word, + and data that holds no `?>`, holds only legal characters, and + does not start with whitespace (the printer writes one space + before the data, and the parser skips whitespace there, so a + data value starting with whitespace would lose it). -/ +inductive WFNode : Node → Prop where + | text {cs : List Char} (hne : cs ≠ []) (hlegal : ∀ c ∈ cs, LegalChar c) : + WFNode (.text cs) + | elem {name : List Char} {attrs : List (List Char × List Char)} + {content : List Node} (hname : ValidName name) (hattrs : AttrsOk attrs) + (hcontent : WFNodes content) : WFNode (.elem name attrs content) + | comment {cs : List Char} (hdd : NoDashDash cs) (hde : NotDashEnd cs) + (hlegal : ∀ c ∈ cs, LegalChar c) : WFNode (.comment cs) + | pi {t d : List Char} (hname : ValidName t) (hres : ¬ IsXmlTarget t) + (hq : NoQClose d) (hlegal : ∀ c ∈ d, LegalChar c) + (hstart : d = [] ∨ ∀ c cs, d = c :: cs → ¬ IsWs c) : + WFNode (.pi t d) + +/-- A content list whose nodes are all well formed, with no two + text runs next to each other: the parser merges the character + data between two marks into one run, so a tree with two text + runs side by side would print to a text the parser reads back + as one run. -/ +inductive WFNodes : List Node → Prop where + | nil : WFNodes [] + | cons {n : Node} {ns : List Node} (hn : WFNode n) (hns : WFNodes ns) + (hadj : (∃ cs, n = .text cs) → ∀ cs, ns.head? ≠ some (.text cs)) : + WFNodes (n :: ns) +end + +/-- A node in a prolog or an epilog: a comment or a processing + instruction, and well formed. -/ +def MiscOk (ns : List Node) : Prop := + ∀ n ∈ ns, WFNode n ∧ + ((∃ cs, n = .comment cs) ∨ (∃ t d, n = .pi t d)) + +/-- A document the printer can write and the parser reads back: + prolog and epilog hold only comments and processing + instructions, and the root is an element. -/ +def WF (d : Document) : Prop := + MiscOk d.prolog ∧ WFNode d.root ∧ + (∃ name attrs content, d.root = .elem name attrs content) ∧ + MiscOk d.epilog + +end Xml diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..5b8a3ba --- /dev/null +++ b/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.3.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "xml", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/lakefile.toml b/lakefile.toml new file mode 100644 index 0000000..685b22c --- /dev/null +++ b/lakefile.toml @@ -0,0 +1,13 @@ +name = "xml" +version = "0.1.0" +defaultTargets = ["Xml", "Proofs", "xml"] + +[[lean_lib]] +name = "Xml" + +[[lean_lib]] +name = "Proofs" + +[[lean_exe]] +name = "xml" +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..cfe0ecd --- /dev/null +++ b/tests/TEST-RESULTS.md @@ -0,0 +1,20 @@ +# Test results + +Written by `tests/run_tests.py`. Rerun it to check these numbers. + +- Oracle: Python 3.12.3 `xml.etree.ElementTree` (expat), subset mode as described in the harness +- Lean tool: Lean (version 4.35.0, x86_64-unknown-linux-gnu, commit eb6cafb7290e8bd5f2937522d8d804f58f02bafc, Release) +- Seed: 20261026 +- Fixed cases passed: 35 of 35 +- Generated in-subset documents: 3200 +- Generated documents where the tool's canonical print matches the tree and ElementTree agrees on the tree: 3200 +- ElementTree tree agreements on generated documents: 3200 +- Named rejections rejected by the tool: 43 of 43 +- Out of subset disagreements (ElementTree accepts, this slice rejects, by design): 4 + - document type declaration + - document type declaration with internal subset + - colon in an attribute name + - the XML declaration form +- Malformed requests answered error: 10 of 10 +- Bare parse requests answered none: yes +- Failures: 0 diff --git a/tests/run_tests.py b/tests/run_tests.py new file mode 100644 index 0000000..001121f --- /dev/null +++ b/tests/run_tests.py @@ -0,0 +1,745 @@ +#!/usr/bin/env python3 +"""Tests for the Lean XML safe-subset parser and printer. + +Three parts. + +1. Fixed cases: hand written documents covering each feature of + the subset (nesting, both quote forms, empty elements in both + spellings, attribute references and tab normalization, text + with the five entities and numeric references in both bases, + CDATA holding markup-like text, comments in the prolog, the + content, and the epilog, processing instructions, mixed + content). For each, the Lean answer must be the canonical + print written here. + +2. A differential run against Python's `xml.etree.ElementTree`, + with a recorded seed. Random documents inside the subset are + built as trees in Python, then spelled in XML with random + choices that do not change the tree: quote choice, CDATA + spellings of text, entity and character reference spellings, + the two empty element spellings, literal whitespace in + attribute values (which the subset normalizes to a space). + For every document: + + - the Lean tool must accept it, and its canonical print must + equal the canonical print computed in Python from the tree; + - ElementTree must accept it, and the tree ElementTree reads + (for the root element; ElementTree does not keep the prolog + and epilog) must equal the tree that was generated. + + Named differences, counted apart and not failures: + + - ElementTree normalizes a literal carriage return in text, + comments, processing instruction data, and CDATA to a line + feed (XML line ending normalization). This slice keeps the + carriage return as it is; it is a stated boundary in + SPEC.md. The generator therefore never writes a literal + carriage return in those positions (a carriage return in a + tree is always spelled as a character reference there). + Literal carriage returns and tabs in attribute values are + fine: both sides read them as a space. + +3. Named rejections: one input per rejection rule in SPEC.md. + The Lean tool must reject every one. ElementTree agrees with + most of them; where ElementTree accepts (a document type + declaration, a colon in a name, the XML declaration form), + that is an out of subset disagreement, counted apart, because + the subset is narrower than XML by design. + +Malformed request lines must be answered `error`, as in the +other slices' harnesses. + + python3 tests/run_tests.py [--seed N] [--count N] + +The tool is built first if needed, driven in batches of request +lines, and the results are written to tests/TEST-RESULTS.md. +The exit code is non-zero if any check fails. Python 3.11+. +""" + +import argparse +import random +import subprocess +import sys +import xml.etree.ElementTree as ET +from pathlib import Path + +ROOT = Path(__file__).resolve().parent.parent +EXE = ROOT / ".lake" / "build" / "bin" / "xml" +RESULTS = ROOT / "tests" / "TEST-RESULTS.md" +TIMEOUT = 900 +BUILD_TIMEOUT = 3600 +CHUNK = 2000 + +SEED_DEFAULT = 20261026 +COUNT_DEFAULT = 3200 + + +# ---------------------------------------------------------------- +# The tree model, mirroring Xml/Value.lean. +# +# A node is one of: +# ("text", s) +# ("elem", name, [(attr, value), ...], [node, ...]) +# ("comment", s) +# ("pi", target, data) +# A document is (prolog, root, epilog) with prolog and epilog +# lists of comment and pi nodes. + + +def escape_text(s): + out = [] + for c in s: + if c == "&": + out.append("&") + elif c == "<": + out.append("<") + elif c == ">": + out.append(">") + elif c == "\r": + out.append(" ") + else: + out.append(c) + return "".join(out) + + +def escape_attr(s): + out = [] + for c in s: + if c == "&": + out.append("&") + elif c == "<": + out.append("<") + elif c == '"': + out.append(""") + elif c == "\t": + out.append(" ") + elif c == "\n": + out.append(" ") + elif c == "\r": + out.append(" ") + else: + out.append(c) + return "".join(out) + + +def print_node(n): + kind = n[0] + if kind == "text": + return escape_text(n[1]) + if kind == "comment": + return "" + if kind == "pi": + if n[2] == "": + return "" + return "" + _, name, attrs, content = n + parts = ["<" + name] + for k, v in attrs: + parts.append(" " + k + '="' + escape_attr(v) + '"') + if not content: + parts.append("/>") + else: + parts.append(">") + for c in content: + parts.append(print_node(c)) + parts.append("") + return "".join(parts) + + +def print_doc(doc): + prolog, root, epilog = doc + return ("".join(print_node(n) for n in prolog) + + print_node(root) + + "".join(print_node(n) for n in epilog)) + + +# ---------------------------------------------------------------- +# ElementTree reading, converted to the model. Only the root +# element is compared: ElementTree drops the prolog and epilog. + + +def et_to_model(elem): + if elem.tag is ET.Comment: + return ("comment", elem.text or "") + if elem.tag is ET.ProcessingInstruction: + text = elem.text or "" + if " " in text: + target, data = text.split(" ", 1) + else: + target, data = text, "" + return ("pi", target, data) + content = [] + if elem.text: + content.append(("text", elem.text)) + for child in elem: + content.append(et_to_model(child)) + if child.tail: + content.append(("text", child.tail)) + return ("elem", elem.tag, list(elem.attrib.items()), content) + + +def et_parse(text): + builder = ET.TreeBuilder(insert_comments=True, insert_pis=True) + return ET.fromstring(text, parser=ET.XMLParser(target=builder)) + + +# ---------------------------------------------------------------- +# The tool driver: one request per line, character codes. + + +def codes(text): + return ",".join(str(ord(c)) for c in text) + + +def request(text): + return "parse " + codes(text) + + +def run_tool(lines, timeout=TIMEOUT): + proc = subprocess.Popen( + [str(EXE)], stdin=subprocess.PIPE, stdout=subprocess.PIPE, + stderr=subprocess.PIPE) + try: + out, _ = proc.communicate( + ("\n".join(lines) + "\n").encode(), timeout=timeout) + except subprocess.TimeoutExpired: + proc.kill() + raise + return out.decode().splitlines() + + +def run_requests(texts): + lines = [request(t) for t in texts] + answers = [] + for i in range(0, len(lines), CHUNK): + answers.extend(run_tool(lines[i:i + CHUNK])) + return answers + + +# ---------------------------------------------------------------- +# Fixed cases: (input, expected canonical print). + +FIXED = [ + ("", ""), + ("", ""), + ("x", "x"), + ("deep", "deep"), + ("t", 't'), + ("x", 'x'), + ("x", "x"), + # literal tab and newline in a value read as a space; a + # character reference to a tab stays a tab + ("", ''), + ("", ''), + ("", + ''), + ("<>&'"", "<>&'\""), + ("ABc", "ABc"), + ("éé", "éé"), + ("1 > 0 and 2 < 3", "1 > 0 and 2 < 3"), + (" & z]]>", "x <y> & z"), + ("t1t3", "t1t2t3"), + ("]]>", "]>"), + ("", ""), + ("", ""), + ("", ""), + ("", ""), + ("", ""), + ("", ""), + ("", ""), + ("xyzw", "xyzw"), + ("", ''), + ("x", "x"), + (" ", " "), + ("", ''), + ("text with ] and ]] but no close", + "text with ] and ]] but no close"), + ("<_x.y-z_9/>", "<_x.y-z_9/>"), + ("", ''), + ("\n spaced\n", "\n spaced\n"), + ("", ""), + ("t", + "t"), +] + +# Named rejections: (rule, input). ElementTree's verdict is +# recorded for each; where it accepts, the case is an out of +# subset disagreement, not a failure. +REJECTIONS = [ + ("document type declaration", ""), + ("document type declaration with internal subset", + "]>&e;"), + ("entity declaration door (any other "), + ("undefined entity", " "), + ("undefined entity in an attribute", ""), + ("mismatched tags", ""), + ("mismatched tags, nested", ""), + ("unclosed element", ""), + ("unclosed element after content", ""), + ("a second root element", ""), + ("text before the root", "x"), + ("text after the root", "x"), + ("duplicate attribute", ""), + ("raw < in an attribute value", ""), + ("]]> in text", "x]]>y"), + ("-- inside a comment", ""), + ("comment ending in a dash", ""), + ("surrogate character reference", "�"), + ("zero character reference", "�"), + ("character reference past the last character", + "�"), + ("colon in a name", ""), + ("colon in an attribute name", ""), + ("name starting with a digit", "<1a/>"), + ("attribute name starting with a digit", ""), + ("unquoted attribute value", ""), + ("missing equals", ""), + ("CDATA section in the prolog", ""), + ("CDATA section in the epilog", ""), + ("the XML declaration form", ""), + ("the XML declaration, upper case target", + ""), + ("bare ampersand in text", "a & b"), + ("reference without a semicolon", "&"), + ("empty reference", "&;"), + ("hex reference with no digits", "&#x;"), + ("control character reference", " "), + ("raw control character in text", "x\x0by"), + ("unterminated comment", ""), +] + +MALFORMED = [ + "parse x", + "parse 60,,62", + "parse 60, 62", + "parse -1", + "parse 1114112", + "parse 55296", + "print 60", + "PARSE 60", + "parse 60 62", + "", +] + +# parse with no codes is a plain empty input, not malformed: +# it must answer none (the empty text is not a document). + + +# ---------------------------------------------------------------- +# The generator: random trees in the subset, spelled with random +# choices that do not change the tree. Each generated case is +# (spelling, model document). The model is built alongside the +# spelling, token by token, so that the two always agree: a +# literal tab spelled in an attribute value is a space in the +# model, a character reference to a tab is a tab in the model. + +NAME_START = "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ_" +NAME_CHARS = NAME_START + "0123456789.-" +TEXT_PLAIN = ("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ" + "0123456789 .,;:!?()[]{}+-*/=_%$#@~^|") +COMMENT_WORDS = ["note", "a", "draft-1", "x", "see above", "ok", + "todo: fix", "caf\u00e9", "na\u00efve", "123"] + + +def gen_name(rng): + n = rng.randint(1, 7) + return rng.choice(NAME_START) + "".join( + rng.choice(NAME_CHARS) for _ in range(n - 1)) + + +def spell_text_char(rng, c, emitted): + """One spelling of a text character, and it is never a raw + less sign, a raw ampersand, or a raw greater sign right after + two right brackets.""" + if c == "&": + return "&" + if c == "<": + return "<" + if c == ">": + if rng.random() < 0.5: + return ">" + return ">" + if c == "\r": + return rng.choice([" ", " "]) + if c == "\n" or c == "\t": + return c + r = rng.random() + if r < 0.06: + return "&#%d;" % ord(c) + if r < 0.10: + return "&#x%X;" % ord(c) + return c + + +def gen_text_run(rng): + """A text run: returns (spelling, model text). The spelling + may split the run into plain pieces and CDATA sections; the + model is one merged run.""" + n = rng.randint(1, 14) + chars = [] + for _ in range(n): + r = rng.random() + if r < 0.72: + chars.append(rng.choice(TEXT_PLAIN)) + elif r < 0.78: + chars.append("&") + elif r < 0.84: + chars.append("<") + elif r < 0.90: + chars.append(">") + elif r < 0.94: + chars.append("\r") + elif r < 0.97: + chars.append("'") + else: + chars.append('"') + model = "".join(chars) + # Spell it: choose up to two cut points where a CDATA section + # starts or ends. Inside CDATA everything is literal except + # the model holds no ]]> (it cannot: > after ]] is possible, + # so keep CDATA pieces free of a ] ] > run by construction: + # a CDATA piece may not end with ]] when the next model char + # is >, and may not contain ]]> at all. The generator simply + # avoids CDATA around ] characters. + pieces = [] + i = 0 + emitted = "" + while i < len(chars): + if (rng.random() < 0.3 and chars[i] != "]" + and (i + 1 >= len(chars) or chars[i + 1] != "]")): + j = i + buf = [] + while (j < len(chars) and chars[j] not in "<&" + and chars[j] != "\r" + and not (chars[j] == "]" and j + 1 < len(chars) + and chars[j + 1] == "]")): + buf.append(chars[j]) + j += 1 + if buf and buf[-1] != "]": + pieces.append("") + emitted += "".join(buf) + i = j + continue + sp = spell_text_char(rng, chars[i], emitted) + pieces.append(sp) + emitted += chars[i] + i += 1 + return "".join(pieces), model + + +def gen_attr_value(rng): + """Returns (spelling inside the quotes, model value, quote). + The quote is chosen so a literal quote of the other kind may + appear.""" + quote = rng.choice(['"', "'"]) + toks = [] + model = [] + for _ in range(rng.randint(0, 10)): + r = rng.random() + if r < 0.55: + c = rng.choice(TEXT_PLAIN) + toks.append(c) + model.append(c) + elif r < 0.62: + toks.append("\t") # literal tab: model space + model.append(" ") + elif r < 0.68: + # literal newline: a model space, unless it completes + # a literal CRLF pair, which reads as one space + if not (toks and toks[-1] == "\r"): + model.append(" ") + toks.append("\n") + elif r < 0.72: + toks.append("\r") # literal CR: model space + model.append(" ") + elif r < 0.78: + toks.append(" ") + model.append("\t") + elif r < 0.82: + toks.append(" ") + model.append("\n") + elif r < 0.86: + toks.append(" ") + model.append("\r") + elif r < 0.90: + toks.append("<") + model.append("<") + elif r < 0.93: + toks.append("&") + model.append("&") + elif r < 0.96: + other = "'" if quote == '"' else '"' + toks.append(other) + model.append(other) + else: + toks.append(""" if quote == '"' else "'") + model.append(quote) + return "".join(toks), "".join(model), quote + + +def gen_comment(rng): + words = [rng.choice(COMMENT_WORDS) + for _ in range(rng.randint(0, 4))] + body = " " + " ".join(words) + " " if words else "" + if rng.random() < 0.3: + body = body + "- x " + return "", ("comment", body) + + +def gen_pi(rng): + target = gen_name(rng) + while target.lower() == "xml": + target = gen_name(rng) + if rng.random() < 0.35: + return "", ("pi", target, "") + words = [rng.choice(COMMENT_WORDS) + for _ in range(rng.randint(1, 3))] + data = " ".join(words) + return ("", + ("pi", target, data)) + + +def gen_element(rng, depth): + name = gen_name(rng) + used = set() + attrs = [] + attr_spell = [] + for _ in range(rng.randint(0, 3)): + an = gen_name(rng) + if an in used: + continue + used.add(an) + sp, val, q = gen_attr_value(rng) + attrs.append((an, val)) + eq = rng.choice(["=", " = ", "= ", " ="]) + attr_spell.append(" " + an + eq + q + sp + q) + content = [] + content_spell = [] + if depth < 4: + for _ in range(rng.randint(0, 4)): + r = rng.random() + if r < 0.38: + sub_sp, sub = gen_element(rng, depth + 1) + content.append(sub) + content_spell.append(sub_sp) + elif r < 0.52: + sp, node = gen_comment(rng) + content.append(node) + content_spell.append(sp) + elif r < 0.62: + sp, node = gen_pi(rng) + content.append(node) + content_spell.append(sp) + else: + sp, model = gen_text_run(rng) + if content and content[-1][0] == "text": + content[-1] = ("text", content[-1][1] + model) + else: + content.append(("text", model)) + content_spell.append(sp) + model = ("elem", name, attrs, content) + if not content: + if rng.random() < 0.5: + return "<" + name + "".join(attr_spell) + "/>", model + return ("<" + name + "".join(attr_spell) + ">", + model) + return ("<" + name + "".join(attr_spell) + ">" + + "".join(content_spell) + "", model) + + +def gen_document(rng): + prolog = [] + prolog_spell = [] + for _ in range(rng.randint(0, 2)): + if rng.random() < 0.5: + sp, node = gen_comment(rng) + else: + sp, node = gen_pi(rng) + prolog.append(node) + prolog_spell.append(sp) + root_sp, root = gen_element(rng, 0) + epilog = [] + epilog_spell = [] + for _ in range(rng.randint(0, 2)): + if rng.random() < 0.5: + sp, node = gen_comment(rng) + else: + sp, node = gen_pi(rng) + epilog.append(node) + epilog_spell.append(sp) + text = "".join(prolog_spell) + root_sp + "".join(epilog_spell) + return text, (prolog, root, epilog) + + +# ---------------------------------------------------------------- + + +def build_exe(): + if EXE.exists(): + return + subprocess.run(["lake", "build"], cwd=ROOT, check=True, + timeout=BUILD_TIMEOUT) + + +def lean_version(): + out = subprocess.run(["lean", "--version"], capture_output=True, + text=True, timeout=60, + env={**__import__("os").environ, + "PATH": str(Path.home() / ".elan" / "bin") + + ":" + __import__("os").environ["PATH"]}) + return out.stdout.strip() or "unknown" + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument("--seed", type=int, default=SEED_DEFAULT) + ap.add_argument("--count", type=int, default=COUNT_DEFAULT) + args = ap.parse_args() + rng = random.Random(args.seed) + + build_exe() + failures = [] + + # Part 1: fixed cases. + inputs = [t for t, _ in FIXED] + answers = run_requests(inputs) + fixed_ok = 0 + if len(answers) != len(inputs): + failures.append("fixed: tool gave %d answers for %d requests" + % (len(answers), len(inputs))) + answers += [""] * (len(inputs) - len(answers)) + for (text, expected), ans in zip(FIXED, answers): + want = "ok:" + codes(expected) + if ans == want: + fixed_ok += 1 + else: + failures.append("fixed case %r: got %r, want %r" + % (text, ans, want)) + + # Part 2: generated differential. + gen_inputs = [] + gen_docs = [] + for _ in range(args.count): + text, doc = gen_document(rng) + gen_inputs.append(text) + gen_docs.append(doc) + answers = run_requests(gen_inputs) + gen_ok = 0 + et_ok = 0 + gen_fail = 0 + for text, doc, ans in zip(gen_inputs, gen_docs, answers): + want = "ok:" + codes(print_doc(doc)) + good = True + if ans != want: + good = False + if gen_fail < 10: + failures.append( + "generated: tool answer differs for %r: got %r..." + % (text, ans[:120])) + try: + et_root = et_parse(text) + if et_to_model(et_root) != doc[1]: + good = False + if gen_fail < 10: + failures.append( + "generated: ElementTree tree differs for %r" + % (text,)) + else: + et_ok += 1 + et_canon = et_parse(print_doc(doc)) + if et_to_model(et_canon) != doc[1]: + good = False + if gen_fail < 10: + failures.append( + "generated: ElementTree tree of the print " + "differs for %r" % (text,)) + except ET.ParseError: + good = False + if gen_fail < 10: + failures.append( + "generated: ElementTree rejected in-subset %r" + % (text,)) + if good: + gen_ok += 1 + else: + gen_fail += 1 + + # Part 3: named rejections. Also record ElementTree's verdict + # on each: accepted means an out of subset disagreement. + rej_inputs = [t for _, t in REJECTIONS] + answers = run_requests(rej_inputs) + rej_ok = 0 + oos = [] + for (rule, text), ans in zip(REJECTIONS, answers): + if ans == "none": + rej_ok += 1 + else: + failures.append("rejection %s: tool answered %r for %r" + % (rule, ans, text)) + try: + et_parse(text) + oos.append(rule) + except ET.ParseError: + pass + + # Malformed requests. + bad_answers = run_tool(MALFORMED) + bad_ok = 0 + for line, ans in zip(MALFORMED, bad_answers): + if ans == "error": + bad_ok += 1 + else: + failures.append("malformed %r: got %r, want error" + % (line, ans)) + empty_ans = run_tool(["parse", "parse "]) + if empty_ans != ["none", "none"]: + failures.append("bare 'parse' answered %r, want two nones" + % (empty_ans,)) + + lines = [] + lines.append("# Test results") + lines.append("") + lines.append("Written by `tests/run_tests.py`. Rerun it to " + "check these numbers.") + lines.append("") + lines.append("- Oracle: Python %s `xml.etree.ElementTree` " + "(expat), subset mode as described in the harness" + % sys.version.split()[0]) + lines.append("- Lean tool: %s" % lean_version()) + lines.append("- Seed: %d" % args.seed) + lines.append("- Fixed cases passed: %d of %d" + % (fixed_ok, len(FIXED))) + lines.append("- Generated in-subset documents: %d" % len(gen_inputs)) + lines.append("- Generated documents where the tool's canonical " + "print matches the tree and ElementTree agrees on " + "the tree: %d" % gen_ok) + lines.append("- ElementTree tree agreements on generated " + "documents: %d" % et_ok) + lines.append("- Named rejections rejected by the tool: %d of %d" + % (rej_ok, len(REJECTIONS))) + lines.append("- Out of subset disagreements (ElementTree " + "accepts, this slice rejects, by design): %d" + % len(oos)) + for rule in oos: + lines.append(" - %s" % rule) + lines.append("- Malformed requests answered error: %d of %d" + % (bad_ok, len(MALFORMED))) + lines.append("- Bare parse requests answered none: %s" + % ("yes" if empty_ans == ["none", "none"] else "no")) + lines.append("- Failures: %d" % len(failures)) + for f in failures[:40]: + lines.append(" - %s" % f) + RESULTS.write_text("\n".join(lines) + "\n") + print("\n".join(lines)) + return 1 if failures else 0 + + +if __name__ == "__main__": + sys.exit(main()) From 4875cec609f0247a2b37c778d4cbe59882926736 Mon Sep 17 00:00:00 2001 From: shah Date: Tue, 27 Oct 2026 20:11:31 -0500 Subject: [PATCH 2/2] Add the bar file set: Spec.lean, comparator.json, bar.toml, CI workflow --- .github/workflows/bar.yml | 21 ++++ Proofs.lean | 1 + Proofs/SpecProofs.lean | 102 +++++++++++++++++++ README.md | 205 +++++++++++++++++++++++++++++--------- SPEC.md | 57 +++++++++-- Spec.lean | 115 +++++++++++++++++++++ bar.toml | 52 ++++++++++ comparator.json | 1 + lakefile.toml | 3 + 9 files changed, 500 insertions(+), 57 deletions(-) create mode 100644 .github/workflows/bar.yml create mode 100644 Proofs/SpecProofs.lean create mode 100644 Spec.lean create mode 100644 bar.toml create mode 100644 comparator.json 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/Proofs.lean b/Proofs.lean index 1a31d95..2a0b7e9 100644 --- a/Proofs.lean +++ b/Proofs.lean @@ -1 +1,2 @@ import Proofs.RoundTrip +import Proofs.SpecProofs diff --git a/Proofs/SpecProofs.lean b/Proofs/SpecProofs.lean new file mode 100644 index 0000000..f7af403 --- /dev/null +++ b/Proofs/SpecProofs.lean @@ -0,0 +1,102 @@ +/- + Proofs of the statements in `Spec.lean`, under the same names. + + The round trip is the theorem proved in + `Proofs/RoundTrip.lean`. The refusals are single inputs, + checked in the kernel with `decide +kernel`: no native + evaluation, which the bar forbids. +-/ + +import Xml +import Proofs.RoundTrip + +open Xml + +theorem Spec.parse_print (d : Document) (hwf : WF d) : + parse (print d) = some d := + Xml.Proofs.parse_print d hwf + + +theorem Spec.rejects_doctype : + (parse "".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_undefined_entity : + (parse " ".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_mismatched_tags : + (parse "".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_unclosed_element : + (parse "".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_second_root : + (parse "".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_text_before_root : + (parse "x".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_duplicate_attribute : + (parse "".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_lt_in_attribute : + (parse "".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_cdata_close_in_text : + (parse "x]]>y".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_dashdash_in_comment : + (parse "".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_surrogate_ref : + (parse "�".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_zero_ref : + (parse "�".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_colon_in_name : + (parse "".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_digit_name : + (parse "<1a/>".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_unquoted_attribute : + (parse "".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_cdata_in_prolog : + (parse "".toList).isSome = false := by + decide +kernel + + +theorem Spec.rejects_xml_declaration : + (parse "".toList).isSome = false := by + decide +kernel diff --git a/README.md b/README.md index 86ac722..4e1958d 100644 --- a/README.md +++ b/README.md @@ -1,68 +1,179 @@ # xml: an XML safe-subset parser and printer, with a proved round trip -A parser and printer in Lean for a safe subset of XML 1.0: elements, attributes, text, comments, processing instructions, character references, and CDATA sections, with one root element. There is no document type declaration, no entity declarations, no namespaces, and no XML declaration in the subset; a document with any of those is rejected, not parsed leniently. The printer writes one canonical form. The main claim is proved: printing a well formed document gives a text that parses to the same document. The tests run the parser against Python's `xml.etree.ElementTree` in subset mode; see `tests/TEST-RESULTS.md` for the counts. The full subset rules are in `SPEC.md`. +Status: in-progress + +A parser and printer in Lean for a safe subset of XML 1.0: +elements, attributes, text, comments, processing +instructions, character references, and CDATA sections, +with one root element. There is no document type +declaration, no entity declarations, no namespaces, and +no XML declaration in the subset; a document with any of +those is rejected, not parsed leniently. The definitions +are in `Xml/Value.lean` (the tree type, the printer, and +the well-formedness rules) and `Xml/Parse.lean` (the +parser). The proofs are in `Proofs/RoundTrip.lean`. The +full subset rules are in `SPEC.md`. + +The statements a reviewer approves are in `Spec.lean`, +with their proofs in `Proofs/SpecProofs.lean`. No reviewer +has approved them yet, so this project is not called +verified. + +## How to run it + +Needs Linux and [elan](https://github.com/leanprover/elan). +`lake build` builds the library, the proofs, and the +command line tool. The tool reads one request per line: +the word `parse`, a space, and the text as +comma-separated decimal character codes. It answers +`ok:` and the character codes of the canonical print +when the text parses, `none` when it is rejected, and +`error` when the request itself is malformed. -Status: in progress. The specification has not yet been approved by a reviewer apart from its author, and no statement file (`Spec.lean`) has been added by a reviewer, so this is not verified. +``` +echo "parse 60,97,47,62" | .lake/build/bin/xml +``` + +That request is the text ``, and the answer is +`ok:60,97,47,62`. See `SPEC.md` for the full protocol. + +`python3 tests/run_tests.py` rebuilds the tool if needed, +runs the fixed cases, and runs the differential tests +against Python's `xml.etree.ElementTree` in subset mode +with a fixed seed, writing the counts to +`tests/TEST-RESULTS.md`. ## What is proved -The definitions are in `Xml/Value.lean` (the tree type, the printer, and the well-formedness rules) and `Xml/Parse.lean` (the parser). The proofs are in `Proofs/RoundTrip.lean`. +Each claim below names the theorem behind it. The +theorems are stated in `Spec.lean` (the challenge file, +where they end in `sorry`) and proved in +`Proofs/SpecProofs.lean`, under the same names. +`comparator.json` lists all of them. | Claim | Theorem | |-------|---------| -| Parsing the printed form of a well formed document gives the document back. | `Xml.Proofs.parse_print` | -| The same for one element and for a list of content nodes, proved together by strong induction on the length of the printed form. | `Xml.Proofs.elem_nodes` | -| The same for a prolog or epilog list of comments and processing instructions. | `Xml.Proofs.parseMisc_print` | -| Reading back a printed comment body gives the body back. | `Xml.Proofs.parseCommentBody_print` | -| Reading back a printed processing instruction gives the instruction back. | `Xml.Proofs.parsePI_print` | -| Reading back escaped text and escaped attribute values gives the characters back. | `Xml.Proofs.parseCharData_escapeText`, `Xml.Proofs.parseAttrValue_escapeAttr` | - -A document is well formed when its names match the subset's name rule, attribute names are unique per element, text holds only legal XML characters and no two text runs stand next to each other, comment bodies contain no `--` and do not end with `-`, processing instruction targets are valid and not the reserved word `xml`, and the prolog and epilog hold only comments and processing instructions. `SPEC.md` states the rules in full. `parse_print` checks against the standard axioms only (`propext`, `Classical.choice`, `Quot.sound`), which a reader can confirm with `#print axioms Xml.Proofs.parse_print`. - -The command-line tool in `Main.lean` calls these functions directly. +| Parsing the printed form of a well formed document gives the document back. | `Spec.parse_print` | +| A document carrying a document type declaration is refused. | `Spec.rejects_doctype` | +| A reference to an entity the subset does not define is refused. | `Spec.rejects_undefined_entity` | +| An end tag that does not match the start tag is refused. | `Spec.rejects_mismatched_tags` | +| An element with no end tag is refused. | `Spec.rejects_unclosed_element` | +| A second root element is refused. | `Spec.rejects_second_root` | +| Character data before the root element is refused. | `Spec.rejects_text_before_root` | +| An attribute name standing twice on one element is refused. | `Spec.rejects_duplicate_attribute` | +| A raw less sign inside an attribute value is refused. | `Spec.rejects_lt_in_attribute` | +| The run `]]>` inside text is refused. | `Spec.rejects_cdata_close_in_text` | +| Two dashes in a row inside a comment body are refused. | `Spec.rejects_dashdash_in_comment` | +| A character reference naming a surrogate value is refused. | `Spec.rejects_surrogate_ref` | +| A character reference naming zero is refused. | `Spec.rejects_zero_ref` | +| A colon in a name is refused. | `Spec.rejects_colon_in_name` | +| A name starting with a digit is refused. | `Spec.rejects_digit_name` | +| An attribute value with no quotes is refused. | `Spec.rejects_unquoted_attribute` | +| A CDATA section in the prolog is refused. | `Spec.rejects_cdata_in_prolog` | +| The XML declaration form is refused. | `Spec.rejects_xml_declaration` | + +A document is well formed when its names match the +subset's name rule, attribute names are unique per +element, text holds only legal XML characters and no two +text runs stand next to each other, comment bodies +contain no `--` and do not end with `-`, processing +instruction targets are valid and not the reserved word +`xml`, and the prolog and epilog hold only comments and +processing instructions. `SPEC.md` states the rules in +full. + +The round trip theorem rests on the proof in +`Proofs/RoundTrip.lean`, where it is +`Xml.Proofs.parse_print`. It uses no axiom but the three +standard ones (`propext`, `Classical.choice`, +`Quot.sound`): `comparator.json` names those three as the +permitted axioms, and `lake comparator` checks each proof +in `Proofs/SpecProofs.lean` against its statement in +`Spec.lean` and against that list. The refusal theorems +are single inputs checked in the kernel with +`decide +kernel`. + +The command line tool in `Main.lean` calls `Xml.parse` +and `Xml.print` directly, the same functions the theorems +are about. ## What is not proved -- That the parser accepts every text the subset allows, and rejects every text it forbids. The round trip does not need either, so neither is proved. The differential tests check that behaviour instead, and the results file records the outcome, including any failure. -- Anything about documents outside the subset: documents with a document type declaration, entities beyond the five predefined ones, namespaces, an XML declaration, or non-ASCII names. The parser rejects them; whether a full XML parser would accept them is not a claim here. -- Reading requests and printing answers in `Main.lean`: splitting lines, the decimal parser, and the check that a code is a Unicode scalar value. The tests cover them, malformed requests included. -- Speed. The code works on lists of characters, which suits proofs, not large data. The parser's fuel is the length of the input text, which very deep inputs can reach. +- That the parser accepts every text the subset allows, + and rejects every text it forbids. The round trip does + not need either, and the refusal theorems pin single + inputs only, so neither holds in general as a proof. + The differential tests check that behaviour instead, + and the results file records the outcome, including any + failure. +- Anything about documents outside the subset: documents + with a document type declaration, entities beyond the + five predefined ones, namespaces, an XML declaration, + or non-ASCII names. The parser rejects them; whether a + full XML parser would accept them is not a claim here. +- Reading requests and printing answers in `Main.lean`: + splitting lines, the decimal parser, and the check that + a code is a Unicode scalar value. The tests cover them, + malformed requests included. +- Speed. The code works on lists of characters, which + suits proofs, not large data. The parser's fuel is the + length of the input text, which very deep inputs can + reach. Three deliberate choices, also stated in `SPEC.md`: -- CDATA sections are a spelling, not a tree difference. CDATA content becomes ordinary character data in the same text node stream, and the printer never writes a CDATA section. The claim is at tree level, so this is sound. -- There is no line ending normalization in text, comments, processing instruction data, or CDATA: a literal carriage return reads as itself. Full XML normalizes it to a line feed. Inside attribute values both readings agree (either form reads as a space), and the printer always writes a carriage return as a character reference. -- The XML declaration is not in the model. A processing instruction target of `xml` in any letter case rejects everywhere, which keeps the declaration out. +- CDATA sections are a spelling, not a tree difference. + CDATA content becomes ordinary character data in the + same text node stream, and the printer never writes a + CDATA section. The claim is at tree level, so this is + sound. +- There is no line ending normalization in text, + comments, processing instruction data, or CDATA: a + literal carriage return reads as itself. Full XML + normalizes it to a line feed. Inside attribute values + both readings agree (either form reads as a space), and + the printer always writes a carriage return as a + character reference. +- The XML declaration is not in the model. A processing + instruction target of `xml` in any letter case rejects + everywhere, which keeps the declaration out. ## What you must trust -- The Lean kernel, which checks the proofs. -- The Lean compiler, with the C compiler and linker shipped with it, and the runtime, which turn the proved definitions into the program that runs. -- Lean's core library, including the compiled code it puts in place of some definitions the proofs reason about. -- The operating system and hardware it runs on. -- Python's standard library, as the oracle in the differential tests. The results file names the version used. The plan also names Go's encoding/xml and Rust's quick-xml as oracles; neither is wired in yet, and the harness says so rather than counting them. - -This project has no dependencies beyond Lean itself. - -## Run it - -Needs Linux and [elan](https://github.com/leanprover/elan). Build, then feed request lines to the tool: - -``` -lake build -echo "parse 60,97,47,62" | .lake/build/bin/xml -``` - -That request is the text `` as character codes, and the answer is `ok:60,97,47,62`. A text the parser rejects, such as the single code `120` (the letter `x`), answers `none`. A malformed request answers `error`. See `SPEC.md` for the full protocol. +- The Lean kernel (Lean 4.35.0, pinned in + `lean-toolchain`), which checks every proof. +- The Lean compiler, which turns the proved definitions + into the program that runs. +- The Lean runtime, which runs that program. +- The hardware the program runs on. +- Every dependency in `lake-manifest.json`: the manifest + lists no packages, so there are no library dependencies + to trust beyond the Lean toolchain itself. +- That `SPEC.md` states the reading of XML 1.0 you + intend. The proofs are about the parser and printer in + this repo following each other exactly; the fidelity of + the spec to XML 1.0 is a reading, pinned in SPEC.md + where the standard leaves a choice open. +- Python's standard library, as the oracle in the + differential tests. The results file names the version + used. The plan also names Go's encoding/xml and Rust's + quick-xml as oracles; neither is wired in yet, and the + harness says so rather than counting them. +- There are no exceptions to item 4 of the bar: the + project uses none of the features it forbids. ## Re-check it -Needs Linux, elan, and Python 3.11 or later. - -``` -lake build -grep -rn "sorry" --include="*.lean" Xml Proofs Main.lean Xml.lean Proofs.lean -python3 tests/run_tests.py -``` - -The grep should print nothing: there is no `sorry` anywhere. The test script rebuilds the tool if needed, runs the fixed cases, runs the differential tests against Python's `xml.etree.ElementTree` with a fixed seed, and writes the counts to `tests/TEST-RESULTS.md`. +1. `lake comparator --paranoid`: builds the challenge + file `Spec.lean` and the proofs in a sandbox and + checks that each theorem named in `comparator.json` + proves exactly the statement in the challenge file, + uses no axiom but the three standard ones, and is + accepted by Lean's kernel and every other kernel + shipped with Lean. +2. `python3 tests/run_tests.py`: the fixed cases, the + named rejections, and the differential run against + Python's `xml.etree.ElementTree`, with counts and any + failures written to `tests/TEST-RESULTS.md`. +3. `lake build`: the library, the proofs, and the tool + build clean. diff --git a/SPEC.md b/SPEC.md index 2f71396..e3f5956 100644 --- a/SPEC.md +++ b/SPEC.md @@ -2,8 +2,8 @@ A parser and printer in Lean for a safe subset of XML 1.0 (Fifth Edition), narrowed as stated here. A reviewer who did not write -this specification approves it, together with any statement file -a reviewer adds later. No such file exists yet, so nothing here +this specification approves it, together with the statement file +`Spec.lean`. No reviewer has approved them yet, so nothing here counts toward the verified bar yet. Text is `List Char`. A Lean `Char` is one Unicode scalar value. @@ -175,14 +175,51 @@ formedness predicate (`WF` in `Xml/Value.lean`): - the root is an element, and the prolog and epilog hold only comments and processing instructions. -## The claim - -Printing a well formed document gives a text that parses to -the same document: `parse (print d) = some d`. The theorem is -`Xml.Proofs.parse_print`. It checks against the standard axioms -only (`propext`, `Classical.choice`, `Quot.sound`), which a -reader can confirm with `#print axioms -Xml.Proofs.parse_print`. +## Properties and their theorems + +Each property a reader can check in the page (`README.md`) +names its theorem. The theorems are stated in `Spec.lean` +and proved in `Proofs/SpecProofs.lean`. The refusal +theorems are single inputs; the tests in `tests/` cover +each rule on many more inputs. + +| Property | Theorem | +|----------|---------| +| Parsing the printed form of a well formed document gives the document back | `Spec.parse_print` | +| A document carrying a document type declaration is refused | `Spec.rejects_doctype` | +| A reference to an entity the subset does not define is refused | `Spec.rejects_undefined_entity` | +| An end tag that does not match the start tag is refused | `Spec.rejects_mismatched_tags` | +| An element with no end tag is refused | `Spec.rejects_unclosed_element` | +| A second root element is refused | `Spec.rejects_second_root` | +| Character data before the root element is refused | `Spec.rejects_text_before_root` | +| An attribute name standing twice on one element is refused | `Spec.rejects_duplicate_attribute` | +| A raw less sign inside an attribute value is refused | `Spec.rejects_lt_in_attribute` | +| The run `]]>` inside text is refused | `Spec.rejects_cdata_close_in_text` | +| Two dashes in a row inside a comment body are refused | `Spec.rejects_dashdash_in_comment` | +| A character reference naming a surrogate value is refused | `Spec.rejects_surrogate_ref` | +| A character reference naming zero is refused | `Spec.rejects_zero_ref` | +| A colon in a name is refused | `Spec.rejects_colon_in_name` | +| A name starting with a digit is refused | `Spec.rejects_digit_name` | +| An attribute value with no quotes is refused | `Spec.rejects_unquoted_attribute` | +| A CDATA section in the prolog is refused | `Spec.rejects_cdata_in_prolog` | +| The XML declaration form is refused | `Spec.rejects_xml_declaration` | + +The round trip behind `Spec.parse_print` is +`Xml.Proofs.parse_print` in `Proofs/RoundTrip.lean`. Its +proofs rest on helper round trips proved in the same file: +one element and a list of content nodes together +(`Xml.Proofs.elem_nodes`), a prolog or epilog list +(`Xml.Proofs.parseMisc_print`), a printed comment body +(`Xml.Proofs.parseCommentBody_print`), a printed +processing instruction (`Xml.Proofs.parsePI_print`), and +escaped text and attribute values read back +(`Xml.Proofs.parseCharData_escapeText`, +`Xml.Proofs.parseAttrValue_escapeAttr`). Each proof in +`Proofs/SpecProofs.lean` uses no axiom but the three +standard ones (`propext`, `Classical.choice`, +`Quot.sound`): `comparator.json` names those three as the +permitted axioms, and `lake comparator` checks the proofs +against that list. ## Boundaries and named differences diff --git a/Spec.lean b/Spec.lean new file mode 100644 index 0000000..86070d4 --- /dev/null +++ b/Spec.lean @@ -0,0 +1,115 @@ +/- + The specification as Lean statements: the challenge file. + + A reviewer who did not write this file approves it, and `bar.toml` + records the SHA-256 it had then. The proofs live in `Proofs` + (`Proofs/SpecProofs.lean`); `lake comparator` checks that each one + proves exactly the statement written here. The `sorry` below is + expected in this file only. + + The statements use only the definitions in `Xml/Value.lean` and + `Xml/Parse.lean`, the code under proof named in `bar.toml`. No + definition of their own is needed, so this project has no + `Spec/Defs.lean`. +-/ + +import Xml + +open Xml + +/-! ## The round trip + +The statement the slice stands on. It is the statement of the +proved theorem of the same shape in `Proofs/RoundTrip.lean`, over +the same well formedness predicate, `Xml.WF`. -/ + +/-- Parsing the printed form of a well formed document gives the + document back. So a printer that wrote nothing, or wrote + something shorter, fails this statement. -/ +theorem Spec.parse_print (d : Document) (hwf : WF d) : + parse (print d) = some d := sorry + +/-! ## Refused inputs + +Single inputs the parser refuses, one for each headline rule of +`SPEC.md`. Each input is one of the named rejection cases in the +test harness. The differential tests cover these rules on many +more inputs; these statements pin them so a reader of the +specification can check each rule against one concrete case. -/ + +/-- A document carrying a document type declaration is refused, + not read leniently. -/ +theorem Spec.rejects_doctype : + (parse "".toList).isSome = false := sorry + +/-- A reference to an entity the subset does not define is + refused: no entity is ever expanded, because none exist. -/ +theorem Spec.rejects_undefined_entity : + (parse " ".toList).isSome = false := sorry + +/-- An end tag that does not match the start tag is refused. -/ +theorem Spec.rejects_mismatched_tags : + (parse "".toList).isSome = false := sorry + +/-- An element with no end tag is refused. -/ +theorem Spec.rejects_unclosed_element : + (parse "".toList).isSome = false := sorry + +/-- A document has one root element; a second one is refused. -/ +theorem Spec.rejects_second_root : + (parse "".toList).isSome = false := sorry + +/-- Character data before the root element is refused. -/ +theorem Spec.rejects_text_before_root : + (parse "x".toList).isSome = false := sorry + +/-- An attribute name standing twice on one element is refused. -/ +theorem Spec.rejects_duplicate_attribute : + (parse "".toList).isSome = false := sorry + +/-- A raw less sign inside an attribute value is refused. -/ +theorem Spec.rejects_lt_in_attribute : + (parse "".toList).isSome = false := sorry + +/-- The run `]]>` inside text is refused, as XML requires + outside a CDATA section. -/ +theorem Spec.rejects_cdata_close_in_text : + (parse "x]]>y".toList).isSome = false := sorry + +/-- Two dashes in a row inside a comment body are refused. -/ +theorem Spec.rejects_dashdash_in_comment : + (parse "".toList).isSome = false := sorry + +/-- A character reference naming a surrogate value is refused: + a surrogate is not a legal XML character. -/ +theorem Spec.rejects_surrogate_ref : + (parse "�".toList).isSome = false := sorry + +/-- A character reference naming zero is refused: zero is not a + legal XML character. -/ +theorem Spec.rejects_zero_ref : + (parse "�".toList).isSome = false := sorry + +/-- A colon in a name is refused: in XML a colon signals + namespace use, and namespaces are out of this subset. -/ +theorem Spec.rejects_colon_in_name : + (parse "".toList).isSome = false := sorry + +/-- A name starting with a digit is refused. -/ +theorem Spec.rejects_digit_name : + (parse "<1a/>".toList).isSome = false := sorry + +/-- An attribute value with no quotes is refused. -/ +theorem Spec.rejects_unquoted_attribute : + (parse "".toList).isSome = false := sorry + +/-- A CDATA section in the prolog is refused: CDATA stands in + element content only. -/ +theorem Spec.rejects_cdata_in_prolog : + (parse "".toList).isSome = false := sorry + +/-- The XML declaration form is refused: the declaration is not + part of this subset, and a target of `xml` rejects + everywhere. -/ +theorem Spec.rejects_xml_declaration : + (parse "".toList).isSome = false := sorry diff --git a/bar.toml b/bar.toml new file mode 100644 index 0000000..16aab56 --- /dev/null +++ b/bar.toml @@ -0,0 +1,52 @@ +# Read by bar/check.py in Proven-Commons/mission. +# See playbook/verified-bar.md there for what each field means. + +[project] +name = "xml" +# "in-progress" until every bar item passes, then "verified". +status = "in-progress" +page = "README.md" +# GitHub handles of everyone who wrote the specification. +spec_authors = ["abu-aska"] +# The program people run. A change to it voids the approval. +entry_points = ["Main.lean"] + +[spec] +files = ["SPEC.md", "Spec.lean"] +# The code under proof: the functions the statements are about. +code = [ + # The data types the statements are about, and their constructors. + "Xml.Node", "Xml.Node.text", "Xml.Node.elem", "Xml.Node.comment", + "Xml.Node.pi", "Xml.Document", + # Characters, names, and the conditions a well formed tree meets. + "Xml.LegalChar", "Xml.isLegalChar", "Xml.IsNameStart", "Xml.IsNameChar", + "Xml.isNameStart", "Xml.isNameChar", "Xml.ValidName", "Xml.IsWs", + "Xml.NoDashDash", "Xml.NotDashEnd", "Xml.NoQClose", "Xml.IsXmlTarget", + "Xml.AttrsOk", "Xml.WFNode", "Xml.WFNode.text", "Xml.WFNode.elem", + "Xml.WFNode.comment", "Xml.WFNode.pi", "Xml.WFNodes", "Xml.WFNodes.nil", + "Xml.WFNodes.cons", "Xml.MiscOk", "Xml.WF", + # The printer. + "Xml.escapeTextChar", "Xml.escapeText", "Xml.escapeAttrChar", + "Xml.escapeAttr", "Xml.printAttrs", "Xml.printNode", "Xml.printElem", + "Xml.printNodes", "Xml.print", + # The parser helpers and the parser. + "Xml.isWs", "Xml.skipWs", "Xml.isDigit", "Xml.hexVal", "Xml.isHexDigit", + "Xml.takeDigits", "Xml.takeHexDigits", "Xml.digitsValue", + "Xml.charRefChar", "Xml.parseRef", "Xml.takeNameChars", "Xml.parseName", + "Xml.parseTextRun", "Xml.parseCDATABody", "Xml.parseCommentBody", + "Xml.parsePIData", "Xml.parseAttrValue", "Xml.parsePI", + "Xml.parseCharData", "Xml.parseAttrs", "Xml.parseElement", + "Xml.parseNodes", "Xml.parseMisc", "Xml.parseDocument", "Xml.parse", +] + +# 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/xml/pull/" + +[tests] +results = "tests/TEST-RESULTS.md" +command = "python3 tests/run_tests.py" +files = ["tests/run_tests.py"] diff --git a/comparator.json b/comparator.json new file mode 100644 index 0000000..3837303 --- /dev/null +++ b/comparator.json @@ -0,0 +1 @@ +{"challenge_module":"Spec","permitted_axioms":["propext","Classical.choice","Quot.sound"],"solution_module":"Proofs","theorem_names":["Spec.parse_print","Spec.rejects_doctype","Spec.rejects_undefined_entity","Spec.rejects_mismatched_tags","Spec.rejects_unclosed_element","Spec.rejects_second_root","Spec.rejects_text_before_root","Spec.rejects_duplicate_attribute","Spec.rejects_lt_in_attribute","Spec.rejects_cdata_close_in_text","Spec.rejects_dashdash_in_comment","Spec.rejects_surrogate_ref","Spec.rejects_zero_ref","Spec.rejects_colon_in_name","Spec.rejects_digit_name","Spec.rejects_unquoted_attribute","Spec.rejects_cdata_in_prolog","Spec.rejects_xml_declaration"]} \ No newline at end of file diff --git a/lakefile.toml b/lakefile.toml index 685b22c..66452b8 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -8,6 +8,9 @@ name = "Xml" [[lean_lib]] name = "Proofs" +[[lean_lib]] +name = "Spec" + [[lean_exe]] name = "xml" root = "Main"