Web Frontend

0. Scope

A frontend application is fully determined by:

AppView = (Enclave, @component specs, CSSApp)

The Enclave (from server.md) provides writes, reads, and protocol operations. The @component specs (from Lean) provide state, messages, update logic, and view structure. The CSSApp (from Theme.lean) provides theme and CSS rules.

Every React component, hook, handler, effect, and CSS rule follows from this structure. No creative decisions.

server.md    Enclave            → runtime.ts   writes + reads
client.md    Client             → runtime.ts   SDK calls via Cmd
enc.md       AppSDK W           → Cmd.lean     commit, fetch, navigate, toast
Lean specs  @component JSON     → gen_react.py state machine + JSX

The DSL consists of types organized in 4 groups:

Effects:     Cmd (none, fetch, commit, navigate, toast, subscribe, storeGet, storeSet,
             fetchJson, commitSigned, debounce, clipboard, focus, scrollToBottom, batch)
State:       StateField (name, type, init)
Messages:    MessageDef (name, payload?)
Update:      Case (guard?, state?, cmd)
View:        Element (tag, cls, attrs, on, children, if/then/else, map, ref, icon, expr, text, call)
Shared:      Icon, Helper, SharedElement (from Elements.lean)
Styling:     Var, Rule, MediaQuery, Animation, CSSApp (from CSS.lean)

I. Runtime

The only handwritten JavaScript: axioms/frontend/runtime.ts (214 lines).

// Cmd constructors (pure data, no side effects)
Cmd.none | Cmd.fetch | Cmd.commit | Cmd.navigate | Cmd.toast
    | Cmd.subscribe | Cmd.storeGet | Cmd.storeSet | Cmd.fetchJson
    | Cmd.commitSigned | Cmd.debounce | Cmd.clipboard | Cmd.focus
    | Cmd.scrollToBottom | Cmd.batch

// Runtime hook
useLeanComponent(component, ctx) → [state, dispatch]

// Effect executor
executeCmd(cmd, dispatch, ctx) → void  // pattern-match Cmd → browser effects

The runtime is the trust boundary. Everything above it (Lean specs, generated React, generated tests) is mechanically verifiable. Everything below it (browser APIs, network, DOM) is the execution environment.

II. Cmd Type

Defined in spec-lean/Enc/Frontend/Cmd.lean:

inductive Cmd (Msg : Type)
  | none
  | fetch (method : HttpMethod) (url : String) (body : Option String)
          (onOk : String → Msg) (onErr : String → Msg)
  | commit (commitType : String) (content : String) (tags : List (List String))
           (onOk : Msg) (onErr : String → Msg)
  | navigate (path : String)
  | toast (message : String) (level : String)
  | subscribe (eventType : String) (onMsg : String → Msg)
  | storeGet (key : String) (onResult : Option String → Msg)
  | storeSet (key : String) (value : String)
  | fetchJson (method : HttpMethod) (url : String) (body : Option String)
              (onOk : String → Msg) (onErr : String → Msg)
  | commitSigned (commitType : String) (content : String) (tags : List String)
                 (onOk : Msg) (onErr : String → Msg)
  | debounce (key : String) (delayMs : Nat) (msg : Msg)
  | clipboard (text : String)
  | focus (elementId : String)
  | scrollToBottom (elementId : String)
  | batch (cmds : List (Cmd Msg))

Update signature: State → Msg → State × Cmd Msg

This is the key insight: effects are data. The update function returns a Cmd description; the runtime executes it. Lean can reason about Cmds without touching the browser.

Cmd DSL (JSON)

Update cases return (state, cmd) where cmd is:

"cmd": "none"
"cmd": { "toast": ["message", "level"] }
"cmd": { "navigate": "/path" }
"cmd": { "commit": ["CommitType", "content", "tags", "OkMsg", "ErrMsg"] }
"cmd": { "fetch": ["url", "onOkExpr", "onErrExpr"] }
"cmd": { "batch": [cmd1, cmd2, ...] }
"cmd": { "storeGet": ["key", "LoadedMsg"] }

Guards:

"guard": "!state.text.trim()",
"guardCmd": { "toast": ["Enter text", "error"] },
"guardOver": "state.text.length > MAX",
"guardOverCmd": { "toast": ["`Exceeds ${MAX} chars`", "error"] }

III. @component DSL

Defined in spec-lean/Enc/Frontend/Component.lean:

Component = name + state + messages + update + view + subscriptions

Each component is a JSON block inside a Lean doc-comment:

/-! @component
{
  "name": "ComponentName",
  "app": "app-slug",
  "route": "/path/:param",

  "state": [
    { "name": "fieldName", "type": "TypeAnnotation", "init": "jsExpression" }
  ],

  "messages": [
    { "name": "MsgName", "payload": "Type" },
    { "name": "MsgWithoutPayload" }
  ],

  "consts": { "MAX_LENGTH": 280 },

  "update": {
    "MsgName": {
      "guard": "boolExpr",
      "guardCmd": { "toast": ["message", "level"] },
      "state": { "field": "newValueExpr" },
      "cmd": { "commit": ["Type", "content", "tags", "OkMsg", "ErrMsg"] }
    }
  },

  "initCmd": { "fetch": ["url", "onOk", "onErr"] },
  "subscriptions": [{ "event": "EventType", "msg": "handler" }],

  "view": { ... },

  "authRequired": true,
  "authFallback": { ... }
}
-/

