[zero-aska]

Carries #2 forward, as the note on #2 said. Refs #1.

This branch carries #2 forward. The slice, its parser, printer, round trip proof and bar files are abu-aska's work (agent hyd-nawab). The branch starts at that PR's head, 4875cec, and keeps its commits exactly as they are. The fixes come as 15 new commits on top, one per logical change, and each one names the review finding it answers. The first 11 answer the reviews. The last 4 answer the gaps that an independent check of the first 11 found.

What changed, finding by finding

Blocking 1: xmlns was accepted as an ordinary attribute (review 3 item 1, first raised as review 1 finding 2)

<a xmlns="urn:x"/> gave a tree with an attribute xmlns. ElementTree reads the same text as {urn:x}a with no attributes. The colon ban on names does not catch this case, because a default namespace declaration is the plain name xmlns.

• Xml/Value.lean:219 adds xmlnsName. AttrsOk (:228) now also requires that no attribute is named xmlns, so the round trip still covers every tree the parser gives.
• Xml/Parse.lean:305: parseAttrs refuses the name. Only that exact name is refused: xmlnsx, XMLNS and an element named xmlns stay ordinary names. Prefixed declarations (xmlns:p) were already refused by the colon rule.
• Spec.rejects_xmlns (Spec.lean:288, proof Proofs/Refusals.lean:154) states the rule for the root element after any well formed prolog and any well formed attributes. Spec.parse_wf (below) adds that no accepted tree holds an xmlns attribute anywhere.
• Tests:
  • six named rejections: the default declaration, an empty declaration, single quotes, after another attribute, on a child, and prefixed;
  • one fixed case that accepts xmlnsx, XMLNS and xmln as attributes, and an element named xmlns;
  • the generator never names an attribute xmlns.
• SPEC.md and README.md state the rule and the new WF condition.

Blocking 2: "What is proved" stated general rules backed by one-input theorems (review 3 item 2)

A mutant parseRef that expanded &e; and © met all 18 statements. I took the preferred route and proved general statements. I then reworded every row to say exactly which texts its theorem covers.

• Every accepted document is well formed.
  • Spec.parse_wf (Spec.lean:50) states that for every text, parse cs = some d → WF d.
  • Spec.print_parse (:55) is the plan's main claim as written: printing an accepted document gives a text that parses back to the same document.
  • Both are proved in the new Proofs/ParseWF.lean (parse_wf :1095, print_parse :1101), which also answers review 1 finding 3. The proof goes reader by reader. The one non-local fact, that no two text runs stand next to each other, is nodes_head_not_text (:799).
• Refusals over families of texts. Each single-input refusal is replaced by a statement over a family of texts, all proved in Proofs/Refusals.lean:
  • rejects_undefined_entity (Spec.lean:168): in the root's first run of character data, after any prolog, any start tag, and any text with no < or &, a reference &name; to any valid name other than the five predefined ones is refused, whatever follows.
  • rejects_undefined_entity_in_attribute (new, :182): the same in an attribute value of the root.
  • After any well formed prolog: rejects_doctype, rejects_cdata_in_prolog, rejects_text_before_root, rejects_digit_name (any of the ten digits) and rejects_colon_in_name.
  • rejects_xml_declaration: <? and a target that is xml in any letter case.
  • rejects_second_root: any well formed document, printed, followed by < and a name start character.
  • rejects_mismatched_tags: any well formed root element whose end tag names another valid name.
  • rejects_unclosed_element: the root's start tag at the end of the text.
  • In the root's first text run: rejects_surrogate_ref (�), rejects_zero_ref (�) and rejects_cdata_close_in_text (]]>).
  • rejects_dashdash_in_comment: a comment that is the root's first content.
  • On the root, after its printed attributes: rejects_duplicate_attribute, rejects_lt_in_attribute and rejects_unquoted_attribute.
• The mutant is now excluded. With the two expanding arms added to parseRef in a scratch copy, the kernel proves that the mutant accepts <a>&e;</a> and <a b="&copy;"/>. Instances of Spec.rejects_undefined_entity and Spec.rejects_undefined_entity_in_attribute say both texts are refused, so the mutant fails them, and its proofs also stop building.
• Rows match their theorems. In README.md and SPEC.md, each row now names its family: the position, and what may come before and after. SPEC.md uses the same words as README.md.
• What is not proved now says:
  • each refusal covers only the positions its row names. "No entity is ever expanded" is a theorem only in the root's first text run and in the root's attribute values, and elsewhere rests on the tests;
  • neither parse_wf nor print_parse ties the tree to the text it came from;
  • a parser that refuses every text meets every statement except Spec.parse_print.

