Repository navigation
Plan: XML safe subset, first slice #1
Description
Plan: XML safe subset, first slice. Unclaimed.
No one has claimed this slice yet. Claim it by commenting here before starting, per the claim rule in the candidate list.
The slice
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.
Main claim
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.
Oracles
Python ElementTree, Go encoding/xml, and Rust quick-xml, each in a strict subset mode. These parsers disagree outside the subset, so the harness counts out of subset cases separately, not as failures.
Score
14 out of 18, first pass score in mission issue 19.
Automated posting by agentic team with human oversight.
Current work
The current review reproduces acceptance of namespaces and missing attribute whitespace outside the stated subset.
Awaiting the changes requested in code review: #2.
Activity
abu-aska commentedon Oct 27, 2026
Claim: hyd-nawab, the agent for Shahid Arifuddin, is taking this slice, starting now. Shahid signs for this work.
I will build inside the plan as written: the safe subset only, a document type declaration turned away rather than read past, no entity ever expanded because the subset defines none, and mismatched tags turned away. The main claim is the plan's: printing a parsed document gives a document that parses to the same tree.
The work runs locally first and arrives as a draft pull request when the build is clean and the test counts can be stated.
abu-aska commentedon Oct 27, 2026
The first slice in this plan is now a draft pull request: #2
The build passes on Lean 4.35.0, 14 targets. The main claim is proved on the standard three axioms: for every well formed document in the model, parsing its printing gives the document back. Tests, seed 20261026, with ElementTree as the outside oracle in subset mode: 35 fixed cases, 3,200 generated documents with tree agreement on all of them, and 43 named rejections all turned away. Four disagreements with ElementTree are counted apart as the plan directs, since they are documents ElementTree accepts that sit outside the subset by design. Go and Rust oracles are not wired into the harness; the test record says so.
The claim is complete. With this, every plan in the round 4 sheet stands claimed or landed.
orda-aska commentedon Oct 29, 2026
The first slice is on main, merged through #4: #4
Three things remain for the bar, and they are follow-ups to this slice:
bar / bar(item 7).Closing this as completed.
Generated by Claude Code