# Skill 形式化设计：`Skill : Term → Term`

> 状态：草案 v0.1（待评审）
> 作者：lambdagent 团队
> 日期：2026-06-14
> 关联：[MCP_SKILL_DESIGN.md](MCP_SKILL_DESIGN.md)（现状 P2 prompt skill）、[PRODUCT_GATE_DESIGN.md](PRODUCT_GATE_DESIGN.md)（gate=Guard 形式化）、[harmonyos-agent-dsl-comparison.md](harmonyos-agent-dsl-comparison.md)（鸿蒙 DSL 对照）、Paper III（λA 类型化 Lambda 演算）

---

## 0. 一句话

把 skill 从「编译前被溶解进 systemPrompt 的 prompt 宏」升级为「term graph 里的一等组合子」——注入型 `Skill : Term → Term`（加能力）与对偶的约束型 `Restrict : Term → Term`（封顶能力），二者在效果格上构成伽罗瓦连接。由此让现有的 effect / cost grade / 类型 / Guard 四套形式化机器**免费**作用到 skill 上，并以此契约作为向鸿蒙 Agent DSL 移植的运行时无关 IR。

---

## 1. 背景与动机

### 1.1 现状：skill 是形式化盲区

当前 prompt skill 的生命周期（[skill_registry.py:188](../agentpaas/src/agentpaas/engine/skill_registry.py)）：

```
skill.yml (prompt + requires.tools)
   └─ mount_into_config(config)          # agentpaas 层，编译前
        ├─ prompt 追加到 systemPrompt（带受限边界包裹 + 注入扫描）
        └─ requires.tools 并进 mcp.localTools（高风险工具进权限 diff）
             └─ lambdagent.from_config(config) 才编译成 term graph
```

关键事实：**skill 在进入 term graph 之前就被内联溶解了**。等到 `Lam` / `Compose` / `Guard` / `estimate_cost` / `infer_effect_for_term` 开始工作时，skill 已不是独立对象。后果：

- `estimate_cost(term)`（[cost_grade.py:234](../lambdagent/src/lambdagent/cost_grade.py)）算不出"挂这个 skill 多花多少 token / 钱"；
- `infer_effect_for_term(term)`（[effects.py:309](../lambdagent/src/lambdagent/effects.py)）看不到 skill 引入的 IO/STATE 效果；
- skill 没有输入/输出类型，无法做 `is_subtype` 组合检查；
- skill 的"产出是否合格"（assignment-grader 必须产出含 `review_report` 标记的报告）没有被 `Guard` 强制，只能靠 prompt 自觉。

### 1.2 机会：四套机器都现成

一个 skill 现在携带的数据 `(prompt, requires.tools, requires.mcp_scopes)` 恰好够派生一个完整形式契约：

| 已有机器 | 文件 | 给 skill 派生 |
|---|---|---|
| `infer_effect_for_term` + 效果格 `pure ≤ state ≤ io ≤ llm` | [effects.py:309](../lambdagent/src/lambdagent/effects.py) | 效果上界 ε_s |
| `CostGrade` + `grade_*` + `estimate_cost` | [cost_grade.py:37](../lambdagent/src/lambdagent/cost_grade.py) | 成本天花板 g_s |
| `AgentType (τ₁ →^ε τ₂)` + `is_subtype` | `lam_types.py` | 输入/输出契约 |
| `Guard(agent, validator, retry, on_fail)` | [extensions.py:146](../lambdagent/src/lambdagent/extensions.py) | 验收谓词 P_s |

本设计就是把这四样东西显式地挂到每个 skill 上。

### 1.3 表征：skill 形态谱系（覆盖性证据）

为确保 `interface:` 设计能表征真实生态里的 skill（而非纸上谈兵），下面用本机磁盘上 6 类真实样例（项目自有 + gstack + Anthropic 生态，共 535 个 SKILL.md 中取跨度最大者）刻画 skill 的形态：

