inductive JSONValue : Type

JSON値の型定義

JSON仕様（RFC 8259）に基づく6つのプリミティブ型：

• null: ヌル値
• bool: 真偽値
• number: 数値（整数または浮動小数点）
• string: 文字列
• array: 値の順序付きリスト
• object: キー・値ペアの非順序集合

設計上の注意:

• numberは簡略化のためFloatで表現（実際のJSON仕様では任意精度）
• objectはList (String × JSONValue)で表現（重複キーは許容）

• null : JSONValue
• bool : Bool → JSONValue
• number : Float → JSONValue
• string : String → JSONValue
• array : List JSONValue → JSONValue
• object : List (String × JSONValue) → JSONValue

instance instReprJSONValue : Repr JSONValue

Equations

• instReprJSONValue = { reprPrec := reprJSONValue✝ }

instance instBEqJSONValue : BEq JSONValue

Equations

• instBEqJSONValue = { beq := beqJSONValue✝ }

def JSONValue.lookup (obj : List (String × JSONValue)) (key : String) : Option JSONValue

オブジェクトからプロパティを検索

Equations

• JSONValue.lookup obj key = List.lookup key obj

def JSONValue.arrayLength : JSONValue → Option Nat

配列の長さを取得

Equations

• (JSONValue.array items).arrayLength = some items.length
• x✝.arrayLength = none

def JSONValue.objectSize : JSONValue → Option Nat

オブジェクトのプロパティ数を取得

Equations

• (JSONValue.object props).objectSize = some props.length
• x✝.objectSize = none

def JSONValue.numberIsInt (f : Float) : Bool

数値が整数かどうかを判定

Equations

• JSONValue.numberIsInt f = (f.floor == f)

def JSONValue.isType : JSONValue → String → Bool

JSON値が指定された基本型かどうかを判定

Equations

• JSONValue.null.isType "null" = true
• (JSONValue.bool a).isType "boolean" = true
• (JSONValue.number a).isType "number" = true
• (JSONValue.number n).isType "integer" = JSONValue.numberIsInt n
• (JSONValue.string a).isType "string" = true
• (JSONValue.array a).isType "array" = true
• (JSONValue.object a).isType "object" = true
• x✝¹.isType x✝ = false

@[reducible, inline]

abbrev JSONPointer : Type

JSON Pointer型（エラーパスの表現に使用）

Equations

• JSONPointer = String

inductive Schema : Type

JSON Schema型（AMATELUSサブセット）

JSON Schemaは以下のいずれか：

• Boolean schema: true (すべて受理) または false (すべて拒否)
• Object schema: キーワードのリストを含むオブジェクト

サブセットの特徴:

• $ref, $defs を含まない（循環参照を防止）
• additionalProperties を検証しない（プロトコルレベルで無視）
• if/then/else を含まない（oneOf で代替）

• boolSchema : Bool → Schema
• objectSchema : List SchemaKeyword → Schema

inductive SchemaKeyword : Type

スキーマキーワードの型（AMATELUSサブセット）

サポートされるキーワード:

• 型: type
• 文字列: maxLength, minLength, pattern
• 数値: maximum, minimum, multipleOf
• 配列: maxItems, minItems, uniqueItems, items
• オブジェクト: maxProperties, minProperties, required, properties
• 汎用: enum, const
• 組み合わせ: allOf, anyOf, oneOf, not (最大3レベル)
• アノテーション: title, description (検証に影響しない)

除外されたキーワード:

• $ref, $defs, $dynamicRef (参照系)
• additionalProperties, patternProperties (動的検証)
• if, then, else (条件分岐)
• format (フォーマット検証)
• その他のアノテーション (default, examples, deprecated, etc.)

• 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

def Schema.getType : Schema → Option (List String)

スキーマからtypeキーワードを取得

Equations

• (Schema.objectSchema keywords).getType = List.findSome? (fun (kw : SchemaKeyword) => match kw with | SchemaKeyword.type types => some types | x => none) keywords
• x✝.getType = none

def Schema.getRequired : Schema → List String

スキーマからrequiredキーワードを取得

Equations

• One or more equations did not get rendered due to their size.
• x✝.getRequired = []

def Schema.getProperties : Schema → List (String × Schema)

スキーマからpropertiesキーワードを取得

Equations

• One or more equations did not get rendered due to their size.
• x✝.getProperties = []

structure ValidationError : Type

バリデーションエラーの情報

• message : String
• path : JSONPointer
• keyword : String

instance instReprValidationError : Repr ValidationError

Equations

• instReprValidationError = { reprPrec := reprValidationError✝ }

inductive ValidationResult : Type

バリデーション結果

• valid : ValidationResult
• invalid : List ValidationError → ValidationResult

instance instReprValidationResult : Repr ValidationResult

Equations

• instReprValidationResult = { reprPrec := reprValidationResult✝ }

def ValidationResult.isValid : ValidationResult → Bool

バリデーション結果が有効かどうか

Equations

• ValidationResult.valid.isValid = true
• (ValidationResult.invalid a).isValid = false

