structure AMT.LocalInput : Type

The version is an external template selector, not a prefix of the digest.

• version : ℕ
• publicKey : PublicKey

instance AMT.instReprLocalInput : Repr LocalInput

Equations

• AMT.instReprLocalInput = { reprPrec := AMT.reprLocalInput✝ }

def AMT.alphabet : List Char

Canonical wire alphabet; no checksum, separators or aliases.

Equations

• AMT.alphabet = "0123456789ABCDEFGHJKMNPQRSTVWXYZ".toList

def AMT.crockfordEncode (bytes : List UInt8) : String

MSB-first byte encoding with zero bits appended to the final 5-bit group.

Equations

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

def AMT.crockfordDecode (s : String) : Option (List UInt8)

Strict decoder; rejects aliases, lowercase and nonzero trailing padding bits.

Equations

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

def AMT.encodePublicKey (pk : PublicKey) : String

Draft-specific k + Crockford representation. This is NOT the registered multibase k (base36); interoperability requires an explicit AMT draft codec.

Equations

• AMT.encodePublicKey pk = "k" ++ AMT.crockfordEncode pk.bytes

def AMT.decodePublicKey (s : String) : Option PublicKey

Equations

• AMT.decodePublicKey s = if (!s.startsWith "k") = true then none else do let bytes ← AMT.crockfordDecode (s.drop 1) if (bytes.length == 32) = true then some { bytes := bytes } else none

def AMT.templateV0 (pk : PublicKey) : String

Exact JCS serialization of the fixed ASCII-only Version 0 template. All keys are sorted, all constants are included, no whitespace is emitted. Only the encoded public key varies; it cannot contain JSON metacharacters. This is not a general JSON canonicalizer.

Equations

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

def AMT.preimage (input : LocalInput) : Option (List UInt8)

Equations

• AMT.preimage input = if (input.version == 0 && input.publicKey.bytes.length == 32) = true then some (AMT.templateV0 input.publicKey).toUTF8.data.toList else none

def AMT.didFromHash (digest : Hash) : W3C.DID

Equations

• AMT.didFromHash digest = { value := "did:amt:" ++ AMT.crockfordEncode digest.value }

def AMT.finalizeV0 (pk : PublicKey) (did : W3C.DID) : W3C.DIDDocument

Fill self references only after hashing. W3C's data model stores resolved DID URLs; the wire form of the two relationship references is #key-1. The fixed @context is implicit in this W3C model and explicit in templateV0.

Equations

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

def AMT.matchesV0 (doc : W3C.DIDDocument) (pk : PublicKey) (did : W3C.DID) : Bool

Full Version 0 shape check, including derived references and absence of extra claims/services. Parsing must also check the fixed @context and reject unknown/duplicate JSON members before entering this W3C model.

Equations

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

def AMT.deriveWith (sha3512 : List UInt8 → Hash) (input : LocalInput) : Option (W3C.DID × W3C.DIDDocument)

Executable boundary with an explicitly supplied SHA3-512 implementation. Reject unsupported versions, malformed key sizes and wrong digest sizes.

Equations

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

def AMT.verifyWith (sha3512 : List UInt8 → Hash) (input : LocalInput) (claimed : W3C.DID) (doc : W3C.DIDDocument) : Bool

Equations

• AMT.verifyWith sha3512 input claimed doc = match AMT.deriveWith sha3512 input with | none => false | some (did, snd) => claimed == did && AMT.matchesV0 doc input.publicKey did

theorem AMT.finalized_id (pk : PublicKey) (did : W3C.DID) : (finalizeV0 pk did).id = did

theorem AMT.finalized_matches (pk : PublicKey) (did : W3C.DID) : matchesV0 (finalizeV0 pk did) pk did = true

theorem AMT.matchesV0_id (doc : W3C.DIDDocument) (pk : PublicKey) (did : W3C.DID) (h : matchesV0 doc pk did = true) : doc.id = did

Acceptance binds the completed document id to the derived id.