Verification Manifest

Deterministic hash chain from Lean spec → codegen → generated code → deployed node.

Spec tag: v0.2.0 Node: https://enc-node.ocrybit.workers.dev Date: 2026-04-22

Verification chain

Lean Spec (259 theorems)  →  DSL Codegen (55 proofs)  →  Generated JS (19 files)  →  Deployed
     sha256: 564cfc7e           sha256: 649573bd            sha256: see below         wrangler deploy

To verify: clone, build, compare hashes.

git clone --recurse-submodules https://github.com/enc-protocol/impl-node.git
cd impl-node
cd spec/spec-lean && git checkout v0.2.0 && cd ../..
yarn build:js
# Compare hashes below against the generated output

Layer hashes

Composite hashes (SHA-256 of all per-file SHA-256 hashes in sorted order):

Layer	Hash	Files
Lean Spec (`Enc/Core/`)	`564cfc7e3aef6d01e7e39f7e38f2eedb83f08ef1b7b793a736c08f0977943748`	34
DSL Codegen (`Enc/DSL/` + `Enc/Gen.lean` + `Enc/Codegen/`)	`649573bd67380ee276429cbb75f1a50bbb61474d4d865c7129eefe9624f5e6b8`	30+
Generated JS — `sdk/core/`	`92a2db86f419745f03a9495c6f140f3b3489651f1a0abccf8650e87b2d3ba382`	7
Generated JS — `sdk/client/`	`e5f55927141d0e2336a651729dc7ec3ddd9ce80df020f0df0ca98d6fa2413355`	7
Generated JS — `js/node/`	`6eb1fe825acde06fc066f0699c68bb64cf4b301019aadf9501455c74380952ef`	7
Rust source (`rs/src/`)	`eb80df749031302341afb901527a7689cbb87b2f91322b0e678f1dcd96c69c49`	10
WASM binary	`dba67eb0a396d3e48187dcb2d31c6ea294c0a9ed34c655fe5e678731f1b9350e`	1

Per-file hashes — sdk/core/

8d3cb142d423615a82fc31ceb1694fc35ccec56dbb69855a9b77e7500b2599a6  crypto.js
bca02b9d58ccbd227329af8d9b5e4bed94c4c19c954a7aa6b7b53a234a3bd8e0  ct.js
18e5e65172dbe58cfaf11087a8cefa0948a3b15a82f10b59129e5ae3947dde4c  event.js
cfe18201cc4941236e47fb7cbf6119ec15de4c478cfdd2020beb3ffac6434f20  index.js
5c1fd14169fee179e536e07a59771b68b228199091d75ed10f6bc19bcf35c96d  rbac.js
d5eddf2efc7d7cf01a3bfd914714b5069ee73842394df4369529f1610d88e64c  smt.js
baaa21448f5afaa4b5afb924a424e2455a8affbe470b5c577d61ed94a86dc8e6  types.js

Per-file hashes — sdk/client/

31b72865b594df81214b368d463d81c3caacd7dde1c8d8430afb477beda6cd73  http.js
84dc0a8a05872a4ddd9a3d23ba75003f661cd8754ac6ef034b725b2d660e653f  index.js
f36420b28d52e2e6c294071515da9cad1385028db0716fbba74e29494fb0d087  registry-client.js
0387086e58dd1b013298ab36668295134e8ac8f6c61f83d9fd2945aec4816ff8  sdk.js
fc783de9915cfe50e8249b665dfef44b6ab26e5287655a25ebadf03f06182e34  session.js
9fafb903c9491daf1c1ffedf591a24d8f9e64d707756153b153e00e28c53461c  wallet.js
b1cec82443e3c16d3e71f90c3a2b6491ad1fe5d19f12ccc428469e8da6e902b8  ws.js

Per-file hashes — js/node/

e48e4cf7782188bd44d10dc19cf41bc265e326911382a1148682edc8ea0f3bf4  handlers.js
abf8b46e61919022c3c516eaf2e3a829fc1c8cd96ef58fc65cf2bdb0446ca096  node.js
a6d7918aab8edf8ad5889c2d735f4da3dc12c5aa6916dccb2119a831b87f89f8  persistence.js
2702fa7e278b96398a59f98cd8f38373a5cb1f0cb339b1119cbd941e51fc7dc9  push.js
1e7bb4aa84f22407342b73b7b858131d9475c414fd29f0f8364b146113d58e0b  worker/enclave.js
664827f447c340943627ed93f5214d8aaa92e5a7fee2d84c9efc500ab55e3941  worker/index.js
f1e5722189de8456ce079ab4d051fb070d10a1fdb47694c136d61ae084c42a0c  ws-handlers.js

Per-file hash — WASM

dba67eb0a396d3e48187dcb2d31c6ea294c0a9ed34c655fe5e678731f1b9350e  encvm_bg.wasm

How to verify

# 1. Verify proofs compile (259 theorems, 0 sorry)
cd spec/spec-lean && lake build
 
# 2. Regenerate JS from Lean
lake env lean --run Enc/Gen.lean
 
# 3. Compare hashes
cd ../..
sha256sum sdk/core/*.js | sort -k2
sha256sum js/node/*.js js/node/worker/*.js | sort -k2
 
# 4. If hashes match → deployed code is the proven code

Cross-implementation verification

The same protocol logic compiled to Rust and WASM produces byte-identical output:

yarn test:cross    # 46 tests: 29 JS↔Rust + 17 JS↔WASM

Same inputs → same SHA-256 → same Schnorr signatures → same event IDs → same state.