Enclave → Runtime → Service → Cloudflare DO. One structure determines the complete backend.
The FTA defines an abstract ordering authority trusted to order, not to read or forge. The ENC protocol instantiates it as a sequencer Node running inside a Durable Object. This document specifies the four backend services that compose the server.
fta.md ordering authority → enc.md sequencer / Node fta.md data space → enc.md enclave fta.md reduce → enc.md validateCommit pipeline fta.md Store → enc.md NodeStore / DataViewStore fta.md Binding.Push → enc.md WebSocket subscription + P/N delivery
Each service is a Cloudflare Worker dispatching to Durable Objects. Each DO is an FTA Store (fta.md §VI) with provable = true.
A service is fully determined by:
Enclave = (SchemaMode, hasDataView, hasPush, hasBootstrap, Addressing, encrypted, extraRoutes)
Routes, DDL, handlers, client read endpoints, frontend fetches — ALL derive from this single structure. No re-specification.
┌─────────────────────────────────────────────┐ │ registry │ │ singleton RegistryDO (Node + DataView) │ │ discovery: nodes, enclaves, identities │ └──────────┬──────────────────────────────────┘ │ resolves to ┌───────────────┼───────────────────┐ │ │ │ ▼ ▼ ▼ ┌──────────┐ ┌──────────┐ ┌──────────┐ │ enc-node │ │ chat │ │ timeline │ │EnclaveDO │ │ ChatDO │ │TimelineDO│ │ per-enc │ │per-group │ │ per-user │ │ Node │ │ Node │ │Node + DV │ │ push out │ │ MLS enc │ │plaintext │ └──────────┘ └──────────┘ └──────────┘ │ ▲ │ P/N delivery (enc.md §VI) │ └────────────────────────────────┘
All four services share the same Node core: the commit pipeline, proof endpoints, WebSocket protocol, and persistence layer defined in enc.md §III–§VIII. They differ only in the seven fields of the Enclave structure.
Every DO that runs a Node implements the following. This is the ordering authority from fta.md §0 made concrete.
validateCommit(commit, node_state): 1. Structure required fields, valid types 2. Expiration exp ≥ now - 60s ∧ exp ≤ now + 3600s 3. Hash commit_hash = H(0x10, enclave, from, type, content_hash, exp, tags) 4. Signature schnorr_verify(from, commit_hash, sig) 5. Dedup commit_hash ∉ recent set 6. Lifecycle Terminated|Migrated → reject; Paused → only Resume|Terminate|Migrate 7. RBAC schema.permits(roles_of(from), type, op) 8. AC logic target_roles check, Self match, ownership 9. Finalize assign seq, timestamp, seq_sig, event_hash, event_id 10. SMT update role bitmask (AC events only) 11. CT append to bundle; full bundle → CT leaf 12. Persist write event + node_state to SQL 13. Broadcast notify WebSocket subscribers 14. Push enqueue P/N delivery (enc-node only)
Steps 1–8 are fta.md Theorem 4 (Guard): unauthorized → state unchanged. Steps 9–11 are fta.md Theorems 16–22 (Origin, Order, Proof).
Every Node DO exposes 6 protocol routes plus WebSocket:
POST / handleMultiplexedPost commit / query / pull GET /sth handleSTH Signed Tree Head POST /inclusion handleInclusion CT inclusion proof POST /state handleState SMT state proof GET /info/manifest handleInfoManifest GET /info/enclave handleInfoEnclave GET / (WS upgrade) handleWebSocketUpgrade enc.md §VII WebSocket
The unified POST / detects request type by field presence: exp → Commit, type:"Query" → Query, type:"Pull" → Pull.
events seq INTEGER PRIMARY KEY, id, hash, enclave, from_pub, type, content, exp, sig, timestamp, seq_sig, type_seq node_state key TEXT PRIMARY KEY, value TEXT
DataView DOs additionally persist:
sync_state enclave TEXT PRIMARY KEY, last_seq INTEGER, updated_at INTEGER
The complete specification of one Durable Object class.
Enclave = {
schema : SchemaMode, -- .fixed Schema | .dynamic
hasDataView : Bool, -- colocated read index
hasPush : Bool, -- outbound P/N delivery
hasBootstrap : Bool, -- _bootstrap endpoint
addressing : Addressing, -- .perRequest segment | .singleton name
encrypted : Bool, -- transport encryption flag
extraRoutes : [Route] -- app-specific routes beyond protocol
}Route table:
allRoutes(e) = protocolRoutes ++ [wsRoute] ++ (if e.hasBootstrap then [bootstrapRoute] else []) ++ e.extraRoutes
DDL:
ddl(e) = [NODE_TABLES_DDL]
++ (if e.hasDataView then [SYNC_STATE_DDL] else [])Read endpoints (used by client.md and web.md):
reads(e) = if e.hasDataView then e.extraRoutes.filter(r => r.method == GET) else []
Read endpoints are not separately specified. They are derived from extraRoutes by filtering for GET methods. This is the single source of truth for both server routing and client SDK generation.
Generic sequencer. Dynamic schema. Only service that delivers P/N.
Enclave = {
schema = .dynamic,
hasDataView = false,
hasPush = true,
hasBootstrap = false,
addressing = .perRequest 1,
encrypted = true,
extraRoutes = [
GET /consistency handleConsistency
POST /bundle handleBundle
]
}Push tables:
push_endpoints identity TEXT, url TEXT, enclave TEXT, UNIQUE(identity, url) push_pending id INTEGER PRIMARY KEY, queue_key, event_seq, enclave push_seq queue_key TEXT PRIMARY KEY, seq INTEGER push_delivered id INTEGER PRIMARY KEY, identity, url, push_seq, payload, delivered_at
Push delivery via alarm(): initial 1s, 2× backoff, max 5 min, max 10 retries.
Singleton discovery service. Node + colocated DataView.
Enclave = {
schema = .fixed Registry.App.schema,
hasDataView = true,
hasPush = false,
hasBootstrap = false,
addressing = .singleton "registry",
encrypted = false,
extraRoutes = [
GET /nodes handleGetNodes
GET /nodes/:id handleGetNode
GET /enclaves/:id handleGetEnclave
GET /resolve/:id handleResolve
GET /identities/:id handleGetIdentity
POST /push handlePush
]
}Derived reads: 5 GET endpoints.
DataView tables:
nodes seq_pub TEXT PRIMARY KEY, endpoints, protocols, enc_v, from_pub, registered_at enclaves enclave_id TEXT PRIMARY KEY, node_pub, manifest, from_pub, registered_at, app identities pub_key TEXT PRIMARY KEY, display_name, avatar, bio, registered_at
Discovery: id_pub → GET /identities/:id → enclave_id → GET /resolve/:id → node.
MLS-encrypted group chat. No DataView (server cannot index ciphertext).
Enclave = {
schema = .fixed Chat.App.schema,
hasDataView = false,
hasPush = false,
hasBootstrap = true,
addressing = .perRequest 1,
encrypted = false,
extraRoutes = []
}Derived reads: 0. Clients use WebSocket for all data.
Secrecy scheme: (Tree N, Epoch, 24h, 24h). Worker-level route: POST /api/create-group.
Public microblog. Node + colocated DataView.
Enclave = {
schema = .fixed Timeline.App.schema,
hasDataView = true,
hasPush = false,
hasBootstrap = true,
addressing = .perRequest 1,
encrypted = false,
extraRoutes = [
GET /posts handleGetPosts
GET /posts/:id handleGetPost
GET /feed handleGetFeed
GET /likes/:ref handleGetLikes
GET /profile/:id handleGetProfile
GET /search handleSearch
POST /push handlePush
GET /health handleHealth
]
}Derived reads: 7 GET endpoints.
DataView tables:
posts seq INTEGER PRIMARY KEY, id, from_pub, text, timestamp likes seq INTEGER PRIMARY KEY, from_pub, ref_id profiles from_pub TEXT PRIMARY KEY, display_name, bio, avatar
enc-node registry chat timeline schema dynamic static static static hasDataView ✗ ✓ ✗ ✓ hasPush ✓ ✗ ✗ ✗ hasBootstrap ✗ ✗ ✓ ✓ addressing perReq 1 singleton perReq perReq encrypted ✓ ✗ ✗ ✗ extraRoutes 2 6 0 8 reads (GET) 0 5 0 7
The IO boundary. 12 axiomatized methods that Lean declares but does not implement. Implementation is ~50 lines JS binding to Cloudflare's Durable Object API.
Runtime M = {
pure, bind monadic structure
sqlExec execute SQL statement
sqlQuery query SQL, return rows
respond return HTTP response (status + body)
getBody extract request body
getPath extract request path
acceptWS upgrade to WebSocket
sendWS send WebSocket message
now current timestamp
setAlarm schedule alarm callback
fetch outbound HTTP request
}Runtime ∘ Pipeline. Given Enclave + Runtime, Service is unique.
Service M = {
init : Enclave → SQL → M NodeState
handle : Enclave → NodeState → SQL → Request → M (NodeState × Response)
ws : Enclave → NodeState → SQL → WSConn → ByteArray → M NodeState
alarm : Enclave → NodeState → SQL → M NodeState
}alarm_noop: hasPush = false → alarm(e, ns, sql) = pure ns. pipeline_guard: failed validation → state unchanged (fta.md Theorem 4).
protocol_routes_count protocolRoutes.length = 6 decide push_only_encnode only enc-node has hasPush = true rfl dataview_iff_public registry + timeline have DataView rfl chat_opaque no DataView, no push rfl registry_singleton singleton addressing rfl registry_schema = Registry.App.schema rfl chat_schema = Chat.App.schema rfl timeline_schema = Timeline.App.schema rfl bootstrap_iff_app chat + timeline have bootstrap rfl registry_reads reads.length = 5 decide timeline_reads reads.length = 7 decide chat_no_reads reads.length = 0 decide encnode_no_reads reads.length = 0 decide ddl_without_dv no DV → [NODE_TABLES_DDL] simp ddl_with_dv DV → [NODE_TABLES, SYNC_STATE] simp alarm_noop no push → alarm = identity axiom pipeline_guard failed → state unchanged axiom
fta.md server.md
====== =========
ordering authority Enclave (7 fields determine the DO)
Store.interface protocolRoutes + wsRoute + extraRoutes
Store.auth commit sig + session token
Store.provable = true SMT + CT proof endpoints
Binding.Pull HTTP POST / (commit, query, pull)
Binding.Push WebSocket subscription + P/N delivery
reduce validateCommit steps 1–11
effect steps 12–14 (persist, broadcast, push)
Lean codegen
==== ======
Enclave one DO class per Enclave definition
Enclave.allRoutes Worker route dispatch
Enclave.ddl DO constructor (SQL CREATE TABLE)
Enclave.reads Client SDK read methods (client.md)
Runtime (12 methods) ~50 lines JS (Cloudflare DO API)
Service (4 entry points) DO class (init, fetch, webSocketMessage, alarm)ENC PROTOCOL · 66 FILES · 14,869 LINES · 162 THEOREMS