Typed signature preimages. Crypto callbacks are trusted implementation contracts, never booleans supplied by a requester. Prefix lengths are byte lengths.

def RequestBinding.text (s : String) : List UInt8

Equations

• RequestBinding.text s = s.toUTF8.data.toList

def RequestBinding.encode (fields : List (List UInt8)) : List UInt8

Equations

• RequestBinding.encode fields = List.flatMap encodeAHIField fields

def RequestBinding.strings (xs : List String) : List UInt8

Equations

• RequestBinding.strings xs = RequestBinding.encode (List.map RequestBinding.text xs)

def RequestBinding.nat (n : ℕ) : List UInt8

Equations

• RequestBinding.nat n = RequestBinding.text (toString n)

def RequestBinding.did (d : ValidDID) : List UInt8

Equations

• RequestBinding.did d = RequestBinding.text d.w3cDID.value

def RequestBinding.optionalNat : Option ℕ → List UInt8

Equations

• RequestBinding.optionalNat none = RequestBinding.text "none"
• RequestBinding.optionalNat (some n) = RequestBinding.encode [RequestBinding.text "some", RequestBinding.nat n]

def RequestBinding.optionalText : Option String → List UInt8

Equations

• RequestBinding.optionalText none = RequestBinding.text "none"
• RequestBinding.optionalText (some s) = RequestBinding.encode [RequestBinding.text "some", RequestBinding.text s]

def RequestBinding.claim (c : ClaimConditions) : List UInt8

Equations

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

inductive RequestBinding.KeyOperation : Type

• rotate : KeyOperation
• emergencyRevoke : KeyOperation

instance RequestBinding.instReprKeyOperation : Repr KeyOperation

Equations

• RequestBinding.instReprKeyOperation = { reprPrec := RequestBinding.reprKeyOperation✝ }

instance RequestBinding.instDecidableEqKeyOperation : DecidableEq KeyOperation

Equations

• RequestBinding.instDecidableEqKeyOperation x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

def RequestBinding.operation : KeyOperation → String

Equations

• RequestBinding.operation RequestBinding.KeyOperation.rotate = "rotate"
• RequestBinding.operation RequestBinding.KeyOperation.emergencyRevoke = "emergency-revoke"

inductive RequestBinding.RevocationScope : Type

Issuer-local scope. allIssuedByTarget never means all issuers globally.

• credentials : List String → RevocationScope
• allIssuedByTarget : RevocationScope

instance RequestBinding.instReprRevocationScope : Repr RevocationScope

Equations

• RequestBinding.instReprRevocationScope = { reprPrec := RequestBinding.reprRevocationScope✝ }

instance RequestBinding.instDecidableEqRevocationScope : DecidableEq RevocationScope

Equations

• RequestBinding.instDecidableEqRevocationScope = RequestBinding.decEqRevocationScope✝

def RequestBinding.scopeBytes : RevocationScope → List UInt8

Equations

• RequestBinding.scopeBytes (RequestBinding.RevocationScope.credentials a) = RequestBinding.encode [RequestBinding.text "credentials", RequestBinding.strings a]
• RequestBinding.scopeBytes RequestBinding.RevocationScope.allIssuedByTarget = RequestBinding.text "all-issued-by-target"

structure RequestBinding.KeyPayload : Type

• version : ℕ
• operation : KeyOperation
• targetIssuer : ValidDID
• oldDID : ValidDID
• newDID : Option ValidDID
• scope : RevocationScope
• requestId : String
• challenge : Option String
• issuedAt : ℕ
• expiresAt : ℕ
• reason : String
• transitionDays : ℕ

instance RequestBinding.instReprKeyPayload : Repr KeyPayload

Equations

• RequestBinding.instReprKeyPayload = { reprPrec := RequestBinding.reprKeyPayload✝ }

instance RequestBinding.instDecidableEqKeyPayload : DecidableEq KeyPayload

Equations

• RequestBinding.instDecidableEqKeyPayload = RequestBinding.decEqKeyPayload✝

def RequestBinding.keyBytes (p : KeyPayload) (signerRole : String) : List UInt8

Equations

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

structure RequestBinding.KeyRequest : Type

• payload : KeyPayload
• oldSignature : Signature
• newSignature : Option Signature

structure RequestBinding.KeyChecks : Type

