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.

@component.state → useReducer init → @component.update → pure function → @component.view → JSX tree

@component.messages → { type, payload } → 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

SDD Mobile Codegen

The SDD pipeline adds five codegen scripts that generate mobile apps from app.enc.json declarations. These scripts compose with the existing codegen pipeline — they share the same Lean spec source.

Script	Lines	Input	Output
`gen_from_enc.py`	1,628	`app.enc.json`	Lean spec files (App.lean, SDK.lean, Components.lean)
`gen_mobile.py`	1,036	Lean `@mobile` specs	Expo Router screen files (tabs, detail views)
`gen_service_mobile.py`	837	Lean `@service` specs	Service module (identity, signing, pull, create)
`gen_test_contract.py`	130	Lean `@test_contract`	testID constants (btn:, input:, list:, tab:)
`gen_test_flow.py`	244	Lean `@test_flow`	E2E test workflow (shared across adapters)
	3,875

app.enc.json (34 lines) → gen_from_enc.py → Lean specs

Lean specs → gen_mobile.py → app/(tabs)/*.tsx

Lean specs → gen_service_mobile.py → src/service.ts

Lean specs → gen_test_contract.py + gen_test_flow.py → test contracts + E2E flow

The encryption level (none/ecdh/mls) flows from JSON through Lean to the generated service module, determining whether create() calls use plain signing, ECDH key agreement, or MLS group encryption.

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