10 Formally Verifiable JSON Schema Subset
This chapter covers formally verifiable json schema subset aspects of AMATELUS.
10.1 Abstract
The AMATELUS protocol employs a formally verifiable subset of JSON Schema 2020-12 for Verifiable Credentials validation. This subset is specifically designed to enable formal verification in Lean 4 without axioms or partial definitions.
10.2 Design Principles
The JSON Schema subset is built on these principles:
Formal Verification: All features MUST be provably terminating in Lean 4
Protocol Guarantee: Only features in this subset are guaranteed by AMATELUS protocol
Implementation Freedom: Wallets MAY support full JSON Schema 2020-12 beyond protocol guarantees
Deterministic Validation: Same schema produces identical results across all implementations
Future Evolution: As Lean capability increases, subset expands toward full JSON Schema 2020-12
10.3 Formalization Strategy
10.3.1 Why a Subset?
Full JSON Schema 2020-12 includes features that prevent formal verification:
Circular references (via $ref, $defs): Cause non-termination
Dynamic property validation (additionalProperties, patternProperties): Require unbounded iteration
Infinite nesting: Composition keywords can nest arbitrarily
Format annotations: Depend on external specifications
The subset eliminates these features to enable formal verification.
10.3.2 Lean Formalization Structure
inductive SchemaKeyword | type : List String -> SchemaKeyword | maxLength : Nat -> SchemaKeyword | minLength : Nat -> SchemaKeyword | pattern : String -> SchemaKeyword | maximum : Float -> SchemaKeyword | minimum : Float -> SchemaKeyword | multipleOf : Float -> SchemaKeyword | maxItems : Nat -> SchemaKeyword | minItems : Nat -> SchemaKeyword | uniqueItems : Bool -> SchemaKeyword | items : Schema -> SchemaKeyword | maxProperties : Nat -> SchemaKeyword | minProperties : Nat -> SchemaKeyword | required : List String -> SchemaKeyword | properties : List (String × Schema) -> SchemaKeyword | enum : List JSONValue -> SchemaKeyword | const : JSONValue -> SchemaKeyword | allOf : List Schema -> SchemaKeyword | anyOf : List Schema -> SchemaKeyword | oneOf : List Schema -> SchemaKeyword | not : Schema -> SchemaKeyword | title : String -> SchemaKeyword | description : String -> SchemaKeyword
Note: Excluded keywords like $ref, additionalProperties, format are not in the inductive type.
10.3.3 Termination Guarantee
All supported features are provably terminating:
No circular references: $ref excluded entirely
Bounded recursion: Composition nesting limited to 3 levels
Finite structure: All schemas have finite size
10.4 Supported Features
The following JSON Schema keywords are GUARANTEED by AMATELUS protocol:
10.4.1 Type System
type: String or array of strings (null, boolean, object, array, number, string, integer)
10.4.2 String Validation
maxLength: Non-negative integer
minLength: Non-negative integer
pattern: ECMA-262 regular expression (abstracted in Lean)
10.4.3 Numeric Validation
maximum: Inclusive upper bound
minimum: Inclusive lower bound
multipleOf: Value must be multiple of given number
10.4.4 Array Validation
maxItems: Non-negative integer
minItems: Non-negative integer
uniqueItems: Boolean (default: false)
items: Schema applied to all array items
10.4.5 Object Validation
maxProperties: Non-negative integer
minProperties: Non-negative integer
required: Array of unique property names that must exist
properties: Object mapping property names to schemas
10.4.6 Generic Validation
enum: Non-empty array of allowed values
const: Single fixed JSON value
10.4.7 Schema Composition (Depth-Limited)
allOf: Instance must validate against ALL subschemas (max 3 levels)
anyOf: Instance must validate against AT LEAST ONE subschema (max 3 levels)
oneOf: Instance must validate against EXACTLY ONE subschema (max 3 levels)
not: Instance must NOT validate against subschema (max 3 levels)
10.4.8 Annotation Keywords
title: Human-readable title (informational only)
description: Detailed description (informational only)
10.5 Excluded Features
The following JSON Schema features are NOT GUARANTEED at protocol level:
10.5.1 Reference Keywords
$ref: Schema references (prevents termination proof)
$defs: Schema definitions (only useful with $ref)
$dynamicRef, $dynamicAnchor: Dynamic references
10.5.2 Dynamic Property Validation
additionalProperties: Ignored at protocol level (wallets MAY validate)
patternProperties: Not supported
propertyNames: Not supported
unevaluatedProperties, unevaluatedItems: Not supported
10.5.3 Other Excluded Keywords
if, then, else: Conditional schemas (use oneOf instead)
prefixItems, contains: Advanced array features
dependentRequired, dependentSchemas: Dependency keywords
exclusiveMaximum, exclusiveMinimum: Exclusive bounds
format: Format annotations (use pattern instead)
10.6 Conformance Requirements
10.6.1 Conformant Schema
A schema is AMATELUS-conformant if:
Contains ONLY keywords from supported features
Composition nesting does NOT exceed 3 levels
required array contains unique strings
enum array is non-empty
Numeric constraints are valid numbers
Size constraints are non-negative integers
multipleOf is greater than 0
10.6.2 Conformant Validator
An AMATELUS-conformant validator MUST:
Validate all supported keywords correctly
Ignore excluded keywords without error (e.g., additionalProperties)
Enforce nesting depth limit (3 levels)
Produce deterministic results
Reject schemas exceeding nesting limits
10.7 Future Evolution: Convergence Toward Full JSON Schema
10.7.1 Current Status
This subset represents a formally verifiable foundation. As Lean’s formalization capabilities advance, the subset will gradually expand toward full JSON Schema 2020-12 compliance.
10.7.2 Formalization-Driven Expansion
The expansion strategy follows a principle: expand the subset only as new features become provably terminating in Lean.
Lean 4 v1.0 onwards: Recursive reference support (with termination metrics) may enable $ref formalization
Future versions: Advanced pattern matching and dependent types may enable:
Dynamic property validation with bounded iteration proofs
Conditional schema validation
More complex nesting patterns
Goal: Eventually, full JSON Schema 2020-12 becomes formally verifiable
10.7.3 Backward Compatibility
Current AMATELUS-conformant schemas remain valid
New features are only added when formally verified
Protocol versioning ensures interoperability during transitions
Wallets always free to support full JSON Schema 2020-12 beyond protocol guarantees
10.7.4 Versioning Strategy
AMATELUS JSON Schema Subset v1.0 (current) - Formally verified features: 20+ keywords - Excluded features: circular refs, dynamic validation, format AMATELUS JSON Schema Subset v1.1 (hypothetical) - New formalization: conditional validation via oneOf expansion - Result: if/then/else pattern becomes recommended practice AMATELUS JSON Schema Subset v2.0 (future) - Lean capability: recursive references with termination proof - Result: $ref support added with formal verification guarantees
10.8 Example: AMATELUS-Conformant VC Schema
{
"title": "Identity Credential",
"type": "object",
"properties": {
"type": {
"type": "string",
"enum": ["IdentityCredential"]
},
"credentialSubject": {
"type": "object",
"properties": {
"givenName": {
"type": "string",
"minLength": 1,
"maxLength": 100
},
"familyName": {
"type": "string",
"minLength": 1,
"maxLength": 100
},
"birthDate": {
"type": "string",
"pattern": "^\\d{4}-\\d{2}-\\d{2}$"
}
},
"required": ["givenName", "familyName"],
"minProperties": 2,
"maxProperties": 5
}
},
"required": ["type", "credentialSubject"]
}
10.8.1 Why This Schema is Conformant
Uses only supported keywords (type, properties, required, enum, pattern)
Nesting depth is 2 levels (within limit of 3)
All constraints are valid (minLength, maxLength, minProperties, maxProperties)
No circular references or dynamic validation
Formally verifiable in Lean 4
10.9 Security and Robustness
10.9.1 Validation Guarantees
Termination: All schemas guaranteed to validate in finite time
Determinism: Same input always produces identical output
No side effects: Validation is pure computation
10.9.2 Regular Expression Safety
ReDoS prevention: Implementation SHOULD enforce regex timeout limits
Abstraction in Lean: Regex matching abstracted as MatchedString/UnmatchedString
Implementation responsibility: Wallet implementations must validate regex syntax
10.9.3 Schema Complexity Limits
Max nesting: 3 levels prevents deeply nested schemas
Max properties: No explicit limit, but implementations MAY enforce reasonable bounds
No recursion: Eliminates infinite loops and stack overflow risks