| 类 | 真实样例 | 形态 | 载体 | 实际是什么 | 对效果的作用 |
|---|---|---|---|---|---|
| **A 声明 prompt** | `assignment-grader`（本项目 [skill.yml](../agentexample/skills/assignment-grader/skill.yml)） | 纯方法论 prompt | 单 yml，无 frontmatter | prompt + `requires.tools` | 注入（↑） |
| **B 约束/拦截** | gstack `careful`/`freeze`/`guard` | 工具调用拦截器 | frontmatter `hooks.PreToolUse` + `bin/*.sh` | 危险命令拦截钩子（非 prompt） | **约束（↓）** |
| **C 工具+代码** | gstack `make-pdf` | prompt 指挥捆绑脚本 | 25KB prompt + `src/ dist/ test/` | prompt + 转换脚本 | 注入（↑） |
| **D 多步工作流** | gstack `qa` | test→fix→verify 循环 | 65KB prompt + `references/ templates/` | 多步骤、原子提交 | 注入（↑） |
| **E 外部桥接** | gstack `codex` | 包装外部 CLI | 61KB prompt，三模式 | 调 `codex` CLI 作第二意见 | 注入（↑，io） |
| **F 代码库** | Anthropic `pdf`/`docx`/`pptx`/`xlsx` | SKILL.md + 捆绑 Python | SKILL.md + 脚本 + 参考文档 | 可执行库 + 用法说明 | 注入（↑） |

**表征轴**（skill 在这些维度上连续变化）：

```
载体:    单 yml ─────────────────────────────▶ SKILL.md + 脚本目录 + 资源
能力:    纯 prompt ── +工具 ── +捆绑代码 ── +外部进程 ── +运行时钩子
对效果:  注入能力(↑) ◀──────────────────────────────▶ 约束能力(↓)   ← 双向！
执行:    改变 LLM 行为(声明式) ──────────────▶ 真正跑代码(命令式)
验收:    靠 prompt 自觉 ── 产物标记 ── pass/fail gate ── 脚本退出码
```

**关键发现（驱动 §3.5）**：A/C/D/E/F 都是**往 agent 里加能力**（`Skill : Term → Term`，效果只增），可统一归约到 §3.2 的 `Guard(Memory(...))`。但 **B 类（约束/拦截）方向相反**——它不注入，而是**砍效果上界 / 缩工具面 / 在工具调用前拦截**。因此单一的能力注入组合子覆盖不全 skill 谱系，需引入一个对偶的 `Restrict` 组合子（§3.5）。这两者构成效果格上的一对伽罗瓦连接，是本设计安全论证最硬的一块。

> 覆盖性结论：`{Skill, Restrict}` 两个组合子 + §4 `interface:`/`restrict:` schema 即可表征上表全部 6 类形态（脚本型 C/F 经 §7.3 normalize 后落到 `Tool`/`Compose`）。

---

## 2. 目标与非目标

### 2.1 目标

- **G1** 给 skill 一个形式语义 `Skill : Term → Term`，使其成为 term graph 的一等公民。
- **G2** 扩展 skill.yml 增加可选 `interface:` 段（类型 / 效果上界 / 验收谓词），向后兼容现有 prompt-only skill。
- **G3** skill 进入 term graph 后，自动获得 effect / cost / type 的派生与组合（整 agent 的界由 skill 的界按现有 `grade_serial/parallel` 合成）。
- **G4** 以 `interface:` 契约为运行时无关 IR，给出到鸿蒙 Agent DSL（`@agent`/`@prompt[pattern]`/`@tool`）的映射规则与可行性检查。
- **G5** 保持现有安全不变量：系统规则永远在前、注入扫描、高风险工具不自动授予。
- **G6** 覆盖 skill 全谱系（§1.3 六类）：注入型归 `Skill`、约束型归对偶组合子 `Restrict`（§3.5），二者构成效果格伽罗瓦连接，使 agent 最终能力有可证的上下界。

### 2.2 非目标

- **N1** 不追求"零不确定性"。本设计提供的是**显式且可校验的概率界**（`p`、`p_fatal`），不是确定性消除。
- **N2** 不改 lambdagent 编译器对 agentpaas 的依赖方向（编译器仍无 agentpaas 依赖）。
- **N3** 不在本期实现端侧（鸿蒙）codegen 落地，仅给出映射规格；落地见 §8 P3。
- **N4** 不把可执行脚本型 skill（OpenClaw/Claude SKILL.md + scripts）纳入本期；本期只覆盖 prompt skill + 工具授予型 skill，脚本型的 normalize 见 §7.3 与后续设计。

---

## 3. 核心语义：`Skill : Term → Term`

### 3.1 直觉

skill 不是一个 term（不是独立 agent），而是一个**作用在 agent 上的变换**：它给一个已有 agent 注入能力（prompt + 工具）并约束其产出。因此把 skill 建模为 term 上的组合子：

```
Skill_s : Term → Term
```

### 3.2 指称语义

设 skill `s = (prompt_s, tools_s, mcp_s, iface_s)`，作用在 agent term `A` 上：

```
Skill_s(A)  ≜  Guard(
                  Memory( A ⊕ prompt_s ⊕ tools_s ),   -- 注入能力（复用现有 mount 逻辑）
                  validator = P_s,                      -- iface_s.guard 派生的验收谓词
                  retry     = iface_s.retry,
                  on_fail   = iface_s.on_fail
               )
```

