def InitialMaxDepth : ℕ

初期最大信頼チェーン深さ（N階層対応）

新設計では、プロトコルレベルの上限を設けない。 各委任者がmaxDepthを指定し、単調減少により有限回で停止することを保証する。

この値は検証アルゴリズムの初期remainingDepthとして使用される。 実際の制限は各delegationのmaxDepthで決まる。

Equations

• InitialMaxDepth = 1000

structure DelegationContent : Type

委任内容（Delegation Content）- maxDepth対応

委任者から受託者へのクレーム発行権限の委譲を表現する構造。

設計思想:

• grantorDID: 権限を与える側のDID
• granteeDID: 権限を受ける側のDID
• label: クレームの表示ラベル（人間向け、機能を持たない）
• claimSchema: JSON Schema（正式な定義）
• maxDepth: 最大委任階層数（1以上の自然数、必須）

maxDepthの役割:

• この委任からさらに何階層まで委任を許可するか
• 受託者は親のremainingDepth-1と自分のmaxDepthの小さい方まで委任可能
• 計算式：nextDepth = min(parentDepth - 1, delegation.maxDepth)

• grantorDID : ValidDID

  委任者DID（権限を与える側）

• granteeDID : ValidDID

  受託者DID（権限を受ける側）

• label : String

  クレームの表示ラベル（人間向け）

• claimSchema : Schema

  Legacy parsed view for structural examples; authorization uses schemaSource.

• schemaSource : JSONValue

  Exact signed raw schema; never silently strip unsupported constraints.

• allowedClaims : List String

  Explicit issuance authority, separate from schema format validation.

• maxDepth : ℕ

  最大委任階層数（1以上の自然数）

instance instReprDelegationContent : Repr DelegationContent

Equations

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

def DelegationContent.isValidMaxDepth (d : DelegationContent) : Bool

maxDepthが有効かどうかを判定（1以上であること）

Equations

• d.isValidMaxDepth = decide (d.maxDepth ≥ 1)

def DelegationContent.beq (d1 d2 : DelegationContent) : Bool

DelegationContentの等価性判定（DID比較用）

Equations

• d1.beq d2 = (d1.grantorDID == d2.grantorDID && d1.granteeDID == d2.granteeDID && d1.label == d2.label && d1.maxDepth == d2.maxDepth)

instance DelegationContent.instBEq : BEq DelegationContent

Equations

• DelegationContent.instBEq = { beq := DelegationContent.beq }

structure W3CProof : Type

W3C Proof構造（簡略版）

実際のW3C.Proof型は別モジュールで定義されていますが、 ここでは型定義のために簡略版を使用します。

• verificationMethod : String

  検証メソッド（公開鍵へのリファレンス）

• proofValue : String

  署名値

instance instReprW3CProof : Repr W3CProof

Equations

• instReprW3CProof = { reprPrec := reprW3CProof✝ }

instance instBEqW3CProof : BEq W3CProof

Equations

• instBEqW3CProof = { beq := beqW3CProof✝ }

structure DelegationChain : Type

委任チェーン（Delegation Chain）- N階層対応

複数の委任を連鎖させた構造。

設計思想:

• delegations: 委任のリスト（順序重要：[0]が初代、[n]が最終）
• chainProofs: 各委任に対応する署名リスト（同じ長さ）
• 循環委任の検出が可能（DID重複チェック）
• 単調減少性により無限階層を防止

• delegations : List DelegationContent

  委任のリスト（[0]が初代、[n]が最終）

• chainProofs : List W3CProof

  各委任に対応する署名リスト（delegationsと同じ長さ）

instance instReprDelegationChain : Repr DelegationChain

Equations

• instReprDelegationChain = { reprPrec := reprDelegationChain✝ }

def DelegationChain.getAllDIDs (chain : DelegationChain) : List ValidDID

委任チェーン内のすべてのDIDを取得

Equations

• chain.getAllDIDs = List.flatMap (fun (d : DelegationContent) => [d.grantorDID, d.granteeDID]) chain.delegations

def DelegationChain.hasCircularDelegation (chain : DelegationChain) : Bool

循環委任チェック（DID重複がないことを確認）

アルゴリズム:

• すべてのDID（grantorDIDとgranteeDID）を抽出
• 重複があればtrue（循環委任）、なければfalse

計算量: O(n²) where n = DIDs数

Equations

• chain.hasCircularDelegation = (chain.getAllDIDs.length != chain.getAllDIDs.eraseDups.length)

