Spec and Codegen (the counter path)

The abstract App has function fields and cannot be serialized or codegen'd directly. Spec is its defunctionalized image: the model becomes a key→Int store, messages are tags (strings), and update is a finite handler table — all data. This dataful representation is the bridge between proof and emission.

The algebra layer: `Op`, `Handler`, `Spec`

The minimal serializable update primitive is Op — three cases:

inductive Op where
  | incr
  | decr
  | setTo : Int → Op

Op.apply evaluates an op against a field value:

def Op.apply : Op → Int → Int
  | .incr,    n => n + 1
  | .decr,    n => n - 1
  | .setTo v, _ => v

A Handler pairs a message tag (a string) with the operation to apply:

structure Handler where
  tag   : String    -- message identifier (e.g., "inc")
  field : String    -- which field to mutate
  op    : Op        -- which operation

A Spec is the complete reflected app: initial state, UI tree, and handler table:

structure Spec where
  init   : List (String × Int)  -- initial field values
  view   : Ui String            -- the UI, with string tags
  update : List Handler         -- the message handlers

The Counter example shows this concretely:

def counter : Spec where
  init   := [("count", 0)]
  view   := .col [ .button "-" "dec", .bind "count", .button "+" "inc" ]
  update := [ ⟨"inc", "count", .incr⟩, ⟨"dec", "count", .decr⟩ ]

Store operations: `specGet` and `specSet`

The model is a List (String × Int) association list. Two helpers manage it:

def specGet (m : List (String × Int)) (k : String) : Int := 
  (m.lookup k).getD 0
 
def specSet (m : List (String × Int)) (k : String) (v : Int) : List (String × Int) :=
  if m.any (fun p => p.1 == k) then
    m.map (fun p => if p.1 == k then (k, v) else p)
  else m ++ [(k, v)]

specGet reads a field, defaulting to 0 if absent. specSet writes a field, inserting if absent, updating if present.

The update denotation: `Spec.step`

Spec.step is the operational semantics — it folds one message tag into the store:

def Spec.step (s : Spec) (msg : String) (m : List (String × Int)) : List (String × Int) :=
  match s.update.find? (fun h => h.tag == msg) with
  | some h => specSet m h.field (Op.apply h.op (specGet m h.field))
  | none   => m

It looks up the handler by tag, and if found, applies the op to the named field. Unknown messages are no-ops.

The proof guarantee: `Spec.toApp`

The whole point of Spec is that it typechecks as a lawful abstract App:

def Spec.toApp (s : Spec) : App (List (String × Int)) String where
  init       := s.init
  update msg m := (s.step msg m, [])
  view _     := .text ""

This is not a runtime interpretation or a generated stub. The typechecker verifies that Spec is an App. That typecheck is the guarantee: a Spec is a command-free (pure) instance of TEA, so every generic theorem proven for App — reload equivalence, message-log append law — holds for it without new proof.

Code emission: `Codegen.emit`

The codegen pipeline is three steps: JSON serialization, JS runtime generation, and HTML wrapping.

Step 1: Serialize the Spec to JSON. Spec.toJson encodes the entire spec:

def Spec.toJson (s : Spec) : String :=
  "{\"init\":" ++ specModelJson s.init
    ++ ",\"view\":" ++ uiToJson s.view
    ++ ",\"update\":[" ++ String.intercalate "," (s.update.map Handler.toJson) ++ "]}"

Step 2: Emit the runtime. runtimeJs is the JS mirror of Spec.step plus DOM rendering:

def runtimeJs : String := String.intercalate "\n" [
  "let model = Object.assign({}, APP.init);",
  "function step(msg){",
  "  var h = APP.update.find(function(x){ return x.tag === msg; });",
  "  if(h){ var cur = model[h.field] || 0;",
  "    model[h.field] = h.op==='incr' ? cur+1 : h.op==='decr' ? cur-1 : h.n;",
  "    render(); }",
  "}",
  /* ... DOM rendering functions ... */
]

Step 3: Wrap in HTML. Codegen.emit generates a complete, self-contained SPA:

def Codegen.emit (s : Spec) : String := String.intercalate "\n" [
  "<!doctype html>",
  "<html><head>…</head><body>",
  "<div id='app'></div>",
  "<script>",
  "const APP = " ++ s.toJson ++ ";",
  runtimeJs,
  "</script>",
  "</body></html>" ]

The output is one file with no dependencies, no build step, no framework.

Scope and boundaries

What is proven: Spec.toApp typechecks, so the Lean Spec.step semantics are lawful TEA. Every theorem about App (reload, log append) is inherited.

What is checked, not proven: The JS runtime is not proven to equal the Lean interpreter. What exists instead is empirical: the same corpus replays on multiple runtimes (happy-dom, headless Chromium, React-Native-web) and the algebraic post-conditions are re-asserted there. See What is proven for the full refinement picture.

What is out of scope: The Workflow DSL is designed for ReflApp + Doc apps (like the hello example). Spec apps (like Counter) use a different state model and are not portable to the workflow framework without a rewrite. The full pipeline with effects, bindings, and multiuser is ReflApp + AppGen — a separate codegen path not covered here.

Recap

Op — three serializable update primitives: increment, decrement, set-to-value.
Handler — binds a message tag to an op and a field name.
Spec — the reflected app: initial state, UI tree, and handler table.
Spec.step — the update denotation; folds a message into the store.
Spec.toApp — typechecks as a lawful App, inheriting all App theorems.
Codegen.emit — serializes to JSON, wraps in a generic JS runtime, outputs a complete SPA.

Next steps

The Counter example — see both the proven Spec and the typed-message App Int CMsg form.
What is proven — understand the refinement boundary and what the JS runtime fidelity claim covers.
Host bindings — move from pure data apps to store-backed apps with effects.

Spec and Codegen (the counter path)

The algebra layer: Op, Handler, Spec

Store operations: specGet and specSet

The update denotation: Spec.step

The proof guarantee: Spec.toApp

Code emission: Codegen.emit