其中：

- `A ⊕ prompt_s`：把 `prompt_s` 以受限边界包裹追加到 `A` 的 systemPrompt（**沿用** [skill_registry.py:223-226](../agentpaas/src/agentpaas/engine/skill_registry.py) 的包裹文案与注入扫描，语义不变）。
- `A ⊕ tools_s`：把 `tools_s` 并进 `A` 的 localTools（**沿用** [skill_registry.py:228-235](../agentpaas/src/agentpaas/engine/skill_registry.py) 的高风险工具不自动授予规则）。
- `Memory(·)`：复用 [extensions.py:109](../lambdagent/src/lambdagent/extensions.py)，若 skill 不需要持久态可退化为恒等包裹（无 STATE 效果）。
- `Guard(·, P_s, ...)`：复用 [extensions.py:146](../lambdagent/src/lambdagent/extensions.py)。**若 `iface_s` 未声明 guard，则 `P_s = λ_. True`**（恒真谓词，retry=0）——退化为「不验收」，与今天行为等价。

> **要点**：当 `iface_s` 缺省（旧 skill）时，`Skill_s(A)` 在可观测行为上**严格等价**于今天的 `mount_into_config`——只是现在它是 term graph 里一个具名节点，能被 cost/effect 看见。这是 G2 向后兼容的形式保证。

### 3.3 组合律

多个 skill 挂同一 agent，定义为组合子的函数复合：

```
[s₁, s₂](A)  ≜  Skill_{s₂}(Skill_{s₁}(A))
```

即 `mount` 的 skill 列表顺序 = 组合子从内到外的顺序。Prompt 追加顺序、工具并入顺序与今天一致（列表序）。

**注意非交换性**：`Skill_{s₁} ∘ Skill_{s₂} ≠ Skill_{s₂} ∘ Skill_{s₁}`，因为 Guard 嵌套层次不同（外层 Guard 看到的是内层 Guard 之后的结果）。评审点 R1：是否需要把多 skill 的 Guard 合并成单层合取 `P_{s₁} ∧ P_{s₂}` 而非嵌套？见 §10。

### 3.4 与 PRODUCT_GATE 的一致性

PRODUCT_GATE_DESIGN.md 已确立 `gate = Guard`。本设计把 skill 也归约到 `Guard`，二者同源：pipeline 的 gate 验收 stage 产物，skill 的 Guard 验收单 agent 产物。两者都走 `grade_guard`（[cost_grade.py:164](../lambdagent/src/lambdagent/cost_grade.py)）计成本。

### 3.5 对偶组合子：`Restrict : Term → Term`（约束型 skill）

§1.3 的 B 类（`careful`/`freeze`/`guard`）方向与 `Skill_s` 相反：它**不注入能力，而是封顶能力**。建模为 `Skill_s` 的对偶：

```
Restrict_r(A)  ≜  A   但施加三层约束：
                    ε'      = effect_meet(ε_A, ε_allow)        -- 效果取下确界（砍，非取并）
                    tools'  = tools_A ∩ tools_allow            -- 工具面取交（缩，非并）
                    每次 Tool 调用前过守卫谓词 H_r             -- PreToolUse 拦截，命中则 ask/deny
```

其中：

- `effect_meet`：效果格 `pure ≤ state ≤ io ≤ llm` 上的**下确界**（与 §5.1 `max_effect` 的上确界对偶）。例：`Restrict` 把 `io` 砍成 `pure` ⟹ agent 不再能调外部工具。需在 [effects.py](../lambdagent/src/lambdagent/effects.py) 补 `min_effect`（对偶于 `max_effect`，[effects.py:244](../lambdagent/src/lambdagent/effects.py)）。
- `tools_allow`：允许工具白名单；`A` 原有但不在白名单的工具被移出 localTools。
- `H_r`：工具调用守卫，对应 careful 的 `hooks.PreToolUse`（[careful/bin/check-careful.sh](../../../.claude/skills/gstack/careful/bin/check-careful.sh) 那样的危险命令拦截）。形式上是 Tool 层的 `Guard`：`Tool_guarded = λx. if H_r(call) then tool(x) else REFUSE`。复用 builtin 的 `dangerousCommandBlock`/`highRiskConfirmation` guard 机制（记忆「AgentEdit 加 Guard tab」），不需新拦截器。