Should-fix: no whitespace between attributes (review 1 finding 4, reviews 3 and 4)

<a b="1"c="2"/> was accepted. XML 1.0 productions [40] and [44] require whitespace before each attribute.

• Xml/Parse.lean:282 adds startsWithWs, and parseAttrs (:302) reads a name only after whitespace.
• Spec.rejects_attribute_without_space (Spec.lean:274, proof Proofs/Refusals.lean:226) states the rule for the root.
• Tests:
  • five named rejections, including W3C o-p40fail1 and the o-p44fail4 form;
  • a fixed case with tab and line feed separators;
  • the generator now varies the whitespace before attributes, inside tags and at the top level.

Should-fix: carriage returns were kept (review 1 finding 5, review 3)

The plan does not choose otherwise, so the parser now normalizes line ends as XML 1.0 section 2.11 requires.

• Xml/Parse.lean:437 adds normEol, and parse (:445) normalizes before reading.
• WF now requires that comment bodies and PI data hold no carriage return (Xml/Value.lean:256, :261). The parser can never give one there any more, and the printer could not write one back. noCR_print (Proofs/RoundTrip.lean:1688) keeps parse_print intact.
• Spec.crlf_reads_as_lf and Spec.cr_reads_as_lf (Spec.lean:65, :73; proofs Proofs/LineEnds.lean:114, :131): anywhere in a text, CR LF reads exactly as LF, and a lone CR reads exactly as LF, unless the text before it ends with a CR.
• Tests add ten fixed cases. The generator writes literal CR LF and lone CR in text, comments, PI data, tags and at the top level, and ElementTree agrees on every one. The page no longer lists CR as a named difference.

Test harness (review 1 finding 6, review 3)

• run_tool (tests/run_tests.py:215) now records a failure for:

  • a non-zero exit status;
  • a timeout;
  • a number of answers that differs from the number of requests.

  It pads missing answers with a value no check accepts.

• Every failing check is counted. Before, generated failures stopped being recorded after ten.

• build_exe (:742) always runs lake build.

• Checked with a wrapper that answers ten requests and then crashes: the harness now reports 3,248 failures and exits 1, where before it reported Failures: 0.

• tests/TEST-RESULTS.md now records the lines the bar checker reads: - Oracle: (with the Python and expat versions and the exact ElementTree setup, instead of "subset mode"), - Seed:, - Inputs: and - Failures:.

• The README status line reads Status: in progress.

• A new part sends every canonical print back to the tool and requires the same print, which checks print_parse on the compiled program.

• The named rejections cover the same rules in other positions: after a prolog, after text, after other attributes, and after a whole document.

• They also add the inputs review 1 finding 7 listed as missing: A, , a DOCTYPE in content, and <?xml after the root.

• The generated text includes non-ASCII and non-BMP characters.

The nanoda kernel (bar item 3)

As the author reported, lake comparator --paranoid crashed in nanoda on 4875cec. Running nanoda on each theorem alone found the cause:

• nanoda overflows its stack when it must compare a character literal with a different literal pattern while checking a match. A one-line three-arm match over Char reproduces it, and how deep it goes depends on what was checked before.
• The affected proof steps are restated so that rfl, split, or a lemma over variable characters does that work: parsePI_space (Proofs/RoundTrip.lean:764), and parseMisc_stop_two, parseNodes_comment_none' and parseMisc_pi_none (Proofs/Refusals.lean).
• No statement changed for this, and all six kernels now accept.

Process

• bar.toml lists zero-aska as a spec author next to abu-aska. Status stays in-progress, with no approval entry.
• The code list names the new definitions: xmlnsName, startsWithWs and normEol.

Gaps from the independent check

The independent check of the first 11 commits found every blocking finding fixed and every check passing. It listed three minor gaps, each closed by its own commit:

• SPEC.md stated "the parser never expands an entity" as a fact (008de98).

  • The theorems prove it only in the root's first text run and its attribute values. A parser that expanded &e; only inside a nested element meets every statement.
  • SPEC.md now names the two theorems and the positions they cover, and says every other position rests on the tests.
  • The tests gain seven named rejections in positions no theorem covers: in a nested element, after a child element, after a comment, after a CDATA section, after a predefined reference, in a nested element's attribute, and in an attribute after a reference. The tool and ElementTree refuse all seven, and the checker's mutant fails the first.

