`Encapp.Workflow`

A workflow is the same List (String × Payload) that reflRun already interprets, wrapped with a name and its post-conditions. That is what makes one definition serve as both a proof and a corpus entry.

`WStep`

inductive WStep where
  | fire  : String → Payload → WStep   -- click / nav → step(tag, payload)
  | input : String → Atom → WStep      -- typing → set a scalar
  | back  : WStep                      -- browser history back

def WStep.apply (hs : List RHandler) (d : Doc) : WStep → Doc
  | .fire tag p => reflStep hs tag p d
  | .input k v  => d.setScalar k v
  | .back       => d

back is identity in the proof — browser history is a runtime concern, not part of the Doc model — and is genuinely executed by the replayers. Assert its effect with a ui check.

`WCheck`

inductive WCheck where
  | scalarEq : String → Atom → WCheck
  | tableLen : String → Nat → WCheck
  | rowField : String → Nat → String → Atom → WCheck
  deriving DecidableEq, Inhabited

def WCheck.eval (d : Doc) : WCheck → Bool

Total and decidable, which is what lets the whole workflow reduce under native_decide. An out-of-range rowField index evaluates to false rather than failing.

`UICheck`

inductive UICheck where
  | seesText     : String → UICheck
  | namedControl : String → UICheck

Replay-only DOM assertions. Not part of the proof — the Doc model does not describe the rendered page. The replayers evaluate them against the live DOM.

`Workflow`

structure Workflow where
  name   : String
  users  : List String := ["alice"]
  steps  : List WStep
  checks : List WCheck := []
  ui     : List UICheck := []
  deriving Inhabited

The proof tier

def Workflow.run (app : ReflApp β) (w : Workflow) : Doc :=
  w.steps.foldl (WStep.apply app.handlers) app.init
 
def Workflow.holds (app : ReflApp β) (w : Workflow) : Bool :=
  w.checks.all (WCheck.eval (w.run app))

holds is a Bool, so:

theorem w_holds : w.holds app = true := by native_decide

The app logic is proven at build time. If a handler or the interpreter drifts, it fails to compile.

Aggregate over a corpus:

theorem corpus_all_hold : allWorkflows.all (·.holds app) = true := by native_decide
theorem corpus_single_user :
    allWorkflows.all (fun w => decide (w.users.length ≤ 1)) = true := by native_decide

corpus_single_user guards the emit: Workflow.toJson renders steps as a single user, so a two-user workflow would be silently misrepresented in the corpus. The theorem makes the boundary explicit.

The execution tier

def Workflow.toJson (w : Workflow) : String

Renders the runner-shaped JSON the replayers execute:

{ "name": "...", "users": ["alice"],
  "steps":  [ {"as":"alice","do":"fire","tag":"...","payload":...},
              {"as":"alice","do":"input","field":"...","value":...},
              {"as":"alice","do":"back"} ],
  "checks": [ {"kind":"scalar","key":"...","eq":...},
              {"kind":"tableLen","table":"...","eq":N},
              {"kind":"rowField","table":"...","i":N,"field":"...","eq":...} ],
  "ui":     [ {"kind":"seesText","text":"..."},
              {"kind":"namedControl","name":"..."} ] }

Supporting serializers: payloadJson, WStep.json, WCheck.json, UICheck.json.

Boundary

reflRun is single-Doc, so the proof tier is single-app-instance logic. Multi-user and cross-enclave workflows belong to the node layer; the emitted corpus carries users so a multi-client runner can project it, but the theorem is about one instance.

See Workflows and proofs for the guide, and Testing for the replayers and coverage gates.