@enc-protocol/cvn/enc — ENC, but no app

Two layers sit on CVN in an ENC application, and the line between them is drawn by evidence, not prediction:

• The app's kernel — shared/kernel/families/<family>.ts in impl-super-mvp: Super's verbs as stated decision functions with written invariants. #invitemember mentions rosters, DM epochs and moments; it is Super, and it stays Super.
• cvn/enc — the residue each family surfaces that mentions only enclaves, events, nodes and DataViews. Every ENC client applies these rules; none of them may import an application. A module lands here only when a family in a real app travels it (peerEnclave — declared, green, never travelled — is the failure this order prevents), and it comes with its own tests and, when it is protocol, a Lean oracle case.

Modules

| dm-wire | what a DM write puts on the wire, apart from the crypto: the ratchet envelope {epoch, sender_seq, ciphertext: base64(nonce ‖ ct), ecdh_pub}; a message's tags — to first, one epoch tag per wrap, from_enclave last and only for a real id; the recipients of an epoch wrap (the peer, and its differing sub key); the epoch-0 field of a first Move (the owner wrap, the rest as alternates); the r-tagged Delete and Update | Enc/Cvn/DmWire.lean — messageTags_head, messageTags_length_*, messageTags_bad_enclave, epochRecipients_*, epochZero_*, referenceTags_one; 11 oracle cases | | dataview | a DataView subscription, on both ends of the socket. The server: a filter's table and column names are identifiers (they go into SQL quoted, and this is why quoting is enough) and its values are lowercased; a Query with a sub_id replaces the sub of that id, replays at most 200 rows as Events, then EOSE; a Close answers Closed; anything else, and a frame that does not parse, is a Notice; at most 32 subs per socket; a write reaches every sub on its table whose filter matches — and a delete reaches every sub on the table, because a delete row carries only its id. The client: a frame folds into the rows by id (newest first, capped; a delete removes; no id, no change), and the wanted set's diff is start = want \ have, stop = have \ want | Enc/Cvn/DataView.lean — normalizeFilter_ident, query_ends_with_eose, query_replaces, step_le_maxSubs, close_removes, broadcast_only_matching, broadcast_delete_all, broadcast_other_table, upsert_present, upsert_unique_id, upsert_length_le_cap, diffKeys_disjoint; 39 oracle cases, replayed by test/enc-dataview.test.mjs here and by impl-super-mvp's dataview-conformance.test.mjs through the real server module and kernel | | invite-notice | the group invite notice an admin seals into the invitee's Personal enclave, refining Enclaves.Personal: the four required keys, topic and manifest_hash only when they carry something; the handoff and its epoch_n together or not at all and never for epoch 0 (the mint secret seals the pre-invite history); the highest committed epoch is what travels; group_invite retried on a fixed short cadence, the rest once; a notice only for an admit, to a full pubkey, naming the caller's enclave over the bound one | Enc/Cvn/InviteNotice.lean — toSealed_valid (refines handoffRequiresEpochN), withHandoff_pairs, select_never_zero, select_is_max, preflight_target_len, preflight_override; 19 oracle cases, replayed through the real kernel module | | identity | how an account is made findable, refining Registry.RegIdentityContent: the payload's unconditional fields and the ones absent rather than empty, enclaves last; the snapshot that sees every field; the DataView push BEFORE the enclave commit, committed-but-unpushed neither published nor stamped; the profile commit's mirrors; the lookup key's verdict (8–63 hex partial, 64 exact); the registry row keyed on content.id_pub else from, display_name else name, served as the raw payload with the columns laid over it | Enc/Cvn/Identity.lean — snapshot_sees_change, push_before_commit, unpushed_not_stamped, stamped_iff_published, verdict_exact_iff, inflate_column_wins, row_name_fallback; 24 oracle cases, replayed through the real publisher, families and registry DO | | submit | a submit command, its receipt and the row waiting on it, refining NodeAPI's commit and receipt: the Cmd's validity (an event, a known target by a lowercase 64-hex key, pair tags); the reply's verdict (refused when missing, ok:false or error, one place deciding what a receipt means); the outcome on the optimistic row (a receipt stamps the OLDEST waiting row's id, never its time; a refusal drops the oldest, except sent and message, whose rows the WS echo confirms); the optimistic search; the outbox (retryable only, idempotent by id, due in order, eight attempts is the end); the per-enclave send seq | Enc/Cvn/Submit.lean — valid_tags_pairs, verdict_error_names, outcome_refusal_keeps_sent, find_matches, enqueue_length, due_sublist, expired_attempts, nextSendSeq_*; 31 oracle cases, replayed through the real kernel modules | | query | asking an enclave for its events, beside Handlers.QueryFilter: the client's filter (reverse defaults to newest first, limit to 100, '*' is no type), the subscribe filter (the gap after the cursor, else the newest 1000), what a conforming node returns (deleted excluded, type and sender matched, the cursor strictly after, ordered by seq, at most min(limit ∥ 100, 1000)), the {event, status} unwrap | Enc/Cvn/Query.lean — length_le_1000, sorted_when_reverse, no_deleted, after_cursor, unwrap_typed; 13 oracle cases, the node's half replayed end to end through the real adapter and the real node | | group-wire | what a group membership change puts on the wire, refining Enclaves.Group: the admit and kick grammar over the spec's parseMoveType (a space tolerated; wider than adminMoveCarriesEpoch, stated); who gets the new epoch — the target on an admit, everyone but the target on a kick, the sender always, malformed pubs dropped before the wrap; the epoch a commit follows (the highest recorded or held, floor 0: the mint); the Move's content — the spec's nested epoch with members, three flat mirrors for the rollout, wraps only when non-empty; readmission (an unknown leave time means no) | Enc/Cvn/GroupWire.lean — admit_includes_target, kick_excludes_target, self_included, recipients_wellformed, first_commit_is_one, layout_mirrors, admit_wider_than_spec; 24 oracle cases, replayed through the real roster, readmission and enrichWelcome | | rbac-wire | the manifest as it goes to the node — the object Manifest.lean does not model: {enc_v, nonce, RBAC{use_temp, schema, states, traits, initial_state}} from the authoring manifest; the schema rows in order (customs, lifecycle, moves, slots, grants operator × trait with ops C, readers, the dataview fallback); the owner and the sub-key co-owner under every init state but OUTSIDER and every init trait; the DataView pre-registered; what the flattening DROPS (alias, gate, preserve, scope, retention, transfers), stated as theorems because it is what makes gates and ownership transfer unreachable on this wire | Enc/Cvn/RbacWire.lean — schema_starts_with_customs, grant_rows_are_C, dataview_fallback, move_extras_dropped, transfers_dropped, no_outsider_key, owner_first; 6 oracle cases, the shell and the protocol tier through one source | | push | a row pushed at a DataView, on all three sides, beside Enc.Core.Push: the client's POST <dv>/push with {events} and its attempt loop (one at least, stopping at the first success or when the schedule says stop); the node's payload AS SHIPPED — flat push, one notify per event, a wire message with no type, a backoff of 1000·2ⁿ uncapped and exhausted at ten; the receiver's insert plan — a Delete with an r tag is a tombstone, Shared(k) upserts by the sender, reg_* by its key, the rest append, _tags a JSON string in SQL and an array on the wire | Enc/Cvn/Push.lean — attempts_bounded, attempts_stop_at_success, payload_splits_modes, wire_agrees_but_type, backoff_uncapped_diverges, shared_upserts_by_from, registry_upserts_by_key, row_carries_from, tags_default_empty; 31 oracle cases, replayed through the real client module, the node's generated pipeline and the real DataView DO over the in-process shim | | signaling | the ephemeral relay Homes.lean assigns to the host, stated anyway: the client's rooms (the two shorts sorted, inbox:<short>), the seven call subs and hangup-versus-cancel; the relay's step — a pub of 8–16 lowercase hex or refused, echoes to every OTHER member with from stamped, presence on watch and on every transition, read cursors persisted forward and within a minute of now and broadcast either way, read_state on query and on join, unknown frames dropped | Enc/Cvn/Signaling.lean — bad_pub_refused, echo_never_to_sender, echo_carries_from, watch_replies_now, presence_on_transition_only, read_monotonic, read_future_not_persisted, join_silent_without_cursors, hangup_outgoing_is_cancel; 10 oracle cases (three of them frame sequences), replayed through the real SignalHub over a socket pair with a mocked clock | Crypto primitives are injected (InclusionPrims): the rule is pure, the host owns the hashing and the signature checks, and the same verdict runs on node, web and native without a platform import.

Two things Super's wire carries that RatchetPair.lean does not are stated in dm-wire.ts's header with the spec's own rule, rather than smoothed over. The message content carries a fourth field, ecdh_pub, because Super sends an epoch-less first message (the key derived by ECDH with the peer when no remote epoch is known), a step the spec has no counterpart for; the spec pins the message content to three fields by theorem and declares a wire-layout change a new plugin, so the field is the app's until a plugin version names it. And from_enclave on messages is the Zooid SDK's tag (dm-nip44, tested there), beside the spec's enclave_id on invites. Neither side was edited on a guess: the divergence is named where it is built.

dataview is the one module with a server half. Super's server module (sdk/dataview/_shared/subscriptions.js) is a Worker module that imports nothing, so it does not call this one; it is held to the same corpus instead, replayed through a socket whose attachment and sends are recorded. The kernel's fold and diff (dataview-rows.ts, subscriptions.ts) call foldRows and diffKeys here, with the app's own row readers injected — a public row's id is its event id, else its moment id, else its rowid.

What is stated, and what is only named

Eleven modules are here because a family in a real app travelled them, and each is pinned by a Lean model whose cases the real code replays. The port plan's residue column is closed: every residue the plan-6 table named is stated, and impl-super-mvp's measure reads that (RESIDUE in clean/test-port-complete.mjs: a Lean file, a corpus kind, a module here, a replay through the real code, per row). Formal spec keeps the table. Until a shape is stated here it is app code held by the family's own tests, which is honest and is not the same thing.

The rhythm that grows this layer

1. Pick a verb family in the app. Write its invariants as sentences a test can refute.
2. Redesign it as a decision function. While doing that, ask of each part: does it mention the app's nouns, or only enclaves, events, nodes, DataViews?
3. The protocol-only parts move here, with tests and a Lean case; the app's parts stay in the app's family module and import from here.
4. Gate, commit, next family.
5. When a family adds a feature, its residue is stated the same day: Lean shape, oracle cases as wire frames, a replay through the real module. The measure requires every module here to be called from the app's kernel and to have its own test; a module declared and never travelled is what the order above prevents.

impl-super-mvp/CVM-PORT-6.md is the plan for Super's sixteen families and the code-derived measure its loop halts on. For a native host, the family modules and this layer are exactly what to adopt: the app's kernel plus cvn/enc are the code shared across hosts; the host implements HostPorts and the app's declared ports, nothing else.

What Super's families are, after the port

impl-super-mvp is through: sixteen family modules under shared/kernel/families/, each with INVARIANTS (sentences a test refutes), a RUN_ACTION_TOKENS ceiling the measure holds it to, a family-<F>.test.mjs that runs the family against a fake host recording order, and — for the families that moved decisions out of the interpreter — a family-<F>.projections.test.mjs. run-action.ts is under 100 code lines (the measure refuses more): the pre-action gate call (shared/kernel/pre-action-gate.ts), the apply, one context built by buildFamilyCtx (families/_ctx.ts) from ActionPorts (shared/kernel/action-ports.ts) and the click, and one dispatch line per family. The expression READING the runner used to carry as closures — the live chain, the calls, the two token resolvers, the pair rule — is the framework's, core/action in @enc-protocol/cvn, pinned by Enc/Cvn/ClickPath.lean (26 theorems; one of them, that quotes do not nest, corrected an expectation its author held) and the corpus kind click-path (69 cases, replayed by the framework's test and, through the context builder, by the app's). interpret-action.ts is gone; its shapes are families/_shared.ts.

families/_ctx.ts — FamilyCtx — is what a family's run receives: the runner's _read, _commit, notify, the host's liveness and timer, and the ports a family may call. A family reaches nothing past it, so what a host must supply for a family is that type, not a reading of the runner.

Two of the four families with no region of their own in the runner (open, subscriptions) are fronts over kernel modules; two (invite, calls) hold decisions other families call. The measure treats a family without a runner region as done when another family or kernel module travels it — the plan's step 4 presupposes a region, and a measure that demanded a vacuous import would have been satisfied by a lie.