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

状态：草案 v0.1（待评审）作者：lambdagent 团队日期：2026-06-14 关联：MCP_SKILL_DESIGN.md（现状 P2 prompt skill）、PRODUCT_GATE_DESIGN.md（gate=Guard 形式化）、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）：

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）算不出"挂这个 skill 多花多少 token / 钱"；
infer_effect_for_term(term)（effects.py:309）看不到 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	效果上界 ε_s
`CostGrade` + `grade_*` + `estimate_cost`	cost_grade.py:37	成本天花板 g_s
`AgentType (τ₁ →^ε τ₂)` + `is_subtype`	`lam_types.py`	输入/输出契约
`Guard(agent, validator, retry, on_fail)`	extensions.py:146	验收谓词 P_s

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

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

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

类	真实样例	形态	载体	实际是什么	对效果的作用
A 声明 prompt	`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 的包裹文案与注入扫描，语义不变）。
A ⊕ tools_s：把 tools_s 并进 A 的 localTools（沿用 skill_registry.py:228-235 的高风险工具不自动授予规则）。
Memory(·)：复用 extensions.py:109，若 skill 不需要持久态可退化为恒等包裹（无 STATE 效果）。
Guard(·, P_s, ...)：复用 extensions.py:146。若 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）计成本。

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 补 min_effect（对偶于 max_effect，effects.py:244）。
tools_allow：允许工具白名单；A 原有但不在白名单的工具被移出 localTools。
H_r：工具调用守卫，对应 careful 的 hooks.PreToolUse（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	输出验收+重试	不变	二者复用

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

4.1 新 schema（增量、可选）

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

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）增量校验：

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）即可——因为 Skill_s(A) 展开后就是 Guard(Memory(A'))，三者的 effect 规则（effects.py:330-370）已覆盖。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）已实现：

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）一次递归得到——因为 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）跑完后回填真实值，迭代收敛 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。

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）。本设计的 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 迁移路径

P0：mount_into_config 内部改为构造 Skill_s 组合子节点，但输出仍是等价的 config（保证零行为变化），同时返回 skill 的 term 句柄供 cost/effect 查询。
P1：开放 interface: 段，老 skill 逐个补 guard/类型。
给现有 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 回归

SKILL_FORMALIZATION_DESIGN.md 31 KB Permalink History Raw

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