SKILL_FORMALIZATION_DESIGN.md 31 KB
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}两个组合子 + §4interface:/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.1max_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/highRiskConfirmationguard 机制（记忆「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（
/skillsCRUD）、存储路径（{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 回归 |