def ValidationResult.combineAll : List ValidationResult → ValidationResult

複数の結果を結合（すべて有効なら有効）

Equations

• One or more equations did not get rendered due to their size.
• ValidationResult.combineAll [] = ValidationResult.valid
• ValidationResult.combineAll (ValidationResult.valid :: rest) = ValidationResult.combineAll rest

def ValidationResult.combineAny : List ValidationResult → ValidationResult

複数の結果のうち少なくとも1つが有効なら有効

Equations

• One or more equations did not get rendered due to their size.
• ValidationResult.combineAny [] = ValidationResult.invalid [{ message := "No schemas to validate against", path := "", keyword := "anyOf" }]

def ValidationResult.combineOne : List ValidationResult → ValidationResult

複数の結果のうちちょうど1つが有効なら有効

Equations

• One or more equations did not get rendered due to their size.
• ValidationResult.combineOne [] = ValidationResult.invalid [{ message := "No schemas to validate against", path := "", keyword := "oneOf" }]

@[reducible, inline]

abbrev RegexPattern : Type

正規表現パターン型

Equations

• RegexPattern = String

structure MatchedString : Type

マッチ成功した文字列

正規表現パターンにマッチした文字列を表す型。 型レベルで正規性を保証し、UnknownVCと同様の設計パターンを使用。

設計:

• 実際の正規表現エンジン（ECMA-262）は外部実装に依存
• プロトコルレベルではマッチ成功を抽象化
• Issuer/Validatorが正しい実装を使用することを前提

• value : String
• pattern : RegexPattern

instance instReprMatchedString : Repr MatchedString

Equations

• instReprMatchedString = { reprPrec := reprMatchedString✝ }

structure UnmatchedString : Type

マッチ失敗した文字列

正規表現パターンにマッチしなかった文字列を表す型。

設計:

• 型レベルでマッチ失敗を表現
• 実装の詳細は抽象化

• value : String
• pattern : RegexPattern
• reason : String

instance instReprUnmatchedString : Repr UnmatchedString

Equations

• instReprUnmatchedString = { reprPrec := reprUnmatchedString✝ }

inductive UnknownMatchResult : Type

未検証のマッチ結果

正規表現マッチングの結果を表す和型。 ValidVC/InvalidVCと同様の設計パターン。

命名の意図:

• 「UnknownMatchResult」= 構造的には存在するが、マッチ状態は未確定または既知
• マッチ成功/失敗のいずれかを型レベルで表現

設計の利点:

• 正規表現エンジンの実装詳細を抽象化
• プロトコルレベルでは「マッチ/非マッチ」の区別のみが重要
• 実装バグはunmatchedとして表現され、プロトコルの安全性には影響しない

• matched : MatchedString → UnknownMatchResult
• unmatched : UnmatchedString → UnknownMatchResult

instance instReprUnknownMatchResult : Repr UnknownMatchResult

Equations

• instReprUnknownMatchResult = { reprPrec := reprUnknownMatchResult✝ }

def UnknownMatchResult.checkMatch : UnknownMatchResult → Bool

マッチ検証関数（定義として実装）

設計の核心:

• マッチ成功（matched）: 常に検証成功
• マッチ失敗（unmatched）: 常に検証失敗

この単純な定義により、正規表現エンジンの詳細を抽象化しつつ、 プロトコルの安全性を形式的に証明できる。

Equations

• (UnknownMatchResult.matched a).checkMatch = true
• (UnknownMatchResult.unmatched a).checkMatch = false

def UnknownMatchResult.isMatched (result : UnknownMatchResult) : Prop

マッチ結果が成功かどうかを表す述語

Equations

• result.isMatched = (result.checkMatch = true)

theorem UnknownMatchResult.matched_string_passes (ms : MatchedString) : (matched ms).isMatched

Theorem: マッチ成功した文字列は常に検証成功

正規表現にマッチした文字列は、検証が成功する。 これは定義から自明だが、明示的に定理として示す。

theorem UnknownMatchResult.unmatched_string_fails (us : UnmatchedString) : ¬(unmatched us).isMatched

Theorem: マッチ失敗した文字列は常に検証失敗

正規表現にマッチしなかった文字列は、検証が失敗する。

structure ValidJSONValue : Type

スキーマに対して有効な JSON 値

型レベルでバリデーション成功を保証。 実際の検証ロジックは実装側（Rust/TypeScript等）で行われる。

設計:

• ValidVC と同じパターン
• 型自体が「検証済み」を表現
• プロトコルレベルでは抽象化

• value : JSONValue
• schema : Schema

structure InvalidJSONValue : Type

スキーマに対して無効な JSON 値

型レベルでバリデーション失敗を保証。 実装側のバリデーターがエラーを検出した場合に使用される。

設計:

• InvalidVC と同じパターン
• エラー情報を含む（デバッグ用）

• value : JSONValue
• schema : Schema
• errors : List ValidationError

inductive UnknownValidation : Type

未検証のバリデーション結果

