Skip to content
Logo

Native (React Native)

The native target emits a React Native module, so it covers both Android and iOS — an RN module is platform-neutral by construction. The on-device verification pipeline in this repo drives Android (APK + waydroid); shipping to iOS is ordinary React Native tooling on the same emitted app.cjs.

Emitting

let native := AppGen.emitNative helloReflected (baseText := "color:#18181b")
IO.FS.createDirAll "dist/native"
IO.FS.writeFile "dist/native/app.cjs" native
dist/native/app.cjs   the React Native module

emitNative takes optional base-style parameters:

AppGen.emitNative (a : ReflApp β)
  (baseText   : String := "")
  (baseInput  : String := "")
  (baseButton : String := "")

These exist because the web has a user-agent stylesheet and React Native does not. A <button> on the web inherits a font, a border and padding for free; an RN Pressable inherits nothing. The base styles are how you state the defaults the web got implicitly, so the two renderers agree.

One core, two renderers

        the ReflApp (data)
               │
        ┌──────┴──────┐
   appCoreJs      appCoreJs        ← the SAME emitted string
        │              │
    appDomJs       appRnJs
      web           native

appCoreJs — the Doc, step, the Eff interpreter, gates, routing — is emitted once and used by both targets. Only the renderer differs.

This is asserted, not assumed:

node test/native-core-identity.mjs

fails unless the web and native cores are byte-identical. A logic divergence between platforms would have to be a divergence from the Lean semantics on both platforms at once.

Where the platforms genuinely differ: style

The RView vocabulary carries inline CSS strings. The web renderer hands them to the DOM; the native renderer must parse them into React Native style objects. That parser is the one place a real difference can hide, so it gets the most aggressive testing in the repository:

node test/fuzz-parity.mjs 314159,1,42,303,424242,16180

Differential fuzzing over seeded synthetic apps: generate an app, emit both targets, render both, compare. The pinned seed set is curated — each seed exposed a distinct divergence class:

SeedDivergence class it caught
314159baseline
1relative font weight (bolder) and line-height
42element-buttons
303in-run element-button flow
424242inline inputs colliding with keys
16180styled{text} inheriting font:inherit

Pinning them turns one-shot finds into permanent regression coverage.

The other native gates

CheckAsserts
native-locators-hello.mjsevery handler tag is locatable on-device, so an on-device driver can find the control that fires it
native-input-sync.mjsvisible input values track state on both platforms — the RN TextInput does not drift from S
encapp-replay-rnweb.mjsthe full corpus replays against the native emit running under React-Native-web

The rnweb tier is the practical one: it executes the native renderer in a browser, so the whole corpus can run in CI without an emulator or a device.

Shipping to a device

The emitted app.cjs is a React Native module. Wrapping it in an RN project and building for a device — an Android APK or an iOS app — is ordinary React Native work and lives outside the framework: create the RN app, drop in the emitted module, point the entry at it, build.

For on-device verification, native-locators-hello.mjs is the piece that matters — it guarantees each handler tag has a locatable control, which is what an on-device driver needs to replay the corpus against a real installed app.

Recap

  • emitNative produces a React Native module with base-style parameters (baseText, baseInput, baseButton)
  • The core (appCoreJs) is byte-identical between web and native; only renderer differs
  • Differential fuzzing with six pinned seed sets ensures each divergence class is caught permanently
  • Native gates verify handler locators, input value sync, and full corpus replay on React-Native-web
  • The emitted app.cjs integrates into standard React Native projects for APK builds

Next steps