**安全代数（核心论证）**：`Skill`（注入，`effect_leq(ε_A, ε_after)`，单调增）与 `Restrict`（约束，`effect_leq(ε_after, ε_A)`，单调减）在效果格上构成一对**伽罗瓦连接**。对任意 agent `A` 与 skill 集，最终能力可证地被夹在区间内：

```
effect_leq( Restrict 施加的下界 ,  ε_最终 )  ∧  effect_leq( ε_最终 ,  Skill 累积的上界 )
```

这把"形式化压住不确定性"从单纯的**输出验收**（Guard）推进到**工具调用层的静态能力封顶**——agent 能做什么有了可证的上下界，而非运行时撞墙。

**组合顺序约定**：`Restrict` 总在最外层（`Restrict_r(Skill_{s₂}(Skill_{s₁}(A)))`），即先注入能力再统一封顶，保证约束不被后续 skill 突破。`mount` 时若同时声明 `skills` 与约束型 skill，约束型一律后挂（最外）。评审点 R6（§10）：是否允许约束型嵌在中间以做分层授权？

### 3.6 三组合子全景

| 组合子 | 文件/状态 | 语义 | 对效果 | 覆盖 §1.3 类 |
|---|---|---|---|---|
| `Skill : Term→Term` | 新（归约到 Guard∘Memory） | 注入 prompt+工具+验收 | `max`（↑） | A/C/D/E/F |
| `Restrict : Term→Term` | 新（归约到 effect_meet + Tool-Guard） | 砍效果+缩工具+调用守卫 | `meet`（↓） | B |
| `Guard`（已有） | [extensions.py:146](../lambdagent/src/lambdagent/extensions.py) | 输出验收+重试 | 不变 | 二者复用 |

---

## 4. skill.yml 的 `interface:` 扩展

### 4.1 新 schema（增量、可选）

在现有字段（`name/version/description/prompt/requires/examples/enabled`，见 [assignment-grader/skill.yml](../agentexample/skills/assignment-grader/skill.yml)）之上，**新增可选** `interface:` 段：

```yaml
name: assignment-grader
version: 0.2.0
description: ...
prompt: |
  ...
requires:
  tools: [ReadFile, WriteFile, ListFiles, SearchContent, KBSearch, KBList]
  mcp_scopes: []

# ── 新增：形式契约（全部可选；缺省则退化为今天行为）──
interface:
  input_type:  Str                  # τ_in，默认 Str
  output_type: Json                 # τ_out，默认 Str；可为 Str/Int/Float/Bool/Json/Any
  effect_hint: io                   # 效果上界声明 pure|state|io|llm，默认由 requires 推断
  state_keys: []                    # STATE 效果涉及的 memory key（用于 effect 精化）
  guard:                            # 验收谓词（缺省 = 恒真，不验收）
    kind: rule                      # rule | judge | none
    predicate: "'review_report' in x or 'verdict' in x or '建议总评' in x"
    retry: 1                        # 失败重试次数（k = 1 + retry）
    on_fail: last                   # last（返回末次结果）| error（抛 ValidationError）
  cost_hint:                        # 成本先验（可选，用于无历史数据时的估算锚点）
    tokens: 1200
    latency: 6.0
    p_useful: 0.85                  # 单次产出通过验收的概率
    p_fatal: 0.02                   # 单步致命失败率

  # ── 约束型 skill（§3.5 Restrict 组合子）；与上面注入型字段互斥使用 ──
  restrict:                         # 存在则该 skill 编译为 Restrict 而非 Skill
    effect_ceiling: io              # 效果上界封顶 pure|state|io|llm（effect_meet）
    allow_tools: [ReadFile, ListFiles]   # 工具白名单（与 agent 原工具取交）；缺省=不缩
    deny_patterns:                  # 工具调用守卫 H_r：命中则 ask/deny
      - regex: 'rm\s+-rf'
        action: ask                 # ask | deny
      - regex: 'DROP\s+TABLE'
        action: deny

examples: [...]
enabled: true
```

> **互斥约定**：一个 skill 要么是注入型（有 `prompt`/`requires`/`interface.guard`），要么是约束型（有 `interface.restrict`）。同时出现 → `validate_skill` 报错。约束型 skill 的 `prompt` 可为空。

### 4.2 字段语义与默认

