LAYERS 6–7 · CODEGEN

Architecture & Codegen

Three duals of one Enclave. 37 IO axioms, ~110 lines trusted JS.

3Targets

595Lines

37IO Methods

66Total Files

Codegen

Three-Layer Architecture

The protocol compiles to three deployment targets. Each is a composition of a spec type with an IO boundary. The spec is determined by Enclave. The IO boundary is axiomatized. The composition is canonical — unique implementation.

Server

Enclave → Runtime(12) → Service
Cloudflare Durable Object. Routes, DDL, handlers.

Client

Enclave → ClientRT(10) → Client
TypeScript SDK. ClientView = Enclave. Zero new types.

Frontend

AppView → FrontendRT(8) → Frontend
React app. AppView = (Enclave, AppDef, CSSApp).

Enclave — Single Source of Truth

One structure determines the complete server, SDK, and frontend. The client does not define its own type — ClientView = Enclave.

LeanEnc/Server.lean — Enclave

structure Enclave where
  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  : List Route        -- app-specific routes beyond protocol

Everything derives from these 7 fields:

Derived	Formula	Used by
`allRoutes`	protocolRoutes ++ [ws] ++ bootstrap? ++ extraRoutes	Server routing
`reads`	extraRoutes.filter(GET)	Client SDK, Frontend StateFns
`ddl`	[NODE_TABLES] ++ (hasDataView ? [SYNC_STATE] : [])	DO constructor

The Four Services

Service	Schema	DataView	Push	Bootstrap	Addressing	Extra Routes	Reads
enc-node	dynamic	✗	✓	✗	perRequest	2	0
registry	static	✓	✗	✗	singleton	6	5
chat	static	✗	✗	✓	perRequest	0	0
timeline	static	✓	✗	✓	perRequest	8	7

Trust Boundaries

37 axiomatized IO methods. Everything else — 14,869 lines of Lean — is derived, proven, or structurally enforced.

Boundary	Methods	Implementation	~Lines JS
Server Runtime	12	Cloudflare DO API	50
Client Runtime	10	fetch + WebSocket	30
Frontend Runtime	8	React hooks + DOM	20
Crypto	7	noble-curves	10
Total	37		~110

Frontend Codegen

58 React components across 5 applications, each fully specified in Lean. Every mapping is a bijection — one output per input, no creative decisions.

AppDef.interfaces → types.ts → AppDef.sdkFuncs → sdk.ts → AppDef.stateFns → api.ts

Component.state → useState → Component.effects → useEffect → Component.handlers → callbacks → Component.render → JSX

CSSApp.theme → :root vars → CSSApp.layout → grid → CSSApp.rules → CSS → CSSApp.media → @media

Lean Codebase

66 files organized in 7 layers. Each layer imports only from below. No cycles.

Layer	Files	Lines	What
1 FTA	12	946	Abstract theory — pure math, no ENC knowledge
2 Core	22	3,361	Crypto, SMT, CT, Events, RBAC, Validation, Node, SDK
3 Middleware	2	361	ECDH (1-to-1) + MLS (group) encryption
4 Apps	19	7,182	Registry, Timeline, DM, Chat, Messenger
5 Typeclasses	3	1,215	6 classes × 4 instances, 43 composition theorems
6 Bridge + UI	2	967	Theory↔Protocol mapping, React component DSL
7 Codegen	3	595	Server + Client + Frontend (three duals)
	66	14,869

ENC PROTOCOL · 66 FILES · 14,869 LINES · 162 THEOREMS