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 constraints: Excluded from this subset; authorization import must reject them
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: Unsupported; reject in authorization schemas
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
Reject authorization schemas containing excluded or unknown keywords; never silently strip constraints
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 MUST enforce a receiver-selected regex work budget or hard deadline
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: Receiver profiles MUST specify finite input and work limits
No recursion: Eliminates infinite loops and stack overflow risks
10.10 Authority Is Separate from Schema Conformance
The properties keyword constrains named properties but does not prohibit other properties. Therefore schema conformance alone never grants issuance permission. A delegation signs an explicit allowedClaims list separately from the complete raw schema. This profile grants top-level claim names; nested values are constrained by every ancestor’s schema. Nested authority paths require a separately specified profile. A claim object containing any ungranted name is rejected, even if it conforms to the schema. Duplicate object keys are rejected.
supportedAuthoritySchema checks schema positions recursively before any conversion into the subset type. Unsupported additionalProperties, references, conditions or unknown constraints cause rejection, including inside properties, items and composition branches. Property names and values of enum or const are data, not schema keywords. Backend validation must also reject malformed keyword values, non-finite numbers, excessive composition nesting and unsupported regex syntax. The raw signed schema is retained; it cannot be replaced with a weaker parsed approximation.
10.11 Mandatory Local Resource Profiles
Termination is not a practical CPU or memory bound. Each receiving profile MUST set finite limits for wire bytes, decompressed bytes, JSON nodes and nesting, array/object width, signature checks, schema branches and regex work. The streaming parser enforces byte and expansion bounds while reading, before large allocation. The receiver, not the sender, meters work. Exhaustion, timeout and unsupported validation return rejection or an explicit indeterminate result, never successful validation.
ResourceBudget, admitJSON, consumeWork and boundedRegex model these admission and exhaustion boundaries. Signature and schema adapters must enforce their supplied budgets during execution. These are local interoperability profiles, not a universal small delegation-depth limit or a network service requirement. No proof here establishes execution time of an external cryptographic or regex library.