構造的にはJSON値とスキーマのペアだが、バリデーション結果を表す和型。 ValidVC/InvalidVCと同様の設計パターン。

命名の意図:

• 「UnknownValidation」= 構造的には存在するが、バリデーション状態は未確定または既知
• valid/invalid のいずれかを型レベルで表現

設計の利点:

• バリデーションロジックの実装詳細を抽象化
• プロトコルレベルでは「valid/invalid」の区別のみが重要
• 実装バグはinvalidとして表現され、プロトコルの安全性には影響しない

• valid : ValidJSONValue → UnknownValidation
• invalid : InvalidJSONValue → UnknownValidation

def UnknownValidation.checkValidation : UnknownValidation → Bool

バリデーション検証関数（定義として実装）

設計の核心:

• 有効なJSON値（valid）: 常に検証成功
• 無効なJSON値（invalid）: 常に検証失敗

この単純な定義により、バリデーションロジックの詳細を抽象化しつつ、 プロトコルの安全性を形式的に証明できる。

実装の責任:

• 実装側（Rust/TypeScript）が実際のバリデーションを行う
• Lean側は型と性質のみを定義

Equations

• (UnknownValidation.valid a).checkValidation = true
• (UnknownValidation.invalid a).checkValidation = false

def UnknownValidation.isValid (validation : UnknownValidation) : Prop

バリデーション結果が有効かどうかを表す述語

Equations

• validation.isValid = (validation.checkValidation = true)

theorem UnknownValidation.valid_json_passes (vjv : ValidJSONValue) : (valid vjv).isValid

Theorem: 有効なJSON値は常に検証成功

型レベルで有効と判定されたJSON値は、検証が成功する。 これは定義から自明だが、明示的に定理として示す。

theorem UnknownValidation.invalid_json_fails (ijv : InvalidJSONValue) : ¬(invalid ijv).isValid

Theorem: 無効なJSON値は常に検証失敗

型レベルで無効と判定されたJSON値は、検証が失敗する。

theorem Schema.true_accepts_all (value : JSONValue) : (UnknownValidation.valid { value := value, schema := boolSchema true }).isValid

Theorem: Boolean schema true はすべての値を受理

Boolean schema true に対しては、任意のJSON値が有効。

theorem Schema.false_rejects_all (value : JSONValue) : ¬(UnknownValidation.invalid { value := value, schema := boolSchema false, errors := [{ message := "Schema is 'false' (rejects all values)", path := "", keyword := "false" }] }).isValid

Theorem: Boolean schema false はすべての値を拒否

Boolean schema false に対しては、任意のJSON値が無効。

structure ValidSchema : Type

正規のスキーマ（AMATELUSサブセット）

構文的に正しく、バリデーションに使用できるスキーマ。

制約:

• required配列の要素は一意
• enum配列は空でない
• 数値制約は有効な範囲
• composition keywordsのネスト深さは最大3レベル
• $ref, $defs を含まない

• schema : Schema

structure InvalidSchema : Type

不正なスキーマ

構文的に誤っているか、矛盾を含むスキーマ。

• schema : Schema
• reason : String

inductive UnknownSchema : Type

未検証のスキーマ

パースされたが、正規性が未確定のスキーマ。

• valid : ValidSchema → UnknownSchema
• invalid : InvalidSchema → UnknownSchema

def UnknownSchema.checkSyntax : Schema → Bool

スキーマの構文検証

検証内容:

• required配列の一意性
• enum配列の非空性
• 数値制約の妥当性
• composition nesting depth ≤ 3

簡略化: 実装では常にtrueを返す（実際の検証は省略）

Equations

• UnknownSchema.checkSyntax x✝ = true

def UnknownSchema.toValidSchema : UnknownSchema → Option ValidSchema

未検証スキーマから正規スキーマへの変換

Equations

• (UnknownSchema.valid vs).toValidSchema = some vs
• (UnknownSchema.invalid a).toValidSchema = none

def Examples.stringSchema : Schema

例: 単純な文字列スキーマ

Equations

• Examples.stringSchema = Schema.objectSchema [SchemaKeyword.type ["string"], SchemaKeyword.minLength 1, SchemaKeyword.maxLength 100]

def Examples.personSchema : Schema

例: オブジェクトスキーマ（Person）

Equations

• One or more equations did not get rendered due to their size.

def Examples.stringArraySchema : Schema

例: 配列スキーマ

Equations

• One or more equations did not get rendered due to their size.

def Examples.colorEnumSchema : Schema

例: enum制約

Equations

• Examples.colorEnumSchema = Schema.objectSchema [SchemaKeyword.type ["string"], SchemaKeyword.enum [JSONValue.string "red", JSONValue.string "green", JSONValue.string "blue"]]

def Examples.allOfExampleSchema : Schema

例: allOf 組み合わせ

Equations

• One or more equations did not get rendered due to their size.

def Examples.oneOfExampleSchema : Schema

例: oneOf 組み合わせ（識別された和型）

Equations

• One or more equations did not get rendered due to their size.