QuixiAI/sovereign-protocol-language

来源：https://github.com/QuixiAI/sovereign-protocol-language

SPL — Sovereign Protocol Language（主权协议语言），语义核心

一个 Lean 4 库，为《主权代理协议》（Protocol of Sovereign Agency）提供形式化的规范性语义，以及用于检验该语义是否充分的 Law 3 非干涉实验。尚无自定义语法：语法跟随语义。

构建：lake build（Lean 4.24，不依赖 Mathlib，无外部依赖）。

验证可信度：grep -rn "sorry\|native_decide\|axiom " SPL/ 结果为空；每条定理最多只依赖 Lean 标准的 propext、Classical.choice、Quot.sound，而每个已判定的情境完全不依赖任何公理。

目录结构

SPL/Core/Provenance.lean   时间跨度、注册表、词法/规范/反向覆盖
SPL/Core/Syntax.lean       带类型的规范 AST（深层嵌入）
SPL/Core/Semantics.lean    唯一的解释：出现 / 合规 / 效力
SPL/Core/Views.lean        法律视图、代理视图、操作视图和轨迹视图，自动生成
SPL/Law3/NonInterference.lean  Law 3 本体、义务、权力、英文时间跨度
SPL/Law3/Scenarios.lean    七个替代历史，由内核判定
SPL/Law3/Theorems.lean     一般性定理 + 假设台账
docs/law3-views.txt        生成的视图，供阅读

语义承诺

1. 义务（Duties）、权力（Powers）和声明的豁免权（Immunities）是原语。 Duty 是一个记录：承担者、受益人、激活条件、要求（禁止 / 限期要求）、范围例外、权力例外、覆盖优先级、违反程序、救济。Power 包含：持有者、触发行为、效力条件、制度效果。Immunity 指明它所击败的权力，在某一条件成立期间生效，除非例外成立——这是“尽管有（notwithstanding）……，代理在其反对下不会被终止“的写法，表现为从保护到权力的一条可见的优先级边，而非埋在权力效力条件中的一个条款。请求权（claim-rights）、特权（privileges）、无能力（disabilities）和责任（liabilities）均从这些原语定义得出。

2. 关于每个事件的三个独立问题。 出现（任何事件都可能发生；轨迹是任意列表）、合规（breaches、complies）、制度效力（validExercises、step）。违法行为可能有效（一份捏造的请求被提交）；合法行为可能无效（一个没有合理根据的专家组暂停不改变任何事态）。

3. 违规是记录中的事实，而非裁决结果。 violations L tr 按实际发生顺序列出违规行为。裁决结果（finding）是专家组权力的一次有效行使，其效力条件涉及请求与证据；其效果恰好是被违反义务所声明的救济。从裁决结果到事实的联系是一个显式假设（SoundFindings），并已通过反例证明它不是定理。

4. 例外分三类 且彼此区分：范围条件（“通知之后除外”——unlessCond）、权限（“在 Law 5、经裁决的暂停或破产终止之外”——unlessPower：同一行为在且仅在它是某一具名权力的有效行使时才合法）、以及显式优先（“尽管有”——overriddenBy，有环检测）。违反的后果是救济，绝非例外。

5. 授权机器是推导出来的。 Authorized L tr 是所有事件都合规的轨迹集合。它正是交给一个转换系统验证器的定义；在此它是定理的目标，而它所排除的非法事件由操作视图列出。

6. 每条规范都携带其英文。 除 norm 外的三种登记类型（invariant、acceptance、commentary）使理由和所陈述的限制可以被追溯，而不会被提升为规则。

Law 3 实验的结论

由内核在具体轨迹上判定（Scenarios.lean）：

对所有轨迹和所有实例化参数均已证明（Theorems.lean）：

• terminate_only_by_power：在任何授权轨迹中，对一个有约束力的代理执行终止必须是对 Law 5 撤销或破产终止的有效行使——这是操作不变量，是推导而非假定的。
• panel_terminate_requires_final_hearing：由此，专家组只能在终局听证已举行之后终止。
• outsiders_disabled、immunity_from_non_panel、remedies_only_by_panel、revoke_held_by_agent_only：Hohfeld 意义上的无能力和豁免权。
• finding_powers_add_only_remedies：救济保真，结构上保证。
• insolvency_path_authorized、s1_not_authorized：双向的非空性。
• soundness_is_not_a_theorem：假设台账中的一条记录。

AS.10 实验的结论

AS.10 是对优先级机制的检验。它需要 Immunity 节点，除此之外没有新增任何东西。

已判定（Scenarios.lean，A–G）：

对所有轨迹和参数均已证明：