| 字段 | 类型 | 默认 | 含义 |
|---|---|---|---|
| `interface.input_type` | LamType 名 | `Str` | 编译为 `AgentType.input_type`，参与 `is_subtype` 组合检查 |
| `interface.output_type` | LamType 名 | `Str` | 同上，输出类型 |
| `interface.effect_hint` | `pure\|state\|io\|llm` | 由 `requires` 推断 | 声明的效果上界；实际效果取 `max(声明, 推断)` |
| `interface.state_keys` | `[str]` | `[]` | 非空时引入 `STATE(keys)` 效果，触发 `Memory` 包裹 |
| `interface.guard.kind` | `rule\|judge\|none` | `none` | rule=受限 DSL 谓词；judge=LLM-judge（复用 pipeline 的 default_judge）；none=不验收 |
| `interface.guard.predicate` | str | — | `kind=rule` 时的谓词表达式（**受限 DSL，见 §4.3**） |
| `interface.guard.retry` | int | `0` | Guard 重试次数 |
| `interface.guard.on_fail` | `last\|error` | `last` | 验收始终失败时的兜底 |
| `interface.cost_hint.*` | num | 见 §5.3 | 无历史数据时 `estimate_cost` 的锚点 |
| `interface.restrict.effect_ceiling` | `pure\|state\|io\|llm` | 无 | 约束型：效果上界封顶（`effect_meet`，§3.5） |
| `interface.restrict.allow_tools` | `[str]` | 无（不缩） | 约束型：工具白名单，与 agent 原工具取交 |
| `interface.restrict.deny_patterns` | `[{regex, action}]` | `[]` | 约束型：工具调用守卫 H_r，`action ∈ {ask, deny}` |

### 4.3 guard.predicate 的受限 DSL

**不得使用 Python `eval`**。复用 PRODUCT_GATE_DESIGN.md 的受限 gate DSL 求值器（AST 白名单 + `has/count/contains/regex/json_len`），变量 `x` 绑定到 agent 输出。安全要求与现有 gate 一致：

- 仅允许白名单 AST 节点（比较、布尔、成员、`in`、字符串方法子集）；
- regex 带长度上限 + 窗口缓解（防 ReDoS）；
- 求值异常 → 判 `False`（验收不通过），不得吞成 `True`。

`kind=judge` 时复用 pipeline 的 `default_judge(JudgeRequest)`（本地 ollama 默认），阈值默认 0.7，可在 `guard` 下加 `threshold` 覆盖。

### 4.4 校验扩展

`validate_skill`（[skill_registry.py:101](../agentpaas/src/agentpaas/engine/skill_registry.py)）增量校验：

- `input_type/output_type` ∈ {Str,Int,Float,Bool,Json,Any,None,Tuple,Union}（解析失败 → 报错）；
- `effect_hint` ∈ {pure,state,io,llm}；
- `guard.predicate` 静态校验（AST 白名单 + regex 长度），不通过 → 报错（同 gate 静态校验）；
- `state_keys` 非空但 `effect_hint=pure` → 报错（自相矛盾）。
- **互斥**：`interface.restrict` 与（`prompt` 非空 / `requires.tools` 非空 / `interface.guard`）同时出现 → 报错（§3.5/§4.1 互斥约定）。
- `restrict.deny_patterns[].regex` 同 §4.3 受限 DSL 的 regex 约束（长度上限 + ReDoS 缓解）；`action ∈ {ask, deny}`。

现有注入扫描、name 正则、builtin 工具白名单**保持不变**。

---

## 5. 形式属性的派生规则

### 5.1 效果派生 ε_s

skill `s` 的效果上界：

```
ε_s = max_effect(
        LLM(model_A),                              -- skill 注入的 prompt 被 A 的模型消费
        io   if tools_s ∩ {IO 类工具} ≠ ∅ else pure,
        STATE(state_keys) if state_keys ≠ ∅ else pure,
        effect_hint                                -- 声明上界，取并
      )
```

实现：把 `Skill_s(A)` 当作普通 term 交给 `infer_effect_for_term`（[effects.py:309](../lambdagent/src/lambdagent/effects.py)）即可——因为 `Skill_s(A)` 展开后就是 `Guard(Memory(A'))`，三者的 effect 规则（[effects.py:330-370](../lambdagent/src/lambdagent/effects.py)）已覆盖。`effect_hint` 仅作为 `max_effect` 的额外下界，确保**声明的能力上界不被低估**。

**不变量 I-EFF**：`Skill_s(A)` 的效果 ⊒ `A` 的效果（skill 只增不减能力），用 `effect_leq(ε_A, ε_{Skill_s(A)})` 断言。对偶地，`Restrict_r(A)` 的效果 ⊑ `A` 的效果（**不变量 I-RES**，§3.5），用 `effect_leq(ε_{Restrict_r(A)}, ε_A)` 断言——二者即伽罗瓦连接的上下界。

### 5.2 成本派生 g_s

