Skip to content
ENC Protocol

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 reference kernelthe cross-implementation parity oracle
    Rust / WASM kernelthe canonical enc-core.wasm kernel + Rust host

  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

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