Lyes Attouche
email: lyes.attouche@dauphine.fr

Validation of Modern JSON Schema: Formalization and Complexity

Keywords: CCS Concepts:, Theory of computation → Type theory JSON Schema, complexity of validation : 3 }, 9 { " data " : 3, " childrn " : [ ] }, 10 { " children " : [ { " data " : null }, { " childrn " : [ ] } ] }

JSON Schema is the standard language used to describe the structure of JSON documents. The standard is constantly evolving, and Draft 2019-09 added two new features, dynamic references and annotation-dependent validation. This addition changes the evaluation model, so that the versions after Draft 2019-09 are now called Modern JSON Schema, while Classical JSON Schema indicates those that precede it.

These new features solve important practical problems, but they are not easy to understand, and the modification of the evaluation model renders the theory that has been developed for Classical JSON Schema not applicable to the new versions. In this paper we face these problems. We give the first formal description of Modern JSON Schema, we then use this formal apparatus in order to study the complexity of validation for Modern JSON Schema, and we present a surprising result: with the addition of dynamic references, the problem of JSON Schema validation moves from PTIME-complete to PSPACE-hard. We also show that the problem is PSPACE-complete, by providing a polynomial space algorithm. We show that the problem is in PTIME in the special case when there is a fixed bound on the number of distinct dynamic references in each schema, by defining a deterministic polynomial time algorithm. We study the influence of schema size and of instance size, showing that the problem is PSPACE-complete with respect to the schema size, but is in PTIME when the schema is fixed and only the instance size is allowed to vary. Finally, we run experiments that show that there are schemas where the asymptotic complexity difference between dynamic and static references is extremely visible with small schemas already.

INTRODUCTION

Evolution of JSON Schema

JSON is a data language whose values are nested objects and arrays, and JSON Schema [START_REF]JSON Schema[END_REF] is the de-facto standard schema language for JSON. It is based on the combination of structural operators, describing base values, objects, and arrays, through logical operators such as disjunction, conjunction, negation, and recursive references.

JSON Schema passed through many versions, the most important being Draft-04 [START_REF] Galiegue | JSON Schema: interactive and non interactive validation -draft-fge-json-schemavalidation-00[END_REF], which was the first to be widely adopted, Draft-06 [START_REF] Wright | JSON Schema Validation: A Vocabulary for Structural Validation of JSON -draftwright-json-schema-validation-01[END_REF], which introduced extensions without changing the validation model, Draft 2019-09 [START_REF] Wright | JSON Schema Validation: A Vocabulary for Structural Validation of JSONdraft-handrews-json-schema-validation-02[END_REF], and Draft 2020-12 [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF].

The evaluation model of Draft-04 and Draft-06 is quite easy to understand and to formalize, and it has been studied in many papers, such as [START_REF] Attouche | Witness Generation for JSON Schema[END_REF][START_REF] Bourhis | JSON: Data model, Query languages and Schema specification[END_REF][START_REF] Bourhis | JSON: Data model and query languages[END_REF][START_REF] Pezoa | Foundations of JSON Schema[END_REF]. However, Draft 2019-09 introduces two important novelties to the evaluation model: annotation-dependent validation, and dynamic references; according to the terminology introduced by Henry Handrews in [START_REF] Andrews | Modern JSON Schema[END_REF], because of these modifications to the evaluation model, Draft 2019-09 is the first Draft that defines Modern JSON Schema, while the previous Drafts define variations of Classical JSON Schema. These novelties are motivated by application needs, but none of them is faithfully represented by the abstract models that had been developed and studied for Classical JSON Schema. Further, both novelties seem in need of formal clarification, as documented by many online discussions, such as [START_REF] Neal | Ambiguous behaviour of "additionalProperties" when invalid[END_REF] and [START_REF] Jacobson | The meaning of "additionalProperties" has changed[END_REF]. Draft 2020-12 [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF] is the version of Modern JSON Schema that we study in this paper.

An example of Modern JSON Schema

A JSON Schema schema is a formal specification of a validation process that can be applied to a JSON value called "the instance". A schema, such as the one in Figure 1, can contain nested schemas. A schema is either true, false, or it is an object whose fields, such as "type" : "array", are called keywords, and the term "keyword" is also used to indicate just the name of the field. Two keywords with the same parent object are said to be adjacent.

1 { " $schema " : " https : // json -schema . org / draft /2020 -12/ schema " , 2 " $id " : " https : // example . com / simple -tree " , 3 " $anchor " : " tree " , 4 " type " : " object " ,

5

" properties " : { 6 " data " : true ,

7

" children " : { 8 " type " : " array " , 9 " items " : { " $ref " : " https : // example . com / simple -tree # tree " } Looking at Figure 1, the "$schema" keyword specifies that this schema is based on Draft 2020-12. Subschemas of a JSON schema can be identified with a URI with structure baseURI•"#"•fragmentId (we use 𝑠 1 •𝑠 2 for string concatenation); the "$id" keyword assigns a base URI to its parent schema, and the "$anchor" keyword gives a fragment identifier to its parent schema, so that, in this case, the fragment named "tree" is the entire schema. Hence, this schema can be referred to as either "https://example.com/simple-tree" or as "https://example.com/simple-tree#tree".

The "type" keyword specifies that this schema only validates objects, while it fails on the other JSON types, that is, arrays and base values. The "properties" keyword specifies that, if the instance under validation contains a "data" property, then its value has no constraint, and, if it contains a "children" property, then its value must satisfy the nested subschema of lines 7-10: it must be an array whose elements (if any) must all satisfy "$ref" : "https://example.com/simple-tree#tree".

"$ref" is a reference operator that invokes a local or remote subschema, which, in this case, is the entire current schema. 1 Fig. 2. A schema representing extensible trees.

The contextual redefinition mechanism is illustrated by Figure 3. The schema "https://example.com/strict-tree" redefines the dynamic anchor "tree" (line 4), so that it now indicates a conjunction between "$ref" : "https://example.com/simple-tree#tree" and the keyword "unevaluatedProperties" : false, which forbids the presence of any property that does not match those listed in "https://example.com/simple-tree#tree". If one applies this schema, it will invoke "$ref" : "https://example.com/simple-tree#tree" (Figure 3-line 5), which will execute the schema of Figure 2 in a "dynamic scope" where "https://example.com/strict-tree" has redefined the meaning of "$dynamicRef" : "https://example.com/simple-tree#tree", because "https://example.com/strict-tree" has been met before "https://example.com/simple-tree" (this rule will be formalized in Section 3.7 and discussed in Section 4). 3 Hence, the "outermost" (or "first") schema that contains "$dynamicAnchor" : "fragmentName" is the one that fixes the meaning of that anchor for any other schema 𝑆 ′ that will invoke "$dynamicRef" : "absURI"•"#"•"fragmentName" later, independently from the absolute URI "absURI" used by 𝑆 ′ . This semantics is quite surprising, and we believe it needs a formal definition. We are going to provide that definition, and this was actually the original motivation of this work.

Annotation dependency

In Modern JSON Schema, keywords produce annotations, and the validation result of a keyword may depend on the annotations produced by adjacent keywords. These annotations carry a lot of information, but the information that is relevant for validation is which children of the current instance (that is, which properties, if it is an object, or which items, if it is an array) have already been evaluated. This information is then used by the operators "unevaluatedProperties" and "unevaluatedItems", since they are only applied to children that have not been evaluated, where the exact meaning of this term will be discussed later.

For example, in the schema of Figure 3, the assertion "unevaluatedProperties" : false depends on the annotations returned by the adjacent keyword "$ref" : "https://example.com/simple-tree#tree" (Figure 1). In this case, "$ref" evaluates all and only the fields whose name is either "data" or "children", hence "unevaluatedProperties" : false is applied to any other field, hence it fails if, and only if, fields with a different name exist.

The order in which the keywords appear in the schema is irrelevant for this mechanism; as formalized later, the result is the same as if the "unevaluatedProperties" keyword were always evaluated last among the keywords inside a same schema.

The definition of evaluated in the specifications of Draft 2020-12 ( [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF]) presents many ambiguities, as testified by online discussions such as [START_REF] Neal | Ambiguous behaviour of "additionalProperties" when invalid[END_REF] and [START_REF] Jacobson | The meaning of "additionalProperties" has changed[END_REF]. These ambiguities do not affect the final result of evaluation, but only the error messages that are generated; these aspects are discussed in Appendix G. We believe that an important contribution of this work is that it provides a precise and succinct language where this kind of ambiguities can be discussed and settled.

Our Contribution

We provide the following contributions. i) We provide a formalization of Modern JSON Schema through a set of rules that take into account both annotation-dependent validation and dynamic references (Sections 2 and 3). We implemented a corresponding validator for Modern JSON Schema written in Scala, and used it to verify their correctness using the JSON Schema standard test suite (Section 9). ii) We analyze the complexity of validating a JSON instance against a schema and show that, when dynamic references come into play, the validation problem becomes PSPACE-hard (Section 5); validation was known to be PTIME-complete for Classical JSON Schema. iii) We prove that the bound is strict, hence the problem is PSPACE-complete, by providing a polynomial space algorithm for validation (Section 6). iv) We show that annotation-dependent validation alone does not change the PTIME complexity of JSON Schema validation, by providing an explicit algorithm for Modern JSON Schema that runs in polynomial time on schemas that do not contain dynamic references (Section 7).

The algorithm actually runs in polynomial time on any family of schemas where the number of dynamic references is bounded by a constant. v) We study the data complexity of validation and prove that, when fixing a schema 𝑆, validation remains polynomial even in the presence of dynamic references. To this aim, we provide a technique to substitute dynamic references with static references, at the price of an exponential increase of the schema size (Section 8). vi) We run experiments that show that there are families of schemas where the distinction between dynamic and static references is clearly visible in the experimental result; the experiment also shows that many established validators generally exhibit an exponential behaviour also on the PTIME fragment of JSON Schema (Section 9).

FORMALIZING JSON SCHEMA SYNTAX

Introduction

For reasons of space, we only formalize here a crucial subset of Modern JSON Schema, while the rest is in Appendix A. There are two aspects of JSON Schema, URI management and keyword reordering, that we prefer to address separately from the other aspects, in order to simplify the presentation, through a "normalization process" that we define in Section 2.2; we then formalize the syntax of normalized JSON Schema in Section 2.3.

URI resolution and resource flattening

The keywords "$id", "$ref", and "$dynamicRef" accept any URI reference as value, they apply the resolution process defined in [START_REF] Berners-Lee | Uniform Resource Identifier (URI): Generic Syntax[END_REF], and they then interpret the resulting resolved URI according to JSON Schema rules. Since resolution is already specified in [START_REF] Berners-Lee | Uniform Resource Identifier (URI): Generic Syntax[END_REF], we will not formalize it here, and we will assume that, in every schema that is interpreted through our rules, the values of these three keywords have been already resolved, and that the result of that resolution has the shape absURI •"#"•fragmentId, where fragmentId may be empty for "$ref", and "$dynamicRef", and must be empty for "$id".

A "$id" : absURI keyword at the top-level of a schema object that is nested inside a JSON Schema document indicates that that object is a separate resource, identified by absURI , that is embedded inside that document but is otherwise independent. When the "$id" : absURI keyword is found in an object that is not interpreted as a schema, for example inside an unknown keyword or a non validation keyword such as "default", then it has no special meaning. The set of positions that are interpreted as schemas is defined by the grammar presented in Section 2.3.

Embedded resources are an important feature, since they allow the distribution of different resources with just one file, but they present some problems when they are nested inside arbitrary keywords, and when a reference crosses the boundaries between resources, as does "$ref" : "#/properties/foo/items" in Figure 4 (see also Section 9.2.1 of the specifications [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF]).

To avoid this kind of problems, we assume that every JSON Schema document is resource-flattened before validation. Resource flattening consists in moving every embedded resource identified as absURI into the value of a field named absURI of a "$defs" keyword at the top level of the document, and replacing the resource with an equivalent schema {"$ref" : absURI • "#"} that invokes that resource; "$defs" is a placeholder keyword that is not evaluated, but which provides a place to collect schemas that can be invoked using "$ref" or "$dynamicRef". During this phase, we also replace any reference that crosses resource boundaries with a canonical reference that directly refers the target (as suggested in Section 8.2 of the specifications [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF]) (Figure 4). Closed schemas. The input of a validation problem includes a schema 𝑆 and all schemas that are recursively reachable from 𝑆 by following the URIs used in the "$ref" and "$dynamicRef" operators. For complexity evaluation we will only consider closed schemas, that is, schemas that include all the different resources that can be recursively reached from the top-level schema (see Figure 6 for an example). There is no loss of generality, since external schemas can be embedded in a top-level one by copying them in the "$defs" section, using the "$id" operator to preserve their base URI.

JSON Schema Normalized Grammar

JSON Schema syntax is a subset of JSON syntax. We present in Figure 5 the grammar for a subset of the keywords, which is rich enough to present our results -the full grammar is in Appendix A. In this grammar, the meta-symbols are (X ) * , which is Kleene star of 𝑋 , and (X ) ? , which is an optional 𝑋 . Non-terminals are italic words, and everything else -including { [ , : ] } -are terminal symbols.

Our grammar imposes a specific order among keywords, because the result of some JSON Schema keywords depends on that of some adjacent keywords. Specifically, the two keywords in FstDep depend on some keywords in IndKey (such as "properties" and "patternProperties"), and the two keywords in SndDep depend on the keywords in FstDep, and on many keywords in IndKey, such as "properties", "patternProperties","anyOf", "allOf", "$ref", and others.

JSON Schema allows the keywords to appear in any order, and evaluates them in an order that respects the dependencies among keywords. We formalize this behaviour by assuming that, before validation, each schema is reordered to respect the grammar in Figure 5. The grammar specifies that a schema 𝑆 is either a boolean schema, or it begins with a possibly empty sequence of independent keywords or triples, followed by a possibly empty sequence of first-level dependent keywords, followed by a possibly empty sequence of second-level dependent keywords. FstDep ::= "additionalProperties" : 𝑆 | "items" : 𝑆 SndDep ::= "unevaluatedProperties" : 𝑆 | "unevaluatedItems" : 𝑆 This grammar specifies the predefined keywords, the type of the associated value (here JVal is the set of all JSON values), and their order. We do not formalize here further restrictions on patterns 𝑝, absolute URIs absURI , and fragment identifiers 𝑓 . A valid schema must also satisfy two more constraints: (1) every URI that is the argument of "$ref" or "$dynamicRef" must reference a schema, and (2) any two adjacent keywords must have different names.

𝑞

{ 𝑘 1 : 𝑆 1 , . . . , 𝑘 𝑛 : 𝑆 𝑛 } | "$ref" : absURI •"#"•f | "$dynamicRef" : absURI •"#"•f | "$

JSON SCHEMA VALIDATION

JSON data model

JSON values are either base values, or nested arrays and objects; the order of object fields is irrelevant.

𝑠 ∈ Str, 𝑑 ∈ Num, 𝑛 ∈ Int, 𝑛 ≥ 0 𝐽 ::= null | true | false | 𝑑 | 𝑠 | [ 𝐽 1 , . . . , 𝐽 𝑛 ] | { 𝑙 1 : 𝐽 1 , . . . , 𝑙 𝑛 : 𝐽 𝑛 } 𝑖 ≠ 𝑗 ⇒ 𝑙 𝑖 ≠ 𝑙 𝑗

Introduction to the proof system

We are going to define a judgment that describes the result and the annotations that are returned when a keyword 𝐾 = 𝑘 : 𝑃 is applied to an instance 𝐽 in a context 𝐶, where 𝐶 provides the information needed to interpret dynamic references. Hence, we read the following judgment

𝐶 ⊢ K 𝐽 ? 𝐾 → (𝑟, 𝜅)
as: the application of the keyword 𝐾 to the instance 𝐽 , in the context 𝐶, returns the boolean 𝑟 and the annotations 𝜅. The annotations as defined in [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF] are a complex data structure, but we only represent here the small subset that is relevant for validation, that is, the set of evaluated children, of the instance 𝐽 . The evaluated children of an object are represented by their names, and the evaluated children of an array by their position, so that:

𝐶 ⊢ K 𝐽 ? 𝐾 → (𝑟, 𝜅) ∧ 𝐽 = { 𝑘 1 : 𝐽 1 , . . . , 𝑘 𝑛 : 𝐽 𝑛 } ⇒ 𝜅 ⊆ {| 𝑘 1 , . . . , 𝑘 𝑛 | } 𝐶 ⊢ K 𝐽 ? 𝐾 → (𝑟, 𝜅) ∧ 𝐽 = [ 𝐽 1 , . . . , 𝐽 𝑛 ] ⇒ 𝜅 ⊆ {| 1, . . . , 𝑛 | } 𝐶 ⊢ K 𝐽 ? 𝐾 → (𝑟, 𝜅) ∧ 𝐽 a base value ⇒ 𝜅 = ∅
We define a similar schema judgment 𝐶 ⊢ S 𝐽 ? 𝑆 → (𝑟, 𝜅) in order to describe the result of applying a schema 𝑆 to an instance 𝐽 , and we define a list evaluation judgment 𝐶 ⊢ L 𝐽 ? [| 𝐾 1 , . . . , 𝐾 𝑛 | ] → (𝑟, 𝜅) in order to apply a list of keywords to 𝐽 , passing the annotations produced by a sublist [| 𝐾 1 , . . . , 𝐾 𝑖 | ] to the following keyword 𝐾 𝑖+1 . Observe that the letters K, S, and L that appear on top of ⊢ are not metavariables but just symbols used to differentiate the three judgments.

In the next sections we define the rules for keywords and for schemas. Keywords are called assertions when they assert properties of the analyzed instance, so that "$id" is not an assertion, while "type" is. Assertions are called applicators when they have schema parameters, such as 𝑆 1 and 𝑆 2 in "anyOf" : [𝑆 1 , 𝑆 2 ], that they apply either to the instance, in which case they are in-place applicators (e.g, "anyOf" : [𝑆 1 , 𝑆 2 ]), or to elements or items of the instance, in which case they are object applicators or array applicators (e.g., "properties" : { 𝑘 1 : 𝑆 1 , 𝑘 2 : 𝑆 2 }).

In the following sections we present the rules for "terminal" assertions, Boolean in-place applicators, and for object and array applicators. We also illustrate the rules for sequential evaluation and for the schema judgments, and finally the rules for static and dynamic references.

Terminal assertions

