`Encapp.Doc`

A counter's key → Int model is too thin for a real app. Doc is the general state: named scalar fields and named tables of rows, where every leaf is a typed Atom — no stringly-typed cells, so the whole thing stays decidable and provable.

`Atom`

inductive Atom where
  | str  : String → Atom
  | int  : Int → Atom
  | bool : Bool → Atom
  | null : Atom
  deriving DecidableEq, Inhabited

DecidableEq is what lets native_decide settle a workflow's post-conditions by computation.

`Row` and `Doc`

abbrev Row := List (String × Atom)
 
structure Doc where
  scalars : List (String × Atom)
  tables  : List (String × List Row)
  deriving DecidableEq, Inhabited

Association lists rather than maps: ordered, decidable, and small enough to reduce under native_decide. Row order is meaningful — appended rows stay in insertion order, which is what lets a workflow assert rowField "messages" 0 "body".

Accessors

Function	Behaviour
`Doc.getScalar d k`	reads scalar `k`, defaulting to `.null`
`Doc.setScalar d k v`	writes scalar `k`, inserting if absent
`Doc.rows d t`	reads table `t`, defaulting to `[]`
`Doc.appendRow d t r`	appends `r` to table `t`, creating the table if absent

Every accessor is total. There is no failure mode where a missing key throws — a missing scalar reads as .null and a missing table reads as empty, which keeps handlers total and therefore decidable.

Helpers

def short16 (s : String) : String := String.mk (s.data.take 16)

The short sender id used by the store convention — the first 16 characters of an identity.

@[inline] def asStr : Atom → String
  | .str s => s
  | _      => ""

Projects an Atom to its string, or "". This is the idiom for reading a scalar you know is textual:

match asStr (d.getScalar "path") with
| "/feed" => …

Working with `Doc`

Everything is a scalar, including routing. The current page is the path scalar. There is no separate routing mechanism to learn — see Routing and gates.

Tables are append-mostly. appendRow is the primary write; removal exists as an effect (removeWhereField) rather than as a Doc method, because removals are policy and belong in a handler where a workflow can prove them.

Prefer declared row-builders over hand-assembly. The appendFromScalars effect builds a row from constants plus named scalars, which keeps the row shape visible as data instead of buried in code.

JSON projection

Encapp/AppGen.lean provides the serializers the emitter and the compatibility diff use:

Function	Emits
`atomJson`	an `Atom` as JSON (strings escaped)
`rowObjJson`	a `Row` as a JSON object
`rowsArrJson`	a list of rows as a JSON array
`docInitJson`	a whole `Doc` as the emitted `init`

These are what make a Doc comparable against an external oracle — hellocheck prints hello's final state as JSON so compat/check.mjs can diff it byte-for-byte against the reference implementation.

Encapp.Doc

Atom

Row and Doc