Are you an LLM? Read llms.txt for a summary of the docs, or llms-full.txt for the full context.
Skip to content

Porting an app onto CVN

The port CVN came from moved a 7,400-line application runtime into this shape without a rewrite. The order below is the order the obstacles fell; each step was blocked by the previous one.

0. Publish the measure

Add a declaration to the runtime: owned, delegated, hostCapabilities. Make delegated a list the code produces, and make the loop that drives the port read that list — not a plan file. Twice the port "finished" because every box was ticked while the work behind one was half done.

1. Move decisions, one verb family at a time

For each action family, extract the decision — expression in, patch or Cmd out — into a pure kernel module. Leave effect execution where it is. Measure inline state rebinds inside the action body; they fall from dozens to one.

2. Stop reading and assigning the host's state

A function that assigns to a variable it does not own cannot move to another module. Replace every state = … with cell.commit / cell.replace, every read with cell.value. Count the sites from the function body, not the file — the plan's "≈430 reads" was a whole-file count; the body had 78.

3. Move the body; inject what it imports

The action body becomes a kernel module taking an ActionPorts object. Anything it imported from the host tree that node cannot load (a directory import, a DOM-only module) becomes an injected port. Declare the interface; the contract gate keeps it honest.

4. Let the kernel build the dispatch

createRuntime builds the runner inside the dispatcher, with _perform bound to it. No fallback to a host action: a fallback is how a method is counted as owned while something else still does the work.

5. Shrink the port surface by disposition, not by count

Each remaining port has a written reason: platform, host data, session state, blocked on another move. Trade behaviour ports for data ports. Refuse repackaging.

6. State the protocol residue in Lean; replay it through the real code

Each family, once a decision function, surfaces a residue that mentions only enclaves, events, nodes and DataViews. That residue is ENC's, not the app's, and it is stated three times over: a Lean model with theorems (impl-spec/spec-lean/Enc/Cvn/), oracle cases the model emits as wire frames, and a replay — through the reference in cvn/enc and through the real module the app ships (a server module that imports nothing is held to the corpus with a recorded socket, not rewired). The corpus digest is pinned in both codegen manifests.

And then model the app's own decisions too. This step was written when they were held to be sentences a test refutes rather than theorems — the reasoning being that they name the app's nouns, and Lean would prove the app rather than the protocol. The line moved: which enclave a write names, which cipher seals it, what a receipt does to the row it was for are exactly what a model is good at, and the payoff is not proof for its own sake but the corpus — a decision with a model has cases, and cases replay through the shipping module. See the Formal spec for all thirteen.

The traps, so they are not re-derived

  • let state = getState() in an async function is a stale snapshot after the first await.
  • A kernel module that imports a host-tree module with a directory import is one node cannot load.
  • A port the kernel declares and never travels stays wrong forever.
  • A rt: any ports bag hides a missing port until a branch throws inside a catch.
  • The runner must use the dispatcher's perform, or the dispatcher records nothing.
  • Suite "contention" is an app loop until a profile of the page says otherwise.
  • A corpus replayed only through a copy proves the copy. Replay the module the app ships.
  • A plan's residue column is a list of unstated shapes until the measure reads it.
  • A decision that needs a host capability goes ON the Cmd as a plan; asking and then sending is two resolutions of the same thing, and they come apart.
  • A guard that asks a port whether a write will work is the performer's named refusal, deleted.
  • A gate that asserts a floor on a number the work reduces fails on success.
  • A port survey that reads only the entry point stops counting what a refactor moves out of it.