• verifySignature : ValidDID → List UInt8 → Signature → Bool
• verifyChallenge : KeyPayload → String → Bool

  Called only for a supplied issuer challenge; must bind it to this payload.

@[reducible, inline]

abbrev RequestBinding.KeyLedger : Type

A receiver-owned ledger; commit payload and effects atomically in production.

Equations

• RequestBinding.KeyLedger = List RequestBinding.KeyPayload

inductive RequestBinding.RequestResult : Type

• rejected : RequestResult
• alreadyApplied : RequestResult
• apply : RequestResult

instance RequestBinding.instReprRequestResult : Repr RequestResult

Equations

• RequestBinding.instReprRequestResult = { reprPrec := RequestBinding.reprRequestResult✝ }

instance RequestBinding.instDecidableEqRequestResult : DecidableEq RequestResult

Equations

• RequestBinding.instDecidableEqRequestResult x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

def RequestBinding.verifyKeyRequest (req : KeyRequest) (expected : KeyOperation) (issuer : ValidDID) (now : ℕ) (interactive : Bool) (checks : KeyChecks) (budget : ResourceBudget) : Bool

Equations

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

def RequestBinding.processKeyRequest (req : KeyRequest) (expected : KeyOperation) (issuer : ValidDID) (now : ℕ) (interactive : Bool) (checks : KeyChecks) (budget : ResourceBudget) (ledger : KeyLedger) : RequestResult

Same id+same authenticated payload is idempotent; same id+different payload is rejected. Ledger partitioning is issuer-local. Cached success has no new effect.

Equations

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

def RequestBinding.applyKeyRequest (req : KeyRequest) (expected : KeyOperation) (issuer : ValidDID) (now : ℕ) (interactive : Bool) (checks : KeyChecks) (budget : ResourceBudget) (ledger : KeyLedger) : RequestResult × KeyLedger

Sequential ledger transition. Production must serialize this with the actual revocation/rotation effects; two concurrent reads must not both apply.

Equations

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

theorem RequestBinding.accepted_key_operation (req : KeyRequest) (expected : KeyOperation) (issuer : ValidDID) (now : ℕ) (interactive : Bool) (checks : KeyChecks) (budget : ResourceBudget) (h : verifyKeyRequest req expected issuer now interactive checks budget = true) : req.payload.operation = expected ∧ req.payload.targetIssuer = issuer

def RequestBinding.authorizePersonalReissue (payload : KeyPayload) (verifyIdentityRecords : ValidDID → ValidDID → ValidDID → RevocationScope → Bool) : Bool

Signature/key control never authorizes personal credential reissuance by itself. The issuer's identity-record verification must bind both DIDs and exact scope.

Equations

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

structure RequestBinding.TransferPayload : Type

• version : ℕ
• original : ClaimConditions
• originSignature : Signature
• recipient : ValidDID
• role : PresentationRole
• purpose : String
• transferId : String
• issuedAt : ℕ
• expiresAt : ℕ
• revocationRef : String

instance RequestBinding.instDecidableEqTransferPayload : DecidableEq TransferPayload

Equations

• RequestBinding.instDecidableEqTransferPayload = RequestBinding.decEqTransferPayload✝

def RequestBinding.transferBytes (p : TransferPayload) : List UInt8

Equations

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

structure RequestBinding.TransferRequest : Type

• payload : TransferPayload
• signature : Signature

structure RequestBinding.TransferChecks : Type

• verifySignature : ValidDID → List UInt8 → Signature → Bool
• verifyOriginal : ClaimConditions → Signature → Bool

  Includes origin signature, scope, expiry and status observation policy.

• verifyTransferStatus : String → Bool
• verifyAuthorization : TransferPayload → Bool

  Issuer-authorized same-person relation or explicitly scoped delegation.

def RequestBinding.verifyTransfer (req : TransferRequest) (recipient : ValidDID) (purpose : String) (role : PresentationRole) (now : ℕ) (checks : TransferChecks) (budget : ResourceBudget) : Bool

Equations

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

def RequestBinding.processTransfer (req : TransferRequest) (recipient : ValidDID) (purpose : String) (role : PresentationRole) (now : ℕ) (checks : TransferChecks) (budget : ResourceBudget) (ledger : List TransferPayload) : RequestResult

Equations

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