Terminal assertions are those that do not contain any subschema to reapply. The great majority of them are conditional on a type 𝑇 : they are trivially satisfied when the instance 𝐽 does not belong to 𝑇 , and they otherwise verify a specific condition on 𝐽 . Hence, these keyword are defined by a couple of rules, as exemplified here for the keyword "minimum" : 𝑞. The first rules always returns 𝑇 (true) when 𝐽 is not a number, while the second one, applied to numbers, returns the same boolean 𝑟 ∈ {| 𝑇 , 𝐹 | } as checking whether 𝐽 ≥ 𝑞. The set of evaluated children is ∅.

TypeOf (𝐽 ) ≠ number 𝐶 ⊢ K 𝐽 ? "minimum" : 𝑞 → (𝑇 , ∅) (minimumTriv) TypeOf (𝐽 ) = number 𝑟 = (𝐽 ≥ 𝑞) 𝐶 ⊢ K 𝐽 ? "minimum" : 𝑞 → (𝑟, ∅) (minimum)
Typed terminal assertions are completely defined by a type and a condition; a complete list of these keywords, with the associated type and condition, can be found in Appendix A.2.

We also have four type-uniform terminal assertions, that do not single out any specific type for a special treatment. They are "enum", "const", "type" : [Tp 1 , . . . , Tp 𝑛 ], and "type" : Tp. We only define here the rule for "type" : Tp, where TypeOf (𝐽 ) extracts the type of the instance 𝐽 .

𝑟 = ( TypeOf (𝐽 ) = Tp ) 𝐶 ⊢ K 𝐽 ? "type" : Tp → (𝑟, ∅) (type)
Hence, the rule for a type-uniform terminal assertion is completely defined by a boolean condition, as reported in Table 1.

Boolean applicators

JSON Schema boolean applicators apply a list of schemas to the instance, obtain a list of intermediate boolean results, and combine the intermediate results using a boolean operator. For the annotations, all assertions always return a union of the annotations produced by their subschemas, even when the assertion fails. This should be contrasted with the behaviour of schemas, where a failing schema never returns any annotation (Section 3.6). 4Hence, this is the rule for the disjunctive applicator "anyOf"; it combines the intermediate results using the ∨ operator, and a child of 𝐽 is evaluated if, and only if, it has been evaluated by any subschema 𝑆 𝑖 .

∀𝑖 ∈ {| 1 . . . 𝑛 | }. 𝐶 ⊢ S 𝐽 ? 𝑆 𝑖 → (𝑟 𝑖 , 𝜅 𝑖 ) 𝑟 = ∨({| 𝑟 𝑖 | } 𝑖 ∈ {| 1...𝑛 |} ) 𝐶 ⊢ K 𝐽 ? "anyOf" : [𝑆 1 , ..., 𝑆 𝑛 ] → (𝑟, 𝑖 ∈ {| 1...𝑛 |} 𝜅 𝑖 ) (anyOf)
The rules for "allOf" and for "not" are analogous: "allOf" is successful if all premises are successful and negation is successful if its premise fails.

∀𝑖 ∈ {| 1 . . . 𝑛 | }. 𝐶 ⊢ S 𝐽 ? 𝑆 𝑖 → (𝑟 𝑖 , 𝜅 𝑖 ) 𝑟 = ∧({| 𝑟 𝑖 | } 𝑖 ∈ {| 1...𝑛 |} ) 𝐶 ⊢ K 𝐽 ? "allOf" : [𝑆 1 , ..., 𝑆 𝑛 ] → (𝑟, 𝑖 ∈ {| 1...𝑛 |} 𝜅 𝑖 ) (allOf)
𝐶 ⊢ S 𝐽 ? 𝑆 → (𝑟, 𝜅) 𝐶 ⊢ K 𝐽 ? "not" : 𝑆 → (¬𝑟, 𝜅)

(not)

3.5 Independent object and array applicators (independent structural applicators)

Independent structural applicators are those that reapply a subschema to some children of the instance (structural) and whose behavior does not depend on adjacent keywords (independent). We start with the rules for the "patternProperties" : { 𝑝 1 : 𝑆 1 , . . . , 𝑝 𝑚 : 𝑆 𝑚 } applicator that asserts that, if 𝐽 is an object, then every property of 𝐽 whose name matches a pattern 𝑝 𝑗 has a value that satisfies 𝑆 𝑗 . This rule constraints all instance fields whose name matches any pattern 𝑝 𝑗 in the applicator, but it does not force any of the 𝑝 𝑗 's to be matched by any property name, nor any property name to match any 𝑝 𝑗 ; if there is no match, the keyword is satisfied.

We first have the trivial rule for the case when 𝐽 is not an object: non-object instances trivially satisfy the operator.

TypeOf (𝐽 ) ≠ object 𝐶 ⊢ K 𝐽 ? "patternProperties" : { 𝑝 1 : 𝑆 1 , . . . , 𝑝 𝑚 : 𝑆 𝑚 } → (𝑇 , ∅) (patternPropertiesTriv)
In the non-trivial case, where 𝐽 = { 𝑘 ′ 1 : 𝐽 1 , . . . , 𝑘 ′ 𝑛 : 𝐽 𝑛 }, we first collect the set {| (𝑖 1 , 𝑗 1 ), . . . , (𝑖 𝑙 , 𝑗 𝑙 ) | } of all pairs (𝑖, 𝑗) such that 𝑘 ′ 𝑖 ∈ 𝐿(𝑝 𝑗 ), where 𝐿(𝑝 𝑗 ) is the language of the pattern 𝑝 𝑗 . For each such pair (𝑖 𝑞 , 𝑗 𝑞 ), we collect the boolean 𝑟 𝑞 that specifies whether 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 𝑗 𝑞 holds or not, and the entire keyword is successful over 𝐽 if the conjunction 𝑟 = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) is 𝑇 . According to the standard convention, the empty conjunction ∧({| | }) evaluates to 𝑇 , hence this rule does not force any matching.

111:10

The evaluated properties are all the properties 𝑘 𝑖 𝑞 for which a corresponding pattern 𝑝 𝑖 𝑞 exists, independently of the result 𝑟 𝑞 of the corresponding validation, and independently of the overall result 𝑟 of the keyword. Observe that the sets 𝜅 𝑞 of the children that are evaluated in the subproofs are discarded; this happens because elements of 𝜅 𝑞 are children of a child 𝐽 𝑖 𝑞 of 𝐽 ; we collect information about the evaluation of the children of 𝐽 , and are not interested in children of children.

𝐽 = { 𝑘 ′ 1 : 𝐽 1 , . . . , 𝑘 ′ 𝑛 : 𝐽 𝑛 } {| (𝑖 1 , 𝑗 1 ), . . . , (𝑖 𝑙 , 𝑗 𝑙 ) | } = {| (𝑖, 𝑗) | 𝑘 ′ 𝑖 ∈ 𝐿(𝑝 𝑗 ) | } ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 𝑗 𝑞 → (𝑟 𝑞 , 𝜅 𝑞 ) 𝑟 = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) 𝐶 ⊢ K 𝐽 ? "patternProperties" : { 𝑝 1 : 𝑆 1 , . . . , 𝑝 𝑚 : 𝑆 𝑚 } → (𝑟, {| 𝑘 ′ 𝑖 1 , . . . , 𝑘 ′ 𝑖 𝑙 | }) (patternProperties)
The rule for "properties" : { 𝑘 1 : 𝑆 1 , . . . , 𝑘 𝑚 : 𝑆 𝑚 } is essentially the same, with equality 𝑘 ′ 𝑖 = 𝑘 𝑗 taking the place of matching 𝑘 ′ 𝑖 ∈ 𝐿(𝑝 𝑗 ); also in this case, no name match is required, but, if a match happens, then the corresponding child of 𝐽 must satisfy the subschema with the same name.

𝐽 = { 𝑘 ′ 1 : 𝐽 1 , . . . , 𝑘 ′ 𝑛 : 𝐽 𝑛 } {| (𝑖 1 , 𝑗 1 ), . . . , (𝑖 𝑙 , 𝑗 𝑙 ) | } = {| (𝑖, 𝑗) | 𝑘 ′ 𝑖 = 𝑘 𝑗 | } ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 𝑗 𝑞 → (𝑟 𝑞 , 𝜅 𝑞 ) 𝑟 = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) 𝐶 ⊢ K 𝐽 ? "properties" : { 𝑘 1 : 𝑆 1 , . . . , 𝑘 𝑚 : 𝑆 𝑚 } → (𝑟, {| 𝑘 ′ 𝑖 1 , . . . , 𝑘 ′ 𝑖 𝑙 | }) (properties)
Of course, we also have the trivial rule (propertiesTriv), analogous to rule (patternPropertiesTriv): when 𝐽 is not an object, "properties" is trivially satisfied. The rules for the other independent object applicators, and for the independent array applicators, can be found in Appendix A.

The independent keywords presented in this section (and in the previous one) produce (respectively, collect and transmit) annotations that influence the behavior of the dependent keywords, which are "additionalProperties", "items", "unevaluatedProperties", and "unevaluatedItems". These dependencies are formalized in the next sections.

3.6

The semantics of schemas: sequential evaluation of keywords 3.6.1 Schemas and sequential evaluation. We have defined the semantics of the independent keywords. We now introduce the rules for schemas and for the sequential executions of keywords.

The rules for the true and false schemas are trivial.

𝐶 ⊢ S 𝐽 ? true → (𝑇 , ∅) (trueSchema) 𝐶 ⊢ S 𝐽 ? false → (𝐹, ∅) (falseSchema)
The rule for an object schema

{ ì 𝐾 } is based on the keyword-list judgment 𝐶 ⊢ L 𝐽 ? ì 𝐾 ì 𝑟 → 𝜅,
which applies the keywords in the ordered list ì 𝐾, passing the annotations from left to right. Rule (schema-false) specifies that, as dictated by [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF], when schema validation fails, no annotation is passed, hence no instance child is regarded as evaluated. This is a crucial difference with keywords, since the 𝐶 ⊢ K 𝐽 ? 𝐾 → (𝑟, 𝜅) judgment may return non empty annotations even when 𝑟 = 𝐹 .5

𝐶 ⊢ L 𝐽 ? [| 𝐾 1 , . . . , 𝐾 𝑛 | ] → (𝑇 , 𝜅) 𝐶 ⊢ S 𝐽 ? { 𝐾 1 , . . . , 𝐾 𝑛 } → (𝑇 , 𝜅) (schema-true) 𝐶 ⊢ L 𝐽 ? [| 𝐾 1 , . . . , 𝐾 𝑛 | ] → (𝐹, 𝜅) 𝐶 ⊢ S 𝐽 ? { 𝐾 1 , . . . , 𝐾 𝑛 } → (𝐹, ∅) (schema-false)
We now describe the rules for the sequential evaluation judgment 𝐶 ⊢ L 𝐽 ? ì 𝐾 → (𝑟, 𝜅). The rules are specified for each list ì 𝐾 + 𝐾 by induction on ì 𝐾 and by cases on 𝐾. We start with the crucial rule, that for ì 𝐾 + "unevaluatedProperties" : 𝑆. To evaluate ì 𝐾 + "unevaluatedProperties" : 𝑆 we first evaluate ì 𝐾, which yields a set of evaluated children 𝜅, we then evaluate 𝑆 on the other children, and we combine the results by conjunction. We return every property as evaluated.

𝐽 = { 𝑘 1 : 𝐽 1 , . . . , 𝑘 𝑛 : 𝐽 𝑛 } 𝐶 ⊢ L 𝐽 ? ì 𝐾 → (𝑟, 𝜅) {| 𝑖 1 , . . . , 𝑖 𝑙 | } = {| 𝑖 | 1 ≤ 𝑖 ≤ 𝑛 ∧ 𝑘 𝑖 ∉ 𝜅 | } ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 → (𝑟 𝑞 , 𝜅 𝑞 ) 𝑟 ′ = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) 𝐶 ⊢ L 𝐽 ? ( ì 𝐾 + "unevaluatedProperties" : 𝑆) → (𝑟 ∧ 𝑟 ′ , {| 𝑘 1 . . . , 𝑘 𝑛 | }) (unevaluatedProperties)
The rule for ì 𝐾 +"additionalProperties" : 𝑆 is identical, apart from the fact that we only eliminate the properties that have been evaluated by adjacent keywords. The specifications [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF] indicate that this information should be passed as annotation, but that a static analysis is acceptable if it gives the same result. We formalize this second approach since it is slightly simpler. We define a function propsOf( ì 𝐾) that extracts all the patterns and all the names that appear in any "properties" and "patternProperties" keywords that appear in ì 𝐾 and combines them into a pattern; a property is directly evaluated by a keyword in ì 𝐾 if, and only if, it belongs to 𝐿(propsOf( ì 𝐾)). The notation k i used in the first line indicates a pattern whose language is {| 𝑘 𝑖 | }; ∅ in the third line is a pattern such that 𝐿(∅) = ∅.

propsOf("properties" : { 𝑘 1 : 𝑆 1 , . . . , 𝑘 𝑚 :

𝑆 𝑚 }) = k 1 •"|"•. . .•"|"•k n propsOf("patternProperties" : { 𝑝 1 : 𝑆 1 , . . . , 𝑝 𝑚 : 𝑆 𝑚 }) = 𝑝 1 •"|"•. . .•"|"•𝑝 𝑚 propsOf(𝐾 ) = ∅ otherwise propsOf( [| 𝐾 1 , . . . , 𝐾 𝑛 | ]) = propsOf(𝐾 1 ) •"|"•. . .•"|"•propsOf(𝐾 𝑛 )
The keyword "additionalProperties" was already present in Classical JSON Schema, and it does not really depends on the annotations passed by the previous keywords, but only on information that can be statically extracted from "properties" and "patternProperties"; critically, it is not influenced by what is evaluated by an adjacent "$ref", as happens to "unevaluatedProperties" in the example of Figure 3. Modern JSON Schema introduced "unevaluatedProperties" in order to overcome this limitation.

𝐽 = { 𝑘 1 : 𝐽 1 , . . . , 𝑘 𝑛 : 𝐽 𝑛 } 𝐶 ⊢ L 𝐽 ? ì 𝐾 → (𝑟, 𝜅) {| 𝑖 1 , . . . , 𝑖 𝑙 | } = {| 𝑖 | 1 ≤ 𝑖 ≤ 𝑛 ∧ 𝑘 𝑖 ∉ 𝐿(propsOf( ì 𝐾)) | } ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 → (𝑟 𝑞 , 𝜅 𝑞 ) 𝑟 ′ = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) 𝐶 ⊢ L 𝐽 ? ( ì 𝐾 + "additionalProperties" : 𝑆) → (𝑟 ∧ 𝑟 ′ , {| 𝑘 1 . . . , 𝑘 𝑛 | }) (additionalProperties)
The rules for "unevaluatedItems" : 𝑆 and "items" : 𝑆 are similar, and they can be found in Appendix A.

Having exhausted the rules for dependent keywords, we have a catch-all rule for all other keywords, that says that, when 𝐾 is an independent keyword, we combine the results of 𝐶 ⊢ L 𝐽 ? ì 𝐾 → (𝑟 𝑙 , 𝜅 𝑙 ) and 𝐶 ⊢ K 𝐽 ? 𝐾 → (𝑟, 𝜅), but no information is passed between the two judgments.

𝐾 ∈ IndKey 𝐶 ⊢ L 𝐽 ? ì 𝐾 → (𝑟 𝑙 , 𝜅 𝑙 ) 𝐶 ⊢ K 𝐽 ? 𝐾 → (𝑟, 𝜅) 𝐶 ⊢ L 𝐽 ? ( ì 𝐾 + 𝐾) → (𝑟 𝑙 ∧ 𝑟, 𝜅 𝑙 ∪ 𝜅) (klist-(n+1))
Since the above rule is inductive, we need a terminal rule for the case of an empty list of keywords.

𝐶 ⊢ L 𝐽 ? [| | ] → (𝑇 , ∅) (klist-0)
111:12

Static and dynamic references

The "$ref" and "$dynamicRef" in-place applicators allow a URI-identified subschema to be applied to the current instance, but the two applicators interpret the URI in a very different way.

As specified in Section 2.2, we assume that the parameter of any "$ref" and "$dynamicRef" is a resolved URI with structure absUri•"#"•fragmentId, where the fragment identifier may be empty; "$ref" : absURI • "#" • fragmentId retrieves the resource 𝑆 identified by absUri, which may be the current schema or a different one, retrieves the subschema 𝑆 ′ of 𝑆 identified by fragmentId, and applies 𝑆 ′ to the current instance 𝐽 .

The application of absUri •"#"•fragmentId changes the dynamic scope; this fact is recorded by extending the context 𝐶 in the premise with absUri. The context 𝐶 is the ordered list of the absolute URIs of the "dynamic scopes" that have been met by the current branch of the validation proof, and is used to interpret dynamic references -in the rule, 𝐿 + 𝑒 denotes the operation of adding an element 𝑒 at the end of a list 𝐿.

𝑆 ′ = get(load(absURI ), f ) 𝐶 + absURI ⊢ S 𝐽 ? 𝑆 ′ → (𝑟, 𝜅) 𝐶 ⊢ K 𝐽 ? "$ref" : absURI •"#"•f → (𝑟, 𝜅) ($ref)
Here, load(absURI ) returns the schema 𝑆 identified by absURI , an operation that we cannot formalize since the standards leave it undefined [START_REF] Berners-Lee | Uniform Resource Identifier (URI): Generic Syntax[END_REF][START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF]. get(𝑆, f ) returns the subschema identified by 𝑓 inside 𝑆; the fragment 𝑓 may either be empty, hence identifying the entire 𝑆, or a plain-name, which is matched by a corresponding "$anchor" operator inside 𝑆, 6 or a JSON Pointer, that begins with "/" and is interpreted by navigation -the get function is formally defined in Appendix B.

For simplicity, we assume that the schema has already been analyzed to ensure the following properties; it would not be difficult to formalize these conditions in the rules:

(1) the load function will not fail;

(2) the get function will not fail;

(3) every "$id" operator assigns to its schema a URI that is different from the URI of any other resource recursively reachable from its schema. The applicator "$dynamicRef" is very different, and is defined as follows (see [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF] Section 8.2.3.2):