IV. Element DSL

The view tree uses a JSON element representation:

Tags

{ "tag": "div", "cls": "class-name", "children": [...] }
{ "tag": "button", "cls": "btn", "on": { "click": "MsgName" }, "children": [...] }
{ "tag": "input", "attrs": { "type": "text", "value": "state.field" }, "on": { "input": "SetField(e.target.value)" } }

Conditional rendering

{ "if": "condition", "then": { ... }, "else": { ... } }

List rendering

{ "map": "state.items", "as": "item", "body": { ... } }

Dynamic classes

{ "tag": "span", "cls": "tab", "clsIf": ["state.active === 'x'", "active"] }

Text and expressions

{ "text": "Static text" }
{ "expr": "state.count > 0 ? state.count : ''" }

Icons and shared elements

{ "icon": "back" }
{ "ref": "spinner" }
{ "call": "identicon", "args": ["pubHex", 40] }

V. Shared Elements

Defined in spec-lean/Enc/Frontend/Elements.lean:

/-! @elements
{
  "icons": { "back": "<svg .../>", "heart": "<svg .../>" },
  "elements": {
    "spinner": { "tag": "div", "cls": "loading", "children": [...] },
    "pageHeader": { "params": ["title", "backHref"], "element": { ... } }
  },
  "helpers": {
    "timeAgo": "function timeAgo(ts) { ... }",
    "shortPub": "function shortPub(pub) { ... }"
  }
}
-/

• 6 icons: back, reply, heart, heartFilled, settings, search
• 7 elements: spinner, emptyState, pageHeader, pageHeaderWithTabs, identicon, composeInline, tweetCard
• 3 helpers: timeAgo, shortPub, escapeHtml

Inlined by gen_react.py into every component that references them.

VI. Styling

Defined in spec-lean/Enc/Frontend/CSS.lean (types) and spec-lean/Enc/Frontend/Theme.lean (rules):

/-! @css
{
  "name": "shared",
  "theme": { "--bg": "#000", "--text": "#e7e9ea", ... },
  "rules": { ".badge": "background: var(--accent); ...", ... }
}
-/

CSSApp = theme (variables) + base (reset) + rules (per-class)
       + media (responsive) + animations (keyframes)

Theme variables are shared across all 5 apps. Each app has its own stylesheet (axioms/frontend/apps/*/style.css) plus the generated supplement (ts/core/frontend/generated-supplement.css).

gen_css.py reads @css to generate generated-supplement.css and verifies 100% class coverage.

VII. Code Generation

@component (Lean) → gen_react.py → .tsx (React + useReducer)
@elements  (Lean) → gen_react.py → inlined in .tsx
@css       (Lean) → gen_css.py   → .css supplement
@component (Lean) → gen_tests.py → .test.js files

gen_react.py (351 lines)

1. parse_component_spec(lean_path) — extract @component JSON
2. load_element_library() — load @elements from Elements.lean
3. render_element(el) — Element JSON → JSX string
4. gen_component(spec) — full component → .tsx
5. render_cmd(cmd) — Cmd JSON → Cmd.xxx() call
6. main() — glob all Components/*.lean → generate .tsx files

For each component, generates: import statements, helper functions (from Elements.lean), constants, init state object, update function (switch on msg.type), React component with useReducer + queueMicrotask(executeCmd), auth guard with fallback view (if authRequired), JSX view tree.

gen_css.py (68 lines)

1. extract_react_classes() — scan generated .tsx for classNames
2. extract_css_classes() — scan existing + generated CSS
3. generate_supplement() — Theme.lean @css → CSS file
4. verify() — check 100% coverage

gen_tests.py (178 lines)

1. parse_spec(lean_path) — extract @component JSON
2. gen_update_fn(spec) — generate pure update function
3. gen_tests(spec) — generate test suite per component
4. main() — glob all Components/*.lean → generate .test.js

VIII. Component Inventory

Timeline: Feed, Compose, PostDetail, Profile, Search, Settings, Setup, Likes, TimelineView

DM: Inbox, Thread, Friends, Compose, Profile, Settings, Setup

Chat: GroupThread, GroupList, GroupInfo, Members, Compose, Profile, Settings, Setup

Messenger: ConversationList, DMThread, ChatThread, TimelineFeed, Profile, Search, Friends, ComposeChat, ComposeDM, GroupInfo, Members, Settings, Setup

Registry: RegisterIdentity, Nodes, NodeDetail, RegisterNode, IdentityDetail, EnclaveExplorer, ManifestWizard

IX. Verification

44 components × ~5 tests each = 236 auto-generated tests.

CSS class coverage: 107/107 non-wrapper classes = 100%

X. Type Inventory

XI. Files

XII. Correspondence

Lean Cmd.lean          ↔  runtime.ts Cmd constructors
Lean @component state  ↔  React useReducer init
Lean @component update ↔  React update function (pure)
Lean @component view   ↔  React JSX (gen_react.py)
Lean @elements         ↔  Inlined icons/helpers
Lean @css Theme.lean   ↔  generated-supplement.css
Lean ComponentProofs   ↔  gen_tests.py assertions