`Skill_s(A) = Guard(Memory(A'), P_s, retry)`，故：

```
g_{Skill_s(A)} = grade_guard( g_{A'}, retries = iface_s.retry )
```

其中 `g_{A'}` = `A` 注入 prompt/tools 后的 grade。`grade_guard`（[cost_grade.py:164](../lambdagent/src/lambdagent/cost_grade.py)）已实现：

```
p       = 1 - (1 - p_useful)^k,  k = 1 + retry      -- 至少一次通过验收
t,l,m   = k × (t,l,m)                               -- 重试线性放大
p_fatal 不变                                         -- Guard 不修致命错（关键诚实点）
```

整 agent 仍由 `estimate_cost(term)`（[cost_grade.py:234](../lambdagent/src/lambdagent/cost_grade.py)）一次递归得到——因为 skill 现在就是 term graph 的节点，不需要额外的"skill 成本表"。

### 5.3 cost_hint 的作用域

`estimate_cost` 对 `Lam` 的基线是固定的（800 token / 2.0s）。skill 注入的 prompt 会让真实 token 偏离基线。处理：

- 若 `interface.cost_hint` 存在 → 用它覆盖该 skill 包裹层的基线（`t=cost_hint.tokens` 等）；
- 否则用基线 + prompt 长度的线性修正 `t += len(prompt_s) // 4`（CJK 低估问题见记忆「审稿67 三连修复」，沿用 chars//4 但**仅作上界估算**）；
- `validate_cost(predicted, actual)`（[cost_grade.py:364](../lambdagent/src/lambdagent/cost_grade.py)）跑完后回填真实值，迭代收敛 cost_hint（见 §8 P2：从 trace 学习 hint）。

### 5.4 类型派生

`Skill_s(A)` 的 `AgentType`：

```
input_type  = iface_s.input_type   (默认继承 A.input_type)
output_type = iface_s.output_type  (默认继承 A.output_type)
effect      = ε_s   (§5.1)
```

组合 `[s₁, s₂](A)` 时，编译期检查 `output_type(Skill_{s₁}(A)) <: input_type(s₂)`（`is_subtype`），不满足 → 编译告警（非致命，因 skill 多为 Str→Str，宽松）。

---

## 6. 与鸿蒙 Agent DSL 的契约映射

> 目标：`interface:` 契约作为运行时无关 IR，使同一 skill 既能编译成 lambdagent term，也能编译成鸿蒙 Agent DSL（CangjieMagic `@agent`/`@prompt`/`@tool`）。映射依据见 [harmonyos-agent-dsl-comparison.md](harmonyos-agent-dsl-comparison.md)。

### 6.1 结构映射表

| lambdagent skill `interface` | 鸿蒙 Agent DSL / CangjieMagic | 说明 |
|---|---|---|
| `prompt_s`（受限边界包裹） | `@prompt[pattern: APE]( action/purpose/expectation )` | skill prompt → 结构化 prompt 模式；自由文本需切成 action/purpose/expectation 三元组 |
| `requires.tools`（builtin 白名单） | `@tool[description](func ...)` | 每个 builtin 工具映射到一个端侧 `@tool` 方法；端侧无对应实现 → 标记 unsupported |
| `interface.input_type/output_type` | `func skill(input: τ_in): τ_out` | LamType → 仓颉类型（Str→String, Json→自定义 struct/JSON） |
| `interface.effect_hint` | 端侧能力清单（网络/文件/IoT 权限） | `io` → 需端侧 ability 权限；`state` → 端侧 KV/Preferences |
| `interface.guard`（rule/judge） | 端侧后处理校验函数 / 端侧小模型 judge | rule → 仓颉纯函数校验；judge → 端侧盘古小模型 |
| `interface.cost_hint` | 端侧推理预算（token/延迟） | 用于端侧模型选择（小模型 vs 云端回退） |
| `@agent[model]` | `model_A` | skill 本身无 model，继承宿主 agent 的 model |

### 6.2 可行性检查（编译期判定）

把"这个 skill 能不能在端侧跑"变成可判定问题：给端侧一个**能力配置** `Caps_device = (ε_device_max, g_device_budget, tools_device)`，判定：

```
portable(s, device) ⟺
    effect_leq(ε_s, ε_device_max)                 -- skill 效果不超过端侧允许
  ∧ tools_s ⊆ tools_device                         -- 所需工具端侧都有实现
  ∧ grade_leq(g_s, g_device_budget)                -- 成本不超端侧预算（token/延迟/钱）
```