If the initially resolved starting point URI includes a fragment that was created by the "$dynamicAnchor" keyword, the initial URI MUST be replaced by the URI (including the fragment) for the outermost schema resource in the dynamic scope (Section 7.1) that defines an identically named fragment with "$dynamicAnchor". Otherwise, its behavior is identical to "$ref", and no runtime resolution is needed. This sentence is not easy to decode, but it means that, given an assertion "$dynamicRef" : absURI • "#"•f , one first verifies whether the resource referenced by the "starting point URI" absURI contains a dynamic anchor "$dynamicAnchor" : 𝑓 ′ with 𝑓 ′ = 𝑓 . In this is the case, "$dynamicRef" : absURI•"#"•f will be interpreted according to the dynamic interpretation specified in the second part of the sentence, otherwise it will be interpreted as if it were a static reference "$ref"; this verification is formalized by the premises dget(load(absURI ), f ) ≠ ⊥ and dget(load(absURI ), f ) = ⊥ of the two rules that we present below for "$dynamicRef". The function dget(𝑆, 𝑓 ) looks inside 𝑆 for a subschema that contains "$dynamicAnchor" : 𝑓 , but it returns ⊥ if there is no such subschema. 7 After this check is passed, the dynamic interpretation focuses on the fragment 𝑓 , and it looks for the first (the "outermost") resource in 𝐶 + that contains a subschema identified by "$dynamicAnchor" : 𝑓 , where 𝐶 + is the dynamic context 𝐶 extended with the initial URI absURI .

We formalize this specification using two functions: dget(𝑆, f ) and fstURI(𝐶, f ). The function dget(𝑆, f ) returns the subschema 𝑆 ′ that is identified in 𝑆 by a plain-name f that has been defined by "$dynamicAnchor" : "f", and returns ⊥ when no such subschema is found in 𝑆, and its definition is given in Appendix B. The function fstURI(𝐿, f ) returns the first URI in the list 𝐿 that defines 𝑓 , that is, such that dget(load(absURI ), f ) ≠ ⊥:

fstURI( [| | ], f ) = ⊥ fstURI(absURI + 𝐿, f ) = absURI if dget(load(absURI ), f ) ≠ ⊥ fstURI(absURI + 𝐿, f ) = fstURI(𝐿, f ) if dget(load(absURI ), f ) = ⊥
We can finally formalize the dynamic reference rule. It first checks that the initial URI refers to a dynamic anchor, but, after this check, the result of load(absURI ) is forgotten. Instead, we look for the first URI fURI in 𝐶 + absURI where the dynamic anchor 𝑓 is defined, and we extract the corresponding subschema 𝑆 ′ by executing dget(load(fURI ), 𝑓 ).

dget(load(absURI ), f ) ≠ ⊥ fURI = fstURI(𝐶 + absURI, 𝑓 ) 𝑆 ′ = dget(load(fURI ), f ) 𝐶 + fURI ⊢ S 𝐽 ? 𝑆 ′ → (𝑟, 𝜅) 𝐶 ⊢ K 𝐽 ? "$dynamicRef" : absURI •"#"•f → (𝑟, 𝜅) ($dynamicRef)
Remark 1. Observe that fstURI(𝐶 + absURI, 𝑓 ) searches fstURI into a list that contains the dynamic context extended with the URI absURI . We have the impression that the specifications, that we copied above, would rather require fURI = fstURI(𝐶, 𝑓 ), but we contacted the specification authors, and we checked some online verifiers that are widely adopted, and there seems to be a general agreement that fURI = fstURI(𝐶 + absURI, 𝑓 ) is the correct formula (see Appendix C for a concrete example). We do not really understand where the specifications would mandate to search into absURI as well, and the current version of the official test cases (as for 26 𝑡ℎ Jan. 2023) does not help us resolving the ambiguity, but this is not essential, since none of our theoretical results is affected by this choice.

On the other side, we believe that these difficulties in the interpretation of the natural language specifications are a further indication of the relevance of a formal specification.

The second rule for "$dynamicRef" applies when the initially resolved starting point URI does not include a fragment that was created by the "$dynamicAnchor" keyword, hence "$dynamicRef" behaves as "$ref".

dget(load(absURI ), f ) = ⊥ 𝑆 ′ = get(load(absURI ), f ) 𝐶 + absURI ⊢ S 𝐽 ? 𝑆 ′ → (𝑟, 𝜅) 𝐶 ⊢ K 𝐽 ? "$dynamicRef" : absURI •"#"•f → (𝑟, 𝜅) ($dynamicRefAsRef)

Compressing the context by saturation

The only rule that depends on the context 𝐶 is rule ($dynamicRef) that uses fstURI(𝐶 + absURI, 𝑓 ) to retrieve the first 𝑈 𝑅𝐼 in 𝐶 + absURI that identifies a schema where f identifies a dynamic fragment. For this operation, when 𝑈 𝑅𝐼 is already present in 𝐶, its addition at the end of 𝐶 is irrelevant; for each 𝑈 𝑅𝐼 we could just retain its first occurrence in 𝐶. Let us define 𝐶+?𝑈 𝑅𝐼 , that we read as 𝐶 saturated with 𝑈 𝑅𝐼 , as 𝐶+?𝑈 𝑅𝐼 = 𝐶 when 𝑈 𝑅𝐼 ∈ 𝐶 and 𝐶+?𝑈 𝑅𝐼 = 𝐶 + 𝑈 𝑅𝐼 when 𝑈 𝑅𝐼 ∉ 𝐶. By the observation above, we can substitute 𝐶 + 𝑈 𝑅𝐼 with 𝐶+?𝑈 𝑅𝐼 in the premises of rules ($ref), ($dynamicRef), and ($dynamicRefAsRef), obtaining, for example the following rule.

dget(load(absURI ), f ) ≠ ⊥ fURI = fstURI(𝐶+?absURI, 𝑓 ) 𝑆 ′ = dget(load(fURI ), f ) 𝐶+?fURI ⊢ S 𝐽 ? 𝑆 ′ → (𝑟, 𝜅) 𝐶 ⊢ K 𝐽 ? "$dynamicRef" : absURI •"#"•f → (𝑟, 𝜅) ($dynamicRef 𝑐 )
This observation will be crucial in our complexity evaluations, hence, from now on, we adopt saturation in the reference rules, and we assume that contexts are URI lists with no repetition.

DYNAMIC REFERENCES AS A PARAMETRIZATION MECHANISM

Dynamic references look like a data parametrization mechanism, similar to the 𝑋 variable in a classical List < X > data structure, but with a peculiar instantiation mechanism. While parametric data structures such as List < X > are usually instantiated by parameter-passing, as in newList < Integer > () (Java syntax), dynamic references are instantiated by giving a first definition, as we do in Figure 2 for the "#tree" dynamic anchor, and by refining it later on, as we do in Figure 3, where we recall the original definition and add an extra condition "unevaluatedProperties" : false. Here, "later on" describes the typical order in which one would design this piece of code; crucially, the order is inverted at run-time, when we would invoke "https://example.com/strict-tree#tree" first, and this order would cause the definition in "https://example.com/strict-tree" to overwrite the definition in "https://example.com/tree". Hence, dynamic references are not "instantiated" by parameter passing, but rather "overwritten", in a way that is driven by invocation order. For this reason, they resemble self parametrization in object-oriented languages, where the structure is first defined in a superclass, is later refined in subclasses, and the programmer can decide which version to use, which will depend on their entry-point, that is, on which class they choose to instantiate. A further parallelism with object-oriented inheritance is the emphasis on refinement: in many standard examples, the new definition of a dynamic reference invokes the previous definition and adds more constraints, as we do in Figure 3; this looks very similar to inheritance, where the subclass refines the superclass.

This peculiar instantiation mechanism is related to the intended application of dynamic references. Dynamic references have been introduced (as "recursiveRef") in Draft 2019-09 as a refinement mechanism for recursive data structures, as in our example. The driving example was the metaschema of JSON Schema, that is, a schema specifying what is a well formed JSON Schema schema. If you consider the grammar in Figure 5, they needed a mechanism to describe, in JSON Schema, that grammar, together with different extensions. That mechanism had to allow different extensions to that grammar to be specified, each one adding its own cases, and all of them recursively interpreting 𝑆 according to a combination of all different extensions [START_REF]JSON Schema meta-schema[END_REF] (core metaschema). Hence, the mechanism has not been designed to support "parametric data types", but rather "refinable recursive data types", which explains the reliance on "rebinding" rather than "parameter passing".

PSPACE HARDNESS: USING DYNAMIC REFERENCES TO ENCODE A QBF SENTENCE

Dynamic references add a seemingly minor twist to the validation rules, but this twist has a dramatic effect on validation complexity. We prove here that dynamic references make validation PSPACEhard, by reducing quantified Boolean formulas (QBF) validity, a well-known PSPACE-complete problem [START_REF] Stockmeyer | The Polynomial-Time Hierarchy[END_REF][START_REF] Stockmeyer | Word Problems Requiring Exponential Time: Preliminary Report[END_REF], to JSON Schema validation. In detail, we encode an arbitrary closed QBF formula 𝜓 as a schema 𝑆 𝜓 whose size is linear in 𝜓 and with the property that, given any JSON instance 𝐽 , the assertion [| 𝑏 | ] ⊢ S 𝐽 ? 𝑆 𝜓 , where b is the base URI of 𝑆 𝜓 , holds if, and only if, 𝑆 𝜓 is valid. Observe that the actual value of 𝐽 is irrelevant: the schema 𝑆 𝜓 is either satisfied by any instance, or by none at all. In our encoding we use a Boolean subset of JSON Schema, which only includes "$ref", "$anchor", "$dynamicRef", "$dynamicAnchor", "anyOf", "allOf", true, and false, where true, "$ref", and "$anchor" are only used to improve readability: every "anyOf" : [true] could just be removed, while "$ref" and "$anchor" could be substituted by "$dynamicRef" and "$dynamicAnchor". We start with an example. Consider the following QBF formula: ∀𝑥1. ∃𝑥2. (𝑥1∧¬𝑥2) ∨ (¬𝑥1∧𝑥2); Figure 6 shows how it can be encoded as a JSON Schema schema.

1 { 2 " $schema " : " https : // json -schema . org / draft /2020 -12/ schema " , 3 " $id " : " urn : psi " , 4 " $ref " : " urn : start # forall . x1 " ,

5

" $defs " : { 6 " urn : start " : { 7 " $id " : " urn : start " , 8 " $defs " : { 9 " forall . x1 " : { " $anchor " : " forall . x1 " , " allOf " : [ { " $ref " : " urn : setvar1 # afterq1 " } , { " $ref " : " urn : start # afterq1 " } ] } , " exists . x2 " : { " $anchor " : " exists . x2 " , " anyOf " : [ { " $ref " : " urn : setvar2 # afterq2 " } , { " $ref " : " urn : start # afterq2 " } ] } , " afterq1 " : { " $anchor " : " afterq1 " , " $ref " : " urn : start # exists . x2 " } , " afterq2 " : { " $anchor " : " afterq2 " , " $ref " : " urn : close # phi " } } } , " urn : setvar1 " : { " $id " : " urn : setvar1 " , " $defs " : { " afterq1 " : { " $anchor " : " afterq1 " , " $ref " : " urn : start # exists . x2 " } , " x1 " :

{ " $dynamicAnchor " : " x1 " , " anyOf " : [ true ] } , " not . x1 " : { " $dynamicAnchor " : " not . x1 " , " anyOf " : [ false ] } } } , " urn : setvar2 " : { " $id " : " urn : setvar2 " , " $defs " : { " afterq2 " : { " $anchor " : " afterq2 " , " $ref " : " urn : close # phi " } , " x2 " :

{ " $dynamicAnchor " : " x2 " , " anyOf " : [ true ] } , " not . x2 " : { " $dynamicAnchor " : " not . x2 " , " anyOf " : [ false ] } } } , " urn : close " : { " $id " : " urn : close " , " $defs " : { " x1 " : { " $dynamicAnchor " : " x1 " , " anyOf " : [ false ] } , " not . x1 " : { " $dynamicAnchor " : " not . x1 " , " anyOf " : [ true ] } , " x2 " :

{ " $dynamicAnchor " : " x2 " , " anyOf " : [ false ] } , " not . x2 " : { " $dynamicAnchor " : " not . x2 " , " anyOf " : [ true ] } , " phi " : { " $anchor " : " phi " , " anyOf " : [ { " allOf " : [ { " $dynamicRef " : "urn:close# x1 " } , { " $dynamicRef " : "urn:close# not . x2 " } ] } , { " allOf " : [ { " $dynamicRef " : "urn:close# not . x1 " } , { " $dynamicRef " : "urn:close# x2 " } ] } ] } } } } } Fig. 6. Encoding ∀𝑥1. ∃𝑥2. (𝑥1 ∧ ¬𝑥2) ∨ (¬𝑥1 ∧ 𝑥2) as a JSON Schema.

