diff --git a/.github/workflows/bar.yml b/.github/workflows/bar.yml
new file mode 100644
index 0000000..32457ed
--- /dev/null
+++ b/.github/workflows/bar.yml
@@ -0,0 +1,21 @@
+name: verified bar
+
+on:
+ push:
+ pull_request:
+ # Rerun when the spec reviewer approves, or an approval is dismissed.
+ pull_request_review:
+ types: [submitted, dismissed]
+
+jobs:
+ bar:
+ # pull-requests: read lets the check confirm the spec approval on GitHub.
+ permissions:
+ contents: read
+ pull-requests: read
+ # Both lines pin the same commit of Proven-Commons/mission: bar v2, as
+ # proposed in its pull request #2. Move both to a release tag once
+ # mission publishes one.
+ uses: Proven-Commons/mission/.github/workflows/verified-bar.yml@6ba85c27abaaf07905c9316aa96dc29f7b5847a2
+ with:
+ bar-ref: 6ba85c27abaaf07905c9316aa96dc29f7b5847a2
diff --git a/.gitignore b/.gitignore
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..2a0b7e9
--- /dev/null
+++ b/Proofs.lean
@@ -0,0 +1,2 @@
+import Proofs.RoundTrip
+import Proofs.SpecProofs
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/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 2a9ab1d..4e1958d 100644
--- a/README.md
+++ b/README.md
@@ -1,32 +1,179 @@
-# 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.
+Status: in-progress
-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.
+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`.
-## First slice
+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.
-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.
+## How to run it
-## Main claim
+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.
-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.
+```
+echo "parse 60,97,47,62" | .lake/build/bin/xml
+```
-## Test oracles
+That request is the text ``, and the answer is
+`ok:60,97,47,62`. See `SPEC.md` for the full protocol.
-- 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.
+`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`.
-## Score
+## What is proved
-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.
+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.
-## What is not in this slice
+| Claim | 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` |
-- Document type declarations.
-- Entities.
-- Namespaces.
-- Full XML 1.0.
+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.
-## Layout, when the first slice lands
+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 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.
+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, 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.
+
+## What you must trust
+
+- 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
+
+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
new file mode 100644
index 0000000..e3f5956
--- /dev/null
+++ b/SPEC.md
@@ -0,0 +1,261 @@
+# 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 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.
+
+## 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.
+
+## 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
+
+- 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/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/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/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/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..66452b8
--- /dev/null
+++ b/lakefile.toml
@@ -0,0 +1,16 @@
+name = "xml"
+version = "0.1.0"
+defaultTargets = ["Xml", "Proofs", "xml"]
+
+[[lean_lib]]
+name = "Xml"
+
+[[lean_lib]]
+name = "Proofs"
+
+[[lean_lib]]
+name = "Spec"
+
+[[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())