Client Protocol

ClientView = Enclave

server.md   Enclave           → client.md   ClientView (same type)
server.md   Enclave.reads     → client.md   read endpoints
server.md   protocolRoutes    → client.md   protocol operations
enc.md      AppSDK W          → client.md   write operations
enc.md      ECDH/MLS          → client.md   encrypt/decrypt

ClientView = Enclave = {
  schema       : SchemaMode,
  hasDataView  : Bool,
  hasPush      : Bool,
  hasBootstrap : Bool,
  addressing   : Addressing,
  encrypted    : Bool,
  extraRoutes  : [Route]
}

schema         determines valid event types (RBAC check before submit)
hasDataView    determines whether read endpoints exist
encrypted      determines whether to encrypt queries/responses
extraRoutes    source of read endpoint paths (via Enclave.reads)

write(enclave, session, w, exp):
  commit = AppSDK.buildCommit(w, session.identity, session.enclave, exp)
  body   = if enclave.encrypted
           then encryptQuery(session.signerPriv, session.seqPub, commit)
           else serialize(commit)
  (status, response) = httpPost(session.baseUrl, body)
  receipt = if enclave.encrypted
            then decryptResponse(session.signerPriv, session.seqPub, response)
            else deserialize(response)
  return receipt

Timeline:  createPost, updateProfile, like, unlike, comment, grantFollower, revokeFollower
Registry:  registerNode, registerEnclave, registerIdentity
Chat:      addMember, addAdmin, removeMember, leaveGroup, sendReaction
DM:        sendReadReceipt, sendTyping

read(enclave, session, endpoint, params):
  url = session.baseUrl ++ "/" ++ endpoint.path ++ "?" ++ params
  (status, body) = httpGet(url)
  return deserialize(body)

enc-node:   0 reads (no DataView)
registry:   5 reads (nodes, nodes/:id, enclaves/:id, resolve/:id, identities/:id)
chat:       0 reads (MLS encrypted, no DataView)
timeline:   7 reads (posts, posts/:id, feed, likes/:ref, profile/:id, search, health)

query(enclave, session, filter):
  body   = if enclave.encrypted
           then encryptQuery(session.signerPriv, session.seqPub, filter)
           else serialize(filter)
  (status, response) = httpPost(session.baseUrl, body)
  events = if enclave.encrypted
           then decryptResponse(session.signerPriv, session.seqPub, response)
           else deserialize(response)
  return events

subscribe(enclave, session, filter, onEvent):
  ws = wsConnect(session.baseUrl)
  wsSend(ws, serialize({ type: "Query", filter, session? }))
  wsOnMessage(ws, msg =>
    event = if enclave.encrypted
            then decryptPush(session.signerPriv, session.seqPub, msg)
            else deserialize(msg)
    onEvent(event)
  )
  return ws

connect(enclave, identity, baseUrl):
  seqPub = fetchSTH(baseUrl).sequencer
  sessionMgr = createSession(identity)
  return Session { identity, enclave, seqPub, baseUrl, sessionMgr }

Session = {
  identity    : Identity,
  enclave     : Hash,
  seqPub      : PubKey,
  baseUrl     : String,
  sessionMgr  : SessionManagerState
}

token      = r || session_pub || be32(expires)    -- 68 bytes
signer_priv = session_priv + sha256(session_pub || seq_pub || enclave)
signer_pub  = session_pub + t·G

ClientRuntime M = {
  pure, bind      monadic structure
  httpPost        POST request → (status, body)
  httpGet         GET request → (status, body)
  wsConnect       open WebSocket → connection state
  wsSend          send message on WebSocket
  wsOnMessage     register message callback
  wsClose         close WebSocket
  now             current timestamp
  randomBytes     generate random bytes
}

Client W M = {
  connect    : ClientView → Identity → String → M Session
  write      : ClientView → Session → W → Timestamp → M (Option Receipt)
  read       : ClientView → Session → Route → ByteArray → M (Option ByteArray)
  query      : ClientView → Session → ByteArray → M (Option (List Event))
  subscribe  : ClientView → Session → ByteArray → (Event → M Unit) → M WS
}

registry_reads         registry.reads.length = 5        (= Server.registry_reads)
timeline_reads         timeline.reads.length = 7        (= Server.timeline_reads)
chat_no_reads          chat.reads.length = 0            (= Server.chat_no_reads)
no_reads_without_dv    hasDataView = false → reads = [] (simp)
write_is_buildCommit   all writes = AppSDK.buildCommit  (axiom, proven in Instances)
reads_subset_routes    reads ⊆ extraRoutes              (axiom, structural)

Lean definition              JS SDK artifact
═══════════════════════════════════════════════════
AppSDK W constructors        sdk.createPost(text), sdk.like(id), ...
Enclave.reads                sdk.getFeed(opts), sdk.getProfile(id), ...
protocolRoutes               sdk.query(filter), sdk.getSTH(), ...
ClientRuntime                fetch() / WebSocket (trusted FFI)
Enclave.encrypted            encrypt/decrypt wiring (conditional)

sdk/lib/index.js      write methods (1 per W constructor)
                      read methods (1 per Enclave.reads route)
                      protocol methods (shared, 6)
sdk/lib/session.js    SessionManager (from Core/SDK)
sdk/lib/http.js       NodeClient (from ClientRuntime.httpPost/httpGet)
sdk/lib/ws.js         NodeWebSocket (from ClientRuntime.wsConnect)

core/sdk/lib/wallet.js    BIP-39 seed generation, BIP-32 HD derivation,
                          EVM address derivation, transaction signing,
                          ERC-20 transfers, balance queries

1. One JS method per W constructor      (bijection with AppSDK)
2. One JS method per read endpoint      (bijection with Enclave.reads)
3. Shared protocol methods              (from protocolRoutes, same for all)
4. Encrypt/decrypt wrapping             (conditional on Enclave.encrypted)

enc.md                     client.md
======                     =========

Commit                     write(enclave, session, w, exp)
Query                      query(enclave, session, filter)
Filter                     subscribe(enclave, session, filter, onEvent)
Receipt                    write return value
Event                      query/subscribe return values
Session                    connect(enclave, identity, baseUrl)
ECDH transport             if enclave.encrypted: encryptQuery/decryptResponse
MLS/ECDH content           AppMiddleware.encrypt/decrypt (application layer)

server.md                  client.md
=========                  =========

Enclave                    ClientView (= Enclave, same type)
Enclave.reads              read endpoint paths
Enclave.extraRoutes        source of reads (filtered by GET)
protocolRoutes             protocol operations (POST /, GET /sth, ...)
Runtime                    ClientRuntime (dual IO boundary)
Service                    Client (dual composition)