For each variable 𝑥𝑖 we define a resource "urn:setvar" •𝑖 (lines 23-30 and 31-38 of Figure 6), each defining two dynamic schemas, one with plain-name "x" •𝑖 and value true, and the other one with plain-name "not.x"•𝑖 and value false 8 (lines [START_REF] Stockmeyer | The Polynomial-Time Hierarchy[END_REF][START_REF] Stockmeyer | Word Problems Requiring Exponential Time: Preliminary Report[END_REF][35][36]. The body of the formula to evaluate is defined in the "phi" property inside a resource "urn:close" (line 46-55). All variables in "urn:close#phi" are encoded as dynamic references, so that their value depends on the resources that are in-scope at the moment of the formula evaluation. If the context of the evaluation of the formula "urn:close"#"phi"includes the resource "urn:setvar" •𝑖, then this resource is in the context before the resource "urn:close", hence "$dynamicRef" : "urn:close#x" •𝑖 resolves to the true subschema defined there. If the context of the evaluation does not include the resource "urn:setvar" • 𝑖, then "urn:close#x" • 𝑖 resolves to the schema defined for 𝑥𝑖 inside the "urn:close" resource, whose value is false.

Now we describe how we encode the quantifiers. The first quantifier is encoded inside the "urn:start" resource. If the quantifier is ∀, as in this case, then we apply "allOf" to two references (lines 9-13), one that checks whether the rest of the formula holds when 𝑥1 is true, by invoking "urn:setvar1#afterq1", which sets 𝑥1 to true by bringing "urn:setvar1" in scope, and the second one that evaluates the rest of the encoding in a context that does not contain "urn:setvar1", so that 𝑥1 will be set to false by the definition that is provided by "urn:close".

The existential quantifier is encoded exactly in the same way (lines 14-18), with the only difference that we use "anyOf", so that "urn:start#exists.x2" holds if the rest of the formula holds for at least one boolean value of 𝑥2. This technique allows one to encode any QBF formula. The size of the "urn:start" part of that schema is linear in the number of variables. Each "urn:setvar"•𝑖 resource has a constant size, and their number is linear in the number of variables. Finally, the "urn:close" resource contains a part whose size is linear in the number of variables and a second part whose size is linear with the rest of the formula. Hence, the size of the entire schema is linear in the size of the encoded sentence.

We now formalize this encoding. We substitute the names "#forall.x"•𝑖 and "#exists.x"•𝑖, used in the example, with "#quant.x"•𝑖, in order to simplify the description and the proofs.

Definition 1 (𝑆 𝜓 ). Consider a generic closed QBF formula:

𝜓 = 𝑄 1 𝑥 1 . . . 𝑄 𝑛 𝑥 𝑛 . 𝜙
where 𝑄 𝑖 ∈ {| ∀, ∃ | } and 𝜙 is generated by:

𝜙 ::= 𝑥 𝑖 | ¬𝑥 𝑖 | 𝜙 ∨ 𝜙 | 𝜙 ∧ 𝜙 .
The schema 𝑆 𝜓 contains 𝑛 + 3 resources: "urn:psi" (the root), "urn:start", "urn:setvar"•1, . . . , "urn:setvar"• 𝑛, and "urn:close", and its root contains the only assertion "$ref" : "urn:start#quant.x1"

The "urn:start" resource contains, for each 𝑥 𝑖 , two subschemas, named "urn:start#quant.x"•𝑖 and "urn:start#afterq"•𝑖. Every named subschema has a "$anchor" or a "$dynamicAnchor" keyword that assigns it a name, and an assertion that we call its "body". The body of "urn:start#quant.x" • 𝑖 is boolOp : [ {"$ref" : "urn:setvar"•𝑖 •"#afterq"•𝑖} , {"$ref" : "urn:start#afterq"•𝑖} ] where boolOp = "allOf" when 𝑄 𝑖 = ∀, and boolOp = "anyOf" when 𝑄 𝑖 = ∃. The body of "urn:start#afterq"•𝑖 is "$ref" : "urn:start#quant.x"•(𝑖+1) when 𝑖 < 𝑛 and is "$ref" : "urn:close#phi" when 𝑖 = 𝑛.

Each "urn:setvar"•𝑖 resource contains 3 subschemas: "afterq"•𝑖, "x"•𝑖, and "not.

x"•𝑖. The body of "afterq"•𝑖 is equal to the body of "urn:start#afterq"•𝑖; the body of "x"•𝑖 is "anyOf" : [true], and the body of "not.x"•𝑖 is "anyOf" : [false].

8 More precisely, it is "anyOf" : [false], since we cannot add an anchor to a schema that is just false; "anyOf" : [true] in the body of "x" •𝑖 is clearly redundant, and is there only for readability.

Finally, the "urn:close" resource contains, for each variable 𝑥 𝑖 , two subschemas, named "urn:close#x"• 𝑖 and "urn:close#not.x"•𝑖, and a schema "phi". The body each "x"•𝑖 is "anyOf" : [false], and the body of each "not.x"•𝑖 is "anyOf" : [true]. For a formula 𝑄 1 𝑥 1 . . . 𝑄 𝑛 𝑥 𝑛 . 𝜙, the body of "phi" is 𝑆 𝜙 , which is recursively defined as follows:

𝑆 𝑥 𝑖 = {"$dynamicRef" : "urn:close#x"•𝑖} 𝑆 ¬𝑥 𝑖 = {"$dynamicRef" : "urn:close#not.x"•𝑖} 𝑆 𝜙 1 ∨𝜙 2 = "anyOf" : [ 𝑆 𝜙 1 , 𝑆 𝜙 2 ] 𝑆 𝜙 1 ∧𝜙 2 = "allOf" : [ 𝑆 𝜙 1 , 𝑆 𝜙 2 ].
The following theorem, whose proof is in Appendix D, states the correctness of the translation.

Theorem Since the encoding has linear size, PSPACE-hardness is an immediate corollary; as already discussed, true, "$ref", and "$anchor" are not really necessary to our encoding.

Corollary 3 (PSPACE-hardness).

Validation in any fragment of Modern JSON Schema that includes "$dynamicRef", "$dynamicAnchor", "anyOf", "allOf", and false, is PSPACE-hard.

VALIDATION IS IN PSPACE

After we established that validation of dynamic references is PSPACE-hard, we show here that the bound is tight, by exhibiting a validation algorithm that runs in polynomial space. To this aim, we consider the algorithm that applies the typing rules through recursive calls, using a list of already-met subproblems in order to cut infinite loops.

The algorithm is specified in Figure 1. For each schema, it evaluates its keywords, passing the current value of the boolean result and of the evaluated children from one keyword to the next one. Independent keywords (such as "anyOf" and "patternProperties") execute their own rule and update the current result and the current evaluated items using conjunction and union, as dictated by rule (klist-(n+1)), while each dependent keyword, (such as "unevaluatedProperties"), updates these two values as specified by its own rule.

In Algorithm 1 we exemplify one in-place independent applicator ("anyOf"), one in-place applicator that updates the context ("$dynamicRef"), one structural independent applicator ("patternProperties"), and one dependent applicator ("unevaluatedProperties").

Function SchemaValidate (Context, Instance, Schema, StopList) applies Schema in the context Context, that is a list of absolute URIs without repetitions, to Instance, and uses StopList in order to avoid infinite recursion. The Context list is extended by evaluation of dynamic and static references using the function Saturate (Context, URI ) (line 31), which adds URI to Context only if it is not already there. The StopList records the (Context, Instance, Schema) triples that have been met in the current call stack. It stops the algorithm when the same triple is met twice in the same evaluation branch, which prevents infinite loops, since any infinite branch must find the same triple infinitely many times, because every instance and schema that is met is a subterm of the input, and only finitely many different contexts can be generated.

We prove now that this algorithm runs in polynomial space. To this aim, the key observation is the fact that we have a polynomial bound of the length of the call stack. The call stack is a sequence of alternating tuples SchemaValidate (Context, Instance, Schema, StopList) -KeywordValidate (. . . ) -k(...) -SchemaValidate (Context', Instance', Schema', StopList'), where 𝑘(. . . ) is the keywordspecific function invoked by KeywordValidate. We focus on the sequence of SchemaValidate (Context, Instance, Schema, StopList) tuples, ignoring the intermediate calls. This sequence can be divided in at most 𝑛 subsequences, if 𝑛 is the input size, the first one with a context that only contains one URI, the second one with contexts with two URIs, and the last one having a number of URIs that is bound by the input size, since no URI is repeated twice in a context. In each subsequence all the (Instance, Schema) pairs are different, since the stoplist test would otherwise raise a failure. Since every instance in a call stack tuple is a subinstance of the initial one, and every schema is a subschema of the initial one, we have at most 𝑛 2 elements in each subsequence, hence the entire call stack never exceeds 𝑛 3 . We finally observe that every single function invocation can be executed in polynomial space plus the space used by the functions that it invokes, directly and indirectly; the result follows, since we have seen that these functions are never more than 3 * 𝑛 3 at the same time. This is the basic idea behind the following Theorem, whose full proof can be found in Appendix D. Since our algorithm runs in polynomial space, the problem of validation for Modern JSON Schema is PSPACE-complete.

Theorem 4. For any closed schema 𝑆 and instance 𝐽 whose total size is less than 𝑛, Algorithm 1 applied to 𝐽 and 𝑆 requires an amount of space that is polynomial in 𝑛.

POLYNOMIAL TIME VALIDATION FOR STATIC REFERENCES

While dynamic references make validation PSPACE-hard, annotation-dependent validation alone does not change the PTIME complexity of Classical JSON Schema validation. We prove this fact here by defining an optimized variant of Algorithm 1 that runs in polynomial time in situations where there is a fixed bound on the maximum number of dynamic references, hence, a fortiori, for schemas where no dynamic reference is present.

Our optimized algorithm exploits a memoization technique. To this aim, it returns, from each evaluation of 𝑆 over 𝐽 in a context 𝐶, not only the boolean result and the evaluated children, but also a DFragSet, that specifies which dynamic fragments have been resolved during that evaluation. For each evaluated judgment 𝐶 ⊢ S 𝐽 ? 𝑆 → (𝑟, 𝜅), we write the tuple (𝐶, 𝐽, 𝑆, 𝑟, 𝜅, DFragSet) in an updatable store. When, during the same validation, we evaluate again 𝐽 and 𝑆 in an arbitrary context 𝐶 ′ , we retrieve any previous evaluation with the same pair (𝐽, 𝑆), and we verify whether the new 𝐶 ′ is equivalent to the context 𝐶 used for that evaluation, with respect to the set of fragments that have been actually evaluated, reported in the DFragSet; here equivalent means that, for each fragment 𝑓 in DFragSet, fstURI(𝐶, 𝑓 ) and fstURI(𝐶 ′ , 𝑓 ) coincide. If the two contexts are equivalent, then we do not recompute the result, but we just return the previous (𝑟, 𝜅, DFragSet) triple. It is easy to prove that, when the number of different dynamic references is bounded, this equivalence relation has a number of equivalence classes that is polynomial in the size of 𝑆, hence that memoization limits the number of recursive call below a polynomial bound.

For simplicity, in our algorithm we keep the UpdatableStore and the StopList separated; it would not be difficult to merge them in a single data structure that can be used for the purposes of both. We show here how SchemaValidate changes from Algorithm 1. In Appendix E we also report how KeywordValidate is modified.

This optimized algorithm returns the same result as the base algorithm, and runs in polynomial time if the number of different dynamic fragments is limited by a fixed bound. The proofs can be found in Appendix D.

Theorem 5. Algorithm 2 applied to (𝐶, 𝐽, 𝑆, ∅, ∅) returns (𝑟, 𝜅, 𝑑), for some 𝑑, if, and only if, 𝐶 ⊢ S 𝐽 ? 𝑆 → (𝑟, 𝜅). Theorem 6. Consider a family of closed schemas 𝑆 and judgments 𝐽 such that (|𝑆 | + |𝐽 |) ≤ 𝑛, and let 𝐷 be the set of different fragments 𝑓 that appear in the argument of a "$dynamicRef" : initURI •"#"•f in 𝑆. Then, Algorithm 2 runs on 𝑆 and 𝐽 in time 𝑂 (𝑛 𝑘+|𝐷 | ) for some constant 𝑘. Corollary 7. Validation is in PTIME for every family of schemas where the maximum number of different fragments that are argument of "$dynamicRef" is bounded by a constant.

PTIME DATA COMPLEXITY THROUGH ELIMINATION OF DYNAMIC REFERENCES

As we have seen, dynamic references change the computational and algebraic properties of JSON Schema. We define here a process to eliminate dynamic references, by substituting them with static references; this allows us to reuse results and algorithms that have been defined for Classical JSON Schema. Specifically, we will prove here that dynamic references can be eliminated from a schema, and substituted with static references, at the price of a potentially exponential increase in the size of the schema. This entails that the data complexity of the problem is polynomial (Corollary 9).

A dynamic reference "$dynamicRef" : initURI • "#" • f is resolved, during validation, to a URI reference fstURI(𝐶+?initURI, 𝑓 ) • "#" • f that depends on the context 𝐶 of the validation (Section 3.7), so that the same schema 𝑆 behaves in different ways when applied in different contexts. This context-dependency extends to static references: a static reference "$ref" : absURI •"#"•f is always resolved to the same subschema, however, when this subschema invokes some dynamic reference, directly or through a chain of static references, then the validation behaviour of this subschema depends on the context, as happens with "$ref" : "urn:close#phi" in our example, which is a static reference, but the behaviour of the schema it refers to depends on the context.

To obtain the same effect without dynamic references, we observe that, once the context 𝐶 is fixed, then every dynamic reference has a fixed behaviour, and it can be encoded using a static reference "$ref" : fstURI(𝐶+?initURI, 𝑓 ) •"#"•f . Every dynamic reference can be eliminated if we iterate this process by defining, for each subschema 𝑆 ′ and for each context 𝐶, a context-injected version CI(𝐶, 𝑆 ′ ), which describes how 𝑆 ′ behaves when the context is 𝐶. The context-injected CI(𝐶, 𝑆 ′ ) is obtained by (1) substituting in 𝑆 ′ every dynamic reference "$dynamicRef" : initURI•"#"•f with a static reference to the context-injected version of the schema identified by fstURI(𝐶+?initURI, 𝑓 ) •"#"•f , and (2) substituting every static reference "$ref" : absURI • "#" • f with a static reference to the context-injected version of the schema identified by absURI •"#"•f . Step ( 2) is crucial, since a static reference may recursively invoke a dynamic one, hence the context must be propagated through the static references.

Before giving a formal definition of the process that we outlined, we start with an example. Consider the context 𝐶 = [| "urn:psi", "urn:start", "urn:setvar1" | ] and a reference "$ref" : "urn:close#phi", which refers to the following schema 𝑆 ′ that contains four dynamic references.

1 " urn : close # phi " : { 2 " $anchor " : " phi " ,

3 " anyOf " : [ 4 { " allOf " : [ { " $dynamicRef " : "urn:close# x1 " } , 5
{ " $dynamicRef " : "urn:close# not . x2 " } ] } ,

6

{ " allOf " : [ { " $dynamicRef " : "urn:close# not . x1 " } ,

7 { " $dynamicRef " : "urn:close# x2 " } ] } 8 ] 9 }
The corresponding context-injected schema CI(𝐶, 𝑆 ′ ) is the following one. When a schema is identified by absURI •"#"•f , we identify its context-injected version CI(𝐶, 𝑆 ′ ) using absURI •"#"•𝐶 •f , where 𝐶 is an invertible encoding of 𝐶 into a plain-name.9

1 " urn : close # urn : psi_urn : start_urn : setvar1_phi " : { 2 " $anchor " : " urn : psi_urn : start_urn : setvar1_phi " , Let us use 𝐶 + to abbreviate 𝐶+?"urn:close". Observe that, in CI(𝐶, 𝑆 ′ ), all dynamic references have been substituted with static references, which depend on the context 𝐶: for example, "x1" in line 4 has a URI that starts with "urn:setvar1", which is fstURI(𝐶 + , "x1"), while "x2" in line 7 has a URI that starts with "urn:close", which is fstURI(𝐶 + , "x2"). The fragment name of a static reference, such as "urn:psi_urn:start_urn:setvar1_phi", encodes both the injected context ("urn:psi_..._urn:setvar1_") and the original fragment name ( "_phi").

Observe that the injected context of the "$ref"'s in lines 4-7 extends "urn:psi_..._urn:setvar1_" with "urn:close_". This corresponds to what happens in the rule ($dynamicRef):

dget(load(absURI ), f ) ≠ ⊥ fURI = fstURI(𝐶+?absURI, 𝑓 ) 𝑆 ′ = dget(load(fURI ), f ) 𝐶+?fURI ⊢ S 𝐽 ? 𝑆 ′ → (𝑟, 𝜅) 𝐶 ⊢ K 𝐽 ? "$dynamicRef" : absURI •"#"•f → (𝑟, 𝜅) ($dynamicRef)
The rule dictates that the schema 𝑆 ′ must be analyzed in the extended context 𝐶 + , not in the original context. Hence, in CI(𝐶, 𝑆 ′ ), each dynamic reference to "urn:close#"•𝑓 ′ 𝑖 has been substituted with a static reference to the context-injected schema CI(𝐶 + , fstURI(𝐶

+ , 𝑓 ′ 𝑖 ) •"#"•f ′ i ), whose URI- reference is fstURI(𝐶 + , 𝑓 ′ 𝑖 ) •"#"•𝐶 + •f ′ i .
The complete unfolding is in Appendix F.

We can now give a formal definition of the translation process. For simplicity, we assume that all fragment identifiers are plain-names defined using "$anchor" or "$dynamicAnchor", without loss of generality, since JSON Pointers can be easily translated using the anchor mechanism.

Given a judgment 𝑆 0 with base URI 𝑏, we first define a "local" translation function CI that maps every pair (𝐶, 𝑆), where 𝐶 is a list of URIs from 𝑆 0 without repetitions and 𝑆 is a subschema of 𝑆 0 , into a schema without dynamic references, and that maps every pair (𝐶, 𝐾) to a keyword without dynamic references. This function maps references as specified below, and acts as an homomorphism on all the other operators, as exemplified here with "anyOf".

CI(𝐶, "$dynamicRef" : absURI

•"#"•f ) = "$ref" : fstURI(𝐶+?absURI, f ) •"#"•𝐶 •f CI(𝐶, "$ref" : absURI •"#"•f ) = "$ref" : absURI •"#"•𝐶 •f CI("anyOf" : [ 𝑆 1 , . . . , 𝑆 𝑛 ])
= "$ref" : "anyOf" : [ CI(𝐶, 𝑆 1 ), . . . , CI(𝐶, 𝑆 𝑛 ) ]

. . .

Consider now a schema 𝑆 0 and the set C of all possible contexts, that is, of all lists with no repetitions of absolute URIs of resources inside 𝑆 0 ; a fragment of 𝑆 0 is any subschema that defines a static or a dynamic anchor (e.g., the subschema identified by "urn:close#phi" is a fragment). The static translation of 𝑆 0 , Static(𝑆 0 ), is obtained by substituting, in 𝑆 0 , each fragment 𝑆 𝑓 identified by absURI •"#"•f with many fragments 𝐶 •f , one for any context 𝐶 ∈ C, where the schema identified by each absURI • "#" •𝐶 • f is CI(𝐶, 𝑆 𝑓 ), as exemplified in Appendix F. 10 If we have 𝑛 𝑈 absolute URIs in 𝑆 0 , we have Σ 𝑖 ∈ {| 0...𝑛 𝑈 |} (𝑖!) lists of URIs without repetitions, hence, if we have 𝑛 𝑓 fragments, the possible (𝐶, 𝑆 𝑓 ) pairs are (Σ 𝑖 ∈ {| 0...𝑛 𝑈 |} (𝑖!)) × 𝑛 𝑓 , which is included between 𝑛 𝑈 ! × 𝑛 𝑓 and (𝑛 𝑈 + 1)! × 𝑛 𝑓 . This last formula gives an exponential upper bound, or, more precisely, an upper bound in 𝑂 (2 𝑛 •log 𝑛 ). In practice, the number of reachable schemas will be much smaller, but our example shows that it can actually be exponential.

We can now prove that this process preserves schema behaviour; the proof is in Appendix D.

Theorem 8 (Encoding correctness). Let 𝑆 be a closed schema with base URI b. Then:

[| b | ] ⊢ S 𝐽 ? Static(𝑆) → (𝑟, 𝜅) ⇔ [| b | ] ⊢ S 𝐽 ? 𝑆 → (𝑟, 𝜅)
As an immediate consequence of this construction, and of the polynomiality of validation in JSON Schema without dynamic references, we have the fact that validation in Modern JSON Schema has an 𝑂 (2 𝑛 •log 𝑛 ) upper bound when the schema size is considered, but is polynomial when the schema is fixed and it is only the instance that varies. This is an important result, reminiscent of data complexity in query evaluation, but the parallelism is not precise: while queries are smaller than data in most application fields, there are many situations where JSON Schema documents are generally bigger than the checked instances, for example when complex schemas are used in order to validate function parameters, that may be quite small. Corollary 9 (Instance complexity). When 𝑆 is fixed, the validation problem

[| 𝑏 | ] ⊢ S 𝐽 ? 𝑆 → (𝑟, 𝜅) is in PTIME.

EXPERIMENTS

We implemented Algorithm 2 for the entire JSON Schema language. This algorithm applies the rules in Appendix A. Our Scala implementation can be accessed (anonymously) as an online tool from 10 We say that a translated fragment absURI •"#" •𝐶 •f refers another translated fragment if the schema of the first contains a reference to the second; when we translate a schema 𝑆 0 , we do not actually need to generate every possible fragment absURI •"#" •𝐶 •f , but we only need to translate those that are recursively reachable from the root fragment b

•"#" • [| 𝑏 |] •𝑆 0 ;
this is exemplified in the translation of our example, in Appendix F, where we only translate the context-fragment pairs that are reachable. https://validationproofs.oa.r.appspot.com/. 11 We further make the schemas used in our experiments available (see below).

Correctness of formalization

We applied our algorithm to the official JSON Schema test suite [START_REF] Bergman | JSON-Schema-Test-Suite[END_REF]. 12 We pass all tests apart from those that contain references to external files (concerning 24 schemas out of 345, at the time of writing). These references must be resolved at runtime, a feature that we do not yet support. This is merely a technical limitation that we plan to overcome within the upcoming weeks.

Discussion. This experiment proves that the rules that we presented, and which are faithfully reflected by our algorithm, are correct and complete with respect to the standard test suite.

Complexity

We have proved that validation in Modern JSON Schema is PSPACE-complete in the presence of dynamic references, while it is in PTIME when dynamic references are not present. In the upcoming experiment, we test (1) whether there exist families of schemas where this difference is reflected by considerable validation times, and (2) whether they already manifest with small schemas.

Schemas. We designed three families of schemas that are universally satisfiable, and we validate the JSON instance null against them.

The family of schemas from "dyn1.js" up to "dyn100.js" generalizes our running example; the file "dyn"•𝑖•".js" contains the encoding of

∀𝑥 1 . ∃𝑥 2 . . . . ∀𝑥 2𝑖 . ∃𝑥 2𝑖+1 . ((𝑥 1 ∧ 𝑥 2 ) ∨ (¬𝑥 1 ∧ ¬𝑥 2 )) ∧ . . . ∧ ((𝑥 2𝑖 ∧ 𝑥 2𝑖+1 ) ∨ (¬𝑥 2𝑖 ∧ ¬𝑥 2𝑖+1 ))
as defined in Section 5. We then have a corresponding family of Draft-04 schemas "stat1.js" up to "stat100.js", where dynamic references are substituted with static references, and boolean schemas true and false are substituted with { } and { "not" : { } }.

The third family of schemas, from "dyn.bounded1.js" up to "dyn.bounded100.js", encodes

∀𝑥 1 . ∃𝑥 2 . . . . ∀𝑥 2𝑖 . ∃𝑥 2𝑖+1 . ((𝑥 1 ∧ 𝑥 2𝑖+1 ) ∨ (¬𝑥 1 ∧ ¬𝑥 2𝑖+1 )).
These "dynamic-bounded" schemas, hence, contain dynamic references that respect the condition of Corollary 7, which allows an optimized algorithm to run in polynomial time.

We provide the schemas online: https://anonymous.4open.science/r/modern-jsonschema-908C/.

Validators. For running third-party validators, we employ the meta-validator Bowtie [START_REF] Bergman | Bowtie JSON Schema Meta Validator[END_REF], which invokes validators encapsulated in Docker containers. We tested all 14 different open-source validators currently provided by Bowtie, written in 10 different programming languages, as detailed in Table 2, Appendix H. We also prepared a container for the validator from [START_REF] Pezoa | Foundations of JSON Schema[END_REF], to include it in our experiments.

Execution environment. Our execution environment is a 40-core Debian server with 384MB of RAM. Each core runs with with 3.1Gz and CPU frequency set to performance mode. We are running Docker version 20.10.12, Bowtie version 0.67.0, and Scala version 2.12.

All runtimes with Bowtie were measured with GNU time, averaged over three runs, and include the overhead of invoking Bowtie and Docker. We overrode the default timeout setting in Bowtie. Our Scala implementation was run outside of Bowtie ("solo"). Here, we measure at the level of 111:24 microseconds, from within the Scala code. Out of 5 such runs for each experiment, we discard the smallest and the largest runtime (to ignore caching effects), and average over the remaining three.

Lines in our plots terminate when either the validator produces a logical validation error, a runtime exception (most commonly, a stack overflow), or when Bowtie reported that the validator did not respond. Results. The results in Figure 7 are perfectly coherent with the theoretical results in the paper. Results on the "dyn" and "stat" schemas show that, on this specific example, the difference in the asymptotic complexity of the static and the dynamic version is extremely visible: if we focus on our validator (red line), we see that validation with dynamic references can become impractical even with reasonably-sized files (e.g., schema "stat5.js" counts fewer than 250 lines when prettyprinted), while the runtime remains very modest when dynamic references are substituted with static references. The runtime on the "bounded" family reflects Corollary 7, showing the effectiveness of the proposed optimization on this specific example.

The results on the other implementations strongly suggest that many validators have chosen to implement an algorithm that is exponential even when no dynamic reference is present. This is not surprising for the validators designed for Draft 2020-12, since we have been the first to describe an algorithm (Algorithm 2) that runs in polynomial time over the static fragment of Draft 2020-12. It is a bit more surprising for the algorithm published as additional material for [START_REF] Pezoa | Foundations of JSON Schema[END_REF], since it implements Draft-04, which belongs to Classical JSON Schema, whose validation problem is in PTIME, as proved for the first time in that same paper.

Discussion. This experiment shows there are families of schemas where the PSPACE-hardness of the problem is visible, and that the algorithm we describe in Section 7 is extremely effective when the dynamic references are substituted with static references, or limited in number. In this paper we focus on worst-case asymptotic complexity, and we do not present claims about real-world relevance of our algorithm, which is an important issue, but is not in the scope of this paper.

RELATED WORK

To the best of our knowledge, modern JSON Schema has not been formalized before, nor validation in the presence of dynamic references has been studied.

Overviews over schema languages for JSON can be found in [START_REF] Baazizi | Schemas And Types For JSON Data[END_REF][START_REF] Baazizi | Schemas and Types for JSON Data: From Theory to Practice[END_REF][START_REF] Bourhis | JSON: Data model, Query languages and Schema specification[END_REF][START_REF] Pezoa | Foundations of JSON Schema[END_REF]. In [START_REF] Pezoa | Foundations of JSON Schema[END_REF] Pezoa et al. proposed the first formalization of Classical JSON Schema Draft-04 and studied the complexity of validation. They proved that JSON Schema Draft-04 expressive power goes beyond MSO and tree automata, and showed that validation is PTIME-complete. They also described and experimentally analyzed a Python validator that exhibits good performance and scalability. Their formalization of semantics and validation, however, cannot be extended to modern JSON Schema due to the presence of dynamic references.

In [START_REF] Bourhis | JSON: Data model, Query languages and Schema specification[END_REF] Bourhis et al. refined the analysis of Pezoa et al. They mapped Classical JSON Schema onto an equivalent modal logic, called recursive JSL, and studied the complexity of validation and satisfiability. In particular, they proved that validation for recursive JSL and Classical JSON Schema is PTIME-complete and that it can be solved in 𝑂 (|𝐽 | 2 |𝑆 |) time; then they showed that satisfiability for Classical JSON Schema is EXPTIME-complete for schemas without uniqueItems and is in 2EXPTIME otherwise. Again, their approach does not seem very easy to extend to modern JSON Schema, as it relies on modal logic and a very special kind of alternating tree automata.

While we are not aware of any other formal study about JSON Schema validation, dozens of validators have been designed and implemented in the past (please, see [START_REF]JSON Schema validators[END_REF] for a rather complete list of about 50 implementations). Only some of them (about 11), like ajv [START_REF]Ajv JSON Schema validator[END_REF] and Hyperjump [START_REF]Hyperjump JSON Schema Validator[END_REF], support modern JSON Schema and dynamic references. These validators, usually compile schemas in an efficient internal representation, that is later used for validation purposes. ajv, for instance, uses modern code generation techniques and compiles a schema into a specialized validator, designed to support advanced v8 optimization.

Validation has been widely studied in the context of XML data (see [START_REF] Martens | Complexity of Decision Problems for XML Schemas and Chain Regular Expressions[END_REF][START_REF] Martens | Expressiveness and complexity of XML Schema[END_REF], for instance). However, schema languages for XML are based on regular expressions, while JSON Schema exploits record types, recursion, and full boolean logics, and this makes it very difficult to import techniques from one field to the other.

Schema languages such as JSON Schema and type systems for functional languages are clearly related, and a lot of work has been invested in the analysis of the computational complexity of type checking and type inference for programming languages and for module systems (we will only cite [START_REF] Henglein | The Complexity of Type Inference for Higher-Order Typed lambda Calculi[END_REF], as an example). We are well aware of this research field, but we do not think that it is related to this specific work, since in that case the focus is on the analysis of code while JSON Schema validation analyses instances of data structures.

CONCLUSIONS AND OPEN PROBLEMS

Modern JSON Schema introduced annotation-dependent validation and dynamic references, which are widely regarded as complex additions, and which changed the evaluation model, hence invalidating the theory developed for Classical JSON Schema.

Here we provide the first published formalization for Modern JSON Schema. This formalization provides a language to unambiguously describe and discuss the standard, and a tool to understand its subtleties.

We use our formalization to study the complexity of validation of Modern JSON Schema. We proved that the problem is PSPACE-complete, and that a very small fragment of the language is already PSPACE-hard. We proved that this increase in asymptotic complexity is caused by dynamic references, while annotation-dependent validation without dynamic references can be decided in PTIME, and we have defined and implemented and experimented an explicit algorithm to this aim.

We defined a technique to eliminate dynamic references, at the price of a potential exponential increase in the schema size, and we used it to prove that data-complexity of validation is in PTIME.

We leave many open problems, such as the definition of a new notion of schema equivalence and inclusion that is compatible with annotation-dependent validation, the study of its properties, and the study of the computational complexity of the problems of satisfiability, validity, inclusion, and example generation. The complete grammar groups the keywords "if"-"then"-"else", and specifies that the presence of any keyword among "if"-"then"-"else" implies the presence of "then" and "else", which is enforced by adding a trivial "then" : {}, or "else" : {}, when one or both are missing; this presentation reduces the number of rules needed to formalize "if"-"then"-"else". In the same way, the grammar groups "contains"-"minContains"-"maxContains" and imposes the presence of "minContains" when any of the three is present, which is enforced by adding the default "minContains" : 1 when "minContains" is missing.

A.2 Terminal keywords

The types and the conditions of the terminal keywords are specified in the following table. There, the length operator |𝐽 | counts the number of characters of a string, the number of fields of an object, and the number of elements of an array. names(J) extracts the names of an object. When 𝑝 is a pattern or a format, we use 𝐿(𝑝) to indicate the corresponding set of strings.

When TypeOf (kw) is no type then the assertion does not have the (kwTriv) rule and does not have the condition TypeOf (𝐽 ) = TypeOf (kw) in the (kw) rule. assertion kw:J' TypeOf (kw) cond(J,kw:J') number 𝐽 > 𝑞 "exclusiveMaximum": q number 𝐽 < 𝑞 "minimum": q number J ≥ q "maximum": q number J ≤ q "multipleOf": q number ∃𝑖 ∈ Int. 𝐽 = 𝑖 × 𝑞 "pattern": p dget(𝑆, 𝑓 ) searches inside 𝑆 for a subschema { "$dynamicAnchor" : 𝑓 , 𝐾 1 , . . . , 𝐾 𝑛 } and returns it. However, it only searches inside known keywords that contain a schema as a parameter, and the search is stopped by the presence of an internal "$id" keyword, because "$id" indicates that the subschema is a separate resource, with a different URI. We formalize this behaviour by defining two functions:

) | } = {| (𝑖, 𝑗) | 𝑘 ′ 𝑖 ∈ 𝐿(𝑝 𝑗 ) | } ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 𝑗 𝑞 → (𝑟 𝑞 , 𝜅 𝑞 ) 𝑟 = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) 𝐶 ⊢ K 𝐽 ? "patternProperties" : { 𝑝 1 : 𝑆 1 , . . . , 𝑝 𝑚 : 𝑆 𝑚 } → (𝑟, {| 𝑘 ′ 𝑖 1 , . . . , 𝑘 ′ 𝑖 𝑙 | }) (patternProperties) 𝐽 = { 𝑘 ′ 1 : 𝐽 1 , . . . , 𝑘 ′ 𝑛 : 𝐽 𝑛 } {| (𝑖 1 , 𝑗 1 ), . . . , (𝑖 𝑙 , 𝑗 𝑙 ) | } = {| (𝑖, 𝑗) | 𝑘 ′ 𝑖 = 𝑘 𝑗 | } ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 𝑗 𝑞 → (𝑟 𝑞 , 𝜅 𝑞 ) 𝑟 = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙
𝐽 = { 𝑘 ′ 1 : 𝐽 1 , . . . , 𝑘 ′ 𝑚 : 𝐽 𝑚 } {| 𝑖 1 , . . . , 𝑖 𝑙 | } = {| 𝑖 | 𝑖 ∈ {| 1 . . . 𝑛 | }, 𝑘 𝑖 ∈ {| 𝑘 ′ 1 , . . . , 𝑘 ′ 𝑚 | } | } ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 ? 𝑆 𝑖 𝑞 → 𝜅 𝑞 𝑟 = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) 𝐶 ⊢ K 𝐽 ? "dependentSchemas" : { 𝑘 1 : 𝑆 1 , . . . , 𝑘 𝑛 : 𝑆 𝑛 } → (𝑟, 𝑞 ∈ {| 1...𝑙 |} 𝜅 𝑞 ) (dependentSchemas)
𝑚 }) = k 1 •"|"•. . .•"|"•k n propsOf("patternProperties" : { 𝑝 1 : 𝑆 1 , . . . , 𝑝 𝑚 : 𝑆 𝑚 }) = 𝑝 1 •"|"•. . .•"|"•𝑝 𝑚 propsOf(𝐾 ) = ∅ otherwise propsOf( [| 𝐾 1 , . . . , 𝐾 𝑛 | ]) = propsOf(𝐾 1 ) •"|"•. . .•"|"•propsOf(𝐾 𝑛 ) 𝐽 = { 𝑘 1 : 𝐽 1 , . . . , 𝑘 𝑛 : 𝐽 𝑛 } 𝐶 ⊢ L 𝐽 ? ì 𝐾 → (𝑟, 𝜅) {| 𝑖 1 , . . . , 𝑖 𝑙 | } = {| 𝑖 | 1 ≤ 𝑖 ≤ 𝑛 ∧ 𝑘 𝑖 ∉ 𝐿(propsOf( ì 𝐾)) | } ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 → (𝑟 𝑞 , 𝜅 𝑞 ) 𝑟 ′ = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) 𝐶 ⊢ L 𝐽 ? ( ì 𝐾 + "additionalProperties" : 𝑆) → (𝑟 ∧ 𝑟 ′ , {| 𝑘 1 . . . , 𝑘 𝑛 | }) (additionalProperties) 𝐽 = { 𝑘 1 : 𝐽 1 , . . . , 𝑘 𝑛 : 𝐽 𝑛 } 𝐶 ⊢ L 𝐽 ? ì 𝐾 → (𝑟, 𝜅) {| 𝑖 1 , . . . , 𝑖 𝑙 | } = {| 𝑖 | 1 ≤ 𝑖 ≤ 𝑛 ∧ 𝑘 𝑖 ∉ 𝜅 | } ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 → (𝑟 𝑞 , 𝜅 𝑞 ) 𝑟 ′ = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) 𝐶 ⊢ L 𝐽 ? ( ì 𝐾 + "unevaluatedProperties" : 𝑆) → (𝑟 ∧ 𝑟 ′ , {| 𝑘 1 . . . , 𝑘 𝑛 | }) (unevaluatedProperties
| } = {| 1 . . . 𝑛 | } \ {| 1 . . . maxPrefixOf ( ì 𝐾) | } ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 → 𝜅 𝑞 𝑟 ′ = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) 𝐶 ⊢ L 𝐽 ? ( ì 𝐾 + "items" : 𝑆) → (𝑟 ∧ 𝑟 ′ , {| 1 . . . , 𝑛 | }) (items) 𝐽 = [ 𝐽 1 , ..., 𝐽 𝑛 ] 𝐶 ⊢ L 𝐽 ? ì 𝐾 → (𝑟, 𝜅) {| 𝑖 1 , . . . , 𝑖 𝑙 | } = {| 1 . . . 𝑛 | } \ 𝜅 ∀𝑞 ∈ {| 1 . . . 𝑙 | }. 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 → 𝜅 𝑞 𝑟 ′ = ∧({| 𝑟 𝑞 | } 𝑞 ∈ {| 1...𝑙 |} ) 𝐶 ⊢ L 𝐽 ? ( ì 𝐾 + "unevaluatedItems" : 𝑆) → (𝑟 ∧ 𝑟 ′ , {| 1 . . . , 𝑛 | }) (unevaluatedItems) 𝑘 : 𝐽 ′ ∈ IndKeyOrT 𝐶 ⊢ L 𝐽 ? ì 𝐾 → (𝑟 𝑙 , 𝜅 𝑙 ) 𝐶 ⊢ K 𝐽 ? 𝐾 → (𝑟, 𝜅) 𝐶 ⊢ L 𝐽 ? ( ì 𝐾 + 𝐾) → (𝑟 𝑙 ∧ 𝑟, 𝜅 𝑙 ∪ 𝜅) (klist-(n+1)) 𝐶 ⊢ L 𝐽 ? [| | ] → (𝑇 , [| | ]) (klist-0) A.8
(1) dgets(𝑆, 𝑓 ), that searches "$dynamicAnchor" : 𝑓 into 𝑆, and, if not found, invokes dgetk(𝑘 : 𝐽, 𝑓 ) on each keyword 𝑘 : 𝐽 to search inside the schema; (2) dgetk(𝑘 : 𝐽, 𝑓 ) that invokes dgets(𝑆, 𝑓 ) to search 𝑓 inside the parts of 𝐽 that are known to contain a subschema. The function dget(𝑆, 𝑓 ) is defined as dgets(StripId(𝑆), 𝑓 ), where StripId(𝑆) removes any outermost "$id" keyword from 𝑆. This is necessary since dgets interrupts its search when it meets a "$id" keyword, but the presence of an "$id" in the outermost schema should not interrupt the search:

