Native Protocol

React Native instantiation of the ENC protocol.

This document defines the mobile application as generated from the same Lean @component specifications that produce the React web frontend. One spec, two platforms.

---

0. Scope

A native application is fully determined by:

AppView = (Enclave, @component specs, StyleSheet)

The same AppView triple as frontend.md, with CSS replaced by React Native StyleSheet.create(). The component logic — state, messages, update, commands — is identical. Only the rendering target changes.

frontend.md    @component → gen_react.py        → React web (.tsx)
native.md      @component → gen_react_native.py → React Native (.tsx)

Both generators read the same @component JSON blocks from the same Lean files. The state machine is platform-agnostic. The view tree is structurally identical — only the leaf nodes differ.

I. Tag Mapping

HTML elements map to React Native components:

HTML tag        React Native        Notes
───────         ────────────        ─────
div             View                All container elements
span, p, h1-h6 Text                All text content
button, a       TouchableOpacity    All pressable elements
input, textarea TextInput           All text inputs
img             Image               source={} instead of src=
form, nav       View                Structural containers

Text in React Native must always be wrapped in <Text>. A <View> cannot contain raw strings. The generator handles this automatically.

II. Event Mapping

Web events map to React Native gestures:

Web event       React Native        Context
─────────       ────────────        ───────
onClick         onPress             TouchableOpacity
onChange        onChangeText        TextInput (returns string directly)
onSubmit        onPress             Form submit → button press
onInput         onChangeText        Same as onChange in RN

The dispatch pattern is identical:

// Web (gen_react.py)
onClick={() => dispatch({ type: "Submit" })}

// Native (gen_react_native.py)
onPress={() => dispatch({ type: "Submit" })}

III. Style Mapping

CSS classes become StyleSheet references:

// Web
className="feed-header active"

// Native
style={[styles.feed_header, styles.active]}

Conditional styles:

// Web
className={`tab ${active ? "tab-active" : ""}`}

// Native
style={[styles.tab, active && styles.tab_active]}

The generator collects all cls references from the component spec and emits a StyleSheet.create() block with placeholder styles. CSS-to-RN style conversion is a separate step (manual or automated).

IV. Platform-Agnostic Architecture

The useReducer + Cmd pattern works identically on both platforms:

@component.state          → same State type
@component.messages       → same Msg union
@component.update         → same (State, Msg) → [State, Cmd]
@component.view           → View/Text/TouchableOpacity (instead of div/span/button)
@component.subscriptions  → same WebSocket handlers
@component.initCmd        → same initial data fetch

The Cmd type is platform-agnostic:

Cmd.none                  → no-op (both platforms)
Cmd.fetch(url, ok, err)   → fetch() (both platforms)
Cmd.commit(op, data, ...) → HTTP POST (both platforms)
Cmd.navigate(path)        → router.push (web) / navigation.navigate (RN)
Cmd.toast(msg, level)     → toast notification (both platforms)

Only Cmd.navigate and Cmd.toast need platform-specific runtime implementations. Everything else is identical.

V. Runtime

The native runtime mirrors axioms/frontend/runtime.ts with React Navigation instead of browser routing and native toast instead of DOM notifications.

Web runtime:     axioms/frontend/runtime.ts   (214 lines)
Native runtime:  axioms/native/runtime.ts     (planned)

The runtime is the only handwritten code. It implements the Cmd executor — the bridge between pure state machines and platform IO. Same trust boundary, different IO backend.

VI. Code Generation

gen_react_native.py (419 lines) performs:

1. Parse @component JSON from Lean files
2. Emit React Native imports (View, Text, TouchableOpacity, etc.)
3. Emit State type, Msg union, init, update — identical to web
4. Render view tree with tag/event/style mapping
5. Collect className references → StyleSheet.create()
6. Write to ts/apps/{app}/mobile/src/views/{component}.tsx

VII. Component Inventory

44 components across 5 apps:

App          Components   Largest
───          ──────────   ───────
Timeline     9            Profile (266 lines)
Chat         8            GroupThread (166 lines)
DM           7            DMThread (147 lines)
Messenger    13           MsgChatThread (98 lines)
Registry     7            ManifestWizard (101 lines)

Total: 44 components, 4,513 lines of React Native. Same count as web — every web component has a native counterpart.

VIII. Correspondence

The native generator maintains a 1:1 correspondence with the web:

Property                Web (gen_react.py)    Native (gen_react_native.py)
────────                ──────────────────    ───────────────────────────
Source specs            @component JSON       @component JSON (same)
State type              identical             identical
Msg type                identical             identical
Update function         identical             identical
Cmd type                identical             identical
View structure          div/span/button       View/Text/TouchableOpacity
Event handlers          onClick/onChange       onPress/onChangeText
Styling                 className=""           style={styles.xxx}
Output path             frontend/src/views/   mobile/src/views/

This is the key insight: the state machine is the specification. The view tree is a projection. Web and native are two projections of the same mathematical object.