JC Compute — A solution for digital trust through…

Pitch

Description

Comments

About this project

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.