StripId({ "$id" : 𝑈 𝑅𝐼, ì 𝐾 }) = { ì 𝐾 } StripId(𝑆)

= 𝑆 otherwise

The assertion "$ref" : "urn:start#afterq" •𝑛 evaluates "$ref" : "urn:close#phi" in the same context 𝐶, hence 𝐴 𝐶 sets 𝑥 𝑛 to 𝐹 , since 𝐼𝑛𝑑 (𝐶) ≤ 𝑛 -1. Hence, by property ( 2 The assertion "$ref" : "urn:start#afterq"• (𝑛 -𝑖 + 1) evaluates "urn:start#quant.x"• (𝑛 -𝑖 + 2) in the same context 𝐶 with 𝐼𝑛𝑑 (𝐶) ≤ 𝑛 -𝑖, hence 𝐴 𝐶 sets 𝑥 𝑛-𝑖+1 to 𝐹 , by definition of 𝐴 𝐶 .

We rewrite (𝑛 -𝑖 + 2) as (𝑛 -(𝑖 -1) + 1) and we observe that 𝐼𝑛𝑑 (𝐶) ≤ 𝑛 -𝑖 implies that 𝐼𝑛𝑑 (𝐶 + "urn:setvar"•(𝑛 -𝑖 + 1)) ≤ 𝑛 -(𝑖 -1), so that we can apply induction on 𝑖, which provides the following inductive hypothesis: 𝐶 + "urn:setvar"• (𝑛 -𝑖 + 1) ⊢ S 𝐽 ? { "$ref" : "urn:start#quant. Theorem 4. For any closed schema 𝑆 and instance 𝐽 whose total size is less than 𝑛, Algorithm 1 applied to 𝐽 and 𝑆 requires an amount of space that is polynomial in 𝑛.

Proof. We first prove that the call stack has a polynomial depth, thanks to the following properties, where we use 𝑛 for the size of the input instance, and 𝑚 for the size of the input schema.

(1) The depth of the call stack is always less than |StopList| × 3.

(2) Each StopList generated during validation can be divided in 𝑀 distinct sublists 𝑠𝑙 1 , . . . , 𝑠𝑙 𝑀 , such that all elements in the same sublist have the same context, and the context of the sublist 𝑠𝑙 𝑖+1 , with 𝑖 ≥ 1, contains one more URI than the context of the sublist 𝑠𝑙 𝑖 . (3) The size of each sublist 𝑠𝑙 𝑖 is at most 𝑛 × 𝑚.

Property (1) holds since SchemaValidate(. . . ,StopList) invokes KeywordValidate with a stoplist with length |StopList| + 1, and KeywordValidate invokes a rule-specific function that may invoke SchemaValidate with the same stoplist, so that the StopList grows by 1 every time the call stack grows by 3, and vice versa.

Property (2) holds by induction: the function SchemaValidate passes to KeywordValidate the same context it receives, and the function KeywordValidate passes to SchemaValidate either the same context it receives or a context that contains one more URI, which happens when the keyword analyzed is either "$ref" or "$dynamicRef" and the target URI was not yet in the context. Property (3) holds since no two elements of the stoplist can be equal, since a failure is raised when the input is already in the StopList parameter. All elements in a sublist have the same context, hence they must differ either in the instance or in the schema. The instance must be a sub-instance of the input instance, hence we have at most 𝑛 choices. The schema must must be a sub-schema of the input schema, hence we have at most 𝑚 choices. Hence, the size of each sublist 𝑠𝑙 𝑖 is at most 𝑛 × 𝑚.

The combination of these three properties implies that the StopList parameter contains at most (𝑛 × 𝑚) × (𝑚 + 1) elements, since it can be decomposed in at most 𝑚 + 1 sublists, which implies that this parameter has a polynomial size, and that the call stack, by property (1), has a polynomial depth.

We now provide the rest of the proof, which is quite straightforward. We observe that SchemaValidate (Context,Instance,Schema,StopList) scans all keywords inside Schema in sequence, and it only needs enough space to keep the pair (Result,Eval) between one call and the other one, and the size of this pair is in 𝑂 (𝑛), since the list Eval of evaluated properties or items cannot be bigger than the instance. Since we reuse the same space for all keywords, we only need to prove that each single keyword can be recursively evaluated in polynomial space, including the space needed for the call stack and for the parameters.

Every keyword has its own specific algorithm, some of which are exemplified in Figure 1. We first analyze "patternProperties". All the four parameters can be stored in polynomial space; Context since it is a list of URIs that belong to the schema and because it contains no repetition, and the other parameters have already be discussed. Each matching pair can be analyzed in polynomial space, apart from the recursive call. For the recursive call, the call stack has a polynomial length, and every called function employs polynomial space.

We need to repeat the same analysis for all rules, but none of them is more complex than "patternProperties". For example, the dependent keywords such as "unevaluatedProperties" have one extra parameter that contains the already evaluated properties and items, but it only takes polynomial space, as already discussed.

This completes the proof of the fact that the algorithm runs in polynomial space, hence the problem of validation for JSON Schema 2020-12 is PSPACE-complete. □ Theorem 5. Algorithm 2 applied to (𝐶, 𝐽, 𝑆, ∅, ∅) returns (𝑟, 𝜅, 𝑑), for some 𝑑, if, and only if, 𝐶 ⊢ S 𝐽 ? 𝑆 → (𝑟, 𝜅).

Proof. In the following proof, we use the following metavariables conventions:

• 𝑠𝑙 (stoplist) denotes a list of triples (𝐶, 𝐽, 𝑆)

document builds a mental model about the internal logics of JSON Schema, and the way they define a schema, or the way they implement a validator, are guided by this mental model. If the mental model is unclear, or ambiguous, their work becomes more complicated then it should be.

H LIST OF DOWNLOADED VALIDATORS

List of the validators from Section 9.

18 }

 18 Fig. 1. A schema representing trees.

Fig. 3 .

 3 Fig.3. A schema that refines trees.

Fig. 4 .

 4 Fig. 4. A schema with embedded resources and its flattened version.

  ∈ Num, 𝑖 ∈ Int, 𝑘 ∈ Str, absURI ∈ Str, 𝑓 ∈ Str, format ∈ Str, 𝑝 ∈ Str, 𝐽 ∈ JVal Tp ::= "object" | "number" | "integer" | "string" | "array" | "boolean" | "null" S ::= true | false | { IndKey (, IndKey) * (, FstDep) * (, SndDep) * } | { FstDep (, FstDep) * (, SndDep) * } | { SndDep (, SndDep) * } | { } IndKey ::= "minimum" : 𝑞 | "maximum" : 𝑞 | "pattern" : 𝑝 | "required" : [ 𝑘 1 , . . . , 𝑘 𝑛 ] | "type" : Tp | "$id" : absURI | "$defs" :

Fig. 5 .

 5 Fig. 5. Minimal grammar of normalized JSON Schema Draft 2020-12.

19 20 21 Result := True; 22 for

 192122 Equivalent (Context,OldContext,DFragSet) f in DFragSet do Result := And (Result, (FirstURI (Context,f) ==FirstURI (OldContext,f))); 23 return (Result);

8 ]

 8 " : [ { " $ref " : " urn : setvar1 # urn : psi_urn : start_urn : setvar1_urn : close_x1 " } , 5 { " $ref " : " urn : close # urn : psi_urn : start_urn : setvar1_urn : close_not . x2 " } ] } , 6 { " allOf " : [ { " $ref " : " urn : setvar1 # urn : psi_urn : start_urn : setvar1_urn : close_not . x1 " } , 7 { " $ref " : " urn : close # urn : psi_urn : start_urn : setvar1_urn : close_x2 " } ] }

