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

CodeGen

CodeGen is the ENC instance's emit layer: it turns the protocol's checked Lean spec into every implementation that ships — byte-deterministically, with each artifact's hash pinned. The software you run is provably the design that was verified, because it was generated from it rather than written against it.

How it works

  1. One source. The canonical form is Enc.DSL — a protocol DSL induced from prose, Lean definitions, implementation observations, and witness failures by SpecGen. Humans never hand-author it.

  2. Fan-out emit. From that Lean, CodeGen emits multiple targets:

    TargetWhat it is
    Lean referencethe executable referee — the spec that runs
    JS core / client / dataview SDK@enc-protocol/{core, client, dataview}
    JS nodethe pure-JS node implementation
    Rust / WASM kernelthe enc-core.wasm kernel + Rust host
    Cloudflare Workerthe production Worker source

  3. Byte-determinism. Re-running the emit produces zero diff; a codegen manifest pins each artifact's sha256. Today the manifest tracks 55 generated artifacts (47 protocol / 7 platform / 1 operational).

  4. Idempotence gate. Any drift between the committed artifact and a fresh emit fails CI — handwritten protocol residue is a release problem unless it is explicitly classified and accepted.

What makes it sound

Because all targets are emitted from the same Lean, they are byte-identical where it counts: the JS node, the WASM kernel, and the Lean reference answer the same wire request the same way (cross-implementation parity is asserted byte-equally — see Run a Node). There is no spec↔implementation gap to drift, because there is only one source and the rest is a checked projection of it.

Spec layers

ENC's spec is layered so each layer depends only on the ones below it: kernel → node → app → deployment, with appgen depending on kernel + node + app. Changing the kernel changes which histories, states, and proofs are valid; everything above is generated to match.

See also