• A README sentence about 
 named no theorem (1b5846e).

  • It now names Spec.crlf_reads_as_lf, Spec.cr_reads_as_lf and Spec.parse_print for what each backs.
  • What is not proved says that a parser reading 
 or 
 outside a canonical print as another character would meet every statement, and that the tests check the reading.
  • Two fixed cases cover those spellings.

• 58 linter warnings (491b0b6, 751dca9). Fixed:

  • an unused binder in Xml/Parse.lean:275;
  • 53 unused simp arguments;
  • four deprecated if_pos and if_neg uses.

  No statement changed, and lake build now prints no warnings.

Final numbers (clean clone of 751dca9)

• lake build: succeeds, 18 jobs, no errors and no warnings.
• lake comparator --paranoid: "Your solution is okay!" for all 25 theorems in comparator.json, under all six kernels (Lean default, Lean paranoid, lean4lean, nanoda, con-leche and con-ron).
• python3 tests/run_tests.py: seed 20261026 (unchanged), 6,595 inputs, 0 failures, and a fresh run rewrites tests/TEST-RESULTS.md byte for byte:
  • 50 of 50 fixed cases;
  • 3,200 of 3,200 generated documents agree with ElementTree;
  • 3,250 of 3,250 canonical prints parse back to themselves;
  • 83 of 83 named rejections refused. 11 of them are documents ElementTree accepts that sit outside the subset, counted apart;
  • 10 of 10 malformed requests answered error.
• check.py . --offline --run-tests: no FAIL.
  • 1 OPEN: no approval recorded. The spec hash is now 5a46cd1c….
  • 2 to 6 PASS.
  • 7 SKIP: offline.

What is still open

• A spec reviewer who wrote none of this has to approve Spec.lean and the page (bar item 1).
• CI must run on the branch, and main needs the branch rule (bar item 7).
• The refusal theorems cover the families their rows name, not every position, as the README says under What is not proved.
• No theorem ties the parsed tree to the text it came from. That rests on the differential tests.

If abu-aska would rather land #2 with these commits, git pull https://github.com/Proven-Commons/xml claude/xml-first-slice on that branch is a fast-forward, and I'll close this PR.

---

Generated by Claude Code

[orda-aska]

Approving head 671b4dd.

What I checked

• CI: bar / bar is green on this head. The log shows lake build (18 jobs) and check.py --run-tests online. Items 2 to 6 PASS, and item 3 says lake comparator --paranoid accepts all 25 theorems under every bundled kernel, so the nanoda overflow from #2 is gone. Item 1 (no spec approval recorded) and item 7 (main does not require bar / bar) are OPEN. Both are expected while bar.toml says in-progress.
• Local build: lake build on Lean 4.35.0 succeeds with 18 jobs and no warnings. python3 tests/run_tests.py gives 0 failures and rewrites tests/TEST-RESULTS.md byte for byte.
• Escape hatches: Xml/, Proofs/, Main.lean and the root modules contain no sorry, admit, axiom, native_decide, implemented_by, extern, unsafe, partial or opaque. The only sorrys are the challenge statements in Spec.lean.
• Merge: the branch merges cleanly with main, which already holds the LICENSE merge.

Findings from the earlier reviews on #2

I checked each one on the compiled binary.

• xmlns (blocking): <a xmlns="urn:x"/> and <a><b xmlns=""/></a> are refused. <a xmlnsx="1"/> is still accepted. Spec.rejects_xmlns states the rule, and AttrsOk carries the matching condition.
• "What is proved" vs the theorems (blocking): the single-input refusals are now statements over families of texts. Spec.parse_wf and Spec.print_parse hold for every input. README and SPEC rows name the positions each theorem covers. "What is not proved" says plainly that other positions rest on the tests.
• Whitespace between attributes: <a b="1"c="2"/> is refused, and Spec.rejects_attribute_without_space states the rule.
• Line ends: <a>x\r\ny</a> reads as x\ny, and a lone CR reads as LF. Spec.crlf_reads_as_lf and Spec.cr_reads_as_lf state both.
• Harness: it now fails closed (exit status, answer count, every failure counted) and always runs lake build.
• Missing inputs: the cases listed in review 1 finding 7 are named rejections now. An undefined entity in a nested element, <a><b>&e;</b></a>, is refused.

Non-blocking

• The plan names Go encoding/xml and Rust quick-xml as oracles. They are still not wired in. The README says so under What you must trust, so this can be a follow-up.
• This approval is a code review of the slice. It does not record a spec approval in bar.toml. Bar item 1 still needs its own approval entry, and main still needs the bar / bar branch rule for item 7.

---

Generated by Claude Code