Module map

The framework is 2,163 lines of Lean across 14 modules, plus three examples (309 lines) — 2,472 lines in all. Encapp.lean is the umbrella import.

Authoring

Module	Lines	Owns
`Encapp/Core.lean`	57	abstract TEA — `App Model Msg`, `Cmd`, `Event`, `ofMsgLog_append`
`Encapp/Doc.lean`	56	the state model — `Atom`, `Row`, `Doc`, accessors, `short16`
`Encapp/View.lean`	50	the typed view vocabulary, `View Msg`
`Encapp/Ui.lean`	26	the minimal view vocabulary used by the `Spec` path
`Encapp/ViewDsl.lean`	36	app-agnostic authoring sugar over `RView`

Semantics and proof

Module	Lines	Owns
`Encapp/Store.lean`	89	`World`, `Refines`, `refines_sound`, `refines_log`
`Encapp/Adapter.lean`	60	`reversedWorld` — a non-trivial refinement witness
`Encapp/Replay.lean`	42	`applyEv`, `applyEv_idem`, `replayLog_append`
`Encapp/Bridge.lean`	94	the interpreter as a `Foundation.World`; the UI-over-store `Layer` lift

Codegen

Module	Lines	Owns
`Encapp/AppGen.lean`	1,060	`ReflApp`, `Eff`, `RView`, `RHandler`, `HostBinding`, `reflStep`, `appCoreJs`/`appDomJs`/`appRnJs`, all emitters
`Encapp/EmuGen.lean`	310	the ENC emulator authored as `RView` data — the largest worked example of UI-as-data
`Encapp/Codegen.lean`	93	the minimal `Spec` → SPA path used by the counter
`Encapp/Spec.lean`	71	the reflected counter model — `Op`, `Handler`, `Spec`, `Spec.toApp`

Verification

Module	Lines	Owns
`Encapp/Workflow.lean`	119	`WStep`, `WCheck`, `UICheck`, `Workflow`, `holds`, `toJson`

Examples

Module	Lines	What it demonstrates
`Encapp/Examples/Counter.lean`	65	the smallest complete app, both faces (`Spec` and `App Int CMsg`), three theorems — and the only non-messaging example
`Encapp/Examples/Hello.lean`	177	a real app: routing, identity, composer, two tables, reflection, and the typed↔reflected theorem
`Encapp/Examples/HelloWorkflow.lean`	67	three workflows covering all three routes, each `native_decide`-proven, plus the aggregate corpus

Entry points

File	Executable	Emits
`HelloApp.lean`	`helloapp`	the hello app for web, native and desktop
`EmuGenMain.lean`	`emulator`	the ENC emulator
`Main.lean`	`encapp`	the counter through `Codegen.emit`
`HelloCheck.lean`	`hellocheck`	hello's final state as JSON, for the compatibility diff

Dependencies

lakefile.lean requires exactly one package:

require «foundation» from ".." / "impl-foundation"

Foundation.Layer.mono is the keystone Bridge.lean uses to lift a store refinement through a UI layer. The axiom audit pins it to exactly zero axioms.

Encapp depends on no protocol, SDK or network library.

Reading order

For the framework itself: Core → Doc → View → AppGen (the interpreter half) → Workflow → Store → Bridge.

For building an app: Getting started → The app model → Effects → Workflows.