def DelegationChain.depth (chain : DelegationChain) : ℕ

委任チェーンの深さ（委任の数）

Equations

• chain.depth = chain.delegations.length

def DelegationChain.computeNextDepth (parentDepth delegationMaxDepth : ℕ) : ℕ

次の階層の残り深さを計算

計算式: nextDepth = min(parentDepth - 1, delegationMaxDepth)

単調減少性:

• parentDepth = 0の場合: nextDepth = 0（これ以上委任不可）
• それ以外: parentDepth-1とmaxDepthの小さい方

例:

• computeNextDepth 5 3 = min(4, 3) = 3
• computeNextDepth 2 5 = min(1, 5) = 1
• computeNextDepth 0 5 = 0

Equations

• DelegationChain.computeNextDepth parentDepth delegationMaxDepth = if parentDepth = 0 then 0 else min (parentDepth - 1) delegationMaxDepth

@[irreducible]

def DelegationChain.verifyChain (delegations : List DelegationContent) (remainingDepth : ℕ) (trustedAnchors : List ValidDID) : Bool

委任チェーンの検証（再帰的、Nat単調減少で停止性保証）

パラメータ:

• delegations: 検証する委任のリスト
• remainingDepth: 現在の残り深さ
• trustedAnchors: 信頼されたDIDのリスト

検証ロジック:

1. delegationsが空の場合: true（検証成功）
2. remainingDepth=0の場合: false（深さ超過）
3. 先頭のdelegationを取り出し：
   • grantorDIDがtrustedAnchorsに含まれるか確認
   • nextDepthを計算（単調減少）
   • 残りのdelegationsを再帰的に検証

停止性: remainingDepthが0になるか、delegationsが空になるまで必ず減少する。 Natの単調減少により、有限回で必ず停止する。

Equations

• One or more equations did not get rendered due to their size.
• DelegationChain.verifyChain delegations 0 trustedAnchors = delegations.isEmpty
• DelegationChain.verifyChain [] depth.succ trustedAnchors = true

def DelegationChain.verifyStructure (chain : DelegationChain) (trustedAnchors : List ValidDID) : Bool

委任チェーン全体の検証

パラメータ:

• chain: 検証する委任チェーン
• trustedAnchors: 信頼されたDIDのリスト

検証内容:

1. 循環委任チェック
2. 委任チェーンの検証（verifyChain使用）

初期深さ: InitialMaxDepthを初期remainingDepthとして使用。 実際の制限は各delegationのmaxDepthで決まる。

Equations

• chain.verifyStructure trustedAnchors = if chain.hasCircularDelegation = true then false else DelegationChain.verifyChain chain.delegations InitialMaxDepth trustedAnchors

structure DelegationChain.Checks : Type

Crypto/semantic adapters must verify the complete signed delegation (including scope, schemaSource and maxDepth). Schema backend enforces the supplied branch and regex budgets and returns none for unsupported syntax or exhaustion.

• verifyDelegation : DelegationContent → W3CProof → Bool
• validateSchema : JSONValue → JSONValue → ℕ → ℕ → Option Bool

def DelegationChain.verifyLinks (checks : Checks) (budget : ResourceBudget) (value : JSONValue) (issuer : ValidDID) : ℕ → ValidDID → List ValidDID → List DelegationContent → List W3CProof → Bool

Verify a concrete claim against EVERY ancestor scope/schema. No need to solve general schema inclusion. Root anchor only; intermediate links are authenticated by delegation. Structural recursion and a local fuel bound are both explicit.

Equations

• One or more equations did not get rendered due to their size.
• DelegationChain.verifyLinks checks budget value issuer x✝² x✝¹ x✝ [] [] = (x✝¹ == issuer)
• DelegationChain.verifyLinks checks budget value issuer 0 x✝² x✝¹ (head :: tail) x✝ = false
• DelegationChain.verifyLinks checks budget value issuer x✝⁴ x✝³ x✝² x✝¹ x✝ = false

def DelegationChain.verify (chain : DelegationChain) (trustedAnchors : List ValidDID) (issuer : ValidDID) (value : JSONValue) (checks : Checks) (budget : ResourceBudget) : Bool

Public authorization boundary; profile budgets are receiver-selected.

Equations

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

structure Claim : Type

クレーム（Claim）- 属性VCに含まれる個々のクレーム

設計思想:

• 各クレームは自己完結構造（content + delegation chain + proofs）
• 0階層（直接発行）: contentのみ
• N階層（委譲発行）: content + delegationChain + contentProof
• contentProofは最終発行者によるcontentへの署名でZKP検証時にHolderの改ざんを検出

