JSON config (agent writes)
    |
    +-- validate()  --> instant correctness checks (JS, no Lean needed)
    |
    +-- loadConfig() --> runtime config for EncApp
    |
    +-- toLean()    --> complete Lean 4 file (proven by native_decide)
    |
    +-- EncApp      --> headless runtime --> platform renderer
                        |
                        +-- TUI (ink)
                        +-- Web (React/Svelte/vanilla)
                        +-- Native (React Native/SwiftUI/Jetpack)
                        +-- Desktop (Electron/Tauri)

import { EncApp, Emulator, loadConfig, validate, toLean } from '@enc-protocol/enc-app'

import { EncApp, Emulator } from '@enc-protocol/enc-app'
import { config } from './apps/group/config.js'

const emu = new Emulator()
emu.initFromConfig(config)

const app = new EncApp(config.model, {
  emulator: emu,
  enclave: { identity: emu.ownerIdentity },
})

await app.start()

app.navigate('Chat')
const state = await app.state()     // { messages: [...], topic: '...' }
await app.exec('send', { content: 'hello' })

app.on('state', (s) => render(s))   // reactive updates

const app = new EncApp(model, {
  enclave: {
    nodeUrl: 'https://node1.enc.dev',
    enclaveId: 'abc...',
    identity: { pubHex, privateKey, publicKey },
  },
})

await app.start()

import { EncApp } from '@enc-protocol/enc-app'

const app = new EncApp(model, {
  adapter: myNativeAdapter,  // implements fetch, submit, subscribe, connect, disconnect
})

import { loadConfig, validate, toLean } from '@enc-protocol/enc-app'
import config from './my-app.json'

// 1. Validate (instant, no Lean compiler needed)
const result = validate(config)
// { checks: { ownerCanTerminate: true, ... }, errors: [], allPass: true }

// 2. Load into runtime format
const appConfig = loadConfig(config)
// { name, states, traits, schema, model, ... }

// 3. Transpile to Lean (deterministic, write to .lean file)
const lean = toLean(config)
// Complete Lean 4 file with types, validation theorem, codegen blocks

EncApp (orchestrator)
|-- EncRouter (navigation state machine)
|-- EncProvider (local state + adapter routing)
|   +-- Adapter (platform-specific)
|       |-- EmulatorAdapter (testing/TUI)
|       |-- NetworkAdapter (web)
|       |-- NativeAdapter (future)
|       +-- DesktopAdapter (future)
+-- Emulator (optional, in-memory Node with real crypto)

const app = new EncApp(model, config)

await app.start()                  // connect + fetch initial state
app.stop()                         // disconnect

// State
const state = await app.state()    // { fieldName: value, ... }
app.on('state', callback)          // reactive updates

// Commands
const result = await app.exec('send', { content: 'hello' })
// { ok: true, event, receipt } or { ok: false, error: '...' }

// Navigation
app.navigate('Settings')           // -> true/false
app.back()                         // -> true/false
app.currentPage                    // 'Chat'
app.availableTargets               // ['Settings', 'Members']
app.availableCommands              // [{ name, event, role, params }]
app.components                     // current page components

// Events
app.on('state', (s) => {})         // state changed
app.on('navigate', (e) => {})      // page changed
app.on('command', (e) => {})       // command executed
app.on('error', (e) => {})         // error occurred

{
  fetch(field)                      // -> Promise<data>
  submit(identity, type, content)   // -> Promise<{ ok, error?, event?, receipt? }>
  subscribe(events, callback)       // register event listener
  connect()                         // establish persistent connection
  disconnect()                      // tear down
}

User describes app
    |
Agent outputs config.json
    |
validate(json)       -- instant check (milliseconds)
    |
loadConfig(json)     -- runtime config
    |
EncApp runs it       -- any platform
    |
toLean(json)         -- formal proof (write .lean, lake build proves it)

AppModel defines:
  data: [{ name, store, encrypt }]        -- what exists
  commands: [{ name, event, role, params }] -- what can happen
  subscriptions: [{ name, source, events }] -- what to watch
  pages: [{
    name, entry, role,
    components: [{
      state: [fieldName],       -- reads from data
      commands: [cmdName],      -- dispatches commands
      subscriptions: [subName], -- listens for updates
      nav: [{ trigger, target }] -- edges to other pages
    }]
  }]