Skip to content
Logo

The emitted runtime

AppGen.emit produces two interdependent pieces: a platform-neutral core (appCoreJs) and a platform-specific bundle (appDomJs for web, appRnJs for React Native). The core is byte-identical across platforms and contains the proven step semantics; the bundle layer maps UI algebra to DOM or React-Native views and wires history. This page documents the observable contract.

The APP global

Every emitted app declares a global APP object with this shape:

APP = {
  init: { scalars: {...}, tables: {...} },    // initial state doc
  pages: [ {path, view}, ... ],                // routable screens
  handlers: [ {tag, effs}, ... ],              // action → effect list
  gates: [ {scalar, page}, ... ],              // unmet gate → redirect
  binding: { /* vendor-supplied binding */ }   // routing table for host
}

State S is initialized by deep-copying APP.init:

let S = JSON.parse(JSON.stringify(APP.init));

This ensures every instance gets its own mutable S — the state is not shared across browser tabs or app instances.

State, dispatch, and effects

The state document S

S = {
  scalars: { identity, path, draft, chat_with, ... },  // string values
  tables: { messages: [...rows], contacts: [...] }     // append-only logs
}

Scalars are strings or empty string (no null in S directly; see sv(k) below). Tables are arrays of row objects; every row is a POD object keyed by declared field names.

Reading state: sv(k)

function sv(k) { 
  var v = S.scalars[k]; 
  return v == null ? '' : String(v); 
}

