App DSL

Scope

An app.enc.json file is a minimal JSON declaration that a transpiler reads to derive all Lean spec blocks for a complete ENC application. Four top-level fields — data, ui, test, and encryption — define the event schema, RBAC rules, screen layout, and end-to-end test plan. The transpiler (gen_from_enc.py) produces Lean spec blocks that are byte-identical to the hand-written originals.

Here is the complete Chat application — 34 lines:

{
  "app": "Chat",
  "encryption": "mls",
  "color": "#10b981",

  "data": {
    "Message":  "Member CR",
    "Reaction": "Member C",
    "Profile":  "Member C",
    "Topic":    "Admin C",
    "Read":     "Member C",
    "Grant":    "Owner C -> Admin Member",
    "Revoke":   "Owner C -> Admin Member"
  },

  "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 creates group 'Bobs Group' with [bob]",
    "alice sends 'Hello everyone!' in 'Alices Group'",
    "bob sends 'Hey Alice! Bob here.' in 'Alices Group'",
    "charlie sends 'Charlie checking in!' in 'Alices Group'",
    "alice sends 'Welcome!' in 'Bobs Group'",
    "bob sends 'Thanks!' in 'Bobs Group'",
    "---",
    "alice sees 2 groups",
    "alice opens 'Alices Group' sees ['Hello everyone', 'Bob here', 'Charlie']",
    "alice sends 'From UI!' in 'Alices Group'",
    "alice opens 'Bobs Group' sees ['Welcome', 'Thanks']",
    "alice sends 'Also from UI!' in 'Bobs Group'",
    "alice opens groups sees 2 groups",
    "alice opens profile",
    "alice cycles [groups, compose, profile]"
  ]
}

From this single file, the pipeline derives the RBAC schema, role bitmasks, manifest constructor, content validators, frontend routes, mobile screens, service SDK, test contracts, and E2E test flows — across Lean, TypeScript, React, and React Native.

Top-level Fields

Optional fields include roles (explicit role list), endpoints (dev server ports), react (React vs vanilla DOM), and includes (composition from other apps).

Data Schema

The "data" field maps event type names to role shorthand strings. Each entry compiles to an RBAC schema rule with event type, role, and permitted operations.

Shorthand Format

// Basic: role + operations
"EventType": "Role Ops"

// With targets: for Grant/Revoke
"EventType": "Role Ops -> TargetRole1 TargetRole2"

Parsing Rules

Valid operations: C (Create), R (Read), U (Update), D (Delete), P (Push).

Special Event Names

Special Role Names

UI Definition

The "ui" array defines screens as pipe-delimited strings. Each line produces a route, a view file, a mount function, testIDs, and both web and mobile screen shells.

Grammar

route | [tab [default]] | elements

Element Types

Examples

// Tab with default list view
"groups    | tab default | list groups"

// Form with two fields and a submit action
"compose   | tab         | form group-name member-key -> create"

// Thread view (messages + send)
"group/:id |             | thread messages -> send Message"

// Search with toggle
"search    | tab         | form search | toggle [nodes, identities]"

// Detail with action buttons
"post/:id  |             | detail post comments | actions like comment"

// Settings (read-only display)
"settings  | tab         | show dataview-url"

Derived Names

From each screen key the transpiler auto-derives:

• View name — screen key kebab-cased ("groups" stays "groups", "group/:id" becomes "group")
• Mount function — "mount" + PascalCase ("mountGroups", "mountGroup")
• Nav label — title case of screen name (only for tab screens)
• TestIDs — from element names (list:groups, input:group-name, btn:create)

Test Definition

The "test" array contains natural language steps that compile into structured E2E test flows. A "---" separator divides SDK-level setup from UI-level validation.

"test": [
  // ── SDK setup (runs via SDK, no UI) ──
  "alice creates group 'Alices Group' with [bob, charlie]",
  "alice sends 'Hello everyone!' in 'Alices Group'",
  "bob sends 'Hey Alice!' in 'Alices Group'",
  "---",
  // ── UI validation (runs against rendered app) ──
  "alice sees 2 groups",
  "alice opens 'Alices Group' sees ['Hello everyone', 'Hey Alice']",
  "alice cycles [groups, compose, profile]"
]

Setup Patterns

Validation Patterns

Encryption Levels

The "encryption" field selects one of three levels, each adding cryptographic capabilities to the generated wallet, session, and middleware:

Derived Blocks

The transpiler generates six Lean spec blocks from each app.enc.json:

Pipeline

The JSON definition flows through a multi-stage pipeline, producing artifacts at each layer:

The amplification ratio is dramatic:

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.

All Apps

Five applications are defined with app.enc.json, spanning all three encryption levels: