docs: update RESEARCH_GAP_ANALYSIS todolist — P0+P1 all checked

Mark all 8 implemented items as done:
- P0: T-Compose types, effect annotations, store independence, handlers
- P1: CEK upgrade, graded cost, algebraic laws, cost vectors
Update coverage: Paper II 55%→85%, Paper III 10%→75%
175 tests passing across 7 test files.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

RESEARCH_GAP_ANALYSIS.md

@@ -14,8 +14,12 @@
 | 论文 | 核心贡献 | 实现状态 | 覆盖率 |
 |------|---------|---------|--------|
 | **论文 I** | λA DSL + Lint | 接近完成 | **~90%** |
-| **论文 II** | 操作语义 + CEK 机器 | 部分完成 | **~55%** |
-| **论文 III** | 类型与效果系统 | 几乎未实现 | **~10%** |
+| **论文 II** | 操作语义 + CEK 机器 | ✅ P0+P1 完成 | **~85%** |
+| **论文 III** | 类型与效果系统 | ✅ P0+P1 完成 | **~75%** |
+
+> **更新 (2026-04-04)**: P0 (4项) + P1 (4项) 全部实现，共 175 个测试通过。
+> 新增文件: `types.py`, `effects.py`, `store_analysis.py`, `handlers.py`, `cost_grade.py`, `rewrite.py`
+> 升级文件: `cek_machine.py`, `core.py`, `primitives.py`, `extensions.py`, `multiagent.py`, `compiler.py`
 
 ---
 
@@ -43,7 +47,7 @@
 
 ---
 
-## 3. 论文 II（操作语义 + CEK 机器）— 覆盖率 ~55%
+## 3. 论文 II（操作语义 + CEK 机器）— 覆盖率 ~85% ✅
 
 ### 已实现
 
@@ -69,7 +73,7 @@
 
 ---
 
-## 4. 论文 III（类型与效果系统）— 覆盖率 ~10%
+## 4. 论文 III（类型与效果系统）— 覆盖率 ~75% ✅
 
 ### 已实现
 
@@ -179,25 +183,25 @@ def apply(self, input_str, ctx):
 
 ### P0 — 关键（理论到实践的基础）
 
-- [ ] **实现 T-Compose 类型检查**（论文 III §3.3.3）
+- [x] **实现 T-Compose 类型检查**（论文 III §3.3.3）✅ `lambdagent/types.py` — 44 tests
   - 为 YAML schema 添加 `inputType` / `outputType` 标注
   - 实现 `is_subtype()` 及 Json(S) 结构子类型
   - 在 `compiler.py` 中检查组合边界
   - 错误信息应引用论文 III T-Compose 规则
 
-- [ ] **实现效果标注**（论文 III §4）
+- [x] **实现效果标注**（论文 III §4）✅ `lambdagent/effects.py` — 35 tests
   - 定义效果枚举：`pure | llm(m) | io | state(s)`
   - 实现串行 `·`、并行 `∥`、迭代 `εⁿ` 组合
   - 编译期间为每个 Term 标注计算效果
   - 为 YAML schema 添加 `effectAnnotation` 字段
 
-- [ ] **强制执行 Pair 存储独立性**（论文 II 命题 30）
+- [x] **强制执行 Pair 存储独立性**（论文 II 命题 30）✅ `lambdagent/store_analysis.py` — 20 tests
   - 为全部 11 个构造实现 `writes(term)` 分析
   - 在 `AsyncPar` 执行前添加存储独立性检查
   - 实现 `ctx.fork()` 以便每个并行分支有独立的 Context 副本
   - 修复 `AsyncPar` 线程安全问题（迁移至 `asyncio`）
 
-- [ ] **实现代数效果处理器**（论文 III §6）
+- [x] **实现代数效果处理器**（论文 III §6）✅ `lambdagent/handlers.py` — 23 tests
   - 定义效果签名：`LLM`、`ToolIO`、`State`、`Cost`
   - 实现三种标准处理器：`ProductionHandler`、`TestHandler`、`TraceHandler`
   - 允许在 `Runtime.execute()` 级别注入处理器
@@ -205,25 +209,25 @@ def apply(self, input_str, ctx):
 
 ### P1 — 重要（核心引擎升级）
 
-- [ ] **将 CEK 机器提升为主执行器**（论文 II §5）
+- [x] **将 CEK 机器提升为主执行器**（论文 II §5）✅ `lambdagent/cek_machine.py` — 21 tests
   - 用 CEK 状态机替换递归 `Executor.reduce()`
   - 实现 Yield 作为 `async/await` 以实现非阻塞 LLM/工具调用
   - 实现所有 continuation 帧（定义 27）：`compK`、`loopK`、`pairLK`、`pairRK`、`guardK`、`memK`
   - 确保 CEK ↔ 小步对应性（定理 28）
 
-- [ ] **实现分级成本预测**（论文 III §4.3）
+- [x] **实现分级成本预测**（论文 III §4.3）✅ `lambdagent/cost_grade.py` — 18 tests
   - 定义 `CostGrade = (p: float, t: int, l: float, m: float)`
   - 实现分级组合规则（定义 11–12）
   - 编译时为每个 agent 流水线计算最坏情况成本
   - 在 API 中暴露成本预测：`POST /api/v1/agents/{id}/cost-estimate`
 
-- [ ] **实现代数定律作为重写规则**（论文 II 定理 36–41）
+- [x] **实现代数定律作为重写规则**（论文 II 定理 36–41）✅ `lambdagent/rewrite.py` — 14 tests
   - 在编译器中实现 6 条定律作为 AST 重写 pass
   - 添加 identity 消除（左/右单位元定律）
   - 添加路由分配优化
   - 对 Guard 分配反模式发出警告（命题 42）
 
-- [ ] **精确成本向量累积**（论文 II 定义 5）
+- [x] **精确成本向量累积**（论文 II 定义 5）✅ 集成于 `cek_machine.py` cost_summary() + CostMonotonicityViolation
   - 按 CEK 步骤跟踪 `c = (tokens, latency, cost)`
   - 将成本单调性（命题 23）作为运行时不变量验证
   - 在轨迹输出中暴露每步成本
@@ -318,8 +322,12 @@ P1: CEK 机器
 | Paper | Core Contribution | Implementation Status | Coverage |
 |-------|------------------|----------------------|----------|
 | **Paper I** | λA DSL + Lint | Near-complete | **~90%** |
-| **Paper II** | Operational Semantics + CEK Machine | Partial | **~55%** |
-| **Paper III** | Type & Effect System | Minimal | **~10%** |
+| **Paper II** | Operational Semantics + CEK Machine | ✅ P0+P1 done | **~85%** |
+| **Paper III** | Type & Effect System | ✅ P0+P1 done | **~75%** |
+
+> **Update (2026-04-04)**: P0 (4 items) + P1 (4 items) all implemented, 175 tests passing.
+> New files: `types.py`, `effects.py`, `store_analysis.py`, `handlers.py`, `cost_grade.py`, `rewrite.py`
+> Upgraded: `cek_machine.py`, `core.py`, `primitives.py`, `extensions.py`, `multiagent.py`, `compiler.py`
 
 ---
 
@@ -347,7 +355,7 @@ P1: CEK 机器
 
 ---
 
-## 3. Paper II (Operational Semantics + CEK Machine) — Coverage ~55%
+## 3. Paper II (Operational Semantics + CEK Machine) — Coverage ~85% ✅
 
 ### Implemented
 
@@ -373,7 +381,7 @@ P1: CEK 机器
 
 ---
 
-## 4. Paper III (Type & Effect System) — Coverage ~10%
+## 4. Paper III (Type & Effect System) — Coverage ~75% ✅
 
 ### Implemented
 
@@ -506,25 +514,25 @@ Paper II proves 6 algebraic laws (Theorems 36–41) that enable safe, semantic-p
 
 ### P0 — Critical (Theory-to-Practice Foundation)
 
-- [ ] **Implement T-Compose type checking** (Paper III §3.3.3)
+- [x] **Implement T-Compose type checking** (Paper III §3.3.3) ✅ `lambdagent/types.py` — 44 tests
   - Add `inputType` / `outputType` annotations to YAML schema
   - Implement `is_subtype()` with Json(S) structural subtyping
   - Check composition boundaries in `compiler.py`
   - Error messages should reference Paper III T-Compose rule
 
-- [ ] **Implement effect annotations** (Paper III §4)
+- [x] **Implement effect annotations** (Paper III §4) ✅ `lambdagent/effects.py` — 35 tests
   - Define effect enum: `pure | llm(m) | io | state(s)`
   - Implement serial `·`, parallel `∥`, iteration `εⁿ` composition
   - Annotate each Term with computed effect during compilation
   - Add `effectAnnotation` field to YAML schema
 
-- [ ] **Enforce Pair store-independence** (Paper II Proposition 30)
+- [x] **Enforce Pair store-independence** (Paper II Proposition 30) ✅ `lambdagent/store_analysis.py` — 20 tests
   - Implement `writes(term)` analysis for all 11 constructs
   - Add store-independence check before `AsyncPar` execution
   - Implement `ctx.fork()` for independent Context copies per parallel branch
   - Fix thread-safety issues in `AsyncPar` (migrate to `asyncio`)
 
-- [ ] **Implement algebraic effect handlers** (Paper III §6)
+- [x] **Implement algebraic effect handlers** (Paper III §6) ✅ `lambdagent/handlers.py` — 23 tests
   - Define effect signatures: `LLM`, `ToolIO`, `State`, `Cost`
   - Implement three standard handlers: `ProductionHandler`, `TestHandler`, `TraceHandler`
   - Allow handler injection at `Runtime.execute()` level
@@ -532,25 +540,25 @@ Paper II proves 6 algebraic laws (Theorems 36–41) that enable safe, semantic-p
 
 ### P1 — Important (Core Engine Upgrade)
 
-- [ ] **Promote CEK Machine to primary executor** (Paper II §5)
+- [x] **Promote CEK Machine to primary executor** (Paper II §5) ✅ `lambdagent/cek_machine.py` — 21 tests
   - Replace recursive `Executor.reduce()` with CEK state machine
   - Implement Yield as `async/await` for non-blocking LLM/tool calls
   - Implement all continuation frames (Definition 27): `compK`, `loopK`, `pairLK`, `pairRK`, `guardK`, `memK`
   - Ensure CEK ↔ small-step correspondence (Theorem 28)
 
-- [ ] **Implement graded cost prediction** (Paper III §4.3)
+- [x] **Implement graded cost prediction** (Paper III §4.3) ✅ `lambdagent/cost_grade.py` — 18 tests
   - Define `CostGrade = (p: float, t: int, l: float, m: float)`
   - Implement graded composition rules (Definitions 11–12)
   - Compute worst-case cost at compile time for each agent pipeline
   - Expose cost prediction in API: `POST /api/v1/agents/{id}/cost-estimate`
 
-- [ ] **Implement algebraic laws as rewrite rules** (Paper II Theorems 36–41)
+- [x] **Implement algebraic laws as rewrite rules** (Paper II Theorems 36–41) ✅ `lambdagent/rewrite.py` — 14 tests
   - Implement 6 laws as AST rewrite passes in compiler
   - Add identity elimination (left/right unit laws)
   - Add route distribution optimization
   - Warn on Guard distribution anti-pattern (Proposition 42)
 
-- [ ] **Precise cost vector accumulation** (Paper II Definition 5)
+- [x] **Precise cost vector accumulation** (Paper II Definition 5) ✅ integrated in `cek_machine.py` cost_summary() + CostMonotonicityViolation
   - Track `c = (tokens, latency, cost)` per CEK step
   - Verify cost monotonicity (Proposition 23) as runtime invariant
   - Expose per-step cost in trace output