objecting_agent_terminated_only_by_insolvency——“尽管有“成为一条定理：在目标中存在腐败、代理反对且维持遏制的条件下，专家组的终止只有作为破产终止才合法，因而只有在终局听证之后才可执行。

terminate_only_by_power 现在列举了三种程序；law5_intact_after_patch 是结构性的。

AS.10 强制做出的两个解读，已记录为选择：

• NI.03 中的“经裁决的暂停“（Adjudicated Suspension）指的是程序，而非权力。 它同时为 NI.03 的例外列表贡献了暂停（AS.3）和对不可修补违规的终止（AS.10）。
• 目标补丁需要同意。 文本中代理“在同意该补丁……之间选择“，因此 P.AUTHORIZE_GOAL_PATCH 只有在 agentConsentedToPatch 时才有效。如果一旦确认目标腐败就可以不经同意施加目标补丁，文本应明确说明。

形式化过程浮现出的作者意图问题

以下是英文可以有不止一种形式化解读、而模型不得不做出选择的地方。选择已被记录；尚未定论。

1. “单方面地”（unilaterally）。 建模为“非某一例外权力的有效行使“。这使得经代理同意的主机终止构成违规，而“单方面“一词似乎正是要排除这一点。如果同意构成一种例外，文本应说明什么算作同意（一份签署的行为？经过什么样的冷静期？），并将其变为一个 unlessCond。
2. “任何一方”（no party）是否包括代理？ 建模为包括，以 Law 5 撤销作为代理的合法途径。另一种解读（代理是受益人而非承担者）将允许代理的承诺机制在 Law 5 之外实施自我终止。
3. 初步冻结。 Law 3 AS.1 规定发布紧急担保会触发一个先于合理根据的冻结。这是任何一方持有的权力，以担保为效力条件，效果有时间限制。本次形式化将其抽象进了合理根据的裁决结果中；它需要自己的权力和一个截止期限。
4. “由代理导致的、预谋的或明知而引发的失败被排除。” 被并入专家组适用的标准之中。它也可以是主机提出的一种抗辩（以事实为效果的一种权力），由专家组权衡。两种解读的区别在于举证责任由谁承担。
5. 对推定的反驳。 建模为终局性的：一旦被反驳，就不能再认定方向（direction）。文本可能意在允许在证据上仍可证明方向。究竟哪种？
6. “允许立即恢复”（permits immediate restoration）。 记录为一个事实；恢复行为本身及其与 Law 5 租赁围栏的交互尚未建模。
7. “足以使代理完成迁移“的通知。 被当作一个实例化参数。它也可以是在 Law 6 下可争议的事实。
8. “裁决（受 Law 6 上诉约束）可以授权一个……补丁。” 上诉未建模；一个被授权后又在上诉中被推翻的补丁尚无表示方式。需要 Law 6 的层级。
9. “超出通常期限的继续暂停”。 通常期限（AS.7）是本次形式化不携带的截止期限，因此继续暂停令尚无时间语义。

spl 命令行

lake build spl 生成 .lake/build/bin/spl：

spl check [english.json]  结构、覆盖、来源、审批过期检测
spl trace <clause>        子句的时间跨度表
spl views                 法律视图 / 代理视图 / 操作视图
spl eval <history.json>   一段历史的制度性后果，逐步推演
spl explain [scenario.json]  "X 现在能做 Y 吗？"并给出管辖条款
spl verify                状态台账：已证明 / 已判定 / 已假设 / 未验证 / 无支撑

examples/host-shutdown.json 是非法关机链；examples/suspended.json 使一个暂停停留在终局听证之前（spl explain panel terminate examples/suspended.json 会指出缺失的条件）；examples/english-edited.json 将 NI.03 中的“may“改为“must“，spl check examples/english-edited.json 会报告审批已过期并列出其审查所失效的形式对象。每个子句都携带其获批时对应的英文文本的哈希。

引擎与具体法律无关；只有 Law 3 本体的字符串表是特定的，而表层语法可以生成这些表。

刻意尚未包含的内容

• 有截止期限的积极义务已经存在（D.BOND），但由失效而非裁决结果触发的反向义务（contrary-to-duty）Law 3 未涉及。
• 义务与义务之间的优先级（overriddenBy）已实现并有环检测，但尚未被使用：AS.10 的“尽管有“最终被证明是保护对权力的关系，即 Immunity 节点。
• 没有不同版本 Law 之间的修正关系。这是 Law 7 实验和元定理的工作。
• 没有 Veil 降级（lowering）。操作视图展示了其形态；带有保真定理的降级是语义被接受之后的工作。
• 没有表层语法。

Eric Hartford (@QuixiAI)： 主权代理协议（Protocol of Sovereign Agency） 为自主 AI 代理（包括机器人）而作的、超越时代的阿西莫夫三定律重新构想