Formal specification (Lean)

CVN's two load-bearing semantics are specified in Lean in impl-spec (spec-lean/Enc/Cvn/), as executable definitions with theorems checked by Lean's kernel, and the TypeScript is held to them by a conformance corpus the model itself emits.

What is proved

Enc.Cvn.Dispatch — the dispatcher:

theorem	says
`performNow_never_drops`	a Cmd is performed or refused — there is no third outcome
`refusal_names_kind`	a refusal names the kind it could not route
`run_records`	while recording, running an action appends exactly its emitted Cmds and performs nothing
`dispatch_performs_all_in_order`	outside a dispatch, every emitted Cmd — nested dispatches included — is performed exactly once, in emission order, after the action, and the recording closes
`nested_dispatch_drains_nothing`	a nested dispatch appends to the outer list and drains nothing
`perform_outside_is_immediate`	outside any dispatch, `perform` performs now
`dispatch_performs_exactly_emitted`	nothing invented, nothing lost

Enc.Cvn.Ladder — the epoch ladder (shared/kernel/dm-epoch.ts):

theorem	says
`replay_is_idempotent`	identical bytes at a held epoch: silent, unchanged
`conflict_is_refused`	different bytes at a held epoch: refused
`refused_leaves_ladder`	a refusal never changes the ladder
`opens_at_zero`	an empty ladder accepts exactly epoch 0
`accepted_is_above_max`	acceptance is strictly monotone
`accepted_is_held`	what was accepted is held afterwards, with the bytes given

How the code is held to it

The DSL that impl-spec compiles to TypeScript is first-order (bytes, maps, scalars, crypto); a dispatcher with callbacks is not expressible in it, so the TypeScript stays hand-written and is refined by replay, the same way the wire protocol is held to enc-oracle:

lake exe cvn-oracle (in impl-spec/spec-lean) runs the Lean definitions over a fixed corpus and writes spec/cvn-conformance.jsonl into this repo — one JSON line per case with the model's expected outcome.
test/spec-conformance.test.mjs replays every dispatch case through createDispatcher; impl-super-mvp's ladder-conformance.test.mjs replays every ladder case through dmEpochSet.
spec/codegen-manifest.json pins the corpus by SHA-256; test/manifest.test.mjs refuses a mismatch — a model change that was not re-generated, or a corpus edited by hand.

What this proves: the implementation agrees with the model on every case the model enumerates. What it does not: that the corpus covers every path — a new behaviour gets a new case in Enc/Cvn/Oracle.lean, and a new theorem when it is a property rather than an example.

Regenerating

cd ../impl-spec/spec-lean
lake build Enc.Cvn.Dispatch Enc.Cvn.Ladder   # the proofs
lake exe cvn-oracle                            # the corpus → ../impl-cvn/spec/

then update expectedDigest in spec/codegen-manifest.json to the new SHA-256 and commit both repos. Enc.Cvn is part of EncProofs, the framework-free public verification surface, so a public clone re-checks these theorems with the codegen framework absent.