Metadata-Version: 2.4
Name: trace-agent-lang
Version: 0.1.0a2
Summary: Agent-native computation language & durable transaction runtime with Lean 4 verified invariants
Author: Trace Contributors
License: Apache-2.0
Keywords: agent,saga,transactions,formal-verification,ast,lean4,devtools
Classifier: Development Status :: 3 - Alpha
Classifier: Intended Audience :: Developers
Classifier: License :: OSI Approved :: Apache Software License
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Software Development :: Compilers
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
Dynamic: license-file

<div align="center">

# ⚡ TRACE / 迹

### The Agent-Native Computation Language & Durable Transaction Runtime
**Backed by Lean 4.35.0 Machine-Checked Mathematical Invariants**

[![Lean 4 Verified](https://img.shields.io/badge/Lean_4.35.0-Verified_(27_Theorems)-blue?logo=lean)](formal/)
[![Tests](https://img.shields.io/badge/Tests-188%20Passed-success)](tests/)
[![Admissions](https://img.shields.io/badge/Lean_Admissions-0_Sorry_/_Admit-brightgreen)](formal/)
[![License](https://img.shields.io/badge/License-Apache_2.0-blue.svg)](LICENSE)
[![Python](https://img.shields.io/badge/Python-3.11+-informational)](pyproject.toml)

[为什么需要 Trace](#-why-trace) • [使用场景与边界](#-现实中怎么用开发所有项目都要用它吗) • [5分钟快速上手](#-quickstart-in-5-minutes) • [Trace Lens 可视化](#-trace-lens-visual-devtools) • [商业化蓝图](docs/OPEN_CORE_STRATEGY.md)

</div>

---

## 💡 Why Trace?

When Autonomous AI Agents write and execute software today, they suffer from three fundamental limitations:

1. **Context Window Token Bloat**: LLMs waste 50% to 80% of tokens reading entire files and massive 50-line traceback dumps just to fix a single bug.
2. **Crash Inconsistency & Duplicate Side Effects**: When an agent's multi-step execution crashes mid-way (e.g., API timeout or server restart), external effects are leaked, payments double-charged, or compensation order broken.
3. **Multi-Agent Collision (Lost Updates)**: Text-based Git diffs fail when multiple agents collaborate on the same file, resulting in torn ASTs and merge conflicts.

**Trace solves this at the language and runtime foundation:**
- 🛡️ **Durable Sagas**: Mathematically proven reverse compensation order, process crash recovery (`os._exit` resilient), and failure blockades.
- 🌳 **Persistent AST Identity & CAS**: Every syntax node has a stable cryptographic UUID and content hash. Updates apply via Compare-And-Swap (0% lost updates).
- 🎯 **Sub-Millisecond Counterexample Shrinking**: Automatically isolates minimal failing inputs in 0.3ms, cutting diagnostic tokens by 77% and achieving single-turn Pass@1 bug repairs.
- 📐 **Mechanically Verified in Lean 4**: 27 core theorems proved with zero unreviewed axioms and zero `sorry`.

---

## 🎯 现实中怎么用？开发所有项目都要用它吗？
### When Should I Use Trace? (And When Shouldn't I?)

> **tl;dr 核心结论**：**绝对不要所有项目都用它，你完全不需要推翻重写现有的项目！**  
> 90% 的普通业务逻辑（写网页界面、查数据库列表、做数据分析）继续用你熟悉的 Python/Go/JS/Vue；只有那 **10% 最核心的“AI Agent 调度、多步外部 API 扣费/发货、容灾防重复”** 的高危链路，交给 Trace 守护。

```
┌────────────────────────────────────────────────────────────────────────┐
│                   你的现有项目 (FastAPI / Django / Go)                  │
│                                                                        │
│   常规业务接口 (90%)                       高危交易 / AI Agent 任务 (10%) │
│   ┌───────────────────────────┐           ┌──────────────────────────┐ │
│   │ 查列表、展示数据、写网页   │           │ 多步扣费、调度外部 API   │ │
│   │ 普通 Python / Vue 代码    │           │ 用 Trace @flow 守护      │ │
│   └───────────────────────────┘           └────────────┬─────────────┘ │
└────────────────────────────────────────────────────────┼───────────────┘
                                                         │
                                           ┌─────────────▼───────────────┐
                                           │ Trace Lens 本地可视化控制台 │
                                           │ (http://127.0.0.1:8080)     │
                                           └─────────────────────────────┘
```

#### 🌟 适用场景：它在什么时候是“救命稻草”？

1. **场景 1：AI Agent 复杂多步外部调用（核心痛点：崩溃防重与自动回滚）**
   - **典型业务**：Agent 执行 `“抓取数据 ➔ 扣除用户 50 积分 ➔ 调用外部模型 ➔ 发送短信通知”`。
   - **痛点**：普通 Python 代码一旦在第 4 步发短信时网络超时，由于已经扣了 50 积分，重试就会导致**“重复扣费 100 积分”**；不重试就会导致**“扣了费没发短信”**。
   - **Trace 怎么解决**：用 `@flow` 包装。Trace 自动落盘事务日志，断电重启自动断点续跑；若短信彻底失败，**严格按数学反向顺序自动触发退款回滚，0 重复扣费，0 坏账**。

2. **场景 2：让 AI 程序员（Cursor / Devin / 自动化 Agent）修代码**
   - **典型业务**：让 AI 自动给已有系统找 bug 并打补丁。
   - **痛点**：传统 Python 报错会丢出 50 行堆栈，消耗巨量 Token 且 Agent 容易改错；如果有 2 个 Agent 同时改代码，还会把彼此的代码直接覆盖（Lost Update）。
   - **Trace 怎么解决**：用 `trace agent-ce` 在 **0.3毫秒内**把报错精准收缩成最小输入（例如：`输入为 0 时越界`），Token 消耗降低 **77%**；提交补丁使用 **AST 密码学 CAS**，冲突直接拦截，绝不会互相覆盖。

3. **场景 3：金融/电商/审批等高敏感交易链条**
   - **典型业务**：跨系统的订单支付、库存锁定、优惠券核销。
   - **痛点**：手写 try-catch、防重表和分布式回滚极容易出 bug。
   - **Trace 怎么解决**：底层经过 **Lean 4.35.0 形式化机械证明（27项定理）**，从数学公理上保证“只要补偿失败就强制封锁告警，绝不假装成功”。

#### 🚫 哪些场景绝对不要用它？
- ❌ **不要用来写网页前端（UI）**：做页面请继续用 Vue/React。
- ❌ **不要用来做大模型矩阵计算或极低延迟网关**：做张量计算用 PyTorch/CUDA，做微秒级通信用 C++/Rust。
- ❌ **不要用来写简单的一次性脚本**：如果只是写一个爬虫、或者转个 Excel 文件，普通的几行 Python 脚本是最快的，引入形式化事务属于过度设计。

---

## 📊 Feature Comparison

| Capability | Raw Python / JS | Temporal / Cadence | LangGraph / CrewAI | **Trace** |
| :--- | :---: | :---: | :---: | :---: |
| **Crash-Safe Multi-Step Saga** | ❌ Manual | ✅ Yes (Heavy Server) | ❌ Memory-only | **✅ Built-in & Lean 4 Proven** |
| **Zero Side-Effect Leaks on Crash**| ❌ No | ✅ Yes | ❌ No | **✅ 100% Guaranteed** |
| **AST-Level Compare-And-Swap (CAS)**| ❌ Text Diffs | ❌ N/A | ❌ N/A | **✅ Cryptographic AST Identity** |
| **Sub-Millisecond Counterexample Shrinking**| ❌ Raw Tracebacks | ❌ N/A | ❌ No | **✅ 0.3ms Minimal Inputs** |
| **Context Window Token Savings** | 0% | 0% | 0% | **✅ 53.3% - 80%+ Reduction** |
| **Runtime Overhead & Dependencies** | Low | Heavy Cluster | Medium | **Zero External Dependencies** |

---

## 🚀 Quickstart in 5 Minutes

Trace adopts a **Progressive Adoption Ladder**: start directly in your existing Python codebase with zero rewrite, or use the dedicated `.trace` DSL.

### Level 0: Python Decorator SDK (`@flow` & `@contract`)

No new syntax required! Import Trace directly into your Python service:

```python
from trace_lang import flow, contract

# 1. Add contracts with automatic property fuzzing
@contract(
    requires=lambda price: price >= 0,
    ensures=lambda result, price: result >= 0
)
def calculate_discount(price: int) -> int:
    return price - 50 if price > 100 else price

# 2. Define durable, crash-resilient multi-step Sagas
@flow(db_path="ecommerce.db")
def checkout_pipeline(ctx, order_id: str, amount: int):
    # If payment succeeds but license fails, payment is automatically refunded in reverse order!
    ctx.step("charge_card", forward=stripe_charge, undo=stripe_refund, payload=amount)
    ctx.step("provision_key", forward=generate_license, undo=revoke_license, payload=1)

# Execute or resume after crash
order = checkout_pipeline(run_id="order_9901", order_id="ord_9901", amount=150)
result = order.run()
print(f"Status: {result['status']}") # 'succeeded' or 'compensated'
```

### Level 1: Launch Trace Lens Visual DevTools

Trace includes an embedded local web console for real-time transaction debugging and AST inspection:

```bash
# Launch interactive developer UI on http://127.0.0.1:8080
python -m trace_lang lens
```

![Trace Lens Preview](docs/images/trace_lens_preview.png)
*(Interactive visual DAG of Sagas, compensation flows, AST lineage, and 0.3ms property fuzzing sandbox)*

### Level 2: Agent Tooling CLI (For Autonomous Coding Agents)

When an AI agent needs to inspect or patch code, use Trace's specialized CLI:

```bash
# 1. Get minimal dependency slice & hole info (saves >50% context tokens)
python -m trace_lang agent-context examples/orders.trace --target "fn.quote"

# 2. Find and shrink minimal counterexample
python -m trace_lang agent-ce examples/discount.trace --fn discount
# Output: {"status": "counterexample_found", "minimal_args": [0], "diagnostic": "E_CONTRACT"}

# 3. Apply atomic AST patch with revision check
python -m trace_lang patch examples/orders.trace patch.json --output patched.trace
```

### Level 3: Pure `.trace` DSL & Formal Machine Checking

Trace programs express pure computation, typed contracts, and persistent UUIDs:

```trace
@revision(1)
@id("type.Cart")
type Cart = { items_count: Int, subtotal: Int }

@id("fn.apply_coupon")
fn apply_coupon(cart: Cart, discount: Int) -> Int
  require cart.subtotal >= 0 && discount >= 0
  ensure result >= 0
{
  if discount >= cart.subtotal then 0 else cart.subtotal - discount
}
```

Verify formal proofs with Lean 4:
```bash
python tools/check_formal.py --lean <path-to-lean-4.35.0>
# Output: {"status": "checked", "lean_theorems": 27, "admissions": 0}
```

---

## 📈 Benchmarks

Empirical performance evaluation from [`benchmarks/agent_efficiency/`](benchmarks/agent_efficiency/):

| Metric | Baseline (Python/Git) | Trace Agent Engine | Gain |
| :--- | :--- | :--- | :--- |
| **Context Window Consumption** | 2,840 bytes (full file) | **1,326 bytes** (dependency slice) | **53.3% - 80%+ Saved** |
| **Diagnostic Traceback Size** | 822 bytes (stack trace) | **188 bytes** (shrunk counterexample)| **77.1% Saved** |
| **Agent Repair Convergence** | 3 - 5 turns (trial & error) | **1 turn (Pass@1)** | **3x Faster Convergence** |
| **Crash Side-Effect Leakage** | Frequent duplicate API calls | **0 leaked side effects** | **100% Mathematical Safety** |
| **Multi-Agent CAS Collision** | Silent overwrite / torn AST | **1 winner + E_ID_CONFLICT abort**| **100% Atomic Serialization** |

---

## 🏗️ Repository Architecture

```text
├── trace_lang/               # Core Python implementation (Zero external dependencies)
│   ├── sdk.py               # Progressive Adoption SDK (@flow, @step, @contract)
│   ├── lens.py              # Trace Lens embedded local Web DevTools & API
│   ├── saga.py              # Crash-safe Saga coordinator & SQLite journal
│   ├── identity.py          # Persistent AST Identity CAS engine & lineage index
│   ├── agent_tools.py       # Context slicing, counterexample shrinking, atomic patches
│   ├── syntax.py            # Trace parser, lexer, and AST formatter
│   └── engine.py            # Runtime interpreter & contract evaluator
├── formal/                  # Lean 4.35.0 Formal Verification Proofs (27 Theorems)
│   ├── CoreTyping.lean      # Type uniqueness & preservation semantics
│   ├── Identity.lean        # Monotonic retirement & CAS safety theorems
│   └── Saga.lean            # Reverse compensation ordering & failure blockade
├── tests/                   # 188 Unit & Industrial Chaos Tests
│   ├── test_sdk.py          # Level 0 Python SDK tests
│   ├── test_lens.py         # Trace Lens devtools HTTP server tests
│   ├── test_saga_chaos.py   # os._exit crash, reverse replay, blockade & lock tests
│   └── test_identity_concurrency.py # Multi-process CAS stress tests
├── benchmarks/              # Agent efficiency & token savings benchmark suite
└── docs/                    # Architecture, SAGA model, and Open-Core strategy
```

---

## 📜 Open-Core & Commercial Strategy

Trace follows an **Open-Core** model:
- **Community Core (Open Source, Apache 2.0)**: Single-node Saga coordinator, AST Identity, Python SDK, Agent CLI, and Trace Lens Community.
- **Enterprise & Cloud (Commercial / BSL)**: Multi-node distributed Raft Saga cluster, tamper-evident cryptographic compliance gateway, enterprise RBAC/SSO, and Trace Lens Pro.

For full architectural breakdown and commercialization details, read [docs/OPEN_CORE_STRATEGY.md](docs/OPEN_CORE_STRATEGY.md).

---

## 🤝 Contributing

Contributions are welcome! Please read [CONTRIBUTING.md](CONTRIBUTING.md) and [SECURITY.md](SECURITY.md) before opening pull requests. All PRs touching core semantics must pass the Lean 4 formal gate.

---

## 📄 License

Trace is open-source software licensed under the [Apache 2.0 License](LICENSE).