Fig. 7 .

 7 Fig. 7. Runtimes of validators on the three schema families. Distinguishing validators that support Draft 4, Draft 2020, as well as our algorithm "modern-jsonschema". The inlet shows a closeup of modern-jsonschema.

Fig. 8 .

 8 Fig. 8. Complete grammar of normalized JSON Schema Draft 2020-12.

  𝑖"required" : [ 𝑘 1 , .

  ), 𝐶 ⊢ S 𝐽 ? { "$ref" : "urn:close#phi" } → 𝑇 ⇔ 𝑉 𝑎𝑙𝑖𝑑 (𝜙, 𝐴 𝐶 ) ⇔ 𝑉 𝑎𝑙𝑖𝑑 (𝜙, 𝐴 𝐶 [𝑥 𝑛 ←𝐹 ] )We can then conclude that "allOf" : [ {"$ref" : "urn:setvar"•𝑛 •"#afterq"•𝑛} , {"$ref" : "urn:start#afterq"•𝑛} ] evaluates to𝑇 if, and only if 𝑉 𝑎𝑙𝑖𝑑 (𝜙, 𝐴 𝐶 [𝑥 𝑛 ← 𝑇 ])∧𝑉 𝑎𝑙𝑖𝑑 (𝜙, 𝐴 𝐶 [𝑥 𝑛 ← 𝐹 ]), that is, 𝑉 𝑎𝑙𝑖𝑑 (𝑇 𝑎𝑖𝑙 1 . 𝜙, 𝐴 𝐶 ).Case 2 ≤ 𝑖 ≤ 𝑛: we want to prove that𝐼𝑛𝑑 (𝐶) ≤ 𝑛-𝑖 ⇒ 𝐶 ⊢ S 𝐽 ? { "$ref" : "urn:start#quant.x"• (𝑛 -𝑖 + 1) } → 𝑇 ⇔ 𝑉 𝑎𝑙𝑖𝑑 (𝑇 𝑎𝑖𝑙 𝑖 . 𝜙, 𝐴 𝐶 )By definition, 𝑇 𝑎𝑖𝑙 𝑖 . 𝜙 = 𝑄 𝑛-𝑖+1 𝑥 𝑛-𝑖+1 .𝑇 𝑎𝑖𝑙 𝑖-1 . 𝜙; we assume that 𝑄 𝑛-𝑖+1 = ∀; the case for 𝑄 𝑛-𝑖+1 = ∃ is analogous.From 𝑄 𝑛-𝑖+1 = ∀ we get:𝑉 𝑎𝑙𝑖𝑑 (𝑇 𝑎𝑖𝑙 𝑖 . 𝜙, 𝐴 𝐶 ) ⇔ (𝑉 𝑎𝑙𝑖𝑑 (𝑇 𝑎𝑖𝑙 𝑖-1 . 𝜙, 𝐴 𝐶 [𝑥 𝑛-𝑖+1 ← 𝑇 ]) ∧ 𝑉 𝑎𝑙𝑖𝑑 (𝑇 𝑎𝑖𝑙 𝑖-1 . , 𝐴 𝐶 [𝑥 𝑛-𝑖+1 ← 𝐹 ]))Since 𝑄 𝑛-𝑖+1 = ∀, then the body of "urn:start#quant.x"• (𝑛 -𝑖 + 1) is"allOf" : [ {"$ref" : "urn:setvar"•(𝑛-𝑖+1)• "#afterq"•(𝑛-𝑖+1)•} , {"$ref" : "urn:start#afterq"•(𝑛-𝑖+1)} ]The body of "urn:setvar"•(𝑛 -𝑖 + 1)•"#afterq"•(𝑛 -𝑖 + 1) is "$ref" : "urn:start#quant.x"•(𝑛 -𝑖 + 2) , and the body of "urn:start#afterq"•(𝑛 -𝑖 + 1) is equal. Hence, the assertion "$ref" : "urn:setvar"• (𝑛 -𝑖 + 1)•"#afterq"•(𝑛 -𝑖 + 1) evaluates "urn:start#quant.x"•(𝑛 -𝑖 + 2) in a context 𝐶 𝑇 which is 𝐶 extended with "$ref" : "urn:setvar"• (𝑛 -𝑖 + 1); by definition, 𝐴 𝐶 𝑇 is equal to 𝐴 𝐶 [𝑥 𝑛-𝑖+1 ← 𝑇 ]. Hence, by property (2), 𝐶 𝑇 ⊢ S 𝐽 ? { "$ref" : "urn:close#phi" } → 𝑇 ⇔ 𝑉 𝑎𝑙𝑖𝑑 (𝜙, 𝐴 𝐶 [𝑥 𝑛-𝑖+1 ←𝑇 ] )

  x"• (𝑛 -𝑖 + 2) } → 𝑇 ⇔ 𝑉 𝑎𝑙𝑖𝑑 (𝑇 𝑎𝑖𝑙 𝑖-1 . 𝜙, 𝐴 𝐶 [𝑥 𝑛-𝑖+1 ← 𝑇 ])and:𝐶 ⊢ S 𝐽 ? { "$ref" : "urn:start#quant.x"• (𝑛 -𝑖 + 2) } → 𝑇 ⇔ 𝑉 𝑎𝑙𝑖𝑑 (𝑇 𝑎𝑖𝑙 𝑖-1 . 𝜙, 𝐴 𝐶 [𝑥 𝑛-𝑖+1 ← 𝐹 ])We can then conclude that "allOf" : [ {"$ref" : "urn:setvar"•(𝑛-𝑖+1)• "#afterq"•(𝑛-𝑖+1)•} , {"$ref" : "urn:start#afterq"•(𝑛-𝑖+1)} ] evaluates to 𝑇 if, and only if𝑉 𝑎𝑙𝑖𝑑 (𝑇 𝑎𝑖𝑙 𝑖-1 . 𝜙, 𝐴 𝐶 [𝑥 𝑛-𝑖+1 ← 𝑇 ]) ∧ 𝑉 𝑎𝑙𝑖𝑑 (𝑇 𝑎𝑖𝑙 𝑖-1 . , 𝐴 𝐶 [𝑥 𝑛-𝑖+1 ← 𝐹 ])which concludes the proof. □From Section 6:

  In this paper we reserve the notation { . . . } to JSON objects, hence we use {| 𝑎 1 , . . . , 𝑎 𝑛 | } and {| 𝑎 𝑖 | } 𝑖 ∈𝑁 to indicate a set. When the order of the elements is relevant, we use the list notation [| 𝑎 1 , . . . , 𝑎 𝑛 | ]; we also use ì 𝑎 to indicate a list.

  [Tp 1 , . . . , Tp 𝑛 ] TypeOf (𝐽 ) ∈ {| Tp 1 , . . . , Tp 𝑛 |} Table1. Boolean conditions for type-uniform terminal assertions.

	assertion: kw :J'	condition: cond(J, kw :J')
	"enum" : [𝐽 1 , . . . , 𝐽 𝑛 ]	𝐽 ∈ {| 𝐽 1 , . . . , 𝐽 𝑛 |}
	"const" : 𝐽 𝑐	𝐽 = 𝐽 𝑐
	"type" : Tp	TypeOf (𝐽 ) = Tp
	"type" :

  2. Given a QBF closed formula 𝜓 = 𝑄 1 𝑥 1 . . . 𝑄 𝑛 𝑥 𝑛 . 𝜙 and the corresponding schema 𝑆 𝜓 with base URI 𝑏, 𝜓 is valid if, and only if, for every 𝐽 , [| 𝑏 | ] ⊢ S 𝐽 ? 𝑆 𝜓 → 𝑇 .

Algorithm 2 :

 2 Polynomial Time Validation/* The UpdatableStore maps each evaluated Instance-Schema pair to the list, maybe empty, of all contexts where it has been evaluated, each context paired to the associated result */

	1 SchemaValidateAndStore(Context,Instance,Schema,StopList,UpdatableStore)
	2	if (Schema == True) then return (True,EmptySet,EmptySet) ;
	3	if (Schema == False) then return (False,EmptySet,EmptySet) ;
	4	Input := (Context,Instance,Schema);
	5	if (Present (Input,StopList)) then raise ("error: infinite loop") ;
	6	PreviousResultsForSameSchemaAndInstance := UpdatableStore.get(Instance,Schema);
	7	for (OldContext,OldResult,OldEval,OldDFragSet) in PreviousResultsForSameSchemaAndInstance do
	8	if (Equivalent (Context,OldContext,OldDFragSet)) then /* If the current Context is equivalent
		to the OldContext we reuse the old output	*/
	9	return (OldOutput);
	10	Output := (True,EmptySet,EmptySet);

11 for Keyword in Keywords (Schema) do 12 Output := KeywordValidate (Context, Instance, Keyword, Output, StopList+Input,UpdatableStore) ; 13 (Result,Eval,DFragSet) := Output; 14 UpdatableStore.addToList((Instance,Schema),(Context,Result,Eval,DFragSet)); 15 if Result == True then 16 return (Result, Eval, DFragSet);

