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

Local Build and Test Guide

Prerequisites

Required

  • Node.js 20+ and Yarn
  • Lean 4 via elan 
    curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh

Optional (for cross-impl tests)

  • Rust via rustup 
    curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
  • wasm-pack (for WASM target) 
    cargo install wasm-pack

Setup

git clone --recurse-submodules https://github.com/enc-protocol/impl-node.git
cd impl-node
yarn install

If you already cloned without --recurse-submodules:

git submodule update --init

Build

Generate JS from Lean (required before testing)

yarn build:js

This does two things:

  1. lake build — type-checks all 259 theorems, compiles the codegen binary
  2. lean --run Gen.lean — generates 19 JS files into sdk/core/, sdk/client/, js/node/

First build takes ~2 minutes (downloads Lean dependencies). Subsequent builds take ~3 seconds.

Build Rust (optional)

yarn build:rs

Compiles rs/ with cargo. Required for Rust cross-impl tests.

Build WASM (optional)

yarn build:wasm

Runs wasm-pack build on rs/, outputs to wasm/ (~92KB). Required for WASM cross-impl tests.

Build everything

yarn build          # JS + Rust + WASM

Test

Core tests (no server needed)

yarn test:pure         # 62 tests — crypto, RBAC, SMT, CT, events
yarn test:property     # 27 tests — randomized protocol properties
yarn test:verifier     # 35 tests — independent signature verification
yarn test:mutation     # 16 mutations — all killed

Node tests (spawns local wrangler automatically)

yarn test:node         # 95 tests — full protocol conformance
yarn test:concurrent   # 9 tests — parallel commit processing
yarn test:fuzz         # 31 tests — adversarial inputs
yarn test:persistence  # 6 tests — state survives restart
yarn test:coverage     # 31 tests — migration, gates, sessions, bundles

These tests start a local wrangler dev instance, run the tests, and shut it down. You don't need to start wrangler manually.

Cross-implementation tests

yarn test:cross        # 29 Rust + 17 WASM — byte-identical output
yarn test:rs           # 25 Rust unit tests

Run everything

yarn test:all          # All JS tests + cross-impl + Rust

Local development server

Start a local node:

npx wrangler dev

This starts the Cloudflare Worker locally at http://localhost:8787. You need to set the NODE_PRIVATE_KEY secret first:

# Generate a keypair
yarn keygen
 
# Set it for local dev (add to .dev.vars file)
echo 'NODE_PRIVATE_KEY = "your_64_hex_private_key"' > .dev.vars

Then start the server:

npx wrangler dev

Test against local node

Create an enclave:

curl -X POST http://localhost:8787/create-enclave \
  -H 'Content-Type: application/json' \
  -d '{"manifest": {"enc_v": 2, "nonce": 1, "RBAC": {"use_temp": "none", "schema": [{"event": "*", "role": "Public", "ops": ["C","R"]}], "states": [], "traits": [], "initial_state": {}}}}'

Submit a commit (requires SDK — see test/node.test.js for examples).

Verify proofs

cd spec/spec-lean && lake build

This type-checks all 259 theorems. If any proof uses sorry, it fails. The build succeeds only if every theorem is kernel-checked.

Project structure

package.json          — build and test scripts
wrangler.toml         — Cloudflare Worker config
.dev.vars             — local dev secrets (not committed)
 
spec/                 — Lean specification (git submodule → impl-spec)
sdk/core/             — 6 generated protocol files
sdk/client/           — 6 generated client SDK files
js/node/              — 5 generated server files + 2 worker templates
rs/             — Rust implementation
wasm/             — WASM binary output
test/                 — all test suites
docs/                 — guides and audits