フィールド:

• content: クレームの実データ（ZKPの入力となる）
• delegationChain: 委任チェーン（N階層の場合のみ）
• contentProof: 最終発行者によるcontentへの署名（N階層の場合のみ、ZKP検証に必要）

• content : String

  クレームの実データ

• delegationChain : Option DelegationChain

  委任チェーン（None=直接発行、Some=委譲発行）

• contentProof : Option W3CProof

  最終発行者によるcontentへの署名（ZKP検証に必要）

instance instReprClaim : Repr Claim

Equations

• instReprClaim = { reprPrec := reprClaim✝ }

def Claim.makeDirectClaim (content : String) : Claim

0階層（直接発行）のクレームを構築

Equations

• Claim.makeDirectClaim content = { content := content, delegationChain := none, contentProof := none }

def Claim.makeDelegatedClaim (content : String) (chain : DelegationChain) (contentProof : W3CProof) : Claim

N階層（委譲発行）のクレームを構築

Equations

• Claim.makeDelegatedClaim content chain contentProof = { content := content, delegationChain := some chain, contentProof := some contentProof }

def Claim.isDelegated (claim : Claim) : Bool

クレームが委譲発行かどうか判定

Equations

• claim.isDelegated = claim.delegationChain.isSome

def Claim.depth (claim : Claim) : ℕ

クレームの委任階層数を取得

戻り値:

• 0: 直接発行
• N: N階層の委任チェーン

Equations

• claim.depth = match claim.delegationChain with | none => 0 | some chain => chain.depth

def Claim.verifyStructure (claim : Claim) (trustedAnchors : List ValidDID) : Bool

クレームの検証

パラメータ:

• claim: 検証するクレーム
• trustedAnchors: 信頼されたDIDのリスト

検証内容:

• 直接発行: 常にtrue（issuer検証は別途実施）
• 委譲発行: delegationChainを検証

Equations

• claim.verifyStructure trustedAnchors = match claim.delegationChain with | none => true | some chain => chain.verifyStructure trustedAnchors

def Claim.verify (claim : Claim) (issuer : ValidDID) (trustedAnchors : List ValidDID) (checks : DelegationChain.Checks) (budget : ResourceBudget) (parse : ResourceBudget → String → Option JSONValue) (verifyContent : ValidDID → String → Option W3CProof → Bool) : Bool

Original claim signature plus independently parsed content and issuance scope. The parser enforces ResourceBudget while reading; it must parse this exact content. Holder packaging is outside this original-claim verification boundary.

Equations

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

theorem computeNextDepth_decreasing (parentDepth maxDepth : ℕ) : parentDepth > 0 → DelegationChain.computeNextDepth parentDepth maxDepth < parentDepth

Theorem: computeNextDepthは単調減少

parentDepth > 0の場合、computeNextDepthの結果は必ずparentDepthより小さい。 これにより、有限回の適用でゼロに到達することが保証される。

theorem verifyChain_terminates (delegations : List DelegationContent) (remainingDepth : ℕ) (trustedAnchors : List ValidDID) : ∃ (result : Bool), DelegationChain.verifyChain delegations remainingDepth trustedAnchors = result

Theorem: verifyChainは有限回で停止

verifyChainは remainingDepth を単調減少させるため、有限回で必ず停止する。 これはtermination_by remainingDepthで自動的に保証されている。

@[irreducible]

theorem verifyChain_length_bound (delegations : List DelegationContent) (remainingDepth : ℕ) (trustedAnchors : List ValidDID) : DelegationChain.verifyChain delegations remainingDepth trustedAnchors = true → delegations.length ≤ remainingDepth

補助定理: verifyChainの長さ上限

verifyChainがtrueを返す場合、委任リストの長さはremainingDepth以下である。

証明戦略: verifyChainの構造を利用し、再帰的に証明する。 各ステップで、computeNextDepthによりremainingDepthが減少することを使う。

theorem finite_delegation_chain (delegations : List DelegationContent) (initialDepth : ℕ) (trustedAnchors : List ValidDID) : DelegationChain.verifyChain delegations initialDepth trustedAnchors = true → delegations.length ≤ initialDepth

Theorem: 委任チェーンの深さは有限

verifyChainがtrueを返す場合、委任チェーンの長さは initialDepth以下であることが保証される。

証明: 補助定理verifyChain_length_boundから直接導かれる。