17 else 18 return (Result, EmptySet, DFragSet);

  Tp "type" : [Tp 1 , . . . , Tp 𝑛 ] no type TypeOf ( 𝐽 ) ∈ {| Tp 1 , . . . , Tp 𝑛 |}

	"enum" : [𝐽 1 , . . . , 𝐽 𝑛 ]	no type	𝐽 ∈ {| 𝐽 1 , . . . , 𝐽 𝑛 |}
	"const" : 𝐽 𝑐	no type	𝐽 = 𝐽 𝑐
	"type" : Tp TypeOf ( 𝐽 ) = "exclusiveMinimum": q no type

  . . , 𝑘 𝑛 ] object ∀𝑖. 𝑘 𝑖 ∈ names(𝐽 ) "uniqueItems": true array𝐽 = [𝐽 1 , . . . , 𝐽 𝑛 ] with 𝑛 ≥ 0 ∧ ∀𝑖, 𝑗 . 1 ≤ 𝑖 ≠ 𝑗 ≤ 𝑛 ⇒ 𝐽 𝑖 ≠ 𝐽 𝑗 ∀𝑖 ∈ {| 1 . . . 𝑛 | }. 𝐶 ⊢ S 𝐽 ? 𝑆 𝑖 → (𝑟 𝑖 , 𝜅 𝑖 ) 𝑟 = ∨({| 𝑟 𝑖 | } 𝑖 ∈ {| 1...𝑛 |} ) 𝐶 ⊢ K 𝐽 ? "anyOf" : [𝑆 1 , ..., 𝑆 𝑛 ] → (𝑟, 𝑖 ∈ {| 1...𝑛 |} 𝜅 𝑖 ) ∀𝑖 ∈ {| 1 . . . 𝑛 | }. 𝐶 ⊢ S 𝐽 ? 𝑆 𝑖 → (𝑟 𝑖 , 𝜅 𝑖 ) 𝑟 = ∧({| 𝑟 𝑖 | } 𝑖 ∈ {| 1...𝑛 |} ) 𝐶 ⊢ K 𝐽 ? "allOf" : [𝑆 1 , ..., 𝑆 𝑛 ] → (𝑟, 𝑖 ∈ {| 1...𝑛 |} 𝜅 𝑖 ) ∀𝑖 ∈ {| 1 . . . 𝑛 | }. 𝐶 ⊢ S 𝐽 ? 𝑆 𝑖 → (𝑟 𝑖 , 𝜅 𝑖 ) 𝑟 = ( |{| 𝑖 | 𝑟 𝑖 = 𝑇 | }| = 1 ) 𝐶 ⊢ K 𝐽 ? "oneOf" : [𝑆 1 , ..., 𝑆 𝑛 ] → (𝑟, 𝑖 ∈ {| 1...𝑛 |} 𝜅 𝑖 ) 𝐽 1 , . . . , 𝑘 ′ 𝑛 : 𝐽 𝑛 } {| (𝑖 1 , 𝑗 1 ), . . . , (𝑖 𝑙 , 𝑗 𝑙

	111:30
	A.4 References
	𝑆 ′ = get(load(absURI ), f )	𝐶+?absURI ⊢ S 𝐽 ? 𝑆 ′ → (𝑟, 𝜅)
				($ref)
		𝐶 ⊢ K 𝐽 ? "$ref" : absURI •"#"•f → (𝑟, 𝜅)
	dget(load(absURI ), f ) ≠ ⊥	fURI = fstURI(𝐶+?absURI, 𝑓 )
	𝑆 ′ = dget(load(fURI ), f )	𝐶+?fURI ⊢ S 𝐽 ? 𝑆 ′ → (𝑟, 𝜅)
				($dynamicRef)
	𝐶 ⊢ K 𝐽 ? "$dynamicRef" : absURI •"#"•f → (𝑟, 𝜅)
		dget(load(absURI ), f ) = ⊥
	𝑆 ′ = get(load(absURI ), f )	𝐶+?absURI ⊢ S 𝐽 ? 𝑆 ′ → (𝑟, 𝜅)
				($dynamicRefAsRef)
	𝐶 ⊢ K 𝐽 ? "$dynamicRef" : absURI •"#"•f → (𝑟, 𝜅)
	A.5 If-then-else
	𝐶 ⊢
	"uniqueItems": false	array	T
	"minItems": i	array	|𝐽 | ≥ 𝑖
	"maxItems": i	array	|𝐽 | ≤ 𝑖
	"format": format	string	𝐽 ∈ 𝐿 (format)
	"dependentRequired" :		∀𝑖 ∈ {| 1 . . . 𝑛 |}.
	{ 𝑘 1 : [ 𝑘 1 1 , . . . , 𝑘 1 𝑜 1 ]	object	𝑘 𝑖 ∈ names(𝐽 )
	. . . , 𝑘 𝑛 : [ 𝑘 𝑛 1 , . . . , 𝑘 𝑛 𝑜𝑛 ] }		⇒ {| 𝑘 𝑖 1 , . . . , 𝑘 𝑖 𝑜 𝑖 |} ⊆ names(𝐽 )
	A.3 The boolean applicators
				(anyOf)
				(allOf)
				(oneOf)
			𝐶 ⊢ (not)

S 𝐽 ? 𝑆 → (𝑟, 𝜅) 𝐶 ⊢ K 𝐽 ? "not" : 𝑆 → (¬𝑟, 𝜅) S 𝐽 ? 𝑆 𝑖 → (𝑇 , 𝜅 𝑖 ) 𝐶 ⊢ S 𝐽 ? 𝑆 𝑡 → (𝑟, 𝜅 𝑡 ) 𝐶 ⊢ L 𝐽 ? ("if" : 𝑆 𝑖 + "then" : 𝑆 𝑡 + "else" :

𝑆 𝑒 ) → (𝑟, 𝜅 𝑖 ∪ 𝜅 𝑡 ) (if-true) 𝐶 ⊢ S 𝐽 ? 𝑆 𝑖 → (𝐹, 𝜅 𝑖 ) 𝐶 ⊢ S 𝐽 ? 𝑆 𝑒 → (𝑟, 𝜅 𝑒 ) 𝐶 ⊢ L 𝐽 ? ("if" : 𝑆 𝑖 + "then" : 𝑆 𝑡 + "else" : 𝑆 𝑒 ) → (𝑟, 𝜅 𝑖 ∪ 𝜅 𝑒 ) (if-false)

𝐶 ⊢ L 𝐽 ? ("then" : 𝑆 𝑡 + "else" : 𝑆 𝑒 ) → (𝑇 , ∅) (missing-if)

A.6 Object and array applicators: independent applicators Independent applicators are defined by a set of two rules: (kwTriv) and (kw); the (kwTriv) rules are specified by the following table; the (kw) rules are specified after the table. assertion kw : 𝐽 ′ TypeOf (kw) "patternProperties" : { 𝑝 1 : 𝑆 1 , . . . , 𝑝 𝑚 : 𝑆 𝑚 } object "properties" : { 𝑘 1 : 𝑆 1 , . . . , 𝑘 𝑚 : 𝑆 𝑚 } object "propertyNames" : 𝑆 object "prefixItems" : 𝑆 array "contains" : 𝑆 array "dependentSchemas" : { 𝑘 1 : 𝑆 1 , . . . , 𝑘 𝑛 : 𝑆 𝑛 } object 𝐽 = { 𝑘 ′ 1 :

  |} ) 𝐶 ⊢ K 𝐽 ? "properties" : { 𝑘 1 : 𝑆 1 , . . . , 𝑘 𝑚 :𝑆 𝑚 } → (𝑟, {| 𝑘 ′ 𝑖 1 , . . . , 𝑘 ′ 𝑖 𝑙 | }) 𝐽 = [ 𝐽 1 , . . . , 𝐽 𝑚 ] ∀𝑖 ∈ {| 1 . . . min(𝑛, 𝑚) | }. 𝐶 ⊢ S 𝐽 𝑖 ? 𝑆 𝑖 → (𝑟 𝑖 , 𝜅 𝑖 ) 𝑟 = ∧({| 𝑟 𝑖 | } 𝑖 ∈ {| 1...min(𝑛,𝑚) |} ) 𝐶 ⊢ K 𝐽 ? "prefixItems" : [ 𝑆 1 , . . . , 𝑆 𝑛 ] → (𝑟, {| 1, . . . , min(𝑛, 𝑚) | }) (prefixItems) 𝐽 = [ 𝐽 1 , ..., 𝐽 𝑛 ] ∀𝑖 ∈ {| 1 . . . 𝑛 | }. 𝐶 ⊢ S 𝐽 𝑖 ? 𝑆 → (𝑟 𝑖 , 𝜅 𝑖 ) 𝜅 𝑐 = {| 𝑖 | 𝑟 𝑖 = 𝑇 | } 𝑟 𝑐 = (𝑖 ≤ |𝜅 𝑐 | ≤ 𝑗)𝐶 ⊢ K 𝐽 ? ("contains" : 𝑆 + "minContains" : 𝑖 + "maxContains" :𝑗) → (𝑟 𝑐 , 𝜅 𝑐 ) 𝐽 1 , ..., 𝐽 𝑛 ] ∀𝑖 ∈ {| 1 . . . 𝑛 | }. 𝐶 ⊢ S 𝐽 𝑖 ? 𝑆 → (𝑟 𝑖 , 𝜅 𝑖 ) 𝜅 𝑐 = {| 𝑖 | 𝑟 𝑖 = 𝑇 | } 𝑟 𝑐 = (𝑖 ≤ |𝜅 𝑐 |)𝐶 ⊢ K 𝐽 ? ("contains" : 𝑆 + "minContains" : 𝑖) → (𝑟 𝑐 , 𝜅 𝑐 )

		(contains-max)
	rule (contains-max) does not apply and	𝐽 = [ (contains-no-max)
	rules (contains-max) and (contains-no-max) do not apply
	𝐶 ⊢
		(properties)

𝐽 = { 𝑘 1 : 𝐽 1 , . . . , 𝑘 𝑛 : 𝐽 𝑛 } ∀𝑖 ∈ {| 1 . . . 𝑛 | }. 𝐶 ⊢ S 𝑘 𝑖 ? 𝑆 → (𝑟 𝑖 , 𝜅 𝑖 ) 𝑟 = ∧({| 𝑟 (𝜅 𝑖 ) | } 𝑖 ∈ {| 1...𝑛 |} )

𝐶 ⊢ K 𝐽 ? "propertyNames" : 𝑆 → (𝑟, ∅) (propertyNames) K 𝐽 ? ("minContains" : 𝑖 (+"maxContains"𝑖) ? ) → (𝑇 , ∅)

(missing-contains)

  ) 𝑚 if ("prefixItems" : [ 𝑆 1 , . . . , 𝑆 𝑚 ]) ∈ ì 𝐾 for some 𝑆 1 , . . . , 𝑆 𝑛 maxPrefixOf( ì 𝐾) = 0 if ("prefixItems" : [ 𝑆 1 , . . . , 𝑆 𝑚 ]) ∉ ì 𝐾 for any 𝑆 1 , . . . , 𝑆 𝑛 𝐽 = [ 𝐽 1 , ..., 𝐽 𝑛 ] 𝐶 ⊢ L 𝐽 ? ì 𝐾 → (𝑟, 𝜅) {| 𝑖 1 , . . . , 𝑖 𝑙

	111:32
	maxPrefixOf( ì 𝐾) =

Table 2 .

 2 Validators used in our experiments, first listing active open-source projects, then two academic implementations. Stating programming language and supported drafts. (×) means that draft is officially supported, but logical or runtime errors occurred in our experiments.

	Validator	Language Draft4 Draft 2020 Origin/Version
	clojure-json-schema	clojure	×		Bowtie, release tag b07e5
	cpp-valijson	C++	×		Bowtie, release tag b07e5
	go-jsonschema	go	×	×	Bowtie, release tag b07e5
	js-ajv	javascript	×	(×)	Bowtie, release tag b07e5
	js-hyperjump	javascript	(×)	×	Bowtie, release tag b07e5
	lua-jsonschema	lua	×		Bowtie, release tag b07e5
	ruby-json_schemer	ruby	×		Bowtie, release tag b07e5
	rust-boon	python	×	(×)	Bowtie, release tag 992c2
	rust-jsonschema	rust	×	×	Bowtie, release tag b07e5
	python-fastjsonschema	python	×		Bowtie, release tag b07e5
	python-jschon	python		×	Bowtie, release tag b07e5
	python-jsonschema	python	×	×	Bowtie, release tag b07e5
	ts-vscode-json-languageservice typescript	×	(×)	Bowtie, release tag b07e5
	dotnet-jsonschema-net	dotnet		×	Bowtie, release tag b07e5
	foundations-jsonsonschema	python	×		Code from [21], integrated into Bowtie
	modern-jsonschema	Scala		×	Algorithm 2, integrated into Bowtie

Other interpretations of the specifications of Draft 2020-12 are possible; see Appendix G for a discussion.

See the discussion in Appendix G.

Actually, it can also be matched by a "$dynamicAnchor" operator, which, in this case, is interpreted as exactly as "$anchor".

Observe that dget(load(absURI ), f ) ≠ ⊥ is a static check that may be performed once for all when the schema is loaded.This check is called "the bookending requirement", and it may be dropped in future Drafts (see Remove $dynamicRef bookending requirement), but our results would not be affected by this decisions.

In the example, we encode a sequence of absolute URIs such as [| "urn:psi", "urn:start", "urn:setvar1" |] as "urn:psi_urn:start_urn:setvar1_", that is, we escape any underscore inside the URIs (not exemplified here), and we terminate each URI with an underscore.

As an AppEngine application, the online version of the tool comes with strict limitations regarding main memory and timeouts. It is not suitable for benchmarking, but allows one to interact with the system and to inspect the proofs.

URI "https://example.com/simple-tree#tree" could be substituted by https : // json -schema . org / draft /2020 -12/ schema " , " $id " : " https : // example . com / resource1 " , " type " : " object " , " $ref " : "#/ properties / foo / items " , " properties " : { " foo " : { " $schema " : " https : // json -schema . org / draft /2019 -09/ schema " , " $id " : " https : // example . com / embedded " , " items " : { " $id " : " https : // example . com / embeddedInside " , " type " : " number " } } } , " default " : { " $id " : " https : // example . com / irrelevantId " ... , " $ref " : " https : // example . com / flattened #" , " properties " : { " foo " : { " $ref " : " https : // example . com / embedded " } } , " default " : { " $id " : " https : // example . com / irrelevantId " , " type " : " number } , " $defs " : { " https : // example . com / embedded " : { " $schema " : " https : // json -schema . org / draft /2019 -09/ schema " , " $id " : " https : // example . com / embedded " , " items " : { " $ref " : " https : // example . com / embeddedInside " } } , " https : // json -schema . org / draft /2020 -12/ schema " : { " $schema " : " https : // json -schema . org / draft /2019 -09/ schema " , " $id " : " https : // example . com

The functions dgets(𝑆, 𝑓 ) and dgetk(𝑆, 𝑓 ) are defined as follows, where max returns the maximum element of a set that contains either schemas or ⊥, according to the trivial order defined by ⊥ ≤ 𝑆: that is, max select the only element in the set that is different from ⊥, if it exists and is unique. If we assume that no plain-name is used by two different anchors in the same schema, then, in line 4, there exists at most one value of 𝑖 such that dget(𝐾 𝑖 , 𝑓 ) ≠ ⊥, hence the maximum is well defined, and the same holds for lines 6 and 7. 0 dget(𝑆, 𝑓 )

= dgets(StripId(𝑆), 𝑓 ) where kwSimPar = {| "not", "contains", "propertyNames", "items", "additionalProperties", "unevaluatedProperties", "unevaluatedItems" | } kwObjPar = {| "$defs", "patternProperties", "properties", "dependentSchemas" | } kwArrPar = {| "anyOf", "allOf", "oneOf", "prefixItems" | } kwOther = Str \ kwSimPar \ kwObjPar \ kwArrPar

The four lines of dgetk definition specify that the search for a "$dynamicAnchor" keyword is performed only inside keywords that are known and whose parameter contains a schema object in a known position. For example, the search is not performed inside a user-defined keyword or inside "const" or "default".

When 𝑓 is a plain-name, then the function get is identical to dget, but it extends case 3, since it matches both "$anchor" and "$dynamicAnchor": [START_REF] Bryan | JavaScript Object Notation (JSON) Pointer[END_REF]. However, Draft 2020-12 specs [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF] (Section 9.2.1) specify that the behaviour is undefined when the pointer crosses resource boundaries .

C WHERE TO SEARCH FOR DYNAMIC ANCHORS

In Remark 1 we discuss the difference between looking for a dynamic reference in 𝐶 or in 𝐶+?absURI . We report here a concrete test.

When the schema of Figure 9 is applied to the JSON instance { "children" : { } }, the keyword "$dynamicRef" : "https://example.com/tree#node" is applied in a dynamic context that only contains "https://example.com/outer", which denotes a resources that does not contain any "$dynamicAnchor" : "node" keyword. The only such keyword in the schema is at line 7, and is belongs to the embedded resource "https://example.com/tree". This specific example relies on the fact that an embedded resource, as identified by the "$id" keyword, is not part of the scope of the embedding resource, the one identified by "https://example.com/outer", but it could be rephrased by putting the embedded resource in a separate file. Hence, if "$dynamicRef" : "https://example.com/tree#node" were resolved using the dynamic context only, if would raise a run-time failure. But our rule dictates that it is resolved in 𝐶+?absURI , that is in "https://example.com/outer" + "https://example.com/tree" hence raising a validation error since the value of "children" is not an array. In Figure 9 we see how four different validators behaved at the date of 10 𝑡ℎ Jan 2023: the first two exhibit an internal bug, and the other two use the approach that we formalized; none of them reports a resolution error due to the fact that "$dynamicAnchor" : "node" is not present in the dynamic scope. Hence, they validate the choice to look for the fragment id 𝑓 inside 𝐶+?absURI , and not inside 𝐶 only.

Schema:

1 { " $schema " : " https : // json -schema . org / draft /2020 -12/ schema " , " $id " : 2 " https : // example . com / outer " , 3 " $dynamicRef " : " https : // example . com / tree # node " ,

4

" $defs " : {

5

" https : // example . com / tree " : { 6 " $id " : " https : // example . com / tree " , 7 " $dynamicAnchor " : " node " ,

8

" type " : " object " ,

9

" properties " : { Proof. Consider a QBF formula 𝜓 = 𝑄 1 𝑥 1 . . . 𝑄 𝑛 𝑥 𝑛 . 𝜙 and the corresponding schema 𝑆 𝜓 . We say that a context 𝐶 is well-formed for 𝑆 𝜓 if (1) its elements are URIs of resources of 𝑆 𝜓 and (2) in case it contains "urn:close", then "urn:close" is the last element of 𝐶. We associate every well-formed context 𝐶 to an assignment 𝐴 𝐶 as follows:

may contain open variables and an assignment 𝐴 that is defined for every variable of 𝜓 ′ , we use 𝑉 𝑎𝑙𝑖𝑑 (𝜓 ′ , 𝐴) to indicate the fact that 𝜓 ′ is valid when every open variable is substituted with its value in 𝐴.

The index of a context 𝐶, 𝐼𝑛𝑑 (𝐶), is the maximal 𝑖 such that "urn:setvar"•𝑖 ∈ 𝐶, and is 0 if no "urn:setvar"•𝑖 belongs to 𝐶.

We prove, by induction, the following properties, for every context 𝐶 well-formed for 𝑆 𝜓 , where we define𝑇 𝑎𝑖𝑙 0 (𝜓 ) = 𝜙 and𝑇 𝑎𝑖𝑙 𝑖+1 (𝜓 ) = 𝑄 𝑛-𝑖 𝑥 𝑛-𝑖 𝑇 𝑎𝑖𝑙 𝑖 (𝜓 ), so that𝑇 𝑎𝑖𝑙 𝑖 (𝜓 ) = 𝑄 𝑛-𝑖+1 𝑥 𝑛-𝑖+1 . . . 𝑄 𝑛 𝑥 𝑛 . 𝜙:

The theorem follows from case (3), in the case 𝑖 = 𝑛, with 𝐶 equal to the base context [| "urn:psi" | ]. Property (1a): it holds since "x"• 𝑖 is defined as "anyOf" : [true] in "urn:setvar"• 𝑖 and as "anyOf" : [false] in "urn:close". In a well-formed context that contains "urn:close", when "urn:setvar"•𝑖 is present, then it precedes "urn:close", hence the value of { "$dynamicRef" : "x" • 𝑖 } is determined by "urn:setvar" • 𝑖, hence is "anyOf" : [true]. If "urn:setvar" • 𝑖 is absent, then the value of { "$dynamicRef" : "x"•𝑖 } is defined by "urn:close", hence is "anyOf" :

Property (2): by induction on 𝜙, using property (1) for the 𝑥 𝑖 and ¬𝑥 𝑖 , and induction for 𝑆 1 ∧ 𝑆 2 and 𝑆 1 ∨ 𝑆 2 .

Property (3): by induction on 𝑖. Case 𝑖 = 1: we want to prove that

By definition, 𝑇 𝑎𝑖𝑙 1 . 𝜙 = 𝑄 𝑛 𝑥 𝑛 .𝜙; we assume that 𝑄 𝑛 = ∀; the case for 𝑄 𝑛 = ∃ is analogous.

From 𝑄 𝑛 = ∀ we get:

Since 𝑄 𝑛 = ∀, then the body of "urn:start#quant.x"•𝑛 is

The body of "urn:setvar"•𝑛•"#afterq"•𝑛 is "$ref" : "urn:close#phi", and the body of "urn:start#afterq"• 𝑛 is equal. Hence, the assertion "$ref" : "urn:setvar"•𝑛•"#afterq"•𝑛 evaluates "$ref" : "urn:close#phi" in a context 𝐶 𝑇 which is 𝐶 extended with "$ref" : "urn:setvar"•𝑛; by definition,

Hence, by property (2),

This means that when we say "for any 𝑠𝑙. . . " we actually mean "for any list 𝑠𝑙 of tuples (𝐶, 𝐽, 𝑆). . . "

We first define an enriched version of the typing rules, that defines a judgment 𝐶 ⊢ Sd 𝐽 ? 𝑆 → (𝑟, 𝜅, 𝑑) that returns in 𝑑 the fragment names of the dynamic references that are resolved. The most important rule is ($dynamicRef 𝑑 ), that adds the resolved f to the list 𝑑.

All the applicators pass the evaluated dynamic references to their result, and a schema passes all the evaluated dynamic references even when it fails. We present here the failing schema rule and the rule for (patternProperties 𝑑 ), (schema-false 𝑑 ), and (klist-(𝑛 + 1) 𝑑 ), the other rules are analogous.

These new judgments just return some extra information with respect to the basic judgment, hence the following facts are immediate.

We define an equivalence relation 𝐶 ∼ 𝑑 𝐶 ′ defined as:

We prove the following property:

We prove it by induction on the rules. The proof is immediate for the terminal rules. For the applicators, consider rule (patternProperties 𝑑 ).

From the hypothesis that 𝑞 ∈ {| 1...𝑙 |} 𝑑 𝑞 ⊆ 𝑑 we immediately deduce that for 𝑞 ∈ {| 1 . . . 𝑙 | } we have 𝑑 𝑞 ⊆ 𝑑, hence we can apply the inductive hypothesis to each 𝐶 ⊢ S 𝐽 𝑖 𝑞 ? 𝑆 𝑗 𝑞 → (𝑟 𝑞 , 𝜅 𝑞 , 𝑑 𝑞 ), and conclude. All the rules that do not modify the context are proved in the same way. We are left with the rules that modify the context, which are ($ref 𝑑 ) and ($dynamicRef 𝑑 ). This is rule ($ref 𝑑 ).

We prove now that 𝐶 ∼ 𝑑 𝐶 ′ implies 𝐶+?absURI ∼ 𝑑 𝐶 ′ +?absURI . Consider any f ∈ 𝑑; if fstURI(𝐶, 𝑓 ) are both different from ⊥ we have:

if fstURI(𝐶, 𝑓 ) are both equal to ⊥ we have: fstURI(𝐶+?absURI, 𝑓 ) = absURI = fstURI(𝐶 ′ +?absURI, 𝑓 ).

Hence 𝐶+?absURI ∼ 𝑑 𝐶 ′ +?absURI , and we can apply induction to the ($ref) rule.

Consider finally rule ($dynamicRef 𝑑 ), applied to 𝐶 and to 𝐶 ′ .

dget(load(absURI ), f ) ≠ ⊥ fURI = fstURI(𝐶+?absURI, 𝑓 ) 𝑆 0 = dget(load(fURI ), f ) 𝐶+?fURI ⊢ S 𝐽 ? 𝑆 0 → (𝑟, 𝜅, 𝑑 0 )

By hypothesis, (𝑑 0 ∪ {| f | }) ⊆ 𝑑, hence f ∈ 𝑑. By reasoning as for rule ($ref), we deduce that fstURI(𝐶+?absURI, 𝑓 ) = fstURI(𝐶 ′ +?absURI, 𝑓 ), hence fURI = fURI ′ , hence 𝑆 ′ 0 = 𝑆 0 . By reasoning as for rule ($ref), absURI = absURI ′ implies that 𝐶+?fURI ∼ 𝑑 𝐶 ′ +?fURI ′ . Hence, since 𝑑 0 ⊆ (𝑑 0 ∪ {| f | }) ⊆ 𝑑, we can apply the induction hypothesis, and deduce that (𝑟 ′ , 𝜅 ′ , 𝑑 ′ 0 ) = (𝑟, 𝜅, 𝑑 0 ), from which we deduce that

) Hence, we have proved that the following deduction rule is sound, that is, that its application does not allow any new judgment to be deduced:

Our algorithm applies the rules of 𝐶 ⊢ Sd 𝐽 ? 𝑆 plus (reuse 𝑑 ) that is sound, hence it can only prove correct statements. On the other direction, completeness of the algorithm follows from the fact that it is correct and that it always terminates. □

We can now prove that Algorithm 2 runs in polynomial time when we have a constant bound on the number of dynamic references. Theorem 6. Consider a family of closed schemas 𝑆 and judgments 𝐽 such that (|𝑆 | + |𝐽 |) ≤ 𝑛, and let 𝐷 be the set of different fragments 𝑓 that appear in the argument of a "$dynamicRef" : initURI •"#"•f in 𝑆. Then, Algorithm 2 runs on 𝑆 and 𝐽 in time 𝑂 (𝑛 𝑘+|𝐷 | ) for some constant 𝑘.

Proof. Consider 𝑆, 𝐽 , 𝑛, and 𝐷, as in the statement of the Theorem. Consider the call tree of a run of Algorithm 2 applied to the tuple (𝐶, 𝐽, 𝑆, ∅, ∅), with 𝑆. The top node of this tree is a call to SchemaValidateAndStore, from now on abbreviates as SVAS, applied to (𝐶, 𝐽, 𝑆, ∅, ∅), which in turn invokes from 0 to 𝑛 times KeywordValidate(𝐶, 𝐽, 𝐾 𝑖 , . . .), each applying one specific rule, each rule invoking a certain number of times SVAS(𝐶 ′ , 𝐽 ′ , 𝑆 ′ , 𝑠𝑙 ′ , 𝑢𝑝 ′ ).

We first observe that, for any invocation SVAS(𝐶 ′ , 𝐽 ′ , 𝑆 ′ , 𝑠𝑙 ′ , 𝑢𝑝 ′ ) in the call tree rooted in SVAS(𝐶, 𝐽, 𝑆, ∅, ∅), with 𝑆 closed, 𝐽 ′ is a subtree of 𝐽 , 𝑆 ′ is a subschema of 𝑆, and 𝐶 ′ is a list of URIs of resources in 𝑆 with no repetitions. We also observe that the call tree is finite, since any infinite call tree would have an infinite branch, every infinite branch would contain two different invocations of SVAS with the same triple (𝐶, 𝐽, 𝑆), and this possibility is prevented by the test executed on 𝑠𝑙.

We observe that every two nodes labeled with SVAS(𝐶 ′ , 𝐽 ′ , 𝑆 ′ , 𝑠𝑙 ′ , 𝑢𝑝 ′ ) and SVAS(𝐶 ′′ , 𝐽 ′′ , 𝑆 ′′ , 𝑠𝑙 ′′ , 𝑢𝑝 ′′ ) in that call tree either differ in 𝐽 ′ , or they differ in 𝑆 ′ , or they enjoy the property that 𝐶 ≁ 𝐷 𝐶 ′ , since the check performed on 𝑢𝑠 prevents a second call to SVAS with the same 𝐽 and 𝑆 when 𝐶 ∼ 𝑑 ′ 𝐶 ′ where 𝑑 ′ is the DFragSet returned for (𝐶, 𝐽, 𝑆), hence, for any two calls with the same (𝐽, 𝑆), the corresponding 𝐶 and 𝐶 ′ enjoy 𝐶 ≁ 𝑑 ′ 𝐶 ′ for some 𝑑 ′ ⊆ 𝐷, hence they enjoy 𝐶 ≁ 𝐷 𝐶 ′ . Each equivalence class of the relation 𝐶 ∼ 𝐷 𝐶 ′ is characterized by a different function that maps each f ∈ 𝐷 to a URI, or to ⊥; if we have 𝑛 different URIs in 𝑆, the equivalence relation has at most (𝑛 + 1) |𝐷 | distinct classes, since we have at most 𝑛 + 1 possible different choices for each fragment identifier. We have at most 𝑛 subschemas of 𝑆 and subterms of 𝐽 , and (𝑛 + 1) |𝐷 | different equivalence classes for 𝐶, hence the call tree for SVAS(𝐶, 𝐽, 𝑆, ∅, ∅) has at most (𝑛 + 1) |𝐷 | × 𝑛 × 𝑛 nodes labeled with SVAS. The time needed to invoke the at most 𝑛 instances of SVAS that are immediately invoked by a call to SVAS is polynomial -the most complicated case is (patternProperties) where each of the 𝑛 label in 𝐽 must be matched against each of the 𝑛 regular expressions of the patterns of 𝐾, hence SVAS(𝐶, 𝐽, 𝑆, ∅, ∅) runs in time 𝑂 (𝑛 𝑘+ |𝐷 | ) for some constant 𝑘. □

From Section 8:

Theorem 8 (Encoding correctness). Let 𝑆 be a closed schema with base URI b. Then:

Proof. For any schema 𝑆 0 with base URI 𝑏, we want to prove that

Our validation rules are deterministic, hence for each triple 𝐶, 𝐽, 𝑆 or 𝐶, 𝐽, 𝐾 we can define its "standard proof", that is just the only proof obtained by the application of the rules.

We then consider the standard proof for

and we prove that, for any judgment 𝐶 ⊢ S 𝐽 ? 𝑆 → (𝑟, 𝜅) in that proof, we have that:

𝐶 ⊢ S 𝐽 ? 𝑆 → (𝑟, 𝜅) ⇔ 𝐶 ⊢ S 𝐽 ? CI(𝐶, 𝑆) → (𝑟, 𝜅)

and similarly that for any judgment 𝐶 ⊢ K 𝐽 ? 𝐾 → (𝑟, 𝜅) in that proof, we have that:

We prove that by mutual induction on the size of the proof. The base cases are trivial, since CI(𝐶, 𝐾) is equal to 𝐾 when 𝐾 is not a reference operator and does not contain any subschema. All the applicators different from references, such as "anyOf", are immediate by induction.

The only interesting cases are those for "$ref" and "$dynamicRef".

CI(𝐶, "$dynamicRef" : absURI

Let us consider the ("$dynamicRef") case. Let this be the root of the proof of 𝐶 ⊢ K 𝐽 ? 𝐾 → (𝑟, 𝜅):

By definition, CI(𝐶, "$dynamicRef" : absURI

Hence, the proof for 𝐶 ⊢ K 𝐽 ? CI(𝐶, 𝐾) → (𝑟, 𝜅) is the following one.

By definition of Static(𝑆 0 ), if 𝑆 ′ is the schema identified by fURI •"#"•f , then fURI •"#"•𝐶 •f refers to CI(𝐶, 𝑆 ′ ), hence 𝑆 ′ 1 = CI(𝐶, 𝑆 ′ ), and we conclude by induction.

F UNFOLDING OF THE EXAMPLE

We report here the complete unfolding of the running example, using the procedure defined in Section 8. It is the following document, where contexts are represented inside anchors using the abbreviations "urn:psi" → "p", "urn:start" → "s", "urn:setvar1" → "sv1", "urn:setvar2" → "sv2", and "urn:close" → "c". This is the first part.

{ " $schema " : " https : // json -schema . org / draft /2020 -12/ schema " , " $id " : " urn : psi " , " $ref " : " urn : start # p_s_forall . x1 " , " $defs " : { " urn : start " : { " $id " : " urn : start " , " $defs " : { " p_s_forall . x1 " : { " $anchor " : " p_s_forall . x1 " , " allOf " : [ { " $ref " : " urn : setvar1 # p_s_afterq1 " } , { " $ref " : " urn : start # p_s_afterq1 " } ] } , " p_s_exists . x2 " : { " $anchor " : " p_s_exists . x2 " , " anyOf " : [ { " $ref " : " urn : setvar2 # p_s_afterq2 " } , { " $ref " : " urn : start # p_s_afterq2 " } ] } , " p_s_sv1_exists . x2 " : { " $anchor " : " p_s_sv1_exists . x2 " , " anyOf " : [ { " $ref " : " urn : setvar2 # p_s_sv1_afterq2 " } , { " $ref " : " urn : start # p_s_sv1_afterq2 " } ] } , " p_s_afterq1 " : { " $anchor " : " p_s_afterq1 " , " $ref " : " urn : start # p_s_exists . x2 " } , " p_s_afterq2 " : { " $anchor " : " p_s_afterq2 " , " $ref " : " urn : close # p_s_phi " } , " p_s_sv1_afterq2 " : { " $anchor " : " p_s_sv1_afterq2 " , " $ref " : " urn : close # p_s_sv1_phi " } } } , " urn : setvar1 " : { " $id " : " urn : setvar1 " , " $defs " : { " p_s_afterq1 " : { " $anchor " : " p_s_afterq1 " , " $ref " : " urn : start # p_s_sv1_exists . x2 " } , " p_s_sv1 _sv2_c_x1 " :

{ " $anchor " : " p_s_sv1_sv2_c_ x1 " , " anyOf " : [ true ] } , " p_s_sv1_c_x1 " :

{ " $anchor " : " p_s_sv1_c_x1 " , " anyOf " : [ true ] } , " p_s _s v1_ sv 2_c _n ot . x1 " : { " $anchor " : " p _s _sv 1_ sv2 _c _no t . x1 " , " anyOf " : [ false ] } , " p_s_sv1_c_not . x1 " :

{ " $anchor " : " p_s_sv1_c_not . x1 " , " anyOf " : [ false ] } } } , " urn : setvar2 " : { " $id " : " urn : setvar2 " , " $defs " : { " p_s_sv1_afterq2 " : { " $anchor " : " p_s_sv1_afterq2 " , " $ref " : " urn : close # p_s_sv1_sv2_phi " } , " p_s_afterq2 " :

{ " $anchor " : " p_s_afterq2 " , " $ref " : " urn : close # p_s_sv2_phi " } , " p_s_sv1 _sv2_c_x2 " :

{ " $anchor " : " p_s_sv1_sv2_c_ x2 " , " anyOf " : [ true ] } , " p_s_sv2_c_x2 " :

{ " $anchor " : " p_s_sv2_c_x2 " , " anyOf " : [ true ] } , " p_s _s v1_ sv 2_c _n ot . x2 " : { " $anchor " : " p _s _sv 1_ sv2 _c _no t . x2 " , " anyOf " : [ false ] } , " p_s_sv2_c_not . x2 " :

{ " $anchor " : " p_s_sv2_c_not . x2 " , " anyOf " : [ false ] } } } , " urn : close " : { " $id " : " urn : close " , " $defs " : { " p_s_sv2_c_x1 " : { " $anchor " : " p_s_sv2_c_x1 " , " anyOf " : [ false ] } , " p_s_c_x1 " : { " $anchor " : " p_s_c_x1 " , " anyOf " : [ false ] } , " p_s_sv2_c_not . x1 " : { " $anchor " : " p_s_sv2_c_not . x1 " , " anyOf " : [ true ] } , " p_s_c_not . x1 " : { " $anchor " : " p_s_c_not . x1 " , " anyOf " : [ true ] } , " p_s_sv1_c_x2 " : { " $anchor " : " p_s_sv1_c_x2 " , " anyOf " : [ false ] } , " p_s_c_x2 " :

{ " $anchor " : " p_s_c_x2 " , " anyOf " : [ false ] } , " p_s_sv1_c_not . x2 " : { " $anchor " : " p_s_sv1_c_not . x2 " , " anyOf " : [ true ] } , " p_s_c_not . x2 " : { " $anchor " : " p_s_c_not . x2 " , " anyOf " : [ true ] } , " p_s_sv1_sv2_phi " : { ...

111:44

Here is the last part; since "urn:close#phi" can be reached from four different contexts, we need four different definitions, as follows. In the four cases, the way the dynamic variables "x1" and "x2" are resolved varies depending on the context 𝐶, encoded in the anchor 𝐶 • 𝑓 .

" urn : close # urn : psi_urn : start_urn : setvar1_urn : setvar2_phi " : { " $anchor " : " urn : psi_urn : start_urn : setvar1_urn : setvar2_phi " , " anyOf " : [ { " allOf " : [ { " $ref " : " urn : setvar1 #... _urn : setvar1_urn : setvar2_urn : close_x1 " } , { " $ref " : " urn : setvar2 #... _urn : setvar1_urn : setvar2_urn : close_not . x2 " } ] } , { " allOf " : [ { " $ref " : " urn : setvar1 #... _urn : setvar1_urn : setvar2_urn : close_not . x1 " } , { " $ref " : " urn : setvar2 # u ... _urn : setvar1_urn : setvar2_urn : close_x2 " } ] } ] } , " urn : close # urn : psi_urn : start_urn : setvar1_phi " : { " $anchor " : " urn : psi_urn : start_urn : setvar1_phi " , " anyOf " : The keyword "unevaluatedProperties" is applied to the instance properties that have not been evaluated by adjacent keywords, as discussed in Section 1.3, but, unfortunately, the definition in [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF] of what counts as evaluated presents some ambiguities.

The successful application of a "properties" keyword evaluates all instance properties whose name appears in the value of the "properties" keyword; in Figure 1, these are the properties named "data" or "children". Moreover, a property is evaluated by the successful application of a keyword that invokes a schema that evaluates that property, as happens in Figure 1 with the keyword "$ref" : "https://example.com/simple-tree#tree".

If, however, the "properties" keyword fails, then the specifications of Draft 2020-12 ( [START_REF] Wright | JSON Schema: A Media Type for Describing JSON Documentsdraft-bhutton-json-schema-01[END_REF]) are ambiguous. They state without any ambiguity that validation will fail, but they give contradictory indications about which instance fields are evaluated, which is a problem, since it affects the error messages and the annotations returned by the validation tool. Consider the following example.

Example 1. The following schema expresses the fact that a property "a", if present, must have type "integer", and that no other property, neither equal to "b" nor different from "a" and "b", may appear.

1 { 2 " $id " : " https : // frml . edu / onlya_no_b . json " , 3 " type " : " object " , 4 " properties " : { 5 " a " : { " type " : " integer " } , When applied to the instance { "a" : 0, "b" : 0, "c" : 0 }, this schema fails, because of properties "b" and "c". While this is clear, it is not clear which properties count as evaluated by the "properties" keyword, hence, which error messages should be produced by "unevaluatedProperties". This is testified by the discussion in [START_REF] Neal | Ambiguous behaviour of "additionalProperties" when invalid[END_REF], by that in [START_REF] Jacobson | The meaning of "additionalProperties" has changed[END_REF], and by several more that are cited therein.

We tested the above schemas with the json-everything validator [START_REF]json-everything validator[END_REF], Jim Blackler's JSON tools [START_REF] Blackler | JSON Generator[END_REF], the jschon.dev validator [1], and Hyperjump [START_REF]Hyperjump JSON Schema Validator[END_REF], in the online-versions on 10/30/2022. These are established well-known validators that support Draft 2019-09 and Draft 2020-12. By analyzing their output, reported respectively in Figures 10,[START_REF] Bergman | Bowtie JSON Schema Meta Validator[END_REF][START_REF] Bergman | JSON-Schema-Test-Suite[END_REF], and 13, (Appendix I), we observe that the first two validators apply "unevaluatedItems" to "c" only, hence they regard every matching field as evaluated even when "properties" fails; we call it the failure-tolerating interpretation: every property that matches is evaluated, even if the keyword fails, and even if the subschema applied to that property fails, as happens here to "b". However, jschon.dev applies "unevaluatedProperties" to "a", "b", and "c", hence it considers no property as evaluated; we call it the success-only interpretation: when the keyword fails no property is regarded as evaluated, neither "a", whose value satisfies the "type" : "integer" assertion, neither "b". Finally, Hyperjump does not apply "properties" to any object property, because it adopts an interpretation where the failure of "properties" produces a special null annotation that completely prevents the execution of "unevaluatedProperties"; we call it the null-annotation interpretation.

In this paper we formalize the failure-tolerating interpretation, since it seems the one that is currently more accepted by the community. Moreover, we provide a formal framework where these different interpretations can be formalized and discussed.

It is important to clarify that these ambiguities do not affect validation, since they only arise with failing schemas, but they are still very relevant, because they affect the error messages and, more importantly, the mental model of the specification reader. Whoever reads the specification

I OUTPUT EXAMPLES

Instance:

{ " a " : 0 , " b " : 0 , " c " : 0 } Schema:

1 { 2 " $id " : " https : // formalize . edu / onlya_no_b . json " ,

3

" type " : " object " ,

4

" properties " : { 5 " a " : { " type " : " integer " } ,

111:48

Instance:

{ " a " : 0 , " b " : 0 , " c " : 0 } Schema:

{ " $id " : " https : // formalize . edu / onlya_no_b . json " , " type " : " object " , " properties " : { " a " : { " type " : " integer " } , " b " : false } , " u n e v a l u a t e d P r o p e r t i e s " : false { " a " : 0 , " b " : 0 , " c " : 0 } Schema:

1 { 2 " $id " : " https : // formalize . edu / onlya_no_b . json " ,

3

" type " : " object " ,

4

" properties " : { 5 " a " : { " type " : " integer " } ,

Instance:

{ " a " : 0 , " b " : 0 , " c " : 0 } Schema:

1 { 2 " $id " : " https : // formalize . edu / onlya_no_b . json " ,

3

" type " : " object " ,

4

" properties " : { 5 " a " : { " type " : " integer " } ,