Always returns a string. Used by all rendering paths (node() for DOM, the RN bundle's field lookup). Null/undefined in S reads as empty string.

Dispatch: step(tag, payload)

function step(tag, payload) {
  var h = APP.handlers.find(function(x) { return x.tag === tag; });
  if (!h) return;
  var __pp = S.scalars.path;
  h.effs.forEach(function(e) { applyEff(e, payload); });
  render();
  if (typeof history !== 'undefined' && S.scalars.path !== __pp) {
    try { history.pushState({encp: S.scalars.path}, ''); } catch(e) {}
  }
}
  1. Find the handler by tag (no-op if not found).
  2. Snapshot the old path.
  3. Apply each effect in sequence.
  4. Call render() to update the display.
  5. If the path changed, push it to browser history (typeof-guarded; RN has no history).

The runtime is synchronous — effects are applied in order before re-render. Async operations (network, storage) are the adapter's responsibility.

Effect dispatch: applyEff(e, payload)

The applyEff function handles ~14 effect kinds, all deterministic and synchronous. Key examples:

// Scalar mutations
if (e.k === 'setConst') S.scalars[e.field] = e.val;
if (e.k === 'setInput') S.scalars[e.field] = payload;
 
// Table mutations (all via ADAPTER.append)
if (e.k === 'pushDraft') 
  ADAPTER.append(S.tables, e.table, postRow());
if (e.k === 'pushInput') { 
  if (S.scalars.draft && String(S.scalars.draft).trim())
    ADAPTER.append(S.tables, String(payload), postRow());
}
 
// Routing effects
if (e.k === 'routeIfHex64') {
  var rv = String(S.scalars[e.target] || '');
  if (/^[0-9a-fA-F]{64}$/.test(rv)) {
    S.scalars.chat_with = rv;
    S.scalars.path = e.valid;
  } else {
    S.scalars.path = e.invalid;
  }
}
 
// Lookup routing (e.g., find a contact by name)
if (e.k === 'lookupRoute') {
  var v = S.scalars[e.target];
  var rows = S.tables[e.table] || [];
  var hit = v ? rows.find(function(r) { return r[e.field] === v; }) : null;
  if (hit) {
    S.scalars.chat_with = v;
    S.scalars.chat_name = (hit.name != null ? hit.name : v);
    S.scalars.path = e.found;
  } else {
    S.scalars.path = e.notfound;
  }
}

Every table mutation goes through ADAPTER.append(). This is the store seam — the boundary between the proven state machine and the injectable host.

The ADAPTER seam

The ADAPTER is an object that hosts provide (or the default in-memory version is used). It has two optional methods:

append(tables, tableName, row)

Required. Called whenever an effect writes a row. The default implementation:

var ADAPTER = (typeof window !== 'undefined' && window.ENC_ADAPTER) || {
  append: function(tables, t, row) { 
    if (!tables[t]) tables[t] = [];
    tables[t] = tables[t].concat([row]);
  }
};

The default mutates S.tables in-place by concatenation. A live adapter (deployed on a server) replaces this with a call to the host's store, submits the row to a backend, receives folded events, and calls render() again to refresh the view.

init(S, render)

Optional. Called at app boot after the core runtime loads. Used for hydration — the adapter can seed S from the server, then call render() to display:

// At the end of appDomJs:
if (ADAPTER.init) ADAPTER.init(S, render);

A deployed adapter typically uses this to fetch initial state from a node. If not defined, the app starts with APP.init as-is (in-memory emulator mode).

Routing and gate evaluation

The gate evaluation happens before the path lookup, not after. This ensures an unmet gate always wins over a user-navigated path:

function pageView() {
  var path = S.scalars.path;
  
  // Route guards run BEFORE the path lookup
  var gs = (APP.gates || []);
  for (var i = 0; i < gs.length; i++) {
    var v = S.scalars[gs[i].scalar];
    if (v == null || v === '' || v === false) {
      path = gs[i].page;
      break;
    }
  }
  
  var p = APP.pages.find(function(x) { return x.path === path; });
  return p ? p.view : (APP.pages[0] && APP.pages[0].view);
}

Example: if a gate requires identity to be set, and the user navigates to /chat, the gate check runs first. If identity is empty, the path is overridden to the gate's page (typically /login).

Publication and test hooks

window.__ENC_APP (binding only)

Published immediately after the core runtime loads:

if (typeof window !== 'undefined' && APP.binding)
  window.__ENC_APP = { binding: APP.binding };

This is synchronous — it happens before the first render(). Adapters that need the binding (e.g., to set up routing tables) can read window.__ENC_APP.binding at load time.

window.__enc (test hook)

Exposed by appDomJs only, for test runners and debugging:

if (typeof window !== 'undefined') {
  window.__enc = { S: S, step: step, render: render };
}

The workflow replayer uses this to drive the app semantically — it sets scalars directly and calls step() without going through the DOM. This is how the same Lean proof can be executed as both a native_decide theorem and a replay corpus.

Browser history wiring

The web runtime hooks popstate to sync back/forward navigation with the in-app path scalar:

if (typeof window !== 'undefined') {
  // On first load, establish the initial state entry
  try { history.replaceState({encp: S.scalars.path}, ''); } catch(e) {}
  
  // On back/forward, update the path scalar and re-render
  window.addEventListener('popstate', function(ev) {
    if (ev.state && ev.state.encp != null) {
      S.scalars.path = ev.state.encp;
      render();
    }
  });
}

Every time step() changes the path, it pushes a history entry. Browser back/forward restores the old path and re-renders.

React Native differences

The core (appCoreJs) is byte-identical on web and native. The differences are in the platform bundle:

  • typeof-guarding: All window and history touches are typeof-guarded, so the core is inert on RN.
  • RN platform alias: In Hermes and older RN, window is an alias for global.
  • Renderer: appRnJs uses React state and RN components (View, TextInput, Pressable) instead of DOM elements.
  • SVG: elAttr elements use react-native-svg on both native and RN-web. SVG support is default-OFF on web (globalThis.__ENC_RN_SVG = 0) because react-native-svg's web build passes array-style props that react-dom rejects. The honest fallback is a sized placeholder.
  • Input behavior: TextInput uses defaultValue + onChangeText (not controlled), matching the DOM oninput semantics — scalars mutate without triggering re-render until step() calls it.

Recap

  • APP global: init (state), pages (routes), handlers (actions → effects), gates (guards), binding (metadata).
  • step(tag, payload): Synchronous dispatch — find handler, apply effects, re-render, push history.
  • ADAPTER seam: append() required; init() optional for hydration. Default is in-memory.
  • Gates run first: An unmet guard overrides the requested path before lookup.
  • window.__ENC_APP: Binding published synchronously at boot (adapter can read it immediately).
  • window.__enc: Test hook for replayers — direct state + dispatch access.
  • History wiring: Back/forward restores path scalar and re-renders (web only, typeof-guarded).
  • RN parity: Core is byte-identical; bundle differs; all window/history calls are typeof-guarded.

Next steps

  • Host bindings — how to declare the app's routing table and adapt it to a live backend.
  • The proof tier — what theorems hold about this runtime.
  • Workflows — how the same interpreter proves theorems and runs replay corpus.