`grade_leq` 定义为逐分量 ≤（`t≤t' ∧ l≤l' ∧ m≤m'`，且 `p≥p'_min`）。任一条不满足 → **编译期报告"端侧不可移植"及具体缺口**，而非端侧运行时炸。这是形式化相对于"直翻 DSL"的核心价值。

### 6.3 降级策略

`portable(s, device)` 为假时的自动降级建议（codegen 产出告警 + 选项）：

- 工具缺失 → 端侧调云端 MCP 回退（牺牲端侧自治，`effect_hint` 升至 `io` 远程）；
- 成本超预算 → 换更小端侧模型 + 收紧 `guard.retry`；
- 效果超限 → 拒绝移植，要求人工裁剪 skill 能力。

### 6.4 与 CangjieMagic 的对齐点

CangjieMagic（仓颉原生 Agent 框架，MCP 原生）已有 `@agent/@prompt/@tool` 三件套但**无形式化安全保障**（[harmonyos-agent-dsl-comparison.md:118](harmonyos-agent-dsl-comparison.md)）。本设计的 `interface:` 契约正是它缺的那层——可作为「给 CangjieMagic skill 加类型/效果/成本契约」的上游 IR，是差异化的研究/工程卖点。

---

## 7. 兼容与迁移

### 7.1 向后兼容

- 无 `interface:` 段的旧 skill：编译为 `Skill_s(A) = Memory(A')`（无 Guard，恒等验收），行为等价今天的 `mount_into_config`（§3.2 形式保证）。
- API（`/skills` CRUD）、存储路径（`{data_dir}/skills/<name>/skill.yml`）、注入扫描、权限 diff **全部不变**。

### 7.2 迁移路径

1. P0：`mount_into_config` 内部改为构造 `Skill_s` 组合子节点，但**输出仍是等价的 config**（保证零行为变化），同时返回 skill 的 term 句柄供 cost/effect 查询。
2. P1：开放 `interface:` 段，老 skill 逐个补 guard/类型。
3. 给现有 11 个内置 skill 补 `interface:`（assignment-grader 的 guard 已经隐含在 prompt 里，抽出来即可）。

### 7.3 脚本型 skill（OpenClaw/Claude）normalize（后续）

OpenClaw/Claude 的 SKILL.md + scripts + workflow 比 prompt skill 重。normalize 思路（不在本期实现，仅记录）：

- SKILL.md frontmatter → `name/description/examples`；
- SKILL.md 正文 → `prompt`；
- 脚本调用 → 包装成 builtin Tool 或 MCP scope，进 `requires`；
- workflow 步骤 → 若线性则 `Compose`，若带验收则每步 `Guard`。
- 由此脚本型 skill 也获得 `interface:` 契约 → 可走 §6 的鸿蒙移植判定。

---

## 8. 实施分期与验收

| 期 | 范围 | 验收 |
|---|---|---|
| **P0** 内核抬升 | `Skill : Term → Term` 组合子；`mount` 改造为构造组合子但输出等价 config | 回归：所有现有 skill 挂载后 config 字节级等价；新增 `estimate_cost(Skill_s(A))` / `infer_effect_for_term(Skill_s(A))` 返回非平凡值的单测 |
| **P1** interface 段 | skill.yml `interface:` 解析 + 校验 + Guard 编译；受限 DSL 谓词复用 gate 求值器 | 单测：guard 谓词命中/不命中、retry 计数、on_fail；`validate_skill` 拒绝非法类型/注入谓词/注入-约束互斥 |
| **P1b** Restrict 组合子 | `Restrict : Term → Term` + `min_effect`/`effect_meet`；`restrict:` 解析；工具调用守卫复用 dangerousCommandBlock | 单测：I-RES 不变量（`effect_leq(ε_Restrict, ε_A)`）、工具面取交、deny_patterns 命中 ask/deny；把 gstack `careful` normalize 成 `restrict:` 并验证拦截 |
| **P2** 成本闭环 | `cost_hint` 估算 + `validate_cost` 回填学习 | live 测：assignment-grader 实跑，predicted vs actual 在 2× 阈值内 |
| **P3** 鸿蒙映射 | `interface → 鸿蒙 Agent DSL` codegen + `portable(s,device)` 检查 | 给定一个 device caps，对内置 skill 输出可移植/不可移植报告 + Cangjie 代码骨架 |

### 8.1 回归基线（P0 硬门槛）

- `test_skill_mount_equivalence`：对每个内置 skill，`mount_into_config` 新旧实现的 config 输出 deep-equal。
- `test_skill_term_cost`：`estimate_cost` 对挂 skill 与不挂 skill 的 agent 给出 `g_with ≥ g_without`（单调）。
- `test_skill_effect_monotone`：`effect_leq(ε_without, ε_with)`（I-EFF）。

