Native Protocol

Mobile instantiation of the ENC protocol via the SDD pipeline.

A native app is not handwritten. It is generated from a 34-line app.enc.json file through a deterministic pipeline: JSON → Lean spec → codegen → Expo Router app with WDK wallet onboarding, service modules, screen shells, and E2E test contracts.

0. Scope

A native application is fully determined by:

MobileApp = gen_from_enc(app.enc.json) → gen_mobile(Lean spec) → Expo Router app

Not React Navigation — Expo Router with file-based routing. The app.enc.json (34 lines) declares data schema, UI tabs, test scenarios, encryption level, and accent color. Everything else is derived.

app.enc.json  (34 lines)  → gen_from_enc.py  → spec-lean/ (Lean specs)
spec-lean/               → gen_mobile.py    → Expo Router screens
                         → gen_service_mobile.py → service module
                         → gen_test_contract.py  → testID contracts
                         → gen_test_flow.py      → E2E workflow

I. SDD Pipeline

The full pipeline from enc.json to deployed app:

The JSON declares what. The pipeline derives how. Five apps ship from five JSON files — no per-app handwriting.

{
  "app": "Chat",
  "encryption": "mls",
  "color": "#10b981",
  "data": {
    "Message":  "Member CR",
    "Reaction": "Member C",
    "Profile":  "Member C",
    ...
  },
  "ui": [
    "groups    | tab default | list groups",
    "compose   | tab         | form group-name member-key -> create",
    "group/:id |             | thread messages -> send Message",
    "profile   | tab         | form display-name bio -> save Profile"
  ],
  "test": [
    "alice creates group 'Alices Group' with [bob, charlie]",
    "alice sends 'Hello everyone!' in 'Alices Group'",
    ...
  ]
}

II. Shared Core

All five apps share a common mobile core in axioms/core/mobile/. This eliminates 93% of boilerplate — each app only generates its unique screens and service module.

axioms/core/mobile/
├── layout/RootShell.tsx           Tab navigator shell
├── wallet-setup/
│   ├── _layout.tsx               Stack navigator
│   ├── name-wallet.tsx           Step 1: wallet name
│   ├── secure-wallet.tsx         Step 2: show seed phrase
│   ├── confirm-phrase.tsx        Step 3: verify words
│   └── complete.tsx              Step 4: done
├── onboarding/WelcomeScreen.tsx    App welcome
├── constants/createColors.ts      Dynamic color palette
├── providers/MobileAppContext.tsx  App-wide state
└── lib/
    ├── seed-bridge.ts            Seed phrase persistence
    └── test-bridge.ts            __test_state emitter

III. WDK Wallet

Every mobile app includes WDK wallet onboarding. The wallet generates a BIP-39 seed phrase, derives BIP-44 keys, and stores them in secure device storage.

Onboarding flow (4 steps):
──────────────────────────
1. name-wallet      User names their wallet
2. secure-wallet    Display 12-word seed phrase
3. confirm-phrase   Verify 3 random words from phrase
4. complete         Wallet ready, navigate to app

The MobileAppConfig structure configures each app:

interface MobileAppConfig {
  appName: string          // from enc.json "app"
  color: string            // from enc.json "color"
  encryption: 'none' | 'ecdh' | 'mls'
  tabs: TabConfig[]        // from enc.json "ui" lines with "tab"
  nodeUrl: string          // ENC node endpoint
}

IV. Service Module

Generated from @service annotations in the Lean spec by gen_service_mobile.py (837 lines). Each app gets a single service module that handles identity, signing, pull, and create.

gen_service_mobile.py generates:

  getIdentity()              // derive keypair from seed
  getSession()               // sign session token
  pull(eventType)             // fetch events from node
  create(eventType, content)  // commit new event

  Encryption level determines middleware:
    none  → plain createCommit
    ecdh  → ECDH key agreement + encrypt
    mls   → MLS group key + encrypt

V. Screen Shells

Generated from @mobile and @test_contract annotations by gen_mobile.py (1,036 lines). Each UI line in enc.json produces an Expo Router screen file.

"ui" line pattern:
  "route | tab [default] | list|form|thread ..."

Generates:
  app/(tabs)/route.tsx     // tab screen (FlatList or form)
  app/route/[id].tsx       // detail screen (thread pattern)

Three screen patterns:

VI. Encryption Levels

The "encryption" field in enc.json determines the middleware layer generated into the service module:

Level    Middleware    Key management         Apps
─────    ──────────    ──────────────         ────
none     (direct)      Plain signing           Registry, Timeline
ecdh     ECDH          Pairwise DH agreement   DM
mls      MLS           Group epoch keys        Chat, Messenger

The encryption level flows through the entire pipeline: enc.json → Lean spec middleware field → gen_service_mobile.py conditional output → service module create() with appropriate encryption.

VII. __test_state Bridge

The key innovation for mobile E2E testing. Instead of fragile UI selectors, the app emits structured state to logcat via console.log. The test runner reads logcat and asserts on state — never on pixels.

// App emits state after every render
console.log('__test_state', JSON.stringify({
  screen: 'groups',
  items: groups.length,
  loading: false
}))

// Test runner reads logcat, asserts on state
// adb logcat | grep __test_state
// → zero flakiness: no timing issues, no pixel matching

This eliminates the primary source of mobile test flakiness: UI rendering timing. The test does not wait for pixels — it waits for state. State is deterministic. Pixels are not.

VIII. testID Convention

Generated by gen_test_contract.py (130 lines). Every interactive element gets a testID prop following a strict prefix convention:

Prefix     Element type         Example
──────     ────────────         ───────
btn:       Pressable/Button     testID="btn:create-group"
input:     TextInput            testID="input:group-name"
list:      FlatList             testID="list:groups"
tab:       Tab bar item         testID="tab:groups"

On Android, testID maps to resource-id, enabling UIA2 selectors in Waydroid E2E tests. The contract between generated screens and generated tests is the testID — both derive from the same Lean spec, so they cannot drift.

IX. Axiom Override Pattern

Generated screens are functional but minimal. When an app needs custom behavior beyond what the pipeline generates, axiom files in axioms/apps/{app}/mobile/ override the generated output.

Priority: axiom file > generated file
Pipeline: gen_mobile.py writes to ts/apps/{app}/mobile/
          build-ts.sh copies axioms/ over ts/ (axiom wins)

Trend: toward zero axiom overrides
  Registry:  2 axiom overrides (nodes tab, search)
  Timeline:  0 (fully generated)
  Chat:      0 (fully generated)
  DM:        0 (fully generated)
  Messenger: 1 axiom override (composed SDK)

As the generators improve, axiom overrides shrink. The goal is zero overrides — every app fully generated from enc.json.

X. Code Ratio

The SDD pipeline achieves a 1:683 JSON-to-TypeScript ratio:

Layer           Lines    Ratio
─────           ─────    ─────
JSON input      34       1
Lean specs      306      9
TypeScript out  23,222   683
                ─────
                1 : 9 : 683

34 lines of JSON produce 306 lines of Lean spec which generate 23,222 lines of TypeScript — screens, service modules, test contracts, and E2E workflows. The developer writes JSON. The pipeline writes everything else.