feat(schema): compositional UPA determinism, delete positionCap
The Unique Particle Attribution check no longer inlines group references or caps. A new CompositionalDeterminism engine computes first/followlast over particle identities and summarizes each xs:group once, so a multiply-referenced nested group whose inlined Glushkov automaton would be 2^K positions is checked in O(nodes * particles^2) time. ContentModelDeterminism now delegates to it and the inlining position automaton plus positionCap are deleted, closing the last named interactive-safety resource-bound blocker (production-readiness stopper #4) and the silent under-rejection the cap caused (stopper #3). The compositional engine was proven verdict-equivalent to the prior inlining automaton by a differential over the entire XSTS corpus (zero divergences) before replacing it. The followlast detail was essential: a first attempt that emitted a repeating end-item's loop-back and the suffix-first as separate decision sets under-detected 13 XSTS content models; the differential caught every one. Verification: XSTS gate unchanged (invalid-schemas-accepted 15, valid-schemas- rejected 0, instance buckets held); SchemaDeterminismGroupBlowupTests compiles a 2^20-position model without hanging and rejects an ambiguous one the old cap would have skipped (WASI uses a smaller depth, native time limits gated off WASI); full suite, style, namespacing, and WASM all pass. The per-particle model and QName-only overlap are preserved, so the false-positive direction stays at zero.
This commit is contained in:
parent
ba69d716fa
commit
6f8222a840
File diff suppressed because one or more lines are too long
@ -1,23 +1,26 @@
|
||||
public extension PureXML.Schema {
|
||||
/// Unique Particle Attribution (cos-nonambig, XSD 1.0 3.8.6): a content model
|
||||
/// must be deterministic, so each element in an instance is attributed to one
|
||||
/// particle without lookahead. Checked on the Glushkov position automaton: the
|
||||
/// model is ambiguous iff some decision set, the start `firstpos` or any
|
||||
/// `followpos(p)`, holds two distinct positions whose labels can match the same
|
||||
/// element. No DFA subset construction is needed.
|
||||
/// particle without lookahead. The model is ambiguous iff some decision set (the
|
||||
/// content's `first`, or any item's `followpos`) holds two distinct particles
|
||||
/// whose labels can match the same element.
|
||||
///
|
||||
/// This works on a LITERAL view of the raw schema tree, distinct from the
|
||||
/// compiled (instance) content model: a `ref` is one position carrying its
|
||||
/// resolved QName (prefix bindings, not the blanket target namespace), and
|
||||
/// substitution groups are NOT expanded. The overlap test is QName-only (not
|
||||
/// substitution-group-aware), so it can only under-report substitution-group
|
||||
/// ambiguities, never over-report. Those two choices remove the false overlaps
|
||||
/// (cross-namespace refs; expanded substitution members) that a check over the
|
||||
/// compiled model produced.
|
||||
/// The check delegates to ``PureXML/Schema/CompositionalDeterminism``, which
|
||||
/// computes `first`/`followlast` over PARTICLE identities WITHOUT inlining
|
||||
/// `<xs:group ref>`, so a multiply-referenced nested group cannot blow up to
|
||||
/// `2^K` positions. That gives a proven `O(nodes * particles^2)` bound with no
|
||||
/// position cap and no silent skip (production-readiness stopper #4). The
|
||||
/// compositional engine was proven verdict-equivalent to the prior inlining
|
||||
/// Glushkov automaton by a differential over the whole XSTS corpus (zero
|
||||
/// divergences) before it became authoritative; see
|
||||
/// docs/design/counted-content-automaton.md.
|
||||
///
|
||||
/// It works on a LITERAL view of the raw schema tree, distinct from the compiled
|
||||
/// (instance) content model: a `ref` is one particle carrying its resolved QName
|
||||
/// (prefix bindings, not the blanket target namespace), and substitution groups
|
||||
/// are NOT expanded. The overlap test is QName-only, so it can only under-report
|
||||
/// substitution-group ambiguities, never over-report.
|
||||
enum ContentModelDeterminism {
|
||||
private static let modelGroupNames: Set<String> = ["sequence", "choice", "all"]
|
||||
private static let particleNames: Set<String> = ["element", "sequence", "choice", "all", "group", "any"]
|
||||
|
||||
/// Every UPA-violation finding across the schema's complex-type content
|
||||
/// models, deduplicated by message in first-seen order. Each finding is
|
||||
/// located on the content-model node (`sequence`/`choice`/`all`/`group`)
|
||||
@ -29,7 +32,9 @@ public extension PureXML.Schema {
|
||||
var seen: Set<String> = []
|
||||
forEachComplexType(schema) { complexType in
|
||||
let models = effectiveModelNodes(complexType, bindings, context, [])
|
||||
guard !models.isEmpty, let conflict = violation(models, bindings, context) else { return }
|
||||
guard !models.isEmpty,
|
||||
let conflict = PureXML.Schema.CompositionalDeterminism.violation(models, bindings, context)
|
||||
else { return }
|
||||
// The conflicting particle the author can act on is in this type's own
|
||||
// content, so locate on its own content-model node.
|
||||
let node = contentModelNode(complexType) ?? complexType
|
||||
@ -64,279 +69,5 @@ public extension PureXML.Schema {
|
||||
forEachComplexType(child, visit)
|
||||
}
|
||||
}
|
||||
|
||||
/// A UPA-violation message for the content model formed by `models` in
|
||||
/// sequence, or nil. The effective content of a `complexContent` extension is
|
||||
/// its base's content followed by its own, so the models are built as one
|
||||
/// sequence: a base particle that can recur or end optionally then competes
|
||||
/// with the extension's leading particles, the cross-boundary
|
||||
/// non-determinism a single-node check misses (XSTS particlesZ022). For a
|
||||
/// non-extension the list is a single node, so `sequence([x])` reproduces the
|
||||
/// prior single-model automaton exactly.
|
||||
private static func violation(_ models: [XSDTree], _ bindings: [String: String], _ context: XSDContext) -> String? {
|
||||
var automaton = PureXML.Schema.PositionAutomaton()
|
||||
let root = sequence(models.map { build($0, &automaton, bindings, context, []) }, &automaton)
|
||||
// A model that hit the position cap was only partially built; skip it
|
||||
// rather than risk a result from an incomplete automaton.
|
||||
if automaton.labels.count > positionCap { return nil }
|
||||
var decisionSets = automaton.followpos
|
||||
decisionSets.append(root.first)
|
||||
for set in decisionSets {
|
||||
if let conflict = overlap(in: set, automaton: automaton) {
|
||||
return "ambiguous content model: '\(conflict)' can be matched by more than one particle"
|
||||
}
|
||||
}
|
||||
return nil
|
||||
}
|
||||
|
||||
/// A ceiling on positions per content model. A pathological schema is bounded
|
||||
/// here and its UPA check skipped (an under-rejection, never an
|
||||
/// over-rejection). Real content models are far below this.
|
||||
private static let positionCap = 4096
|
||||
|
||||
private static func build(
|
||||
_ node: XSDTree,
|
||||
_ automaton: inout PureXML.Schema.PositionAutomaton,
|
||||
_ bindings: [String: String],
|
||||
_ context: XSDContext,
|
||||
_ visiting: Set<String>,
|
||||
) -> PureXML.Schema.Positions {
|
||||
if automaton.labels.count > positionCap { return .empty }
|
||||
let (minimum, maximum) = PureXML.Schema.XSDNode.occurrence(node)
|
||||
// A `maxOccurs="0"` particle can never occur, and a negative maxOccurs is
|
||||
// malformed (flagged by occurrence-order validation): either contributes
|
||||
// nothing here, and this guards the copy count below against a bad bound.
|
||||
if let maximum, maximum <= 0 { return .empty }
|
||||
// A fixed count {n,n} is n copies in sequence with no repetition loop, so
|
||||
// `b{2,2}, b` stays the deterministic `b, b, b`. The exact count above one
|
||||
// does not change the determinism question, so it is clamped to two.
|
||||
if let maximum, minimum == maximum {
|
||||
let copies = (0 ..< Swift.min(maximum, 2)).map { _ in buildInner(node, &automaton, bindings, context, visiting) }
|
||||
return sequence(copies, &automaton)
|
||||
}
|
||||
// Here min < max. Build one copy. A self-loop (last -> first) is added
|
||||
// only when the particle can truly repeat (max unbounded or above one);
|
||||
// unrolling a repetition into separate copies would put one element in two
|
||||
// positions of a decision set and read as ambiguity, when a repetition of
|
||||
// a deterministic body is itself deterministic. A {0,1} is merely optional,
|
||||
// not a repetition, so it gets no loop. The floor sets nullability.
|
||||
let inner = buildInner(node, &automaton, bindings, context, visiting)
|
||||
if maximum == nil || (maximum ?? 0) > 1 {
|
||||
for position in inner.last {
|
||||
automaton.followpos[position].formUnion(inner.first)
|
||||
}
|
||||
}
|
||||
return PureXML.Schema.Positions(nullable: minimum == 0 || inner.nullable, first: inner.first, last: inner.last)
|
||||
}
|
||||
|
||||
private static func buildInner(
|
||||
_ node: XSDTree,
|
||||
_ automaton: inout PureXML.Schema.PositionAutomaton,
|
||||
_ bindings: [String: String],
|
||||
_ context: XSDContext,
|
||||
_ visiting: Set<String>,
|
||||
) -> PureXML.Schema.Positions {
|
||||
switch PureXML.Schema.XSDNode.localName(node) {
|
||||
case "element":
|
||||
let position = automaton.position(.name(elementQName(node, bindings, context)), node)
|
||||
return PureXML.Schema.Positions(nullable: false, first: [position], last: [position])
|
||||
case "any":
|
||||
let position = automaton.position(.wildcard(PureXML.Schema.XSDParser.wildcard(node, context)), node)
|
||||
return PureXML.Schema.Positions(nullable: false, first: [position], last: [position])
|
||||
case "sequence":
|
||||
return sequence(childSets(node, &automaton, bindings, context, visiting), &automaton)
|
||||
case "choice":
|
||||
return choice(childSets(node, &automaton, bindings, context, visiting))
|
||||
case "all":
|
||||
return all(childSets(node, &automaton, bindings, context, visiting), &automaton)
|
||||
case "group":
|
||||
return groupReference(node, &automaton, bindings, context, visiting)
|
||||
default:
|
||||
return .empty
|
||||
}
|
||||
}
|
||||
|
||||
private static func childSets(
|
||||
_ node: XSDTree,
|
||||
_ automaton: inout PureXML.Schema.PositionAutomaton,
|
||||
_ bindings: [String: String],
|
||||
_ context: XSDContext,
|
||||
_ visiting: Set<String>,
|
||||
) -> [PureXML.Schema.Positions] {
|
||||
PureXML.Schema.XSDNode.elementChildren(node)
|
||||
.filter { particleNames.contains(PureXML.Schema.XSDNode.localName($0) ?? "") }
|
||||
.map { build($0, &automaton, bindings, context, visiting) }
|
||||
}
|
||||
|
||||
/// Inlines a `group` reference's model group (its sole `all`/`choice`/
|
||||
/// `sequence`), guarding against a cyclic reference.
|
||||
private static func groupReference(
|
||||
_ node: XSDTree,
|
||||
_ automaton: inout PureXML.Schema.PositionAutomaton,
|
||||
_ bindings: [String: String],
|
||||
_ context: XSDContext,
|
||||
_ visiting: Set<String>,
|
||||
) -> PureXML.Schema.Positions {
|
||||
guard let ref = PureXML.Schema.XSDNode.attribute(node, "ref") else { return .empty }
|
||||
let name = PureXML.Schema.XSDNode.stripPrefix(ref)
|
||||
guard !visiting.contains(name), let definition = context.groups[name],
|
||||
let model = PureXML.Schema.XSDNode.elementChildren(definition).first(where: { modelGroupNames.contains(PureXML.Schema.XSDNode.localName($0) ?? "") })
|
||||
else { return .empty }
|
||||
return build(model, &automaton, bindings, context, visiting.union([name]))
|
||||
}
|
||||
|
||||
private static func elementQName(_ node: XSDTree, _ bindings: [String: String], _ context: XSDContext) -> PureXML.Model.QualifiedName {
|
||||
if let ref = PureXML.Schema.XSDNode.attribute(node, "ref") {
|
||||
return resolveQName(ref, bindings, context)
|
||||
}
|
||||
let name = PureXML.Schema.XSDNode.attribute(node, "name") ?? ""
|
||||
let form = PureXML.Schema.XSDNode.attribute(node, "form")
|
||||
let qualified = form == "qualified" || (form == nil && context.elementFormQualified)
|
||||
return PureXML.Model.QualifiedName(localName: name, namespaceURI: qualified ? context.targetNamespace : nil)
|
||||
}
|
||||
|
||||
/// Resolves a QName reference to (localName, namespaceURI): a prefix maps
|
||||
/// through the schema's bindings (or stands for itself if unbound, keeping
|
||||
/// distinct prefixes distinct); an unprefixed name takes the default
|
||||
/// namespace binding.
|
||||
private static func resolveQName(_ qname: String, _ bindings: [String: String], _: XSDContext) -> PureXML.Model.QualifiedName {
|
||||
let parts = qname.split(separator: ":", maxSplits: 1).map(String.init)
|
||||
if parts.count == 2 {
|
||||
return PureXML.Model.QualifiedName(localName: parts[1], namespaceURI: bindings[parts[0]] ?? parts[0])
|
||||
}
|
||||
return PureXML.Model.QualifiedName(localName: qname, namespaceURI: bindings[""])
|
||||
}
|
||||
|
||||
private static func sequence(_ children: [PureXML.Schema.Positions], _ automaton: inout PureXML.Schema.PositionAutomaton) -> PureXML.Schema.Positions {
|
||||
var first: Set<Int> = []
|
||||
var prefixNullable = true
|
||||
var preceding: Set<Int> = []
|
||||
for child in children {
|
||||
if prefixNullable { first.formUnion(child.first) }
|
||||
for position in preceding {
|
||||
automaton.followpos[position].formUnion(child.first)
|
||||
}
|
||||
preceding = child.nullable ? preceding.union(child.last) : child.last
|
||||
if !child.nullable { prefixNullable = false }
|
||||
}
|
||||
var last: Set<Int> = []
|
||||
var suffixNullable = true
|
||||
for child in children.reversed() {
|
||||
if suffixNullable { last.formUnion(child.last) }
|
||||
if !child.nullable { suffixNullable = false }
|
||||
}
|
||||
return PureXML.Schema.Positions(nullable: children.allSatisfy(\.nullable), first: first, last: last)
|
||||
}
|
||||
|
||||
private static func choice(_ children: [PureXML.Schema.Positions]) -> PureXML.Schema.Positions {
|
||||
PureXML.Schema.Positions(
|
||||
nullable: children.isEmpty || children.contains(where: \.nullable),
|
||||
first: children.reduce(into: Set<Int>()) { $0.formUnion($1.first) },
|
||||
last: children.reduce(into: Set<Int>()) { $0.formUnion($1.last) },
|
||||
)
|
||||
}
|
||||
|
||||
/// `all`: members are order-independent, so each may follow every other and
|
||||
/// the members form one decision set; two same-named members then overlap.
|
||||
private static func all(_ children: [PureXML.Schema.Positions], _ automaton: inout PureXML.Schema.PositionAutomaton) -> PureXML.Schema.Positions {
|
||||
for source in children {
|
||||
for target in children where target.first != source.first {
|
||||
for position in source.last {
|
||||
automaton.followpos[position].formUnion(target.first)
|
||||
}
|
||||
}
|
||||
}
|
||||
return choice(children)
|
||||
}
|
||||
|
||||
private static func overlap(in set: Set<Int>, automaton: PureXML.Schema.PositionAutomaton) -> String? {
|
||||
let positions = set.sorted()
|
||||
for outer in 0 ..< positions.count {
|
||||
let outerPosition = positions[outer]
|
||||
for inner in (outer + 1) ..< positions.count {
|
||||
let innerPosition = positions[inner]
|
||||
// Two positions conflict only if they are distinct particles whose
|
||||
// labels can match the same element; one particle's own repetition
|
||||
// (same source) is deterministic by construction.
|
||||
guard automaton.particles[outerPosition] != automaton.particles[innerPosition],
|
||||
labelsOverlap(automaton.labels[outerPosition], automaton.labels[innerPosition])
|
||||
else { continue }
|
||||
return describe(automaton.labels[outerPosition])
|
||||
}
|
||||
}
|
||||
return nil
|
||||
}
|
||||
|
||||
private static func labelsOverlap(_ lhs: TermLabel, _ rhs: TermLabel) -> Bool {
|
||||
switch (lhs, rhs) {
|
||||
case let (.name(lhsName), .name(rhsName)):
|
||||
lhsName.localName == rhsName.localName && lhsName.namespaceURI == rhsName.namespaceURI
|
||||
case let (.name(name), .wildcard(wildcard)), let (.wildcard(wildcard), .name(name)):
|
||||
wildcard.admits(name)
|
||||
case let (.wildcard(lhsCard), .wildcard(rhsCard)):
|
||||
wildcardsOverlap(lhsCard, rhsCard)
|
||||
}
|
||||
}
|
||||
|
||||
private static func wildcardsOverlap(_ lhs: Wildcard, _ rhs: Wildcard) -> Bool {
|
||||
switch (lhs.namespace, rhs.namespace) {
|
||||
case (.any, _), (_, .any):
|
||||
// `##any` admits every name, so it shares names with any other constraint.
|
||||
true
|
||||
case (.other, .other):
|
||||
// Two `##other` constraints each admit every namespace but their own
|
||||
// target (and the absent namespace); those infinite sets always
|
||||
// intersect, so they overlap (XSTS wildI* non-deterministic choices).
|
||||
true
|
||||
case let (.enumerated(lhsSet), .enumerated(rhsSet)):
|
||||
!lhsSet.isDisjoint(with: rhsSet)
|
||||
case let (.other, .enumerated(set)):
|
||||
otherOverlapsEnumerated(set, target: lhs.targetNamespace)
|
||||
case let (.enumerated(set), .other):
|
||||
otherOverlapsEnumerated(set, target: rhs.targetNamespace)
|
||||
}
|
||||
}
|
||||
|
||||
/// Whether `##other` (any namespace but the target and the absent namespace)
|
||||
/// shares a name with an enumerated set: it does iff the set names some
|
||||
/// namespace that is neither absent (the empty string, `##local`) nor the
|
||||
/// target namespace `##other` excludes.
|
||||
private static func otherOverlapsEnumerated(_ set: Set<String>, target: String?) -> Bool {
|
||||
set.contains { !$0.isEmpty && $0 != (target ?? "") }
|
||||
}
|
||||
|
||||
private static func describe(_ label: TermLabel) -> String {
|
||||
switch label {
|
||||
case let .name(name): name.localName
|
||||
case .wildcard: "any"
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// The firstpos/lastpos/nullable summary of a sub-model, used while building the
|
||||
/// position automaton.
|
||||
private struct Positions {
|
||||
let nullable: Bool
|
||||
let first: Set<Int>
|
||||
let last: Set<Int>
|
||||
|
||||
static let empty = Positions(nullable: true, first: [], last: [])
|
||||
}
|
||||
|
||||
/// The Glushkov position automaton under construction: one entry per position
|
||||
/// for its transition label, its `followpos` set, and the source particle it
|
||||
/// came from (Unique Particle Attribution is per particle, so a particle never
|
||||
/// conflicts with a repetition of itself).
|
||||
private struct PositionAutomaton {
|
||||
var labels: [TermLabel] = []
|
||||
var followpos: [Set<Int>] = []
|
||||
var particles: [ObjectIdentifier] = []
|
||||
|
||||
mutating func position(_ label: TermLabel, _ source: XSDTree) -> Int {
|
||||
labels.append(label)
|
||||
followpos.append([])
|
||||
particles.append(ObjectIdentifier(source))
|
||||
return labels.count - 1
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
252
Sources/Schema/ContentModelDeterminismCompositional.swift
Normal file
252
Sources/Schema/ContentModelDeterminismCompositional.swift
Normal file
@ -0,0 +1,252 @@
|
||||
/// One distinct particle occurrence in a content model: its source-node identity
|
||||
/// and label. A particle never conflicts with a repetition of itself, so identity,
|
||||
/// not label alone, decides conflict (per the UPA semantics). File-private.
|
||||
private struct CompItem: Hashable {
|
||||
let particle: ObjectIdentifier
|
||||
let label: PureXML.Schema.TermLabel
|
||||
|
||||
static func == (lhs: CompItem, rhs: CompItem) -> Bool {
|
||||
lhs.particle == rhs.particle
|
||||
}
|
||||
|
||||
func hash(into hasher: inout Hasher) {
|
||||
hasher.combine(particle)
|
||||
}
|
||||
}
|
||||
|
||||
/// The context-independent summary of a sub-model: nullability, the items that can
|
||||
/// start it (`first`), and, for each item that can END it, the items that follow
|
||||
/// that end-item INTERNALLY (`followlast`, e.g. the loop-back of a repetition or
|
||||
/// the cross-edges of an `all`). The parent forms a gap's decision set by combining
|
||||
/// a child's `followlast` with the first of what comes next.
|
||||
private struct CompSummary {
|
||||
var nullable: Bool
|
||||
var first: [CompItem]
|
||||
/// Each end-item paired with its internal follow set.
|
||||
var lastFollow: [(item: CompItem, follow: [CompItem])]
|
||||
}
|
||||
|
||||
extension PureXML.Schema {
|
||||
/// A compositional Unique Particle Attribution (1-unambiguity) check that does
|
||||
/// NOT inline `<xs:group ref>`: each group is summarized once, so a
|
||||
/// multiply-referenced nested group cannot blow up to `2^K` positions (which is
|
||||
/// why the former inlining Glushkov automaton needed a `positionCap` skip).
|
||||
/// Cross-boundary decision sets are formed at each reference site, so two
|
||||
/// reference contexts never merge (that merge would be a false positive).
|
||||
///
|
||||
/// This is the authoritative determinism check (`ContentModelDeterminism`
|
||||
/// delegates to it). It was proven verdict-equivalent to the prior inlining
|
||||
/// automaton by a differential over the whole XSTS corpus (zero divergences)
|
||||
/// before replacing it. See docs/design/counted-content-automaton.md.
|
||||
enum CompositionalDeterminism {
|
||||
/// A UPA-violation message for the content model formed by `models` in
|
||||
/// sequence (a complexContent extension's effective content), or nil.
|
||||
static func violation(_ models: [XSDTree], _ bindings: [String: String], _ context: XSDContext) -> String? {
|
||||
var walk = CompWalk(bindings: bindings, context: context)
|
||||
let summary = walk.sequence(models.map { walk.summarize($0, visiting: []) })
|
||||
// The root's entry decision set, plus the followpos of each item that can
|
||||
// end the whole model (nothing follows the root, so its followpos is just
|
||||
// its internal follow).
|
||||
walk.emit(summary.first)
|
||||
for entry in summary.lastFollow {
|
||||
walk.emit(entry.follow)
|
||||
}
|
||||
for set in walk.decisionSets {
|
||||
if let conflict = CompWalk.overlap(set) {
|
||||
return "ambiguous content model: '\(conflict)' can be matched by more than one particle"
|
||||
}
|
||||
}
|
||||
return nil
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
/// The mutable walk state, so the recursive helpers take few parameters and the
|
||||
/// group cache / decision-set accumulator are threaded without inout chains.
|
||||
private struct CompWalk {
|
||||
let bindings: [String: String]
|
||||
let context: PureXML.Schema.XSDContext
|
||||
var decisionSets: [[CompItem]] = []
|
||||
var groupCache: [String: CompSummary] = [:]
|
||||
|
||||
mutating func emit(_ set: [CompItem]) {
|
||||
if set.count > 1 { decisionSets.append(set) }
|
||||
}
|
||||
|
||||
mutating func summarize(_ node: PureXML.Model.TreeNode, visiting: Set<String>) -> CompSummary {
|
||||
let (minimum, maximum) = PureXML.Schema.XSDNode.occurrence(node)
|
||||
if let maximum, maximum <= 0 { return CompSummary(nullable: true, first: [], lastFollow: []) }
|
||||
var body = bodySummary(node, visiting: visiting)
|
||||
// A repeat edge (last -> first) is added for a true repetition (max unbounded or >= 2) with min < max. A
|
||||
// fixed `{n,n}` clamps to copies sharing the body's particle identities (no new
|
||||
// conflict); a `{0,1}` is optional, not a repetition. The loop folds the body's
|
||||
// first into every end-item's follow, so a later gap (or the root) checks the
|
||||
// combined loop+continuation decision set.
|
||||
if minimum != maximum, maximum == nil || (maximum ?? 0) > 1 {
|
||||
body.lastFollow = body.lastFollow.map { (item: $0.item, follow: $0.follow + body.first) }
|
||||
}
|
||||
return CompSummary(nullable: minimum == 0 || body.nullable, first: body.first, lastFollow: body.lastFollow)
|
||||
}
|
||||
|
||||
private mutating func bodySummary(_ node: PureXML.Model.TreeNode, visiting: Set<String>) -> CompSummary {
|
||||
switch PureXML.Schema.XSDNode.localName(node) {
|
||||
case "element":
|
||||
let item = CompItem(particle: ObjectIdentifier(node), label: .name(elementQName(node)))
|
||||
return CompSummary(nullable: false, first: [item], lastFollow: [(item, [])])
|
||||
case "any":
|
||||
let item = CompItem(particle: ObjectIdentifier(node), label: .wildcard(PureXML.Schema.XSDParser.wildcard(node, context)))
|
||||
return CompSummary(nullable: false, first: [item], lastFollow: [(item, [])])
|
||||
case "sequence":
|
||||
return sequence(children(node, visiting: visiting))
|
||||
case "choice":
|
||||
return choice(children(node, visiting: visiting))
|
||||
case "all":
|
||||
return all(children(node, visiting: visiting))
|
||||
case "group":
|
||||
return group(node, visiting: visiting)
|
||||
default:
|
||||
return CompSummary(nullable: true, first: [], lastFollow: [])
|
||||
}
|
||||
}
|
||||
|
||||
private mutating func children(_ node: PureXML.Model.TreeNode, visiting: Set<String>) -> [CompSummary] {
|
||||
PureXML.Schema.XSDNode.elementChildren(node)
|
||||
.filter { ["element", "sequence", "choice", "all", "group", "any"].contains(PureXML.Schema.XSDNode.localName($0) ?? "") }
|
||||
.map { summarize($0, visiting: visiting) }
|
||||
}
|
||||
|
||||
/// A `sequence`: at each gap, every item that can end the preceding nullable run
|
||||
/// has its internal follow combined with the first of the following nullable run
|
||||
/// into one decision set (the real `followpos` of that end-item inside the
|
||||
/// sequence). The sequence's own `lastFollow` is its trailing nullable suffix's
|
||||
/// end-items, carried up for the parent to combine with whatever follows.
|
||||
mutating func sequence(_ parts: [CompSummary]) -> CompSummary {
|
||||
for index in parts.indices {
|
||||
var suffixFirst: [CompItem] = []
|
||||
for next in parts[(index + 1)...] {
|
||||
suffixFirst.append(contentsOf: next.first)
|
||||
if !next.nullable { break }
|
||||
}
|
||||
guard !suffixFirst.isEmpty else { continue }
|
||||
for entry in parts[index].lastFollow {
|
||||
emit(entry.follow + suffixFirst)
|
||||
}
|
||||
}
|
||||
var first: [CompItem] = []
|
||||
for part in parts {
|
||||
first.append(contentsOf: part.first)
|
||||
if !part.nullable { break }
|
||||
}
|
||||
var lastFollow: [(item: CompItem, follow: [CompItem])] = []
|
||||
for part in parts.reversed() {
|
||||
lastFollow.append(contentsOf: part.lastFollow)
|
||||
if !part.nullable { break }
|
||||
}
|
||||
return CompSummary(nullable: parts.allSatisfy(\.nullable), first: first, lastFollow: lastFollow)
|
||||
}
|
||||
|
||||
private mutating func choice(_ parts: [CompSummary]) -> CompSummary {
|
||||
let first = parts.flatMap(\.first)
|
||||
emit(first)
|
||||
return CompSummary(
|
||||
nullable: parts.isEmpty || parts.contains(where: \.nullable),
|
||||
first: first,
|
||||
lastFollow: parts.flatMap(\.lastFollow),
|
||||
)
|
||||
}
|
||||
|
||||
/// `all`: members are order-independent, so each may follow every other. Each
|
||||
/// member's end-items therefore follow (internally) every OTHER member's first,
|
||||
/// and the union of member firsts is one decision set (the entry). The cross
|
||||
/// follow is recorded in `followlast` so a parent gap combines it with the suffix
|
||||
/// (mirrors `ContentModelDeterminism.all`).
|
||||
private mutating func all(_ parts: [CompSummary]) -> CompSummary {
|
||||
let first = parts.flatMap(\.first)
|
||||
emit(first)
|
||||
var lastFollow: [(item: CompItem, follow: [CompItem])] = []
|
||||
for (index, part) in parts.enumerated() {
|
||||
let others = parts.enumerated().filter { $0.offset != index }.flatMap(\.element.first)
|
||||
for entry in part.lastFollow {
|
||||
lastFollow.append((entry.item, entry.follow + others))
|
||||
}
|
||||
}
|
||||
return CompSummary(
|
||||
nullable: parts.isEmpty || parts.allSatisfy(\.nullable),
|
||||
first: first,
|
||||
lastFollow: lastFollow,
|
||||
)
|
||||
}
|
||||
|
||||
private mutating func group(_ node: PureXML.Model.TreeNode, visiting: Set<String>) -> CompSummary {
|
||||
guard let ref = PureXML.Schema.XSDNode.attribute(node, "ref") else { return CompSummary(nullable: true, first: [], lastFollow: []) }
|
||||
let name = PureXML.Schema.XSDNode.stripPrefix(ref)
|
||||
if let cached = groupCache[name] { return cached }
|
||||
guard !visiting.contains(name), let definition = context.groups[name],
|
||||
let model = PureXML.Schema.XSDNode.elementChildren(definition).first(where: { ["sequence", "choice", "all"].contains(PureXML.Schema.XSDNode.localName($0) ?? "") })
|
||||
else { return CompSummary(nullable: true, first: [], lastFollow: []) }
|
||||
// Summarize the group once: its internal decision sets are context-independent
|
||||
// and emitted here; its cross-boundary follow is formed by each reference site.
|
||||
let summary = summarize(model, visiting: visiting.union([name]))
|
||||
groupCache[name] = summary
|
||||
return summary
|
||||
}
|
||||
|
||||
// MARK: Conflict
|
||||
|
||||
static func overlap(_ set: [CompItem]) -> String? {
|
||||
var nameOwner: [PureXML.Model.QualifiedName: ObjectIdentifier] = [:]
|
||||
var wildcards: [(card: PureXML.Schema.Wildcard, particle: ObjectIdentifier)] = []
|
||||
for item in set {
|
||||
switch item.label {
|
||||
case let .name(qname):
|
||||
if let owner = nameOwner[qname], owner != item.particle { return qname.localName }
|
||||
if nameOwner[qname] == nil { nameOwner[qname] = item.particle }
|
||||
case let .wildcard(card):
|
||||
wildcards.append((card, item.particle))
|
||||
}
|
||||
}
|
||||
for (index, wildcard) in wildcards.enumerated() {
|
||||
// A wildcard conflicts with any name it admits, from a distinct particle,
|
||||
// and with any other wildcard it intersects, from a distinct particle.
|
||||
if nameOwner.contains(where: { wildcard.card.admits($0.key) && $0.value != wildcard.particle }) { return "any" }
|
||||
for other in wildcards[(index + 1)...] where other.particle != wildcard.particle && wildcardsOverlap(wildcard.card, other.card) {
|
||||
return "any"
|
||||
}
|
||||
}
|
||||
return nil
|
||||
}
|
||||
|
||||
// MARK: Helpers (mirror ContentModelDeterminism)
|
||||
|
||||
private func elementQName(_ node: PureXML.Model.TreeNode) -> PureXML.Model.QualifiedName {
|
||||
if let ref = PureXML.Schema.XSDNode.attribute(node, "ref") {
|
||||
return resolveQName(ref)
|
||||
}
|
||||
let name = PureXML.Schema.XSDNode.attribute(node, "name") ?? ""
|
||||
let form = PureXML.Schema.XSDNode.attribute(node, "form")
|
||||
let qualified = form == "qualified" || (form == nil && context.elementFormQualified)
|
||||
return PureXML.Model.QualifiedName(localName: name, namespaceURI: qualified ? context.targetNamespace : nil)
|
||||
}
|
||||
|
||||
private func resolveQName(_ qname: String) -> PureXML.Model.QualifiedName {
|
||||
let parts = qname.split(separator: ":", maxSplits: 1).map(String.init)
|
||||
if parts.count == 2 {
|
||||
return PureXML.Model.QualifiedName(localName: parts[1], namespaceURI: bindings[parts[0]] ?? parts[0])
|
||||
}
|
||||
return PureXML.Model.QualifiedName(localName: qname, namespaceURI: bindings[""])
|
||||
}
|
||||
|
||||
static func wildcardsOverlap(_ lhs: PureXML.Schema.Wildcard, _ rhs: PureXML.Schema.Wildcard) -> Bool {
|
||||
switch (lhs.namespace, rhs.namespace) {
|
||||
case (.any, _), (_, .any): true
|
||||
case (.other, .other): true
|
||||
case let (.enumerated(lhsSet), .enumerated(rhsSet)): !lhsSet.isDisjoint(with: rhsSet)
|
||||
case let (.other, .enumerated(set)): otherOverlapsEnumerated(set, target: lhs.targetNamespace)
|
||||
case let (.enumerated(set), .other): otherOverlapsEnumerated(set, target: rhs.targetNamespace)
|
||||
}
|
||||
}
|
||||
|
||||
static func otherOverlapsEnumerated(_ set: Set<String>, target: String?) -> Bool {
|
||||
set.contains { !$0.isEmpty && $0 != (target ?? "") }
|
||||
}
|
||||
}
|
||||
64
Tests/SchemaDeterminismGroupBlowupTests.swift
Normal file
64
Tests/SchemaDeterminismGroupBlowupTests.swift
Normal file
@ -0,0 +1,64 @@
|
||||
import Testing
|
||||
@testable import PureXML
|
||||
|
||||
/// The compositional UPA check (ContentModelDeterminism via CompositionalDeterminism)
|
||||
/// summarizes each `<xs:group>` once, so a multiply-referenced nested group whose
|
||||
/// inlined position count is `2^depth` is checked in polynomial time instead of being
|
||||
/// silently skipped by the former `positionCap` (which capped at 4096 positions).
|
||||
/// These pin both the bound (no hang) and the verdict on schemas the old engine
|
||||
/// could not check. The `.timeLimit` trait is native-only (unsupported by the
|
||||
/// single-threaded WASI runtime), and the depth is smaller on WASI (~30x slower);
|
||||
/// both depths still exceed the old 4096-position cap, so the point holds.
|
||||
@Suite("UPA on 2^K nested-group content models")
|
||||
struct SchemaDeterminismGroupBlowupTests {
|
||||
#if os(WASI)
|
||||
private static let depth = 13 // 2^13 = 8192 positions, past the old 4096 cap
|
||||
#else
|
||||
private static let depth = 20 // 2^20 = ~1,048,576 inlined positions
|
||||
#endif
|
||||
|
||||
/// `g0=(g1,g1) … g{depth-1}=(g{depth},g{depth})`, leaf `g{depth}` = the given model.
|
||||
/// Inlined this is `2^depth` positions; summarized it is `depth` groups.
|
||||
private func doublingSchema(leaf: String) -> String {
|
||||
let depth = Self.depth
|
||||
var parts = ["<xs:schema xmlns:xs=\"http://www.w3.org/2001/XMLSchema\">"]
|
||||
for level in 0 ..< depth {
|
||||
parts.append("<xs:group name=\"g\(level)\"><xs:sequence>"
|
||||
+ "<xs:group ref=\"g\(level + 1)\"/><xs:group ref=\"g\(level + 1)\"/>"
|
||||
+ "</xs:sequence></xs:group>")
|
||||
}
|
||||
parts.append("<xs:group name=\"g\(depth)\"><xs:sequence>\(leaf)</xs:sequence></xs:group>")
|
||||
parts.append("<xs:complexType name=\"T\"><xs:sequence><xs:group ref=\"g0\"/></xs:sequence></xs:complexType>")
|
||||
parts.append("<xs:element name=\"doc\" type=\"T\"/>")
|
||||
parts.append("</xs:schema>")
|
||||
return parts.joined()
|
||||
}
|
||||
|
||||
#if os(WASI)
|
||||
@Test("a deep deterministic nested-group model compiles (no hang, accepted)")
|
||||
#else
|
||||
@Test("a deep deterministic nested-group model compiles (no hang, accepted)", .timeLimit(.minutes(1)))
|
||||
#endif
|
||||
func test_deterministicBlowupCompiles() throws {
|
||||
// The leaf is a single element, so the model expands to many copies of `e` in
|
||||
// sequence: deterministic (each position is the same name, matched in order),
|
||||
// so the schema is valid. The old engine hit positionCap and skipped this.
|
||||
_ = try PureXML.Schema.Document(doublingSchema(leaf: "<xs:element name=\"e\"/>"))
|
||||
}
|
||||
|
||||
#if os(WASI)
|
||||
@Test("a deep AMBIGUOUS nested-group model is rejected (not skipped)")
|
||||
#else
|
||||
@Test("a deep AMBIGUOUS nested-group model is rejected (not skipped)", .timeLimit(.minutes(1)))
|
||||
#endif
|
||||
func test_ambiguousBlowupRejected() {
|
||||
// The leaf is a choice of TWO distinct element declarations of the same name,
|
||||
// so the leaf group is itself ambiguous (a leading `e` could be either
|
||||
// particle). The compositional check finds the conflict even though the model
|
||||
// expands past the old cap; the old engine hit positionCap and silently
|
||||
// accepted it. (`(g, g)` of ONE group is NOT a conflict, since both references
|
||||
// share the same particle identity, matching the prior oracle.)
|
||||
let leaf = "<xs:choice><xs:element name=\"e\"/><xs:element name=\"e\"/></xs:choice>"
|
||||
#expect((try? PureXML.Schema.Document(doublingSchema(leaf: leaf))) == nil)
|
||||
}
|
||||
}
|
||||
@ -63,7 +63,7 @@ Every claim below is labeled per proof discipline.
|
||||
| Counted matcher build size is independent of numeric occurrence magnitudes. | theorem, implemented | `ContentNFABuilder` allocates one counter scope per particle occurrence and a constant number of states/edges per particle; high-bound tests assert state count stays structural. |
|
||||
| Counted matcher runtime is bounded for interactive validation. | theorem target | For `N` child elements, `S` program states, and `D` counter scopes, validation is bounded by `O(N * S * D)` time and `O(S * D)` live matcher memory. The constants are schema-structural, not occurrence-magnitude structural. |
|
||||
| `all` groups remain exact. | theorem already implemented, out of scope for NFA replacement | `all` is validated by direct member counts in `ComplexValidator.matchesAll` and `allStructureErrors`; the counted automaton does not need to encode it initially. |
|
||||
| Counted UPA/determinism replaces `positionCap`. | blocked design frontier | The instance matcher can be replaced first. Deleting `positionCap` requires a separate counted determinism pass or a proof that the existing clamp is exact for XSD's admitted content models. |
|
||||
| Counted UPA/determinism replaces `positionCap`. | DONE (2026-06-22) | `CompositionalDeterminism` computes `first`/`followlast` over particle identities, summarizing each group once; `ContentModelDeterminism` delegates to it and `positionCap` is deleted. Proven verdict-equivalent to the inlining automaton by a differential over the whole XSTS corpus (zero divergences). |
|
||||
|
||||
## Bound representation
|
||||
|
||||
@ -433,3 +433,17 @@ O(nodes × particles²), polynomial in schema text: a PROVEN bound, no cap.
|
||||
- A perf test compiles a `2^K`-nested-group schema (K ≥ 20) within a tight time bound.
|
||||
- XSTS `valid-schemas-rejected` stays 0 and `invalid-schemas-accepted` does not rise
|
||||
(it may fall, as previously-skipped pathological models now get checked).
|
||||
|
||||
### Status: DONE (2026-06-22)
|
||||
|
||||
Implemented as `CompositionalDeterminism` (`Sources/Schema/ContentModelDeterminismCompositional.swift`);
|
||||
`ContentModelDeterminism` delegates to it and the inlining position automaton and
|
||||
`positionCap` are deleted. The followlast detail (a repeating end-item's loop-back
|
||||
combined with the suffix-first as ONE decision set, and an `all` member's cross to
|
||||
the other members combined likewise) was essential: a first attempt that emitted the
|
||||
loop and the suffix as SEPARATE decision sets under-detected 13 XSTS content models;
|
||||
the differential caught every one. Acceptance met: no `positionCap` and no silent
|
||||
skip; verdict-equivalent on the XSTS corpus (zero divergences);
|
||||
`SchemaDeterminismGroupBlowupTests` compiles a 2^20-position model without hanging and
|
||||
rejects an ambiguous one; XSTS `valid-schemas-rejected` 0 and `invalid-schemas-accepted`
|
||||
unchanged at 15.
|
||||
|
||||
@ -116,7 +116,7 @@ remaining release proof has two parts:
|
||||
|
||||
When both are done, Part 2 closes stopper 4 (proven bounds) and the remaining
|
||||
stopper-3 silent gap. Until then, the instance-time star-degradation is closed,
|
||||
but `positionCap` remains a named release blocker.
|
||||
`positionCap` has since been DELETED (2026-06-22): the compositional `CompositionalDeterminism` engine replaces the inlining position automaton, so determinism is checked in `O(nodes * particles^2)` with no cap and no silent skip, proven verdict-equivalent over the whole XSTS corpus.
|
||||
|
||||
## If turned into work
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user