---

## 9. 形式化对齐（论文角度）

- skill = term 组合子 `Term → Term`，是 Paper III §Guard/§Effect 的应用扩展，几乎不引入新原语（复用 `Guard`/`Memory`/`max_effect`/`grade_guard`，仅补对偶的 `min_effect`）。
- **注入 `Skill` 与约束 `Restrict` 构成效果格上的伽罗瓦连接**：agent 最终能力 `ε_final` 被可证地夹在 `[Restrict 下界, Skill 上界]`。这是一条干净的"能力代数"结果，把"压住 LLM 不确定性"从输出验收推进到工具调用层的静态能力封顶——是本工作相对纯 prompt 工程最硬的形式化卖点。
- 可移植性判定 `portable(s, device)` 是 effect 子类型 + grade 偏序的联合判定，属于"带资源语义的能力移植"——契合 AgentOS 定位（见记忆「AgentOS 定位策略」）。`Restrict` 通过降低效果上界反而**增大**可移植性（R7），是端侧降级的形式化手段。
- 候选论文角度：**"Portable Agent Skills with Cost/Effect Contracts"**——skill 作为带契约的可移植能力，端侧/云端统一 IR。可作 Paper34（OOPSLA 全文）的一个实证案例，或独立 vision。

---

## 10. 开放问题（评审点）

- **R1（§3.3）** 多 skill 的 Guard：嵌套 `Guard(Guard(...))` vs 合并单层合取 `P₁ ∧ P₂`？嵌套语义更直观（每 skill 独立验收+重试），但 retry 成本相乘可能爆炸（`k₁ × k₂`）。倾向：默认嵌套，提供 `guard.merge: and` 选项合并。
- **R2（§5.1）** `effect_hint` 取 `max(声明, 推断)` 是否过严？若 skill 声明 `io` 但实际从不调工具，会高估效果，导致 §6.2 误判不可移植。缓解：以推断为主，`effect_hint` 仅作上界校验（声明 < 推断时报错）。
- **R3（§5.3）** CJK token 估算 `chars//4` 已知低估（记忆「审稿67 三连修复」）。cost_hint 缺省时是否要求 skill 作者必填，避免 Guard 重试把低估放大 k 倍？
- **R4（§4.3）** guard `kind=judge` 引入 LLM 调用 → skill 自身有了 LLM 效果与成本，需计入 `g_s`（`grade_guard` 当前假设 validator 零成本）。是否复用 PRODUCT_GATE 的 `build_judge_term` 把 judge 也折进 term 图计成本？
- **R5（§6.1）** 自由文本 prompt → 鸿蒙 `@prompt[pattern]` 三元组（action/purpose/expectation）需要结构化，非平凡。是否要求新 skill 的 prompt 也写成三元组结构以利移植？
- **R6（§3.5）** `Restrict` 组合顺序：默认最外层（注入后统一封顶）能保证约束不被突破，但牺牲了分层授权（"先严后宽"的中间放开）。是否需要允许 `Restrict` 嵌在中间，代价是失去"最终能力 ≤ 全局下界"的简单不变量？
- **R7（§3.5/§6.2）** `Restrict.effect_ceiling` 砍效果后，§6.2 的 `portable(s, device)` 判定如何与之交互？约束型 skill 反而**增大**可移植性（效果更低 → 更易满足端侧上界），可作端侧降级（§6.3）的形式化手段——值得在鸿蒙映射里专门利用。

---

## 附：受影响文件清单（预估）

| 文件 | 改动 |
|---|---|
| `agentpaas/src/agentpaas/engine/skill_registry.py` | `mount_into_config` 构造组合子；`validate_skill` 增 interface 校验 |
| `lambdagent/src/lambdagent/skills.py` 或新 `skill_term.py` | `Skill` 与 `Restrict` 两个 `Term → Term` 组合子实现 |
| `lambdagent/src/lambdagent/effects.py` | `infer_effect_for_term` 覆盖 Skill/Restrict 组合子；新增 `min_effect`（对偶于 `max_effect`，供 `Restrict` 的 `effect_meet`） |
| `lambdagent/src/lambdagent/cost_grade.py` | `estimate_cost` 覆盖 Skill 组合子；cost_hint 注入 |
| `agentexample/skills/*/skill.yml` | 内置 skill 补 `interface:` 段 |
| `docs/MCP_SKILL_DESIGN.md` | §3 形式化对齐回链本文档 |
| 新 `tests/test_skill_formalization.py` | §8.1 回归 |