JC Compute offers a formal computational model focused on deterministic causality and authority. It integrates machine-checked proofs and model-checked specifications into a cohesive framework, ensuring reliability in digital trust applications. Explore its extensive core, runtime, and application layers to leverage advanced computational guarantees.
JC Compute is an advanced formal computational model focusing on Authority-Constrained Deterministic Causal Computation. Its core principle is that computations can be defined as replayable reductions over causally ordered event histories, with strict bounds enforced by capability authority. This repository provides comprehensive components essential for implementing the model, detailed as follows:
| Layer | Contents |
|---|---|
Formal foundations (formal/) | Machine-checked proofs using Lean 4 and TLA⁺ model-checked specifications |
Core substrate (packages/) | Components include Field, Reducer, IR, Merkle, Root, Sync, Query, and Runtime based on UniStack v3 |
Runtime (runtime/) | Features such as fixed-point operator F_Q, oracle functionality, CRDT consensus, and a compression phase space |
Application layer (app/) | Provides a CLI and HTTP server, with six domain demonstrations and a full computational pipeline |
Tests (tests/, test/) | Over 20 unit and integration tests ensuring robustness |
Benchmarks (benchmarks/) | 13 benchmark suites for performance evaluation |
Formal Theorems
The model includes six machine-checked theorems that validate its foundations:
| # | Theorem | Tool | File |
|---|---|---|---|
| T1 | Deterministic Replay | TLA⁺ / TLC | formal/tla/DeterministicReplay.tla |
| T2 | Convergence | TLA⁺ / TLC | formal/tla/Convergence.tla |
| T3 | Capability Preservation | Lean 4 / Mathlib | formal/lean/CapabilityPreservation.lean |
| T4 | Commutativity Characterisation | Lean 4 / Mathlib | formal/lean/CommutativityCharacterization.lean |
| T5 | Projection Consistency | Lean 4 / Mathlib | formal/lean/ProjectionConsistency.lean |
| T6 | Fixed-Point Existence | Lean 4 / Mathlib | formal/lean/FixedPointExistence.lean |
Quick Start (JavaScript Runtime)
Example commands to quickly explore the application include:
npm install
# CLI demo
node src/cli.js --help
node src/cli.js domains
node src/cli.js run --domain financial-settlement
# Application server (port 3000)
npm run app:start
# Tests
npm test
# Benchmarks
npm run bench:kcr
npm run bench:frontier
Architecture Overview
The JC Compute architecture integrates components of history, reduction, capability, and projection:
JC Compute Formal Model
(H, C, R, π, ⊔)
History
│
Reduction (R)
│
State ──── Projection (π) ──── View
│
Merge (⊔) ◄──── Capability (C)
│
Fixed Point
Package Details
The repository includes various packages, each serving specific functionalities:
| Package | Description |
|---|---|
unistack-core | Core primitives including Field, Reducer, IR, and Merkle |
unistack-sync | Handles merging, Pareto frontier, and delta synchronization |
unistack-query | Supports reachability and membership queries, as well as fixpoint analysis |
unistack-meta | Aids in reducer search and architectural dominance analysis |
unistack-runtime | Manages scheduling and execution loops in the node runtime |
unistack-store | Provides persistent state storage |
Domains Supported
The application layer of JC Compute offers various domain capabilities:
| Domain | ID |
|---|---|
| 🤖 Distributed Robotics | distributed-robotics |
| 🧠 AI Agent OS | ai-agent-os |
| 💹 Financial Settlement | financial-settlement |
| 🏭 Autonomous Manufacturing | autonomous-manufacturing |
| 🐝 Multi-Agent Swarms | multi-agent-swarms |
| 🔮 Digital Twin | digital-twin |
Protocol Properties
JC Compute is designed with deterministic principles ensuring:
- No randomness — Execution is fully deterministic.
- No clocks — Time-independence enhances reliability.
- No ordering assumptions — Convergence is maintained regardless of event delivery order.
- No consensus layer — Structural convergence achieved through Pareto merge.
- No privilege escalation — Capability preservation is formally guaranteed.
JC Compute presents a robust framework for developing reliable solutions for computational challenges across multiple domains.
No comments yet.
Sign in to be the first to comment.