Host bindings

An Encapp app cannot perform I/O. Something outside it must: talk to a network, hold keys, persist state. That something is the host, and the binding is how an app declares what it expects the host to do.

The typeclass

class HostBinding (β : Type) where
  toJson : β → String
 
instance : HostBinding Unit where
  toJson _ := "null"

That is the whole interface. Encapp knows a binding can be serialized and nothing else.

ReflApp is parametric in the binding type:

structure ReflApp (β : Type) where
  …
  binding : Option β := none

so ReflApp Unit is a pure view app with no host expectations, and an app with a real protocol declares its own binding type and its own HostBinding instance. Anything protocol-shaped — SDK package names, enclaves, plugins, tables, events — is defined by the layer above Encapp and passed in as β.

The dependency arrow therefore points one way: apps and generators may depend on Encapp; Encapp never depends on a protocol.

Why it exists

The seam used to be an ambient, untyped global: window.ENC_ADAPTER. Nothing declared what a deployment owed the app. A hand-written protocol implementation could fill that hole and pass every UI check, every differ and every render test — because none of those can see the wire.

The lesson, stated as a rule:

An untyped extension point is an invitation to hand-write protocol. A typed, declared one is not.

What a real binding looks like

The flagship app declares its SDK and its store seams as data. Sketched:

structure SdkBinding where
  package    : String
  cls        : String
  submits    : List (String × String)      -- table → SDK method
  queries    : List (String × String)      -- table → SDK query
  deletes    : List OpBinding              -- op-dispatch → wire delete
  moves      : List MoveBinding            -- membership transitions
  provisions : List ProvisionBinding       -- "mint a dedicated enclave for this row"
  peerSends  : List PeerSendBinding        -- which rails an outbound invite travels
  rowSubmits : List RowSubmitBinding       -- a SHAPED submit built from row + identity
  peerRecvs  : List PeerRecvBinding        -- which rails this client listens on
 
instance : HostBinding SdkBinding where
  toJson b := "{\"package\":\"" ++ b.package ++ "\", … }"

and the app declares instances of those forms:

deletes := [{ table := "message_ops", op := "delete", idField := "id" }]
 
moves   := [{ table := "group_ops", whenField := "op", whenValue := "leave",
              fromRole := "MEMBER", toRole := "OUTSIDER",
              subject := "self", scope := "row" }]

The emitted artifact carries the serialized binding, and the host reads it at runtime:

const rule = deleteRuleFor(table)          // read the DECLARATION
if (rule && row.op === rule.op) {
  wireDelete(row[rule.idField])            // execute it
}

The split: policy is app data, mechanics are host code

The line that has held up in practice:

Ask: "would a reviewer reading only the Lean app be surprised by this?" If yes, it is policy and belongs in the declaration.

The failure mode this creates — decorative declarations

Moving policy into the binding is only worth something if the host then obeys the declaration. It is entirely possible — and has happened — to declare a rule that no host code reads. The app looks declarative, the ledger cites the declaration as evidence, and deleting the declaration changes nothing.

Three real instances found in one audit of the flagship app:

• a declared membership transition whose branch still spelled out its own trigger and event name;
• a scope field the host never read, while documentation argued at length that the distinction mattered;
• a kind field naming what to provision, while the host passed a literal.

"The app declares X" and "the host obeys the declaration of X" are different claims, and only the second is worth anything.

Test declarations by deletion, not by grep

A grep for a declaration's presence cannot tell those two claims apart. The only reliable test is the deletion test:

1. delete or flip the declaration in the Lean app;
2. rebuild;
3. a test that depends on that behaviour must go red.

If nothing goes red, the declaration is a comment.

A cheap mechanical net helps between deletion tests: walk the emitted binding and fail on any declared field with no reader in the host source. It is sound for absence — a field never accessed is certainly decoration — but it can be fooled by an unrelated access of the same name, so it complements the deletion test rather than replacing it.

Designing a new binding form

1. Name the trigger and the parameters, not the mechanism. whenField/whenValue plus the transition, not "call this function".
2. Keep crypto and I/O on the host side. Declare which rails an invite travels; let the host decide how to seal each payload.
3. Key branches off the declared meaning, not the table name. A guard on to == "OUTSIDER" survives a table rename and reads as what it is — a removal. A guard on the table name hides that.
4. Write the red-proof before the migration. Decide in advance which test goes red when the declaration is deleted. If you cannot name one, you are not ready to declare it.
5. Emit it, then read it back. Parse the binding out of the built artifact — with a brace-matching parser, not a regex; a nested array will truncate a regex capture and the failure will point nowhere near the cause.

Testing against the real binding

Any test that exercises host behaviour driven by the declaration must load the emitted binding, not a hand-written stub. A stub is a fiction: the app can declare one thing and the test assert another, and nothing notices. This is not hypothetical — a sweep to remove fabricated binding stubs from a test suite took three rounds, and each additional round was found by writing the refuting command rather than by reading the code.

For the concrete contract a deployment implements — window.ENC_ADAPTER, the hydration seam, and the failure that makes a broken integration look green — see ENC protocol integration.

Recap

• A binding is a typed data structure that declares what an app expects from its host; it prevents hand-written protocol from hiding inside untyped seams
• The binding is the place for policy (which table, which transition, which rails); keep mechanics (crypto, I/O, signing) on the host side
• Decorative declarations happen when policy is declared but the host never reads it; three real instances were found in a single audit
• The deletion test is the reliable way to verify a declaration is obeyed: delete or flip it, rebuild, and a dependent test must go red
• When designing a new binding form, name the trigger and parameters, not the mechanism; emit it and read it back with a brace-matching parser, not regex

Next steps

• ENC protocol integration — the concrete window.ENC_ADAPTER contract and real-world integration failures
• Testing an integrated app — how to test declarations without fabricated stubs
• Testing and coverage gates — the four verification tiers