Lean 4 formalization of the current JAR design up to the JAVM kernel level.
All commands below run from the spec/ directory.
JAR stands for Join-Accumulate Refine. It describes the core data flow of the protocol: work packages are refined off-chain, then join-accumulated on-chain into the global state.
- Readable core spec — keep the decided SSZ, PVM2, capability, SubVM, and kernel rules in machine-checked notation.
- Executable reference fragments — expose small definitions that can be evaluated and tested while the Rust implementation evolves.
- Proof hooks — state the invariants that matter at the JAVM kernel boundary without carrying old JAM/EVLES machinery.
| Module | Description |
|---|---|
Jar.Basic |
Shared byte, hash, key, slot-path, memory-layout, and depth constants. |
Jar.SSZ |
SSZ type descriptors, layout validity, offset monotonicity, and merkleization boundary. |
Jar.PVM2.* |
RV64E register map, 32-bit memory envelope, instruction classes, basic blocks, and gas model. |
Jar.Cap |
Image, data, CNode, instance capabilities and management operations. |
Jar.Kernel |
Gas/quota resources and yield routing, including the kernel yield namespace. |
Jar.SubVM |
Invocation, pause/well-formedness, scratchpad slot, depth, and gas-charge rules. |
Jar.JAVM |
Aggregate JAVM image and execution state. |
Genesis.* |
Proof-of-Intelligence genesis scoring, kept as the established standalone library. |
lake buildmake testThis builds the Jar library, the Genesis library, and the genesis CLI.
Build the rendered Lean manual:
make bookJAR uses a Proof-of-Intelligence model for its genesis token distribution. Every merged PR is scored on difficulty, novelty, and design quality by ranked comparison against past commits. Contributors earn weight proportional to their demonstrated intelligence. See GENESIS.md for the full protocol design.
Lean 4.27.0 — pinned in lean-toolchain.